code wiki / _hdl_build / nx_proc_snapshot_gate.nx
nx_proc_snapshot_gate.nx source
↩ module page · 198 lines · 10135 B
1// nx_proc_snapshot_gate.nx -- proves the seq1318 fix is CORRECT (same answers) and ACTUALLY O(P)
2// (one walk serves many questions). Every tooth fires on the BAD state and is silent on the good one.
3//
4// The two teeth that matter, and why they are not vacuous:
5// T5 EQUIVALENCE vs THE ORACLE: for a battery of names -- present, absent, and every name this
6// supervisor actually guards -- snapshot answer MUST equal the direct per-name /proc scan. The
7// oracle is the pre-existing implementation, so this proves "no behaviour changed", not "the new
8// code agrees with itself".
9// T6 THE O(P) PROPERTY ITSELF: 25 queries after one refresh must leave the BUILD COUNTER at 1. A
10// correctness-only gate would pass even if the fix silently rebuilt per query -- i.e. if the
11// defect were still there. This measures the fix, not just its output.
12// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
13import "nx_proc_snapshot.nx"
14import "nx_syscalls.nx"
15
16const GT_QUERIES: i64 = 25 // the ~25 guarded services of the real poll
17const GT_SPANCAP: i64 = 512
18const GT_STDOUT: i64 = 1
19
20func gt_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
21func gt_puts(s: *u8) -> i64 { sys_write(GT_STDOUT, s, gt_slen(s)); return 0 }
22func gt_putn(v: i64) -> i64 {
23 let t: *u8 = sys_mmap(32); var m: i64 = v
24 if m < 0 { m = 0 - m; sys_write(GT_STDOUT, "-" as *u8, 1) }
25 var k: i64 = 0
26 if m == 0 { t[0] = 48 as u8; k = 1 }
27 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
28 let b: *u8 = sys_mmap(32); var i: i64 = 0
29 while i < k { b[i] = t[k-1-i]; i = i + 1 }
30 sys_write(GT_STDOUT, b, k)
31 return 0
32}
33// a tooth: fires (prints FAIL, returns 1) when `bad` is 1
34func gt_bite(bad: i64, id: *u8, why: *u8) -> i64 {
35 if bad == 1 { gt_puts("FAIL " as *u8); gt_puts(id); gt_puts(": " as *u8); gt_puts(why); gt_puts("\n" as *u8); return 1 }
36 gt_puts("ok " as *u8); gt_puts(id); gt_puts("\n" as *u8)
37 return 0
38}
39
40func main(argc: i64, argv: *i64) -> i64 {
41 var fails: i64 = 0
42
43 // T1 -- a build must succeed on a live box and see a plausible process population
44 let cnt: i64 = ps_refresh()
45 var bad: i64 = 0
46 if cnt <= 0 { bad = 1 }
47 fails = fails + gt_bite(bad, "T1-build" as *u8, "ps_refresh returned no processes (a live box always has some)" as *u8)
48
49 // T2 -- the snapshot must be VALID and its age sane right after a build
50 bad = 0
51 if ps_valid() != 1 { bad = 1 }
52 let age: i64 = ps_age_ms()
53 if age < 0 { bad = 1 }
54 fails = fails + gt_bite(bad, "T2-valid" as *u8, "snapshot not valid / negative age immediately after refresh" as *u8)
55
56 // T3 -- PRESENT: this gate's own process is in /proc by construction, so its own name must be found
57 bad = 0
58 if ps_alive_snap("nx_proc_snapshot_gate" as *u8) != 1 { bad = 1 }
59 fails = fails + gt_bite(bad, "T3-self-present" as *u8, "snapshot cannot find the gate's OWN cmdline (it is provably running)" as *u8)
60
61 // T4 -- ABSENT: a name that cannot exist must be 0, never 1 (no false-alive)
62 bad = 0
63 if ps_alive_snap("zzz_no_such_daemon_zzz_9174" as *u8) != 0 { bad = 1 }
64 fails = fails + gt_bite(bad, "T4-absent" as *u8, "snapshot reported a nonexistent daemon ALIVE" as *u8)
65
66 // T5 -- EQUIVALENCE vs THE ORACLE across the real guarded set (the non-vacuity tooth)
67 let names: *i64 = sys_mmap(64 * 8) as *i64
68 names[0] = "nx_proc_snapshot_gate" as *u8 as i64
69 names[1] = "zzz_no_such_daemon_zzz_9174" as *u8 as i64
70 names[2] = "sites.elf" as *u8 as i64
71 names[3] = "nx_mgmt_api.elf" as *u8 as i64
72 names[4] = "nx_tools_api_serve.elf" as *u8 as i64
73 names[5] = "nx_gallery_serve.elf" as *u8 as i64
74 names[6] = "nx_gallery_gateway.elf" as *u8 as i64
75 names[7] = "nx_wiki_gw.elf" as *u8 as i64
76 names[8] = "nx_torrent_seed.elf" as *u8 as i64
77 names[9] = "nx_docportal_admin_daemon.elf" as *u8 as i64
78 names[10] = "nx_email_portal_daemon.elf" as *u8 as i64
79 names[11] = "nx_siteedit_daemon.elf" as *u8 as i64
80 names[12] = "nx_vroom_daemon.elf" as *u8 as i64
81 names[13] = "redirect.elf" as *u8 as i64
82 names[14] = "nx_clock_tickless.elf" as *u8 as i64
83 names[15] = "nx_media_server_auth.elf" as *u8 as i64
84 let nn: i64 = 16
85 var mismatch: i64 = 0
86 var firstbad: i64 = 0 - 1
87 var i: i64 = 0
88 while i < nn {
89 let nm: *u8 = names[i] as *u8
90 let a: i64 = ps_alive_snap(nm)
91 let b: i64 = ps_alive_direct(nm)
92 if a != b { mismatch = mismatch + 1; if firstbad < 0 { firstbad = i } }
93 i = i + 1
94 }
95 bad = 0
96 if mismatch > 0 { bad = 1 }
97 fails = fails + gt_bite(bad, "T5-oracle-equivalence" as *u8, "snapshot DISAGREED with the direct /proc scan (behaviour changed)" as *u8)
98 if mismatch > 0 { gt_puts(" mismatches=" as *u8); gt_putn(mismatch); gt_puts(" first_idx=" as *u8); gt_putn(firstbad); gt_puts("\n" as *u8) }
99
100 // T6 -- THE O(P) PROPERTY: many queries, ONE walk. This is the tooth that measures the FIX.
101 ps_refresh()
102 let b0: i64 = ps_builds()
103 var q: i64 = 0
104 while q < GT_QUERIES { ps_alive_snap("sites.elf" as *u8); q = q + 1 }
105 let b1: i64 = ps_builds()
106 bad = 0
107 if b1 != b0 { bad = 1 }
108 fails = fails + gt_bite(bad, "T6-one-walk-many-queries" as *u8, "the snapshot REBUILT during the query burst -- still O(S x P), the defect is not fixed" as *u8)
109 gt_puts(" builds_before=" as *u8); gt_putn(b0); gt_puts(" after_" as *u8); gt_putn(GT_QUERIES); gt_puts("_queries=" as *u8); gt_putn(b1); gt_puts("\n" as *u8)
110
111 // T7 -- INVALIDATION really forces a rebuild (the spawn/kill safety property)
112 let b2: i64 = ps_builds()
113 ps_invalidate()
114 bad = 0
115 if ps_valid() != 0 { bad = 1 }
116 ps_alive_snap("sites.elf" as *u8)
117 if ps_builds() != b2 + 1 { bad = 1 }
118 fails = fails + gt_bite(bad, "T7-invalidate-rebuilds" as *u8, "after ps_invalidate the next query did NOT rebuild (a just-spawned daemon could read as dead)" as *u8)
119
120 // T8 -- SPAN SAFETY: a needle straddling two cmdline records must NOT match. Built from the blob
121 // itself: take the bytes around a real separator, which is a string that exists in the blob ONLY
122 // as a cross-record span. A naive concatenation without a separator would match it.
123 bad = 0
124 let blen: i64 = ps_blob_len()
125 if blen <= 0 { bad = 1 } else {
126 var sepi: i64 = 0 - 1
127 var s: i64 = 8
128 while s < blen - 8 {
129 if sepi < 0 { if ps_blob[s] == (1 as u8) { sepi = s } }
130 s = s + 1
131 }
132 if sepi < 0 { bad = 1 } else {
133 // span = 4 bytes before the separator + 4 bytes after it, with the separator REMOVED
134 let span: *u8 = sys_mmap(GT_SPANCAP)
135 var o: i64 = 0
136 var k: i64 = sepi - 4
137 while k < sepi { span[o] = ps_blob[k]; o = o + 1; k = k + 1 }
138 k = sepi + 1
139 while k < sepi + 5 { span[o] = ps_blob[k]; o = o + 1; k = k + 1 }
140 span[o] = 0 as u8
141 if ps_contains(ps_blob, blen, span, o) == 1 { bad = 1 }
142 }
143 }
144 fails = fails + gt_bite(bad, "T8-span-safety" as *u8, "a needle spanning TWO cmdlines matched -- record separation is broken (false-alive class)" as *u8)
145
146 // T9 -- the production entry point must agree with the oracle too (fallback path included)
147 bad = 0
148 if ps_alive_or_direct("nx_proc_snapshot_gate" as *u8) != ps_alive_direct("nx_proc_snapshot_gate" as *u8) { bad = 1 }
149 if ps_alive_or_direct("zzz_no_such_daemon_zzz_9174" as *u8) != 0 { bad = 1 }
150 fails = fails + gt_bite(bad, "T9-production-entry" as *u8, "ps_alive_or_direct disagreed with the oracle" as *u8)
151
152 // T10 -- empty needle must not be treated as a wildcard match against a real question
153 bad = 0
154 if ps_contains("abc" as *u8, 3, "zz" as *u8, 2) != 0 { bad = 1 }
155 if ps_contains("abc" as *u8, 3, "bc" as *u8, 2) != 1 { bad = 1 }
156 fails = fails + gt_bite(bad, "T10-contains-core" as *u8, "the byte-run matcher itself is wrong" as *u8)
157
158 // T11 -- ASYMMETRY: an ALIVE answer must cost ZERO extra walks (the hot path is where the win is)
159 ps_refresh()
160 let c0: i64 = ps_builds()
161 var z: i64 = 0
162 while z < GT_QUERIES { ps_alive_or_direct("nx_proc_snapshot_gate" as *u8); z = z + 1 }
163 let c1: i64 = ps_builds()
164 bad = 0
165 if c1 != c0 { bad = 1 }
166 fails = fails + gt_bite(bad, "T11-alive-is-free" as *u8, "the ALIVE path rebuilt the snapshot -- the O(P) win is lost on the common case" as *u8)
167
168 // T12 -- ASYMMETRY, the safety half: a NEGATIVE must never be served from an AGED snapshot. Age the
169 // snapshot deliberately, then ask about an absent name: the answer must come from a rebuild.
170 ps_refresh()
171 let d0: i64 = ps_builds()
172 sys_sleep_ms(400) // now older than PS_CONFIRM_AGE_MS (250)
173 ps_alive_or_direct("zzz_no_such_daemon_zzz_9174" as *u8)
174 let d1: i64 = ps_builds()
175 bad = 0
176 if d1 <= d0 { bad = 1 }
177 fails = fails + gt_bite(bad, "T12-negative-is-confirmed" as *u8, "a NOT-ALIVE verdict was returned from a STALE snapshot -- could double-spawn a just-started daemon" as *u8)
178
179 // T13 -- and the confirmation is SHARED: many negatives in one window must not each rebuild
180 ps_refresh()
181 let e0: i64 = ps_builds()
182 var y: i64 = 0
183 while y < GT_QUERIES { ps_alive_or_direct("zzz_no_such_daemon_zzz_9174" as *u8); y = y + 1 }
184 let e1: i64 = ps_builds()
185 bad = 0
186 if e1 - e0 > 1 { bad = 1 }
187 fails = fails + gt_bite(bad, "T13-confirm-is-shared" as *u8, "each negative forced its OWN rebuild -- back to O(S x P) whenever a daemon is down" as *u8)
188 gt_puts(" rebuilds_for_" as *u8); gt_putn(GT_QUERIES); gt_puts("_negatives=" as *u8); gt_putn(e1 - e0); gt_puts("\n" as *u8)
189
190 gt_puts("nx_proc_snapshot_gate: fails=" as *u8); gt_putn(fails)
191 gt_puts(" procs=" as *u8); gt_putn(ps_count())
192 gt_puts(" blob_bytes=" as *u8); gt_putn(ps_blob_len())
193 gt_puts("\n" as *u8)
194 if fails > 0 { sys_exit(1); return 1 }
195 gt_puts("GATE GREEN 13/13\n" as *u8)
196 sys_exit(0)
197 return 0
198}