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

↩ module page · 164 lines · 8799 B
1// nx_v128_gate.nx -- F618 STANDING SIMD GATE, POST-FLIP FORM (2026-07-21): proves the v128 SAD path
2// BIT-EXACT vs a pure-scalar reference, mechanically, through the SHARED pipeline (nx_compile_wat ->
3// nx_wat_compiler -> nx_wasm_vm, all carrying the F618 SIMD flip), against the NATIVE authority. Teeth:
4//   T1 native reference-equivalence: pvr_* (pre-flip scalar copies) == vm_* natively (the flip did
5//      not change a single native result)
6//   T2 VM scalar sweep == native (the pipeline lowers the pure-SCALAR reference faithfully)
7//   T3 VM SIMD sweep == native (THE CLAIM: real v128 opcodes interpreted == scalar ground truth)
8//   T4 micro 16-byte SAD at an UNALIGNED address: VM simd == VM ref == native
9//   T5 non-vacuity: the wasm MUST contain 0xFD 0x73 (i8x16.sub_sat_u) sequences -- a stale or
10//      scalar-pipeline build cannot fake GREEN (doubles as /tmp-staleness detection)
11//   T6 NEGATIVE CONTROL: corrupt ONE frame byte in VM memory -> the simd sweep checksum MUST move
12// usage: build the two STOCK pipeline elfs (nx_sov_build_run nx_compile_wat / nx_wat_compiler
13// --build-only) + this gate, then run /tmp/nx_v128_gate.sov.elf
14// license_tier: ORIGINAL
15import "nx_syscalls.nx"
16import "nx_wasm_vm.nx"
17import "nx_v128_probe.nx"
18import "nx_gate_verdict.nx"
19
20// ★PATHS PORTABLE-FIXED 2026-08-01 (debt 1785560248). This gate reported 'FAIL: no wasm artifact' and
21// exited 3 with pass=0/0 -- ZERO teeth -- and is one of the two REDs BLOCKING EVERY DEPLOY via
22// nx_deploy_ready evidence-honesty. It was never a code fault. THREE path assumptions had inverted when
23// execution moved laptop->NAS:
24//   1. the two toolchain ELFs were expected in /tmp, which the NAS clears (and mounts noexec), so the
25//      forks produced nothing and the missing OUTPUT was reported instead of the missing TOOL;
26//   2. the probe SOURCE was an absolute /mnt/c laptop path that does not exist here.
27// Both compilers existed only as SOURCE on the NAS; they are now built + promoted (nx_compile_wat
28// 437418B, nx_wat_compiler 52309B) and addressed at their real locations. VSRC is relative so it resolves
29// on BOTH hosts. Outputs stay in /tmp: writing there is fine, only EXECUTING from it is not.
30const VCWAT: *u8 = "nx_compile_wat.elf"
31const VWATC: *u8 = "nx_wat_compiler.elf"
32const VSRC:  *u8 = "buildroot/runtime/_hdl_build/nx_v128_probe.nx"
33const VWAT:  *u8 = "/tmp/nx_v128_probe.wat"
34const VWASM: *u8 = "/tmp/nx_v128_probe.wasm"
35
36func vw(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
37func vn(v: i64) -> i64 {
  let b: *u8=sys_mmap(28); var m: i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m}
  let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48 as u8;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{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 }
41
42func vrun_elf(elf: *u8, a1: *u8, a2: *u8) -> i64 {
  let pid: i64 = sys_fork()
  if pid == 0 {
      let argv: *i64 = sys_mmap(64) as *i64
      argv[0] = elf as i64
      argv[1] = a1 as i64
      argv[2] = a2 as i64
      argv[3] = 0
      let envp: *i64 = sys_mmap(16) as *i64
      envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64
      envp[1] = 0
      sys_execve(elf, argv, envp)
      sys_exit(127)
  }
  let st: *i64 = sys_mmap(16) as *i64
  sys_wait4(pid, st, 0)
  return (st[0] >> 8) & 0xff }
59
60func main() -> i64 {
  vw("=== nx_v128_gate: F618 v128 SAD kernel, bit-exact vs scalar (native + VM + wasm bytes) ===\n" as *u8)
  var pass: i64 = 0
  var total: i64 = 0
  let RTBASE: i64 = 0x20000
  let QP: i64 = 22
  // ---- build the probe through the shared pipeline (2 forks = the WSL budget) ----
  vw("  [pipeline] .nx -> .wat -> .wasm via the shared toolchain ..." as *u8)
  vrun_elf(VCWAT, VSRC, VWAT)
  vrun_elf(VWATC, VWAT, VWASM)
  let box: *i64 = sys_mmap(16) as *i64
  let wasm: *u8 = sys_read_file(VWASM, box)
  if (wasm as i64) == 0 { vw(" FAIL: no wasm artifact\n" as *u8); sys_exit(3); return 3 }
  vw(" wasm=" as *u8); vn(box[0]); vw("B\n" as *u8)
  // ---- T5 non-vacuity FIRST (also catches a stale scalar wasm faking the rest) ----
  total = total + 1
  var nfd73: i64 = 0
  var nfd00: i64 = 0
  var bi: i64 = 0
  let wn: i64 = box[0] - 1
  while bi < wn {
      if wasm[bi] == (0xFD as u8) {
          if wasm[bi+1] == (0x73 as u8) { nfd73 = nfd73 + 1 }
          if wasm[bi+1] == (0x00 as u8) { nfd00 = nfd00 + 1 }
      }
      bi = bi + 1
  }
  vw("  [T5 vacuity ] FD73(sub_sat_u)=" as *u8); vn(nfd73); vw("  FD00(v128.load)=" as *u8); vn(nfd00)
  if nfd73 >= 2 { pass = pass + 1; vw("  PASS (SIMD really present)\n" as *u8) } else { vw("  FAIL\n" as *u8) }
  // ---- native ground truth + T1 reference-equivalence, 3 corpora ----
  let natbase: *u8 = sys_mmap(2097152)
  let nb: i64 = natbase as i64
  let seeds: *i64 = sys_mmap(64) as *i64
  let ws: *i64 = sys_mmap(64) as *i64
  let hs: *i64 = sys_mmap(64) as *i64
  seeds[0]=3;  ws[0]=64; hs[0]=64
  seeds[1]=17; ws[1]=64; hs[1]=64
  seeds[2]=9;  ws[2]=96; hs[2]=80
  let gs: *i64 = sys_mmap(64) as *i64
  total = total + 1
  var t1ok: i64 = 1
  var ci: i64 = 0
  while ci < 3 {
      pv_fill(nb, seeds[ci], ws[ci], hs[ci])
      let a: i64 = pv_sweep_scalar(nb, ws[ci], hs[ci], QP)
      let bsw: i64 = pv_sweep_simd(nb, ws[ci], hs[ci], QP)
      gs[ci] = a
      if a != bsw { t1ok = 0 }
      ci = ci + 1
  }
  vw("  [T1 refequiv] native pvr_* == vm_* over 3 corpora: " as *u8)
  if t1ok == 1 { pass = pass + 1; vw("PASS  (g0=" as *u8); vn(gs[0]); vw(" g1=" as *u8); vn(gs[1]); vw(" g2=" as *u8); vn(gs[2]); vw(")\n" as *u8) } else { vw("FAIL\n" as *u8) }
  // ---- load the wasm in the shared VM ----
  let mod: *WasmMod = wm_new(wasm, box[0])
  if wm_parse(mod) != 0 { vw("  FAIL wasm parse\n" as *u8); sys_exit(4); return 4 }
  // ---- T2 VM scalar == native ; T3 VM simd == native ----
  total = total + 1
  total = total + 1
  var t2ok: i64 = 1
  var t3ok: i64 = 1
  ci = 0
  while ci < 3 {
      wm_run(mod, "pv_fill" as *u8, RTBASE, seeds[ci], ws[ci], hs[ci], 0, 4)
      let vsc: i64 = wm_run(mod, "pv_sweep_scalar" as *u8, RTBASE, ws[ci], hs[ci], QP, 0, 4)
      let vsi: i64 = wm_run(mod, "pv_sweep_simd" as *u8, RTBASE, ws[ci], hs[ci], QP, 0, 4)
      if vsc != gs[ci] { t2ok = 0; vw("    T2 DIVERGE corpus=" as *u8); vn(ci); vw(" vm=" as *u8); vn(vsc); vw(" nat=" as *u8); vn(gs[ci]); vw("\n" as *u8) }
      if vsi != gs[ci] { t3ok = 0; vw("    T3 DIVERGE corpus=" as *u8); vn(ci); vw(" vm=" as *u8); vn(vsi); vw(" nat=" as *u8); vn(gs[ci]); vw("\n" as *u8) }
      ci = ci + 1
  }
  vw("  [T2 vmscalar] VM scalar sweep == native: " as *u8)
  if t2ok == 1 { pass = pass + 1; vw("PASS\n" as *u8) } else { vw("FAIL\n" as *u8) }
  vw("  [T3 vmsimd  ] VM v128 sweep == native:   " as *u8)
  if t3ok == 1 { pass = pass + 1; vw("PASS\n" as *u8) } else { vw("FAIL\n" as *u8) }
  // ---- T4 micro unaligned 16-byte SAD (offset 0x20003 vs 0x20011 -- both odd-aligned) ----
  total = total + 1
  wm_run(mod, "pv_fill" as *u8, RTBASE, 7, 64, 64, 0, 4)
  let ua: i64 = RTBASE + 3
  let ub: i64 = RTBASE + 4096 + 17
  let vms: i64 = wm_run(mod, "pv_sad16" as *u8, ua, ub, 0, 0, 0, 2)
  let vmr: i64 = wm_run(mod, "pv_sad16_ref" as *u8, ua, ub, 0, 0, 0, 2)
  pv_fill(nb, 7, 64, 64)
  let na2: i64 = nb + 3
  let nb2: i64 = nb + 4096 + 17
  let nat4: i64 = pv_sad16(na2, nb2)
  vw("  [T4 unalign ] vm_simd=" as *u8); vn(vms); vw(" vm_ref=" as *u8); vn(vmr); vw(" native=" as *u8); vn(nat4)
  if vms == vmr { if vms == nat4 { pass = pass + 1; vw("  PASS\n" as *u8) } else { vw("  FAIL\n" as *u8) } } else { vw("  FAIL\n" as *u8) }
  // ---- T6 negative control: one corrupted pixel MUST move the simd checksum ----
  total = total + 1
  wm_run(mod, "pv_fill" as *u8, RTBASE, 3, 64, 64, 0, 4)
  let m2: *u8 = mod.mem
  let cb: i64 = RTBASE + 1234
  let old: i64 = m2[cb] as i64
  let flip: i64 = old ^ 1
  m2[cb] = flip as u8
  let vneg: i64 = wm_run(mod, "pv_sweep_simd" as *u8, RTBASE, 64, 64, QP, 0, 4)
  m2[cb] = old as u8
  vw("  [T6 negctl  ] corrupted-pixel simd chk=" as *u8); vn(vneg); vw(" vs clean=" as *u8); vn(gs[0])
  if vneg != gs[0] { pass = pass + 1; vw("  PASS (gate can fail)\n" as *u8) } else { vw("  FAIL (VACUOUS)\n" as *u8) }
  // ---- verdict ----
  vw("=== V128 GATE: " as *u8); vn(pass); vw("/" as *u8); vn(total); vw(" " as *u8)
  if pass == total { vw("GREEN ===\n" as *u8) } else { vw("RED ===\n" as *u8) }
  let ctr: *i64 = gv_ctr()
  ctr[0] = pass
  ctr[1] = total
  return gv_verdict("V128-GATE" as *u8, ctr, "v128 SAD bit-exact vs scalar across native + VM + real wasm, negctl proven" as *u8) }
nx_v128_gate.nx source

`nx_v128_gate.nx` source
