_drv_proto_gate.nx source

1// _drv_proto_gate.nx -- the gate for DRIVER-PROTOCOL-FROM-SPEC (X-DRV-W1). NO mocks. 2// 3// Drives the GENERIC emitter end to end: runs the REAL nx_drv_proto_emit on TWO different driver 4// SPECS (op-lists), runs EACH emitted image on the SOVEREIGN rv64 emulator (nx_boot_run_sov, with 5// the legacy virtio-MMIO blk @0x10001000 + net @0x10002000 device models attached), and asserts: 6// 7// (1) BLK -- spec A (virtio-blk, DeviceID=2) drives the FULL register/ring/irq transaction 8// (handshake -> queue config -> descriptor lay -> avail/used ring -> status writeback -> 9// sector-data round-trip): the captured serial CONTAINS golden A + the emu reports a clean 10// SiFive-finisher halt. The device genuinely DMA-walked the ring the driver laid (the driver 11// verifies QueueDescPeek/UsedIdxPeek/StatPeek/SectPeek read-backs), so a stuck device cannot 12// fake it. 13// (2) NET -- spec B (virtio-net, DeviceID=1) drives a DIFFERENT op-list against a DIFFERENT 14// device class: serial CONTAINS golden B + clean halt. 15// (3) DISTINCT -- golden A != golden B AND both non-empty, BOTH authored by the SAME emitter 16// binary. Two different op-lists -> two different working drivers proves the protocol STATE 17// MACHINE is synthesized FROM THE SPEC, not a fixed virtio-blk template (the no-false-green 18// keystone: a fixed template could not produce two distinct device-class drivers). 19// (4) TAMPER -- two independent corruptions of the BLK image, each must drop golden A: 20// t1: bump the device-base lui immediate (byte 7) -> all MMIO reads target a non-device 21// address -> the identity verify fails -> the whole transcript collapses (proves the 22// driver REALLY talks to the device at the spec's base; a no-op driver would be immune). 23// t2: bump the magic-EXPECTED constant (byte 15, the first verify's li high byte) -> the 24// identity verify mismatches -> transcript collapses (proves the VERIFY logic is real, 25// not a rubber stamp). 26// 27// Evidence -> knowledge/status/driver_spec.log (DRVPROTOGATE row; the queue row's ||MARK= reads 28// it). Sovereign orchestration (fork/dup3/execve/wait4), no gcc/.sh. license_tier: ORIGINAL 29import "nx_syscalls.nx" 30 31const EMIT_ELF: *u8 = "_offc/nx_drv_proto_emit.elf" 32const SOV_ELF: *u8 = "_offc/nx_boot_run_sov.elf" 33 34func 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 } 35func 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 } 36func g_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 prog with one arg (a1, may be null); serial/stdout -> outpath; return WEXITSTATUS (or 128+sig). 39func g_run1(prog: *u8, a1: *u8, outpath: *u8) -> i64 { 40 let pid: i64 = sys_fork() 41 if pid == 0 { 42 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 43 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 44 let argv: *i64 = sys_mmap(32) as *i64 45 argv[0] = prog as i64 46 var k: i64 = 1 47 if a1 != (0 as *u8) { argv[k] = a1 as i64; k = k + 1 } 48 argv[k] = 0 49 let envp: *i64 = sys_mmap(16) as *i64 50 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0 51 sys_execve(prog, argv, envp) 52 sys_exit(127) 53 } 54 let st: *i64 = sys_mmap(16) as *i64 55 sys_wait4(pid, st, 0) 56 let sig: i64 = st[0] & 0x7f 57 if sig != 0 { return 128 + sig } 58 return (st[0] >> 8) & 0xff 59} 60 61// read whole file into buf (cap-1 max); return byte count (0 if absent). 62func g_read(path: *u8, buf: *u8, cap: i64) -> i64 { 63 let fd: i64 = sys_openat_rd(path) 64 if fd < 0 { return 0 } 65 var n: i64 = 0 66 var go: i64 = 1 67 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 } } 68 sys_close(fd) 69 return n 70} 71 72// does buf[0,n) contain pat (length pl)? 1/0 73func g_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 74 if pl <= 0 { return 0 } 75 var i: i64 = 0 76 while i + pl <= n { 77 var k: i64 = 0; var hit: i64 = 1 78 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } 79 if hit == 1 { return 1 } 80 i = i + 1 81 } 82 return 0 83} 84 85func g_strlen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n } 86 87// are two NUL-terminated strings equal? 1/0 88func g_streq(a: *u8, b: *u8) -> i64 { 89 var i: i64 = 0 90 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 } 91 if b[i] != (0 as u8) { return 0 } 92 return 1 93} 94 95// emit a driver from spec, run it on the sovereign emu; return 1 iff serial CONTAINS golden + 96// clean SiFive halt. golden read from <out>.gold; out path passed in. serialpath = scratch. 97func g_emit_run(spec: *u8, out: *u8, goldout: *u8, gbuf: *u8, gcap: i64, serialpath: *u8) -> i64 { 98 let est: i64 = g_run1(EMIT_ELF, spec, "/tmp/_drvproto_emit.out" as *u8) 99 if est != 0 { return 0 } 100 let gn: i64 = g_read(goldout, gbuf, gcap) 101 if gn <= 0 { return 0 } 102 gbuf[gn] = 0 as u8 103 let rst: i64 = g_run1(SOV_ELF, out, serialpath) 104 let sbuf: *u8 = sys_mmap(65536) 105 let sbn: i64 = g_read(serialpath, sbuf, 65536) 106 let has: i64 = g_buf_has(sbuf, sbn, gbuf, gn) 107 let halt: i64 = g_buf_has(sbuf, sbn, "BOOTSOV verdict=GREEN" as *u8, 21) 108 if rst == 0 { if has == 1 { if halt == 1 { return 1 } } } 109 return 0 110} 111 112// run the BLK image with byte[pos] bumped by 1; return 1 iff golden A is now ABSENT (tamper bites). 113func g_tamper(srcbin: *u8, pos: i64, golden: *u8, gn: i64, tampbin: *u8, serialpath: *u8) -> i64 { 114 let ibuf: *u8 = sys_mmap(16384) 115 let ibn: i64 = g_read(srcbin, ibuf, 16384) 116 if ibn <= pos { return 0 } 117 ibuf[pos] = (ibuf[pos] + 1) as u8 118 let tfd: i64 = sys_openat_wr(tampbin, 0x1a4) 119 if tfd < 0 { return 0 } 120 sys_write(tfd, ibuf, ibn); sys_close(tfd) 121 let rst: i64 = g_run1(SOV_ELF, tampbin, serialpath) 122 let sbuf: *u8 = sys_mmap(65536) 123 let sbn: i64 = g_read(serialpath, sbuf, 65536) 124 let has: i64 = g_buf_has(sbuf, sbn, golden, gn) 125 if has == 0 { return 1 } // golden gone -> tamper bites 126 return 0 127} 128 129func main() -> i64 { 130 g_p("=== driver-protocol-from-spec gate (X-DRV-W1: op-list spec -> emitted rv64 driver -> real virtio device on sovereign emu) ===\n" as *u8) 131 let lfd: i64 = sys_openat_append("knowledge/status/driver_spec.log" as *u8, 0x1a4) 132 133 let blk_out: *u8 = "runtime/_hdl_build/_drv_proto_blk.bin" as *u8 134 let blk_gold: *u8 = "runtime/_hdl_build/_drv_proto_blk.bin.gold" as *u8 135 let net_out: *u8 = "runtime/_hdl_build/_drv_proto_net.bin" as *u8 136 let net_gold: *u8 = "runtime/_hdl_build/_drv_proto_net.bin.gold" as *u8 137 138 let gA: *u8 = sys_mmap(2048) 139 let gB: *u8 = sys_mmap(2048) 140 141 // (1) BLK full register/ring/irq transaction on the sovereign emu. 142 let blk_ok: i64 = g_emit_run("knowledge/specs/drv_proto_blk_virt.spec" as *u8, blk_out, blk_gold, gA, 2048, "/tmp/_drvproto_blk_serial.txt" as *u8) 143 // (2) NET handshake (different device class, DeviceID=1) on the sovereign emu. 144 let net_ok: i64 = g_emit_run("knowledge/specs/drv_proto_net_virt.spec" as *u8, net_out, net_gold, gB, 2048, "/tmp/_drvproto_net_serial.txt" as *u8) 145 146 // (3) DISTINCT: two op-lists -> two different drivers (same emitter binary). 147 var distinct: i64 = 0 148 if g_strlen(gA) > 0 { if g_strlen(gB) > 0 { if g_streq(gA, gB) == 0 { distinct = 1 } } } 149 150 // (4) TAMPER x2 on the BLK image: device-base lui imm (byte 7) + magic-expected li high (byte 15). 151 let gAn: i64 = g_strlen(gA) 152 let t1: i64 = g_tamper(blk_out, 7, gA, gAn, "/tmp/_drvproto_t1.bin" as *u8, "/tmp/_drvproto_t1.txt" as *u8) 153 let t2: i64 = g_tamper(blk_out, 15, gA, gAn, "/tmp/_drvproto_t2.bin" as *u8, "/tmp/_drvproto_t2.txt" as *u8) 154 var tamper_bites: i64 = 0 155 if t1 == 1 { if t2 == 1 { tamper_bites = 1 } } 156 157 g_p(" blk_full_txn=" as *u8) 158 if blk_ok == 1 { g_p("GREEN(VIO..SECT: handshake+queue+descriptor+avail/used+status+sector roundtrip, clean halt)" as *u8) } else { g_p("RED" as *u8) } 159 g_p(" net_handshake=" as *u8) 160 if net_ok == 1 { g_p("GREEN(NET..RUN: DeviceID=1 @0x10002000, clean halt)" as *u8) } else { g_p("RED" as *u8) } 161 g_p(" distinct=" as *u8) 162 if distinct == 1 { g_p("yes(goldenA!=goldenB, same emitter binary)" as *u8) } else { g_p("no" as *u8) } 163 g_p(" tamper_bites=" as *u8) 164 if tamper_bites == 1 { g_p("yes(base-imm + magic-const corrupt -> golden drops)\n" as *u8) } else { g_p("no\n" as *u8) } 165 166 var pass: i64 = 0 167 if blk_ok == 1 { if net_ok == 1 { if distinct == 1 { if tamper_bites == 1 { pass = 1 } } } } 168 169 if pass == 1 { 170 g_p("DRVPROTOGATE verdict=GREEN (the GENERIC nx_drv_proto_emit synthesized a full virtio-blk register/ring/irq driver AND a virtio-net handshake driver from two op-list SPECS; BOTH completed against the real device models on the sovereign rv64 emu with clean halts; the protocol state machine is DATA-driven [distinct device classes from distinct op-lists]; two independent BLK tampers REJECTED -- driver-from-spec, author=emitter)\n" as *u8) 171 if lfd >= 0 { 172 g_fp(lfd, "DRVPROTOGATE verdict=GREEN keystone=driver-protocol-from-spec composes=emitter-of-emitters+HWMAP runtime=sovereign-emu transport=legacy-virtio-mmio blk_full_txn=VIO..SECT net_handshake=NET..RUN goldenA=" as *u8) 173 g_fp(lfd, gA); g_fp(lfd, " goldenB=" as *u8); g_fp(lfd, gB) 174 g_fp(lfd, " distinct=yes tamper=rejected(base-imm+magic-const) epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8); sys_close(lfd) 175 } 176 sys_exit(0); return 0 177 } 178 g_p("DRVPROTOGATE verdict=RED (blk_ok/net_ok/distinct/tamper not all green)\n" as *u8) 179 if lfd >= 0 { 180 g_fp(lfd, "DRVPROTOGATE verdict=RED blk_ok=" as *u8); g_fn(lfd, blk_ok) 181 g_fp(lfd, " net_ok=" as *u8); g_fn(lfd, net_ok) 182 g_fp(lfd, " distinct=" as *u8); g_fn(lfd, distinct) 183 g_fp(lfd, " t1=" as *u8); g_fn(lfd, t1); g_fp(lfd, " t2=" as *u8); g_fn(lfd, t2); g_fp(lfd, "\n" as *u8); sys_close(lfd) 184 } 185 sys_exit(1) 186 return 1 187}