code wiki / _hdl_build / nx_nishios_kernel_gate.nx

nx_nishios_kernel_gate.nx source

↩ module page · 215 lines · 10199 B

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" 23 24const NKG_BIN: *u8 = "runtime/_hdl_build/_boot_nishi_virt.bin" 25const NKG_GOLD: *u8 = "runtime/_hdl_build/_boot_nishi_virt.bin.gold" 26const NKG_BIN_ALT: *u8 = "_boot_nishi_virt.bin" 27const NKG_GOLD_ALT: *u8 = "runtime/_hdl_build/_boot_nishi_virt.bin.gold" 28const NKG_LOG: *u8 = "knowledge/status/boot_stub.log" 29 30const NKG_MEM_BASE: i64 = 0x80000000 31const NKG_MEM_SIZE: i64 = 65536 32const NKG_TX_CAP: i64 = 4096 33const NKG_MAX_STEPS: i64 = 100000 34const NKG_BANNER_BYTES: i64 = 72 35const NKG_BANNER_STEPS: i64 = 17 36 37func 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 } 38func 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 } 39func nkg_fn(fd: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m}; 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 } 40 41// Boot one image on a FRESH machine. Thin wrapper over the shared bootcap primitive so this 42// gate cannot drift from the census/adoption rulers about what a boot is. 43// res[0]=halted res[1]=halt_code res[2]=steps res[3]=tx_count 44func nkg_run(img: *u8, ilen: i64, tx_buf: *u8, res: *i64) -> i64 { 45 bootcap_run(img, ilen, tx_buf, NKG_TX_CAP, res) 46 return 0 47} 48 49func nkg_eq(a: *u8, an: i64, b: *u8, bn: i64) -> i64 { 50 if an != bn { return 0 } 51 var i: i64 = 0 52 while i < an { if a[i] != b[i] { return 0 } i = i + 1 } 53 return 1 54} 55// substring search: 1 if `needle` (NUL-terminated) occurs in hay[0..hn) 56func nkg_has(hay: *u8, hn: i64, needle: *u8) -> i64 { 57 var nn: i64 = 0 58 while needle[nn] != (0 as u8) { nn = nn + 1 } 59 if nn == 0 { return 1 } 60 if nn > hn { return 0 } 61 var i: i64 = 0 62 while i <= hn - nn { 63 var k: i64 = 0 64 var ok: i64 = 1 65 while k < nn { if hay[i+k] != needle[k] { ok = 0; k = nn } else { k = k + 1 } } 66 if ok == 1 { return 1 } 67 i = i + 1 68 } 69 return 0 70} 71 72func nkg_tooth(name: *u8, ok: i64, pass: *i64, fail: *i64) -> i64 { 73 if ok == 1 { nkg_p(" PASS " as *u8); pass[0] = pass[0] + 1 } else { nkg_p(" FAIL " as *u8); fail[0] = fail[0] + 1 } 74 nkg_p(name); nkg_p("\n" as *u8) 75 return 0 76} 77 78// argv[1] = image path, argv[2] = golden path. Defaults match the buildroot layout; the LIVE NAS 79// keeps the image at the SERVING ROOT and the golden under runtime/_hdl_build/ (the "two roots, one 80// name" split), so the gate must be told where to look rather than assume one tree. 81func main(argc: i64, argv: *i64) -> i64 { 82 var binp: *u8 = NKG_BIN 83 var goldp: *u8 = NKG_GOLD 84 if argc >= 2 { binp = argv[1] as *u8 } 85 if argc >= 3 { goldp = argv[2] as *u8 } 86 var pass: *i64 = sys_mmap(16) as *i64 87 var fail: *i64 = sys_mmap(16) as *i64 88 pass[0] = 0 89 fail[0] = 0 90 nkg_p("=== nx_nishios_kernel_gate -- the composed NishiOS boot, checked by TRANSCRIPT ===\n" as *u8) 91 nkg_p(" image=" as *u8); nkg_p(binp); nkg_p(" golden=" as *u8); nkg_p(goldp); nkg_p("\n" as *u8) 92 93 // RESOLVE, THEN SAY WHICH. The buildroot keeps the image under runtime/_hdl_build/ while the 94 // live serving root keeps it at ./ -- one name, two roots. A gate that silently picked the 95 // wrong one would measure an artifact nobody boots, so try both and PRINT the resolved path. 96 let lenp: *i64 = sys_mmap(16) as *i64 97 var img: *u8 = sys_read_file(binp, lenp) 98 var ilen: i64 = lenp[0] 99 if ilen <= 0 { 100 binp = NKG_BIN_ALT 101 img = sys_read_file(binp, lenp) 102 ilen = lenp[0] 103 } 104 let glenp: *i64 = sys_mmap(16) as *i64 105 var gold: *u8 = sys_read_file(goldp, glenp) 106 var glen: i64 = glenp[0] 107 if glen <= 0 { 108 goldp = NKG_GOLD_ALT 109 gold = sys_read_file(goldp, glenp) 110 glen = glenp[0] 111 } 112 nkg_p(" resolved image=" as *u8); nkg_p(binp); nkg_p(" golden=" as *u8); nkg_p(goldp); nkg_p("\n" as *u8) 113 114 if ilen <= 0 { nkg_p("NISHIOSKERNELGATE verdict=RED reason=image-missing\n" as *u8); return 1 } 115 if glen <= 0 { nkg_p("NISHIOSKERNELGATE verdict=RED reason=golden-missing\n" as *u8); return 1 } 116 117 // T1 -- the chokepoint image is no longer the banner it replaced 118 var t1: i64 = 0 119 if ilen > NKG_BANNER_BYTES { t1 = 1 } 120 nkg_tooth("T1 image is a composed kernel, not the 72-byte banner" as *u8, t1, pass, fail) 121 122 let tx: *u8 = sys_mmap(NKG_TX_CAP) 123 let res: *i64 = sys_mmap(64) as *i64 124 nkg_run(img, ilen, tx, res) 125 let halted: i64 = res[0] 126 let hcode: i64 = res[1] 127 let steps: i64 = res[2] 128 let txn: i64 = res[3] 129 130 // T2 -- clean finisher halt 131 var t2: i64 = 0 132 if halted == 1 { if hcode == 0 { t2 = 1 } } 133 nkg_tooth("T2 booted to a clean finisher halt" as *u8, t2, pass, fail) 134 135 // T3 -- the transcript is EXACTLY the golden (what BOOTSOV never checks) 136 let t3: i64 = nkg_eq(tx, txn, gold, glen) 137 nkg_tooth("T3 serial transcript == golden transcript" as *u8, t3, pass, fail) 138 139 // T4 -- every phase left its marker 140 var t4: i64 = 1 141 if nkg_has(tx, txn, "NISHI" as *u8) != 1 { t4 = 0 } 142 if nkg_has(tx, txn, "TRAP" as *u8) != 1 { t4 = 0 } 143 if nkg_has(tx, txn, "ABABABABABAB" as *u8) != 1 { t4 = 0 } 144 if nkg_has(tx, txn, "SCHED" as *u8) != 1 { t4 = 0 } 145 if nkg_has(tx, txn, "TICK" as *u8) != 1 { t4 = 0 } 146 if nkg_has(tx, txn, "PQPQPQ" as *u8) != 1 { t4 = 0 } 147 if nkg_has(tx, txn, "PREEMPT" as *u8) != 1 { t4 = 0 } 148 if nkg_has(tx, txn, "BLK" as *u8) != 1 { t4 = 0 } 149 if nkg_has(tx, txn, "NET" as *u8) != 1 { t4 = 0 } 150 if nkg_has(tx, txn, "HEAP" as *u8) != 1 { t4 = 0 } 151 if nkg_has(tx, txn, "PAGE" as *u8) != 1 { t4 = 0 } 152 if nkg_has(tx, txn, "USER" as *u8) != 1 { t4 = 0 } 153 nkg_tooth("T4 all ten phase markers (banner/trap/sched/timer/preempt/blk/net/heap/paging/user)" as *u8, t4, pass, fail) 154 155 // T4b -- no phase-failure marker may appear 156 var t4b: i64 = 1 157 if nkg_has(tx, txn, "PGX" as *u8) == 1 { t4b = 0 } 158 if nkg_has(tx, txn, "TX" as *u8) == 1 { t4b = 0 } 159 if nkg_has(tx, txn, "UX" as *u8) == 1 { t4b = 0 } 160 if nkg_has(tx, txn, "BX" as *u8) == 1 { t4b = 0 } 161 if nkg_has(tx, txn, "NF" as *u8) == 1 { t4b = 0 } 162 if nkg_has(tx, txn, "HX" as *u8) == 1 { t4b = 0 } 163 nkg_tooth("T4b no phase-failure marker (PGX/TX/UX/BX/NF/HX) in the transcript" as *u8, t4b, pass, fail) 164 165 // T5 -- NEG-comparator: a mutated golden MUST be rejected, else T3 proves nothing 166 let mg: *u8 = sys_mmap(NKG_TX_CAP) 167 var c: i64 = 0 168 while c < glen { mg[c] = gold[c]; c = c + 1 } 169 mg[0] = (mg[0] + 1) as u8 170 var t5: i64 = 0 171 if nkg_eq(tx, txn, mg, glen) == 0 { t5 = 1 } 172 nkg_tooth("T5 NEG comparator rejects a mutated golden (the check can say no)" as *u8, t5, pass, fail) 173 174 // T6 -- NEG-subject: a corrupted kernel must NOT reproduce the golden transcript 175 let bad: *u8 = sys_mmap(NKG_MEM_SIZE) 176 var d: i64 = 0 177 while d < ilen { bad[d] = img[d]; d = d + 1 } 178 bad[0] = 0 as u8 179 bad[1] = 0 as u8 180 bad[2] = 0 as u8 181 bad[3] = 0 as u8 182 let tx2: *u8 = sys_mmap(NKG_TX_CAP) 183 let res2: *i64 = sys_mmap(64) as *i64 184 nkg_run(bad, ilen, tx2, res2) 185 var t6: i64 = 0 186 if nkg_eq(tx2, res2[3], gold, glen) == 0 { t6 = 1 } 187 nkg_tooth("T6 NEG subject: a corrupted kernel does not reproduce the golden" as *u8, t6, pass, fail) 188 189 // T7 -- the boot does real work, far above the banner baseline 190 var t7: i64 = 0 191 if steps > NKG_BANNER_STEPS * 5 { t7 = 1 } 192 nkg_tooth("T7 step count far exceeds the 17-step banner baseline" as *u8, t7, pass, fail) 193 194 nkg_p(" transcript=[" as *u8); sys_write(1, tx, txn); nkg_p("]\n" as *u8) 195 nkg_p(" bytes=" as *u8); nkg_fn(1, ilen) 196 nkg_p(" steps=" as *u8); nkg_fn(1, steps) 197 nkg_p(" serial_bytes=" as *u8); nkg_fn(1, txn); nkg_p("\n" as *u8) 198 199 let total: i64 = pass[0] + fail[0] 200 nkg_p("NISHIOSKERNELGATE " as *u8); nkg_fn(1, pass[0]); nkg_p("/" as *u8); nkg_fn(1, total) 201 if fail[0] == 0 { nkg_p(" verdict=GREEN\n" as *u8) } else { nkg_p(" verdict=RED\n" as *u8) } 202 203 let lf: i64 = sys_openat_append(NKG_LOG, 420) 204 if lf >= 0 { 205 nkg_fp(lf, "NISHIOSKERNELGATE pass=" as *u8); nkg_fn(lf, pass[0]) 206 nkg_fp(lf, " of=" as *u8); nkg_fn(lf, total) 207 nkg_fp(lf, " bytes=" as *u8); nkg_fn(lf, ilen) 208 nkg_fp(lf, " steps=" as *u8); nkg_fn(lf, steps) 209 nkg_fp(lf, " transcript=" as *u8); sys_write(lf, tx, txn) 210 if fail[0] == 0 { nkg_fp(lf, " verdict=GREEN\n" as *u8) } else { nkg_fp(lf, " verdict=RED\n" as *u8) } 211 sys_close(lf) 212 } 213 if fail[0] == 0 { return 0 } 214 return 1 215}