code wiki / (root) / nx_gate_verdict.nx

nx_gate_verdict.nx source

↩ module page · 155 lines · 6854 B

1// nx_gate_verdict.nx -- THE canonical gate-AUTHORING verdict lib (D001 first rung, 2026-07-18). 2// The debt: 2555 gate organs each hand-roll puts/num/pass/ttl/PASS-FAIL/verdict -- zero DRY. 3// This is the ONE copy gates import instead. Sibling of nx_gate_green.nx (which JUDGES a gate's 4// output from outside; this lib EMITS it from inside). Contract emitted: 5// " <check-name>: PASS\n" | " <check-name>: FAIL\n" per check 6// "\nNX-<GATE-NAME> passed <p>/<t> verdict=GREEN (<note>)\n" | " verdict=RED\n" 7// -- the exact shape nx_gate_green / nx_autograde already judge (anchor "verdict=", pat "GREEN"). 8// Usage: 9// let ctr: *i64 = gv_ctr() // [0]=pass [1]=ttl 10// gv_head("my gate -- what it proves") 11// gv_check("T1 the thing holds", t1_ok, ctr) // t1_ok: 1 pass, else fail 12// ... 13// let rc: i64 = gv_verdict("MY-GATE", ctr, "green note") // prints summary; 0 GREEN / 1 RED 14// sys_exit(rc) 15// license_tier: ORIGINAL No hw writes (Rule 26). 16import "nx_syscalls.nx" 17 18const GV_NL: i64 = 10 19const GV_CTR_BYTES: i64 = 16 20const GV_NUM_SCRATCH: i64 = 28 21const GV_ZERO: i64 = 48 22const GV_B10: i64 = 10 23 24func gv_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 25func gv_num(v: i64) -> i64 { 26 let b: *u8 = sys_mmap(GV_NUM_SCRATCH) 27 let t: *u8 = sys_mmap(GV_NUM_SCRATCH) 28 var m: i64 = v 29 if m < 0 { m = 0 - m; sys_write(1, "-" as *u8, 1) } 30 var k: i64 = 0 31 if m == 0 { t[0] = GV_ZERO as u8; k = 1 } 32 while m > 0 { t[k] = (GV_ZERO + (m % GV_B10)) as u8; m = m / GV_B10; k = k + 1 } 33 var i: i64 = 0 34 while i < k { b[i] = t[k-1-i]; i = i + 1 } 35 sys_write(1, b, k) 36 sys_munmap(b, GV_NUM_SCRATCH) 37 sys_munmap(t, GV_NUM_SCRATCH) 38 return 0 39} 40func gv_ctr() -> *i64 { 41 let c: *i64 = sys_mmap(GV_CTR_BYTES) as *i64 42 c[0] = 0 43 c[1] = 0 44 return c 45} 46func gv_head(title: *u8) -> i64 { gv_puts(title); gv_puts("\n\n" as *u8); return 0 } 47// one check: prints " <name>: PASS|FAIL", bumps counters, returns cond 48func gv_check(name: *u8, cond: i64, ctr: *i64) -> i64 { 49 ctr[1] = ctr[1] + 1 50 gv_puts(" " as *u8) 51 gv_puts(name) 52 gv_puts(": " as *u8) 53 if cond == 1 { ctr[0] = ctr[0] + 1; gv_puts("PASS\n" as *u8) } else { gv_puts("FAIL\n" as *u8) } 54 return cond 55} 56// ---- HOISTED FROM THE NAS COPY 2026-07-31 (ws=gate-dry-d001). THE BASE CLASS HAD FORKED: the NAS tree 57// carried gv_bite/gv_cat/gv_catn/gv_journal and this tree carried only the original six, so a gate written 58// against one tree would not compile on the other -- and, worse, an identical migration bought DIFFERENT 59// capability depending on where it happened. Converging the ANCESTOR is the fix; every descendant gains 60// these without being touched, including the ones not written yet. That is the whole point of a base class. 61// 62// BITE-PROVEN cell: the non-vacuity law made structural. A detector counts ONLY if it FIRES on the crafted 63// bad input AND stays SILENT on the crafted good one. A cell green before the defect exists is VACUOUS and 64// proves nothing (the gates-green-on-garbage class). Prints the sub-verdict so vacuity is SEEN, not counted. 65func gv_bite(name: *u8, bad: i64, good: i64, ctr: *i64) -> i64 { 66 var ok: i64 = 0 67 if bad == 1 { if good == 0 { ok = 1 } } 68 ctr[1] = ctr[1] + 1 69 gv_puts(" " as *u8) 70 gv_puts(name) 71 if ok == 1 { ctr[0] = ctr[0] + 1; gv_puts(": BITE-PROVEN (fires on bad, silent on good)\n" as *u8) } 72 if ok == 0 { 73 gv_puts(": FAIL " as *u8) 74 if bad != 1 { gv_puts("[VACUOUS: did not fire on the bad input]" as *u8) } 75 if good != 0 { gv_puts("[FALSE-POSITIVE: fired on the good input]" as *u8) } 76 gv_puts("\n" as *u8) 77 } 78 return ok 79} 80 81const GV_MODE_644: i64 = 420 82const GV_LINE: i64 = 512 83const GV_TAB: i64 = 9 84const GV_SLASH: i64 = 47 85const GV_MINUS: i64 = 45 86 87func gv_cat(d: *u8, o: i64, s: *u8) -> i64 { var i: i64 = 0; var p: i64 = o; while s[i] != (0 as u8) { d[p] = s[i]; p = p + 1; i = i + 1 } return p } 88func gv_catn(d: *u8, o: i64, v: i64) -> i64 { 89 let t: *u8 = sys_mmap(GV_NUM_SCRATCH) 90 var m: i64 = v 91 var p: i64 = o 92 if m < 0 { d[p] = GV_MINUS as u8; p = p + 1; m = 0 - m } 93 var k: i64 = 0 94 if m == 0 { t[0] = GV_ZERO as u8; k = 1 } 95 while m > 0 { t[k] = (GV_ZERO + (m % GV_B10)) as u8; m = m / GV_B10; k = k + 1 } 96 var i: i64 = 0 97 while i < k { d[p] = t[k-1-i]; p = p + 1; i = i + 1 } 98 sys_munmap(t, GV_NUM_SCRATCH) 99 return p 100} 101 102// FAIL-SOFT outcome journal: every gate that emits a verdict self-records ONE actlog-grammar frame, so 103// the HARNESS class finally has evidence at all -- flake and EROSION (a banked GREEN later going RED) 104// become derivable, and the frames are minable for free. A write failure NEVER touches the verdict: 105// no permission, no journal, no problem. Append-only, single line, conflict-free (O_APPEND). 106// Deliberately self-contained (no new imports): organs define their own sj_*/cat helpers, so importing a 107// json lib here would collide across hundreds of consumers. 108func gv_journal(name: *u8, passed: i64, total: i64, green: i64) -> i64 { 109 let fd: i64 = sys_openat_append("knowledge/status/harness.jrnl" as *u8, GV_MODE_644) 110 if fd < 0 { return 0 } 111 let ln: *u8 = sys_mmap(GV_LINE) 112 var o: i64 = gv_catn(ln, 0, sys_now_realtime_sec()) 113 ln[o] = GV_TAB as u8; o = o + 1 114 o = gv_cat(ln, o, "harness" as *u8) 115 ln[o] = GV_TAB as u8; o = o + 1 116 o = gv_cat(ln, o, name) 117 ln[o] = GV_TAB as u8; o = o + 1 118 o = gv_cat(ln, o, "run" as *u8) 119 ln[o] = GV_TAB as u8; o = o + 1 120 if green == 1 { o = gv_cat(ln, o, "GREEN" as *u8) } else { o = gv_cat(ln, o, "RED" as *u8) } 121 ln[o] = GV_TAB as u8; o = o + 1 122 o = gv_catn(ln, o, passed) 123 ln[o] = GV_SLASH as u8; o = o + 1 124 o = gv_catn(ln, o, total) 125 ln[o] = GV_NL as u8; o = o + 1 126 sys_write(fd, ln, o) 127 sys_close(fd) 128 sys_munmap(ln, GV_LINE) 129 return 0 130} 131 132// summary + verdict; returns exit code (0 GREEN / 1 RED). Caller sys_exit(rc). 133func gv_verdict(name: *u8, ctr: *i64, note: *u8) -> i64 { 134 gv_puts("\nNX-" as *u8) 135 gv_puts(name) 136 gv_puts(" passed " as *u8) 137 gv_num(ctr[0]) 138 gv_puts("/" as *u8) 139 gv_num(ctr[1]) 140 if ctr[0] == ctr[1] { 141 if ctr[1] > 0 { 142 gv_puts(" verdict=GREEN (" as *u8) 143 gv_puts(note) 144 gv_puts(")\n" as *u8) 145 // The journal write is a FILE side-effect only -- stdout, the PASS/FAIL vector and the 146 // verdict line are byte-unchanged, so every migration already proven judge-equivalent 147 // stays valid. Every inheriting gate now records its own outcome without being touched. 148 gv_journal(name, ctr[0], ctr[1], 1) 149 return 0 150 } 151 } 152 gv_puts(" verdict=RED\n" as *u8) 153 gv_journal(name, ctr[0], ctr[1], 0) 154 return 1 155}