code wiki / _hdl_build / nx_ecomat_seed_clobber_gate.nx

nx_ecomat_seed_clobber_gate.nx source

↩ module page · 175 lines · 9135 B

1// nx_ecomat_seed_clobber_gate.nx -- proves the ANTI-CLOBBER guard in nx_ecomat_seed BITES. 2// 3// ★WHY (measured 2026-08-07). ss_commit REPLACES a plane with the write-set handed to it 4// (nx_ecomat_put.nx:66, gate-proven). nx_ecomat_seed authors its domains from SOURCE and never 5// reloads, so the moment the live plane carries a domain the source does not author, running the 6// seeder DELETES it. Measured that day: the live plane held 26 domains, the laptop source authored 7// 23 and the NAS source 22 -- so either one destroyed 3-4 domains AND REPORTED GREEN, because the 8// success check was a hardcoded `ver == N` equality that had been hand-edited down to match. 9// 10// ★THE GUARD IS KEYED ON IDENTITY, AND THIS GATE'S JOB IS TO PROVE THAT DISTINCTION IS REAL. 11// A count-based shrink refusal was built in the SHARED PRIMITIVE on 2026-08-02 and reverted before 12// promote (nx_store_seed_lib.nx:207) because it broke legitimate whole-plane rewriters. Debt 13// 1785710884 concluded such a guard belongs at the PLANE-WRITER layer. T5 below is the anti-vacuity 14// tooth for exactly that: a plane whose ROW COUNT SHRINKS but whose every NAME survives must still 15// be ALLOWED. A naive count-based reimplementation passes T1-T4 and FAILS T5, which is the point -- 16// a tooth the trivial wrong implementation can also pass proves nothing. 17// 18// Forks the REAL resolved nx_ecomat_seed.elf via ar_resolve (never a hardcoded path -- the 19// 127-vacuous lesson), so what is proven is the artifact that actually runs. T0 asserts the subject 20// was FOUND, because an absent artifact (exit 127) is indistinguishable from a passing refusal. 21// license_tier: ORIGINAL expect_exit: 0 22import "nx_ecomat_lib.nx" 23import "nx_artifact_root.nx" 24import "nx_gate_verdict.nx" 25import "nx_syscalls.nx" 26 27const EG_EXIT_REFUSED: i64 = 4 28const EG_EXIT_NOTFOUND: i64 = 127 29const EG_AUTHORED: i64 = 23 // rows the seeder authors from source; T5 needs a fixture ABOVE this 30const EG_SHRINK_ROWS: i64 = 26 // > EG_AUTHORED so T5 is a genuine count-shrink 31const EG_MODE: i64 = 420 32 33// count contiguous ecomat:dom:N records on a plane 34func eg_count(prefix: *u8) -> i64 { 35 let h: *i64 = ss_open(prefix) 36 if (h as i64) == 0 { return 0 } 37 let pq: *i64 = sys_mmap(16) as *i64 38 let lq: *i64 = sys_mmap(16) as *i64 39 var n: i64 = 0 40 var go: i64 = 1 41 while go == 1 { 42 let key: *u8 = sys_mmap(64); ec_key(n, key) 43 if ss_hget(h, key, pq, lq) == 1 { n = n + 1 } else { go = 0 } 44 } 45 return n 46} 47 48// is `name` present as a domain on the plane? 49func eg_has(prefix: *u8, name: *u8) -> i64 { 50 let h: *i64 = ss_open(prefix) 51 if (h as i64) == 0 { return 0 } 52 let pq: *i64 = sys_mmap(16) as *i64 53 let lq: *i64 = sys_mmap(16) as *i64 54 let dom: *u8 = sys_mmap(ECOMAT_DOM_CAP) 55 var n: i64 = 0 56 var found: i64 = 0 57 var go: i64 = 1 58 while go == 1 { 59 let key: *u8 = sys_mmap(64); ec_key(n, key) 60 if ss_hget(h, key, pq, lq) == 1 { 61 ec_str(pq[0] as *u8, 0, dom, ECOMAT_DOM_CAP) 62 if el_streq(dom, name) == 1 { found = 1 } 63 n = n + 1 64 } else { go = 0 } 65 } 66 return found 67} 68 69// manufacture a fixture plane holding `rows` domains all named `name` 70func eg_make(prefix: *u8, rows: i64, name: *u8) -> i64 { 71 let w: *i64 = ss_begin() 72 var i: i64 = 0 73 while i < rows { 74 if ec_seed_one(w, i, 0, 1, 2, 5, 7, 1, name, "fixture-bench" as *u8, "fixture-next" as *u8) != 0 { return 0 - 1 } 75 i = i + 1 76 } 77 if ss_commit(prefix, w, ss_next_segid(prefix)) != 0 { return 0 - 1 } 78 return rows 79} 80 81// fork the resolved seeder against `prefix`; return its exit code 82func eg_run(prefix: *u8) -> i64 { 83 let pid: i64 = sys_fork() 84 if pid == 0 { 85 let ofd: i64 = sys_openat_wr("knowledge/status/ecomat_clobber_gate.out\x00" as *u8, EG_MODE) 86 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 87 let elf: *u8 = sys_mmap(512) 88 if ar_resolve("_offc/nx_ecomat_seed.elf" as *u8, elf) == 0 { sys_exit(EG_EXIT_NOTFOUND) } 89 let av: *i64 = sys_mmap(64) as *i64 90 av[0] = elf as i64 91 av[1] = prefix as i64 92 av[2] = 0 93 let envp: *i64 = sys_mmap(16) as *i64 94 envp[0] = 0 95 sys_execve(elf, av, envp) 96 sys_exit(EG_EXIT_NOTFOUND) 97 } 98 let stp: *i64 = sys_mmap(16) as *i64 99 sys_wait4(pid, stp, 0) 100 let sig: i64 = stp[0] & 0x7f 101 if sig != 0 { return 128 + sig } 102 return (stp[0] >> 8) & 0xff 103} 104 105// PER-RUN FIXTURE PREFIX. Fixed scratch paths made this gate non-idempotent: the first NAS run was 106// killed mid-flight by /api/gate_run's 12s deadline and the NEXT run inherited its debris, scoring 107// 4/7 against the very artifact that scores 7/7 on a clean tree. A gate that is not idempotent 108// reports on its first run and lies about every run after -- and a teardown does not run when a run 109// is killed, so the isolation has to come from the NAME, not from cleanup. 110func eg_pfx(out: *u8, ep: i64, tag: *u8) -> i64 { 111 var o: i64 = ss_cat(out, 0, "/tmp/ecgclob-" as *u8) 112 o = ss_catn(out, o, ep) 113 o = ss_cat(out, o, "-" as *u8) 114 o = ss_cat(out, o, tag) 115 o = ss_cat(out, o, "-" as *u8) 116 out[o] = 0 as u8 117 return o 118} 119 120func main() -> i64 { 121 let ctr: *i64 = gv_ctr() 122 _p("=== nx_ecomat_seed_clobber_gate -- the anti-clobber guard must BITE, not merely exist ===\n" as *u8) 123 let ep: i64 = sys_now_realtime_sec() 124 let fx: *u8 = sys_mmap(160); eg_pfx(fx, ep, "dmg" as *u8) 125 let hx: *u8 = sys_mmap(160); eg_pfx(hx, ep, "ok" as *u8) 126 let sx: *u8 = sys_mmap(160); eg_pfx(sx, ep, "shrink" as *u8) 127 _p(" fixture epoch=" as *u8); _fn(1, ep); _p(" (per-run prefixes; no run can inherit another's debris)\n" as *u8) 128 129 // ---- T1: manufacture the EXACT live damage: a plane carrying a domain the source cannot author. 130 // ASSERT THE FIXTURE REACHED THE CONDITION before asserting any outcome -- a fixture the defect 131 // cannot fail is not a test. 132 let unauth: *u8 = "neg-control-unauthored-domain" as *u8 133 let made: i64 = eg_make(fx, 1, unauth) 134 let n0: i64 = eg_count(fx) 135 let present0: i64 = eg_has(fx, unauth) 136 _p(" fixture: made=" as *u8); _fn(1, made); _p(" rows=" as *u8); _fn(1, n0) 137 _p(" unauthored_present=" as *u8); _fn(1, present0); _p("\n" as *u8) 138 gv_check("T1 fixture damaged: plane carries a domain the seeder does not author" as *u8, (made == 1) & (present0 == 1), ctr) 139 140 // ---- T2: THE BITE. The seeder must REFUSE (exit 4) rather than commit its 23 over the top. 141 let rc: i64 = eg_run(fx) 142 _p(" seeder on damaged plane rc=" as *u8); _fn(1, rc); _p(" (want " as *u8); _fn(1, EG_EXIT_REFUSED); _p(" REFUSED)\n" as *u8) 143 gv_check("T0 subject resolved: not exit 127 (an absent artifact must not read as a pass)" as *u8, rc != EG_EXIT_NOTFOUND, ctr) 144 gv_check("T2 guard BITES: seeder refuses a plane holding an unauthored domain" as *u8, rc == EG_EXIT_REFUSED, ctr) 145 146 // ---- T3: the refusal changed NOTHING. A guard that refuses AND corrupts is not a guard. 147 let n1: i64 = eg_count(fx) 148 let present1: i64 = eg_has(fx, unauth) 149 _p(" after refusal rows=" as *u8); _fn(1, n1); _p(" unauthored_present=" as *u8); _fn(1, present1); _p("\n" as *u8) 150 gv_check("T3 plane untouched by the refusal: row count and the at-risk domain both survive" as *u8, (n1 == n0) & (present1 == 1), ctr) 151 152 // ---- T4: NEG-CONTROL. A plane whose every name IS authored must still be accepted, or the 153 // guard is simply refusing everything -- which passes every negative test and is worthless. 154 eg_make(hx, 2, "compiler" as *u8) 155 let rch: i64 = eg_run(hx) 156 let nh: i64 = eg_count(hx) 157 _p(" healthy-plane rc=" as *u8); _fn(1, rch); _p(" rows_now=" as *u8); _fn(1, nh); _p(" (want 0 / " as *u8); _fn(1, EG_AUTHORED); _p(")\n" as *u8) 158 gv_check("T4 neg-control: plane losing no NAME is accepted and commits the full domain set" as *u8, (rch == 0) & (nh == EG_AUTHORED), ctr) 159 160 // ---- T5: ANTI-VACUITY -- the tooth a count-based guard CANNOT pass. 161 // 26 rows in, 23 authored out: the row count SHRINKS, but every name ("compiler") survives, so 162 // this is a LEGITIMATE whole-plane rewrite and must be ALLOWED. This is the precise case that 163 // forced the 2026-08-02 revert of the count-based guard; identity-keying is what makes it legal. 164 eg_make(sx, EG_SHRINK_ROWS, "compiler" as *u8) 165 let nbefore: i64 = eg_count(sx) 166 let rcs: i64 = eg_run(sx) 167 let nafter: i64 = eg_count(sx) 168 _p(" shrink-but-no-name-lost rows " as *u8); _fn(1, nbefore); _p(" -> " as *u8); _fn(1, nafter) 169 _p(" rc=" as *u8); _fn(1, rcs); _p(" (want allowed rc=0)\n" as *u8) 170 // Assert the fixture is genuinely a shrink FIRST, else T5 passes vacuously on a non-shrink. 171 gv_check("T5a fixture is a real count-shrink: rows_before > authored" as *u8, nbefore > EG_AUTHORED, ctr) 172 gv_check("T5b anti-vacuity: count shrinks but no NAME lost -> ALLOWED (a count-based guard fails here)" as *u8, rcs == 0, ctr) 173 174 return gv_verdict("ecomat_seed_clobber" as *u8, ctr, "guard bites on a vanishing domain, spares a legitimate name-preserving rewrite" as *u8) 175}