code wiki / _hdl_build / nx_frontier_store_gate.nx
nx_frontier_store_gate.nx source
↩ module page · 59 lines · 2922 B
1// nx_frontier_store_gate.nx -- F-201 (store-law) verification with a NEGATIVE CONTROL.
2// Proves the frontier backlog round-trips through the SOVEREIGN seg-store: frs_seed a fixture into an
3// ISOLATED /tmp store -> frs_load reconstructs the exact rows; a re-seed with a changed row is REFLECTED
4// (live store read, not cached); a never-seeded prefix loads empty. Exit 0 = GREEN.
5// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
6import "nx_frontier_store.nx"
7import "nx_syscalls.nx"
8
9const G_PFX: *u8 = "/tmp/frtest-a-"
10const G_PFX_FRESH: *u8 = "/tmp/frtest-never-"
11const G_CAP: i64 = 65536
12const G_NROWS: i64 = 2 // fixture has 2 real rows
13
14func g_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
15func g_w(s: *u8) -> i64 { sys_write(1, s, g_slen(s)); return 0 }
16// 1 if needle (cstr) occurs in h[0..hn)
17func g_find(h: *u8, hn: i64, needle: *u8) -> i64 {
18 let nn: i64 = g_slen(needle)
19 if nn == 0 { return 1 }
20 var i: i64 = 0
21 while i + nn <= hn {
22 var j: i64 = 0
23 var ok: i64 = 1
24 while j < nn { if h[i+j] != needle[j] { ok = 0; j = nn } else { j = j + 1 } }
25 if ok == 1 { return 1 }
26 i = i + 1
27 }
28 return 0
29}
30func g_fail(s: *u8) -> i64 { g_w("VERDICT RED -- " as *u8); g_w(s); g_w("\n" as *u8); sys_exit(1); return 1 }
31
32func main() -> i64 {
33 let out: *u8 = sys_mmap(G_CAP)
34 // fixture: a comment + 2 rows (B depends on A, B DONE)
35 let fx: *u8 = "# hdr\nA\tfoo\t9\t1\town\tT\t-\t-\tlane\nB\tbar\t8\t2\town\tD\tA\t-\tlane\n" as *u8
36 let n1: i64 = frs_seed(G_PFX, fx, g_slen(fx))
37 if n1 != G_NROWS { g_fail("T1 seed row count != 2" as *u8) }
38
39 // T2: load reconstructs both rows (comment dropped), joined by newline
40 let m: i64 = frs_load(G_PFX, out, G_CAP)
41 if m <= 0 { g_fail("T2 load empty after seed" as *u8) }
42 if g_find(out, m, "A\tfoo\t9\t1\town\tT\t-\t-\tlane" as *u8) != 1 { g_fail("T2 row A missing" as *u8) }
43 if g_find(out, m, "B\tbar\t8\t2\town\tD\tA\t-\tlane" as *u8) != 1 { g_fail("T2 row B missing" as *u8) }
44 if g_find(out, m, "# hdr" as *u8) == 1 { g_fail("T2 comment leaked into store" as *u8) }
45
46 // T3 NEG-CONTROL: re-seed with B flipped D->T; the LIVE store read must reflect it
47 let fx2: *u8 = "# hdr\nA\tfoo\t9\t1\town\tT\t-\t-\tlane\nB\tbar\t8\t2\town\tT\tA\t-\tlane\n" as *u8
48 frs_seed(G_PFX, fx2, g_slen(fx2))
49 let m2: i64 = frs_load(G_PFX, out, G_CAP)
50 if g_find(out, m2, "B\tbar\t8\t2\town\tT\tA" as *u8) != 1 { g_fail("T3 re-seed not reflected (stale read)" as *u8) }
51
52 // T4 NEG-CONTROL: a never-seeded prefix loads EMPTY (no phantom rows)
53 let m3: i64 = frs_load(G_PFX_FRESH, out, G_CAP)
54 if m3 != 0 { g_fail("T4 unseeded prefix returned data" as *u8) }
55
56 g_w("VERDICT GREEN nx_frontier_store (4/4: seed count + round-trip + comment-drop + neg-control reseed/empty)\n" as *u8)
57 sys_exit(0)
58 return 0
59}