code wiki / _hdl_build / nx_store_put_gate.nx
nx_store_put_gate.nx source
↩ module page · 174 lines · 7440 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 let elf: *u8 = "/tmp/nx_store_put.sov.elf" as *u8
43 let outf: *u8 = "/tmp/spg_out.txt" as *u8
44 let epoch: i64 = sys_now_realtime_sec()
45 let px: *u8 = sys_mmap(SPG_PFXCAP)
46 var pxo: i64 = ss_cat(px, 0, "/tmp/spg" as *u8)
47 pxo = ss_catn(px, pxo, epoch)
48 pxo = ss_cat(px, pxo, "-" as *u8)
49 px[pxo] = 0 as u8
50 let hx: *u8 = sys_mmap(SPG_PFXCAP)
51 var hxo: i64 = ss_cat(hx, 0, "/tmp/spg" as *u8)
52 hxo = ss_catn(hx, hxo, epoch)
53 hxo = ss_cat(hx, hxo, "hist-" as *u8)
54 hx[hxo] = 0 as u8
55
56 let av: *i64 = sys_mmap(SPG_AV_BYTES) as *i64
57 let dump: *u8 = sys_mmap(SPG_CAP)
58
59 // T1: put bootstraps an unseeded plane
60 av[0] = px as i64
61 av[1] = "put" as *u8 as i64
62 av[2] = "gate-actor" as *u8 as i64
63 av[3] = "W900" as *u8 as i64
64 av[4] = "first feature row" as *u8 as i64
65 av[5] = "7" as *u8 as i64
66 av[6] = "open" as *u8 as i64
67 av[7] = "gate" as *u8 as i64
68 av[8] = "tmp/" as *u8 as i64
69 av[9] = "born by put not staging" as *u8 as i64
70 let r1: i64 = dep_run_capture(elf, av, SPG_NARG_PUT, outf)
71 var dn: i64 = sts_load(px, dump, SPG_CAP)
72 if dn < 0 { dn = 0 }
73 var t1: i64 = 0
74 if r1 == 0 { if spg_has(dump, dn, "W900" as *u8) == 1 { if spg_count_lines(dump, dn) == 1 { t1 = 1 } } }
75 gv_check("T1 put BOOTSTRAPS unseeded plane (rc=0, W900 present, rows=1)" as *u8, t1, ctr)
76
77 // T2: put same id replaces
78 av[4] = "renamed feature row" as *u8 as i64
79 let r2: i64 = dep_run_capture(elf, av, SPG_NARG_PUT, outf)
80 dn = sts_load(px, dump, SPG_CAP)
81 if dn < 0 { dn = 0 }
82 var t2: i64 = 0
83 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 } } } }
84 gv_check("T2 put EXISTING id REPLACES row (rows still 1, new title, old gone)" as *u8, t2, ctr)
85
86 // T3: close flips status + appends note
87 av[1] = "close" as *u8 as i64
88 av[3] = "W900" as *u8 as i64
89 av[4] = "eaten by gate" as *u8 as i64
90 let r3: i64 = dep_run_capture(elf, av, SPG_NARG_CLOSE, outf)
91 dn = sts_load(px, dump, SPG_CAP)
92 if dn < 0 { dn = 0 }
93 var t3: i64 = 0
94 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 } } }
95 gv_check("T3 close flips open->closed + appends note" as *u8, t3, ctr)
96
97 // T4: close unknown id refused, plane untouched
98 let before: *u8 = sys_mmap(SPG_CAP)
99 let bn: i64 = sts_load(px, before, SPG_CAP)
100 av[3] = "W999" as *u8 as i64
101 let r4: i64 = dep_run_capture(elf, av, SPG_NARG_CLOSE, outf)
102 dn = sts_load(px, dump, SPG_CAP)
103 if dn < 0 { dn = 0 }
104 var t4: i64 = 0
105 if r4 != 0 { if dn == bn {
106 t4 = 1
107 var i: i64 = 0
108 while i < dn { if dump[i] != before[i] { t4 = 0; i = dn } else { i = i + 1 } }
109 } }
110 gv_check("T4 close UNKNOWN id REFUSED (rc!=0) + plane byte-untouched" as *u8, t4, ctr)
111
112 // T5: hist provenance exact
113 let hd: *u8 = sys_mmap(SPG_CAP)
114 var hn: i64 = sts_load(hx, hd, SPG_CAP)
115 if hn < 0 { hn = 0 }
116 var t5: i64 = 0
117 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 } } } }
118 gv_check("T5 hist = 3 provenanced revisions (actor, put x2 + close, old rows preserved)" as *u8, t5, ctr)
119
120 // T6: deterministic readback
121 let d2: *u8 = sys_mmap(SPG_CAP)
122 let n2: i64 = sts_load(px, d2, SPG_CAP)
123 var t6: i64 = 0
124 if n2 == dn {
125 t6 = 1
126 var k: i64 = 0
127 while k < n2 { if d2[k] != dump[k] { t6 = 0; k = n2 } else { k = k + 1 } }
128 }
129 gv_check("T6 deterministic readback (two loads byte-identical)" as *u8, t6, ctr)
130
131 // T7 (v2): N-col put -- 9-col frontier-shaped row
132 let fx: *u8 = sys_mmap(SPG_PFXCAP)
133 var fxo: i64 = ss_cat(fx, 0, "/tmp/spgf" as *u8)
134 fxo = ss_catn(fx, fxo, epoch)
135 fxo = ss_cat(fx, fxo, "-" as *u8)
136 fx[fxo] = 0 as u8
137 av[0] = fx as i64
138 av[1] = "put" as *u8 as i64
139 av[2] = "gate-actor" as *u8 as i64
140 av[3] = "F900" as *u8 as i64
141 av[4] = "nine col rock" as *u8 as i64
142 av[5] = "8" as *u8 as i64
143 av[6] = "2" as *u8 as i64
144 av[7] = "gate-owner" as *u8 as i64
145 av[8] = "T" as *u8 as i64
146 av[9] = "-" as *u8 as i64
147 av[10] = "M9" as *u8 as i64
148 av[11] = "gatelane" as *u8 as i64
149 let r7: i64 = dep_run_capture(elf, av, 12, outf)
150 let fd: *u8 = sys_mmap(SPG_CAP)
151 var fn: i64 = sts_load(fx, fd, SPG_CAP)
152 if fn < 0 { fn = 0 }
153 var t7: i64 = 0
154 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 } } } }
155 gv_check("T7 v2 N-col put (9-col frontier-shaped row lands whole)" as *u8, t7, ctr)
156
157 // T8 (v2): setcol flips col5 T->D; unknown id refused
158 av[1] = "setcol" as *u8 as i64
159 av[3] = "F900" as *u8 as i64
160 av[4] = "5" as *u8 as i64
161 av[5] = "D" as *u8 as i64
162 let r8: i64 = dep_run_capture(elf, av, 6, outf)
163 fn = sts_load(fx, fd, SPG_CAP)
164 if fn < 0 { fn = 0 }
165 av[3] = "F999" as *u8 as i64
166 let r8b: i64 = dep_run_capture(elf, av, 6, outf)
167 var t8: i64 = 0
168 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 } } } }
169 gv_check("T8 v2 setcol col5 T->D lands + unknown id REFUSED" as *u8, t8, ctr)
170
171 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)
172 sys_exit(rc)
173 return rc
174}