code wiki / (root) / nx_retire_onto_gate.nx
`nx_retire_onto_gate.nx` source

↩ module page · 193 lines · 13950 B
1// nx_retire_onto_gate.nx -- GATE for retire-onto-owner (global tooling, 2026-08-24). Composes the lib in-process.
2//
3// FIXTURES: the differential PROBE imports the candidate and the owner BY BASENAME through the estate's own
4// builder, so the fixtures must live where that resolver looks -- the corpus root the gatekit resolves
5// (<X>/runtime/). They are named _ro_fixture_* so any reader recognises them as transient, written at SETUP and
6// removed at the end (and at setup, so a crashed prior run cannot poison this one). The sweep fixture plane and
7// the scratch live in /tmp/nx_retire_onto_gate/.
8//
9// THE ANTI-VACUITY TOOTH: the fixture body carries a `}` inside a LINE COMMENT and a `}` inside a STRING LITERAL.
10// A naive brace matcher ends the body at the first of those, leaves the rest of the old body behind the new
11// closing brace, and the file still LOOKS rewritten -- so the tooth asserts the leftover Newton loop is GONE.
12//
13// THE PROOF TEETH: prove against a true floor-sqrt owner PASSES; against an IDENTITY owner with the same
14// signature it must report SEMANTICS-DIFFER (the signature-only rewrite would have silently changed behaviour);
15// an unbuildable candidate must report UNBUILDABLE; a two-argument function must report UNSUPPORTED. Every
16// refusal leaves the bytes untouched, and apply writes ONLY after a PASS.
17
18import "nx_syscalls.nx"
19import "nx_gate_verdict.nx"
20import "nx_retire_onto_lib.nx"
21
22const VRG_MKDIR_MODE: i64 = 0x1ff
23// sys_read_file's size-out pair (two i64) -- the shape every read below hands back
24const VRG_LP_BYTES: i64 = 16
25// the two fixture rows the sweep tooth seeds: well under one page even with absolute corpus paths
26const VRG_ROWS_CAP: i64 = 8192
27
28func vrg_dir() -> *u8 { return "/tmp/nx_retire_onto_gate" as *u8 }
29func vrg_scratch() -> *u8 { return "/tmp/nx_retire_onto_gate/plane.scratch" as *u8 }
30func vrg_plane() -> *u8 { return "/tmp/nx_retire_onto_gate/plane-" as *u8 }
31
32// corpus-root fixture paths, derived from the same resolver the probe uses
33func vrg_root_path(out: *u8, name: *u8) -> i64 {
  let root: *u8 = sys_mmap(RO_PROBE_PATH_CAP)
  if gk_corpus_root(root) == 0 { out[0] = 0 as u8; return 0 }
  var o: i64 = ro_emit(out, 0, root)
  o = ro_emit(out, o, name)
  out[o] = 0 as u8
  return 1
40}
41func vrg_owner_src() -> *u8 {
  return "// _ro_fixture_owner.nx -- TRANSIENT gate fixture (nx_retire_onto_gate); safe to delete\nfunc sh_isqrt(v: i64) -> i64 { if v <= 0 { return 0 } var x: i64 = v; var y: i64 = (x + 1) / 2; while y < x { x = y; y = (x + v / x) / 2 } return x }\nfunc sh_ident(v: i64) -> i64 { return v }\nfunc sh_two(a: i64, b: i64) -> i64 { return a + b }\nfunc sh_sub2(a: i64, b: i64) -> i64 { return a - b }\nfunc sh_ret(v: i64) -> u8 { return v as u8 }\n" as *u8
43}
44func vrg_cons_src() -> *u8 {
  return "// _ro_fixture_cons.nx -- TRANSIENT gate fixture (nx_retire_onto_gate); safe to delete\nimport \"nx_syscalls.nx\"\n\nfunc fx_isqrt(n: i64) -> i64 {\n    if n <= 0 { return 0 }\n    // a brace in a comment } must not end the body\n    let s: *u8 = \"}\" as *u8\n    var x: i64 = n\n    var y: i64 = (x + 1) / 2\n    while y < x { x = y; y = (x + n / x) / 2 }\n    return x\n}\nfunc fx_other(n: i64) -> i64 { return n + 1 }\nfunc fx_add2(a: i64, b: i64) -> i64 { let s: i64 = a + b; return s }\n" as *u8
46}
47func vrg_broken_src() -> *u8 {
  return "// _ro_fixture_broken.nx -- TRANSIENT gate fixture (nx_retire_onto_gate); deliberately does not compile\nfunc fb_isqrt(v: i64) -> i64 { return vrg_no_such_symbol(v) }\n" as *u8
49}
50func vrg_read(path: *u8, lp: *i64) -> *u8 {
  let b: *u8 = sys_read_file(path, lp)
  if (b as i64) == 0 { lp[0] = 0 - 1 }
  return b
54}
55
56func main() -> i64 {
  let c: *i64 = gv_ctr()
  gv_head("NX-RETIRE-ONTO-GATE -- retire a private function onto its shared owner: rewrite, proof, refusals, sweep" as *u8)
  sys_mkdir(vrg_dir(), VRG_MKDIR_MODE)
  let owner: *u8 = sys_mmap(RO_PROBE_PATH_CAP)
  let cons: *u8 = sys_mmap(RO_PROBE_PATH_CAP)
  let broken: *u8 = sys_mmap(RO_PROBE_PATH_CAP)
  let have_root: i64 = vrg_root_path(owner, "_ro_fixture_owner.nx" as *u8)
  vrg_root_path(cons, "_ro_fixture_cons.nx" as *u8)
  vrg_root_path(broken, "_ro_fixture_broken.nx" as *u8)
  gv_puts("  corpus fixtures: " as *u8); gv_puts(cons); gv_puts("\n" as *u8)
  gv_subjects("corpus-root-resolved" as *u8, have_root, c)
  // idempotent setup: a crashed prior run must not poison this one
  gk_rm(owner); gk_rm(cons); gk_rm(broken)
  gk_write(owner, vrg_owner_src())
  gk_write(cons, vrg_cons_src())
  gk_write(broken, vrg_broken_src())
  let lp: *i64 = sys_mmap(VRG_LP_BYTES) as *i64
  let before: *u8 = vrg_read(cons, lp)
  let nb: i64 = lp[0]
  gv_puts("  fixture bytes=" as *u8); gv_num(nb); gv_puts("\n" as *u8)
  gv_subjects("fixture-bytes-examined" as *u8, nb, c)
78
  // ---- dry: signature check only, no probe, no write ----
  let cd: i64 = ro_one(cons, "fx_isqrt" as *u8, owner, "sh_isqrt" as *u8, RO_MODE_DRY, 0)
  let lp1: *i64 = sys_mmap(VRG_LP_BYTES) as *i64
  let after_dry: *u8 = vrg_read(cons, lp1)
  let same_dry: i64 = ro_span_eq(before, 0, nb, after_dry, 0, lp1[0])
  gv_check("dry-run-reports-retirable-and-writes-nothing" as *u8, cd == RO_RETIRABLE && same_dry == 1, c)
85
  // ---- prove: the differential probe, built and run through the estate's own builder ----
  let pp: i64 = ro_one(cons, "fx_isqrt" as *u8, owner, "sh_isqrt" as *u8, RO_MODE_PROVE, 0)
  let lp1b: *i64 = sys_mmap(VRG_LP_BYTES) as *i64
  let after_prove: *u8 = vrg_read(cons, lp1b)
  let same_prove: i64 = ro_span_eq(before, 0, nb, after_prove, 0, lp1b[0])
  gv_puts("  prove vs floor-sqrt owner code=" as *u8); gv_num(pp); gv_puts(" (PROVEN=" as *u8); gv_num(RO_PROVEN); gv_puts(")\n" as *u8)
  gv_check("prove-against-a-true-floor-sqrt-owner-passes-and-writes-nothing" as *u8, pp == RO_PROVEN && same_prove == 1, c)
  let pd: i64 = ro_one(cons, "fx_isqrt" as *u8, owner, "sh_ident" as *u8, RO_MODE_PROVE, 0)
  gv_puts("  prove vs identity owner code=" as *u8); gv_num(pd); gv_puts("\n" as *u8)
  gv_check("neg-control-same-signature-different-semantics-is-refused-by-the-probe" as *u8, pd == RO_REFUSED_DIFFER, c)
  let pu: i64 = ro_one(broken, "fb_isqrt" as *u8, owner, "sh_isqrt" as *u8, RO_MODE_PROVE, 0)
  gv_puts("  prove on an unbuildable candidate code=" as *u8); gv_num(pu); gv_puts("\n" as *u8)
  gv_check("neg-control-unbuildable-candidate-is-refused-not-guessed" as *u8, pu == RO_REFUSED_UNBUILDABLE, c)
  let ps: i64 = ro_one(owner, "sh_two" as *u8, cons, "fx_other" as *u8, RO_MODE_PROVE, 0)
  gv_check("neg-control-arity-mismatch-is-refused-before-any-probe" as *u8, ps == RO_REFUSED, c)
  // ---- binary prove: the cartesian ladder ----
  let pb: i64 = ro_one(cons, "fx_add2" as *u8, owner, "sh_two" as *u8, RO_MODE_PROVE, 0)
  gv_puts("  binary prove vs a+b owner code=" as *u8); gv_num(pb); gv_puts("\n" as *u8)
  gv_check("binary-prove-against-an-equal-two-argument-owner-passes" as *u8, pb == RO_PROVEN, c)
  let pb2: i64 = ro_one(cons, "fx_add2" as *u8, owner, "sh_sub2" as *u8, RO_MODE_PROVE, 0)
  gv_check("neg-control-binary-prove-against-a-minus-b-is-refused-by-the-probe" as *u8, pb2 == RO_REFUSED_DIFFER, c)
107
  // ---- the probe path is unique per run: its name must end in the pid's digits ----
  let pn: *u8 = sys_mmap(RO_PAT_CAP)
  let pnl: i64 = ro_probe_name(pn, "fx_isqrt" as *u8)
  let lastc: i64 = pn[pnl - 1] as i64
  gv_puts("  probe name=" as *u8); gv_puts(pn); gv_puts("\n" as *u8)
  gv_check("probe-name-carries-a-pid-suffix-so-concurrent-provers-cannot-collide" as *u8, lastc >= 48 && lastc <= 57, c)
114
  // ---- the builder-exit classifier: a box refusal must never be filed against the candidate ----
  let q1: i64 = ro_build_rc_class("BUILD-ADMIT ... VERDICT=QUEUE -- one of: the D-state roster shows an I/O storm" as *u8, 71, 1)
  let q2: i64 = ro_build_rc_class("error at line 12: unresolved identifier 'vrg_no_such_symbol'" as *u8, 60, 1)
  let q3: i64 = ro_build_rc_class("SOVEREIGN build ok" as *u8, 18, 0)
  gv_check("builder-admission-refusal-classifies-as-deferred-not-unbuildable" as *u8, q1 == RO_PROVE_ADMISSION, c)
  gv_check("neg-control-compile-error-classifies-as-unbuildable-not-deferred" as *u8, q2 == RO_PROVE_UNBUILDABLE, c)
  gv_check("neg-control-clean-build-classifies-as-pass" as *u8, q3 == RO_PROVE_PASS, c)
122
  // ---- apply: probe, then write ----
  let ca: i64 = ro_one(cons, "fx_isqrt" as *u8, owner, "sh_isqrt" as *u8, RO_MODE_APPLY, 0)
  let lp2: *i64 = sys_mmap(VRG_LP_BYTES) as *i64
  let after: *u8 = vrg_read(cons, lp2)
  let na: i64 = lp2[0]
  let has_new: i64 = ro_count(after, na, "func fx_isqrt(n: i64) -> i64 { return sh_isqrt(n) }" as *u8)
  let imports: i64 = ro_count(after, na, "import \"_ro_fixture_owner.nx\"" as *u8)
  let other_ok: i64 = ro_count(after, na, "func fx_other(n: i64) -> i64 { return n + 1 }" as *u8)
  let leftover: i64 = ro_count(after, na, "while y < x" as *u8)
  let str_left: i64 = ro_count(after, na, "let s: *u8" as *u8)
  gv_puts("  apply code=" as *u8); gv_num(ca); gv_puts(" bytes " as *u8); gv_num(nb); gv_puts("->" as *u8); gv_num(na)
  gv_puts(" new_body=" as *u8); gv_num(has_new); gv_puts(" imports=" as *u8); gv_num(imports)
  gv_puts(" other_intact=" as *u8); gv_num(other_ok); gv_puts(" leftover=" as *u8); gv_num(leftover + str_left); gv_puts("\n" as *u8)
  gv_check("apply-after-a-passing-probe-rewrites-the-body-to-one-call-of-the-owner" as *u8, ca == RO_APPLIED && has_new == 1, c)
  gv_check("apply-inserts-the-owner-import-exactly-once-after-the-last-import" as *u8, imports == 1, c)
  gv_check("sibling-function-survives-untouched" as *u8, other_ok == 1, c)
  gv_check("anti-vacuity-brace-in-comment-and-string-did-not-truncate-the-body" as *u8, leftover == 0 && str_left == 0, c)
  let import_before_func: i64 = ro_find(after, na, 0, "import \"_ro_fixture_owner.nx\"" as *u8) < ro_find(after, na, 0, "func fx_isqrt" as *u8)
  gv_check("import-lands-before-the-first-function" as *u8, import_before_func == 1, c)
142
  // ---- idempotent ----
  let c2: i64 = ro_one(cons, "fx_isqrt" as *u8, owner, "sh_isqrt" as *u8, RO_MODE_APPLY, 0)
  let lp3: *i64 = sys_mmap(VRG_LP_BYTES) as *i64
  let again: *u8 = vrg_read(cons, lp3)
  let same_again: i64 = ro_span_eq(after, 0, na, again, 0, lp3[0])
  gv_check("second-apply-reports-already-and-bytes-are-identical" as *u8, c2 == RO_ALREADY && same_again == 1, c)
149
  // ---- neg-controls on the signature layer: every refusal leaves the bytes untouched ----
  let r1: i64 = ro_one(cons, "fx_other" as *u8, owner, "sh_two" as *u8, RO_MODE_APPLY, 0)
  let r2: i64 = ro_one(cons, "fx_nope" as *u8, owner, "sh_isqrt" as *u8, RO_MODE_APPLY, 0)
  let r3: i64 = ro_one(cons, "fx_other" as *u8, owner, "sh_nope" as *u8, RO_MODE_APPLY, 0)
  let r4: i64 = ro_one(owner, "sh_isqrt" as *u8, owner, "sh_isqrt" as *u8, RO_MODE_APPLY, 0)
  let r5: i64 = ro_one(cons, "fx_other" as *u8, owner, "sh_ret" as *u8, RO_MODE_APPLY, 0)
  let lp4: *i64 = sys_mmap(VRG_LP_BYTES) as *i64
  let after_neg: *u8 = vrg_read(cons, lp4)
  let untouched: i64 = ro_span_eq(after, 0, na, after_neg, 0, lp4[0])
  gv_check("neg-control-arity-mismatch-refuses" as *u8, r1 == RO_REFUSED, c)
  gv_check("neg-control-absent-private-function-refuses" as *u8, r2 == RO_REFUSED, c)
  gv_check("neg-control-absent-owner-function-refuses" as *u8, r3 == RO_REFUSED, c)
  gv_check("neg-control-owner-lib-as-subject-refuses" as *u8, r4 == RO_REFUSED, c)
  gv_check("neg-control-return-type-mismatch-refuses" as *u8, r5 == RO_REFUSED, c)
  gv_check("neg-control-refusals-leave-the-file-byte-identical" as *u8, untouched == 1, c)
165
  // ---- sweep over a fixture plane whose rows point at the corpus fixtures ----
  let rows: *u8 = sys_mmap(VRG_ROWS_CAP)
  var o: i64 = ro_emit(rows, 0, "cons\t" as *u8); o = ro_emit(rows, o, cons); o = ro_emit(rows, o, "\t cons fixture\t fx_isqrt fx_other\n" as *u8)
  o = ro_emit(rows, o, "owner\t" as *u8); o = ro_emit(rows, o, owner); o = ro_emit(rows, o, "\t owner fixture\t sh_isqrt sh_ident sh_two sh_ret\n" as *u8)
  rows[o] = 0 as u8
  gk_write(vrg_scratch(), rows)
  var seeded: i64 = 0 - 1
  let lk: i64 = sts_lock(vrg_plane())
  if lk >= 0 { seeded = sts_seed(vrg_plane(), rows, o); sts_unlock(lk) }
  gv_puts("  fixture plane rows seeded=" as *u8); gv_num(seeded); gv_puts("\n" as *u8)
  gv_check("fixture-plane-seeded-two-rows" as *u8, seeded == 2, c)
  let tally: *i64 = sys_mmap(RO_T_N * 8) as *i64
  let sw: i64 = ro_sweep(vrg_plane(), "isqrt" as *u8, owner, "sh_isqrt" as *u8, RO_MODE_DRY, tally)
  gv_puts("  sweep rc=" as *u8); gv_num(sw); gv_puts(" candidates=" as *u8); gv_num(tally[RO_T_CAND])
  gv_puts(" already=" as *u8); gv_num(tally[RO_ALREADY]); gv_puts("\n" as *u8)
  gv_check("sweep-finds-the-one-candidate-and-skips-the-owner-own-symbol" as *u8, sw == 0 && tally[RO_T_CAND] == 1, c)
  gv_check("sweep-classifies-the-retired-candidate-as-already" as *u8, tally[RO_ALREADY] == 1, c)
  let tally2: *i64 = sys_mmap(RO_T_N * 8) as *i64
  let sw2: i64 = ro_sweep("/tmp/nx_retire_onto_gate/no-such-plane-" as *u8, "isqrt" as *u8, owner, "sh_isqrt" as *u8, RO_MODE_DRY, tally2)
  gv_check("neg-control-absent-plane-refuses-rather-than-reporting-zero-candidates" as *u8, sw2 < 0, c)
186
  // ---- teardown: the corpus must not keep the fixtures (libindex would index them) ----
  gk_rm(owner); gk_rm(cons); gk_rm(broken)
  gv_check("teardown-removed-every-corpus-fixture" as *u8, gk_exists(owner) == 0 && gk_exists(cons) == 0 && gk_exists(broken) == 0, c)
190
  return gv_verdict("nx_retire_onto_gate" as *u8, c,
      "Retire-onto-owner: the rewrite, the differential proof with its three refusal classes, idempotence, the signature refusals and the plane sweep, each tooth printing what it measured." as *u8)
193}
nx_retire_onto_gate.nx source

`nx_retire_onto_gate.nx` source
