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}