code wiki / _hdl_build / _k_r2_001c1_gate.nx
`_k_r2_001c1_gate.nx` source

↩ module page · 307 lines · 15816 B
1// _k_r2_001c1_gate.nx -- the K-R2-001c1 gate (virtio-NET MMIO transport HANDSHAKE, the
2// SECOND virtio device).  Clones the K-R2-001a blk handshake gate but drives the net
3// (DeviceID=1) device block carved into the sovereign sim at base 0x10002000.  NO mocks:
4// runs the REAL nx_virtio_hs_emit (the SAME emitter the blk b-series uses -- data-only on
5// the net spec's base/device-id/banner, so it stays byte-for-byte backward-compatible),
6// then RUNS the emitted image on the SOVEREIGN rv64 emulator (rv64im_min_sim + the second
7// rv64im_min_virtio net block at 0x10002000 -- the PRIMARY, gating lane: Nishi owns the
8// runtime) and asserts the captured serial transcript CONTAINS the emitter's golden
9// ("VNET ACK DRV FEAT OK\n" -- the driver verified magic/version/device-id==1, drove Status
10// through ACK/DRIVER/FEATURES_OK/DRIVER_OK, read HostFeatures, wrote GuestFeatures, re-read
11// Status to confirm FEATURES_OK stuck) AND the sovereign emu reports a clean SiFive-finisher
12// halt.  The blk device at 0x10001000 is left BYTE-UNTOUCHED (its own gate, _k_r2_001a, still
13// passes -- proven by the regression re-run alongside this gate).
14//
15// Then the ALIGNMENT lane: qemu-system-riscv64 -machine virt -global
16// virtio-mmio.force-legacy=true with a REAL virtio-blk-device (first) + a REAL
17// virtio-net-device (second).  qemu fills its virtio-mmio slots in REVERSE, so the first
18// device (blk) lands at the highest slot 0x10008000 and the SECOND device (net) lands at the
19// next slot DOWN, 0x10007000.  The gate authors a SECOND net image from a derived spec whose
20// base = the qemu net slot 0x10007000 and runs THAT on qemu; the SAME handshake driver
21// completes against the REAL legacy virtio-net transport and emits the SAME golden transcript
22// -> lanes AGREE on the handshake (alignment = handshake-completes-on-real-hw, transcript-
23// identical against a real qemu virtio-net-device).
24//
25// Finally a TAMPER test: corrupt the net device-id-EXPECTED constant in the sovereign image ->
26// the driver's device-id verify fails (actual=1 != corrupted-expected) -> it branches PAST the
27// whole handshake straight to the finisher -> the transcript loses its golden -> the gate MUST
28// go RED (proves the gate bites, not a rubber stamp).  The device-id-expected li is encoded as
29// lui t4,0 + addi t4,t4,1 over image words 11-12; its addi immediate high byte is image byte 51
30// -- bumping it changes the expected away from 1 (verified: byte51 0x00->0x01 -> expected 17).
31// Evidence -> knowledge/status/virtio_net.log (NETHSGATE row; the queue row's ||MARK= reads it).
32// Sovereign orchestration (fork/dup3/execve/wait4).  license_tier: ORIGINAL
33import "nx_syscalls.nx"
34import "nx_gate_verdict.nx"
35
36const G_QEMU_BASE: i64 = 0x10007000   // the slot qemu-virt assigns the SECOND device (net)
37const G_TAMPER_BYTE: i64 = 51         // image byte of the net device-id-expected addi immediate high
38
39func 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 }
40func 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 }
41func 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 }
42
43// run nx_virtio_hs_emit <spec>; return child wait status (0 = ok)
44func g_run_emit(spec: *u8) -> i64 {
  let pid: i64 = sys_fork()
  if pid == 0 {
      let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4)
      if dn >= 0 { sys_dup3(dn, 1, 0) }
      let argv: *i64 = sys_mmap(32) as *i64
      argv[0] = "_offc/nx_virtio_hs_emit.elf" as *u8 as i64
      argv[1] = spec as i64
      argv[2] = 0
      let envp: *i64 = sys_mmap(16) as *i64
      envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64
      envp[1] = 0
      sys_execve("_offc/nx_virtio_hs_emit.elf" as *u8, argv, envp)
      sys_exit(127)
  }
  let st: *i64 = sys_mmap(16) as *i64
  sys_wait4(pid, st, 0)
  return st[0]
62}
63
64// run the SOVEREIGN rv64 emulator on binpath; serial -> outpath; return wait status
65func g_run_sov(binpath: *u8, outpath: *u8) -> i64 {
  let pid: i64 = sys_fork()
  if pid == 0 {
      let ofd: i64 = sys_openat_wr(outpath, 0x1a4)
      if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) }
      let argv: *i64 = sys_mmap(32) as *i64
      argv[0] = "_offc/nx_boot_run_sov.elf" as *u8 as i64
      argv[1] = binpath as i64
      argv[2] = 0
      let envp: *i64 = sys_mmap(16) as *i64
      envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64
      envp[1] = 0
      sys_execve("_offc/nx_boot_run_sov.elf" as *u8, argv, envp)
      sys_exit(127)
  }
  let st: *i64 = sys_mmap(16) as *i64
  sys_wait4(pid, st, 0)
  return st[0]
83}
84
85// run qemu-system-riscv64 virt + legacy virtio-blk-device (first) + virtio-net-device
86// (second) on binpath; serial -> outpath.  The net device lands at qemu reverse slot
87// 0x10007000 (blk takes the top slot 0x10008000); the derived-base net image targets that
88// slot.  The blk backing image must exist; the gate creates it first via g_make_backing.
89func g_run_qemu(binpath: *u8, outpath: *u8, backing: *u8) -> i64 {
  let pid: i64 = sys_fork()
  if pid == 0 {
      let ofd: i64 = sys_openat_wr(outpath, 0x1a4)
      if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) }
      let argv: *i64 = sys_mmap(128) as *i64
      argv[0] = "/usr/bin/qemu-system-riscv64" as *u8 as i64
      argv[1] = "-machine" as *u8 as i64
      argv[2] = "virt" as *u8 as i64
      argv[3] = "-global" as *u8 as i64
      argv[4] = "virtio-mmio.force-legacy=true" as *u8 as i64
      argv[5] = "-nographic" as *u8 as i64
      argv[6] = "-bios" as *u8 as i64
      argv[7] = binpath as i64
      argv[8] = "-drive" as *u8 as i64
      argv[9] = "file=/tmp/_vnetgate_backing.img,if=none,format=raw,id=hd0" as *u8 as i64
      argv[10] = "-device" as *u8 as i64
      argv[11] = "virtio-blk-device,drive=hd0" as *u8 as i64
      argv[12] = "-device" as *u8 as i64
      argv[13] = "virtio-net-device" as *u8 as i64
      argv[14] = 0
      let envp: *i64 = sys_mmap(16) as *i64
      envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64
      envp[1] = 0
      sys_execve("/usr/bin/qemu-system-riscv64" as *u8, argv, envp)
      sys_exit(127)
  }
  let st: *i64 = sys_mmap(16) as *i64
  sys_wait4(pid, st, 0)
  return st[0]
119}
120
121// create a small raw backing file for the qemu virtio-blk device (4 sectors of zeros).
122func g_make_backing(path: *u8) -> i64 {
  let fd: i64 = sys_openat_wr(path, 0x1a4)
  if fd < 0 { return 0 - 1 }
  let z: *u8 = sys_mmap(2048)
  var i: i64 = 0
  while i < 2048 { z[i] = 0 as u8; i = i + 1 }
  sys_write(fd, z, 2048)
  sys_close(fd)
  return 0
131}
132
133// read whole file into buf (cap-1 max); return byte count (0 if absent)
134func g_read(path: *u8, buf: *u8, cap: i64) -> i64 {
  let fd: i64 = sys_openat_rd(path)
  if fd < 0 { return 0 }
  var n: i64 = 0
  var go: i64 = 1
  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 } }
  sys_close(fd)
  return n
142}
143
144// does buf[0,n) contain pat (length pl)?  1/0
145func g_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 {
  if pl <= 0 { return 0 }
  var i: i64 = 0
  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
  }
  return 0
156}
157
158func g_strlen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
159
160// does line [ls,le) of buf begin with key?  1/0
161func g_line_is(buf: *u8, ls: i64, le: i64, key: *u8) -> i64 {
  var k: i64 = 0
  while key[k] != (0 as u8) {
      if ls + k >= le { return 0 }
      if buf[ls + k] != key[k] { return 0 }
      k = k + 1
  }
  return 1
169}
170
171// author the qemu-alignment spec: copy the main net spec, but replace the `base ` line value
172// with G_QEMU_BASE (the qemu net reverse-slot 0x10007000) and the `out ` line with the qemu
173// image path.  Writes derived spec.
174func g_write_qemu_spec(mainspec: *u8, derived: *u8, qemu_out: *u8) -> i64 {
  let buf: *u8 = sys_mmap(8192)
  let n: i64 = g_read(mainspec, buf, 8192)
  if n <= 0 { return 0 - 1 }
  let ofd: i64 = sys_openat_wr(derived, 0x1a4)
  if ofd < 0 { return 0 - 1 }
  var ls: i64 = 0
  while ls < n {
      var le: i64 = ls
      var scan: i64 = 1
      while scan == 1 { if le >= n { scan = 0 } else { if buf[le] == (10 as u8) { scan = 0 } else { le = le + 1 } } }
      // [ls,le) is one line (without newline).  Rewrite base/out lines.
      if g_line_is(buf, ls, le, "base " as *u8) == 1 {
          g_fp(ofd, "base 0x10007000\n" as *u8)
      } else {
          if g_line_is(buf, ls, le, "out " as *u8) == 1 {
              g_fp(ofd, "out " as *u8); g_fp(ofd, qemu_out); g_fp(ofd, "\n" as *u8)
          } else {
              sys_write(ofd, (buf as i64 + ls) as *u8, le - ls)
              g_fp(ofd, "\n" as *u8)
          }
      }
      ls = le + 1
  }
  sys_close(ofd)
  return 0
200}
201
202func main() -> i64 {
  let spec: *u8 = "knowledge/specs/virtio_net_handshake_virt.spec" as *u8
  let binpath: *u8 = "runtime/_hdl_build/_virtio_net_hs_virt.bin" as *u8
  let goldpath: *u8 = "runtime/_hdl_build/_virtio_net_hs_virt.bin.gold" as *u8
  let qemu_spec: *u8 = "/tmp/_vnetgate_qemu.spec" as *u8
  let qemu_bin: *u8 = "/tmp/_vnetgate_qemu.bin" as *u8
  let backing: *u8 = "/tmp/_vnetgate_backing.img" as *u8
  let tamper_bin: *u8 = "/tmp/_vnetgate_tamper.bin" as *u8
  let sov_serial: *u8 = "/tmp/_vnetgate_sov.txt" as *u8
  let qemu_serial: *u8 = "/tmp/_vnetgate_qemu.txt" as *u8
  let sov_tamper: *u8 = "/tmp/_vnetgate_sov_tamper.txt" as *u8
  g_p("=== virtio-NET MMIO handshake gate (K-R2-001c1: SOVEREIGN rv64 net transport @0x10002000 + qemu virtio-net-device alignment @0x10007000) ===\n" as *u8)
214
  let lfd: i64 = sys_openat_append("knowledge/status/virtio_net.log" as *u8, 0x1a4)
216
  // STEP 1: author the SOVEREIGN net handshake image (base 0x10002000) + the golden transcript.
  let est: i64 = g_run_emit(spec)
  if est != 0 {
      g_p("NETHSGATE verdict=RED reason=emit-failed\n" as *u8)
      if lfd >= 0 { g_fp(lfd, "NETHSGATE verdict=RED reason=emit-failed\n" as *u8); sys_close(lfd) }
      sys_exit(1); return 1
  }
  let gold: *u8 = sys_mmap(512)
  let gn: i64 = g_read(goldpath, gold, 512)
  gold[gn] = 0 as u8
  if gn <= 0 {
      g_p("NETHSGATE verdict=RED reason=golden-missing\n" as *u8)
      if lfd >= 0 { g_fp(lfd, "NETHSGATE verdict=RED reason=golden-missing\n" as *u8); sys_close(lfd) }
      sys_exit(1); return 1
  }
232
  // STEP 2 (PRIMARY): the Nishi sovereign rv64 emulator RUNS the net handshake image.
  let sst: i64 = g_run_sov(binpath, sov_serial)
  let sbuf: *u8 = sys_mmap(65536)
  let sbn: i64 = g_read(sov_serial, sbuf, 65536)
  let trans_ok: i64 = g_buf_has(sbuf, sbn, gold, gn)                 // serial CONTAINS golden
  let halt_ok: i64 = g_buf_has(sbuf, sbn, "BOOTSOV verdict=GREEN" as *u8, 21)
  var sov_ok: i64 = 0
  if sst == 0 { if trans_ok == 1 { if halt_ok == 1 { sov_ok = 1 } } }
241
  // STEP 3 (ALIGNMENT): author the qemu-base net image (slot 0x10007000) + run qemu with a
  // REAL legacy virtio-blk-device (first) + virtio-net-device (second); assert the SAME golden
  // transcript appears (lanes agree on the net handshake against real qemu virtio-net hw).
  g_make_backing(backing)
  g_write_qemu_spec(spec, qemu_spec, qemu_bin)
  let qest: i64 = g_run_emit(qemu_spec)
  var align: i64 = 0
  if qest == 0 {
      let qst: i64 = g_run_qemu(qemu_bin, qemu_serial, backing)
      let qbuf: *u8 = sys_mmap(65536)
      let qbn: i64 = g_read(qemu_serial, qbuf, 65536)
      let qtrans: i64 = g_buf_has(qbuf, qbn, gold, gn)
      if qst == 0 { if qtrans == 1 { align = 1 } }
  }
256
  // STEP 4 (TAMPER): corrupt the net device-id-EXPECTED constant in the sovereign image.  The
  // device-id-expected li is lui t4,0 + addi t4,t4,1 over image words 11-12; the addi immediate
  // high byte is image byte G_TAMPER_BYTE (51).  Bumping it changes the expected away from 1, so
  // the device-id verify (bne t3,t4) fails (actual device-id 1 != corrupted expected) -> the
  // driver jumps to the finisher -> the transcript loses its golden.  Gate MUST then go RED.
  let ibuf: *u8 = sys_mmap(8192)
  let ibn: i64 = g_read(binpath, ibuf, 8192)
  ibuf[G_TAMPER_BYTE] = (ibuf[G_TAMPER_BYTE] + 1) as u8
  let tfd: i64 = sys_openat_wr(tamper_bin, 0x1a4)
  if tfd >= 0 { sys_write(tfd, ibuf, ibn); sys_close(tfd) }
  let tst: i64 = g_run_sov(tamper_bin, sov_tamper)
  let tbuf: *u8 = sys_mmap(65536)
  let tbn: i64 = g_read(sov_tamper, tbuf, 65536)
  let tamper_trans: i64 = g_buf_has(tbuf, tbn, gold, gn)             // should now MISS
  var tamper_bites: i64 = 0
  if tamper_trans == 0 { tamper_bites = 1 }
273
  g_p("  sovereign_emu=" as *u8)
  if sov_ok == 1 { g_p("GREEN(transcript==golden+clean-halt)" as *u8) } else { g_p("RED" as *u8) }
  g_p(" qemu_align=" as *u8)
  if align == 1 { g_p("yes(real-virtio-net @0x10007000)" as *u8) } else { g_p("no" as *u8) }
  g_p(" tamper_bites=" as *u8)
  if tamper_bites == 1 { g_p("yes\n" as *u8) } else { g_p("no\n" as *u8) }
280
  // ---- D001 MIGRATION 2026-08-06 -- IDIOM G (boolean conjunction, no counter) -------------------
  // Seventh of the family; see _mmu_gate for the reasoning. ONE gv_check PER CONJUNCT creates the
  // counter idioms A-F assume exists; gv_verdict is GREEN iff pass==total, exactly the old
  // `sov_ok && align && tamper_bites`. Teeth unchanged; only the verdict reporter moves.
  // SINGLE verdict anchor on stdout (the _nndev_gate lesson: emits_verdict=2 is worse than none).
  // The knowledge/status log rows are preserved verbatim, golden transcript included.
  let ctr: *i64 = gv_ctr()
  gv_check("T1 sovereign rv64 emu drives the virtio-NET transport handshake @0x10002000 (ACK|DRIVER|FEATURES_OK|DRIVER_OK, transcript == golden, clean halt)" as *u8, sov_ok, ctr)
  gv_check("T2 qemu virtio-net-device cross-check @0x10007000 AGREES -- an INDEPENDENT implementation reaches the same transcript" as *u8, align, ctr)
  gv_check("T3 tamper BITES (device-id-expected immediate mutated) -- the transcript match is load-bearing, not incidental" as *u8, tamper_bites, ctr)
  let rc__g: i64 = gv_verdict("NETHSGATE" as *u8, ctr, "sovereign rv64 emu drove the virtio-NET transport handshake @0x10002000; transcript == golden; clean halt; qemu virtio-net-device cross-check @0x10007000 AGREES; tamper REJECTED; blk @0x10001000 untouched" as *u8)
  if lfd >= 0 {
      if rc__g == 0 {
          g_fp(lfd, "NETHSGATE verdict=GREEN runtime=sovereign-emu transport=legacy-virtio-mmio device=virtio-net device-id=1 net_base=0x10002000 handshake=ACK|DRIVER|FEATURES_OK|DRIVER_OK transcript==golden align_qemu=yes(virtio-net-device@0x10007000) tamper=rejected blk=untouched golden=" as *u8)
          g_fp(lfd, gold)
          g_fp(lfd, " epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8)
      }
      if rc__g != 0 {
          g_fp(lfd, "NETHSGATE verdict=RED sov_ok=" as *u8); g_fn(lfd, sov_ok)
          g_fp(lfd, " align=" as *u8); g_fn(lfd, align)
          g_fp(lfd, " tamper_bites=" as *u8); g_fn(lfd, tamper_bites); g_fp(lfd, "\n" as *u8)
      }
      sys_close(lfd)
  }
  sys_exit(rc__g)
  return rc__g
307}
_k_r2_001c1_gate.nx source

`_k_r2_001c1_gate.nx` source
