code wiki / _hdl_build / _nndev_gate.nx

_nndev_gate.nx source

↩ module page · 196 lines · 11147 B

1// _nndev_gate.nx -- gate for the SOVEREIGN-DEVICE-PROTOCOL exceed (Nishi-native device, NNDP). NO mocks. 2// 3// (1) NATIVE WORKS -- emits the native driver via the SAME nx_drv_proto_emit (the native device is 4// just another op-list spec -> the emitter is protocol-general, not virtio-specific), runs it on 5// the SOVEREIGN rv64 emu against the real NNDP device model, and asserts the serial CONTAINS the 6// golden "NNDENACMDOKDAT" + a clean halt. "DAT" appears ONLY if the device DMA-read the data 7// word the driver wrote (via the inline command descriptor's addr binding) and the driver read 8// RESULT back == that word -- a real data round-trip, not faked. 9// (2) MEASURED EXCEED (the no-wave head-to-head) -- runs the native driver AND the virtio-blk driver 10// for the SAME block-I/O round-trip on the SAME emu and compares emu STEPS (instructions to 11// complete one I/O). Asserts native_steps < virtio_steps -- the lean native protocol (self- 12// describing identity + single-step enable + ONE inline descriptor + ONE doorbell, direct 13// completion) genuinely beats legacy virtio-MMIO (4-stage handshake + split virtqueue + two 14// kicks + used-ring walk). Apples-to-apples: same substrate, same workload. 15// (3) TAMPER x2 on the native image -- bump the device-base lui imm (byte 7) and the magic-expected 16// const (byte 15); each must drop the golden (proves the driver really talks to the device + the 17// verify logic is real, not a rubber stamp). 18// 19// Evidence -> knowledge/status/nndev.log (NNDEVGATE row). Sovereign. license_tier: ORIGINAL 20import "nx_syscalls.nx" 21import "nx_gate_verdict.nx" 22 23const N_EMIT: *u8 = "_offc/nx_drv_proto_emit.elf" 24const N_SOV: *u8 = "_offc/nx_boot_run_sov.elf" 25const N_NSPEC: *u8 = "knowledge/specs/drv_proto_nndp_virt.spec" 26const N_VSPEC: *u8 = "knowledge/specs/drv_proto_blk_virt.spec" 27const N_NBIN: *u8 = "runtime/_hdl_build/_drv_proto_nndp.bin" 28const N_NGOLD: *u8 = "runtime/_hdl_build/_drv_proto_nndp.bin.gold" 29const N_VBIN: *u8 = "runtime/_hdl_build/_drv_proto_blk.bin" 30 31func 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 } 32func 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 } 33func 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 } 34 35func g_run(prog: *u8, a1: *u8, a2: *u8, a3: *u8, outpath: *u8) -> i64 { 36 let pid: i64 = sys_fork() 37 if pid == 0 { 38 if outpath != (0 as *u8) { let ofd: i64 = sys_openat_wr(outpath, 0x1a4); if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } } 39 let argv: *i64 = sys_mmap(64) as *i64 40 argv[0] = prog as i64 41 var k: i64 = 1 42 if a1 != (0 as *u8) { argv[k] = a1 as i64; k = k + 1 } 43 if a2 != (0 as *u8) { argv[k] = a2 as i64; k = k + 1 } 44 if a3 != (0 as *u8) { argv[k] = a3 as i64; k = k + 1 } 45 argv[k] = 0 46 let envp: *i64 = sys_mmap(16) as *i64 47 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0 48 sys_execve(prog, argv, envp) 49 sys_exit(127) 50 } 51 let st: *i64 = sys_mmap(16) as *i64 52 sys_wait4(pid, st, 0) 53 let sig: i64 = st[0] & 0x7f 54 if sig != 0 { return 128 + sig } 55 return (st[0] >> 8) & 0xff 56} 57 58func g_read(path: *u8, buf: *u8, cap: i64) -> i64 { 59 let fd: i64 = sys_openat_rd(path) 60 if fd < 0 { return 0 } 61 var n: i64 = 0 62 var go: i64 = 1 63 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 } } 64 sys_close(fd) 65 return n 66} 67 68func g_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 69 if pl <= 0 { return 0 } 70 var i: i64 = 0 71 while i + pl <= n { var k: i64 = 0; var hit: i64 = 1; while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } if hit == 1 { return 1 } i = i + 1 } 72 return 0 73} 74func g_strlen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n } 75 76// parse the integer after the first "steps=" in buf[0,n); -1 if absent. 77func g_parse_steps(buf: *u8, n: i64) -> i64 { 78 let key: *u8 = "steps=" as *u8 79 let kl: i64 = 6 80 var i: i64 = 0 81 while i + kl <= n { 82 var k: i64 = 0; var hit: i64 = 1 83 while k < kl { if buf[i+k] != key[k] { hit = 0; k = kl } else { k = k + 1 } } 84 if hit == 1 { 85 var p: i64 = i + kl 86 var v: i64 = 0; var any: i64 = 0 87 while p < n { let c: i64 = buf[p] as i64; if c >= 48 { if c <= 57 { v = v*10 + (c-48); any = 1; p = p + 1 } else { p = n } } else { p = n } } 88 if any == 1 { return v } 89 return 0 - 1 90 } 91 i = i + 1 92 } 93 return 0 - 1 94} 95 96// emit a driver from spec, run it on the emu; return steps (or -1), set *ok (golden+halt). 97func g_emit_run(spec: *u8, bin: *u8, gold: *u8, serialpath: *u8, ok: *i64) -> i64 { 98 ok[0] = 0 99 let est: i64 = g_run(N_EMIT, spec, 0 as *u8, 0 as *u8, "/tmp/_nndev_emit.out" as *u8) 100 if est != 0 { return 0 - 1 } 101 let gb: *u8 = sys_mmap(2048) 102 var gn: i64 = 0 103 if gold != (0 as *u8) { gn = g_read(gold, gb, 2048); gb[gn] = 0 as u8 } 104 g_run(N_SOV, bin, 0 as *u8, 0 as *u8, serialpath) 105 let sb: *u8 = sys_mmap(65536) 106 let sn: i64 = g_read(serialpath, sb, 65536) 107 let halt: i64 = g_has(sb, sn, "BOOTSOV verdict=GREEN" as *u8, 21) 108 var golden_ok: i64 = 1 109 if gn > 0 { golden_ok = g_has(sb, sn, gb, gn) } 110 if halt == 1 { if golden_ok == 1 { ok[0] = 1 } } 111 return g_parse_steps(sb, sn) 112} 113 114// run an already-built image (no emit); return steps. 115func g_run_steps(bin: *u8, serialpath: *u8) -> i64 { 116 g_run(N_SOV, bin, 0 as *u8, 0 as *u8, serialpath) 117 let sb: *u8 = sys_mmap(65536) 118 let sn: i64 = g_read(serialpath, sb, 65536) 119 return g_parse_steps(sb, sn) 120} 121 122// tamper: bump native image byte[pos]; run; return 1 iff golden now ABSENT (bites). 123func g_tamper(pos: i64, gold: *u8, gn: i64) -> i64 { 124 let ib: *u8 = sys_mmap(16384) 125 let ibn: i64 = g_read(N_NBIN, ib, 16384) 126 if ibn <= pos { return 0 } 127 ib[pos] = (ib[pos] + 1) as u8 128 let tfd: i64 = sys_openat_wr("/tmp/_nndev_tamper.bin" as *u8, 0x1a4) 129 if tfd < 0 { return 0 } 130 sys_write(tfd, ib, ibn); sys_close(tfd) 131 g_run(N_SOV, "/tmp/_nndev_tamper.bin" as *u8, 0 as *u8, 0 as *u8, "/tmp/_nndev_tamper.txt" as *u8) 132 let sb: *u8 = sys_mmap(65536) 133 let sn: i64 = g_read("/tmp/_nndev_tamper.txt" as *u8, sb, 65536) 134 if g_has(sb, sn, gold, gn) == 0 { return 1 } 135 return 0 136} 137 138func main() -> i64 { 139 g_p("=== sovereign-device-protocol gate (NNDP: Nishi-native device EXCEEDS virtio, measured on the same emu) ===\n" as *u8) 140 let lfd: i64 = sys_openat_append("knowledge/status/nndev.log" as *u8, 0x1a4) 141 142 // (1) native works + native steps 143 let nok: *i64 = sys_mmap(16) as *i64 144 let native_steps: i64 = g_emit_run(N_NSPEC, N_NBIN, N_NGOLD, "/tmp/_nndev_native.txt" as *u8, nok) 145 let native_ok: i64 = nok[0] 146 147 // (2) virtio baseline steps (emit fresh, same workload) 148 let vok: *i64 = sys_mmap(16) as *i64 149 let virtio_steps: i64 = g_emit_run(N_VSPEC, N_VBIN, 0 as *u8, "/tmp/_nndev_virtio.txt" as *u8, vok) 150 151 var exceed: i64 = 0 152 if native_steps > 0 { if virtio_steps > 0 { if native_steps < virtio_steps { exceed = 1 } } } 153 154 // (3) tamper x2 on the native image 155 let gb: *u8 = sys_mmap(2048) 156 let gn: i64 = g_read(N_NGOLD, gb, 2048) 157 let t1: i64 = g_tamper(7, gb, gn) 158 let t2: i64 = g_tamper(15, gb, gn) 159 var tamper_bites: i64 = 0 160 if t1 == 1 { if t2 == 1 { tamper_bites = 1 } } 161 162 g_p(" native_works=" as *u8); if native_ok == 1 { g_p("GREEN(NNDENACMDOKDAT round-trip)" as *u8) } else { g_p("RED" as *u8) } 163 g_p(" native_steps=" as *u8); g_fn(1, native_steps); g_p(" virtio_steps=" as *u8); g_fn(1, virtio_steps) 164 g_p(" exceed=" as *u8); if exceed == 1 { g_p("yes(native<virtio,same emu+workload)" as *u8) } else { g_p("no" as *u8) } 165 g_p(" tamper_bites=" as *u8); if tamper_bites == 1 { g_p("yes\n" as *u8) } else { g_p("no\n" as *u8) } 166 167 // ---- D001 MIGRATION 2026-08-06 -- IDIOM G (boolean conjunction, no counter) ------------------- 168 // Sixth of the family; see _mmu_gate for the reasoning. ONE gv_check PER CONJUNCT creates the 169 // counter idioms A-F assume exists; gv_verdict is GREEN iff pass==total, exactly the old 170 // `native_ok && exceed && tamper_bites`. Teeth unchanged; only the verdict reporter moves. 171 // The gv_* summary is emitted BEFORE the original rich GREEN/RED lines so both the base-class 172 // verdict AND the measured exceed numbers survive -- this gate's whole point is the STEP COUNTS, 173 // and a migration that dropped them would keep the verdict and lose the evidence. 174 let ctr: *i64 = gv_ctr() 175 gv_check("T1 native NNDP device completes a block-I/O round-trip (NNDENACMDOKDAT) on the sovereign emu" as *u8, native_ok, ctr) 176 gv_check("T2 EXCEED: native finishes in fewer emu-steps than legacy virtio-MMIO, same emu and same workload" as *u8, exceed, ctr) 177 gv_check("T3 tamper BITES on both probes -- the round-trip match is load-bearing, not incidental" as *u8, tamper_bites, ctr) 178 let rc__g: i64 = gv_verdict("NNDEVGATE" as *u8, ctr, "the Nishi-NATIVE device protocol completes a block-I/O round-trip in fewer emu-steps than legacy virtio-MMIO on the SAME sovereign emu and SAME workload; native device + driver authored by the SAME nx_drv_proto_emit, so the emitter is protocol-general, not virtio-specific; tamper rejected. keystone=sovereign-device-protocol" as *u8) 179 180 // SINGLE verdict anchor on stdout. The first cut of this migration kept the old hand-rolled 181 // GREEN/RED prints alongside gv_verdict and the probe reported emits_verdict=2 -- TWO verdict= 182 // anchors are worse than none, because a judge cannot tell which one is authoritative. The 183 // measured step counts are NOT lost: they are already on the detail line printed above. 184 // The knowledge/status log rows are preserved verbatim -- the rollup reads that file. 185 if lfd >= 0 { 186 if rc__g == 0 { 187 g_fp(lfd, "NNDEVGATE verdict=GREEN keystone=sovereign-device-protocol probe=nishi-devproto native_steps=" as *u8); g_fn(lfd, native_steps); g_fp(lfd, " virtio_steps=" as *u8); g_fn(lfd, virtio_steps); g_fp(lfd, " exceed=native-fewer-steps-same-emu emitter=protocol-general(same-nx_drv_proto_emit) tamper=rejected epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8) 188 } 189 if rc__g != 0 { 190 g_fp(lfd, "NNDEVGATE verdict=RED native_ok=" as *u8); g_fn(lfd, native_ok); g_fp(lfd, " native_steps=" as *u8); g_fn(lfd, native_steps); g_fp(lfd, " virtio_steps=" as *u8); g_fn(lfd, virtio_steps); g_fp(lfd, " exceed=" as *u8); g_fn(lfd, exceed); 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) 191 } 192 sys_close(lfd) 193 } 194 sys_exit(rc__g) 195 return rc__g 196}