nx_synthroom_gate.nx source
↩ module page · 196 lines · 11160 B
1// nx_synthroom_gate.nx -- GATE for the room protocol (nx_synthroom_lib, /compare/synthroom rung SR1).
2//
3// THE LOAD-BEARING TEETH ARE T8 AND T9: the SAME log replayed twice yields BYTE-IDENTICAL intent streams,
4// and the intent count is a PARTITION of the log (one row per event, none skipped). Everything else here
5// checks a shape; those two check the contract the board promises.
6// The neg-controls are the wire's three rules made falsifiable: a duplicate nonce is REFUSED (never
7// double-applied), an unknown verb is REFUSED on the way in, a corrupt row is REFUSED on the way out with
8// its index, and a menu without a fallback is REFUSED before the first tip.
9//
10// The lib is exercised IN-PROCESS so a mutation bite reaches it; the fixture lives under /tmp/<gate>/
11// created at SETUP (a teardown does not run when a run crashes) and the log is unlinked at setup so the
12// gate is idempotent -- a gate that is not idempotent reports on its first run and lies about every run
13// after. The comment character is CONSTRUCTED (SR_CH_HASH) because a literal hash inside a string is an
14// nx_cc lexer trap.
15// license_tier: ORIGINAL No hw writes (Rule 26).
16import "nx_syscalls.nx"
17import "nx_synthroom_lib.nx"
18import "nx_gate_verdict.nx"
19
20const SG_DIR: *u8 = "/tmp/nx_synthroom_gate" as *u8
21const SG_MENU: *u8 = "/tmp/nx_synthroom_gate/menu.conf" as *u8
22const SG_BADMENU: *u8 = "/tmp/nx_synthroom_gate/menu_nofallback.conf" as *u8
23const SG_LOG: *u8 = "/tmp/nx_synthroom_gate/room.log" as *u8
24const SG_BADLOG: *u8 = "/tmp/nx_synthroom_gate/corrupt.log" as *u8
25const SG_ROWS: i64 = 16
26const SG_WORD: i64 = 8
27const SG_OUT: i64 = 16384
28const SG_TS: i64 = 1787840000
29// the fixture menu: three tiers and a fallback. Amounts chosen so every branch of sr_menu_intent fires.
30const SG_MENU_ROWS: i64 = 3
31const SG_TIP_TOP: i64 = 500
32const SG_TIP_MID: i64 = 120
33const SG_TIP_LOW: i64 = 25
34const SG_TIP_UNDER: i64 = 3
35// the fixture log: seven events, one per verb
36const SG_EVENTS: i64 = 7
37
38func sg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
39
40// write a whole file (truncate) -- fixture helper, not the subject
41func sg_put(path: *u8, body: *u8) -> i64 {
42 let fd: i64 = sys_openat_wr(path, MODE_0644)
43 if fd < 0 { return 0 }
44 let n: i64 = sg_slen(body)
45 let w: i64 = sys_write(fd, body, n)
46 sys_close(fd)
47 if w != n { return 0 }
48 return 1
49}
50
51func sg_bufeq(a: *u8, an: i64, b: *u8, bn: i64) -> i64 {
52 if an != bn { return 0 }
53 var i: i64 = 0
54 while i < an { if a[i] != b[i] { return 0 } i = i + 1 }
55 return 1
56}
57
58func sg_append(nonce: *u8, verb: *u8, actor: *u8, a1: *u8, a2: *u8, line: *u8, scratch: *u8, lp: *i64) -> i64 {
59 return sr_event_append(SG_LOG, nonce, SG_TS, verb, actor, a1, a2, line, SR_LINE, scratch, lp)
60}
61
62func main() -> i64 {
63 let ctr: *i64 = gv_ctr()
64 gv_head("nx_synthroom -- the room protocol: append-only events, a tip menu as data, bit-identical replay" as *u8)
65
66 // ---- SETUP: fixture dir, menu conf with a CONSTRUCTED comment line, a fresh log ----
67 sys_mkdir(SG_DIR, MODE_0755)
68 sys_unlinkat(SG_LOG)
69 sys_unlinkat(SG_BADLOG)
70 let menu: *u8 = sys_mmap(SR_LINE)
71 var mo: i64 = 0
72 menu[mo] = SR_CH_HASH as u8; mo = mo + 1
73 mo = sr_cat(menu, mo, " fixture menu\nmenu|kiss|25|blow_kiss\nmenu|dance|120|dance_short\nmenu|dance|500|dance_long\nfallback|thank_you\n" as *u8)
74 menu[mo] = 0 as u8
75 let put1: i64 = sg_put(SG_MENU, menu)
76 let put2: i64 = sg_put(SG_BADMENU, "menu|kiss|25|blow_kiss\n" as *u8)
77 gv_need("fixture menu confs written under /tmp/nx_synthroom_gate" as *u8, put1 & put2, ctr)
78
79 let lp: *i64 = sys_mmap(SG_WORD * 2) as *i64
80 let why: *i64 = sys_mmap(SG_WORD) as *i64
81 let fb: *i64 = sys_mmap(SG_WORD) as *i64
82 let tab: *i64 = sys_mmap(SG_ROWS * SR_M_STRIDE * SR_I64_BYTES) as *i64
83 let rows: i64 = sr_menu_load(SG_MENU, tab, SG_ROWS, fb, why, lp)
84 gv_check("T1 the menu conf parses to three tiers, the comment line skipped" as *u8, (rows == SG_MENU_ROWS) as i64, ctr)
85 var t2: i64 = 0
86 var t3: i64 = 0
87 var t4: i64 = 0
88 var t5: i64 = 0
89 if rows == SG_MENU_ROWS {
90 let fbp: *u8 = fb[0] as *u8
91 if sr_streq(sr_menu_intent(tab, rows, fbp, SG_TIP_TOP, SR_EMPTY), "dance_long" as *u8) == 1 { t2 = 1 }
92 if sr_streq(sr_menu_intent(tab, rows, fbp, SG_TIP_MID, "dance" as *u8), "dance_short" as *u8) == 1 { t3 = 1 }
93 if sr_streq(sr_menu_intent(tab, rows, fbp, SG_TIP_UNDER, SR_EMPTY), "thank_you" as *u8) == 1 { t4 = 1 }
94 // a named item the amount does not reach falls back rather than silently taking a cheaper item
95 if sr_streq(sr_menu_intent(tab, rows, fbp, SG_TIP_LOW, "dance" as *u8), "thank_you" as *u8) == 1 { t5 = 1 }
96 }
97 gv_check("T2 an unnamed tip takes the HIGHEST tier its amount reaches" as *u8, t2, ctr)
98 gv_check("T3 a named item takes that item's tier when the amount reaches it" as *u8, t3, ctr)
99 gv_check("T4 a tip below every threshold maps to the declared fallback, never to nothing" as *u8, t4, ctr)
100 gv_check("T5 a named item the amount does not reach falls back rather than buying a cheaper item" as *u8, t5, ctr)
101
102 // ---- the writer: one event per verb ----
103 let line: *u8 = sys_mmap(SR_LINE)
104 let scratch: *u8 = sys_mmap(SR_SCRATCH)
105 var okw: i64 = 1
106 if sg_append("n1" as *u8, "enter" as *u8, "alice" as *u8, SR_EMPTY, SR_EMPTY, line, scratch, lp) != SR_OK { okw = 0 }
107 if sg_append("n2" as *u8, "say" as *u8, "alice" as *u8, "hello" as *u8, SR_EMPTY, line, scratch, lp) != SR_OK { okw = 0 }
108 if sg_append("n3" as *u8, "tip" as *u8, "alice" as *u8, "120" as *u8, "dance" as *u8, line, scratch, lp) != SR_OK { okw = 0 }
109 if sg_append("n4" as *u8, "gesture" as *u8, "alice" as *u8, "wave" as *u8, SR_EMPTY, line, scratch, lp) != SR_OK { okw = 0 }
110 if sg_append("n5" as *u8, "command" as *u8, "alice" as *u8, "turn" as *u8, "left" as *u8, line, scratch, lp) != SR_OK { okw = 0 }
111 if sg_append("n6" as *u8, "toy" as *u8, "alice" as *u8, "level2" as *u8, SR_EMPTY, line, scratch, lp) != SR_OK { okw = 0 }
112 if sg_append("n7" as *u8, "leave" as *u8, "alice" as *u8, SR_EMPTY, SR_EMPTY, line, scratch, lp) != SR_OK { okw = 0 }
113 gv_check("T6 seven events, one per verb, append and each is accepted" as *u8, okw, ctr)
114
115 let dup: i64 = sg_append("n3" as *u8, "tip" as *u8, "alice" as *u8, "120" as *u8, "dance" as *u8, line, scratch, lp)
116 gv_check("neg-control-duplicate-nonce-refused a retry with a nonce already in the log is REFUSED by name, never double-applied" as *u8, (dup == SR_D_DUPNONCE) as i64, ctr)
117 let badv: i64 = sg_append("n8" as *u8, "teleport" as *u8, "alice" as *u8, SR_EMPTY, SR_EMPTY, line, scratch, lp)
118 gv_check("neg-control-unknown-verb-refused a verb outside the vocabulary is REFUSED on the way in" as *u8, (badv == SR_D_BADVERB) as i64, ctr)
119 let badn: i64 = sg_append("n9|x" as *u8, "say" as *u8, "alice" as *u8, "hi" as *u8, SR_EMPTY, line, scratch, lp)
120 gv_check("neg-control-separator-in-nonce-refused a nonce carrying the wire separator is REFUSED" as *u8, (badn == SR_D_BADNONCE) as i64, ctr)
121
122 // the log must hold exactly the seven accepted rows -- the refusals wrote nothing
123 let lg: *u8 = sys_read_file(SG_LOG, lp)
124 var nlines: i64 = 0
125 var ln: i64 = 0
126 if (lg as i64) != 0 {
127 ln = lp[0]
128 var i: i64 = 0
129 while i < ln { if lg[i] == (SR_CH_NL as u8) { nlines = nlines + 1 } i = i + 1 }
130 }
131 gv_check("T7 the log holds exactly seven rows: every refusal left it unchanged" as *u8, (nlines == SG_EVENTS) as i64, ctr)
132
133 // ---- the reader: replay twice from two independent reads, compare bytes ----
134 let out1: *u8 = sys_mmap(SG_OUT)
135 let out2: *u8 = sys_mmap(SG_OUT)
136 let c1: *i64 = sys_mmap(SG_WORD) as *i64
137 let c2: *i64 = sys_mmap(SG_WORD) as *i64
138 let b1: *i64 = sys_mmap(SG_WORD) as *i64
139 let b2: *i64 = sys_mmap(SG_WORD) as *i64
140 var r1: i64 = 0 - 1
141 var r2: i64 = 0 - 1
142 var o1: i64 = 0
143 var o2: i64 = 0
144 if (lg as i64) != 0 { if rows == SG_MENU_ROWS {
145 r1 = sr_replay(lg, ln, tab, rows, fb[0] as *u8, out1, SG_OUT, c1, b1)
146 o1 = sg_slen(out1)
147 let lg2: *u8 = sys_read_file(SG_LOG, lp)
148 if (lg2 as i64) != 0 {
149 r2 = sr_replay(lg2, lp[0], tab, rows, fb[0] as *u8, out2, SG_OUT, c2, b2)
150 o2 = sg_slen(out2)
151 }
152 } }
153 var t8: i64 = 0
154 if r1 == SR_OK { if r2 == SR_OK { if sg_bufeq(out1, o1, out2, o2) == 1 { if o1 > 0 { t8 = 1 } } } }
155 gv_check("T8 the same log replayed twice yields BYTE-IDENTICAL intent streams" as *u8, t8, ctr)
156 var t9: i64 = 0
157 if r1 == SR_OK { if c1[0] == SG_EVENTS { t9 = 1 } }
158 gv_check("T9 the intent count is a partition of the log: seven events, seven intents, none skipped" as *u8, t9, ctr)
159 var t10: i64 = 0
160 if r1 == SR_OK { if sr_has(out1, o1, "|dance_short|alice|120|n3" as *u8) == 1 { t10 = 1 } }
161 gv_check("T10 the tip event derives its intent THROUGH the menu: 120 for dance is dance_short" as *u8, t10, ctr)
162 var t11: i64 = 0
163 if r1 == SR_OK { if sr_has(out1, o1, "|turn|alice|0|n5" as *u8) == 1 { if sr_has(out1, o1, "|enter|alice|0|n1" as *u8) == 1 { t11 = 1 } } }
164 gv_check("T11 a command carries its own name as the intent and a bare enter is its verb" as *u8, t11, ctr)
165 gv_puts(" replay bytes=" as *u8); gv_num(o1); gv_puts(" intents=" as *u8); gv_num(c1[0]); gv_puts("\n" as *u8)
166
167 // ---- corrupt log: a row that is not an event row is REFUSED with its index ----
168 let putc: i64 = sg_put(SG_BADLOG, "ev|c1|1787840000|enter|bob|-|-\nnot an event row\nev|c3|1787840000|say|bob|hi|-\n" as *u8)
169 var t12: i64 = 0
170 if putc == 1 { if rows == SG_MENU_ROWS {
171 let cl: *u8 = sys_read_file(SG_BADLOG, lp)
172 if (cl as i64) != 0 {
173 let out3: *u8 = sys_mmap(SG_OUT)
174 let c3: *i64 = sys_mmap(SG_WORD) as *i64
175 let b3: *i64 = sys_mmap(SG_WORD) as *i64
176 let r3: i64 = sr_replay(cl, lp[0], tab, rows, fb[0] as *u8, out3, SG_OUT, c3, b3)
177 if r3 == SR_D_UNPARSED { if b3[0] == 1 { t12 = 1 } }
178 }
179 } }
180 gv_check("neg-control-corrupt-row-refused-with-index a log row that is not an event row is REFUSED naming row 1, never skipped" as *u8, t12, ctr)
181
182 // ---- menu without a fallback: refused at parse time, before any tip ----
183 let tab2: *i64 = sys_mmap(SG_ROWS * SR_M_STRIDE * SR_I64_BYTES) as *i64
184 let fb2: *i64 = sys_mmap(SG_WORD) as *i64
185 let why2: *i64 = sys_mmap(SG_WORD) as *i64
186 let rows2: i64 = sr_menu_load(SG_BADMENU, tab2, SG_ROWS, fb2, why2, lp)
187 var badfires: i64 = 0
188 if rows2 < 0 { if why2[0] == SR_D_NOFALLBACK { badfires = 1 } }
189 var goodsilent: i64 = 1
190 if rows < 0 { goodsilent = 0 }
191 gv_bite("neg-control-menu-without-fallback-refused the parser fires on a menu with no fallback and stays silent on the good menu" as *u8, badfires, (goodsilent == 0) as i64, ctr)
192
193 let rc: i64 = gv_verdict("SYNTHROOM-PROTOCOL" as *u8, ctr, "append-only events with nonce idempotence, a tip menu as data, and bit-identical replay" as *u8)
194 sys_exit(rc)
195 return rc
196}