nx_state_spool_gate.nx source
↩ module page · 118 lines · 5001 B
1// nx_state_spool_gate.nx -- liar-killed GATE for the store-and-forward state spool (CR-R1a).
2// Proves NAS-first/local-fallback semantics OFFLINE via the deterministic fixture transport
3// (nx_spool_txfix: argv[1] contains "ok" -> delivered, else fail): spooled lines persist; a
4// working transport drains them; a FAILING transport keeps them (offline = NOTHING LOST -- the
5// negative control); partial failure keeps exactly the failed lines in order without blocking
6// later lines; a MISSING transport binary keeps everything (fail-safe, never fabricates
7// delivery); empty spool is a no-op. usage: nx_state_spool_gate [txfix_elf]
8// license_tier: ORIGINAL expect_exit: 0
9import "nx_syscalls.nx"
10import "nx_state_spool_core.nx"
11
12func t_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
13
14func t_putn(v: i64) -> i64 {
15 let b: *u8 = sys_mmap(32)
16 let e: i64 = ccz_cat_num(b, 0, v)
17 sys_write(1, b, e)
18 return 0
19}
20
21func t_check(name: *u8, got: i64, want: i64, passp: *i64) -> i64 {
22 t_puts("T " as *u8)
23 t_puts(name)
24 t_puts(" got=" as *u8)
25 t_putn(got)
26 t_puts(" want=" as *u8)
27 t_putn(want)
28 if got == want { t_puts(" PASS\n" as *u8); passp[0] = passp[0] + 1 } else { t_puts(" FAIL\n" as *u8) }
29 return 0
30}
31
32// count occurrences of needle in the spool file (bounded read)
33func t_count(path: *u8, needle: *u8) -> i64 {
34 let buf: *u8 = sys_mmap(65536)
35 let n: i64 = ccz_read(path, buf, 65535)
36 if n <= 0 { return 0 }
37 let nl: i64 = ccz_slen(needle)
38 var cnt: i64 = 0
39 var i: i64 = 0
40 while i + nl <= n {
41 var k: i64 = 0
42 var ok: i64 = 1
43 while k < nl { if buf[i+k] != needle[k] { ok = 0; k = nl } k = k + 1 }
44 if ok == 1 { cnt = cnt + 1; i = i + nl } else { i = i + 1 }
45 }
46 return cnt
47}
48
49func main(argc: i64, argv: *i64) -> i64 {
50 var tx: *u8 = "/tmp/nx_spool_txfix.sov.elf" as *u8
51 if argc >= 2 { tx = argv[1] as *u8 }
52 let pass: *i64 = sys_mmap(16) as *i64
53 pass[0] = 0
54 let sp: *u8 = "/tmp/ssp_gate.spool" as *u8
55 let lk: *u8 = "/tmp/ssp_gate.spool.lock" as *u8
56 let tp: *u8 = "/tmp/ssp_gate.spool.tmp" as *u8
57 let sent: *i64 = sys_mmap(16) as *i64
58 let kept: *i64 = sys_mmap(16) as *i64
59
60 // reset any prior fixture state (drain-to-empty with a spool that may not exist is T6's job;
61 // here just truncate)
62 let rfd: i64 = sys_openat_wr(sp, 420)
63 if rfd >= 0 { sys_close(rfd) }
64
65 // T1 spool persists lines
66 ssp_spool(sp, lk, "beat ok alpha" as *u8)
67 ssp_spool(sp, lk, "beat ok bravo" as *u8)
68 t_check("spool-persists" as *u8, t_count(sp, "beat ok " as *u8), 2, pass)
69
70 // T2 drain with working transport -> all delivered, spool empty
71 ssp_drain(sp, lk, tp, tx, sent, kept)
72 var ok2: i64 = 0
73 if sent[0] == 2 { if kept[0] == 0 { if t_count(sp, "beat" as *u8) == 0 { ok2 = 1 } } }
74 t_check("drain-delivers-all" as *u8, ok2, 1, pass)
75
76 // T3 NEG-CONTROL: failing transport -> nothing lost (offline is a normal state)
77 ssp_spool(sp, lk, "beat FAIL charlie" as *u8)
78 ssp_drain(sp, lk, tp, tx, sent, kept)
79 var ok3: i64 = 0
80 if sent[0] == 0 { if kept[0] == 1 { if t_count(sp, "FAIL charlie" as *u8) == 1 { ok3 = 1 } } }
81 t_check("negctl-offline-keeps" as *u8, ok3, 1, pass)
82
83 // T4 partial: ok + FAIL + ok -> 2 delivered, exactly the failed one kept
84 ssp_spool(sp, lk, "beat ok delta" as *u8)
85 ssp_spool(sp, lk, "beat ok echo" as *u8)
86 ssp_drain(sp, lk, tp, tx, sent, kept)
87 var ok4: i64 = 0
88 if sent[0] == 2 { if kept[0] == 1 { if t_count(sp, "FAIL charlie" as *u8) == 1 { if t_count(sp, "ok delta" as *u8) == 0 { ok4 = 1 } } } }
89 t_check("partial-drain-order" as *u8, ok4, 1, pass)
90
91 // T5 head-of-line non-blocking: a new deliverable line drains PAST the stuck one
92 ssp_spool(sp, lk, "beat ok foxtrot" as *u8)
93 ssp_drain(sp, lk, tp, tx, sent, kept)
94 var ok5: i64 = 0
95 if sent[0] == 1 { if kept[0] == 1 { if t_count(sp, "FAIL charlie" as *u8) == 1 { ok5 = 1 } } }
96 t_check("head-of-line-nonblocking" as *u8, ok5, 1, pass)
97
98 // T6 missing transport binary -> exec fails (127) -> everything kept (never fabricates delivery)
99 ssp_drain(sp, lk, tp, "/tmp/ssp_gate_no_such_transport.elf" as *u8, sent, kept)
100 var ok6: i64 = 0
101 if sent[0] == 0 { if kept[0] == 1 { if t_count(sp, "FAIL charlie" as *u8) == 1 { ok6 = 1 } } }
102 t_check("missing-transport-failsafe" as *u8, ok6, 1, pass)
103
104 // T7 empty spool drain = clean no-op (drain the kept line away first with a fresh truncate)
105 let zfd: i64 = sys_openat_wr(sp, 420)
106 if zfd >= 0 { sys_close(zfd) }
107 ssp_drain(sp, lk, tp, tx, sent, kept)
108 var ok7: i64 = 0
109 if sent[0] == 0 { if kept[0] == 0 { ok7 = 1 } }
110 t_check("empty-spool-noop" as *u8, ok7, 1, pass)
111
112 t_puts("SSP-GATE pass=" as *u8)
113 t_putn(pass[0])
114 t_puts("/7 verdict=" as *u8)
115 if pass[0] == 7 { t_puts("GREEN\n" as *u8); return 0 }
116 t_puts("RED\n" as *u8)
117 return 1
118}