code wiki / _hdl_build / nx_store_put_shrink_gate.nx
`nx_store_put_shrink_gate.nx` source

↩ module page · 238 lines · 11669 B
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 {
  let wtr: *i64 = ss_begin_cap(1 << 16)
  let key: *u8 = sys_mmap(64)
  let val: *u8 = sys_mmap(128)
  var i: i64 = 0
  while i < rows {
      sts_rowkey(i, key)
      var o: i64 = 0
      let p: *u8 = "sgrow-"
      var q: i64 = 0
      while p[q] != (0 as u8) { val[o] = p[q]; o = o + 1; q = q + 1 }
      o = ss_catn(val, o, i)
      val[o] = 9 as u8
      o = o + 1
      let d: *u8 = "detail"
      var e: i64 = 0
      while d[e] != (0 as u8) { val[o] = d[e]; o = o + 1; e = e + 1 }
      if ss_add(wtr, STS_KIND_LIVE, key, val, o) < 0 { return 0 - 1 }
      i = i + 1
  }
  let cb: *u8 = sys_mmap(32)
  let cl: i64 = ss_catn(cb, 0, lie)
  if ss_add(wtr, STS_KIND_LIVE, "q:n" as *u8, cb, cl) < 0 { return 0 - 1 }
  if ss_commit(prefix, wtr, ss_next_segid(prefix)) != 0 { return 0 - 1 }
  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 {
  let pid: i64 = sys_fork()
  if pid == 0 {
      let ofd: i64 = sys_openat_wr("knowledge/status/shrink_gate.out\x00" as *u8, 0x1a4)
      if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) }
      let elf: *u8 = sys_mmap(512)
      if ar_resolve("_offc/nx_store_put.elf" as *u8, elf) == 0 { sys_exit(127) }
      let av: *i64 = sys_mmap(96) as *i64
      av[0] = elf as i64
      av[1] = prefix as i64
      av[2] = "put" as i64
      av[3] = "shrink-gate" as i64
      av[4] = id as i64
      av[5] = "toolX" as i64
      av[6] = "ownerX" as i64
      av[7] = "scopeX" as i64
      av[8] = "LIVE" as i64
      av[9] = "0" as i64
      av[10] = 0
      let envp: *i64 = sys_mmap(16) as *i64
      envp[0] = 0
      sys_execve(elf, av, envp)
      sys_exit(127)
  }
  let stp: *i64 = sys_mmap(16) as *i64
  sys_wait4(pid, stp, 0)
  let sig: i64 = stp[0] & 0x7f
  if sig != 0 { return 128 + sig }
  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 {
  let pid: i64 = sys_fork()
  if pid == 0 {
      let ofd: i64 = sys_openat_wr("knowledge/status/shrink_gate.out\x00" as *u8, 0x1a4)
      if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) }
      let elf: *u8 = sys_mmap(512)
      if ar_resolve("_offc/nx_store_put.elf" as *u8, elf) == 0 { sys_exit(127) }
      let av: *i64 = sys_mmap(160) as *i64
      av[0] = elf as i64
      av[1] = prefix as i64
      var i: i64 = 0
      while tail[i] != 0 { av[2+i] = tail[i]; i = i + 1 }
      av[2+i] = 0
      let envp: *i64 = sys_mmap(16) as *i64
      envp[0] = 0
      sys_execve(elf, av, envp)
      sys_exit(127)
  }
  let stp: *i64 = sys_mmap(16) as *i64
  sys_wait4(pid, stp, 0)
  let sig: i64 = stp[0] & 0x7f
  if sig != 0 { return 128 + sig }
  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 {
  let pq: *i64 = sys_mmap(4096) as *i64
  let pl: *i64 = sys_mmap(4096) as *i64
  if ss_get(prefix, "q:n" as *u8, pq, pl) == 1 { return sts_atoi(pq[0] as *u8, pl[0]) }
  return 0 - 1
121}
122
123func main() -> i64 {
  let ctr: *i64 = gv_ctr()
  w("=== nx_store_put_shrink_gate -- the anti-clobber guard must BITE, not just exist ===\n")
126
  // fresh fixture prefix per run: unlink is not available, so use the segid-forward property --
  // a re-run commits a NEWER segment and newest-wins; the lie is re-manufactured each run.
  let fx: *u8 = "knowledge/status/sgfix-\x00" as *u8
130
  // ---- T1: the damage is REAL (declared > reachable), manufactured not simulated ----
  let made: i64 = sg_make_damaged(fx, SG_REALROWS, SG_LIE)
  let pq: *i64 = sys_mmap(4096) as *i64
  let pl: *i64 = sys_mmap(4096) as *i64
  var declared: i64 = 0 - 1
  if ss_get(fx, "q:n" as *u8, pq, pl) == 1 { declared = sts_atoi(pq[0] as *u8, pl[0]) }
  w("  fixture: made="); wn(made); w(" declared="); wn(declared); w("\n")
  gv_check("T1 fixture damaged: 3 real rows, q:n lies 9" as *u8, (made == SG_REALROWS) & (declared == SG_LIE), ctr)
139
  // ---- T2 (REWRITTEN 2026-09-02, loadgov LV17): put no longer reseeds the plane, so an over-declared q:n is no
  // longer a reason to refuse -- a write that touches ONE key cannot delete the rows it could not see. The new law:
  // the put SUCCEEDS as an append at the declared count (q:9), q:n advances 9->10, and nothing is lost.
  let rc: i64 = sg_put(fx, "victim-row" as *u8)
  w("  put on damaged plane rc="); wn(rc); w(" (want 0: a one-key append cannot clobber)\n")
  gv_check("T2 row-level put on an over-declared plane SUCCEEDS instead of refusing" as *u8, rc == 0, ctr)
146
  // ---- T3: the append advanced q:n by exactly one and every real row is still readable (3 real + 1 new) ----
  var decl2: i64 = 0 - 1
  if ss_get(fx, "q:n" as *u8, pq, pl) == 1 { decl2 = sts_atoi(pq[0] as *u8, pl[0]) }
  let lb3: *u8 = sys_mmap(65536)
  let ln3: i64 = sts_load(fx, lb3, 65536)
  var rows3: i64 = 0
  var q3: i64 = 0
  while q3 < ln3 { if lb3[q3] == (10 as u8) { rows3 = rows3 + 1 } q3 = q3 + 1 }
  w("  after put: q:n="); wn(decl2); w(" readable rows="); wn(rows3); w(" (want 10 / 4)\n")
  gv_check("T3 append advanced q:n by one and deleted nothing: the 3 real rows and the new one read back" as *u8, (decl2 == SG_LIE + 1) & (rows3 == SG_REALROWS + 1), ctr)
157
  // ---- T4: NEG-CONTROL: a HEALTHY plane still accepts the same put (guard is not over-broad) ----
  let hx: *u8 = "knowledge/status/sghealthy-\x00" as *u8
  var t4: i64 = 0
  if sg_make_damaged(hx, SG_REALROWS, SG_REALROWS) == SG_REALROWS {
      let rch: i64 = sg_put(hx, "legit-row" as *u8)
      var decl3: i64 = 0 - 1
      if ss_get(hx, "q:n" as *u8, pq, pl) == 1 { decl3 = sts_atoi(pq[0] as *u8, pl[0]) }
      w("  healthy-plane put rc="); wn(rch); w(" q:n now="); wn(decl3); w(" (want 0 / 4)\n")
      if rch == 0 { if decl3 == SG_REALROWS + 1 { t4 = 1 } }
  }
  gv_check("T4 neg-control: healthy plane still accepts a put (rc=0, q:n 3->4)" as *u8, t4, ctr)
169
  // ---- T5-T7: THE OTHER THREE VERBS' REFUSALS, each on its OWN damaged fixture (1785718927).
  // putn/close/setcol share the tooth but not the code path to it; a wired-but-unwitnessed branch is an
  // assertion. For close/setcol the target id (sgrow-1) EXISTS among the reachable rows, so the id-not-found
  // refusal (also exit 4) cannot be the one firing -- found=1 falls through to the shrink check.
  let fxn: *u8 = "knowledge/status/sgfixn-\x00" as *u8
  var t5: i64 = 0
  if sg_make_damaged(fxn, SG_REALROWS, SG_LIE) == SG_REALROWS {
      let tn: *i64 = sys_mmap(96) as *i64
      tn[0] = "putn" as i64
      tn[1] = "shrink-gate" as i64
      tn[2] = "2" as i64
      tn[3] = "batchrow" as i64
      tn[4] = "batchdetail" as i64
      tn[5] = 0
      let rcn: i64 = sg_verb(fxn, tn)
      w("  putn on damaged plane rc="); wn(rcn); w(" q:n="); wn(sg_declared(fxn)); w("\n")
      if rcn == SG_EXIT_REFUSED { if sg_declared(fxn) == SG_LIE { t5 = 1 } }
  }
  gv_check("T5 putn refusal fires on over-declared plane, store untouched" as *u8, t5, ctr)
189
  let fxc: *u8 = "knowledge/status/sgfixc-\x00" as *u8
  var t6: i64 = 0
  if sg_make_damaged(fxc, SG_REALROWS, SG_LIE) == SG_REALROWS {
      let tc: *i64 = sys_mmap(96) as *i64
      tc[0] = "close" as i64
      tc[1] = "shrink-gate" as i64
      tc[2] = "sgrow-1" as i64
      tc[3] = "closing a reachable row on a damaged plane" as i64
      tc[4] = 0
      let rcc: i64 = sg_verb(fxc, tc)
      w("  close on damaged plane rc="); wn(rcc); w(" q:n="); wn(sg_declared(fxc)); w("\n")
      if rcc == 0 { if sg_declared(fxc) == SG_LIE { t6 = 1 } }
  }
  gv_check("T6 row-level close on an over-declared plane succeeds in place: rc 0 and q:n unchanged" as *u8, t6, ctr)
204
  let fxs: *u8 = "knowledge/status/sgfixs-\x00" as *u8
  var t7: i64 = 0
  if sg_make_damaged(fxs, SG_REALROWS, SG_LIE) == SG_REALROWS {
      let ts: *i64 = sys_mmap(96) as *i64
      ts[0] = "setcol" as i64
      ts[1] = "shrink-gate" as i64
      ts[2] = "sgrow-1" as i64
      ts[3] = "1" as i64
      ts[4] = "poked" as i64
      ts[5] = 0
      let rcs: i64 = sg_verb(fxs, ts)
      w("  setcol on damaged plane rc="); wn(rcs); w(" q:n="); wn(sg_declared(fxs)); w("\n")
      if rcs == 0 { if sg_declared(fxs) == SG_LIE { t7 = 1 } }
  }
  gv_check("T7 row-level setcol on an over-declared plane succeeds in place: rc 0 and q:n unchanged" as *u8, t7, ctr)
220
  // ---- T8: NEG-CONTROL for a MODIFY verb -- close on the HEALTHY plane still commits (rc=0).
  var t8: i64 = 0
  let tc2: *i64 = sys_mmap(96) as *i64
  tc2[0] = "close" as i64
  tc2[1] = "shrink-gate" as i64
  tc2[2] = "legit-row" as i64
  tc2[3] = "healthy close after the tooth" as i64
  tc2[4] = 0
  let rch2: i64 = sg_verb(hx, tc2)
  w("  healthy-plane close rc="); wn(rch2); w(" (want 0)\n")
  if rch2 == 0 { t8 = 1 }
  gv_check("T8 neg-control: healthy plane still accepts close (guard not over-broad on modify)" as *u8, t8, ctr)
233
  // D001: gv_verdict's line IS the verdict. A first cut added a hand-rolled GREEN/RED trailer keyed to a
  // GUESSED gv_ctr slot layout -- it printed RED beside a canonical 4/4 GREEN on this gate's first run.
  // Two voices, one wrong: exactly the hand-rolled-verdict class D001 retires. The counter is gv's, not ours.
  return gv_verdict("store_put_shrink" as *u8, ctr, "row-level writes cannot clobber an over-declared plane; the seed-path guard still bites the batch verb; healthy planes unchanged" as *u8)
238}
nx_store_put_shrink_gate.nx source

`nx_store_put_shrink_gate.nx` source
