_k_r2_001b2b_gate.nx source

1// _k_r2_001b2b_gate.nx -- the K-R2-001b2b gate (virtio-MMIO AVAIL-CONSUME + USED-RING 2// WRITEBACK layer; the third slice of the K-R2-001b virtqueue epic, on top of b2a's 3// descriptor-DMA). Drives the full author->handshake->queue-config->descriptor-DMA-> 4// avail/used chain with NO mocks: runs the REAL nx_virtio_hs_emit (the team AUTHORS the 5// rv64 image + the TABLE-COMPUTED golden transcript from the avail/used spec), then RUNS 6// the image on the SOVEREIGN rv64 emulator (rv64im_min_sim + the rv64im_min_virtio device 7// now, on the SECOND QueueNotify kick, reading the avail ring head, walking the descriptor 8// (b2a DMA), WRITING the used ring (used.ring[0].id/.len) + BUMPING used.idx back into guest 9// RAM, and latching used.idx into the QueueUsedIdxPeek RO register -- the PRIMARY, gating 10// lane: Nishi owns the runtime) and asserts the captured serial transcript CONTAINS the 11// emitter's golden ("VIO ACK DRV FEAT OK VQ DESC USED\n" -- after the descriptor-DMA the 12// driver published the avail ring, kicked QueueNotify, the device consumed it + wrote the 13// used ring, then the driver READ QueueUsedIdxPeek BACK and verified it == used_idx_expected: 14// the used-ring writeback binding proof) AND the sovereign emu reports a clean SiFive- 15// finisher halt. 16// 17// Then the ALIGNMENT lane: qemu-system-riscv64 -machine virt -global 18// virtio-mmio.force-legacy=true with a REAL virtio-blk-device backing. The gate authors a 19// SECOND image from a base-rewritten spec (the blk device lands at slot 0x10008000) and runs 20// the SAME driver against the REAL legacy virtio-blk transport: it completes the handshake + 21// queue config, lays the SAME descriptor + the SAME avail ring into qemu guest RAM, and kicks 22// the real QueueNotify -- the real legacy transport genuinely walks the ring. The 23// QueueUsedIdxPeek result register is a sovereign-model instrument the real device does not 24// expose (it reads 0), so on qemu the used-ring read-back verify gracefully drops ONLY 25// " USED" (and the sovereign-only QueueDescPeek already drops " DESC"); the gate asserts the 26// qemu transcript contains the b1 prefix golden ("VIO ACK DRV FEAT OK VQ") -- proving the 27// SAME driver lays the avail ring + kicks the real device -> lanes AGREE on every register 28// the real transport can observe. 29// 30// Finally a TAMPER test: corrupt the QueueUsedIdxPeek-EXPECTED constant in the sovereign 31// image (the driver loads its own QueueUsedIdxPeek read-back into t3 via lw and compares 32// against this li-loaded expected in t4; bumping the expected's immediate makes t3 != t4) -> 33// the read-back verify branches PAST stage 7 straight to the finisher -> the transcript loses 34// ONLY its " USED" canary (the "VIO ACK DRV FEAT OK VQ DESC" tail survives) -> the gate MUST 35// go RED. Evidence -> knowledge/status/virtio_blk.log (USEDGATE row; the queue row's ||MARK= 36// reads it). Sovereign orchestration (fork/dup3/execve/wait4). license_tier: ORIGINAL 37import "nx_syscalls.nx" 38import "nx_gate_verdict.nx" 39 40// bytes qemu actually produced. ZERO means qemu-system-riscv64 never ran (absent on this host) -- 41// an EXTERNAL PRECONDITION, not a failure of the driver or the device model under test. 42static g_qemu_bytes: i64 43 44// the unique rv64 encoding of `lw t3, 0x64(t2)` -- the QueueUsedIdxPeek read-back load (f3=2, 45// sign-extend; used.idx is a small non-negative int). The UsedIdxPeek-expected constant the 46// driver compares against is the li that follows it (lui at +4, addi at +8); corrupting the 47// addi's high immediate byte (+11) is the avail/used tamper. 48const G_QUSEDIDXPEEK_LOAD_WORD: i64 = 0x0643ae03 // lw t3, 0x064(t2) (QueueUsedIdxPeek read-back) 49 50func g_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 51func g_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 } 52func g_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 } 53 54// run nx_virtio_hs_emit <spec>; return child wait status (0 = ok) 55func g_run_emit(spec: *u8) -> i64 { 56 let pid: i64 = sys_fork() 57 if pid == 0 { 58 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4) 59 if dn >= 0 { sys_dup3(dn, 1, 0) } 60 let argv: *i64 = sys_mmap(32) as *i64 61 argv[0] = "_offc/nx_virtio_hs_emit.elf" as *u8 as i64 62 argv[1] = spec as i64 63 argv[2] = 0 64 let envp: *i64 = sys_mmap(16) as *i64 65 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 66 envp[1] = 0 67 sys_execve("_offc/nx_virtio_hs_emit.elf" as *u8, argv, envp) 68 sys_exit(127) 69 } 70 let st: *i64 = sys_mmap(16) as *i64 71 sys_wait4(pid, st, 0) 72 return st[0] 73} 74 75// run the SOVEREIGN rv64 emulator on binpath; serial -> outpath; return wait status 76func g_run_sov(binpath: *u8, outpath: *u8) -> i64 { 77 let pid: i64 = sys_fork() 78 if pid == 0 { 79 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 80 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 81 let argv: *i64 = sys_mmap(32) as *i64 82 argv[0] = "_offc/nx_boot_run_sov.elf" as *u8 as i64 83 argv[1] = binpath as i64 84 argv[2] = 0 85 let envp: *i64 = sys_mmap(16) as *i64 86 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 87 envp[1] = 0 88 sys_execve("_offc/nx_boot_run_sov.elf" as *u8, argv, envp) 89 sys_exit(127) 90 } 91 let st: *i64 = sys_mmap(16) as *i64 92 sys_wait4(pid, st, 0) 93 return st[0] 94} 95 96// run qemu-system-riscv64 virt + legacy virtio-blk-device on binpath; serial -> outpath. 97func g_run_qemu(binpath: *u8, outpath: *u8, backing: *u8) -> i64 { 98 let pid: i64 = sys_fork() 99 if pid == 0 { 100 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 101 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 102 let argv: *i64 = sys_mmap(128) as *i64 103 argv[0] = "/usr/bin/qemu-system-riscv64" as *u8 as i64 104 argv[1] = "-machine" as *u8 as i64 105 argv[2] = "virt" as *u8 as i64 106 argv[3] = "-global" as *u8 as i64 107 argv[4] = "virtio-mmio.force-legacy=true" as *u8 as i64 108 argv[5] = "-nographic" as *u8 as i64 109 argv[6] = "-bios" as *u8 as i64 110 argv[7] = binpath as i64 111 argv[8] = "-drive" as *u8 as i64 112 argv[9] = "file=/tmp/_usedgate_backing.img,if=none,format=raw,id=hd0" as *u8 as i64 113 argv[10] = "-device" as *u8 as i64 114 argv[11] = "virtio-blk-device,drive=hd0" as *u8 as i64 115 argv[12] = 0 116 let envp: *i64 = sys_mmap(16) as *i64 117 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 118 envp[1] = 0 119 sys_execve("/usr/bin/qemu-system-riscv64" as *u8, argv, envp) 120 sys_exit(127) 121 } 122 let st: *i64 = sys_mmap(16) as *i64 123 sys_wait4(pid, st, 0) 124 return st[0] 125} 126 127// create a small raw backing file for the qemu virtio-blk device (4 sectors of zeros). 128func g_make_backing(path: *u8) -> i64 { 129 let fd: i64 = sys_openat_wr(path, 0x1a4) 130 if fd < 0 { return 0 - 1 } 131 let z: *u8 = sys_mmap(2048) 132 var i: i64 = 0 133 while i < 2048 { z[i] = 0 as u8; i = i + 1 } 134 sys_write(fd, z, 2048) 135 sys_close(fd) 136 return 0 137} 138 139// read whole file into buf (cap-1 max); return byte count (0 if absent) 140func g_read(path: *u8, buf: *u8, cap: i64) -> i64 { 141 let fd: i64 = sys_openat_rd(path) 142 if fd < 0 { return 0 } 143 var n: i64 = 0 144 var go: i64 = 1 145 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 } } 146 sys_close(fd) 147 return n 148} 149 150// does buf[0,n) contain pat (length pl)? 1/0 151func g_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 152 if pl <= 0 { return 0 } 153 var i: i64 = 0 154 while i + pl <= n { 155 var k: i64 = 0 156 var hit: i64 = 1 157 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } 158 if hit == 1 { return 1 } 159 i = i + 1 160 } 161 return 0 162} 163 164// read a little-endian 32-bit word from buf at byte offset o. 165func g_w32(buf: *u8, o: i64) -> i64 { 166 let b0: i64 = buf[o] as i64 167 let b1: i64 = buf[o+1] as i64 168 let b2: i64 = buf[o+2] as i64 169 let b3: i64 = buf[o+3] as i64 170 return b0 | (b1 << 8) | (b2 << 16) | (b3 << 24) 171} 172 173// find the byte offset of the (unique) QueueUsedIdxPeek read-back load word in the image; -1 174// if absent. The UsedIdxPeek-expected li the driver compares against is at off+4 (lui) / 175// off+8 (addi); the addi's high immediate byte is at off+11. 176func g_find_usedidxpeek_load(buf: *u8, n: i64) -> i64 { 177 var o: i64 = 0 178 while o + 4 <= n { 179 if g_w32(buf, o) == G_QUSEDIDXPEEK_LOAD_WORD { return o } 180 o = o + 4 181 } 182 return 0 - 1 183} 184 185func g_strlen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 186 187// does line [ls,le) of buf begin with key? 1/0 188func g_line_is(buf: *u8, ls: i64, le: i64, key: *u8) -> i64 { 189 var k: i64 = 0 190 while key[k] != (0 as u8) { 191 if ls + k >= le { return 0 } 192 if buf[ls + k] != key[k] { return 0 } 193 k = k + 1 194 } 195 return 1 196} 197 198// author the qemu-alignment spec: copy the main spec, but replace the `base ` line value 199// with the qemu blk slot and the `out ` line with the qemu image path. (The ring page + 200// data buffer addresses are guest-RAM addresses valid on both lanes -- left as is.) 201func g_write_qemu_spec(mainspec: *u8, derived: *u8, qemu_out: *u8) -> i64 { 202 let buf: *u8 = sys_mmap(8192) 203 let n: i64 = g_read(mainspec, buf, 8192) 204 if n <= 0 { return 0 - 1 } 205 let ofd: i64 = sys_openat_wr(derived, 0x1a4) 206 if ofd < 0 { return 0 - 1 } 207 var ls: i64 = 0 208 while ls < n { 209 var le: i64 = ls 210 var scan: i64 = 1 211 while scan == 1 { if le >= n { scan = 0 } else { if buf[le] == (10 as u8) { scan = 0 } else { le = le + 1 } } } 212 if g_line_is(buf, ls, le, "base " as *u8) == 1 { 213 g_fp(ofd, "base 0x10008000\n" as *u8) 214 } else { 215 if g_line_is(buf, ls, le, "out " as *u8) == 1 { 216 g_fp(ofd, "out " as *u8); g_fp(ofd, qemu_out); g_fp(ofd, "\n" as *u8) 217 } else { 218 sys_write(ofd, (buf as i64 + ls) as *u8, le - ls) 219 g_fp(ofd, "\n" as *u8) 220 } 221 } 222 ls = le + 1 223 } 224 sys_close(ofd) 225 return 0 226} 227 228func main() -> i64 { 229 let spec: *u8 = "knowledge/specs/virtio_blk_availused_virt.spec" as *u8 230 let binpath: *u8 = "runtime/_hdl_build/_virtio_availused_virt.bin" as *u8 231 let goldpath: *u8 = "runtime/_hdl_build/_virtio_availused_virt.bin.gold" as *u8 232 let qemu_spec: *u8 = "/tmp/_usedgate_qemu.spec" as *u8 233 let qemu_bin: *u8 = "/tmp/_usedgate_qemu.bin" as *u8 234 let backing: *u8 = "/tmp/_usedgate_backing.img" as *u8 235 let tamper_bin: *u8 = "/tmp/_usedgate_tamper.bin" as *u8 236 let sov_serial: *u8 = "/tmp/_usedgate_sov.txt" as *u8 237 let qemu_serial: *u8 = "/tmp/_usedgate_qemu.txt" as *u8 238 let sov_tamper: *u8 = "/tmp/_usedgate_sov_tamper.txt" as *u8 239 // the b2a prefix golden the qemu alignment lane asserts (the real device has neither 240 // QueueDescPeek nor QueueUsedIdxPeek, so on qemu the descriptor-DMA + used-ring verifies 241 // drop " DESC" and " USED", leaving the b1 prefix the real transport can observe). 242 let prefix_gold: *u8 = "VIO ACK DRV FEAT OK VQ" as *u8 243 // the b2a "DESC" tail the tamper must KEEP (only " USED" drops under the used-idx tamper). 244 let desconly_gold: *u8 = "VIO ACK DRV FEAT OK VQ DESC" as *u8 245 g_p("=== virtio-MMIO avail/used gate (K-R2-001b2b: SOVEREIGN rv64 avail-ring publish + device used-ring writeback + QueueUsedIdxPeek read-back + qemu virtio-blk alignment) ===\n" as *u8) 246 247 let lfd: i64 = sys_openat_append("knowledge/status/virtio_blk.log" as *u8, 0x1a4) 248 249 // STEP 1: author the SOVEREIGN image (base 0x10001000) + the golden transcript. 250 let est: i64 = g_run_emit(spec) 251 if est != 0 { 252 g_p("USEDGATE verdict=RED reason=emit-failed\n" as *u8) 253 if lfd >= 0 { g_fp(lfd, "USEDGATE verdict=RED reason=emit-failed\n" as *u8); sys_close(lfd) } 254 sys_exit(1); return 1 255 } 256 let gold: *u8 = sys_mmap(512) 257 let gn: i64 = g_read(goldpath, gold, 512) 258 gold[gn] = 0 as u8 259 if gn <= 0 { 260 g_p("USEDGATE verdict=RED reason=golden-missing\n" as *u8) 261 if lfd >= 0 { g_fp(lfd, "USEDGATE verdict=RED reason=golden-missing\n" as *u8); sys_close(lfd) } 262 sys_exit(1); return 1 263 } 264 265 // STEP 2 (PRIMARY): the Nishi sovereign rv64 emulator RUNS the image -- handshake + queue 266 // config + descriptor lay (b2a) + avail-ring publish + QueueNotify kick + device consume + 267 // used-ring writeback + QueueUsedIdxPeek read-back verify -> transcript must CONTAIN the 268 // full golden ("...DESC USED\n"). 269 let sst: i64 = g_run_sov(binpath, sov_serial) 270 let sbuf: *u8 = sys_mmap(65536) 271 let sbn: i64 = g_read(sov_serial, sbuf, 65536) 272 let trans_ok: i64 = g_buf_has(sbuf, sbn, gold, gn) 273 let halt_ok: i64 = g_buf_has(sbuf, sbn, "BOOTSOV verdict=GREEN" as *u8, 21) 274 var sov_ok: i64 = 0 275 if sst == 0 { if trans_ok == 1 { if halt_ok == 1 { sov_ok = 1 } } } 276 277 // STEP 3 (ALIGNMENT): author the qemu-base image (slot 0x10008000) + run qemu with a REAL 278 // legacy virtio-blk-device; the SAME driver lays the SAME descriptor + the SAME avail ring 279 // into qemu guest RAM and kicks the real QueueNotify (the real transport walks the ring). 280 // The sovereign-only QueueDescPeek/QueueUsedIdxPeek registers read 0 on the real device, so 281 // the descriptor-DMA + used-ring verifies drop " DESC"/" USED" there; assert the b1 prefix 282 // golden ("VIO ACK DRV FEAT OK VQ") appears, proving the driver runs identically against 283 // the real transport up to the avail publish + kick. 284 g_make_backing(backing) 285 g_write_qemu_spec(spec, qemu_spec, qemu_bin) 286 let qest: i64 = g_run_emit(qemu_spec) 287 var align: i64 = 0 288 if qest == 0 { 289 let qst: i64 = g_run_qemu(qemu_bin, qemu_serial, backing) 290 let qbuf: *u8 = sys_mmap(65536) 291 let qbn: i64 = g_read(qemu_serial, qbuf, 65536) 292 g_qemu_bytes = qbn 293 let qtrans: i64 = g_buf_has(qbuf, qbn, prefix_gold, g_strlen(prefix_gold)) 294 if qst == 0 { if qtrans == 1 { align = 1 } } 295 } 296 297 // STEP 4 (TAMPER): corrupt the QueueUsedIdxPeek-EXPECTED constant in the sovereign image. 298 // Scan for the unique QueueUsedIdxPeek read-back load word; the expected li the driver 299 // compares against is the addi at load+8. Bump that addi's high immediate byte (load+11) 300 // so the expected != the value the device latched -> the read-back verify branches to the 301 // finisher -> ONLY the " USED" canary drops (the "...DESC" tail survives) -> gate MUST RED. 302 let ibuf: *u8 = sys_mmap(8192) 303 let ibn: i64 = g_read(binpath, ibuf, 8192) 304 let lpos: i64 = g_find_usedidxpeek_load(ibuf, ibn) 305 var tamper_built: i64 = 0 306 if lpos >= 0 { 307 let ebyte: i64 = lpos + 11 // high immediate byte of the expected addi 308 ibuf[ebyte] = (ibuf[ebyte] + 1) as u8 309 let tfd: i64 = sys_openat_wr(tamper_bin, 0x1a4) 310 if tfd >= 0 { sys_write(tfd, ibuf, ibn); sys_close(tfd); tamper_built = 1 } 311 } 312 var tamper_bites: i64 = 0 313 var tamper_keeps_desc: i64 = 0 314 if tamper_built == 1 { 315 let tst: i64 = g_run_sov(tamper_bin, sov_tamper) 316 let tbuf: *u8 = sys_mmap(65536) 317 let tbn: i64 = g_read(sov_tamper, tbuf, 65536) 318 let tamper_trans: i64 = g_buf_has(tbuf, tbn, gold, gn) // full golden should now MISS 319 let tamper_desc: i64 = g_buf_has(tbuf, tbn, desconly_gold, g_strlen(desconly_gold)) // DESC tail survives 320 if tamper_trans == 0 { tamper_bites = 1 } 321 if tamper_desc == 1 { tamper_keeps_desc = 1 } 322 } 323 324 // ---- MIGRATED ONTO THE BASE CLASS (D001), BY HAND ---------------------------------------------- 325 // BUILT-UNPROMOTED and unrunnable before today -- and its SPEC was missing too, so the layer it 326 // covers had no live check at all. ★★★★★★A GATE NOBODY CAN RUN DOES NOT DEGRADE TO NEUTRAL; IT 327 // DEGRADES TO A FALSE SENSE OF COVERAGE, BECAUSE ITS EXISTENCE IS COUNTED AND ITS VERDICT IS NOT. 328 let ctr: *i64 = gv_ctr() 329 gv_check("sovereign_emu: avail ring published at the QueuePFN-bound ring page, QueueNotify kicked, device consumed the avail head + walked the descriptor + wrote the used ring and bumped used.idx in guest RAM, QueueUsedIdxPeek read-back == used_idx_expected, transcript == golden, clean halt", sov_ok, ctr) 330 // qemu is an EXTERNAL BINARY, not part of the system under test. Zero captured bytes means it never 331 // ran, and scoring that as a FAILED alignment check indicts OUR driver for someone else's absence. 332 var qemu_ran: i64 = 0 333 if g_qemu_bytes > 0 { qemu_ran = 1 } 334 if gv_need("qemu-system-riscv64 produced a transcript (the external cross-check binary must exist to be compared against)", qemu_ran, ctr) == 1 { 335 gv_check("qemu_align: the SAME driver lays the SAME descriptor+avail against a REAL legacy virtio-blk-device and both lanes agree on the VQ prefix", align, ctr) 336 } 337 // ★`tamper_keeps_desc` was ALREADY the silent-on-good control, buried in a flat conjunction where its 338 // purpose was invisible. A whole-transcript collapse satisfies "USED dropped" while proving nothing; 339 // the SURVIVING DESC tail is what makes this tamper DISCRIMINATING rather than merely destructive. 340 var tamper_overfired: i64 = 1 341 if tamper_keeps_desc == 1 { tamper_overfired = 0 } 342 gv_bite("tamper-bite-usedidxpeek: corrupting the UsedIdxPeek-expected constant DROPS the USED canary while the ...VQ DESC tail SURVIVES", tamper_bites, tamper_overfired, ctr) 343 344 // ONE evidence row on EVERY path, same fields either way -- the old shape put the golden in the 345 // GREEN branch and the conjuncts in the RED branch, so the field a reader needed was always in the 346 // branch that did not run. 347 if lfd >= 0 { 348 g_fp(lfd, "USEDGATE runtime=sovereign-emu transport=legacy-virtio-mmio layer=avail-used avail=ring[head]|idx used=ring[id|len]|idx ring=QueuePFN<<12 kick=QueueNotify dma=device-consume+writeback sov_ok=" as *u8); g_fn(lfd, sov_ok) 349 g_fp(lfd, " align_qemu=" as *u8); g_fn(lfd, align) 350 g_fp(lfd, " tamper_bites=" as *u8); g_fn(lfd, tamper_bites) 351 g_fp(lfd, " tamper_keeps_desc=" as *u8); g_fn(lfd, tamper_keeps_desc) 352 g_fp(lfd, " golden=" as *u8); g_fp(lfd, gold) 353 g_fp(lfd, " epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()) 354 g_fp(lfd, "\n" as *u8); sys_close(lfd) 355 } 356 let rc: i64 = gv_verdict("USEDGATE", ctr, "the sovereign rv64 emu drove the avail/used layer end to end: the avail ring was published at the QueuePFN-bound ring page, QueueNotify kicked, the device consumed the avail head, walked the descriptor, wrote the used ring and bumped used.idx in guest RAM, and the driver verified QueueUsedIdxPeek == used_idx_expected -- with a qemu cross-check agreeing on the VQ prefix and the UsedIdxPeek tamper rejected") 357 sys_exit(rc) 358 return rc 359}