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

↩ module page · 197 lines · 11348 B
1// nx_vcodec_layout_gate.nx -- PROVE the vcv-10 MV-plane placement is collision-free in the CLIENT's
2// PACKED context slab at PRODUCTION geometry (F617/seq246). Context: nx_faithdiff proved rct9 lowers to
3// wasm BIT-EXACTLY (VM==native, 0 unfaithful) => the field defect (probe835: rx flowing, dec=-1) is
4// INTEGRATION. The ONE untested seam: every bench/probe gives the MV plane an ISOLATED mmap, but the
5// browser DERIVES it as CX+VV_CTX_MVPLANE (0x32000) INSIDE the shared context slab that also holds the
6// range-coder scratch (CX+0x1800). At 416x320 (the shipped tier) a KEYFRAME's rc section is far larger
7// than any bench frame -- if it overruns 0x32000 it silently clobbers the plane => wrong MV predictors
8// => undecodable P-frames => exactly the observed signature.
9// This gate MEASURES instead of estimating (scale-law: declare the envelope, never assume it):
10//   T1  rc high-water: pattern-fill the slab, run key+P with the plane held ISOLATED (so nothing
11//       legitimately writes high in the slab), then scan for the HIGHEST byte the codec touched.
12//       PASS iff high_water < 0x32000 (the packed placement has real clearance).
13//   T2  A/B equivalence: the SAME key+P roundtrip with the plane PACKED (CX+0x32000) vs ISOLATED must
14//       produce an IDENTICAL recon checksum. PASS iff equal (packed placement changes nothing).
15// A T1/T2 failure PROVES the collision and mandates the fix shape: give the MV plane its OWN dedicated
16// region passed EXPLICITLY (the proven R_HEAT/heatp pattern), never a base+offset carve.
17// license_tier: ORIGINAL   No hw writes (Rule 26).   expect_exit: 0
18import "nx_video_codec_wasm.nx"
19import "nx_gate_verdict.nx"
20
21const LW: i64 = 416            // shipped production tier (resTier cls-9 mid rung)
22const LH: i64 = 320
23const CX_EST: i64 = 0x80       // the CLIENT's exact VV_CTX_* offsets (nx_video_client_wasm.nx)
24const CX_PROBS: i64 = 0x180
25const CX_T8C: i64 = 0x280
26const CX_RCSCR: i64 = 0x1800
27const CX_MVPLANE: i64 = 0x32000
28const SLAB: i64 = 0x40000      // context slab we scan (256KB, past the plane)
29const PAT: i64 = 165           // 0xA5 canary
30const EMODE: i64 = 673         // production RTC: rc(1)+sig(32)+part(128)+deblock(512)
31
32// one key(rct8) + P(rct9) roundtrip. fbase = frame-buffer base, cxbase = context slab, plane = MV plane.
33// obox[0] = P bytes, obox[1] = key bytes. Returns the decoded-P recon checksum.
34// kmode: 1 = key via vv_enc_rct8 (what the benches assumed); 0 = key via vv_enc_rc (what PRODUCTION
35// actually does -- t8Flag is OFF by default so the client's cm never carries bit3, so keys ride the 4x4
36// range path while rct9 P-frames force the t8 syntax internally. THE untested shipped chain.)
37// em: the emode for this round (T1-T3 pass EMODE=673; T4 passes 677 = bit2 t8-on-P, the F1114b path).
38func lg_round(fbase: i64, cxbase: i64, plane: i64, kmode: i64, em: i64, obox: *i64) -> i64 {
  let N: i64 = LW*LH
  let C: i64 = (LW/2)*(LH/2)
  let sz: i64 = N + 2*C
  let f0: *u8 = fbase as *u8
  let f1: *u8 = (fbase + sz) as *u8
  let zeros: *u8 = (fbase + 2*sz) as *u8
  let rEK: *u8 = (fbase + 3*sz) as *u8
  let rEP: *u8 = (fbase + 4*sz) as *u8
  let rDK: *u8 = (fbase + 5*sz) as *u8
  let rDP: *u8 = (fbase + 6*sz) as *u8
  let sK: *u8 = (fbase + 7*sz) as *u8
  let sP: *u8 = (fbase + 7*sz + 524288) as *u8
  let blk: *i64 = (fbase + 7*sz + 1048576) as *i64
  let mv: *i64 = (fbase + 7*sz + 1052672) as *i64
  let rctx: *i64 = cxbase as *i64
  let est: *i64 = (cxbase + CX_EST) as *i64
  let probs: *i64 = (cxbase + CX_PROBS) as *i64
  let t8c: *i64 = (cxbase + CX_T8C) as *i64
  let rcbuf: *u8 = (cxbase + CX_RCSCR) as *u8
  vc_t8_init(t8c)
  var i: i64 = 0
  while i < sz { zeros[i] = 0 as u8; i = i + 1 }
  // frame0: gradient + texture (realistic residual); frame1: shifted right 2px => REAL motion => the
  // median-predict + exp-Golomb MVD path fires on most MBs (a static pair would skip and prove nothing)
  i = 0
  while i < N {
      let x: i64 = i % LW
      let y: i64 = i / LW
      var v: i64 = (x + y) * 2 + ((x * y) % 17)
      if x > (LW/2) { v = v + 40 }
      v = v % 256
      f0[i] = v as u8
      i = i + 1 }
  i = N; while i < sz { f0[i] = 128 as u8; i = i + 1 }
  var yy: i64 = 0
  while yy < LH { var xx: i64 = 0
      while xx < LW {
          var sx: i64 = xx - 2
          if sx < 0 { sx = 0 }
          f1[yy*LW + xx] = f0[yy*LW + sx]
          xx = xx + 1 } yy = yy + 1 }
  i = N; while i < sz { f1[i] = f0[i]; i = i + 1 }
  // ENC key(rct8) then P(rct9) -- exactly the shipped chain (keys ride rct8, P rides the lean+MVD pair)
  rctx[0]=em; rctx[1]=est as i64; rctx[2]=probs as i64; rctx[3]=rcbuf as i64; rctx[4]=t8c as i64
  rctx[5]=0; rctx[6]=0; rctx[7]=0; rctx[8]=0; rctx[9]=plane
  var kb: i64 = 0
  if kmode == 1 { kb = vv_enc_rct8(f0, zeros, rEK, LW, LH, 22, 1, 22*188, sK, 524288, blk, mv, rctx) }
  else { kb = vv_enc_rc(f0, zeros, rEK, LW, LH, 22, 1, 22*188, sK, 524288, blk, mv, rctx) }
  rctx[0]=em; rctx[1]=est as i64; rctx[2]=probs as i64; rctx[3]=rcbuf as i64; rctx[4]=t8c as i64
  rctx[5]=0; rctx[6]=0; rctx[7]=0; rctx[8]=0; rctx[9]=plane
  let pb: i64 = vv_enc_rct9(f1, rEK, rEP, LW, LH, 22, 22*94, sP, 524288, blk, mv, rctx)
  // DEC the same order
  rctx[0]=em; rctx[1]=est as i64; rctx[2]=probs as i64; rctx[3]=rcbuf as i64; rctx[4]=t8c as i64
  rctx[5]=0; rctx[6]=0; rctx[7]=0; rctx[8]=0; rctx[9]=plane
  if kmode == 1 { vv_dec_rct8(zeros, rDK, LW, LH, 22, sK, kb, blk, mv, rctx) }
  else { vv_dec_rc(zeros, rDK, LW, LH, 22, sK, kb, blk, mv, rctx) }
  rctx[0]=em; rctx[1]=est as i64; rctx[2]=probs as i64; rctx[3]=rcbuf as i64; rctx[4]=t8c as i64
  rctx[5]=0; rctx[6]=0; rctx[7]=0; rctx[8]=0; rctx[9]=plane
  vv_dec_rct9(rDK, rDP, LW, LH, 22, sP, pb, blk, mv, rctx)
  obox[0] = pb
  obox[1] = kb
  // ★LIAR-KILLER (the check the A/B alone cannot make: two runs can be identically WRONG): the
  // ENCODER's recon must equal the DECODER's recon byte-for-byte, at THIS geometry + THIS emode.
  // The bgop bench proves this at 576x1024/emode-4005; the SHIPPED client runs 416x320/emode-673.
  var mk: i64 = 0
  var mp: i64 = 0
  i = 0
  while i < sz { if rEK[i] != rDK[i] { mk = mk + 1 } i = i + 1 }
  i = 0
  while i < sz { if rEP[i] != rDP[i] { mp = mp + 1 } i = i + 1 }
  obox[2] = mk
  obox[3] = mp
  var sum: i64 = 0
  i = 0
  while i < sz { sum = sum + (rDP[i] & 0xff) * ((i % 251) + 1); i = i + 1 }
  return sum & 0xffffffff }
115
116func main() -> i64 {
  gv_head("=== nx_vcodec_layout_gate: vcv-10 MV-plane vs the CLIENT packed slab @416x320 (F617/seq246) ===" as *u8)
  let ctr: *i64 = gv_ctr()
  let fbase: *u8 = sys_mmap(4194304)
  let cxbase: *u8 = sys_mmap(SLAB + 65536)
  let isoplane: *i64 = sys_mmap(65536) as *i64      // ISOLATED plane (the bench/probe condition)
  let obox: *i64 = sys_mmap(64) as *i64
123
  // ---- T1: MEASURE the codec's true high-water mark inside the context slab ----
  // plane held ISOLATED so nothing legitimately writes high in the slab; whatever moved is rc scratch.
  var i: i64 = 0
  while i < SLAB { cxbase[i] = PAT as u8; i = i + 1 }
  let ck_iso: i64 = lg_round(fbase as i64, cxbase as i64, isoplane as i64, 1, EMODE, obox)
  let pbytes: i64 = obox[0]
  let kbytes: i64 = obox[1]
  var hi: i64 = 0
  i = CX_RCSCR
  while i < SLAB { if cxbase[i] != (PAT as u8) { hi = i } i = i + 1 }
  gv_puts("  key bytes=" as *u8); gv_num(kbytes)
  gv_puts("  P bytes=" as *u8); gv_num(pbytes)
  gv_puts("  rc-scratch high-water=0x" as *u8); gv_num(hi)
  gv_puts("  (plane sits at 0x" as *u8); gv_num(CX_MVPLANE); gv_puts(")\n" as *u8)
  var clear: i64 = 0
  if hi < CX_MVPLANE { clear = 1 }
  gv_check("rc scratch stays BELOW the packed MV-plane offset" as *u8, clear, ctr)
141
  // ---- T1b: DECODE PARITY at the SHIPPED geometry + emode (the config no prior harness covered) ----
  gv_puts("  key recon mismatches=" as *u8); gv_num(obox[2])
  gv_puts("  P(rct9) recon mismatches=" as *u8); gv_num(obox[3]); gv_puts("\n" as *u8)
  var keyok: i64 = 0
  if obox[2] == 0 { keyok = 1 }
  gv_check("KEY(rct8) enc recon == dec recon @416x320 emode673" as *u8, keyok, ctr)
  var pok: i64 = 0
  if obox[3] == 0 { pok = 1 }
  gv_check("P(rct9 lean+MVD) enc recon == dec recon @416x320 emode673" as *u8, pok, ctr)
151
  // ---- T2: A/B -- packed plane must give a BIT-IDENTICAL result to the isolated plane ----
  let packed: i64 = (cxbase as i64) + CX_MVPLANE
  let ck_pack: i64 = lg_round(fbase as i64, cxbase as i64, packed, 1, EMODE, obox)
  var same: i64 = 0
  if ck_pack == ck_iso { same = 1 }
  gv_puts("  checksum isolated=" as *u8); gv_num(ck_iso)
  gv_puts("  packed=" as *u8); gv_num(ck_pack); gv_puts("\n" as *u8)
  gv_check("packed-plane roundtrip == isolated-plane roundtrip" as *u8, same, ctr)
160
  // ---- T3: THE ACTUAL SHIPPED CHAIN -- key via vv_enc_rc (t8Flag is OFF in production so the client's
  // cm never carries bit3) then P via rct9. No prior harness covered this pairing: the bgop bench and
  // T1/T2 above both key with rct8. If rct9 P-frames cannot chain off an rc key, THAT is the field bug.
  let ck_rc: i64 = lg_round(fbase as i64, cxbase as i64, packed, 0, EMODE, obox)
  gv_puts("  [SHIPPED CHAIN key=vv_enc_rc] key bytes=" as *u8); gv_num(obox[1])
  gv_puts("  P bytes=" as *u8); gv_num(obox[0])
  gv_puts("  key mism=" as *u8); gv_num(obox[2])
  gv_puts("  P mism=" as *u8); gv_num(obox[3]); gv_puts("\n" as *u8)
  var rckey: i64 = 0
  if obox[2] == 0 { rckey = 1 }
  gv_check("KEY(vv_enc_rc) enc recon == dec recon (production key path)" as *u8, rckey, ctr)
  var rcp: i64 = 0
  if obox[3] == 0 { rcp = 1 }
  gv_check("P(rct9) chains off an RC key bit-exactly (THE SHIPPED CHAIN)" as *u8, rcp, ctr)
175
  // ---- T4 (F1114b, 2026-07-29): the bit2 t8-on-P chain -- vc_rd_t8_inter freq-domain SSE + the
  // LEVELS HANDBACK (the emit consumes the trial's banked levels + predictor instead of recomputing).
  // enc==dec parity is the discriminating tooth: if the handback ever feeds the emit levels that
  // differ from what reached the wire, encoder recon diverges from decoder recon => RED. Non-vacuity
  // is visible in the printed bytes: P at 677 runs FAR below 673's (many MBs take the 8x8 path), so a
  // silently-dead bit2 would show as P bytes == the T3 number. (BD bound measured: +0.14% avg 4-seq.)
  let ck_t8: i64 = lg_round(fbase as i64, cxbase as i64, packed, 0, 677, obox)
  gv_puts("  [BIT2 CHAIN emode677] key bytes=" as *u8); gv_num(obox[1])
  gv_puts("  P bytes=" as *u8); gv_num(obox[0])
  gv_puts("  key mism=" as *u8); gv_num(obox[2])
  gv_puts("  P mism=" as *u8); gv_num(obox[3])
  gv_puts("  ck=" as *u8); gv_num(ck_t8); gv_puts("\n" as *u8)
  var t8key: i64 = 0
  if obox[2] == 0 { t8key = 1 }
  gv_check("KEY under emode677 enc==dec (bit2 is P-only, key path untouched)" as *u8, t8key, ctr)
  var t8p: i64 = 0
  if obox[3] == 0 { t8p = 1 }
  gv_check("P(rct9+bit2) t8 LEVELS-HANDBACK enc recon == dec recon (F1114b liar-killer)" as *u8, t8p, ctr)
194
  let rc: i64 = gv_verdict("VCODEC-LAYOUT-GATE" as *u8, ctr, "client packed MV-plane placement is collision-free at 416x320" as *u8)
  sys_exit(rc)
  return rc }
nx_vcodec_layout_gate.nx source

`nx_vcodec_layout_gate.nx` source
