nx_nishios_kernel_gate.nx source

1// nx_nishios_kernel_gate.nx -- the TRANSCRIPT gate for the composed NishiOS kernel boot. 2// 3// WHY THIS EXISTS (a measured instrument defect, not a hypothetical): the BOOTSOV runner decides 4// its verdict from `halted && halt_code==0` ALONE -- it never reads the serial transcript. Proven 5// 2026-07-31: a kernel image deliberately tampered so the Sv39 walk faults printed 6// "...TICK TX" instead of "...PAGE USER OK" and BOOTSOV still returned verdict=GREEN exit=0. 7// A runner that returns GREEN on a broken boot is not a check. This gate reads what the kernel 8// actually SAID and compares it to the table-computed golden transcript. 9// 10// TEETH (each independently able to fail; the two NEG teeth are the non-vacuity proof): 11// T1 image present and not the 72-byte banner it replaced 12// T2 boots to a clean finisher halt 13// T3 transcript is EXACTLY the golden transcript 14// T4 every phase marker present (banner/trap/sched/timer/paging/user) 15// T5 NEG-comparator: the comparator must REJECT a mutated golden (proves it can say no) 16// T6 NEG-subject: a corrupted kernel image must NOT reproduce the golden transcript 17// T7 step count is far above the 17-step banner baseline (the boot does real work) 18// Sovereign: the emulator IS the runtime. license_tier: ORIGINAL 19// Boot-and-capture comes from the SHARED primitive, not a private copy: this gate, the census 20// and nx_kernel_adoption must agree byte-for-byte about what "booting the image" means, and three 21// hand-maintained copies is three chances for them to drift apart silently. 22import "nx_bootcap.nx" 23import "nx_gate_verdict.nx" 24 25const NKG_BIN: *u8 = "runtime/_hdl_build/_boot_nishi_virt.bin" 26const NKG_GOLD: *u8 = "runtime/_hdl_build/_boot_nishi_virt.bin.gold" 27const NKG_BIN_ALT: *u8 = "_boot_nishi_virt.bin" 28const NKG_GOLD_ALT: *u8 = "runtime/_hdl_build/_boot_nishi_virt.bin.gold" 29const NKG_LOG: *u8 = "knowledge/status/boot_stub.log" 30 31const NKG_MEM_BASE: i64 = 0x80000000 32const NKG_MEM_SIZE: i64 = 65536 33const NKG_TX_CAP: i64 = 4096 34const NKG_MAX_STEPS: i64 = 100000 35const NKG_BANNER_BYTES: i64 = 72 36const NKG_BANNER_STEPS: i64 = 17 37 38func nkg_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 39func nkg_fp(fd: i64, s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(fd,s,n); return 0 } 40func nkg_fn(fd: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(fd,"-" as *u8,1)}; let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48;k=1}; while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1}; var i: i64=0; while i<k{bb[i]=t[k-1-i];i=i+1}; sys_write(fd,bb,k); return 0 } 41 42// Boot one image on a FRESH machine. Thin wrapper over the shared bootcap primitive so this 43// gate cannot drift from the census/adoption rulers about what a boot is. 44// res[0]=halted res[1]=halt_code res[2]=steps res[3]=tx_count 45func nkg_run(img: *u8, ilen: i64, tx_buf: *u8, res: *i64) -> i64 { 46 bootcap_run(img, ilen, tx_buf, NKG_TX_CAP, res) 47 return 0 48} 49 50func nkg_eq(a: *u8, an: i64, b: *u8, bn: i64) -> i64 { 51 if an != bn { return 0 } 52 var i: i64 = 0 53 while i < an { if a[i] != b[i] { return 0 } i = i + 1 } 54 return 1 55} 56// substring search: 1 if `needle` (NUL-terminated) occurs in hay[0..hn) 57func nkg_has(hay: *u8, hn: i64, needle: *u8) -> i64 { 58 var nn: i64 = 0 59 while needle[nn] != (0 as u8) { nn = nn + 1 } 60 if nn == 0 { return 1 } 61 if nn > hn { return 0 } 62 var i: i64 = 0 63 while i <= hn - nn { 64 var k: i64 = 0 65 var ok: i64 = 1 66 while k < nn { if hay[i+k] != needle[k] { ok = 0; k = nn } else { k = k + 1 } } 67 if ok == 1 { return 1 } 68 i = i + 1 69 } 70 return 0 71} 72 73// ---- D001 MIGRATION 2026-08-06 -- IDIOM H: TOOTH HELPER + fails==0 GUARD --------------------- 74// Same family as nx_suitebench_gate. nx_gate_dry_apply rightly refuses to map the GUARD here (its own 75// text: the fails==0 family -- a direct operand map would INVERT the gate green->red). The correct 76// migration converts the TOOTH HELPER: every nkg_tooth call already carries (name, condition), which 77// is gv_check's signature, so the pass/total counter is BUILT from the teeth that already exist. 78// pass[]/fail[] are still maintained so every other reader of them keeps working unchanged. 79static nkg_ctr: *i64 80 81func nkg_tooth(name: *u8, ok: i64, pass: *i64, fail: *i64) -> i64 { 82 if (nkg_ctr as i64) == 0 { nkg_ctr = gv_ctr() } 83 gv_check(name, ok, nkg_ctr) 84 if ok == 1 { pass[0] = pass[0] + 1 } 85 if ok != 1 { fail[0] = fail[0] + 1 } 86 return 0 87} 88 89// argv[1] = image path, argv[2] = golden path. Defaults match the buildroot layout; the LIVE NAS 90// keeps the image at the SERVING ROOT and the golden under runtime/_hdl_build/ (the "two roots, one 91// name" split), so the gate must be told where to look rather than assume one tree. 92func main(argc: i64, argv: *i64) -> i64 { 93 var binp: *u8 = NKG_BIN 94 var goldp: *u8 = NKG_GOLD 95 if argc >= 2 { binp = argv[1] as *u8 } 96 if argc >= 3 { goldp = argv[2] as *u8 } 97 var pass: *i64 = sys_mmap(16) as *i64 98 var fail: *i64 = sys_mmap(16) as *i64 99 pass[0] = 0 100 fail[0] = 0 101 nkg_p("=== nx_nishios_kernel_gate -- the composed NishiOS boot, checked by TRANSCRIPT ===\n" as *u8) 102 nkg_p(" image=" as *u8); nkg_p(binp); nkg_p(" golden=" as *u8); nkg_p(goldp); nkg_p("\n" as *u8) 103 104 // RESOLVE, THEN SAY WHICH. The buildroot keeps the image under runtime/_hdl_build/ while the 105 // live serving root keeps it at ./ -- one name, two roots. A gate that silently picked the 106 // wrong one would measure an artifact nobody boots, so try both and PRINT the resolved path. 107 let lenp: *i64 = sys_mmap(16) as *i64 108 var img: *u8 = sys_read_file(binp, lenp) 109 var ilen: i64 = lenp[0] 110 if ilen <= 0 { 111 binp = NKG_BIN_ALT 112 img = sys_read_file(binp, lenp) 113 ilen = lenp[0] 114 } 115 let glenp: *i64 = sys_mmap(16) as *i64 116 var gold: *u8 = sys_read_file(goldp, glenp) 117 var glen: i64 = glenp[0] 118 if glen <= 0 { 119 goldp = NKG_GOLD_ALT 120 gold = sys_read_file(goldp, glenp) 121 glen = glenp[0] 122 } 123 nkg_p(" resolved image=" as *u8); nkg_p(binp); nkg_p(" golden=" as *u8); nkg_p(goldp); nkg_p("\n" as *u8) 124 125 if ilen <= 0 { nkg_p("NISHIOSKERNELGATE verdict=RED reason=image-missing\n" as *u8); return 1 } 126 if glen <= 0 { nkg_p("NISHIOSKERNELGATE verdict=RED reason=golden-missing\n" as *u8); return 1 } 127 128 // T1 -- the chokepoint image is no longer the banner it replaced 129 var t1: i64 = 0 130 if ilen > NKG_BANNER_BYTES { t1 = 1 } 131 nkg_tooth("T1 image is a composed kernel, not the 72-byte banner" as *u8, t1, pass, fail) 132 133 let tx: *u8 = sys_mmap(NKG_TX_CAP) 134 let res: *i64 = sys_mmap(64) as *i64 135 nkg_run(img, ilen, tx, res) 136 let halted: i64 = res[0] 137 let hcode: i64 = res[1] 138 let steps: i64 = res[2] 139 let txn: i64 = res[3] 140 141 // T2 -- clean finisher halt 142 var t2: i64 = 0 143 if halted == 1 { if hcode == 0 { t2 = 1 } } 144 nkg_tooth("T2 booted to a clean finisher halt" as *u8, t2, pass, fail) 145 146 // T3 -- the transcript is EXACTLY the golden (what BOOTSOV never checks) 147 let t3: i64 = nkg_eq(tx, txn, gold, glen) 148 nkg_tooth("T3 serial transcript == golden transcript" as *u8, t3, pass, fail) 149 150 // T4 -- every phase left its marker 151 var t4: i64 = 1 152 if nkg_has(tx, txn, "NISHI" as *u8) != 1 { t4 = 0 } 153 if nkg_has(tx, txn, "TRAP" as *u8) != 1 { t4 = 0 } 154 if nkg_has(tx, txn, "ABABABABABAB" as *u8) != 1 { t4 = 0 } 155 if nkg_has(tx, txn, "SCHED" as *u8) != 1 { t4 = 0 } 156 if nkg_has(tx, txn, "TICK" as *u8) != 1 { t4 = 0 } 157 if nkg_has(tx, txn, "PQPQPQ" as *u8) != 1 { t4 = 0 } 158 if nkg_has(tx, txn, "PREEMPT" as *u8) != 1 { t4 = 0 } 159 if nkg_has(tx, txn, "BLK" as *u8) != 1 { t4 = 0 } 160 if nkg_has(tx, txn, "NET" as *u8) != 1 { t4 = 0 } 161 if nkg_has(tx, txn, "HEAP" as *u8) != 1 { t4 = 0 } 162 if nkg_has(tx, txn, "PAGE" as *u8) != 1 { t4 = 0 } 163 if nkg_has(tx, txn, "USER" as *u8) != 1 { t4 = 0 } 164 nkg_tooth("T4 all ten phase markers (banner/trap/sched/timer/preempt/blk/net/heap/paging/user)" as *u8, t4, pass, fail) 165 166 // T4b -- no phase-failure marker may appear 167 var t4b: i64 = 1 168 if nkg_has(tx, txn, "PGX" as *u8) == 1 { t4b = 0 } 169 if nkg_has(tx, txn, "TX" as *u8) == 1 { t4b = 0 } 170 if nkg_has(tx, txn, "UX" as *u8) == 1 { t4b = 0 } 171 if nkg_has(tx, txn, "BX" as *u8) == 1 { t4b = 0 } 172 if nkg_has(tx, txn, "NF" as *u8) == 1 { t4b = 0 } 173 if nkg_has(tx, txn, "HX" as *u8) == 1 { t4b = 0 } 174 nkg_tooth("T4b no phase-failure marker (PGX/TX/UX/BX/NF/HX) in the transcript" as *u8, t4b, pass, fail) 175 176 // T5 -- NEG-comparator: a mutated golden MUST be rejected, else T3 proves nothing 177 let mg: *u8 = sys_mmap(NKG_TX_CAP) 178 var c: i64 = 0 179 while c < glen { mg[c] = gold[c]; c = c + 1 } 180 mg[0] = (mg[0] + 1) as u8 181 var t5: i64 = 0 182 if nkg_eq(tx, txn, mg, glen) == 0 { t5 = 1 } 183 nkg_tooth("T5 NEG comparator rejects a mutated golden (the check can say no)" as *u8, t5, pass, fail) 184 185 // T6 -- NEG-subject: a corrupted kernel must NOT reproduce the golden transcript 186 let bad: *u8 = sys_mmap(NKG_MEM_SIZE) 187 var d: i64 = 0 188 while d < ilen { bad[d] = img[d]; d = d + 1 } 189 bad[0] = 0 as u8 190 bad[1] = 0 as u8 191 bad[2] = 0 as u8 192 bad[3] = 0 as u8 193 let tx2: *u8 = sys_mmap(NKG_TX_CAP) 194 let res2: *i64 = sys_mmap(64) as *i64 195 nkg_run(bad, ilen, tx2, res2) 196 var t6: i64 = 0 197 if nkg_eq(tx2, res2[3], gold, glen) == 0 { t6 = 1 } 198 nkg_tooth("T6 NEG subject: a corrupted kernel does not reproduce the golden" as *u8, t6, pass, fail) 199 200 // T7 -- the boot does real work, far above the banner baseline 201 var t7: i64 = 0 202 if steps > NKG_BANNER_STEPS * 5 { t7 = 1 } 203 nkg_tooth("T7 step count far exceeds the 17-step banner baseline" as *u8, t7, pass, fail) 204 205 nkg_p(" transcript=[" as *u8); sys_write(1, tx, txn); nkg_p("]\n" as *u8) 206 nkg_p(" bytes=" as *u8); nkg_fn(1, ilen) 207 nkg_p(" steps=" as *u8); nkg_fn(1, steps) 208 nkg_p(" serial_bytes=" as *u8); nkg_fn(1, txn); nkg_p("\n" as *u8) 209 210 let total: i64 = pass[0] + fail[0] 211 // SINGLE verdict anchor on stdout -- gv_verdict replaces the hand-rolled line and is GREEN iff 212 // pass==total, the same condition as the old fail[0]==0. The log row below keeps its own verdict 213 // token because the rollup reads that FILE, not stdout. 214 if (nkg_ctr as i64) == 0 { nkg_ctr = gv_ctr() } 215 let rc__g: i64 = gv_verdict("NISHIOSKERNELGATE" as *u8, nkg_ctr, "composed NishiOS kernel boot judged by its TRANSCRIPT, not merely by halted+halt_code -- the defect this gate exists to catch" as *u8) 216 217 let lf: i64 = sys_openat_append(NKG_LOG, 420) 218 if lf >= 0 { 219 nkg_fp(lf, "NISHIOSKERNELGATE pass=" as *u8); nkg_fn(lf, pass[0]) 220 nkg_fp(lf, " of=" as *u8); nkg_fn(lf, total) 221 nkg_fp(lf, " bytes=" as *u8); nkg_fn(lf, ilen) 222 nkg_fp(lf, " steps=" as *u8); nkg_fn(lf, steps) 223 nkg_fp(lf, " transcript=" as *u8); sys_write(lf, tx, txn) 224 if fail[0] == 0 { nkg_fp(lf, " verdict=GREEN\n" as *u8) } else { nkg_fp(lf, " verdict=RED\n" as *u8) } 225 sys_close(lf) 226 } 227 return rc__g 228}