nx_gate_subjects_gate.nx source

1// nx_gate_subjects_gate.nx -- proves gv_subjects makes THE EMPTY-SET LAW structural. 2// 3// THE DEFECT IT EXISTS FOR: gv_check counts TEETH, never SUBJECTS. A gate with ten teeth over ZERO 4// files reports 10/10 GREEN and every consumer reads a pass. The estate had written that law 5// repeatedly and never built the mechanism, so it lived hand-rolled per-organ and was forgotten by 6// default. MEASURED the day gv_subjects was added: a ship harness skipped its work behind a load 7// guard, wrote no log, and EXITED 0 -- inconclusive reading as success. 8// 9// WHY SKIP AND NOT RED: a zero population is the ABSENCE OF EVIDENCE about the subject, not a failure 10// of it. gv_subjects therefore composes gv_need (ctr[2]) instead of inventing a fourth state, which 11// means it inherits the proven ordering -- a SKIP co-occurring with a real failure still escalates to 12// RED and can never amnesty it. T5 pins exactly that. 13import "nx_syscalls.nx" 14import "nx_gate_verdict.nx" 15 16const GS_SRCBUF: i64 = 65536 17const GS_SRC: *u8 = "runtime/nx_gate_verdict.nx" 18const GS_SRC_UP: *u8 = "buildroot/runtime/nx_gate_verdict.nx" 19 20func gs_read(path: *u8, buf: *u8) -> i64 { 21 let fd: i64 = sys_openat_rd(path) 22 if fd < 0 { return 0 } 23 let n: i64 = sys_read(fd, buf, GS_SRCBUF - 1) 24 sys_close(fd) 25 if n < 0 { return 0 } 26 buf[n] = 0 as u8 27 return n 28} 29func gs_find(buf: *u8, n: i64, needle: *u8) -> i64 { 30 var nl: i64 = 0 31 while needle[nl] != (0 as u8) { nl = nl + 1 } 32 if nl == 0 { return 0 } 33 var i: i64 = 0 34 while i + nl <= n { 35 var j: i64 = 0 36 var hit: i64 = 1 37 while j < nl { if buf[i + j] != needle[j] { hit = 0; j = nl } else { j = j + 1 } } 38 if hit == 1 { return 1 } 39 i = i + 1 40 } 41 return 0 42} 43 44func main() -> i64 { 45 let ctr: *i64 = gv_ctr() 46 gv_head("nx_gate_subjects_gate -- can a gate still report GREEN over an empty population?" as *u8) 47 48 // T1 a real population ADMITS and leaves the precondition counter untouched. 49 let c1: *i64 = gv_ctr() 50 let r1: i64 = gv_subjects("t1-population" as *u8, 42, c1) 51 var t1: i64 = 0 52 if r1 == 1 { if c1[2] == 0 { t1 = 1 } } 53 gv_check("T1 a non-empty population ADMITS and records no missing precondition" as *u8, t1, ctr) 54 55 // T2 THE REGRESSION CASE: zero subjects must REFUSE and must register as a missing precondition. 56 let c2: *i64 = gv_ctr() 57 let r2: i64 = gv_subjects("t2-empty" as *u8, 0, c2) 58 var t2: i64 = 0 59 if r2 == 0 { if c2[2] == 1 { t2 = 1 } } 60 gv_check("T2 the-regression-case: ZERO subjects REFUSES and registers a missing precondition" as *u8, t2, ctr) 61 62 // T3 boundary: 1 is a population, 0 is not. 63 let c3: *i64 = gv_ctr() 64 let c4: *i64 = gv_ctr() 65 var t3: i64 = 0 66 if gv_subjects("t3-one" as *u8, 1, c3) == 1 { if gv_subjects("t3-zero" as *u8, 0, c4) == 0 { t3 = 1 } } 67 gv_check("T3 boundary: n==1 ADMITS and n==0 REFUSES (the population test is >0, not >=0)" as *u8, t3, ctr) 68 69 // T4 neg-control fail-closed: a NEGATIVE count (unreadable population) must never admit. 70 let c5: *i64 = gv_ctr() 71 var t4: i64 = 0 72 if gv_subjects("t4-unreadable" as *u8, 0 - 1, c5) == 0 { if c5[2] == 1 { t4 = 1 } } 73 gv_check("T4 neg-control-fail-closed: a NEGATIVE (unreadable) population REFUSES, never admits" as *u8, t4, ctr) 74 75 // T5 ANTI-VACUITY -- the whole point. Build the exact counter state a passing gate over an empty 76 // population produces: EVERY tooth passed (ctr[0]==ctr[1]) AND a precondition is missing (ctr[2]>0). 77 // That is precisely the state gv_verdict maps to SKIP rather than GREEN. Without this tooth, T1-T4 78 // would all pass against a gv_subjects that recorded nothing anywhere the verdict could see it. 79 let c6: *i64 = gv_ctr() 80 gv_check(" (inner) a tooth that passes" as *u8, 1, c6) 81 gv_check(" (inner) another tooth that passes" as *u8, 1, c6) 82 gv_subjects("t5-empty-population" as *u8, 0, c6) 83 var t5: i64 = 0 84 if c6[0] == c6[1] { if c6[0] > 0 { if c6[2] > 0 { t5 = 1 } } } 85 gv_check("T5 anti-vacuity: all teeth passing PLUS an empty population yields the SKIP state, not GREEN" as *u8, t5, ctr) 86 87 // T6 SOURCE CONSISTENCY: tie this to the real base class. gv_subjects must exist there AND 88 // gv_verdict must still branch on the precondition counter, or T5's claim about the verdict is 89 // an assertion about a mirror instead of about the shipped code. 90 let buf: *u8 = sys_mmap(GS_SRCBUF) 91 var n: i64 = gs_read(GS_SRC, buf) 92 if n <= 0 { n = gs_read(GS_SRC_UP, buf) } 93 var srcok: i64 = 0 94 if n > 0 { srcok = 1 } 95 gv_need("nx_gate_verdict.nx source readable from this cwd" as *u8, srcok, ctr) 96 var t6: i64 = 0 97 if n > 0 { 98 var ok: i64 = 1 99 if gs_find(buf, n, "func gv_subjects" as *u8) == 0 { ok = 0 } 100 if gs_find(buf, n, "gv_need(name, present, ctr)" as *u8) == 0 { ok = 0 } 101 if gs_find(buf, n, "ctr[2]" as *u8) == 0 { ok = 0 } 102 t6 = ok 103 } 104 if srcok == 1 { gv_check("T6 the shipped base class carries gv_subjects and still routes it through the precondition counter" as *u8, t6, ctr) } 105 106 // T7 neg-control on the source scanner itself -- a string that must NOT be found. 107 var t7: i64 = 0 108 if n > 0 { if gs_find(buf, n, "zzz_not_in_gate_verdict_zzz" as *u8) == 0 { t7 = 1 } } 109 if srcok == 1 { gv_check("T7 neg-control-source-scanner-does-not-report-an-absent-string" as *u8, t7, ctr) } 110 111 return gv_verdict("GATE-SUBJECTS" as *u8, ctr, "an empty population is reported as absence of evidence (SKIP), never as a pass, and the base class is the one that does it" as *u8) 112}