nx_memindex_put_gate.nx source
↩ module page · 374 lines · 17125 B
1// nx_memindex_put_gate.nx -- liar-killed GATE for the atomic slug-keyed curated upsert (F826).
2// Forks the REAL built elf (_build/nx_memindex_put.sov.elf) against byte-exact fixtures and proves the
3// properties that make it safe to point at the MOST-CONTENDED file in the ecosystem:
4// - a NEW slug APPENDS inside the block; an EXISTING slug is REPLACED IN PLACE (position preserved,
5// so the human thematic grouping survives a rewrite)
6// - a sibling's unmarked line is NEVER touched (the clobber class this organ exists to kill)
7// - IDEMPOTENT: putting identical text twice leaves the file byte-identical
8// - FAIL-CLOSED: missing CURATED markers -> file byte-untouched (never guesses where to write)
9// - DISJOINT OWNERSHIP: a put does not disturb the COINDEX block that nx_memindex_emit owns
10// - NEG-CONTROL: a slug that does not appear is not matched (no accidental overwrite)
11// usage: nx_memindex_put_gate [put_elf] Exit 0 only on 9/9.
12// license_tier: ORIGINAL expect_exit: 0
13import "nx_syscalls.nx"
14import "nx_crashresume_census_core.nx"
15
16static g_av: i64 = 0
17// shared state for the concurrency tooth -- kept in statics so the fork helper takes ZERO data args
18// (the >=3-data-arg helper miscompile class is live on this toolchain; g_run already dodges it).
19static g_elf: i64 = 0
20static g_jr: i64 = 0
21static g_md: i64 = 0
22
23func g_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
24func g_putn(v: i64) -> i64 { nxi_out(v); return 0 }
25func g_bool(name: *u8, got: i64, want: i64, passp: *i64) -> i64 {
26 g_puts("T " as *u8); g_puts(name); g_puts(" got=" as *u8); g_putn(got)
27 if got == want { g_puts(" PASS\n" as *u8); passp[0] = passp[0] + 1 } else { g_puts(" FAIL\n" as *u8) }
28 return 0
29}
30func g_write(path: *u8, s: *u8) -> i64 { let fd: i64 = sys_openat_wr(path, 420); if fd < 0 { return 0 - 1 } sys_write(fd, s, ccz_slen(s)); sys_close(fd); return 0 }
31func g_has(hay: *u8, hn: i64, needle: *u8) -> i64 {
32 let nn: i64 = ccz_slen(needle)
33 if nn == 0 { return 0 }
34 var i: i64 = 0
35 while i + nn <= hn {
36 var k: i64 = 0
37 var ok: i64 = 1
38 while k < nn { if hay[i+k] != needle[k] { ok = 0; k = nn } k = k + 1 }
39 if ok == 1 { return 1 }
40 i = i + 1
41 }
42 return 0
43}
44func g_fhas(p: *u8, needle: *u8) -> i64 {
45 let b: *u8 = sys_mmap(262144)
46 let n: i64 = ccz_read(p, b, 262143)
47 if n <= 0 { return 0 }
48 return g_has(b, n, needle)
49}
50// byte offset of needle in the file, or -1 (used to prove ORDER survived a replace)
51func g_foff(p: *u8, needle: *u8) -> i64 {
52 let b: *u8 = sys_mmap(262144)
53 let n: i64 = ccz_read(p, b, 262143)
54 if n <= 0 { return 0 - 1 }
55 let nn: i64 = ccz_slen(needle)
56 var i: i64 = 0
57 while i + nn <= n {
58 var k: i64 = 0
59 var ok: i64 = 1
60 while k < nn { if b[i+k] != needle[k] { ok = 0; k = nn } k = k + 1 }
61 if ok == 1 { return i }
62 i = i + 1
63 }
64 return 0 - 1
65}
66func g_fsize(p: *u8) -> i64 {
67 let b: *u8 = sys_mmap(262144)
68 let n: i64 = ccz_read(p, b, 262143)
69 return n
70}
71func g_same(p: *u8, q: *u8, qn: i64) -> i64 {
72 let b: *u8 = sys_mmap(262144)
73 let n: i64 = ccz_read(p, b, 262143)
74 if n != qn { return 0 }
75 var i: i64 = 0
76 while i < n { if b[i] != q[i] { return 0 } i = i + 1 }
77 return 1
78}
79func g_run() -> i64 {
80 let av: *i64 = g_av as *i64
81 let pid: i64 = sys_fork()
82 if pid < 0 { return 127 }
83 if pid == 0 {
84 sys_execve(av[0] as *u8, av, 0 as *i64)
85 sys_exit(127)
86 }
87 let st: *i64 = sys_mmap(16) as *i64
88 sys_wait4(pid, st, 0)
89 return wait_exit_code(st[0])
90}
91// ---- fixtures + helper for the BUDGET/EVICT and CONCURRENCY teeth (seq255 sev7 SCALE half) -------
92// empty managed zone, so eviction assertions are about the evicted lines and nothing else
93func fixture_ev(md: *u8) -> i64 {
94 g_write(md, "# head\n<!-- COINDEX:BEGIN -->\nDERIVED-LINE-OWNED-BY-EMIT\n<!-- COINDEX:END -->\n<!-- CURATED:BEGIN -->\n<!-- CURATED:END -->\n## TAILMARK\n" as *u8)
95 return 0
96}
97func fixture_ovfl(ov: *u8) -> i64 {
98 g_write(ov, "# ovfl head OVTOP\n<!-- CURATED-OVFL:BEGIN -->\n<!-- CURATED-OVFL:END -->\n# ovfl tail OVBOT\n" as *u8)
99 return 0
100}
101// FIRE N PUTS CONCURRENTLY: fork ALL of them before reaping any, so they genuinely race for the
102// lock. THIS is the tooth that mechanically proves the debt dead -- the hand-Edit read-modify-write
103// this organ replaces lost writes under exactly this shape (measured: FIVE collisions in one session
104// plus one mangled concatenated line), and the rail's own bench measured git losing 132 of 144.
105// Returns the number of children reaped.
106func g_conc(n: i64) -> i64 {
107 let pids: *i64 = sys_mmap(1024) as *i64
108 var i: i64 = 0
109 while i < n {
110 let sbuf: *u8 = sys_mmap(64)
111 var so: i64 = ccz_cat_str(sbuf, 0, "conc" as *u8)
112 so = ccz_cat_num(sbuf, so, i)
113 sbuf[so] = 0 as u8
114 let lbuf: *u8 = sys_mmap(64)
115 var lo: i64 = ccz_cat_str(lbuf, 0, "- CONCLINE" as *u8)
116 lo = ccz_cat_num(lbuf, lo, i)
117 lbuf[lo] = 0 as u8
118 let av: *i64 = sys_mmap(128) as *i64
119 av[0] = g_elf
120 av[1] = g_jr
121 av[2] = g_md
122 av[3] = sbuf as i64
123 av[4] = lbuf as i64
124 av[5] = 0
125 let pid: i64 = sys_fork()
126 if pid == 0 {
127 sys_execve(av[0] as *u8, av, 0 as *i64)
128 sys_exit(127)
129 }
130 pids[i] = pid
131 i = i + 1
132 }
133 let st: *i64 = sys_mmap(16) as *i64
134 var r: i64 = 0
135 var j: i64 = 0
136 while j < n {
137 if pids[j] > 0 { sys_wait4(pids[j], st, 0); r = r + 1 }
138 j = j + 1
139 }
140 return r
141}
142
143// a fixture carrying BOTH blocks -- so the gate can prove put and emit own disjoint regions
144func fixture(md: *u8) -> i64 {
145 g_write(md, "# head\n<!-- COINDEX:BEGIN -->\nDERIVED-LINE-OWNED-BY-EMIT\n<!-- COINDEX:END -->\n<!-- CURATED:BEGIN -->\n- SIBLING-UNMARKED-LINE\n<!-- CURATED:END -->\n## TAILMARK\n" as *u8)
146 return 0
147}
148
149func main(argc: i64, argv: *i64) -> i64 {
150 var elf: *u8 = "_build/nx_memindex_put.sov.elf" as *u8
151 if argc >= 2 { elf = argv[1] as *u8 }
152 let pass: *i64 = sys_mmap(16) as *i64
153 pass[0] = 0
154 let avb: *i64 = sys_mmap(128) as *i64
155 g_av = avb as i64
156
157 let jr: *u8 = "/tmp/mpg.jrnl" as *u8
158 let md: *u8 = "/tmp/mpg.md" as *u8
159 g_write(jr, "x\n" as *u8)
160 fixture(md)
161
162 // ---- append two slugs ----
163 avb[0] = elf as i64; avb[1] = jr as i64; avb[2] = md as i64; avb[3] = "alpha" as *u8 as i64; avb[4] = "- ALPHAV1" as *u8 as i64; avb[5] = 0
164 let rc1: i64 = g_run()
165 g_bool("put-exit0" as *u8, rc1, 0, pass)
166 avb[3] = "beta" as *u8 as i64; avb[4] = "- BETAV1" as *u8 as i64
167 g_run()
168 var ok2: i64 = 0
169 if g_fhas(md, "- ALPHAV1" as *u8) == 1 { if g_fhas(md, "- BETAV1" as *u8) == 1 { ok2 = 1 } }
170 g_bool("append-both-slugs" as *u8, ok2, 1, pass)
171
172 // ---- replace alpha IN PLACE: new text present, old gone, and STILL BEFORE beta ----
173 avb[3] = "alpha" as *u8 as i64; avb[4] = "- ALPHAV2" as *u8 as i64
174 g_run()
175 var ok3: i64 = 0
176 if g_fhas(md, "- ALPHAV2" as *u8) == 1 { if g_fhas(md, "- ALPHAV1" as *u8) == 0 { ok3 = 1 } }
177 g_bool("replace-not-duplicate" as *u8, ok3, 1, pass)
178 var ok4: i64 = 0
179 let oa: i64 = g_foff(md, "- ALPHAV2" as *u8)
180 let ob: i64 = g_foff(md, "- BETAV1" as *u8)
181 if oa > 0 { if ob > 0 { if oa < ob { ok4 = 1 } } }
182 g_bool("replace-preserves-position" as *u8, ok4, 1, pass)
183
184 // ---- the sibling's unmarked line survives every write (the clobber class) ----
185 var ok5: i64 = 0
186 if g_fhas(md, "- SIBLING-UNMARKED-LINE" as *u8) == 1 { ok5 = 1 }
187 g_bool("sibling-unmarked-line-untouched" as *u8, ok5, 1, pass)
188
189 // ---- disjoint ownership: the COINDEX block emit owns is untouched ----
190 var ok6: i64 = 0
191 if g_fhas(md, "DERIVED-LINE-OWNED-BY-EMIT" as *u8) == 1 { if g_fhas(md, "## TAILMARK" as *u8) == 1 { ok6 = 1 } }
192 g_bool("coindex-block-and-tail-untouched" as *u8, ok6, 1, pass)
193
194 // ---- idempotent: identical put leaves the file byte-identical ----
195 let snap: *u8 = sys_mmap(262144)
196 let sn: i64 = ccz_read(md, snap, 262143)
197 g_run()
198 var ok7: i64 = 0
199 if g_same(md, snap, sn) == 1 { ok7 = 1 }
200 g_bool("idempotent-byte-identical" as *u8, ok7, 1, pass)
201
202 // ---- NEG-CONTROL: an absent slug must APPEND, never hijack another slug's line ----
203 let before_sz: i64 = g_fsize(md)
204 avb[3] = "gamma" as *u8 as i64; avb[4] = "- GAMMAV1" as *u8 as i64
205 g_run()
206 var ok8: i64 = 0
207 if g_fhas(md, "- GAMMAV1" as *u8) == 1 { if g_fhas(md, "- ALPHAV2" as *u8) == 1 { if g_fhas(md, "- BETAV1" as *u8) == 1 { if g_fsize(md) > before_sz { ok8 = 1 } } } }
208 g_bool("negctl-absent-slug-appends-hijacks-nothing" as *u8, ok8, 1, pass)
209
210 // ---- FAIL-CLOSED: no CURATED markers -> file byte-untouched ----
211 let md2: *u8 = "/tmp/mpg2.md" as *u8
212 g_write(md2, "# no markers\n- body\n" as *u8)
213 let snap2: *u8 = sys_mmap(4096)
214 let sn2: i64 = ccz_read(md2, snap2, 4095)
215 avb[2] = md2 as i64; avb[3] = "delta" as *u8 as i64; avb[4] = "- DELTA" as *u8 as i64
216 let rcF: i64 = g_run()
217 var ok9: i64 = 0
218 if rcF != 0 { if g_same(md2, snap2, sn2) == 1 { ok9 = 1 } }
219 g_bool("failclosed-nomarkers-untouched-nonzero-exit" as *u8, ok9, 1, pass)
220
221 // ================= BUDGET + AUTO-EVICT (debt seq255 sev7, the SCALE half) =================
222 // The teeth above prove writes cannot CLOBBER. These prove the zone cannot GROW WITHOUT BOUND --
223 // the other half of the same debt row, and the half a WARNING does not fix.
224 let mde: *u8 = "/tmp/mpge.md" as *u8
225 let ove: *u8 = "/tmp/mpge.ovfl" as *u8
226 fixture_ev(mde)
227 fixture_ovfl(ove)
228 // three puts with NO overflow home -> nothing may be evicted (back-compat with the 4-arg form)
229 avb[0] = elf as i64; avb[1] = jr as i64; avb[2] = mde as i64; avb[5] = 0; avb[6] = 0; avb[7] = 0
230 avb[3] = "e1" as *u8 as i64; avb[4] = "- EV1" as *u8 as i64
231 g_run()
232 avb[3] = "e2" as *u8 as i64; avb[4] = "- EV2" as *u8 as i64
233 g_run()
234 avb[3] = "e3" as *u8 as i64; avb[4] = "- EV3" as *u8 as i64
235 g_run()
236 var okA: i64 = 0
237 if g_fhas(mde, "- EV1" as *u8) == 1 { if g_fhas(mde, "- EV3" as *u8) == 1 { if g_fhas(ove, "- EV1" as *u8) == 0 { okA = 1 } } }
238 g_bool("backcompat-no-ovfl-arg-never-evicts" as *u8, okA, 1, pass)
239
240 // each managed line is `- EVn<!--s:en-->\n` = 17B; budget 20 keeps exactly the NEWEST one
241 avb[3] = "e4" as *u8 as i64; avb[4] = "- EV4" as *u8 as i64; avb[5] = ove as i64; avb[6] = "20" as *u8 as i64; avb[7] = 0
242 let rcE: i64 = g_run()
243 var okB: i64 = 0
244 if rcE == 0 { if g_fhas(mde, "- EV4" as *u8) == 1 { if g_fhas(mde, "- EV1" as *u8) == 0 { if g_fhas(mde, "- EV3" as *u8) == 0 { okB = 1 } } } }
245 g_bool("evict-md-keeps-newest-only" as *u8, okB, 1, pass)
246 var okC: i64 = 0
247 if g_fhas(ove, "- EV1" as *u8) == 1 { if g_fhas(ove, "- EV3" as *u8) == 1 { if g_fhas(ove, "- EV4" as *u8) == 0 { okC = 1 } } }
248 g_bool("evict-ovfl-takes-oldest-only" as *u8, okC, 1, pass)
249 // the structural tail and the block emit owns must survive an EVICTING write too
250 var okD: i64 = 0
251 if g_fhas(mde, "DERIVED-LINE-OWNED-BY-EMIT" as *u8) == 1 { if g_fhas(mde, "## TAILMARK" as *u8) == 1 { okD = 1 } }
252 g_bool("evict-leaves-coindex-and-tail-intact" as *u8, okD, 1, pass)
253
254 // ACCUMULATION: a SECOND evicting put must ADD to the overflow, never replace it. (This is where
255 // the curated zone differs from the COINDEX rail, which re-derives its overflow from the journal.)
256 avb[3] = "e5" as *u8 as i64; avb[4] = "- EV5" as *u8 as i64
257 g_run()
258 var okE: i64 = 0
259 if g_fhas(ove, "- EV1" as *u8) == 1 { if g_fhas(ove, "- EV4" as *u8) == 1 { if g_fhas(mde, "- EV5" as *u8) == 1 { if g_fhas(ove, "- EV5" as *u8) == 0 { okE = 1 } } } }
260 g_bool("ovfl-accumulates-across-puts" as *u8, okE, 1, pass)
261 // NO-LOSS: every slug lands in EXACTLY one of the two files
262 var lost: i64 = 0
263 let nds: *i64 = sys_mmap(64) as *i64
264 nds[0] = "- EV1" as *u8 as i64
265 nds[1] = "- EV2" as *u8 as i64
266 nds[2] = "- EV3" as *u8 as i64
267 nds[3] = "- EV4" as *u8 as i64
268 nds[4] = "- EV5" as *u8 as i64
269 var ni: i64 = 0
270 while ni < 5 {
271 let nd: *u8 = nds[ni] as *u8
272 var f: i64 = 0
273 if g_fhas(mde, nd) == 1 { f = 1 }
274 if g_fhas(ove, nd) == 1 { f = f + 1 }
275 if f != 1 { lost = lost + 1 }
276 ni = ni + 1
277 }
278 g_bool("no-loss-each-slug-exactly-once" as *u8, lost, 0, pass)
279
280 // FAIL-CLOSED: a markerless overflow file -> evict NOTHING (no-loss beats budget) and leave it be
281 let mdf: *u8 = "/tmp/mpgf.md" as *u8
282 let ovnm: *u8 = "/tmp/mpgf.ovnm" as *u8
283 fixture_ev(mdf)
284 g_write(ovnm, "# no markers here NM\n- body\n" as *u8)
285 let snapn: *u8 = sys_mmap(4096)
286 let snn: i64 = ccz_read(ovnm, snapn, 4095)
287 avb[2] = mdf as i64; avb[5] = 0; avb[6] = 0; avb[7] = 0
288 avb[3] = "f1" as *u8 as i64; avb[4] = "- FV1" as *u8 as i64
289 g_run()
290 avb[3] = "f2" as *u8 as i64; avb[4] = "- FV2" as *u8 as i64
291 g_run()
292 avb[3] = "f3" as *u8 as i64; avb[4] = "- FV3" as *u8 as i64; avb[5] = ovnm as i64; avb[6] = "1" as *u8 as i64; avb[7] = 0
293 g_run()
294 var okF: i64 = 0
295 if g_fhas(mdf, "- FV1" as *u8) == 1 { if g_fhas(mdf, "- FV3" as *u8) == 1 { if g_same(ovnm, snapn, snn) == 1 { okF = 1 } } }
296 g_bool("failclosed-markerless-ovfl-evicts-nothing" as *u8, okF, 1, pass)
297
298 // ================= CONCURRENCY: the property the whole organ exists for =================
299 let mdc: *u8 = "/tmp/mpgc.md" as *u8
300 fixture_ev(mdc)
301 g_elf = elf as i64
302 g_jr = jr as i64
303 g_md = mdc as i64
304 let reaped: i64 = g_conc(8)
305 g_bool("conc-8-children-reaped" as *u8, reaped, 8, pass)
306 var present: i64 = 0
307 var q: i64 = 0
308 while q < 8 {
309 let nb2: *u8 = sys_mmap(64)
310 var no2: i64 = ccz_cat_str(nb2, 0, "- CONCLINE" as *u8)
311 no2 = ccz_cat_num(nb2, no2, q)
312 nb2[no2] = 0 as u8
313 if g_fhas(mdc, nb2) == 1 { present = present + 1 }
314 q = q + 1
315 }
316 g_bool("conc-8-writers-ZERO-LOST" as *u8, present, 8, pass)
317
318 // @file line source -- the quoting-proof path for lines carrying unicode/markdown. NEG-CONTROL
319 // included: the literal "@/tmp..." must NOT appear, proving the file was read, not the argv.
320 let mdg: *u8 = "/tmp/mpgg.md" as *u8
321 let lf: *u8 = "/tmp/mpgg.line" as *u8
322 fixture_ev(mdg)
323 g_write(lf, "- LINE-FROM-FILE-NOT-ARGV\n" as *u8)
324 let atbuf: *u8 = sys_mmap(256)
325 var ao: i64 = ccz_cat_str(atbuf, 0, "@" as *u8)
326 ao = ccz_cat_str(atbuf, ao, lf)
327 atbuf[ao] = 0 as u8
328 avb[2] = mdg as i64; avb[3] = "gfile" as *u8 as i64; avb[4] = atbuf as i64; avb[5] = 0; avb[6] = 0; avb[7] = 0
329 let rcG: i64 = g_run()
330 var okG: i64 = 0
331 if rcG == 0 { if g_fhas(mdg, "- LINE-FROM-FILE-NOT-ARGV" as *u8) == 1 { if g_fhas(mdg, "@/tmp" as *u8) == 0 { okG = 1 } } }
332 g_bool("atfile-line-source-reads-file-not-argv" as *u8, okG, 1, pass)
333
334 // ---- PER-ENTRY CAP: one verbose session must not consume the whole shared zone ----
335 // (found by dogfooding: a ~3.4KB pointer line alone exceeded the derived zone budget)
336 let mdh: *u8 = "/tmp/mpgh.md" as *u8
337 fixture_ev(mdh)
338 let lng: *u8 = sys_mmap(4096)
339 var lo2: i64 = ccz_cat_str(lng, 0, "- LONGSTART " as *u8)
340 var fi: i64 = 0
341 while fi < 400 { lng[lo2] = 120 as u8; lo2 = lo2 + 1; lng[lo2] = 32 as u8; lo2 = lo2 + 1; fi = fi + 1 }
342 lo2 = ccz_cat_str(lng, lo2, "LONGEND" as *u8)
343 lng[lo2] = 0 as u8
344 avb[2] = mdh as i64; avb[3] = "hlong" as *u8 as i64; avb[4] = lng as i64; avb[5] = 0; avb[6] = 0; avb[7] = 0
345 g_run()
346 var okH: i64 = 0
347 if g_fhas(mdh, "- LONGSTART" as *u8) == 1 { if g_fhas(mdh, "LONGEND" as *u8) == 0 { if g_fhas(mdh, "..." as *u8) == 1 { okH = 1 } } }
348 g_bool("entry-cap-trims-verbose-line-keeps-head" as *u8, okH, 1, pass)
349
350 // ---- a call must NEVER evict the line it was just asked to bank ----
351 // (found by dogfooding: upsert preserves the OLD position, so a refreshed pointer sat in the
352 // evict range and was thrown out by the very call that wrote it)
353 let mdi: *u8 = "/tmp/mpgi.md" as *u8
354 let ovi: *u8 = "/tmp/mpgi.ovfl" as *u8
355 fixture_ev(mdi)
356 fixture_ovfl(ovi)
357 avb[2] = mdi as i64; avb[5] = 0; avb[6] = 0; avb[7] = 0
358 avb[3] = "a1" as *u8 as i64; avb[4] = "- AV1" as *u8 as i64
359 g_run()
360 avb[3] = "a2" as *u8 as i64; avb[4] = "- AV2" as *u8 as i64
361 g_run()
362 avb[3] = "a3" as *u8 as i64; avb[4] = "- AV3" as *u8 as i64
363 g_run()
364 avb[3] = "a1" as *u8 as i64; avb[4] = "- AV1NEW" as *u8 as i64; avb[5] = ovi as i64; avb[6] = "20" as *u8 as i64; avb[7] = 0
365 g_run()
366 var okI: i64 = 0
367 if g_fhas(mdi, "- AV1NEW" as *u8) == 1 { if g_fhas(ovi, "- AV1NEW" as *u8) == 0 { okI = 1 } }
368 g_bool("never-evicts-the-line-this-call-wrote" as *u8, okI, 1, pass)
369
370 g_puts("MPG-GATE pass=" as *u8); g_putn(pass[0]); g_puts("/21 verdict=" as *u8)
371 if pass[0] == 21 { g_puts("GREEN\n" as *u8); return 0 }
372 g_puts("RED\n" as *u8)
373 return 1
374}