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

↩ module page · 369 lines · 20326 B
1// _k_r2_001b3_gate.nx -- the K-R2-001b3 gate (virtio-MMIO SECTOR-DATA ROUND-TRIP layer; the
2// fifth slice of the K-R2-001b virtqueue epic, on top of b2c's status-byte writeback).  Drives
3// the full author->handshake->queue-config->descriptor-DMA->avail/used->status-byte->sector-data
4// chain with NO mocks: runs the REAL nx_virtio_hs_emit (the team AUTHORS the rv64 image + the
5// TABLE-COMPUTED golden transcript from the sector spec), then RUNS the image on the SOVEREIGN
6// rv64 emulator (rv64im_min_sim + the rv64im_min_virtio device now, on the b2b QueueNotify kick,
7// after the used-ring + status-byte writeback, FOLLOWING the consumed descriptor's data pointer
8// (desc[head].addr) into guest RAM, DMA-READING the first 32-bit word of the data buffer the
9// driver placed the sector pattern into + latching it into the QueueSectPeek RO register -- the
10// PRIMARY, gating lane: Nishi owns the runtime) and asserts the captured serial transcript
11// CONTAINS the emitter's golden ("VIO ACK DRV FEAT OK VQ DESC USED STAT SECT\n" -- after the
12// used-ring + status writeback the device read the sector word the driver wrote, the driver READ
13// QueueSectPeek BACK and verified it == sect_data_expected: the sector-data round-trip binding
14// proof) AND the sovereign emu reports a clean SiFive-finisher halt.
15//
16// Then the ALIGNMENT lane: qemu-system-riscv64 -machine virt -global
17// virtio-mmio.force-legacy=true with a REAL virtio-blk-device backing.  The gate authors a
18// SECOND image from a base-rewritten spec (the blk device lands at slot 0x10008000) and runs
19// the SAME driver against the REAL legacy virtio-blk transport: it completes the handshake +
20// queue config, lays the SAME descriptor + the SAME avail ring + the SAME sector word into qemu
21// guest RAM, and kicks the real QueueNotify -- the real legacy transport genuinely walks the
22// ring.  The sovereign-only QueueDescPeek / QueueUsedIdxPeek / QueueStatPeek / QueueSectPeek
23// result registers are model instruments the real device does not expose (they read 0), so on
24// qemu the descriptor-DMA + used-ring + status-byte + sector-data verifies gracefully drop
25// " DESC" / " USED" / " STAT" / " SECT"; the gate asserts the qemu transcript contains the b1
26// prefix golden ("VIO ACK DRV FEAT OK VQ") -- proving the SAME driver lays the avail ring + the
27// sector word + kicks the real device -> lanes AGREE on every register the real transport can
28// observe.
29//
30// Finally a TAMPER test: corrupt the QueueSectPeek-EXPECTED constant in the sovereign image
31// (the driver loads its own QueueSectPeek read-back into t3 via lwu and compares against this
32// li-loaded expected in t4; bumping the expected's immediate makes t3 != t4) -> the read-back
33// verify branches PAST stage 9 straight to the finisher -> the transcript loses ONLY its
34// " SECT" canary (the "VIO ACK DRV FEAT OK VQ DESC USED STAT" tail survives) -> the gate MUST go
35// RED.  Evidence -> knowledge/status/virtio_blk.log (SECTGATE 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 `lwu t3, 0x6C(t2)` -- the QueueSectPeek read-back load (f3=6,
45// zero-extend; the sector word is read unsigned, matching the lui-built expected).  The
46// SectPeek-expected constant the driver compares against is the li that follows it (lui at +4,
47// addi at +8); corrupting the addi's high immediate byte (+11) is the sector-data tamper.
48const G_QSECTPEEK_LOAD_WORD: i64 = 0x06c3ee03   // lwu t3, 0x06C(t2)  (QueueSectPeek 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 {
  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]
73}
74
75// run the SOVEREIGN rv64 emulator on binpath; serial -> outpath; return wait status
76func 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]
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 {
  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/_sectgate_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] = 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]
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 {
  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
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 {
  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
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 {
  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
162}
163
164// read a little-endian 32-bit word from buf at byte offset o.
165func g_w32(buf: *u8, o: i64) -> i64 {
  let b0: i64 = buf[o] as i64
  let b1: i64 = buf[o+1] as i64
  let b2: i64 = buf[o+2] as i64
  let b3: i64 = buf[o+3] as i64
  return b0 | (b1 << 8) | (b2 << 16) | (b3 << 24)
171}
172
173// find the byte offset of the (unique) QueueSectPeek read-back load word in the image; -1
174// if absent.  The SectPeek-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_sectpeek_load(buf: *u8, n: i64) -> i64 {
  var o: i64 = 0
  while o + 4 <= n {
      if g_w32(buf, o) == G_QSECTPEEK_LOAD_WORD { return o }
      o = o + 4
  }
  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 {
  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
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 + status buffer addresses are guest-RAM addresses valid on both lanes -- left
201// as is.)
202func g_write_qemu_spec(mainspec: *u8, derived: *u8, qemu_out: *u8) -> i64 {
  let buf: *u8 = sys_mmap(16384)
  let n: i64 = g_read(mainspec, buf, 16384)
  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 } } }
      if g_line_is(buf, ls, le, "base " as *u8) == 1 {
          g_fp(ofd, "base 0x10008000\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
227}
228
229func main() -> i64 {
  let spec: *u8 = "knowledge/specs/virtio_blk_sector_virt.spec" as *u8
  let binpath: *u8 = "runtime/_hdl_build/_virtio_sector_virt.bin" as *u8
  let goldpath: *u8 = "runtime/_hdl_build/_virtio_sector_virt.bin.gold" as *u8
  let qemu_spec: *u8 = "/tmp/_sectgate_qemu.spec" as *u8
  let qemu_bin: *u8 = "/tmp/_sectgate_qemu.bin" as *u8
  let backing: *u8 = "/tmp/_sectgate_backing.img" as *u8
  let tamper_bin: *u8 = "/tmp/_sectgate_tamper.bin" as *u8
  let sov_serial: *u8 = "/tmp/_sectgate_sov.txt" as *u8
  let qemu_serial: *u8 = "/tmp/_sectgate_qemu.txt" as *u8
  let sov_tamper: *u8 = "/tmp/_sectgate_sov_tamper.txt" as *u8
  // the b1 prefix golden the qemu alignment lane asserts (the real device has none of
  // QueueDescPeek / QueueUsedIdxPeek / QueueStatPeek / QueueSectPeek, so on qemu the
  // descriptor-DMA + used-ring + status-byte + sector-data verifies drop " DESC" / " USED" /
  // " STAT" / " SECT", leaving the b1 prefix the real transport can observe).
  let prefix_gold: *u8 = "VIO ACK DRV FEAT OK VQ" as *u8
  // the b2c "STAT" tail the tamper must KEEP (only " SECT" drops under the sector-data tamper).
  let statonly_gold: *u8 = "VIO ACK DRV FEAT OK VQ DESC USED STAT" as *u8
  g_p("=== virtio-MMIO sector-data gate (K-R2-001b3: SOVEREIGN rv64 device sector-data round-trip + QueueSectPeek read-back + qemu virtio-blk alignment) ===\n" as *u8)
248
  let lfd: i64 = sys_openat_append("knowledge/status/virtio_blk.log" as *u8, 0x1a4)
250
  // STEP 1: author the SOVEREIGN image (base 0x10001000) + the golden transcript.
  let est: i64 = g_run_emit(spec)
  if est != 0 {
      g_p("SECTGATE verdict=RED reason=emit-failed\n" as *u8)
      if lfd >= 0 { g_fp(lfd, "SECTGATE 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("SECTGATE verdict=RED reason=golden-missing\n" as *u8)
      if lfd >= 0 { g_fp(lfd, "SECTGATE verdict=RED reason=golden-missing\n" as *u8); sys_close(lfd) }
      sys_exit(1); return 1
  }
266
  // STEP 2 (PRIMARY): the Nishi sovereign rv64 emulator RUNS the image -- handshake + queue
  // config + descriptor lay (b2a) + avail-ring publish + used-ring writeback (b2b) + status-
  // byte writeback (b2c) + sector-pattern write + sector-data read-back -> transcript must
  // CONTAIN the full golden ("...USED STAT SECT\n").  On the b2b kick the device followed
  // desc[head].addr into guest RAM, DMA-read the first data word the driver placed there +
  // latched it into QueueSectPeek; the driver read QueueSectPeek back + verified == expected.
  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)
  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 } } }
280
  // STEP 3 (ALIGNMENT): author the qemu-base image (slot 0x10008000) + run qemu with a REAL
  // legacy virtio-blk-device; the SAME driver lays the SAME descriptor + the SAME avail ring +
  // the SAME sector word into qemu guest RAM and kicks the real QueueNotify (the real transport
  // walks the ring).  The sovereign-only QueueDescPeek/QueueUsedIdxPeek/QueueStatPeek/
  // QueueSectPeek registers read 0 on the real device, so the descriptor-DMA + used-ring +
  // status-byte + sector-data verifies drop " DESC"/" USED"/" STAT"/" SECT" there; assert the
  // b1 prefix golden ("VIO ACK DRV FEAT OK VQ") appears, proving the driver runs identically
  // against the real transport up to the avail publish + kick.
  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)
      g_qemu_bytes = qbn
      let qtrans: i64 = g_buf_has(qbuf, qbn, prefix_gold, g_strlen(prefix_gold))
      if qst == 0 { if qtrans == 1 { align = 1 } }
  }
301
  // STEP 4 (TAMPER): corrupt the QueueSectPeek-EXPECTED constant in the sovereign image.
  // Scan for the unique QueueSectPeek read-back load word; the expected li the driver
  // compares against is the addi at load+8.  Bump that addi's high immediate byte (load+11)
  // so the expected != the value the device latched -> the read-back verify branches to the
  // finisher -> ONLY the " SECT" canary drops (the "...USED STAT" tail survives) -> gate MUST RED.
  let ibuf: *u8 = sys_mmap(8192)
  let ibn: i64 = g_read(binpath, ibuf, 8192)
  let lpos: i64 = g_find_sectpeek_load(ibuf, ibn)
  var tamper_built: i64 = 0
  if lpos >= 0 {
      let ebyte: i64 = lpos + 11           // high immediate byte of the expected addi
      ibuf[ebyte] = (ibuf[ebyte] + 1) as u8
      let tfd: i64 = sys_openat_wr(tamper_bin, 0x1a4)
      if tfd >= 0 { sys_write(tfd, ibuf, ibn); sys_close(tfd); tamper_built = 1 }
  }
  var tamper_bites: i64 = 0
  var tamper_keeps_stat: i64 = 0
  if tamper_built == 1 {
      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)                                 // full golden should now MISS
      let tamper_stat: i64 = g_buf_has(tbuf, tbn, statonly_gold, g_strlen(statonly_gold))    // STAT tail survives
      if tamper_trans == 0 { tamper_bites = 1 }
      if tamper_stat == 1 { tamper_keeps_stat = 1 }
  }
328
  // ---- MIGRATED ONTO THE BASE CLASS (D001), BY HAND ----------------------------------------------
  // BUILT-UNPROMOTED before today: compiled and unrunnable, so the layer it covers had NO live check.
  // ★★★★★★A GATE NOBODY CAN RUN DOES NOT DEGRADE TO NEUTRAL -- IT DEGRADES TO A FALSE SENSE OF
  // COVERAGE, BECAUSE ITS EXISTENCE IS COUNTED AND ITS VERDICT IS NOT.
  let ctr: *i64 = gv_ctr()
  gv_check("sovereign_emu: driver wrote a sector pattern into the descriptor's data buffer; on the kick the device followed desc[head].addr into guest RAM, DMA-read that word and latched it into QueueSectPeek; the driver read it back and verified it -- real sector DATA round-tripped through the ring; transcript == golden, clean halt", sov_ok, ctr)
  // qemu is an EXTERNAL BINARY, not part of the system under test. Zero captured bytes means it
  // never ran (absent on this host), and scoring that as a FAILED alignment check indicts OUR driver
  // for the absence of SOMEONE ELSE'S binary -- measured today: sovereign_emu PASS + tamper
  // BITE-PROVEN while this axis read FAIL purely because qemu-system-riscv64 is not installed.
  // ******A DETECTOR THAT CANNOT TELL "I COULD NOT LOOK" FROM "I LOOKED AND IT IS BROKEN" TEACHES
  // EVERYONE TO IGNORE IT. gv_need gives this axis its third state, and SKIP is NOT a pass: it still
  // blocks any claim that the two lanes agree, exactly as missing evidence blocks a GO but never a NO-GO.
  var qemu_ran: i64 = 0
  if g_qemu_bytes > 0 { qemu_ran = 1 }
  if gv_need("qemu-system-riscv64 produced a transcript (the external cross-check binary must exist to be compared against)", qemu_ran, ctr) == 1 {
      gv_check("qemu_align: the SAME driver lays the SAME descriptor+avail+sector against a REAL legacy virtio-blk-device and both lanes agree on the VQ prefix", align, ctr)
  }
  // ★`tamper_keeps_stat` was ALREADY the silent-on-good control, buried inside a flat conjunction where
  // its purpose was invisible. A whole-transcript collapse satisfies "SECT dropped" while proving
  // nothing; the SURVIVING STAT tail is what makes this tamper DISCRIMINATING rather than destructive.
  var tamper_overfired: i64 = 1
  if tamper_keeps_stat == 1 { tamper_overfired = 0 }
  gv_bite("tamper-bite-sectpeek: corrupting the SectPeek-expected constant DROPS the SECT canary while the ...USED STAT tail SURVIVES", tamper_bites, tamper_overfired, ctr)
353
  // ONE evidence row on EVERY path, same fields either way -- the old shape put the golden in the
  // GREEN branch and the conjuncts in the RED branch, so the field a reader needed was always in the
  // branch that did not run.
  if lfd >= 0 {
      g_fp(lfd, "SECTGATE runtime=sovereign-emu transport=legacy-virtio-mmio layer=sector-data roundtrip=guest-buf->device-dma->sectpeek->driver-readback sov_ok=" as *u8); g_fn(lfd, sov_ok)
      g_fp(lfd, " align_qemu=" as *u8); g_fn(lfd, align)
      g_fp(lfd, " tamper_bites=" as *u8); g_fn(lfd, tamper_bites)
      g_fp(lfd, " tamper_keeps_stat=" as *u8); g_fn(lfd, tamper_keeps_stat)
      g_fp(lfd, " 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); sys_close(lfd)
  }
  let rc: i64 = gv_verdict("SECTGATE", ctr, "the sovereign rv64 emu drove the sector-data layer: the driver wrote a sector pattern into the descriptor's data buffer, the device followed desc[head].addr into guest RAM on the kick, DMA-read that word and latched it into QueueSectPeek, and the driver read it back and verified it -- REAL sector data round-tripped through the ring, with a qemu cross-check agreeing on the VQ prefix and the SectPeek tamper rejected")
  sys_exit(rc)
  return rc
369}
_k_r2_001b3_gate.nx source

`_k_r2_001b3_gate.nx` source
