nx_ivvbeat.nx source
↩ module page · 456 lines · 22743 B
1// nx_ivvbeat.nx -- the IV+V beat: re-runs the estate's own verification gates and reports DRIFT.
2//
3// WHY THIS EXISTS. The ivvreg- plane holds four rows of desired independent-verification state and,
4// measured 2026-08-07 across buildroot/*.nx (51,707 files), _offc/*.sh (12,433) and knowledge/registry
5// (297) -- every scan marker-confirmed coverage_complete=1 -- NOTHING HAS EVER READ IT. The consumer was
6// specified in data and never built. So this is not a port of anything; the plane IS the spec.
7// (STAR)A DATA PLANE WITH NO CONSUMER IS A SPECIFICATION NOBODY IMPLEMENTED -- IT LOOKS LIKE STATE AND
8// BEHAVES LIKE A TODO. The rows even include a purpose-built negative control, so whoever wrote them knew
9// exactly what the beat had to do.
10//
11// WHAT IT ANSWERS: "do the estate's own gates still pass?" That is the same hole board item 7 named for
12// published surfaces -- nothing was checking -- one level down: nothing checks the CHECKERS.
13//
14// SAFETY. Every exec and every delete is decided by nx_ivvguard, whose predicates are proven 23/23 by
15// nx_ivvguard_gate INCLUDING all four live rows. That gate previously passed 12/12 while the predicate was
16// WRONG, because every fixture in it was fabricated; the four real rows were what exposed it.
17//
18// THE WIPE IS DELIBERATELY NOT IMPLEMENTED IN v1, and each row says so out loud. The wipe column asks for
19// a prefix-glob delete; the verification value -- do the gates still pass -- is fully available without it.
20// (STAR)WHEN THE RISKY HALF OF A CAPABILITY IS NOT REQUIRED FOR ITS VALUE, SHIP THE OTHER HALF FIRST AND
21// MEASURE WHETHER THE RISKY HALF WAS EVER NEEDED. If gates pass unwiped, the delete is unnecessary; if they
22// fail, that is evidence the wipe is load-bearing, and its predicates are already proven and waiting.
23// A row whose wipe spec is UNSAFE is refused outright rather than run dirty -- the author asked for cleaning
24// this beat will not do, so its result would not mean what the row intended.
25//
26// v1 IS REPORT-ONLY BY CONSTRUCTION: it files no debt. A detector's first live run must be readable before
27// it is allowed to write, or its own defects arrive as a pile of authored records.
28// license_tier: ORIGINAL No hw writes (Rule 26). Deletes nothing.
29import "nx_syscalls.nx"
30import "nx_store_seed_lib.nx"
31import "nx_guarded_run.nx"
32import "nx_ivvguard.nx"
33
34const IVB_PLANECAP: i64 = 1048576
35const IVB_FIELDCAP: i64 = 4096
36const IVB_SCRATCH: i64 = 8192
37const IVB_DEADLINE_MS: i64 = 180000
38const IVB_MAXARGS: i64 = 32
39const IVB_TAB: i64 = 9
40const IVB_NL: i64 = 10
41const IVB_SP: i64 = 32
42const IVB_RC_NOTFOUND: i64 = 127
43// Coverage floor in permil. Data-driven threshold (rule 11) rather than a literal buried in the check.
44// Set to 900: a verification sweep that misses more than a tenth of the estate is not a sweep.
45const IVB_COVERAGE_FLOOR_PERMIL: i64 = 900
46// TOTAL WALL-CLOCK BUDGET FOR ONE SWEEP. With 123 rows and a 180s per-gate deadline the worst case is
47// 6.1 hours against a 7200s clock interval -- the exact "runtime exceeds period on a serial dispatcher"
48// defect diagnosed in nx_clock_sched earlier today. A per-item deadline bounds ONE item; it says nothing
49// about the sweep.
50// (STAR)A PER-ITEM TIMEOUT IS NOT A SWEEP TIMEOUT -- N BOUNDED ITEMS ARE STILL UNBOUNDED IN AGGREGATE.
51// On exhaustion the sweep STOPS and reports how far it got, because a truncated sweep that keeps going
52// past its window starves the next one and a truncated sweep that stays silent overstates its coverage.
53// MATCHED PAIR WITH THE DISPATCHER (2026-08-07). The budget above was sized against the 7200s clock
54// INTERVAL -- correct reasoning about not starving the next run -- but NOT against the dispatcher's
55// CLK_DISPATCH_DEADLINE_MS, which SIGKILLs any job at 1800000 ms. Both numbers were derived
56// independently and landed on the SAME 1800000, so the sweep's self-limit and the clock's kill fire at
57// the same instant. The clock's timer starts FIRST (fork+exec+startup happen inside it), so the clock
58// wins the race and the honest [TRUNCATED] summary this organ exists to print NEVER GETS WRITTEN --
59// the sweep dies silently and the beat reports only a dead exit code.
60// A SELF-LIMIT EQUAL TO THE EXTERNAL KILL IS NOT A SELF-LIMIT; IT IS A COIN FLIP THE OUTER TIMER WINS.
61// Derived from the dispatcher's deadline minus a margin, the same shape as
62// TEA_EXEC_TIMEOUT_SYNC_MS = TEA_EDGE_WINDOW_MS - 1000 in nx_tool_exec_allow.nx, so the two can no
63// longer drift into each other. The margin is for finishing the current row's teardown and writing the
64// summary + the auto-filed drift rows, which is the whole point of stopping early.
65// MUST TRACK nx_clock_sched.nx CLK_DISPATCH_DEADLINE_MS. Mirrored rather than imported because that
66// file is the DISPATCHER and importing it here would drag the scheduler into a verification organ.
67// TRACKS nx_clock_sched.nx CLK_DISPATCH_DEADLINE_MS, LOWERED 1800000 -> 900000 ON 2026-08-14 when that
68// deadline was halved to window/2 (it had been set to the FULL 1800s window, so it could never bind).
69// UPDATED IN THE SAME CHANGE ON PURPOSE: leaving this at 1800000 would have made IVB_SWEEP_BUDGET_MS
70// (deadline - margin = 1680000ms) LARGER than the clock's kill at 900000ms, so the clock would win the
71// race every time and the honest [TRUNCATED] summary this organ exists to print would never be written
72// -- the exact failure the note above describes, re-created by updating one half of a mirrored pair.
73// THIS IS THE DUPLICATE-RULER HAZARD THE COMMENT ABOVE WARNS ABOUT, AND IT BIT WITHIN ONE EDIT.
74const IVB_CLOCK_DEADLINE_MS: i64 = 900000
75const IVB_SWEEP_MARGIN_MS: i64 = 120000
76const IVB_SWEEP_BUDGET_MS: i64 = IVB_CLOCK_DEADLINE_MS - IVB_SWEEP_MARGIN_MS
77const IVB_MODE_644: i64 = 0x1a4
78
79func ivb_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
80
81func ivb_putn(v: i64) -> i64 {
82 if v == 0 { sys_write(1, "0" as *u8, 1); return 0 }
83 var mv: i64 = v
84 if mv < 0 { sys_write(1, "-" as *u8, 1); mv = 0 - mv }
85 let t: *u8 = sys_mmap(32)
86 var k: i64 = 0
87 while mv > 0 { t[k] = (0x30 + (mv - (mv/10)*10)) as u8; mv = mv/10; k = k + 1 }
88 while k > 0 { k = k - 1; sys_write(1, (((t as i64)+k) as *u8), 1) }
89 return 0
90}
91
92func ivb_streq(a: *u8, b: *u8) -> i64 {
93 var i: i64 = 0
94 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 }
95 if b[i] != (0 as u8) { return 0 }
96 return 1
97}
98
99// Copy tab-delimited field `idx` out of buf[s,e) into dst. Returns its length, or -1 if absent.
100// A row missing any field is MALFORMED and is reported, never guessed at.
101func ivb_field(buf: *u8, s: i64, e: i64, idx: i64, dst: *u8, dcap: i64) -> i64 {
102 var f: i64 = 0
103 var i: i64 = s
104 var st: i64 = s
105 while i <= e {
106 var isend: i64 = 0
107 if i == e { isend = 1 }
108 if i < e { if buf[i] == (IVB_TAB as u8) { isend = 1 } }
109 if isend == 1 {
110 if f == idx {
111 var ln: i64 = i - st
112 if ln > dcap - 1 { ln = dcap - 1 }
113 var k: i64 = 0
114 while k < ln { dst[k] = buf[st+k]; k = k + 1 }
115 dst[ln] = (0 as u8)
116 return ln
117 }
118 f = f + 1
119 st = i + 1
120 }
121 i = i + 1
122 }
123 dst[0] = (0 as u8)
124 return 0 - 1
125}
126
127// Split the command field into a NULL-terminated argv over `scratch`. There is NO shell here, so this is
128// plain whitespace tokenisation of data the allowlist has already vetted -- quoting is not a concern
129// because nothing re-parses the result.
130func ivb_build_argv(cmd: *u8, scratch: *u8, slot: *i64) -> i64 {
131 var i: i64 = 0
132 var argc: i64 = 0
133 var w: i64 = 0
134 var inword: i64 = 0
135 while cmd[i] != (0 as u8) {
136 if cmd[i] == (IVB_SP as u8) {
137 if inword == 1 { scratch[w] = (0 as u8); w = w + 1; inword = 0 }
138 }
139 if cmd[i] != (IVB_SP as u8) {
140 if inword == 0 {
141 if argc >= IVB_MAXARGS - 1 { slot[argc] = 0; return argc }
142 slot[argc] = ((scratch as i64) + w)
143 argc = argc + 1
144 inword = 1
145 }
146 scratch[w] = cmd[i]; w = w + 1
147 }
148 i = i + 1
149 }
150 if inword == 1 { scratch[w] = (0 as u8); w = w + 1 }
151 slot[argc] = 0
152 return argc
153}
154
155func ivb_outpath(idx: i64, dst: *u8) -> i64 {
156 let p: *u8 = "/tmp/ivvbeat_out_" as *u8
157 var k: i64 = 0
158 while p[k] != (0 as u8) { dst[k] = p[k]; k = k + 1 }
159 var v: i64 = idx
160 if v == 0 { dst[k] = (0x30 as u8); k = k + 1 }
161 let t: *u8 = sys_mmap(32)
162 var j: i64 = 0
163 while v > 0 { t[j] = (0x30 + (v - (v/10)*10)) as u8; v = v/10; j = j + 1 }
164 while j > 0 { j = j - 1; dst[k] = t[j]; k = k + 1 }
165 dst[k] = (0 as u8)
166 return k
167}
168
169func main() -> i64 {
170 ivb_puts("=== nx_ivvbeat: independent verification + validation sweep (v1, REPORT-ONLY, deletes nothing) ===\n")
171
172 let plane: *u8 = sys_mmap(IVB_PLANECAP)
173 let flags: *i64 = sys_mmap(64) as *i64
174 // THE PREFIX IS A PATH, NOT A NAME. ssc_sig_of concatenates prefix + "manifest.txt" verbatim, so the
175 // caller supplies the whole relative path INCLUDING the trailing dash. Passing the bare plane name
176 // silently reads ZERO rows -- there is no error, because "no manifest" is indistinguishable from
177 // "empty plane" to the loader. Verified against a control: knowledge/store/debt- reads 3,621 rows
178 // while bare debt- reads 0. This organ shipped with the bare form, and its FIRST live run reported
179 // rows=0 verdict=RED rather than a 0/0 pass -- which is the only reason the mistake was visible.
180 // (STAR)A LOADER THAT CANNOT DISTINGUISH "I FOUND NOTHING" FROM "THERE IS NOTHING" REPORTS A
181 // CONFIGURATION ERROR AS AN EMPTY WORLD -- SO THE CALLER MUST REFUSE TO CALL AN EMPTY WORLD GREEN.
182 let n: i64 = sts_load_honest("knowledge/store/ivvreg-" as *u8, plane, IVB_PLANECAP, flags)
183
184 ivb_puts("plane ivvreg- declared_qn="); ivb_putn(flags[0])
185 ivb_puts(" rows_loaded="); ivb_putn(flags[1])
186 ivb_puts(" rows_BEYOND_declared="); ivb_putn(flags[2])
187 ivb_puts(" bytes="); ivb_putn(n)
188 ivb_puts("\n")
189
190 // A plane whose q:n under-declares its contents silently truncates every reader. That exact class
191 // produced a false "surfsentinel dead 12.5 days" alarm in this estate, so it is reported LOUDLY and
192 // makes the sweep RED even if every row it DID reach passes.
193 // (STAR)A SWEEP OVER A TRUNCATED INPUT IS NOT A CLEAN SWEEP, IT IS AN UNMEASURED ONE.
194 if flags[2] > 0 {
195 ivb_puts(" [WARN] the plane holds rows PAST its declared count -- this sweep did NOT see them; verdict forced RED\n")
196 }
197
198 let envp: *i64 = sys_mmap(64) as *i64
199 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64
200 envp[1] = 0
201
202 let idb: *u8 = sys_mmap(IVB_FIELDCAP)
203 let cmdb: *u8 = sys_mmap(IVB_FIELDCAP)
204 let preb: *u8 = sys_mmap(IVB_FIELDCAP)
205 let mkb: *u8 = sys_mmap(IVB_FIELDCAP)
206 let scr: *u8 = sys_mmap(IVB_SCRATCH)
207 let opth: *u8 = sys_mmap(256)
208 let slot: *i64 = sys_mmap(8 * (IVB_MAXARGS + 2)) as *i64
209 let olen: *i64 = sys_mmap(16) as *i64
210 let gres: *i64 = sys_mmap(64) as *i64
211
212 var rows: i64 = 0
213 var ran: i64 = 0
214 var greens: i64 = 0
215 var drift: i64 = 0
216 var refused: i64 = 0
217 var missing: i64 = 0
218 var timeouts: i64 = 0
219 var malformed: i64 = 0
220 var negseen: i64 = 0
221 var negfail: i64 = 0
222
223 let sweep_t0: i64 = sys_now_ms()
224 var budget_hit: i64 = 0
225 var s: i64 = 0
226 var i: i64 = 0
227 while i <= n {
228 var eol: i64 = 0
229 if i == n { eol = 1 }
230 if i < n { if plane[i] == (IVB_NL as u8) { eol = 1 } }
231 if eol == 1 {
232 if i > s {
233 rows = rows + 1
234 let lid: i64 = ivb_field(plane, s, i, 0, idb, IVB_FIELDCAP)
235 let lcm: i64 = ivb_field(plane, s, i, 1, cmdb, IVB_FIELDCAP)
236 let lpr: i64 = ivb_field(plane, s, i, 2, preb, IVB_FIELDCAP)
237 let lmk: i64 = ivb_field(plane, s, i, 3, mkb, IVB_FIELDCAP)
238
239 ivb_puts("-- row "); ivb_putn(rows); ivb_puts(" id="); ivb_puts(idb); ivb_puts("\n")
240
241 var ok: i64 = 1
242 if lid < 0 { ok = 0 }
243 if lcm < 0 { ok = 0 }
244 if lpr < 0 { ok = 0 }
245 if lmk < 0 { ok = 0 }
246 if ok == 0 {
247 malformed = malformed + 1
248 ivb_puts(" [MALFORMED] expected id/cmd/wipe/marker -- row REFUSED, nothing executed\n")
249 }
250
251 if ok == 1 {
252 // WIPE DECISION FIRST: a row whose cleaning we refuse must not be run dirty.
253 var wipeok: i64 = 0
254 if ivv_wipe_none(preb) == 1 {
255 wipeok = 1
256 ivb_puts(" wipe=none (sentinel)\n")
257 }
258 if wipeok == 0 {
259 if ivv_wipe_allowed(preb) == 1 {
260 wipeok = 1
261 ivb_puts(" wipe=PERMITTED-BUT-NOT-PERFORMED (v1 deletes nothing) pre="); ivb_puts(preb); ivb_puts("\n")
262 }
263 }
264 if wipeok == 0 {
265 refused = refused + 1
266 ivb_puts(" [REFUSED] wipe spec is OUTSIDE /tmp or contains traversal: "); ivb_puts(preb)
267 ivb_puts(" -- row NOT executed\n")
268 ok = 0
269 }
270 }
271
272 if ok == 1 {
273 if ivv_cmd_allowed(cmdb) == 0 {
274 refused = refused + 1
275 ivb_puts(" [REFUSED] command is not on the allowlist: "); ivb_puts(cmdb); ivb_puts("\n")
276 ok = 0
277 }
278 }
279
280 if ok == 1 {
281 if sys_now_ms() - sweep_t0 >= IVB_SWEEP_BUDGET_MS {
282 budget_hit = budget_hit + 1
283 ivb_puts(" [BUDGET] sweep wall-clock budget exhausted -- this row and every row after it was NOT verified\n")
284 ok = 0
285 }
286 }
287
288 if ok == 1 {
289 let argc: i64 = ivb_build_argv(cmdb, scr, slot)
290 ivb_outpath(rows, opth)
291 let ofd: i64 = sys_openat_wr(opth, IVB_MODE_644)
292 let t0: i64 = sys_now_ms()
293 let rc: i64 = nx_guarded_run((slot[0] as *u8), slot, envp, IVB_DEADLINE_MS, ofd, ofd)
294 let dt: i64 = sys_now_ms() - t0
295 sys_close(ofd)
296 ran = ran + 1
297
298 olen[0] = 0
299 let cap_out: *u8 = sys_read_file(opth, olen)
300 let on: i64 = olen[0]
301
302 ivb_puts(" argc="); ivb_putn(argc)
303 ivb_puts(" rc="); ivb_putn(rc)
304 ivb_puts(" ms="); ivb_putn(dt)
305 ivb_puts(" out_bytes="); ivb_putn(on)
306 ivb_puts("\n")
307
308 // v2: the tooth floor. res[0]=observed passed res[1]=observed total res[2]=declared floor.
309 var green: i64 = 0
310 if on > 0 { green = ivv_is_green2(rc, cap_out, on, mkb, gres) }
311 if gres[1] >= 0 {
312 ivb_puts(" teeth observed="); ivb_putn(gres[1])
313 ivb_puts(" floor="); ivb_putn(gres[2])
314 if gres[1] > gres[2] { ivb_puts(" (GREW since the row was written -- an improvement, not drift)") }
315 if gres[1] < gres[2] { ivb_puts(" (SHRANK -- TOOTH LOSS, the class an anchor-only check cannot see)") }
316 ivb_puts("\n")
317 }
318
319 let isneg: i64 = ivb_streq(idb, "ivv-negcontrol" as *u8)
320
321 // 127 is the child's own exit after a failed execve: NOT-FOUND, a distinct fault from
322 // a gate that ran and disagreed. Conflating them would blame the gate for a path bug.
323 if rc == IVB_RC_NOTFOUND {
324 missing = missing + 1
325 ivb_puts(" [MISSING] execve failed (127) -- the binary named by the plane is not reachable from this cwd\n")
326 }
327 if rc == NX_GR_TIMEOUT {
328 timeouts = timeouts + 1
329 ivb_puts(" [TIMEOUT] exceeded the deadline and was SIGKILLed -- a wedged gate is drift, not a pass\n")
330 }
331
332 if isneg == 1 {
333 negseen = negseen + 1
334 // THE PLANTED LIE. This row must NEVER go green. If it does, the detector is broken
335 // and every other GREEN on this sweep is worthless.
336 // (STAR)A PLANTED LIE THAT STOPS FAILING HAS NOT BEEN FIXED, IT HAS STOPPED BEING READ.
337 if green == 1 {
338 negfail = negfail + 1
339 ivb_puts(" [DETECTOR FAILURE] the negative control went GREEN -- this sweep proves NOTHING\n")
340 }
341 if green == 0 {
342 ivb_puts(" [NEGCONTROL OK] the planted lie failed, as it must -- the detector has teeth this run\n")
343 }
344 }
345 if isneg == 0 {
346 if green == 1 {
347 greens = greens + 1
348 ivb_puts(" [GREEN] rc=0 AND marker present: "); ivb_puts(mkb); ivb_puts("\n")
349 }
350 if green == 0 {
351 if rc != IVB_RC_NOTFOUND {
352 drift = drift + 1
353 ivb_puts(" [DRIFT rc="); ivb_putn(rc); ivb_puts("] "); ivb_puts("marker NOT confirmed. rc=0 means UNPROVEN (exited clean, cannot prove its teeth ran); non-zero means the GATE FAILED. These need different work: "); ivb_puts(mkb); ivb_puts("\n")
354 }
355 }
356 }
357 }
358 }
359 s = i + 1
360 }
361 i = i + 1
362 }
363
364 // ================= COVERAGE IS PART OF THE VERDICT =================
365 // The first version of this beat reported "rows=4" and nothing else. Four of WHAT? The estate holds
366 // 364 verdict logs, 218 anchored, 121 resolving to a runnable organ -- so four rows was 3% coverage
367 // presented with the same confidence as a full sweep. Nothing in the output could have told anyone.
368 // (STAR)A VERIFIER THAT DOES NOT REPORT ITS OWN COVERAGE IS INDISTINGUISHABLE FROM ONE THAT CHECKS A
369 // SINGLE THING -- THE DENOMINATOR IS NOT CONTEXT, IT IS PART OF THE RESULT.
370 // The denominator is read from the census proposal, which is derived from the estate itself, so it
371 // cannot silently agree with the roster the way a hand-typed number would.
372 var registrable: i64 = 0
373 let plen: *i64 = sys_mmap(16) as *i64
374 plen[0] = 0
375 let prop: *u8 = sys_read_file("knowledge/status/ivvcensus_proposed.tsv" as *u8, plen)
376 let pn: i64 = plen[0]
377 if pn > 0 {
378 var pi: i64 = 0
379 var atbol: i64 = 1
380 while pi + 4 <= pn {
381 if atbol == 1 {
382 if prop[pi] == (82 as u8) { if prop[pi+1] == (79 as u8) { if prop[pi+2] == (87 as u8) { if prop[pi+3] == (9 as u8) { registrable = registrable + 1 } } } }
383 }
384 if prop[pi] == (IVB_NL as u8) { atbol = 1 } else { atbol = 0 }
385 pi = pi + 1
386 }
387 }
388 ivb_puts("\n-- coverage --\n")
389 ivb_puts("registered_rows="); ivb_putn(rows)
390 ivb_puts(" registrable_in_estate="); ivb_putn(registrable)
391 if registrable > 0 {
392 ivb_puts(" coverage_permil="); ivb_putn((rows * 1000) / registrable)
393 }
394 if registrable == 0 {
395 ivb_puts(" [WARN] no census proposal on disk -- the denominator is UNMEASURED, so this sweep cannot claim coverage at all")
396 }
397 ivb_puts("\n")
398
399 ivb_puts("\n-- summary --\n")
400 ivb_puts("rows="); ivb_putn(rows)
401 ivb_puts(" ran="); ivb_putn(ran)
402 ivb_puts(" green="); ivb_putn(greens)
403 ivb_puts(" drift="); ivb_putn(drift)
404 ivb_puts(" refused="); ivb_putn(refused)
405 ivb_puts(" missing="); ivb_putn(missing)
406 ivb_puts(" timeout="); ivb_putn(timeouts)
407 ivb_puts(" malformed="); ivb_putn(malformed)
408 ivb_puts(" negcontrols="); ivb_putn(negseen)
409 ivb_puts(" negfail="); ivb_putn(negfail)
410 ivb_puts("\n")
411
412 // A SWEEP WITH NO NEGATIVE CONTROL IS UNFALSIFIABLE. If the plane ever loses that row, this beat must
413 // NOT report GREEN -- an all-pass result from an untested detector is exactly the fake-green it exists
414 // to catch, one level up.
415 var bad: i64 = 0
416 if drift > 0 { bad = 1 }
417 if refused > 0 { bad = 1 }
418 if malformed > 0 { bad = 1 }
419 if missing > 0 { bad = 1 }
420 if timeouts > 0 { bad = 1 }
421 if negfail > 0 { bad = 1 }
422
423 // Under-coverage is a RED condition, not a footnote. A sweep that verifies 3% of the estate and prints
424 // GREEN is a stronger claim than the evidence supports, and it is exactly how a sample gets mistaken
425 // for a roster. This stays RED until the census-derived roster is actually seeded.
426 if registrable > 0 {
427 if (rows * 1000) / registrable < IVB_COVERAGE_FLOOR_PERMIL {
428 bad = 1
429 ivb_puts("[UNDER-COVERED] this sweep verified "); ivb_putn(rows)
430 ivb_puts(" of "); ivb_putn(registrable)
431 ivb_puts(" registrable gates -- below the floor, so GREEN would overstate the evidence\n")
432 }
433 }
434 if budget_hit > 0 {
435 bad = 1
436 ivb_puts("[TRUNCATED] "); ivb_putn(budget_hit)
437 ivb_puts(" rows went unverified because the sweep budget ran out -- a partial sweep is not a pass\n")
438 }
439 if registrable == 0 {
440 bad = 1
441 ivb_puts("[NO DENOMINATOR] no census proposal found -- coverage is unmeasured and an unmeasured sweep cannot be GREEN\n")
442 }
443 if negseen == 0 {
444 bad = 1
445 ivb_puts("[NO NEGATIVE CONTROL] the plane carries no planted lie this run -- an unfalsifiable sweep cannot be GREEN\n")
446 }
447
448 if bad == 0 {
449 ivb_puts("NX-IVVBEAT passed "); ivb_putn(greens); ivb_puts("/"); ivb_putn(greens)
450 ivb_puts(" verdict=GREEN (every registered gate re-ran and confirmed its marker; the planted lie still failed)\n")
451 sys_exit(0)
452 return 0
453 }
454 ivb_puts("NX-IVVBEAT verdict=RED (see rows above)\n")
455 sys_exit(1)
456 return 1
457}