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

↩ module page · 171 lines · 8474 B
1// nx_plane_repair_gate.nx -- proves nx_plane_repair actually repairs, on a DELIBERATELY DAMAGED plane.
2//
3// ★WHY THIS GATE HAD TO EXIST BEFORE THE TOOL COULD BE TRUSTED. nx_plane_repair shipped with only its
4// NO-OP and REFUSAL paths exercised (a healthy plane declines correctly). The path that actually writes --
5// the one that permanently accepts data loss and rewrites the ecosystem's ledger -- was CODE-REVIEWED, NOT
6// MEASURED. This whole workstream exists to delete exactly that distinction, so leaving it would have been
7// the largest hypocrisy in it.
8//
9// ★THE FIXTURE IS THE HARD PART, and it is why this could not be tested earlier: `sts_seed` ALWAYS writes a
10// correct q:n, so the damage it repairs is unreachable through the normal writer. The gate therefore builds
11// the damaged plane from the RAW store primitives -- ss_add of 5 real rows, then a q:n that LIES and says 8.
12// That reproduces the exact live shape (declared > reachable) without waiting for a real outage.
13//
14// It forks the REAL promoted elf rather than calling a library, so what is proven is the artifact that
15// actually runs. license_tier: ORIGINAL  expect_exit: 0
16import "nx_syscalls.nx"
17import "nx_store_seed_lib.nx"
18import "nx_artifact_root.nx"
19
20const PG_FIXROWS: i64 = 5
21const PG_LIE:     i64 = 8
22
23func w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
24func 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 }
25func ck(pass: i64, label: *u8, fails: *i64) -> i64 {
  w("  "); w(label); w(": ")
  if pass==1 { w("PASS\n") } else { w("FAIL\n"); fails[0]=fails[0]+1 }
  return 0
29}
30
31// Build a plane with `rows` real rows but a q:n that DECLARES `lie`. This is the damage, manufactured.
32func pg_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 = "fixture-row-"
      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)
      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
52}
53
54// fork the REAL elf: nx_plane_repair <prefix> [confirm]; return exit code
55func pg_run(prefix: *u8, confirm: *u8) -> i64 {
  let pid: i64 = sys_fork()
  if pid == 0 {
      let ofd: i64 = sys_openat_wr("knowledge/status/plane_repair_gate.out\x00" as *u8, 0x1a4)
      if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) }
      // ★RESOLVE, DO NOT HARDCODE. The first cut used a literal `./_offc/nx_plane_repair.elf`, which
      // exists on a dev tree and NOT on the NAS, where /api/promote installs flat at the serving root.
      // On the NAS every fork failed with 127, four teeth went RED -- and T3 PASSED VACUOUSLY, because
      // "all 5 rows survived" is trivially true when the repair never ran at all. ★I shipped, inside the
      // gate for a tool about data integrity, the exact artifact-root bug I built ar_resolve to kill.
      let elf: *u8 = sys_mmap(512)
      if ar_resolve("_offc/nx_plane_repair.elf" as *u8, elf) == 0 { sys_exit(127) }
      let av: *i64 = sys_mmap(48) as *i64
      av[0] = elf as i64
      av[1] = prefix as i64
      if (confirm as i64) == 0 { av[2] = 0 } else { av[2] = confirm as i64; av[3] = 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
81}
82
83func main() -> i64 {
  let fails: *i64 = sys_mmap(16) as *i64
  fails[0]=0
  w("=== nx_plane_repair_gate -- repairs a DELIBERATELY DAMAGED plane, and refuses everything else ===\n")
87
  let fx: *u8 = "knowledge/status/pgfix-\x00" as *u8
  let f: *i64 = sys_mmap(64) as *i64
  let buf: *u8 = sys_mmap(1 << 20)
91
  // ---- build the damage: 5 real rows, q:n lying that there are 8 ----
  let made: i64 = pg_make_damaged(fx, PG_FIXROWS, PG_LIE)
  var t0: i64=0
  if made == PG_FIXROWS {
      sts_load_honest(fx, buf, 1 << 20, f)
      if f[0] == PG_LIE { if f[1] == PG_FIXROWS { t0=1 } }
  }
  w("  fixture: declared="); wn(f[0]); w(" reachable="); wn(f[1]); w("\n")
  ck(t0, "T0 fixture is genuinely damaged (declared 8 > reachable 5) -- the bug is reproduced, not simulated" as *u8, fails)
101
  // ---- T1: WITHOUT confirm it must REFUSE and change NOTHING ----
  let rc1: i64 = pg_run(fx, 0 as *u8)
  sts_load_honest(fx, buf, 1 << 20, f)
  var t1: i64=0
  if rc1 == 2 { if f[0] == PG_LIE { if f[1] == PG_FIXROWS { t1=1 } } }
  ck(t1, "T1 no confirm -> exit 2 AND the plane is byte-unchanged (accepting loss is an operator act)" as *u8, fails)
108
  // ---- T2: WITH confirm it repairs, and the plane becomes self-consistent ----
  let rc2: i64 = pg_run(fx, "confirm=yes\x00" as *u8)
  sts_load_honest(fx, buf, 1 << 20, f)
  var t2: i64=0
  if rc2 == 0 { if f[0] == PG_FIXROWS { if f[1] == PG_FIXROWS { t2=1 } } }
  w("  after repair: declared="); wn(f[0]); w(" reachable="); wn(f[1]); w("\n")
  ck(t2, "T2 confirm=yes -> exit 0 and declared==reachable==5 (writes unblocked)" as *u8, fails)
116
  // ---- T3: THE SURVIVING ROWS MUST STILL BE THERE. A 'repair' that reconciles by deleting rows would
  // also make declared==reachable, and would pass T2. This is the tooth that separates repair from
  // destruction. ----
  var t3: i64=0
  var seen: i64 = 0
  let n3: i64 = sts_load_honest(fx, buf, 1 << 20, f)
  var i3: i64 = 0
  while i3 < n3 - 11 {
      let nd: *u8 = "fixture-row-" as *u8
      var m: i64 = 1
      var k: i64 = 0
      while k < 12 { if buf[i3+k] != nd[k] { m = 0; k = 12 } else { k = k + 1 } }
      if m == 1 { seen = seen + 1 }
      i3 = i3 + 1
  }
  // ★T3 MUST NOT BE SATISFIABLE BY THE REPAIR NEVER RUNNING. "All 5 rows survived" is trivially true on
  // an untouched plane -- measured on the NAS, where every fork failed and this tooth went green anyway.
  // So it now ALSO requires the plane to be reconciled: rows preserved AND the count actually fixed.
  if seen == PG_FIXROWS { if f[0] == PG_FIXROWS { t3=1 } }
  w("  surviving fixture rows found in buffer="); wn(seen); w(" declared_now="); wn(f[0]); w("\n")
  ck(t3, "T3 all 5 REACHABLE rows survived the repair (it reconciled the count, it did not delete data)" as *u8, fails)
138
  // ---- T4: IDEMPOTENT. Re-running on the now-healthy plane must decline, not re-write. ----
  let rc4: i64 = pg_run(fx, "confirm=yes\x00" as *u8)
  var t4: i64=0
  if rc4 == 0 { t4=1 }
  sts_load_honest(fx, buf, 1 << 20, f)
  if f[0] != PG_FIXROWS { t4=0 }
  ck(t4, "T4 re-run on a healthy plane -> NOTHING TO REPAIR, still 5 (idempotent)" as *u8, fails)
146
  // ---- T5: the RECEIPT exists and records the loss. If the alarm is not durable, the repair is a cover-up. ----
  let rb: *u8 = sys_mmap(1 << 16)
  let rl: *i64 = sys_mmap(16) as *i64
  rl[0] = 0
  let rbuf: *u8 = sys_read_file("knowledge/status/plane_repair_receipt.log\x00" as *u8, rl)
  var t5: i64=0
  if rl[0] > 0 {
      var j: i64 = 0
      while j < rl[0] - 18 {
          let nd2: *u8 = "lost_unrecoverable" as *u8
          var m2: i64 = 1
          var k2: i64 = 0
          while k2 < 18 { if rbuf[j+k2] != nd2[k2] { m2 = 0; k2 = 18 } else { k2 = k2 + 1 } }
          if m2 == 1 { t5 = 1; j = rl[0] }
          j = j + 1
      }
  }
  ck(t5, "T5 receipt records lost_unrecoverable (the alarm became a durable record, not a deletion)" as *u8, fails)
165
  w("  fails="); wn(fails[0]); w("\n")
  if fails[0]==0 { w("VERDICT: verdict=GREEN (repairs real damage, preserves every reachable row, refuses without confirm, idempotent, records the loss)\n"); sys_exit(0) }
  w("VERDICT: verdict=RED\n")
  sys_exit(1)
  return 1
171}
nx_plane_repair_gate.nx source

`nx_plane_repair_gate.nx` source
