code wiki / _hdl_build / nx_store_put_gate.nx
nx_store_put_gate.nx source
↩ module page · 233 lines · 10388 B
1// nx_store_put_gate.nx -- gate for the unified information-plane write verb (nx_store_put).
2// MIGRATED 2026-07-18 onto nx_gate_verdict (D001 first-rung exemplar: verdict emission via THE lib,
3// no hand-rolled puts/num/pass/ttl). Teeth unchanged:
4// T1 put BOOTSTRAPS an unseeded plane; T2 put replaces by id; T3 close flips+notes; T4 close
5// unknown id REFUSED + plane byte-untouched; T5 hist provenance exact; T6 deterministic readback;
6// T7 v2 N-col put (9-col frontier row); T8 v2 setcol + fail-closed.
7// Per-run-unique /tmp fixture prefixes; drives the staged CLI via dep_run_capture.
8// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
9import "nx_store_seed_lib.nx"
10import "nx_seg_store.nx"
11import "nx_deploy_lib.nx"
12import "nx_gate_verdict.nx"
13import "nx_syscalls.nx"
14
15const SPG_CAP: i64 = 262144
16const SPG_NL: i64 = 10
17const SPG_PFXCAP: i64 = 128
18const SPG_AV_BYTES: i64 = 128
19const SPG_NARG_PUT: i64 = 10
20const SPG_NARG_CLOSE: i64 = 5
21const SPG_HIST_ROWS: i64 = 3
22
23func spg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
24func spg_has(q: *u8, n: i64, s: *u8) -> i64 {
25 let sn: i64 = spg_slen(s)
26 if sn == 0 { return 1 }
27 var i: i64 = 0
28 while i + sn <= n {
29 var hit: i64 = 1
30 var j: i64 = 0
31 while j < sn { if q[i+j] != s[j] { hit = 0; j = sn } else { j = j + 1 } }
32 if hit == 1 { return 1 }
33 i = i + 1
34 }
35 return 0
36}
37func spg_count_lines(q: *u8, n: i64) -> i64 { var k: i64 = 0; var i: i64 = 0; while i < n { if q[i] == (SPG_NL as u8) { k = k + 1 } i = i + 1 } return k }
38
39func main() -> i64 {
40 let ctr: *i64 = gv_ctr()
41 gv_head("nx_store_put gate -- unified information-plane write verb (put/close/hist, provenance, fail-closed)" as *u8)
42 // FIXTURE RESOLVED FROM THE PROMOTED BINARY, NOT /tmp (2026-08-06). This gate used to exec
43 // /tmp/nx_store_put.sov.elf -- a transient BUILD ARTIFACT. It was ABSENT on the live host (0 hits
44 // across 49,476 files in /tmp), so every tooth asserting rc==0 FAILED and the gate read 2/8 RED,
45 // looking exactly like a regression in whichever library had just been edited. It cost a full
46 // bisect to clear.
47 // ★AND THE FALSE RED WAS THE LESSER HALF: T4's entire assertion is "rc != 0", and a FAILED EXEC
48 // ALSO RETURNS rc != 0 -- so T4 reported PASS on a refusal path it never once exercised. A gate
49 // that cannot distinguish a refusal from a missing binary is not merely broken, it is DISHONEST
50 // in the green direction, which is the direction nobody investigates.
51 let elf: *u8 = "nx_store_put.elf" as *u8
52 let stbuf: *u8 = sys_mmap(160)
53 var pre: i64 = 0
54 if sys_fstatat(elf, stbuf) == 0 { pre = 1 }
55 gv_check("T0 PREFLIGHT fixture ELF exists (absent binary would FAKE T4's refusal)" as *u8, pre, ctr)
56 let outf: *u8 = "/tmp/spg_out.txt" as *u8
57 let epoch: i64 = sys_now_realtime_sec()
58 let px: *u8 = sys_mmap(SPG_PFXCAP)
59 var pxo: i64 = ss_cat(px, 0, "/tmp/spg" as *u8)
60 pxo = ss_catn(px, pxo, epoch)
61 pxo = ss_cat(px, pxo, "-" as *u8)
62 px[pxo] = 0 as u8
63 let hx: *u8 = sys_mmap(SPG_PFXCAP)
64 var hxo: i64 = ss_cat(hx, 0, "/tmp/spg" as *u8)
65 hxo = ss_catn(hx, hxo, epoch)
66 hxo = ss_cat(hx, hxo, "hist-" as *u8)
67 hx[hxo] = 0 as u8
68
69 let av: *i64 = sys_mmap(SPG_AV_BYTES) as *i64
70 let dump: *u8 = sys_mmap(SPG_CAP)
71
72 // T1: put bootstraps an unseeded plane
73 av[0] = px as i64
74 av[1] = "put" as *u8 as i64
75 av[2] = "gate-actor" as *u8 as i64
76 av[3] = "W900" as *u8 as i64
77 av[4] = "first feature row" as *u8 as i64
78 av[5] = "7" as *u8 as i64
79 av[6] = "open" as *u8 as i64
80 av[7] = "gate" as *u8 as i64
81 av[8] = "tmp/" as *u8 as i64
82 av[9] = "born by put not staging" as *u8 as i64
83 let r1: i64 = dep_run_capture(elf, av, SPG_NARG_PUT, outf)
84 var dn: i64 = sts_load(px, dump, SPG_CAP)
85 if dn < 0 { dn = 0 }
86 var t1: i64 = 0
87 if r1 == 0 { if spg_has(dump, dn, "W900" as *u8) == 1 { if spg_count_lines(dump, dn) == 1 { t1 = 1 } } }
88 gv_check("T1 put BOOTSTRAPS unseeded plane (rc=0, W900 present, rows=1)" as *u8, t1, ctr)
89
90 // T2: put same id replaces
91 av[4] = "renamed feature row" as *u8 as i64
92 let r2: i64 = dep_run_capture(elf, av, SPG_NARG_PUT, outf)
93 dn = sts_load(px, dump, SPG_CAP)
94 if dn < 0 { dn = 0 }
95 var t2: i64 = 0
96 if r2 == 0 { if spg_count_lines(dump, dn) == 1 { if spg_has(dump, dn, "renamed feature row" as *u8) == 1 { if spg_has(dump, dn, "first feature row" as *u8) == 0 { t2 = 1 } } } }
97 gv_check("T2 put EXISTING id REPLACES row (rows still 1, new title, old gone)" as *u8, t2, ctr)
98
99 // T3: close flips status + appends note
100 av[1] = "close" as *u8 as i64
101 av[3] = "W900" as *u8 as i64
102 av[4] = "eaten by gate" as *u8 as i64
103 let r3: i64 = dep_run_capture(elf, av, SPG_NARG_CLOSE, outf)
104 dn = sts_load(px, dump, SPG_CAP)
105 if dn < 0 { dn = 0 }
106 var t3: i64 = 0
107 if r3 == 0 { if spg_has(dump, dn, "closed" as *u8) == 1 { if spg_has(dump, dn, "eaten by gate" as *u8) == 1 { t3 = 1 } } }
108 gv_check("T3 close flips open->closed + appends note" as *u8, t3, ctr)
109
110 // T4: close unknown id refused, plane untouched
111 let before: *u8 = sys_mmap(SPG_CAP)
112 let bn: i64 = sts_load(px, before, SPG_CAP)
113 av[3] = "W999" as *u8 as i64
114 let r4: i64 = dep_run_capture(elf, av, SPG_NARG_CLOSE, outf)
115 dn = sts_load(px, dump, SPG_CAP)
116 if dn < 0 { dn = 0 }
117 var t4: i64 = 0
118 if r4 != 0 { if dn == bn {
119 t4 = 1
120 var i: i64 = 0
121 while i < dn { if dump[i] != before[i] { t4 = 0; i = dn } else { i = i + 1 } }
122 } }
123 gv_check("T4 close UNKNOWN id REFUSED (rc!=0) + plane byte-untouched" as *u8, t4, ctr)
124
125 // T5: hist provenance exact
126 let hd: *u8 = sys_mmap(SPG_CAP)
127 var hn: i64 = sts_load(hx, hd, SPG_CAP)
128 if hn < 0 { hn = 0 }
129 var t5: i64 = 0
130 if spg_count_lines(hd, hn) == SPG_HIST_ROWS { if spg_has(hd, hn, "gate-actor" as *u8) == 1 { if spg_has(hd, hn, "close" as *u8) == 1 { if spg_has(hd, hn, "first feature row" as *u8) == 1 { t5 = 1 } } } }
131 gv_check("T5 hist = 3 provenanced revisions (actor, put x2 + close, old rows preserved)" as *u8, t5, ctr)
132
133 // T6: deterministic readback
134 let d2: *u8 = sys_mmap(SPG_CAP)
135 let n2: i64 = sts_load(px, d2, SPG_CAP)
136 var t6: i64 = 0
137 if n2 == dn {
138 t6 = 1
139 var k: i64 = 0
140 while k < n2 { if d2[k] != dump[k] { t6 = 0; k = n2 } else { k = k + 1 } }
141 }
142 gv_check("T6 deterministic readback (two loads byte-identical)" as *u8, t6, ctr)
143
144 // T7 (v2): N-col put -- 9-col frontier-shaped row
145 let fx: *u8 = sys_mmap(SPG_PFXCAP)
146 var fxo: i64 = ss_cat(fx, 0, "/tmp/spgf" as *u8)
147 fxo = ss_catn(fx, fxo, epoch)
148 fxo = ss_cat(fx, fxo, "-" as *u8)
149 fx[fxo] = 0 as u8
150 av[0] = fx as i64
151 av[1] = "put" as *u8 as i64
152 av[2] = "gate-actor" as *u8 as i64
153 av[3] = "F900" as *u8 as i64
154 av[4] = "nine col rock" as *u8 as i64
155 av[5] = "8" as *u8 as i64
156 av[6] = "2" as *u8 as i64
157 av[7] = "gate-owner" as *u8 as i64
158 av[8] = "T" as *u8 as i64
159 av[9] = "-" as *u8 as i64
160 av[10] = "M9" as *u8 as i64
161 av[11] = "gatelane" as *u8 as i64
162 let r7: i64 = dep_run_capture(elf, av, 12, outf)
163 let fd: *u8 = sys_mmap(SPG_CAP)
164 var fn: i64 = sts_load(fx, fd, SPG_CAP)
165 if fn < 0 { fn = 0 }
166 var t7: i64 = 0
167 if r7 == 0 { if spg_has(fd, fn, "gatelane" as *u8) == 1 { if spg_has(fd, fn, "M9" as *u8) == 1 { if spg_count_lines(fd, fn) == 1 { t7 = 1 } } } }
168 gv_check("T7 v2 N-col put (9-col frontier-shaped row lands whole)" as *u8, t7, ctr)
169
170 // T8 (v2): setcol flips col5 T->D; unknown id refused
171 av[1] = "setcol" as *u8 as i64
172 av[3] = "F900" as *u8 as i64
173 av[4] = "5" as *u8 as i64
174 av[5] = "D" as *u8 as i64
175 let r8: i64 = dep_run_capture(elf, av, 6, outf)
176 fn = sts_load(fx, fd, SPG_CAP)
177 if fn < 0 { fn = 0 }
178 av[3] = "F999" as *u8 as i64
179 let r8b: i64 = dep_run_capture(elf, av, 6, outf)
180 var t8: i64 = 0
181 if r8 == 0 { if spg_has(fd, fn, "D" as *u8) == 1 { if spg_has(fd, fn, "\x09T\x09" as *u8) == 0 { if r8b != 0 { t8 = 1 } } } }
182 gv_check("T8 v2 setcol col5 T->D lands + unknown id REFUSED" as *u8, t8, ctr)
183
184 // T9 (putn): 2 rows in one call on a fresh plane -- both land, hist has 2 provenanced revisions
185 let bx: *u8 = sys_mmap(SPG_PFXCAP)
186 var bxo: i64 = ss_cat(bx, 0, "/tmp/spgb" as *u8)
187 bxo = ss_catn(bx, bxo, epoch)
188 bxo = ss_cat(bx, bxo, "-" as *u8)
189 bx[bxo] = 0 as u8
190 let bh: *u8 = sys_mmap(SPG_PFXCAP)
191 var bho: i64 = ss_cat(bh, 0, "/tmp/spgb" as *u8)
192 bho = ss_catn(bh, bho, epoch)
193 bho = ss_cat(bh, bho, "hist-" as *u8)
194 bh[bho] = 0 as u8
195 av[0] = bx as i64
196 av[1] = "putn" as *u8 as i64
197 av[2] = "gate-actor" as *u8 as i64
198 av[3] = "3" as *u8 as i64
199 av[4] = "B1" as *u8 as i64
200 av[5] = "row one" as *u8 as i64
201 av[6] = "open" as *u8 as i64
202 av[7] = "B2" as *u8 as i64
203 av[8] = "row two" as *u8 as i64
204 av[9] = "open" as *u8 as i64
205 let r9: i64 = dep_run_capture(elf, av, 10, outf)
206 var bn2: i64 = sts_load(bx, dump, SPG_CAP)
207 if bn2 < 0 { bn2 = 0 }
208 let bhd: *u8 = sys_mmap(SPG_CAP)
209 var bhn: i64 = sts_load(bh, bhd, SPG_CAP)
210 if bhn < 0 { bhn = 0 }
211 var t9: i64 = 0
212 if r9 == 0 { if spg_count_lines(dump, bn2) == 2 { if spg_has(dump, bn2, "B1" as *u8) == 1 { if spg_has(dump, bn2, "row two" as *u8) == 1 { if spg_count_lines(bhd, bhn) == 2 { t9 = 1 } } } } }
213 gv_check("T9 putn batch: 2 rows one call, both land, hist=2 provenanced" as *u8, t9, ctr)
214
215 // T10 (putn): wrong arity REFUSED fail-closed (plane never created)
216 av[3] = "3" as *u8 as i64
217 av[9] = 0
218 let bx2: *u8 = sys_mmap(SPG_PFXCAP)
219 var bx2o: i64 = ss_cat(bx2, 0, "/tmp/spgn" as *u8)
220 bx2o = ss_catn(bx2, bx2o, epoch)
221 bx2o = ss_cat(bx2, bx2o, "-" as *u8)
222 bx2[bx2o] = 0 as u8
223 av[0] = bx2 as i64
224 let r10: i64 = dep_run_capture(elf, av, 9, outf)
225 let n10: i64 = sts_load(bx2, dump, SPG_CAP)
226 var t10: i64 = 0
227 if r10 != 0 { if n10 <= 0 { t10 = 1 } }
228 gv_check("T10 putn wrong arity REFUSED (rc!=0, plane never created)" as *u8, t10, ctr)
229
230 let rc: i64 = gv_verdict("STORE-PUT-GATE" as *u8, ctr, "unified plane write verb: bootstrap-by-put, row replace, fail-closed close, in-plane provenance" as *u8)
231 sys_exit(rc)
232 return rc
233}