_k_r2_001d_nvme_gate.nx source

1// _k_r2_001d_nvme_gate.nx -- the X-DRV-W1 STAGE B gate (the 2nd-device-class round-trip + the 2// new-kind/TAMPER proof, resting on PROOF-1 the no-floating foundation). 3// 4// PROOF-1 (FOUNDATION -- judged FIRST, per no-floating): the device-AGNOSTIC shape library 5// (nx_driver_shapes) re-emits the virtio-blk driver byte-identically and the existing SECTGATE 6// sector-data round-trip still runs GREEN on the SOVEREIGN rv64 emu THROUGH the generic shape 7// path. Three lanes (round-trip / byte-identical / virtio-tamper) -- the stage-A regression guard. 8// PROOF-2 (2nd device class -- only claimed after PROOF-1 GREEN): the SAME shape library, driven 9// by knowledge/specs/nvme_admin_enable_virt.spec alone, has the emitter ORGAN (nx_drvgen) AUTHOR 10// an NVMe-class controller bring-up image; the SOVEREIGN rv64 emu (+ the new NVMe device model) 11// runs it; the driver completes CC.EN->poll-CSTS.RDY, binds ASQ/ACQ, lays the 64-byte SQE, rings 12// the SQ-Tail doorbell, the device posts the phase-tagged CQE, the driver polls the CQE phase bit 13// + reads NvmeCqPeek back == cqpeek_expected. Transcript must CONTAIN "VIO-NVME EN RDY ASQ SQE 14// CQ\n" AND a clean SiFive-finisher halt (BOOTSOV verdict=GREEN). 15// TAMPER (no-false-green): bump cqpeek_expected by ONE in the SPEC, re-emit via nx_drvgen, re-run. 16// The CqPeek read-back verify branches past the last stage -> the transcript loses ONLY its " CQ" 17// canary (the "...ASQ SQE" tail survives) -> the KAT goes RED. The PROOF-2 GREEN is gated on 18// tamper_bites==1, so the green is a REAL run, not an assertion. 19// DISTINCTNESS (refutes "virtio-disguised"): (1) STRUCTURAL -- the NVMe image CONTAINS a backward 20// branch (a poll loop: negative B-type immediate => instruction-word bit31 set on a 0x63 opcode), 21// and the virtio image contains NONE (its handshake is straight-line forward-only; constant- 22// lifting cannot add a loop -- the eoe/X-AUT-006d argument). (2) BYTE-DISTINCT -- the NVMe image 23// bytes != the virtio image bytes AND the goldens differ. 24// 25// Every verdict comes from a PRINTED marker off a REAL run, never an asserted GREEN; raw bytes are 26// read SOVEREIGNLY (sys_read in the organ; a PowerShell pipe would corrupt a raw byte read). NO 27// qemu / gcc / openssl / python anywhere -- the sovereign emu IS the runtime; NVMe/PCI is a last- 28// mile interop probe + measuring stick to EXCEED, never a substrate. Marker -> knowledge/status/ 29// virtio_blk.log (NVMEGATE row). Overall verdict=GREEN iff PROOF-1 GREEN AND PROOF-2 GREEN AND 30// TAMPER bites AND distinctness holds. Sovereign orchestration (fork/dup3/execve/wait4). 31// license_tier: ORIGINAL 32import "nx_syscalls.nx" 33 34func ng_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 35func ng_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 } 36func ng_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 } 37 38// run nx_virtio_hs_emit <spec> (the refactored, shape-library-driven virtio emitter); serial muted. 39func ng_run_virtio_emit(spec: *u8) -> i64 { 40 let pid: i64 = sys_fork() 41 if pid == 0 { 42 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4) 43 if dn >= 0 { sys_dup3(dn, 1, 0) } 44 let argv: *i64 = sys_mmap(32) as *i64 45 argv[0] = "_offc/nx_virtio_hs_emit.elf" as *u8 as i64 46 argv[1] = spec as i64 47 argv[2] = 0 48 let envp: *i64 = sys_mmap(16) as *i64 49 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 50 envp[1] = 0 51 sys_execve("_offc/nx_virtio_hs_emit.elf" as *u8, argv, envp) 52 sys_exit(127) 53 } 54 let st: *i64 = sys_mmap(16) as *i64 55 sys_wait4(pid, st, 0) 56 return st[0] 57} 58 59// run nx_drvgen <spec> (the GENERIC 2nd-class emitter ORGAN); serial muted. 60func ng_run_drvgen(spec: *u8) -> i64 { 61 let pid: i64 = sys_fork() 62 if pid == 0 { 63 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4) 64 if dn >= 0 { sys_dup3(dn, 1, 0) } 65 let argv: *i64 = sys_mmap(32) as *i64 66 argv[0] = "_offc/nx_drvgen.elf" as *u8 as i64 67 argv[1] = spec as i64 68 argv[2] = 0 69 let envp: *i64 = sys_mmap(16) as *i64 70 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 71 envp[1] = 0 72 sys_execve("_offc/nx_drvgen.elf" as *u8, argv, envp) 73 sys_exit(127) 74 } 75 let st: *i64 = sys_mmap(16) as *i64 76 sys_wait4(pid, st, 0) 77 return st[0] 78} 79 80// run the SOVEREIGN rv64 emulator on binpath; serial -> outpath; return wait status 81func ng_run_sov(binpath: *u8, outpath: *u8) -> i64 { 82 let pid: i64 = sys_fork() 83 if pid == 0 { 84 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 85 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 86 let argv: *i64 = sys_mmap(32) as *i64 87 argv[0] = "_offc/nx_boot_run_sov.elf" as *u8 as i64 88 argv[1] = binpath as i64 89 argv[2] = 0 90 let envp: *i64 = sys_mmap(16) as *i64 91 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 92 envp[1] = 0 93 sys_execve("_offc/nx_boot_run_sov.elf" as *u8, argv, envp) 94 sys_exit(127) 95 } 96 let st: *i64 = sys_mmap(16) as *i64 97 sys_wait4(pid, st, 0) 98 return st[0] 99} 100 101// read whole file into buf (cap-1 max) SOVEREIGNLY; return byte count (0 if absent) 102func ng_read(path: *u8, buf: *u8, cap: i64) -> i64 { 103 let fd: i64 = sys_openat_rd(path) 104 if fd < 0 { return 0 } 105 var n: i64 = 0 106 var go: i64 = 1 107 while go == 1 { let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, cap - 1 - n); if r <= 0 { go = 0 } else { n = n + r } if n >= cap - 1 { go = 0 } } 108 sys_close(fd) 109 return n 110} 111 112// does buf[0,n) contain pat (length pl)? 1/0 113func ng_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 114 if pl <= 0 { return 0 } 115 var i: i64 = 0 116 while i + pl <= n { 117 var k: i64 = 0 118 var hit: i64 = 1 119 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } 120 if hit == 1 { return 1 } 121 i = i + 1 122 } 123 return 0 124} 125 126func ng_strlen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 127 128// SOVEREIGN byte-equal: 1 iff same length AND every byte equal. 129func ng_bytes_equal(a: *u8, na: i64, b: *u8, nb: i64) -> i64 { 130 if na != nb { return 0 } 131 var i: i64 = 0 132 while i < na { if a[i] != b[i] { return 0 } i = i + 1 } 133 return 1 134} 135 136// read a little-endian 32-bit word from buf at byte offset o. 137func ng_w32(buf: *u8, o: i64) -> i64 { 138 let b0: i64 = buf[o] as i64 139 let b1: i64 = buf[o+1] as i64 140 let b2: i64 = buf[o+2] as i64 141 let b3: i64 = buf[o+3] as i64 142 return b0 | (b1 << 8) | (b2 << 16) | (b3 << 24) 143} 144 145// count BACKWARD branches in an rv64 flat image: a B-type branch (opcode 0x63) whose imm[12] 146// sign bit (instruction-word bit31) is set -> a negative (backward) branch displacement = a loop. 147// virtio's image has NONE (straight-line forward-only handshake); NVMe's has >=1 (the poll loops). 148func ng_count_backward_branches(buf: *u8, n: i64) -> i64 { 149 var c: i64 = 0 150 var o: i64 = 0 151 while o + 4 <= n { 152 let w: i64 = ng_w32(buf, o) 153 if (w & 0x7f) == 0x63 { if (w & 0x80000000) != 0 { c = c + 1 } } 154 o = o + 4 155 } 156 return c 157} 158 159func main() -> i64 { 160 // ---- PROOF-1 inputs (virtio, the foundation) ---- 161 let vspec: *u8 = "knowledge/specs/virtio_blk_sector_virt.spec" as *u8 162 let vbin: *u8 = "runtime/_hdl_build/_virtio_sector_virt.bin" as *u8 163 let vgold: *u8 = "runtime/_hdl_build/_virtio_sector_virt.bin.gold" as *u8 164 let vref: *u8 = "runtime/_hdl_build/_virtio_sector_virt.ref.bin" as *u8 165 let vtamper: *u8 = "/tmp/_ngate_vtamper.bin" as *u8 166 let vsov: *u8 = "/tmp/_ngate_vsov.txt" as *u8 167 let vsov_t: *u8 = "/tmp/_ngate_vsov_t.txt" as *u8 168 let v_statgold: *u8 = "VIO ACK DRV FEAT OK VQ DESC USED STAT" as *u8 169 // the unique `lwu t3, 0x6C(t2)` -- the virtio QueueSectPeek read-back load; its following li's 170 // high immediate byte (+11) is the byte the virtio tamper corrupts. 171 let NG_VSECT_LOAD: i64 = 0x06c3ee03 172 // ---- PROOF-2 inputs (NVMe, the 2nd class) ---- 173 let nspec: *u8 = "knowledge/specs/nvme_admin_enable_virt.spec" as *u8 174 let nbin: *u8 = "runtime/_hdl_build/_nvme_admin_virt.bin" as *u8 175 let ngold: *u8 = "runtime/_hdl_build/_nvme_admin_virt.bin.gold" as *u8 176 let ntspec: *u8 = "/tmp/_ngate_nvme_tamper.spec" as *u8 177 let nsov: *u8 = "/tmp/_ngate_nsov.txt" as *u8 178 let nsov_t: *u8 = "/tmp/_ngate_nsov_t.txt" as *u8 179 // the "...ASQ SQE" tail the NVMe tamper must KEEP (only " CQ" drops). 180 let n_sqegold: *u8 = "VIO-NVME EN RDY ASQ SQE" as *u8 181 182 ng_p("=== X-DRV-W1 stage B gate (PROOF-1 virtio-reemit foundation -> PROOF-2 NVMe-class round-trip -> TAMPER -> DISTINCTNESS; SOVEREIGN-only, no qemu) ===\n" as *u8) 183 184 let lfd: i64 = sys_openat_append("knowledge/status/virtio_blk.log" as *u8, 0x1a4) 185 186 // ================= PROOF-1: virtio re-emit byte-identical + SECTGATE round-trip ================ 187 let vest: i64 = ng_run_virtio_emit(vspec) 188 let vgbuf: *u8 = sys_mmap(512) 189 let vgn: i64 = ng_read(vgold, vgbuf, 512) 190 vgbuf[vgn] = 0 as u8 191 let vsst: i64 = ng_run_sov(vbin, vsov) 192 let vsbuf: *u8 = sys_mmap(65536) 193 let vsbn: i64 = ng_read(vsov, vsbuf, 65536) 194 var p1_roundtrip: i64 = 0 195 if vest == 0 { if vgn > 0 { if vsst == 0 { 196 if ng_buf_has(vsbuf, vsbn, vgbuf, vgn) == 1 { if ng_buf_has(vsbuf, vsbn, "BOOTSOV verdict=GREEN" as *u8, 21) == 1 { p1_roundtrip = 1 } } 197 } } } 198 // byte-identical vs the frozen reference 199 let vfresh: *u8 = sys_mmap(8192) 200 let vfn: i64 = ng_read(vbin, vfresh, 8192) 201 let vrbuf: *u8 = sys_mmap(8192) 202 let vrn: i64 = ng_read(vref, vrbuf, 8192) 203 var p1_byte_identical: i64 = 0 204 if vrn > 0 { if ng_bytes_equal(vfresh, vfn, vrbuf, vrn) == 1 { p1_byte_identical = 1 } } 205 // virtio tamper: corrupt the SectPeek-expected const; SECT must drop, STAT survive, byte-check flip 206 let vibuf: *u8 = sys_mmap(8192) 207 let vibn: i64 = ng_read(vbin, vibuf, 8192) 208 var vlpos: i64 = 0 - 1 209 var vo: i64 = 0 210 while vo + 4 <= vibn { if ng_w32(vibuf, vo) == NG_VSECT_LOAD { vlpos = vo; vo = vibn } else { vo = vo + 4 } } 211 var p1_tamper: i64 = 0 212 if vlpos >= 0 { 213 let veb: i64 = vlpos + 11 214 vibuf[veb] = (vibuf[veb] + 1) as u8 215 let vtfd: i64 = sys_openat_wr(vtamper, 0x1a4) 216 if vtfd >= 0 { sys_write(vtfd, vibuf, vibn); sys_close(vtfd) } 217 let vtst: i64 = ng_run_sov(vtamper, vsov_t) 218 let vtbuf: *u8 = sys_mmap(65536) 219 let vtbn: i64 = ng_read(vsov_t, vtbuf, 65536) 220 let drops: i64 = ng_buf_has(vtbuf, vtbn, vgbuf, vgn) // full golden should MISS 221 let keeps: i64 = ng_buf_has(vtbuf, vtbn, v_statgold, ng_strlen(v_statgold)) // STAT tail survives 222 let flip: i64 = ng_bytes_equal(vibuf, vibn, vrbuf, vrn) // byte-equal now FALSE 223 if drops == 0 { if keeps == 1 { if flip == 0 { p1_tamper = 1 } } } 224 } 225 var proof1: i64 = 0 226 if p1_roundtrip == 1 { if p1_byte_identical == 1 { if p1_tamper == 1 { proof1 = 1 } } } 227 228 ng_p(" PROOF-1(virtio foundation): roundtrip=" as *u8); if p1_roundtrip==1 {ng_p("GREEN" as *u8)} else {ng_p("RED" as *u8)} 229 ng_p(" byte-identical=" as *u8); if p1_byte_identical==1 {ng_p("yes(" as *u8); ng_fn(1,vfn); ng_p("B)" as *u8)} else {ng_p("no" as *u8)} 230 ng_p(" tamper=" as *u8); if p1_tamper==1 {ng_p("rejected(SECT-drops,STAT-survives,byte-flips)" as *u8)} else {ng_p("not-rejected" as *u8)} 231 ng_p("\n" as *u8) 232 233 // NO-FLOATING: PROOF-2 is only claimed once PROOF-1 is GREEN. 234 var proof2: i64 = 0 235 var nvme_tamper: i64 = 0 236 var distinct_struct: i64 = 0 237 var distinct_bytes: i64 = 0 238 var nback: i64 = 0 239 var vback: i64 = 0 240 var nfn: i64 = 0 241 if proof1 == 1 { 242 // ============== PROOF-2: nx_drvgen authors the NVMe image; sovereign emu round-trip ========== 243 let nest: i64 = ng_run_drvgen(nspec) 244 let ngbuf: *u8 = sys_mmap(512) 245 let ngn: i64 = ng_read(ngold, ngbuf, 512) 246 ngbuf[ngn] = 0 as u8 247 let nsst: i64 = ng_run_sov(nbin, nsov) 248 let nsbuf: *u8 = sys_mmap(65536) 249 let nsbn: i64 = ng_read(nsov, nsbuf, 65536) 250 if nest == 0 { if ngn > 0 { if nsst == 0 { 251 if ng_buf_has(nsbuf, nsbn, ngbuf, ngn) == 1 { if ng_buf_has(nsbuf, nsbn, "BOOTSOV verdict=GREEN" as *u8, 21) == 1 { proof2 = 1 } } 252 } } } 253 254 // ============== TAMPER: bump cqpeek_expected by 1 in the SPEC, re-emit, re-run ============== 255 // author a tampered copy of the spec: replace "cqpeek_expected 0x12340001" -> "...0x12340002". 256 let sbuf: *u8 = sys_mmap(8192) 257 let sn: i64 = ng_read(nspec, sbuf, 8192) 258 // find the literal "cqpeek_expected 0x12340001" and bump the final '1' digit to '2'. 259 let pat: *u8 = "cqpeek_expected 0x12340001" as *u8 260 let pl: i64 = ng_strlen(pat) 261 var ppos: i64 = 0 - 1 262 var si: i64 = 0 263 while si + pl <= sn { 264 var kk: i64 = 0 265 var hh: i64 = 1 266 while kk < pl { if sbuf[si+kk] != pat[kk] { hh = 0; kk = pl } else { kk = kk + 1 } } 267 if hh == 1 { ppos = si; si = sn } else { si = si + 1 } 268 } 269 if ppos >= 0 { 270 // the last char of the pattern is the low nibble '1'; bump it to '2' (0x12340001 -> ...02). 271 sbuf[ppos + pl - 1] = 50 as u8 // ASCII '2' 272 let tfd: i64 = sys_openat_wr(ntspec, 0x1a4) 273 if tfd >= 0 { sys_write(tfd, sbuf, sn); sys_close(tfd) } 274 // the tampered spec emits to its own `out` -- but the spec's out row points at the real 275 // nbin. Re-emitting the tampered spec OVERWRITES nbin with the bad-KAT image; run it, 276 // assert " CQ" drops + "...ASQ SQE" survives, then RE-EMIT the clean spec to restore nbin. 277 let tet: i64 = ng_run_drvgen(ntspec) 278 let tsst: i64 = ng_run_sov(nbin, nsov_t) 279 let tbuf: *u8 = sys_mmap(65536) 280 let tbn: i64 = ng_read(nsov_t, tbuf, 65536) 281 let cq_drops: i64 = ng_buf_has(tbuf, tbn, ngbuf, ngn) // full golden MISS 282 let sqe_keeps: i64 = ng_buf_has(tbuf, tbn, n_sqegold, ng_strlen(n_sqegold)) // ASQ SQE survives 283 if tet == 0 { if cq_drops == 0 { if sqe_keeps == 1 { nvme_tamper = 1 } } } 284 // restore the clean image from the real spec (additive: leave nbin == the GREEN image). 285 ng_run_drvgen(nspec) 286 } 287 288 // ============== DISTINCTNESS ============== 289 // (1) STRUCTURAL: NVMe image HAS backward branch(es) (poll loops); virtio image has NONE. 290 let nfresh: *u8 = sys_mmap(8192) 291 nfn = ng_read(nbin, nfresh, 8192) 292 nback = ng_count_backward_branches(nfresh, nfn) 293 vback = ng_count_backward_branches(vfresh, vfn) 294 if nback >= 1 { if vback == 0 { distinct_struct = 1 } } 295 // (2) BYTE-DISTINCT: NVMe image bytes != virtio image bytes AND goldens differ. 296 let bytes_differ: i64 = ng_bytes_equal(nfresh, nfn, vfresh, vfn) // 0 = differ 297 let gold_differ: i64 = ng_bytes_equal(ngbuf, ngn, vgbuf, vgn) // 0 = differ 298 if bytes_differ == 0 { if gold_differ == 0 { distinct_bytes = 1 } } 299 300 ng_p(" PROOF-2(NVMe 2nd class): roundtrip=" as *u8); if proof2==1 {ng_p("GREEN(transcript==golden+clean-halt, " as *u8); ng_fn(1,nfn); ng_p("B)" as *u8)} else {ng_p("RED" as *u8)} 301 ng_p(" tamper=" as *u8); if nvme_tamper==1 {ng_p("rejected(CQ-drops,SQE-survives)" as *u8)} else {ng_p("not-rejected" as *u8)} 302 ng_p("\n DISTINCT: nvme-backward-branches=" as *u8); ng_fn(1, nback); ng_p(" virtio-backward-branches=" as *u8); ng_fn(1, vback) 303 ng_p(" image-bytes-differ=" as *u8); if distinct_bytes==1 {ng_p("yes" as *u8)} else {ng_p("no" as *u8)} 304 ng_p("\n" as *u8) 305 } else { 306 ng_p(" PROOF-2 SKIPPED: PROOF-1 not GREEN (no-floating: the 2nd class may not rest on a non-DONE foundation)\n" as *u8) 307 } 308 309 var pass: i64 = 0 310 if proof1 == 1 { if proof2 == 1 { if nvme_tamper == 1 { if distinct_struct == 1 { if distinct_bytes == 1 { pass = 1 } } } } } 311 312 if pass == 1 { 313 ng_p("NVMEGATE verdict=GREEN stage=B (PROOF-1 virtio-reemit foundation GREEN -> PROOF-2 NVMe-class CC.EN->CSTS.RDY enable + ASQ/ACQ bind + 64B SQE + SQ-Tail doorbell + phase-tagged CQE + NvmeCqPeek read-back round-tripped GREEN on the sovereign emu; the CqPeek-expected spec TAMPER dropped ONLY the CQ canary; the NVMe driver control-flow is DISTINCT from virtio -- it carries poll-loop backward branches virtio lacks and its bytes+golden differ)\n" as *u8) 314 if lfd >= 0 { 315 ng_fp(lfd, "NVMEGATE verdict=GREEN stage=B runtime=sovereign-emu device=nvme enable=CC.EN->CSTS.RDY queue=ASQ/ACQ+doorbell sqe=64B cqe=phase-tagged cqpeek-readback=verified bytes=" as *u8); ng_fn(lfd, nfn) 316 ng_fp(lfd, " proof1=virtio-reemit-identical transcript==golden tamper=rejected(CQ-drops,SQE-survives) distinct=poll-loop+phase-bit(nvme-backward-branches=" as *u8); ng_fn(lfd, nback) 317 ng_fp(lfd, ",virtio-backward-branches=" as *u8); ng_fn(lfd, vback) 318 ng_fp(lfd, ",bytes+golden-differ) golden=VIO-NVME EN RDY ASQ SQE CQ epoch=" as *u8); ng_fn(lfd, sys_now_realtime_sec()); ng_fp(lfd, "\n" as *u8); sys_close(lfd) 319 } 320 sys_exit(0); return 0 321 } 322 ng_p("NVMEGATE verdict=RED stage=B (one of PROOF-1/PROOF-2/TAMPER/DISTINCT not satisfied)\n" as *u8) 323 if lfd >= 0 { 324 ng_fp(lfd, "NVMEGATE verdict=RED stage=B proof1=" as *u8); ng_fn(lfd, proof1) 325 ng_fp(lfd, " proof2=" as *u8); ng_fn(lfd, proof2) 326 ng_fp(lfd, " nvme_tamper=" as *u8); ng_fn(lfd, nvme_tamper) 327 ng_fp(lfd, " distinct_struct=" as *u8); ng_fn(lfd, distinct_struct) 328 ng_fp(lfd, " distinct_bytes=" as *u8); ng_fn(lfd, distinct_bytes); ng_fp(lfd, "\n" as *u8); sys_close(lfd) 329 } 330 sys_exit(1) 331 return 1 332}