nx_store_put_shrink_gate.nx source

1// nx_store_put_shrink_gate.nx -- proves the shrink-refusal guard in nx_store_put's put verb BITES. 2// 3// ★WHY (debt 1785713373): the guard shipped 2026-08-02 (sha 494abaa2) with only its PASSING paths 4// witnessed -- bootstrap, grow, replace all proven on a scratch plane. By the non-vacuity law a branch 5// that has only ever passed has demonstrated nothing: killed=0 is UNPROVEN-BY-THIS-SAMPLE, never 6// cannot-fail. This gate manufactures the exact damage class the guard exists for and asserts REFUSAL. 7// 8// ★THE FIXTURE RECIPE IS BORROWED, NOT INVENTED (nx_plane_repair_gate's hard-won lesson): sts_seed and 9// nx_store_put always write a CORRECT q:n, so the damage is unreachable through the normal writers. 10// Build it from the RAW primitives: ss_add N real rows, then a q:n that LIES and declares MORE. That is 11// the exact live shape (declared > reachable) that a PARTIAL sts_load feeds into a whole-plane re-seed 12// -- how commontask- went 37->10 and dedupq- 21->3. 13// 14// Forks the REAL promoted nx_store_put.elf via ar_resolve (never a hardcoded path -- the 127-vacuous 15// lesson), so what is proven is the artifact that actually serves writes. 16// license_tier: ORIGINAL expect_exit: 0 17import "nx_syscalls.nx" 18import "nx_store_seed_lib.nx" 19import "nx_artifact_root.nx" 20import "nx_gate_verdict.nx" 21 22const SG_REALROWS: i64 = 3 23const SG_LIE: i64 = 9 24const SG_EXIT_REFUSED: i64 = 4 25 26func w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 27func wn(v: i64) -> i64 { let t: *u8=sys_mmap(28); var m: i64=v; var k: i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} let b: *u8=sys_mmap(28); var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 } 28 29// damage recipe from nx_plane_repair_gate: N real rows + a q:n that lies upward 30func sg_make_damaged(prefix: *u8, rows: i64, lie: i64) -> i64 { 31 let wtr: *i64 = ss_begin_cap(1 << 16) 32 let key: *u8 = sys_mmap(64) 33 let val: *u8 = sys_mmap(128) 34 var i: i64 = 0 35 while i < rows { 36 sts_rowkey(i, key) 37 var o: i64 = 0 38 let p: *u8 = "sgrow-" 39 var q: i64 = 0 40 while p[q] != (0 as u8) { val[o] = p[q]; o = o + 1; q = q + 1 } 41 o = ss_catn(val, o, i) 42 val[o] = 9 as u8 43 o = o + 1 44 let d: *u8 = "detail" 45 var e: i64 = 0 46 while d[e] != (0 as u8) { val[o] = d[e]; o = o + 1; e = e + 1 } 47 if ss_add(wtr, STS_KIND_LIVE, key, val, o) < 0 { return 0 - 1 } 48 i = i + 1 49 } 50 let cb: *u8 = sys_mmap(32) 51 let cl: i64 = ss_catn(cb, 0, lie) 52 if ss_add(wtr, STS_KIND_LIVE, "q:n" as *u8, cb, cl) < 0 { return 0 - 1 } 53 if ss_commit(prefix, wtr, ss_next_segid(prefix)) != 0 { return 0 - 1 } 54 return rows 55} 56 57// fork the REAL promoted nx_store_put.elf: put <actor> <id> <5 fields>; return exit code 58func sg_put(prefix: *u8, id: *u8) -> i64 { 59 let pid: i64 = sys_fork() 60 if pid == 0 { 61 let ofd: i64 = sys_openat_wr("knowledge/status/shrink_gate.out\x00" as *u8, 0x1a4) 62 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 63 let elf: *u8 = sys_mmap(512) 64 if ar_resolve("_offc/nx_store_put.elf" as *u8, elf) == 0 { sys_exit(127) } 65 let av: *i64 = sys_mmap(96) as *i64 66 av[0] = elf as i64 67 av[1] = prefix as i64 68 av[2] = "put" as i64 69 av[3] = "shrink-gate" as i64 70 av[4] = id as i64 71 av[5] = "toolX" as i64 72 av[6] = "ownerX" as i64 73 av[7] = "scopeX" as i64 74 av[8] = "LIVE" as i64 75 av[9] = "0" as i64 76 av[10] = 0 77 let envp: *i64 = sys_mmap(16) as *i64 78 envp[0] = 0 79 sys_execve(elf, av, envp) 80 sys_exit(127) 81 } 82 let stp: *i64 = sys_mmap(16) as *i64 83 sys_wait4(pid, stp, 0) 84 let sig: i64 = stp[0] & 0x7f 85 if sig != 0 { return 128 + sig } 86 return (stp[0] >> 8) & 0xff 87} 88 89// generic runner for the OTHER write verbs: forks the promoted elf with prefix + a null-terminated tail. 90func sg_verb(prefix: *u8, tail: *i64) -> i64 { 91 let pid: i64 = sys_fork() 92 if pid == 0 { 93 let ofd: i64 = sys_openat_wr("knowledge/status/shrink_gate.out\x00" as *u8, 0x1a4) 94 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 95 let elf: *u8 = sys_mmap(512) 96 if ar_resolve("_offc/nx_store_put.elf" as *u8, elf) == 0 { sys_exit(127) } 97 let av: *i64 = sys_mmap(160) as *i64 98 av[0] = elf as i64 99 av[1] = prefix as i64 100 var i: i64 = 0 101 while tail[i] != 0 { av[2+i] = tail[i]; i = i + 1 } 102 av[2+i] = 0 103 let envp: *i64 = sys_mmap(16) as *i64 104 envp[0] = 0 105 sys_execve(elf, av, envp) 106 sys_exit(127) 107 } 108 let stp: *i64 = sys_mmap(16) as *i64 109 sys_wait4(pid, stp, 0) 110 let sig: i64 = stp[0] & 0x7f 111 if sig != 0 { return 128 + sig } 112 return (stp[0] >> 8) & 0xff 113} 114 115// helper: q:n as declared by the plane right now (-1 if absent) 116func sg_declared(prefix: *u8) -> i64 { 117 let pq: *i64 = sys_mmap(4096) as *i64 118 let pl: *i64 = sys_mmap(4096) as *i64 119 if ss_get(prefix, "q:n" as *u8, pq, pl) == 1 { return sts_atoi(pq[0] as *u8, pl[0]) } 120 return 0 - 1 121} 122 123func main() -> i64 { 124 let ctr: *i64 = gv_ctr() 125 w("=== nx_store_put_shrink_gate -- the anti-clobber guard must BITE, not just exist ===\n") 126 127 // fresh fixture prefix per run: unlink is not available, so use the segid-forward property -- 128 // a re-run commits a NEWER segment and newest-wins; the lie is re-manufactured each run. 129 let fx: *u8 = "knowledge/status/sgfix-\x00" as *u8 130 131 // ---- T1: the damage is REAL (declared > reachable), manufactured not simulated ---- 132 let made: i64 = sg_make_damaged(fx, SG_REALROWS, SG_LIE) 133 let pq: *i64 = sys_mmap(4096) as *i64 134 let pl: *i64 = sys_mmap(4096) as *i64 135 var declared: i64 = 0 - 1 136 if ss_get(fx, "q:n" as *u8, pq, pl) == 1 { declared = sts_atoi(pq[0] as *u8, pl[0]) } 137 w(" fixture: made="); wn(made); w(" declared="); wn(declared); w("\n") 138 gv_check("T1 fixture damaged: 3 real rows, q:n lies 9" as *u8, (made == SG_REALROWS) & (declared == SG_LIE), ctr) 139 140 // ---- T2: THE BITE. a put on the damaged plane loads 3 rows + 1 new = 4 < 9 declared => REFUSED(4) 141 let rc: i64 = sg_put(fx, "victim-row" as *u8) 142 w(" put on damaged plane rc="); wn(rc); w(" (want "); wn(SG_EXIT_REFUSED); w(" REFUSED)\n") 143 gv_check("T2 guard BITES: put on over-declared plane exits REFUSED" as *u8, rc == SG_EXIT_REFUSED, ctr) 144 145 // ---- T3: the refusal changed NOTHING -- q:n still declares the lie (store untouched) ---- 146 var decl2: i64 = 0 - 1 147 if ss_get(fx, "q:n" as *u8, pq, pl) == 1 { decl2 = sts_atoi(pq[0] as *u8, pl[0]) } 148 gv_check("T3 store untouched by refusal: q:n unchanged" as *u8, decl2 == SG_LIE, ctr) 149 150 // ---- T4: NEG-CONTROL: a HEALTHY plane still accepts the same put (guard is not over-broad) ---- 151 let hx: *u8 = "knowledge/status/sghealthy-\x00" as *u8 152 var t4: i64 = 0 153 if sg_make_damaged(hx, SG_REALROWS, SG_REALROWS) == SG_REALROWS { 154 let rch: i64 = sg_put(hx, "legit-row" as *u8) 155 var decl3: i64 = 0 - 1 156 if ss_get(hx, "q:n" as *u8, pq, pl) == 1 { decl3 = sts_atoi(pq[0] as *u8, pl[0]) } 157 w(" healthy-plane put rc="); wn(rch); w(" q:n now="); wn(decl3); w(" (want 0 / 4)\n") 158 if rch == 0 { if decl3 == SG_REALROWS + 1 { t4 = 1 } } 159 } 160 gv_check("T4 neg-control: healthy plane still accepts a put (rc=0, q:n 3->4)" as *u8, t4, ctr) 161 162 // ---- T5-T7: THE OTHER THREE VERBS' REFUSALS, each on its OWN damaged fixture (1785718927). 163 // putn/close/setcol share the tooth but not the code path to it; a wired-but-unwitnessed branch is an 164 // assertion. For close/setcol the target id (sgrow-1) EXISTS among the reachable rows, so the id-not-found 165 // refusal (also exit 4) cannot be the one firing -- found=1 falls through to the shrink check. 166 let fxn: *u8 = "knowledge/status/sgfixn-\x00" as *u8 167 var t5: i64 = 0 168 if sg_make_damaged(fxn, SG_REALROWS, SG_LIE) == SG_REALROWS { 169 let tn: *i64 = sys_mmap(96) as *i64 170 tn[0] = "putn" as i64 171 tn[1] = "shrink-gate" as i64 172 tn[2] = "2" as i64 173 tn[3] = "batchrow" as i64 174 tn[4] = "batchdetail" as i64 175 tn[5] = 0 176 let rcn: i64 = sg_verb(fxn, tn) 177 w(" putn on damaged plane rc="); wn(rcn); w(" q:n="); wn(sg_declared(fxn)); w("\n") 178 if rcn == SG_EXIT_REFUSED { if sg_declared(fxn) == SG_LIE { t5 = 1 } } 179 } 180 gv_check("T5 putn refusal fires on over-declared plane, store untouched" as *u8, t5, ctr) 181 182 let fxc: *u8 = "knowledge/status/sgfixc-\x00" as *u8 183 var t6: i64 = 0 184 if sg_make_damaged(fxc, SG_REALROWS, SG_LIE) == SG_REALROWS { 185 let tc: *i64 = sys_mmap(96) as *i64 186 tc[0] = "close" as i64 187 tc[1] = "shrink-gate" as i64 188 tc[2] = "sgrow-1" as i64 189 tc[3] = "closing a reachable row on a damaged plane" as i64 190 tc[4] = 0 191 let rcc: i64 = sg_verb(fxc, tc) 192 w(" close on damaged plane rc="); wn(rcc); w(" q:n="); wn(sg_declared(fxc)); w("\n") 193 if rcc == SG_EXIT_REFUSED { if sg_declared(fxc) == SG_LIE { t6 = 1 } } 194 } 195 gv_check("T6 close refusal fires (id reachable, so not the id-not-found exit)" as *u8, t6, ctr) 196 197 let fxs: *u8 = "knowledge/status/sgfixs-\x00" as *u8 198 var t7: i64 = 0 199 if sg_make_damaged(fxs, SG_REALROWS, SG_LIE) == SG_REALROWS { 200 let ts: *i64 = sys_mmap(96) as *i64 201 ts[0] = "setcol" as i64 202 ts[1] = "shrink-gate" as i64 203 ts[2] = "sgrow-1" as i64 204 ts[3] = "1" as i64 205 ts[4] = "poked" as i64 206 ts[5] = 0 207 let rcs: i64 = sg_verb(fxs, ts) 208 w(" setcol on damaged plane rc="); wn(rcs); w(" q:n="); wn(sg_declared(fxs)); w("\n") 209 if rcs == SG_EXIT_REFUSED { if sg_declared(fxs) == SG_LIE { t7 = 1 } } 210 } 211 gv_check("T7 setcol refusal fires (id reachable, so not the id-not-found exit)" as *u8, t7, ctr) 212 213 // ---- T8: NEG-CONTROL for a MODIFY verb -- close on the HEALTHY plane still commits (rc=0). 214 var t8: i64 = 0 215 let tc2: *i64 = sys_mmap(96) as *i64 216 tc2[0] = "close" as i64 217 tc2[1] = "shrink-gate" as i64 218 tc2[2] = "legit-row" as i64 219 tc2[3] = "healthy close after the tooth" as i64 220 tc2[4] = 0 221 let rch2: i64 = sg_verb(hx, tc2) 222 w(" healthy-plane close rc="); wn(rch2); w(" (want 0)\n") 223 if rch2 == 0 { t8 = 1 } 224 gv_check("T8 neg-control: healthy plane still accepts close (guard not over-broad on modify)" as *u8, t8, ctr) 225 226 // D001: gv_verdict's line IS the verdict. A first cut added a hand-rolled GREEN/RED trailer keyed to a 227 // GUESSED gv_ctr slot layout -- it printed RED beside a canonical 4/4 GREEN on this gate's first run. 228 // Two voices, one wrong: exactly the hand-rolled-verdict class D001 retires. The counter is gv's, not ours. 229 return gv_verdict("store_put_shrink" as *u8, ctr, "guard bites on manufactured damage, spares the healthy" as *u8) 230}