nx_planepeek_gate.nx source
↩ module page · 272 lines · 16087 B
1// nx_planepeek_gate.nx -- THE REFEREE FOR nx_planepeek's FALSE-ABSENCE FIX (debt 1787282525).
2//
3// WHAT IS UNDER TEST. v1 of nx_planepeek printed one word -- MISS -- for five distinguishable
4// conditions, and that word is a NEGATIVE ASSERTION about a plane. It was quoted as proof of
5// absence in a build-refusal message and nearly produced a filed defect against a healthy lane.
6// The fix gives every condition its own word and its own exit code, and prints the coverage each
7// verdict was computed from. THIS GATE PROVES THE SEPARATION IS REAL, IN BOTH DIRECTIONS.
8//
9// WHY IT IS END-TO-END. The defect is in what the ORGAN PRINTS AND EXITS WITH, not in a pure
10// function, so the only honest subject is the built ELF. It is forked with tr_run_capture (the one
11// proven subprocess primitive) and judged on exit code AND emitted bytes.
12//
13// ★A GREEN THAT NEVER HAD A CORRESPONDING RED IS UNVERIFIED, so the decisive teeth are gv_bite
14// pairs: the same organ must FIRE on the broken fixture and stay SILENT on the healthy one.
15// Two tests that each isolate one signal do not prove discrimination between them.
16// ★A READER THAT MISSES EVERYTHING WOULD PASS EVERY ABSENCE TEST -- hence the POSITIVE CONTROL
17// (tooth 2/3): a key that IS present must be found, with its bytes. Without it, an organ that
18// returned MISS unconditionally would score full marks on this gate.
19// ★ASSERT THE FIXTURE REACHED THE CONDITION BEFORE ASSERTING THE OUTCOME: tooth 1 refuses to
20// believe any verdict until the subject has actually run and reported scanning segments>0.
21//
22// FIXTURES ARE ASSEMBLED AT RUNTIME under /tmp/<gate>/ (never the production knowledge/store tree:
23// a gate sharing a fixture with a production beat reports on the FIXTURE, not the code) and the
24// setup is IDEMPOTENT -- every artifact is unlinked before it is written, because a gate that is
25// not idempotent reports on its first run and lies about every run after.
26// license_tier: ORIGINAL Read-only outside /tmp. No hw writes (Rule 26).
27import "nx_gate_verdict.nx"
28import "nx_seg_store.nx"
29import "nx_tool_run.nx"
30import "nx_syscalls.nx"
31
32// 0755 -- the fixture directory must be traversable by the forked subject, which runs as the same
33// user; this is the mode sys_mkdir callers across the estate use for /tmp scratch roots.
34const PG_DIRMODE: i64 = 493
35// Capture buffer for one subject run. Fixture planes declare 2 segments and the organ's longest
36// answer is a headline + one coverage line + one name per unreadable segment, i.e. hundreds of
37// bytes. 65536 is ~2 orders of magnitude above that, and tooth `neg-control-capture-not-truncated`
38// asserts the cap was never reached -- A CAP REACHED IN SILENCE BECOMES A MEASUREMENT NOBODY KNOWS
39// IS PARTIAL.
40const PG_OUTCAP: i64 = 65536
41// Record kinds in a .docs segment (nx_seg_store: ss_scan_seglist reads kind, ss_get treats 2 as a
42// delete marker). Named here so the fixture states what it is building.
43const PG_KIND_PUT: i64 = 1
44const PG_KIND_TOMB: i64 = 2
45// The subject's exit contract, mirrored so a drift between organ and referee is a compile-visible
46// disagreement rather than a silent one.
47const PG_EX_HIT: i64 = 0
48const PG_EX_MISS: i64 = 1
49const PG_EX_UNPROVEN: i64 = 3
50const PG_EX_NOPLANE: i64 = 4
51const PG_EX_TOMBSTONED: i64 = 5
52const PG_EX_NOTAKEY: i64 = 6
53
54const PG_PATHCAP: i64 = 512
55// The SAME column separator the organ names PK_TAB. Writing a bare 9 here while the organ carries a
56// named const is the two-copies-of-one-literal defect: change the separator in one place and the
57// fixture silently stops exercising the NOT-A-KEY path while still passing every other tooth.
58const PG_TAB: i64 = 9
59// Fixture segment ids. Fixed (not ss_next_segid) so the idempotent teardown above can name every
60// artifact it must remove; seg B commits AFTER seg A, which is what makes its tombstone win.
61const PG_SEG_A: i64 = 1
62const PG_SEG_B: i64 = 2
63
64func pg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
65
66// gv_check takes a 1/0 condition, so comparisons are lifted to predicates rather than open-coded at
67// each call site -- one spelling of "equal", not seventeen.
68func pg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 }
69func pg_lt(a: i64, b: i64) -> i64 { if a < b { return 1 } return 0 }
70func pg_gt0(a: i64) -> i64 { if a > 0 { return 1 } return 0 }
71func pg_not(a: i64) -> i64 { if a == 0 { return 1 } return 0 }
72
73// substring search over a captured, NON-terminated byte buffer
74func pg_has(hay: *u8, haylen: i64, needle: *u8) -> i64 {
75 let nl: i64 = pg_len(needle)
76 if nl == 0 { return 1 }
77 if nl > haylen { return 0 }
78 var i: i64 = 0
79 let last: i64 = haylen - nl
80 while i <= last {
81 var t: i64 = 0
82 var eq: i64 = 1
83 while t < nl { if hay[i + t] != needle[t] { eq = 0; t = nl } else { t = t + 1 } }
84 if eq == 1 { return 1 }
85 i = i + 1
86 }
87 return 0
88}
89
90func pg_path(dir: *u8, name: *u8, out: *u8) -> i64 {
91 var o: i64 = ss_cat(out, 0, dir)
92 o = ss_cat(out, o, name)
93 out[o] = 0 as u8
94 return o
95}
96
97func pg_exists(path: *u8) -> i64 {
98 let fd: i64 = sys_openat_rd(path)
99 if fd < 0 { return 0 }
100 sys_close(fd)
101 return 1
102}
103
104func pg_rm(dir: *u8, name: *u8) -> i64 {
105 let p: *u8 = sys_mmap(PG_PATHCAP)
106 pg_path(dir, name, p)
107 sys_unlinkat(p)
108 sys_munmap(p, PG_PATHCAP)
109 return 0
110}
111
112// ---- FIXTURE CONSTRUCTION, through the PRODUCTION writer -----------------------------------
113// The fixture is built with ss_begin/ss_add/ss_commit, the same path nx_store_put commits through,
114// so it cannot drift from the real on-disk format the way a hand-assembled byte blob would.
115// Row values are TAB-joined N-column rows exactly as the N-col planes carry them, which is what
116// makes the NOT-A-KEY tooth a test of DERIVED behaviour and not of a hardcoded convention.
117func pg_row(out: *u8, c0: *u8, c1: *u8, c2: *u8) -> i64 {
118 var o: i64 = ss_cat(out, 0, c0)
119 out[o] = PG_TAB as u8; o = o + 1
120 o = ss_cat(out, o, c1)
121 out[o] = PG_TAB as u8; o = o + 1
122 o = ss_cat(out, o, c2)
123 return o
124}
125
126// seg-1: q:0, q:1, q:2 as live puts. seg-2: q:2 as a TOMBSTONE (later segment wins).
127func pg_build_plane(prefix: *u8) -> i64 {
128 let w: *i64 = ss_begin()
129 let row: *u8 = sys_mmap(PG_PATHCAP)
130 var rl: i64 = pg_row(row, "sitecheck" as *u8, "60" as *u8, "nx_clock_sitecheck.elf" as *u8)
131 ss_add(w, PG_KIND_PUT, "q:0" as *u8, row, rl)
132 rl = pg_row(row, "segguard" as *u8, "600" as *u8, "nx_segsweep.elf" as *u8)
133 ss_add(w, PG_KIND_PUT, "q:1" as *u8, row, rl)
134 rl = pg_row(row, "doomed" as *u8, "1" as *u8, "nx_nothing.elf" as *u8)
135 ss_add(w, PG_KIND_PUT, "q:2" as *u8, row, rl)
136 if ss_commit(prefix, w, PG_SEG_A) < 0 { return 0 - 1 }
137 let w2: *i64 = ss_begin()
138 let z: *u8 = sys_mmap(16)
139 ss_add(w2, PG_KIND_TOMB, "q:2" as *u8, z, 0)
140 if ss_commit(prefix, w2, PG_SEG_B) < 0 { return 0 - 2 }
141 return 0
142}
143
144// ---- SUBJECT RESOLUTION --------------------------------------------------------------------
145// Resolve the built artifact by STAT, never by assumption -- a gate that forks a path it did not
146// confirm reports the absence of a binary as a failure of the code.
147func pg_try_subject(cand: *u8, out: *u8) -> i64 {
148 if pg_exists(cand) == 0 { return 0 }
149 let o: i64 = ss_cat(out, 0, cand)
150 out[o] = 0 as u8
151 return 1
152}
153func pg_subject(out: *u8) -> i64 {
154 if pg_try_subject("_build/nx_planepeek.sov.elf" as *u8, out) == 1 { return 1 }
155 if pg_try_subject("_offc/nx_planepeek.elf" as *u8, out) == 1 { return 1 }
156 if pg_try_subject("nx_planepeek.elf" as *u8, out) == 1 { return 1 }
157 return 0
158}
159
160// one subject run: returns the exit code, fills out/outlen
161func pg_run(subj: *u8, prefix: *u8, key: *u8, out: *u8, outlen: *i64) -> i64 {
162 let av: *i64 = sys_mmap(64) as *i64
163 av[0] = subj as i64
164 av[1] = prefix as i64
165 av[2] = key as i64
166 av[3] = 0
167 return tr_run_capture(subj, av, out, PG_OUTCAP, outlen)
168}
169
170func main(argc: i64, argv: *i64) -> i64 {
171 gv_head("NX-PLANEPEEK-GATE -- MISS must mean PROVEN ABSENT and nothing else (debt 1787282525)" as *u8)
172 let ctr: *i64 = gv_ctr()
173
174 let dir: *u8 = "/tmp/nx_planepeek_gate/" as *u8
175 sys_mkdir("/tmp/nx_planepeek_gate" as *u8, PG_DIRMODE)
176
177 // ---- IDEMPOTENT SETUP: remove every artifact a previous run could have left behind.
178 pg_rm(dir, "good-manifest.txt" as *u8); pg_rm(dir, "good-manifest-archive.txt" as *u8)
179 pg_rm(dir, "good-seg-1.docs" as *u8); pg_rm(dir, "good-seg-2.docs" as *u8)
180 pg_rm(dir, "broken-manifest.txt" as *u8); pg_rm(dir, "broken-manifest-archive.txt" as *u8)
181 pg_rm(dir, "broken-seg-1.docs" as *u8); pg_rm(dir, "broken-seg-2.docs" as *u8)
182 pg_rm(dir, "nosuch-manifest.txt" as *u8)
183
184 let goodp: *u8 = sys_mmap(PG_PATHCAP); pg_path(dir, "good-" as *u8, goodp)
185 let brokp: *u8 = sys_mmap(PG_PATHCAP); pg_path(dir, "broken-" as *u8, brokp)
186 let nonep: *u8 = sys_mmap(PG_PATHCAP); pg_path(dir, "nosuch-" as *u8, nonep)
187
188 let bg: i64 = pg_build_plane(goodp)
189 let bb: i64 = pg_build_plane(brokp)
190 // THE BREAKAGE: a segment still NAMED in manifest.txt but removed from disk. This is the exact
191 // shape ss_readall/ss_scan_seglist swallow in silence (sz=-1 -> the record loop never runs).
192 pg_rm(dir, "broken-seg-2.docs" as *u8)
193
194 let subj: *u8 = sys_mmap(PG_PATHCAP)
195 let havesubj: i64 = pg_subject(subj)
196
197 // ---- PRECONDITIONS. gv_need, so "I could not look" is never reported as "I looked and it failed".
198 // ★ASSERT THE FIXTURE REACHED THE CONDITION BEFORE ASSERTING THE OUTCOME. A fixture the defect
199 // cannot fail is not a test: if the "broken" plane's segment were still on disk, every tooth in
200 // section 4 would pass for the wrong reason.
201 let seg2: *u8 = sys_mmap(PG_PATHCAP); pg_path(dir, "broken-seg-2.docs" as *u8, seg2)
202 let man2: *u8 = sys_mmap(PG_PATHCAP); pg_path(dir, "broken-manifest.txt" as *u8, man2)
203 if gv_need("subject-elf-present" as *u8, havesubj, ctr) == 0 { return gv_verdict("PLANEPEEK-GATE" as *u8, ctr, "subject not built" as *u8) }
204 if gv_need("fixture-good-plane-committed" as *u8, pg_eq(bg, 0), ctr) == 0 { return gv_verdict("PLANEPEEK-GATE" as *u8, ctr, "fixture build failed" as *u8) }
205 if gv_need("fixture-broken-plane-committed" as *u8, pg_eq(bb, 0), ctr) == 0 { return gv_verdict("PLANEPEEK-GATE" as *u8, ctr, "fixture build failed" as *u8) }
206 if gv_need("fixture-broken-segment-REMOVED-from-disk" as *u8, pg_not(pg_exists(seg2)), ctr) == 0 { return gv_verdict("PLANEPEEK-GATE" as *u8, ctr, "fixture not in the intended state" as *u8) }
207 if gv_need("fixture-broken-segment-STILL-NAMED-in-manifest" as *u8, pg_exists(man2), ctr) == 0 { return gv_verdict("PLANEPEEK-GATE" as *u8, ctr, "fixture not in the intended state" as *u8) }
208
209 let ob: *u8 = sys_mmap(PG_OUTCAP)
210 let ol: *i64 = sys_mmap(16) as *i64
211
212 // ============ 1. ANTI-VACUITY: the subject ran and examined something ============
213 let rc_hit: i64 = pg_run(subj, goodp, "q:0" as *u8, ob, ol)
214 gv_check("anti-vacuity-subject-emitted-bytes" as *u8, pg_gt0(ol[0]), ctr)
215 gv_check("anti-vacuity-subject-scanned-segments-not-zero" as *u8, pg_has(ob, ol[0], "segments_declared=2" as *u8), ctr)
216 gv_check("neg-control-capture-not-truncated" as *u8, pg_lt(ol[0], PG_OUTCAP), ctr)
217
218 // ============ 2. POSITIVE CONTROL: a key that IS there must be FOUND ============
219 // Without this tooth an organ that answered MISS unconditionally would pass every other test.
220 gv_check("positive-control-present-key-exit-0-HIT" as *u8, pg_eq(rc_hit, PG_EX_HIT), ctr)
221 gv_check("positive-control-present-key-says-HIT" as *u8, pg_has(ob, ol[0], "HIT" as *u8), ctr)
222 gv_check("positive-control-present-key-returns-its-VALUE" as *u8, pg_has(ob, ol[0], "sitecheck" as *u8), ctr)
223
224 // ============ 3. A GENUINELY ABSENT KEY: MISS, and it says it scanned everything ============
225 let rc_miss: i64 = pg_run(subj, goodp, "q:99" as *u8, ob, ol)
226 gv_check("absent-key-exit-1-MISS" as *u8, pg_eq(rc_miss, PG_EX_MISS), ctr)
227 gv_check("absent-key-claims-PROVEN-ABSENT" as *u8, pg_has(ob, ol[0], "PROVEN ABSENT" as *u8), ctr)
228 gv_check("absent-key-announces-full-coverage" as *u8, pg_has(ob, ol[0], "unreadable=0" as *u8), ctr)
229 gv_check("coverage-partition-sums-declared-eq-read-plus-unreadable" as *u8, pg_has(ob, ol[0], "read=2 unreadable=0 sum=2" as *u8), ctr)
230
231 // ============ 4. THE CORE FIX: an unreadable plane is UNPROVEN, NOT MISS ============
232 let rc_unp: i64 = pg_run(subj, brokp, "q:99" as *u8, ob, ol)
233 let said_unproven_bad: i64 = pg_has(ob, ol[0], "UNPROVEN" as *u8)
234 let said_proven_bad: i64 = pg_has(ob, ol[0], "PROVEN ABSENT" as *u8)
235 gv_check("neg-control-unreadable-plane-exit-3-UNPROVEN" as *u8, pg_eq(rc_unp, PG_EX_UNPROVEN), ctr)
236 gv_check("neg-control-unreadable-plane-does-NOT-claim-absence" as *u8, pg_not(said_proven_bad), ctr)
237 gv_check("neg-control-unreadable-plane-names-its-offender" as *u8, pg_has(ob, ol[0], "UNREADABLE-SEGMENT" as *u8), ctr)
238 gv_check("neg-control-unreadable-plane-counts-it" as *u8, pg_has(ob, ol[0], "unreadable=1" as *u8), ctr)
239
240 // BITE: both signals present at once. The SAME organ, the SAME key, two fixtures.
241 let rc_g: i64 = pg_run(subj, goodp, "q:99" as *u8, ob, ol)
242 let said_unproven_good: i64 = pg_has(ob, ol[0], "UNPROVEN" as *u8)
243 gv_bite("bite-UNPROVEN-fires-on-unreadable-plane-and-not-on-healthy-one" as *u8, said_unproven_bad, said_unproven_good, ctr)
244
245 // ============ 5. A PLANE THAT DOES NOT EXIST IS NOT AN ABSENT KEY ============
246 let rc_np: i64 = pg_run(subj, nonep, "q:0" as *u8, ob, ol)
247 let np_said: i64 = pg_has(ob, ol[0], "NO-SUCH-PLANE" as *u8)
248 gv_check("neg-control-missing-plane-exit-4-NO-SUCH-PLANE" as *u8, pg_eq(rc_np, PG_EX_NOPLANE), ctr)
249 gv_check("neg-control-missing-plane-does-NOT-say-MISS" as *u8, pg_not(pg_has(ob, ol[0], "PROVEN ABSENT" as *u8)), ctr)
250 let rc_g2: i64 = pg_run(subj, goodp, "q:99" as *u8, ob, ol)
251 gv_bite("bite-NO-SUCH-PLANE-fires-on-absent-prefix-and-not-on-real-one" as *u8, np_said, pg_has(ob, ol[0], "NO-SUCH-PLANE" as *u8), ctr)
252
253 // ============ 6. CONTRACT MISUSE IS REFUSED BY NAME, NEVER GUESSED AT ============
254 // `segguard` is COLUMN 0 of the row at q:1. v1 answered MISS -- a confident false absence.
255 let rc_nak: i64 = pg_run(subj, goodp, "segguard" as *u8, ob, ol)
256 let nak_said: i64 = pg_has(ob, ol[0], "NOT-A-KEY" as *u8)
257 gv_check("neg-control-column-value-exit-6-NOT-A-KEY" as *u8, pg_eq(rc_nak, PG_EX_NOTAKEY), ctr)
258 gv_check("neg-control-column-value-does-NOT-claim-absence" as *u8, pg_not(pg_has(ob, ol[0], "PROVEN ABSENT" as *u8)), ctr)
259 gv_check("NOT-A-KEY-names-the-REAL-key-of-that-row" as *u8, pg_has(ob, ol[0], "q:1" as *u8), ctr)
260 let rc_g3: i64 = pg_run(subj, goodp, "q:99" as *u8, ob, ol)
261 gv_bite("bite-NOT-A-KEY-fires-on-a-column-value-and-not-on-a-real-absent-key" as *u8, nak_said, pg_has(ob, ol[0], "NOT-A-KEY" as *u8), ctr)
262
263 // ============ 7. A TOMBSTONE IS A PRESENT KEY, NOT AN ABSENT ONE ============
264 let rc_tb: i64 = pg_run(subj, goodp, "q:2" as *u8, ob, ol)
265 let tb_said: i64 = pg_has(ob, ol[0], "TOMBSTONED" as *u8)
266 gv_check("tombstoned-key-exit-5-TOMBSTONED" as *u8, pg_eq(rc_tb, PG_EX_TOMBSTONED), ctr)
267 gv_check("tombstoned-key-does-NOT-claim-absence" as *u8, pg_not(pg_has(ob, ol[0], "PROVEN ABSENT" as *u8)), ctr)
268 let rc_g4: i64 = pg_run(subj, goodp, "q:99" as *u8, ob, ol)
269 gv_bite("bite-TOMBSTONED-fires-on-a-deleted-key-and-not-on-an-absent-one" as *u8, tb_said, pg_has(ob, ol[0], "TOMBSTONED" as *u8), ctr)
270
271 return gv_verdict("PLANEPEEK-GATE" as *u8, ctr, "MISS is emitted only for a resolved plane whose every declared segment was read" as *u8)
272}