code wiki / _hdl_build / _drv_proto_gate.nx
_drv_proto_gate.nx
buildroot/runtime/_hdl_build/_drv_proto_gate.nx
about
_drv_proto_gate.nx -- the gate for DRIVER-PROTOCOL-FROM-SPEC (X-DRV-W1). NO mocks.
Drives the GENERIC emitter end to end: runs the REAL nx_drv_proto_emit on TWO different driver
SPECS (op-lists), runs EACH emitted image on the SOVEREIGN rv64 emulator (nx_boot_run_sov, with
the legacy virtio-MMIO blk @0x10001000 + net @0x10002000 device models attached), and asserts:
(1) BLK -- spec A (virtio-blk, DeviceID=2) drives the FULL register/ring/irq transaction
(handshake -> queue config -> descriptor lay -> avail/used ring -> status writeback ->
sector-data round-trip): the captured serial CONTAINS golden A + the emu reports a clean
SiFive-finisher halt. The device genuinely DMA-walked the ring the driver laid (the driver
verifies QueueDescPeek/UsedIdxPeek/StatPeek/SectPeek read-backs), so a stuck device cannot
fake it.
(2) NET -- spec B (virtio-net, DeviceID=1) drives a DIFFERENT op-list against a DIFFERENT
device class: serial CONTAINS golden B + clean halt.
(3) DISTINCT -- golden A != golden B AND both non-empty, BOTH authored by the SAME emitter
binary. Two different op-lists -> two different working drivers proves the protocol STATE
MACHINE is synthesized FROM THE SPEC, not a fixed virtio-blk template (the no-false-green
keystone: a fixed template could not produce two distinct device-class drivers).
(4) TAMPER -- two independent corruptions of the BLK image, each must drop golden A:
t1: bump the device-base lui immediate (byte 7) -> all MMIO reads target a non-device
address -> the identity verify fails -> the whole transcript collapses (proves the
driver REALLY talks to the device at the spec's base; a no-op driver would be immune).
t2: bump the magic-EXPECTED constant (byte 15, the first verify's li high byte) -> the
identity verify mismatches -> transcript collapses (proves the VERIFY logic is real,
not a rubber stamp).
Evidence -> knowledge/status/driver_spec.log (DRVPROTOGATE row; the queue row's ||MARK= reads
it). Sovereign orchestration (fork/dup3/execve/wait4), no gcc/.sh. license_tier: ORIGINAL
dependencies 3 imports · 0 importers
imports: nx_syscalls.nxnx_gate_verdict.nxnx_ctxtop_lib.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| 36 | const EMIT_ELF: *u8 = "_offc/nx_drv_proto_emit.elf" |
| 37 | const SOV_ELF: *u8 = "_offc/nx_boot_run_sov.elf" |
functions
| 39 | func 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 } |
| 40 | func 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 } |
| 41 | func 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 } |
| 44 | func g_run1(prog: *u8, a1: *u8, outpath: *u8) -> i64 |
| 67 | func g_read(path: *u8, buf: *u8, cap: i64) -> i64 |
| 78 | func g_find(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 |
| 90 | func g_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 |
| 101 | func g_device_len(buf: *u8, n: i64) -> i64 |
| 107 | func g_strlen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n } called by 1: main |
| 110 | func g_streq(a: *u8, b: *u8) -> i64 called by 1: main |
| 125 | func g_er_reason(c: i64) -> *u8 called by 1: main |
| 142 | func g_emit_run(spec: *u8, out: *u8, goldout: *u8, gbuf: *u8, gcap: i64, serialpath: *u8, emitlog: *u8) -> i64 |
| 181 | func g_tamper(srcbin: *u8, pos: i64, golden: *u8, gn: i64, tampbin: *u8, serialpath: *u8) -> i64 |
| 206 | func g_dump_serial(label: *u8, path: *u8) -> i64 |
| 214 | func main() -> i64 |