code wiki / _hdl_build / nx_gate_migrate.nx
nx_gate_migrate.nx source
↩ module page · 633 lines · 33982 B
1// nx_gate_migrate.nx -- D001 GATE-DRY MIGRATION VERIFIER (2026-07-22).
2//
3// THE DEBT: 1918 of 1996 gate organs (96%) hand-roll their verdict scaffold instead of inheriting
4// nx_gate_verdict. Every prior attempt to eat it reached for a BYTE-equivalence proof and refused,
5// because byte-identity is UNACHIEVABLE BY CONSTRUCTION here: gv_check emits " <name>: PASS" where a
6// hand-rolled row emits " <name> PASS", and gv_verdict reformats the summary line entirely. The wrong
7// oracle -- not a hard problem -- is why D001 never moved.
8//
9// THE SOUND ORACLE = JUDGE-EQUIVALENCE, 4 clauses, measured before vs after in the SAME environment:
10// (a) exit code identical -- the gate still passes/fails the same way
11// (b) judge verdict identical -- gg_line_green(last "verdict=" line, "GREEN") agrees.
12// We COMPOSE nx_gate_green (the ecosystem's ONE judge) rather than reimplement it: the migration
13// is sound exactly when the thing that JUDGES gates cannot tell the difference.
14// (c) PASS/FAIL vector identical -- same checks, same results, same counts
15// (d) evidence side-effect preserved -- OPTIONAL, only when the caller names the file; when
16// absent it is reported UNCHECKED, never silently assumed clean (self-ceiling law L011).
17// Byte-difference alone MUST NOT refuse -- that is the whole point (tooth T5).
18//
19// DIVISION OF LABOUR (deliberate): the EDIT is semantic and belongs to the gate's owner lane; the PROOF
20// is mechanizable and belongs here. So this is a VERIFIER with commit-or-restore, never an auto-editor.
21// never-brick: on ANY divergence, failed build, or harness error the ORIGINAL source is RESTORED and the
22// verdict is REFUSE. The pre-migration copy is kept (rule 13 additive) as <src>.premigrate.
23//
24// nx_gate_migrate verify <gate> <migrated-src> [evidence-file]
25// nx_gate_migrate anchor <gate> <anchored-src> -- seq585: adopt the canonical verdict= anchor
26// nx_gate_migrate probe <gate>
27// nx_gate_migrate selftest
28//
29// ANCHOR RUNG (seq585, MUST precede the DRY rung for the 953 unjudgeable gates): a gate that emits
30// PASS/FAIL + exit 0/1 but no "verdict=" line is machine-read as NOT-GREEN by gg_line_green (missing
31// anchor == failure, nx_gate_green.nx:56) -- a silent false negative. `anchor` verifies an
32// anchor-ADOPTION edit: before must have NO anchor in its output, after MUST have one, exit + PASS/FAIL
33// vector identical, and the emitted verdict must AGREE with the exit code (GREEN iff exit 0 -- an
34// anchor that lies about the exit is worse than no anchor). Same commit-or-restore as verify.
35// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
36import "nx_syscalls.nx"
37import "nx_gate_verdict.nx"
38import "nx_gate_green.nx"
39import "nx_tool_run.nx"
40
41const GM_CAP: i64 = 262144
42const GM_PATH: i64 = 512
43const GM_RES: i64 = 64
44const GM_MODE: i64 = 0x1a4
45// GM_BUILDER was "_offc/nx_buildonly.elf" -- a thin wrapper that is NOT staged in the NAS buildroot/_offc
46// (only its source exists), so every NAS-side build died at execve-127 = harness error. Call the canonical
47// builder directly: it is present in BOTH _offc trees, so the factory no longer depends on an unstaged shim.
48const GM_BUILDER: *u8 = "_offc/nx_sov_build_run.elf"
49const GM_BUILDONLY: *u8 = "--build-only"
50// A root is VALID iff the gate base class this organ migrates TOWARD lives in it. Named, not magic (rule 11).
51const GM_ROOTMARK: *u8 = "runtime/nx_gate_verdict.nx"
52const GM_ROOTALT: *u8 = "buildroot"
53// Builder output dir (cwd-relative, same as the builder itself); GM_ARTALT is the pre-wrapper fallback.
54const GM_ARTDIR: *u8 = "_build/"
55const GM_ARTALT: *u8 = "/tmp/"
56// THE VERIFIER MUST NOT BE HANGABLE BY THE THING IT VERIFIES. Ported from ws=gate-dry-d001 (debt
57// 1785524287/1785524306), which measured a 20-gate batch making ZERO progress for THIRTY MINUTES on one
58// unbounded verify. gm_build/gm_run drive ~2800 UNKNOWN binaries, so an unbounded wait is a guaranteed
59// eventual stall; nx_tool_run documents the bounded twins in its OWN header and they were simply never
60// adopted here -- the adoption gap, in the one organ whose job is running unknown code.
61const GM_BUILD_MS: i64 = 300000
62const GM_RUN_MS: i64 = 120000
63const GM_USAGE: i64 = 2
64const GM_REFUSE: i64 = 3
65const GM_HARNESS: i64 = 4
66// one i64 scratch slot (tr_run_capture's outlen out-param). NOT a bare 16: sizing this by hand is the
67// exact class that produced the pipe2 fd-unpack hang -- name it once, never re-derive it at a call site.
68const GM_SLOT: i64 = 16
69const GM_UNCHECKED: i64 = 0 - 1
70// ENRICHMENT (2026-08-01, debts 1785562495 / 1785562671). BEFORE enumerated NO checks, AFTER enumerates
71// some, all passing. Not divergence -- it is the improvement the migration exists to deliver, and for
72// this population it is UNAVOIDABLE: nx_gate_verdict.nx:127 REFUSES GREEN unless ctr[1] > 0, so a
73// zero-check original CANNOT be expressed on the base class while keeping its exit code. Adding checks
74// failed clause (c); adding none makes gv_verdict return RED and fails (a) and (b). BOTH DOORS WERE
75// CLOSED -- the mechanical reason the composer-generated gates and the whole non-PASS vocabulary never
76// migrated. (Sibling census nx_gate_vocab_census.nx names the VOCABULARY TRAP; this is its second horn.)
77// Same shape as the original D001 blocker one layer in: byte-equivalence was unachievable BY
78// CONSTRUCTION, and so is vector-identity for a gate that enumerates nothing.
79// ACCEPTED ONLY when (a) exit and (b) judge verdict are PRESERVED and NO FAIL appears. One-way.
80const GM_ENRICHED: i64 = 2
81// ---- the res[] contract, shared by gm_clauses (writer) and gm_report (reader). Named because a
82// cross-function index contract expressed as bare integers is a silent-miscompare waiting to happen.
83const GM_RESN: i64 = 11
84const GM_R_EXIT: i64 = 0
85const GM_R_JUDGE: i64 = 1
86const GM_R_VEC: i64 = 2
87const GM_R_EVID: i64 = 3
88const GM_R_BYTES: i64 = 4
89const GM_R_PASSA: i64 = 5
90const GM_R_PASSB: i64 = 6
91const GM_R_FAILA: i64 = 7
92const GM_R_FAILB: i64 = 8
93const GM_R_GREENA: i64 = 9
94const GM_R_GREENB: i64 = 10
95// ---- anchor-verb res[] slots (an_clauses writer / its report reader share these names)
96const GM_A_EXIT: i64 = 0
97const GM_A_VEC: i64 = 1
98const GM_A_BEFORE_CLEAN: i64 = 2
99const GM_A_AFTER_HAS: i64 = 3
100const GM_A_AGREES: i64 = 4
101const GM_ARESN: i64 = 5
102
103func gm_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
104
105func gm_cat(dst: *u8, o: i64, s: *u8) -> i64 {
106 var i: i64 = 0
107 var oo: i64 = o
108 while s[i] != (0 as u8) { dst[oo] = s[i]; oo = oo + 1; i = i + 1 }
109 dst[oo] = 0 as u8
110 return oo
111}
112
113// count non-overlapping occurrences of a NUL-terminated needle in buf[0..n)
114func gm_count(buf: *u8, n: i64, needle: *u8) -> i64 {
115 let nl: i64 = gm_slen(needle)
116 if nl == 0 { return 0 }
117 var c: i64 = 0
118 var i: i64 = 0
119 while i + nl <= n {
120 var m: i64 = 1
121 var k: i64 = 0
122 while k < nl { if buf[i+k] != needle[k] { m = 0; k = nl } else { k = k + 1 } }
123 if m == 1 { c = c + 1; i = i + nl } else { i = i + 1 }
124 }
125 return c
126}
127
128func gm_write_file(path: *u8, buf: *u8, n: i64) -> i64 {
129 let fd: i64 = sys_openat_wr(path, GM_MODE)
130 if fd < 0 { return 0 - 1 }
131 var w: i64 = 0
132 var go: i64 = 1
133 while go == 1 {
134 if w >= n { go = 0 } else {
135 let r: i64 = sys_write(fd, ((buf as i64) + w) as *u8, n - w)
136 if r <= 0 { go = 0 } else { w = w + r }
137 }
138 }
139 sys_close(fd)
140 if w == n { return 0 }
141 return 0 - 1
142}
143
144// copy src -> dst byte-exact; returns bytes copied or -1
145func gm_copy(src: *u8, dst: *u8) -> i64 {
146 let b: *u8 = sys_mmap(GM_CAP)
147 let n: i64 = gg_read(src, b, GM_CAP)
148 if n <= 0 { return 0 - 1 }
149 if gm_write_file(dst, b, n) != 0 { return 0 - 1 }
150 return n
151}
152
153// size of a file in bytes (0 if absent) -- used for the evidence side-effect delta
154func gm_fsize(path: *u8) -> i64 {
155 let b: *u8 = sys_mmap(GM_CAP)
156 let n: i64 = gg_read(path, b, GM_CAP)
157 if n < 0 { return 0 }
158 return n
159}
160
161// ---------- ROOT RESOLUTION -- the tree identity must be DECLARED, never inferred ----------
162// Every path in this organ is CWD-relative (runtime/_hdl_build/..., _offc/...), so WHICH TREE it edits is
163// decided entirely by where it happens to be launched -- and it never said which. That is exactly how the
164// first D001 campaign anchored 395 gates in the LOCAL nxc2 tree while the authoritative NAS warden gauge
165// never moved: two trees, one name, no declaration. Resolve a root, chdir to it, and PRINT the answer so a
166// caller can never again be wrong about which corpus was edited.
167// Fail-fast (rule 20): no corpus root => REFUSE, never silently operate on whatever the cwd happens to be.
168func gm_root_ensure() -> i64 {
169 let probe: *u8 = sys_mmap(GM_CAP)
170 if gg_read(GM_ROOTMARK, probe, GM_CAP) > 0 { gv_puts("GATE-MIGRATE root=cwd\n" as *u8); return 1 }
171 if sys_chdir(GM_ROOTALT) == 0 {
172 if gg_read(GM_ROOTMARK, probe, GM_CAP) > 0 { gv_puts("GATE-MIGRATE root=buildroot\n" as *u8); return 1 }
173 }
174 gv_puts("GATE-MIGRATE-FAIL no-corpus-root (runtime/nx_gate_verdict.nx absent in cwd and in buildroot)\n" as *u8)
175 return 0
176}
177
178// resolve <gate>.nx: _hdl_build first (bare-name builds resolve there), then runtime root
179func gm_resolve(gate: *u8, out: *u8) -> i64 {
180 var o: i64 = gm_cat(out, 0, "runtime/_hdl_build/" as *u8)
181 o = gm_cat(out, o, gate)
182 o = gm_cat(out, o, ".nx" as *u8)
183 let probe: *u8 = sys_mmap(GM_CAP)
184 if gg_read(out, probe, GM_CAP) > 0 { return 1 }
185 o = gm_cat(out, 0, "runtime/" as *u8)
186 o = gm_cat(out, o, gate)
187 o = gm_cat(out, o, ".nx" as *u8)
188 if gg_read(out, probe, GM_CAP) > 0 { return 1 }
189 return 0
190}
191
192// nx_sov_build_run --build-only emits <cwd>/_build/<target>.sov.elf. The old hardcoded "/tmp/" was a
193// stale convention from the nx_buildonly wrapper era: the gate COMPILED fine and then this resolver looked
194// for it somewhere it was never written, so every run reported execve-127 and the oracle read it as a
195// harness failure -- a built artifact judged missing. Probe the real builder output dir first, keep /tmp as
196// the back-compat fallback for any lane whose builder still writes there (rule 19).
197func gm_artifact(gate: *u8, out: *u8) -> i64 {
198 var o: i64 = gm_cat(out, 0, GM_ARTDIR)
199 o = gm_cat(out, o, gate)
200 o = gm_cat(out, o, ".sov.elf" as *u8)
201 let probe: *u8 = sys_mmap(GM_CAP)
202 if gg_read(out, probe, GM_CAP) > 0 { return o }
203 o = gm_cat(out, 0, GM_ARTALT)
204 o = gm_cat(out, o, gate)
205 o = gm_cat(out, o, ".sov.elf" as *u8)
206 return o
207}
208
209// build <gate> via the canonical builder; returns builder exit code
210func gm_build(gate: *u8) -> i64 {
211 let o: *u8 = sys_mmap(GM_CAP)
212 let ol: *i64 = sys_mmap(GM_SLOT) as *i64
213 // tr_run_capture takes a NUL-TERMINATED argv whose argv[0] is the PATH itself (nx_tool_run.nx:14).
214 // This differs from dep_run_capture (count-passing, argv[0]=first arg) as used by nx_buildonly.nx --
215 // copying that convention here would exec the builder with the target in argv[0] and compile nothing.
216 let av: *i64 = sys_mmap(GM_SLOT) as *i64
217 av[0] = GM_BUILDER as i64
218 av[1] = gate as i64
219 av[2] = GM_BUILDONLY as i64
220 av[3] = 0
221 return tr_run_capture_to(GM_BUILDER, av, o, GM_CAP, ol, GM_BUILD_MS)
222}
223
224// run the built gate, capture stdout+stderr; returns the gate's exit code
225func gm_run(gate: *u8, out: *u8, outlen: *i64) -> i64 {
226 let ap: *u8 = sys_mmap(GM_PATH)
227 gm_artifact(gate, ap)
228 return tr_run1_to(ap, 0 as *u8, out, GM_CAP, outlen, GM_RUN_MS)
229}
230
231// ---------- THE ORACLE (pure: no I/O, so it is hermetically gateable) ----------
232// res[] slots are the GM_R_* consts above (GM_R_EXIT/JUDGE/VEC/EVID/BYTES + the PASS/FAIL/GREEN pairs);
233// the names ARE the contract -- do not re-document them as integers here, that is how the two drift apart.
234// dA/dB: evidence-file byte deltas; pass -1 for BOTH to mark clause (d) UNCHECKED.
235// returns 1 = ACCEPT (all applicable clauses hold), 0 = REFUSE
236func gm_clauses(outA: *u8, nA: i64, rcA: i64, outB: *u8, nB: i64, rcB: i64, dA: i64, dB: i64, res: *i64) -> i64 {
237 var i: i64 = 0
238 while i < GM_RESN { res[i] = 0; i = i + 1 }
239
240 if rcA == rcB { res[GM_R_EXIT] = 1 }
241
242 let gA: i64 = gg_line_green(outA, nA, "verdict=" as *u8, "GREEN" as *u8)
243 let gB: i64 = gg_line_green(outB, nB, "verdict=" as *u8, "GREEN" as *u8)
244 res[GM_R_GREENA] = gA
245 res[GM_R_GREENB] = gB
246 if gA == gB { res[GM_R_JUDGE] = 1 }
247
248 let pA: i64 = gm_count(outA, nA, "PASS" as *u8)
249 let pB: i64 = gm_count(outB, nB, "PASS" as *u8)
250 let fA: i64 = gm_count(outA, nA, "FAIL" as *u8)
251 let fB: i64 = gm_count(outB, nB, "FAIL" as *u8)
252 res[GM_R_PASSA] = pA
253 res[GM_R_PASSB] = pB
254 res[GM_R_FAILA] = fA
255 res[GM_R_FAILB] = fB
256 if pA == pB { if fA == fB { res[GM_R_VEC] = 1 } }
257 // VACUITY GUARD: when NEITHER side emits a PASS or FAIL token this clause compared NOTHING, and its
258 // IDENTICAL is agreement it never observed. Found in a real ACCEPT (pass=0 fail=0). It matters because
259 // the neg-control proving this oracle bites was caught SOLELY by clause (c). Declare UNCHECKED, the
260 // same honesty clause (d) already uses. ACCEPTANCE UNCHANGED -- this changes what the tool SAYS.
261 if pA == 0 { if pB == 0 { if fA == 0 { if fB == 0 { res[GM_R_VEC] = GM_UNCHECKED } } } }
262 // ENRICHMENT: 0 checks BEFORE -> N passing checks AFTER. A vector that SHRINKS, or that gains a
263 // FAIL, remains a divergence and is still refused -- growth is not a licence to regress.
264 if pA == 0 { if fA == 0 { if pB > 0 { if fB == 0 { res[GM_R_VEC] = GM_ENRICHED } } } }
265
266 // clause (d): UNCHECKED when the caller named no evidence file -> declared, never assumed clean
267 if dA < 0 { res[GM_R_EVID] = GM_UNCHECKED } else { if dA == dB { res[GM_R_EVID] = 1 } }
268
269 var same: i64 = 0
270 if nA == nB {
271 same = 1
272 var k: i64 = 0
273 while k < nA { if outA[k] != outB[k] { same = 0; k = nA } else { k = k + 1 } }
274 }
275 res[GM_R_BYTES] = same
276
277 var ok: i64 = 0
278 var vecok: i64 = 0
279 if res[GM_R_VEC] == 1 { vecok = 1 }
280 if res[GM_R_VEC] == GM_UNCHECKED { vecok = 1 }
281 if res[GM_R_VEC] == GM_ENRICHED { vecok = 1 }
282 if res[GM_R_EXIT] == 1 { if res[GM_R_JUDGE] == 1 { if vecok == 1 { ok = 1 } } }
283 if ok == 1 { if res[GM_R_EVID] == 0 { ok = 0 } } // (d) checked AND diverged -> refuse
284 return ok
285}
286
287// ---------- ANCHOR-ADOPTION oracle (pure, hermetically gateable). res[] = GM_A_* slots.
288// ACCEPT iff: exit identical + PASS/FAIL vector identical + BEFORE emitted no anchor + AFTER emits one
289// + the AFTER verdict AGREES with the exit code (gg sees GREEN exactly when exit==0).
290func an_clauses(outA: *u8, nA: i64, rcA: i64, outB: *u8, nB: i64, rcB: i64, res: *i64) -> i64 {
291 var i: i64 = 0
292 while i < GM_ARESN { res[i] = 0; i = i + 1 }
293 if rcA == rcB { res[GM_A_EXIT] = 1 }
294 let pA: i64 = gm_count(outA, nA, "PASS" as *u8)
295 let pB: i64 = gm_count(outB, nB, "PASS" as *u8)
296 let fA: i64 = gm_count(outA, nA, "FAIL" as *u8)
297 let fB: i64 = gm_count(outB, nB, "FAIL" as *u8)
298 if pA == pB { if fA == fB { res[GM_A_VEC] = 1 } }
299 if gm_count(outA, nA, "verdict=" as *u8) == 0 { res[GM_A_BEFORE_CLEAN] = 1 }
300 if gm_count(outB, nB, "verdict=" as *u8) > 0 { res[GM_A_AFTER_HAS] = 1 }
301 let gB: i64 = gg_line_green(outB, nB, "verdict=" as *u8, "GREEN" as *u8)
302 var wantg: i64 = 0
303 if rcB == 0 { wantg = 1 }
304 if gB == wantg { res[GM_A_AGREES] = 1 }
305 var ok: i64 = 1
306 i = 0
307 while i < GM_ARESN { if res[i] != 1 { ok = 0 } i = i + 1 }
308 return ok
309}
310
311func an_report(res: *i64, accepted: i64) -> i64 {
312 gv_puts(" exit-code............ " as *u8)
313 if res[GM_A_EXIT] == 1 { gv_puts("IDENTICAL\n" as *u8) } else { gv_puts("DIVERGED\n" as *u8) }
314 gv_puts(" PASS/FAIL vector..... " as *u8)
315 if res[GM_A_VEC] == 1 { gv_puts("IDENTICAL\n" as *u8) } else { gv_puts("DIVERGED\n" as *u8) }
316 gv_puts(" before anchor-free... " as *u8)
317 if res[GM_A_BEFORE_CLEAN] == 1 { gv_puts("YES\n" as *u8) } else { gv_puts("NO (already anchored?)\n" as *u8) }
318 gv_puts(" after emits anchor... " as *u8)
319 if res[GM_A_AFTER_HAS] == 1 { gv_puts("YES\n" as *u8) } else { gv_puts("NO\n" as *u8) }
320 gv_puts(" verdict==exit........ " as *u8)
321 if res[GM_A_AGREES] == 1 { gv_puts("AGREES\n" as *u8) } else { gv_puts("LIES (anchor contradicts exit)\n" as *u8) }
322 if accepted == 1 { gv_puts("\nNX-GATE-MIGRATE verdict=GREEN ANCHORED (gate is now machine-judgeable)\n" as *u8) }
323 else { gv_puts("\nNX-GATE-MIGRATE verdict=RED REFUSED (original restored)\n" as *u8) }
324 return 0
325}
326
327// anchor: same commit-or-restore driver shape as gm_verify, with the anchor oracle
328func gm_anchor(gate: *u8, ancsrc: *u8) -> i64 {
329 let src: *u8 = sys_mmap(GM_PATH)
330 if gm_resolve(gate, src) == 0 { gv_puts("GATE-MIGRATE-FAIL cannot resolve source for gate\n" as *u8); return GM_HARNESS }
331 let probe: *u8 = sys_mmap(GM_CAP)
332 let pn: i64 = gg_read(src, probe, GM_CAP)
333 if gm_count(probe, pn, "verdict=" as *u8) > 0 {
334 gv_puts("ALREADY-ANCHORED (source emits verdict=) -- nothing to do\n" as *u8)
335 return 0
336 }
337 let bak: *u8 = sys_mmap(GM_PATH)
338 var bo: i64 = gm_cat(bak, 0, src)
339 bo = gm_cat(bak, bo, ".premigrate" as *u8)
340 let outA: *u8 = sys_mmap(GM_CAP)
341 let outB: *u8 = sys_mmap(GM_CAP)
342 let lA: *i64 = sys_mmap(GM_SLOT) as *i64
343 let lB: *i64 = sys_mmap(GM_SLOT) as *i64
344 if gm_build(gate) != 0 { gv_puts("GATE-MIGRATE-FAIL original does not build\n" as *u8); return GM_HARNESS }
345 let rcA: i64 = gm_run(gate, outA, lA)
346 // A HANGING GATE IS NOT A MIGRATION CANDIDATE, and it MUST be refused HERE rather than reach the oracle.
347 // Ported from ws=gate-dry-d001 (1785524287) TOGETHER WITH the deadlines, because bounding the runs
348 // ALONE CREATES A WORSE BUG THAN IT FIXES: if the before-run times out the after-run almost certainly
349 // does too, and two timeouts compare EQUAL on every clause -- same exit (-5), same empty output, same
350 // zero PASS/FAIL vector -- so the oracle would hand back a confident GREEN ACCEPTED for a gate nobody
351 // has ever observed run. That is the vacuous-accept class: AGREEMENT BETWEEN TWO NON-OBSERVATIONS IS
352 // NOT EVIDENCE. Never land the timeout half of this pair without this half.
353 if rcA == TR_ERR_TIMEOUT {
354 gv_puts("GATE-MIGRATE-FAIL original HANGS past the run deadline -- not a migration candidate.\n" as *u8)
355 gv_puts(" Refusing here on purpose: two timeouts would compare identical and ACCEPT, certifying\n" as *u8)
356 gv_puts(" a migration of a gate that was never once observed to run.\n" as *u8)
357 return GM_HARNESS
358 }
359 if gm_copy(src, bak) < 0 { gv_puts("GATE-MIGRATE-FAIL cannot back up original\n" as *u8); return GM_HARNESS }
360 if gm_copy(ancsrc, src) < 0 { gm_copy(bak, src); gv_puts("GATE-MIGRATE-FAIL cannot stage anchored source (restored)\n" as *u8); return GM_HARNESS }
361 if gm_build(gate) != 0 {
362 gm_copy(bak, src)
363 gm_build(gate)
364 gv_puts(" anchored source DOES NOT BUILD -> restored\n" as *u8)
365 gv_puts("\nNX-GATE-MIGRATE verdict=RED REFUSED (original restored)\n" as *u8)
366 return GM_REFUSE
367 }
368 let rcB: i64 = gm_run(gate, outB, lB)
369 let res: *i64 = sys_mmap(GM_RES) as *i64
370 let ok: i64 = an_clauses(outA, lA[0], rcA, outB, lB[0], rcB, res)
371 gv_puts("nx_gate_migrate anchor " as *u8)
372 gv_puts(gate)
373 gv_puts("\n" as *u8)
374 an_report(res, ok)
375 if ok == 1 { return 0 }
376 gm_copy(bak, src)
377 gm_build(gate)
378 return GM_REFUSE
379}
380
381func gm_report(res: *i64, accepted: i64) -> i64 {
382 gv_puts(" (a) exit-code........ " as *u8)
383 if res[GM_R_EXIT] == 1 { gv_puts("IDENTICAL\n" as *u8) } else { gv_puts("DIVERGED\n" as *u8) }
384 gv_puts(" (b) judge verdict.... " as *u8)
385 if res[GM_R_JUDGE] == 1 { gv_puts("IDENTICAL (green=" as *u8); gv_num(res[GM_R_GREENA]); gv_puts(")\n" as *u8) } else { gv_puts("DIVERGED\n" as *u8) }
386 if res[GM_R_VEC] == GM_ENRICHED { gv_puts(" (c) PASS/FAIL vector. ENRICHED -- the original enumerated ZERO checks and the base class cannot emit GREEN with zero checks, so enumerating them is the ONLY expressible migration for this population. (a)+(b) are preserved and no FAIL was introduced; one-way, a shrink or a new FAIL still refuses. The raw token comparison on the next line therefore reads DIVERGED BY DESIGN: " as *u8) } else { gv_puts(" (c) PASS/FAIL vector. " as *u8) }
387 if res[GM_R_VEC] == 1 { gv_puts("IDENTICAL pass=" as *u8); gv_num(res[GM_R_PASSA]); gv_puts(" fail=" as *u8); gv_num(res[GM_R_FAILA]); gv_puts("\n" as *u8) } else {
388 if res[GM_R_VEC] < 0 { gv_puts("UNCHECKED (gate emits no PASS/FAIL tokens -- this clause compared nothing)\n" as *u8) }
389 else { gv_puts("DIVERGED\n" as *u8) } }
390 gv_puts(" (d) evidence effect.. " as *u8)
391 if res[GM_R_EVID] < 0 { gv_puts("UNCHECKED (no evidence file named)\n" as *u8) } else {
392 if res[GM_R_EVID] == 1 { gv_puts("PRESERVED\n" as *u8) } else { gv_puts("DIVERGED\n" as *u8) } }
393 gv_puts(" ... bytes............ " as *u8)
394 if res[GM_R_BYTES] == 1 { gv_puts("identical\n" as *u8) } else { gv_puts("DIFFER (expected; byte-proof would refuse this)\n" as *u8) }
395 if accepted == 1 { gv_puts("\nNX-GATE-MIGRATE verdict=GREEN ACCEPTED (judge-equivalence holds)\n" as *u8) }
396 else { gv_puts("\nNX-GATE-MIGRATE verdict=RED REFUSED (original restored)\n" as *u8) }
397 return 0
398}
399
400// ---------- verify: the commit-or-restore driver ----------
401func gm_verify(gate: *u8, migsrc: *u8, evid: *u8) -> i64 {
402 let src: *u8 = sys_mmap(GM_PATH)
403 if gm_resolve(gate, src) == 0 { gv_puts("GATE-MIGRATE-FAIL cannot resolve source for gate\n" as *u8); return GM_HARNESS }
404 let bak: *u8 = sys_mmap(GM_PATH)
405 var bo: i64 = gm_cat(bak, 0, src)
406 bo = gm_cat(bak, bo, ".premigrate" as *u8)
407
408 let outA: *u8 = sys_mmap(GM_CAP)
409 let outB: *u8 = sys_mmap(GM_CAP)
410 let lA: *i64 = sys_mmap(GM_SLOT) as *i64
411 let lB: *i64 = sys_mmap(GM_SLOT) as *i64
412
413 // --- BEFORE ---
414 if gm_build(gate) != 0 { gv_puts("GATE-MIGRATE-FAIL original does not build -- not a migration candidate\n" as *u8); return GM_HARNESS }
415 var eA0: i64 = 0 - 1
416 var eA1: i64 = 0 - 1
417 if (evid as i64) != 0 { eA0 = gm_fsize(evid) }
418 let rcA: i64 = gm_run(gate, outA, lA)
419 // A HANGING GATE IS NOT A MIGRATION CANDIDATE, and it MUST be refused HERE rather than reach the oracle.
420 // Ported from ws=gate-dry-d001 (1785524287) TOGETHER WITH the deadlines, because bounding the runs
421 // ALONE CREATES A WORSE BUG THAN IT FIXES: if the before-run times out the after-run almost certainly
422 // does too, and two timeouts compare EQUAL on every clause -- same exit (-5), same empty output, same
423 // zero PASS/FAIL vector -- so the oracle would hand back a confident GREEN ACCEPTED for a gate nobody
424 // has ever observed run. That is the vacuous-accept class: AGREEMENT BETWEEN TWO NON-OBSERVATIONS IS
425 // NOT EVIDENCE. Never land the timeout half of this pair without this half.
426 if rcA == TR_ERR_TIMEOUT {
427 gv_puts("GATE-MIGRATE-FAIL original HANGS past the run deadline -- not a migration candidate.\n" as *u8)
428 gv_puts(" Refusing here on purpose: two timeouts would compare identical and ACCEPT, certifying\n" as *u8)
429 gv_puts(" a migration of a gate that was never once observed to run.\n" as *u8)
430 return GM_HARNESS
431 }
432 if (evid as i64) != 0 { eA1 = gm_fsize(evid) }
433 var dA: i64 = 0 - 1
434 if (evid as i64) != 0 { dA = eA1 - eA0 }
435
436 // --- SWAP (backup kept, rule 13) ---
437 if gm_copy(src, bak) < 0 { gv_puts("GATE-MIGRATE-FAIL cannot back up original\n" as *u8); return GM_HARNESS }
438 if gm_copy(migsrc, src) < 0 { gm_copy(bak, src); gv_puts("GATE-MIGRATE-FAIL cannot stage migrated source (restored)\n" as *u8); return GM_HARNESS }
439
440 // --- AFTER ---
441 let brc: i64 = gm_build(gate)
442 if brc != 0 {
443 gm_copy(bak, src)
444 gv_puts(" migrated source DOES NOT BUILD -> restored\n" as *u8)
445 gv_puts("\nNX-GATE-MIGRATE verdict=RED REFUSED (original restored)\n" as *u8)
446 return GM_REFUSE
447 }
448 var eB0: i64 = 0 - 1
449 var eB1: i64 = 0 - 1
450 if (evid as i64) != 0 { eB0 = gm_fsize(evid) }
451 let rcB: i64 = gm_run(gate, outB, lB)
452 if (evid as i64) != 0 { eB1 = gm_fsize(evid) }
453 var dB: i64 = 0 - 1
454 if (evid as i64) != 0 { dB = eB1 - eB0 }
455
456 let res: *i64 = sys_mmap(GM_RES) as *i64
457 let ok: i64 = gm_clauses(outA, lA[0], rcA, outB, lB[0], rcB, dA, dB, res)
458 gv_puts("nx_gate_migrate verify " as *u8)
459 gv_puts(gate)
460 gv_puts("\n" as *u8)
461 gm_report(res, ok)
462 if ok == 1 { return 0 }
463 gm_copy(bak, src)
464 gm_build(gate)
465 return GM_REFUSE
466}
467
468func gm_probe(gate: *u8) -> i64 {
469 let src: *u8 = sys_mmap(GM_PATH)
470 if gm_resolve(gate, src) == 0 { gv_puts("PROBE " as *u8); gv_puts(gate); gv_puts(" NO-SOURCE\n" as *u8); return GM_HARNESS }
471 let b: *u8 = sys_mmap(GM_CAP)
472 let n: i64 = gg_read(src, b, GM_CAP)
473 let inherits: i64 = gm_count(b, n, "gv_verdict" as *u8)
474 let builds: i64 = gm_build(gate)
475 let out: *u8 = sys_mmap(GM_CAP)
476 let ol: *i64 = sys_mmap(GM_SLOT) as *i64
477 var rc: i64 = 0 - 1
478 if builds == 0 { rc = gm_run(gate, out, ol) }
479 gv_puts("PROBE " as *u8)
480 gv_puts(gate)
481 gv_puts(" src_bytes=" as *u8)
482 gv_num(n)
483 gv_puts(" inherits_base=" as *u8)
484 if inherits > 0 { gv_puts("1" as *u8) } else { gv_puts("0" as *u8) }
485 gv_puts(" builds=" as *u8)
486 if builds == 0 { gv_puts("1" as *u8) } else { gv_puts("0" as *u8) }
487 gv_puts(" run_exit=" as *u8)
488 gv_num(rc)
489 gv_puts(" emits_verdict=" as *u8)
490 gv_num(gm_count(out, ol[0], "verdict=" as *u8))
491 gv_puts("\n" as *u8)
492 if inherits > 0 { return 1 }
493 if builds != 0 { return 1 }
494 return 0
495}
496
497// ---------- selftest: hermetic, exercises the ORACLE on synthetic pairs (no shared prod state) ----------
498func gm_selftest() -> i64 {
499 let ctr: *i64 = gv_ctr()
500 gv_head("nx_gate_migrate selftest -- the D001 judge-equivalence oracle (4 clauses)" as *u8)
501 let res: *i64 = sys_mmap(GM_RES) as *i64
502
503 // the REAL shapes: hand-rolled (no colon, domain verdict line) vs base class (colon, NX- summary)
504 let legacy: *u8 = "GATE x\n T1 thing PASS\n T2 other PASS\nK4GATE verdict=GREEN keystone=sv39 probe=4kpage\n" as *u8
505 let based: *u8 = "GATE x\n\n T1 thing: PASS\n T2 other: PASS\n\nNX-K4GATE passed 2/2 verdict=GREEN (keystone=sv39 probe=4kpage)\n" as *u8
506 let nl: i64 = gm_slen(legacy)
507 let nb: i64 = gm_slen(based)
508
509 let t1: i64 = gm_clauses(legacy, nl, 0, based, nb, 0, 0-1, 0-1, res)
510 gv_check("T1 real legacy-vs-base pair ACCEPTED (the migration D001 needs)" as *u8, t1, ctr)
511
512 var t5: i64 = 0
513 if res[GM_R_BYTES] == 0 { if t1 == 1 { t5 = 1 } }
514 gv_check("T5 ACCEPTED even though BYTES DIFFER (byte-proof would refuse: the whole point)" as *u8, t5, ctr)
515
516 // (a) exit divergence must refuse
517 var t2: i64 = 0
518 if gm_clauses(legacy, nl, 0, based, nb, 1, 0-1, 0-1, res) == 0 { t2 = 1 }
519 gv_check("T2 NEG exit-code divergence REFUSED" as *u8, t2, ctr)
520
521 // (b) judge divergence must refuse: same exit, but the migrated side judges RED
522 let redb: *u8 = "GATE x\n\n T1 thing: PASS\n T2 other: PASS\n\nNX-K4GATE passed 2/2 verdict=RED\n" as *u8
523 var t3: i64 = 0
524 if gm_clauses(legacy, nl, 0, redb, gm_slen(redb), 0, 0-1, 0-1, res) == 0 { t3 = 1 }
525 gv_check("T3 NEG judge divergence (GREEN->RED) REFUSED" as *u8, t3, ctr)
526
527 // (c) vector divergence must refuse: a check silently vanished
528 let lost: *u8 = "GATE x\n\n T1 thing: PASS\n\nNX-K4GATE passed 1/1 verdict=GREEN (n)\n" as *u8
529 var t4: i64 = 0
530 if gm_clauses(legacy, nl, 0, lost, gm_slen(lost), 0, 0-1, 0-1, res) == 0 { t4 = 1 }
531 gv_check("T4 NEG a check silently DISAPPEARING REFUSED (2 PASS vs 1)" as *u8, t4, ctr)
532
533 // NEG-CONTROL: a RED gate must stay RED and still be accepted (not GREEN-only reasoning)
534 let redl: *u8 = "GATE y\n T1 thing FAIL\nADGATE verdict=RED (t1=0)\n" as *u8
535 let redn: *u8 = "GATE y\n\n T1 thing: FAIL\n\nNX-ADGATE passed 0/1 verdict=RED\n" as *u8
536 var t6: i64 = 0
537 if gm_clauses(redl, gm_slen(redl), 1, redn, gm_slen(redn), 1, 0-1, 0-1, res) == 1 { t6 = 1 }
538 gv_check("T6 NEG-CONTROL RED gate stays RED and is ACCEPTED (oracle is not GREEN-only)" as *u8, t6, ctr)
539
540 // clause (d): evidence divergence refuses; absent evidence is declared UNCHECKED, never assumed
541 var t7: i64 = 0
542 if gm_clauses(legacy, nl, 0, based, nb, 0, 3, 5, res) == 0 { t7 = 1 }
543 gv_check("T7 evidence side-effect divergence (3 vs 5 bytes) REFUSED" as *u8, t7, ctr)
544
545 var t8: i64 = 0
546 gm_clauses(legacy, nl, 0, based, nb, 0, 0-1, 0-1, res)
547 if res[GM_R_EVID] < 0 { t8 = 1 }
548 gv_check("T8 absent evidence file reported UNCHECKED, not assumed-clean (L011 honesty)" as *u8, t8, ctr)
549
550 // ---- anchor-oracle teeth (seq585): the un-anchored shape is nx_aa_gate's real form
551 let noanch: *u8 = "AA gate\n T1 smooth PASS\n T2 det PASS\nAA-GATE GREEN -- ssaa\n" as *u8
552 let anched: *u8 = "AA gate\n T1 smooth PASS\n T2 det PASS\nAA-GATE verdict=GREEN -- ssaa\n" as *u8
553 let ares: *i64 = sys_mmap(GM_RES) as *i64
554 var t9: i64 = 0
555 if an_clauses(noanch, gm_slen(noanch), 0, anched, gm_slen(anched), 0, ares) == 1 { t9 = 1 }
556 gv_check("T9 anchor adoption ACCEPTED (no-anchor -> anchored, exit+vector held)" as *u8, t9, ctr)
557
558 // a LYING anchor: claims GREEN while the gate exits 1 -- worse than no anchor, must refuse
559 var t10: i64 = 0
560 if an_clauses(noanch, gm_slen(noanch), 1, anched, gm_slen(anched), 1, ares) == 0 { t10 = 1 }
561 gv_check("T10 NEG lying anchor (verdict=GREEN but exit 1) REFUSED" as *u8, t10, ctr)
562
563 let lostb: *u8 = "AA gate\n T1 smooth PASS\nAA-GATE verdict=GREEN -- ssaa\n" as *u8
564 var t11: i64 = 0
565 if an_clauses(noanch, gm_slen(noanch), 0, lostb, gm_slen(lostb), 0, ares) == 0 { t11 = 1 }
566 gv_check("T11 NEG anchor edit that drops a check REFUSED (vector 2 PASS vs 1)" as *u8, t11, ctr)
567
568 // RED gate anchored honestly: exit 1 both sides, verdict=RED (gg sees no GREEN) -> accept
569 let redna: *u8 = "AA gate\n T1 smooth FAIL\nAA-GATE RED\n" as *u8
570 let redan: *u8 = "AA gate\n T1 smooth FAIL\nAA-GATE verdict=RED\n" as *u8
571 var t12: i64 = 0
572 if an_clauses(redna, gm_slen(redna), 1, redan, gm_slen(redan), 1, ares) == 1 { t12 = 1 }
573 gv_check("T12 NEG-CONTROL RED gate anchored honestly (verdict=RED, exit 1) ACCEPTED" as *u8, t12, ctr)
574
575 // ---- ENRICHMENT teeth (2026-08-01): the zero-check population BOTH doors used to refuse.
576 // The composer-generated shape: ONE summary line, NO enumerated checks, exit 0, judged GREEN.
577 let zc: *u8 = "PIPEGATE all_ok=0 fail_at=3 steps=4 verdict=GREEN" as *u8
578 let enr: *u8 = "deployclass_gate T1 all-clean: PASS T2 abort point: PASS NX-PIPEGATE passed 2/2 verdict=GREEN (n)" as *u8
579 var t13: i64 = 0
580 if gm_clauses(zc, gm_slen(zc), 0, enr, gm_slen(enr), 0, 0-1, 0-1, res) == 1 { t13 = 1 }
581 gv_check("T13 ENRICHMENT 0 -> N passing checks ACCEPTED (base class cannot emit GREEN with zero checks, so this is the ONLY expressible migration for this population)" as *u8, t13, ctr)
582
583 let enrf: *u8 = "deployclass_gate T1 all-clean: PASS T2 abort point: FAIL NX-PIPEGATE passed 1/2 verdict=GREEN (n)" as *u8
584 var t14: i64 = 0
585 if gm_clauses(zc, gm_slen(zc), 0, enrf, gm_slen(enrf), 0, 0-1, 0-1, res) == 0 { t14 = 1 }
586 gv_check("T14 NEG enrichment that introduces a FAIL still REFUSED (growth is not a licence to regress)" as *u8, t14, ctr)
587
588 var t15: i64 = 0
589 if gm_clauses(enr, gm_slen(enr), 0, zc, gm_slen(zc), 0, 0-1, 0-1, res) == 0 { t15 = 1 }
590 gv_check("T15 NEG the REVERSE direction (N checks -> 0) REFUSED -- enrichment is ONE-WAY" as *u8, t15, ctr)
591
592 return gv_verdict("GATE-MIGRATE-GATE" as *u8, ctr, "judge-equivalence accepts byte-differing safe migrations, refuses exit/judge/vector/evidence divergence, RED stays RED; anchor rung: lying/lossy anchors refused, honest RED accepted" as *u8)
593}
594
595func main(argc: i64, argv: *i64) -> i64 {
596 if argc < 2 {
597 gv_puts("usage: nx_gate_migrate {verify <gate> <migrated-src> [evidence-file] | anchor <gate> <anchored-src> | probe <gate> | selftest}\n" as *u8)
598 sys_exit(GM_USAGE)
599 return GM_USAGE
600 }
601 let verb: *u8 = argv[1] as *u8
602 if gm_count(verb, gm_slen(verb), "selftest" as *u8) > 0 {
603 let rc: i64 = gm_selftest()
604 sys_exit(rc)
605 return rc
606 }
607 // Every corpus-touching verb must know its tree before it resolves a single path; the selftest branch
608 // above is hermetic (synthetic buffers) and deliberately needs no root, so it stays reachable anywhere.
609 if gm_root_ensure() == 0 { sys_exit(GM_HARNESS); return GM_HARNESS }
610 if gm_count(verb, gm_slen(verb), "probe" as *u8) > 0 {
611 if argc < 3 { gv_puts("probe needs <gate>\n" as *u8); sys_exit(GM_USAGE); return GM_USAGE }
612 let rc2: i64 = gm_probe(argv[2] as *u8)
613 sys_exit(rc2)
614 return rc2
615 }
616 if gm_count(verb, gm_slen(verb), "anchor" as *u8) > 0 {
617 if argc < 4 { gv_puts("anchor needs <gate> <anchored-src>\n" as *u8); sys_exit(GM_USAGE); return GM_USAGE }
618 let rca: i64 = gm_anchor(argv[2] as *u8, argv[3] as *u8)
619 sys_exit(rca)
620 return rca
621 }
622 if gm_count(verb, gm_slen(verb), "verify" as *u8) > 0 {
623 if argc < 4 { gv_puts("verify needs <gate> <migrated-src>\n" as *u8); sys_exit(GM_USAGE); return GM_USAGE }
624 var ev: *u8 = 0 as *u8
625 if argc > 4 { ev = argv[4] as *u8 }
626 let rc3: i64 = gm_verify(argv[2] as *u8, argv[3] as *u8, ev)
627 sys_exit(rc3)
628 return rc3
629 }
630 gv_puts("GATE-MIGRATE-FAIL unknown verb\n" as *u8)
631 sys_exit(GM_USAGE)
632 return GM_USAGE
633}