nx_sts_rowwrite_gate.nx source

1// nx_sts_rowwrite_gate.nx -- THE TEETH OF ROW-LEVEL PLANE WRITES (loadgov LV17 sts_put_append, 2026-09-02). 2// In-process over nx_store_seed_lib on a /tmp fixture plane (created at SETUP with sys_mkdir; the fixture-ratchet law: 3// never a production prefix). What is proven: sts_find_seq locates a row by its first column and refuses an absent id; 4// sts_append_fast adds one row and the reader sees it last; sts_replace_fast overwrites exactly one row at its seq, keeps 5// count and order, and newest-wins across two replacements; an out-of-range seq is refused with the plane untouched. 6// NOT proven here: the O(1) cost. It holds BY CONSTRUCTION (each write is one ss_add + one commit) and the honest measure 7// of it is the D-state roster under load, which is nx_dstate's job, not a unit gate's. 8// Inherits nx_gate_verdict: the exit code IS the verdict; every neg-control is NAMED for the gatelaw census. 9// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 10import "nx_syscalls.nx" 11import "nx_gate_verdict.nx" 12import "nx_store_seed_lib.nx" 13 14const RW_DIR: *u8 = "/tmp/nx_sts_rowwrite" 15const RW_PREFIX: *u8 = "/tmp/nx_sts_rowwrite/p-" 16const RW_MODE_DIR: i64 = 493 // 0755 17const RW_CAP: i64 = 65536 18const RW_ROWS0: i64 = 3 19const RW_BAD_SEQ: i64 = 9 // beyond q:n on purpose 20 21func rw_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 22// count newline-terminated rows in buf[0..n) 23func rw_rows(b: *u8, n: i64) -> i64 { var r: i64 = 0; var i: i64 = 0; while i < n { if b[i] == (10 as u8) { r = r + 1 } i = i + 1 } return r } 24// does row number `k` (0-based) of the loaded buffer equal `want` exactly (without its newline)? 25func rw_row_is(b: *u8, n: i64, k: i64, want: *u8) -> i64 { 26 var i: i64 = 0 27 var r: i64 = 0 28 while r < k { if i >= n { return 0 } if b[i] == (10 as u8) { r = r + 1 } i = i + 1 } 29 let wl: i64 = rw_slen(want) 30 var j: i64 = 0 31 while j < wl { if i + j >= n { return 0 } if b[i + j] != want[j] { return 0 } j = j + 1 } 32 if i + wl >= n { return 0 } 33 if b[i + wl] != (10 as u8) { return 0 } 34 return 1 35} 36 37func main() -> i64 { 38 gv_head("nx_sts_rowwrite_gate -- one row written costs one row, and every reader still agrees" as *u8) 39 let ctr: *i64 = gv_ctr() 40 sys_mkdir(RW_DIR, RW_MODE_DIR) 41 // ---- setup: a fresh 3-row plane. The prefix is unique per run (epoch), so a crashed previous run cannot leak into this one. 42 let pfx: *u8 = sys_mmap(256) 43 var po: i64 = 0 44 var pi: i64 = 0 45 while RW_PREFIX[pi] != (0 as u8) { pfx[po] = RW_PREFIX[pi]; po = po + 1; pi = pi + 1 } 46 po = ss_catn(pfx, po, sys_now_realtime_sec()) 47 pfx[po] = 45 as u8 48 pfx[po + 1] = 0 as u8 49 let seed: *u8 = "a\tA1\nb\tB1\nc\tC1\n" as *u8 50 let sn: i64 = rw_slen(seed) 51 let made: i64 = sts_seed(pfx, seed, sn) 52 gv_check("fixture-seeded-three-rows" as *u8, (made == RW_ROWS0) as i64, ctr) 53 let buf: *u8 = sys_mmap(RW_CAP) 54 let n0: i64 = sts_load(pfx, buf, RW_CAP) 55 gv_check("fixture-reads-back-three-rows" as *u8, (rw_rows(buf, n0) == RW_ROWS0) as i64, ctr) 56 let seg0: i64 = ss_max_segid(pfx) 57 58 // ---- (1) locate by id 59 gv_check("find-seq-locates-first-row" as *u8, (sts_find_seq(pfx, "a" as *u8) == 0) as i64, ctr) 60 gv_check("find-seq-locates-middle-row" as *u8, (sts_find_seq(pfx, "b" as *u8) == 1) as i64, ctr) 61 gv_check("find-seq-locates-last-row" as *u8, (sts_find_seq(pfx, "c" as *u8) == 2) as i64, ctr) 62 gv_bite("neg-control-absent-id-is-not-located" as *u8, (sts_find_seq(pfx, "zz" as *u8) < 0) as i64, (sts_find_seq(pfx, "b" as *u8) < 0) as i64, ctr) 63 gv_check("find-seq-matches-whole-column-not-prefix" as *u8, (sts_find_seq(pfx, "ab" as *u8) < 0) as i64, ctr) 64 65 // ---- (2) append one row 66 let ra: i64 = sts_append_fast(pfx, "d\tD1" as *u8, 4) 67 gv_check("append-returns-the-new-count" as *u8, (ra == RW_ROWS0 + 1) as i64, ctr) 68 let n1: i64 = sts_load(pfx, buf, RW_CAP) 69 gv_check("append-reads-back-four-rows-with-the-new-one-last" as *u8, ((rw_rows(buf, n1) == RW_ROWS0 + 1) & rw_row_is(buf, n1, 3, "d\tD1" as *u8)) as i64, ctr) 70 gv_check("append-costs-exactly-one-segment" as *u8, (ss_max_segid(pfx) == seg0 + 1) as i64, ctr) 71 72 // ---- (3) replace one row in place 73 let seg1: i64 = ss_max_segid(pfx) 74 let rr: i64 = sts_replace_fast(pfx, 1, "b\tB2" as *u8, 4) 75 gv_check("replace-returns-the-unchanged-count" as *u8, (rr == RW_ROWS0 + 1) as i64, ctr) 76 let n2: i64 = sts_load(pfx, buf, RW_CAP) 77 gv_check("replace-keeps-the-row-count" as *u8, (rw_rows(buf, n2) == RW_ROWS0 + 1) as i64, ctr) 78 gv_check("replace-changes-only-the-target-row-at-its-position" as *u8, (rw_row_is(buf, n2, 1, "b\tB2" as *u8) & rw_row_is(buf, n2, 0, "a\tA1" as *u8) & rw_row_is(buf, n2, 2, "c\tC1" as *u8) & rw_row_is(buf, n2, 3, "d\tD1" as *u8)) as i64, ctr) 79 gv_check("replace-costs-exactly-one-segment" as *u8, (ss_max_segid(pfx) == seg1 + 1) as i64, ctr) 80 gv_check("find-seq-still-locates-the-replaced-row" as *u8, (sts_find_seq(pfx, "b" as *u8) == 1) as i64, ctr) 81 82 // ---- (4) newest wins across two replacements 83 sts_replace_fast(pfx, 1, "b\tB3" as *u8, 4) 84 let n3: i64 = sts_load(pfx, buf, RW_CAP) 85 gv_check("second-replace-newest-wins" as *u8, rw_row_is(buf, n3, 1, "b\tB3" as *u8), ctr) 86 87 // ---- (5) out-of-range seq is refused and the plane is untouched 88 let segb: i64 = ss_max_segid(pfx) 89 let rb: i64 = sts_replace_fast(pfx, RW_BAD_SEQ, "x\tX1" as *u8, 4) 90 let n4: i64 = sts_load(pfx, buf, RW_CAP) 91 gv_bite("neg-control-out-of-range-seq-is-refused" as *u8, (rb < 0) as i64, (rr < 0) as i64, ctr) 92 gv_check("refused-replace-leaves-plane-untouched" as *u8, ((ss_max_segid(pfx) == segb) & (rw_rows(buf, n4) == RW_ROWS0 + 1)) as i64, ctr) 93 gv_check("refused-replace-leaves-rows-byte-identical" as *u8, (rw_row_is(buf, n4, 1, "b\tB3" as *u8) & rw_row_is(buf, n4, 3, "d\tD1" as *u8)) as i64, ctr) 94 95 return gv_verdict("nx_sts_rowwrite_gate" as *u8, ctr, "row-level plane writes on a /tmp fixture: locate, append, replace, newest-wins, refusal; O(1) cost is by construction, measured by nx_dstate under load, not here" as *u8) 96}