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}