code wiki / (root) / nx_nofloat_q4k_gate.nx
`nx_nofloat_q4k_gate.nx` source

↩ module page · 308 lines · 19661 B
1// nx_nofloat_q4k_gate.nx -- the REFEREE for nx_nofloat_q4k (LM4 resident-quant decode, /compare/engineshift 2026-09-02).
2// In-process teeth that need no model: a hand-built Q4_K super-block matrix with d=1.0, dmin=0, every scale 1 and every
3// min 0 makes each dequantised weight EXACTLY its 4-bit code, and the activation is chosen so the dynamic i16 pack is
4// exact, so nq_mm's Q16 output has ONE correct value that an independent i64 reference computes (both shift regimes,
5// and a full-width 18944 row for the overflow headroom); the route decision is a pure function tested on every branch
6// (Q4_K aligned -> in place; Q6_K -> i16; a non-256 width -> i16, never a silent in-place read); the i16 route must
7// equal mm_pool_i8 on the same inputs; the scale must never let max|x| wrap an i16 lane. Neg-control: one post-shift
8// off must NOT match the reference. T0 (gv_need the Q4_K_M fixture) censuses the fixture's tensor types so the
9// model-level serve gate can only claim the fused path where Q4_K tensors exist -- fixture-reached-the-condition.
10//   nx_nofloat_q4k_gate [model.gguf]   default /home/elderwesto/nx_stage/nx_15b_model.gguf
11// license_tier: ORIGINAL. Writes nothing. No hw writes.
12import "nx_syscalls.nx"
13import "nx_tier.nx"
14import "nx_le.nx"
15import "nx_tensor.nx"
16import "nx_gguf.nx"
17import "nx_gguf_load.nx"
18import "nx_thread_pool.nx"
19import "nx_gate_verdict.nx"
20import "nx_gatekit_lib.nx"
21import "nx_nofloat_llm.nx"
22import "nx_q4k_dot_simd_lib.nx"
23import "nx_nofloat_q4k.nx"
24
25const GQ_IN: i64 = 256
26const GQ_OUT: i64 = 3
27const GQ_WIDE_IN: i64 = 18944         // Qwen2.5-7B ffn width: the overflow-headroom case
28const GQ_WIDE_OUT: i64 = 2
29const GQ_F16_ONE_LO: i64 = 0          // 0x3C00 = 1.0 in IEEE half, little-endian bytes
30const GQ_F16_ONE_HI: i64 = 60
31const GQ_SB_BYTES: i64 = 144
32const GQ_SCALES_OFF: i64 = 4
33const GQ_QS_OFF: i64 = 16
34const GQ_QS_BYTES: i64 = 128
35const GQ_SCALE_ONE: i64 = 1           // 6-bit scale field = 1 (bytes 0..3); packed form for sub-blocks 4..7 = 0x01 in bytes 8..11
36const GQ_V_MAX: i64 = 32767
37const GQ_V_SHIFT24: i64 = 14          // x = v << 14 in Q24 -> sx = 2^14 exactly when max v = 32767
38const GQ_V_SHIFT16: i64 = 6           // x = v << 6 in Q16 -> sx = 2^6
39const GQ_REF_MUL: i64 = 64            // (q<<16 * v<<14) >> 24 = 64*q*v  and  (q<<16 * v<<6) >> 16 = 64*q*v
40const GQ_NIBBLES: i64 = 16
41const GQ_LCG_A: i64 = 6364136223846793005
42const GQ_LCG_C: i64 = 1442695040888963407
43const GQ_LCG_MASK: i64 = 0x7FFFFFFFFFFFFFFF
44const GQ_LCG_SEED: i64 = 88172645463325252
45const GQ_SMALL_IN: i64 = 16
46const GQ_SMALL_OUT: i64 = 3
47const GQ_SMALL_W: i64 = 40000
48const GQ_SMALL_X: i64 = 300000
49const GQ_Q24_BITS: i64 = 24
50const GQ_Q8_VALS: i64 = 32
51const GQ_Q8_BYTES: i64 = 34
52const GQ_Q8_SCALE_BYTES: i64 = 2
53const GQ_Q8_CODE_MAX: i64 = 127
54
55static g_gq_st: i64
56
57func gq_lcg() -> i64 { g_gq_st = (g_gq_st*GQ_LCG_A + GQ_LCG_C) & GQ_LCG_MASK; return g_gq_st >> 16 }
58
59// one Q4_K super-block row set: out_dim rows x (in_dim/256) super-blocks, d=1.0 dmin=0 scales=1 mins=0, q from the LCG.
60// W[o][k] (as an exact small integer) is returned in wref (out_dim*in_dim i64) for the reference.
61func gq_build_q4k(out_dim: i64, in_dim: i64, wref: *i64) -> *u8 {
  let nblk: i64 = in_dim / GQ_IN
  let buf: *u8 = sys_mmap(out_dim*nblk*GQ_SB_BYTES)
  var o: i64 = 0
  while o < out_dim {
      var b: i64 = 0
      while b < nblk {
          let base: i64 = (o*nblk + b)*GQ_SB_BYTES
          buf[base] = GQ_F16_ONE_LO as u8; buf[base+1] = GQ_F16_ONE_HI as u8
          buf[base+2] = 0 as u8; buf[base+3] = 0 as u8
          var s: i64 = 0
          while s < 4 { buf[base+GQ_SCALES_OFF+s] = GQ_SCALE_ONE as u8; buf[base+GQ_SCALES_OFF+4+s] = 0 as u8; buf[base+GQ_SCALES_OFF+8+s] = GQ_SCALE_ONE as u8; s = s + 1 }
          var j: i64 = 0
          while j < GQ_QS_BYTES {
              let g: i64 = j / 32; let t: i64 = j % 32
              let qlo: i64 = gq_lcg() % GQ_NIBBLES
              let qhi: i64 = gq_lcg() % GQ_NIBBLES
              buf[base+GQ_QS_OFF+j] = (qlo | (qhi << 4)) as u8
              wref[o*in_dim + b*GQ_IN + g*64 + t] = qlo
              wref[o*in_dim + b*GQ_IN + g*64 + 32 + t] = qhi
              j = j + 1
          }
          b = b + 1
      }
      o = o + 1
  }
  return buf
88}
89
90// activation v_k in [-32767, 32767] with v_0 pinned to +32767 so the dynamic scale is exactly a power of two.
91func gq_fill_v(v: *i64, n: i64) -> i64 {
  var k: i64 = 0
  while k < n { v[k] = (gq_lcg() % (2*GQ_V_MAX + 1)) - GQ_V_MAX; k = k + 1 }
  v[0] = GQ_V_MAX
  return 0
96}
97func gq_ref(wref: *i64, v: *i64, in_dim: i64, o: i64) -> i64 { var s: i64 = 0; var k: i64 = 0; while k < in_dim { s = s + wref[o*in_dim+k]*v[k]; k = k + 1 } return s*GQ_REF_MUL }
98func gq_all_rows_match(dst: *i64, wref: *i64, v: *i64, in_dim: i64, out_dim: i64) -> i64 {
  var ok: i64 = 1; var o: i64 = 0
  while o < out_dim { if dst[o] != gq_ref(wref, v, in_dim, o) { ok = 0 } o = o + 1 }
  return ok
102}
103func gq_run(buf: *u8, out_dim: i64, in_dim: i64, v: *i64, vshift: i64, shift: i64, dst: *i64) -> i64 {
  let slot: *i64 = sys_mmap(NQ_SLOT_WORDS*8) as *i64
  slot[NQ_S_KIND]=NQ_KIND_Q4K; slot[NQ_S_OFF]=0; slot[NQ_S_IN]=in_dim; slot[NQ_S_OUT]=out_dim
  slot[NQ_S_NBLK]=in_dim/GQ_IN; slot[NQ_S_RSTRIDE]=slot[NQ_S_NBLK]*GQ_SB_BYTES; slot[NQ_S_W16]=0; slot[NQ_S_SW]=0
  let x: *i64 = sys_mmap(in_dim*8) as *i64
  var k: i64 = 0; while k < in_dim { x[k] = v[k] << vshift; k = k + 1 }
  nq_bind_buf(buf)
  nq_mm(x, slot, dst, shift)
  return 0
112}
113
114// one Q8_0 row set (search R0s): out_dim rows x (in_dim/32) blocks, d=1.0 per block and int8 codes from the LCG, so
115// every dequantised weight is EXACTLY its code; W[o][k] is returned in wref for the same exact i64 reference.
116func gq_build_q8(out_dim: i64, in_dim: i64, wref: *i64) -> *u8 {
  let nblk: i64 = in_dim / GQ_Q8_VALS
  let buf: *u8 = sys_mmap(out_dim*nblk*GQ_Q8_BYTES)
  var o: i64 = 0
  while o < out_dim {
      var b: i64 = 0
      while b < nblk {
          let base: i64 = (o*nblk + b)*GQ_Q8_BYTES
          buf[base] = GQ_F16_ONE_LO as u8; buf[base+1] = GQ_F16_ONE_HI as u8
          var i: i64 = 0
          while i < GQ_Q8_VALS {
              let q: i64 = (gq_lcg() % (2*GQ_Q8_CODE_MAX + 1)) - GQ_Q8_CODE_MAX
              buf[base+GQ_Q8_SCALE_BYTES+i] = (q & 0xff) as u8
              wref[o*in_dim + b*GQ_Q8_VALS + i] = q
              i = i + 1
          }
          b = b + 1
      }
      o = o + 1
  }
  return buf
137}
138func gq_run_q8(buf: *u8, out_dim: i64, in_dim: i64, v: *i64, vshift: i64, shift: i64, dst: *i64) -> i64 {
  let slot: *i64 = sys_mmap(NQ_SLOT_WORDS*8) as *i64
  slot[NQ_S_KIND]=NQ_KIND_Q8_0; slot[NQ_S_OFF]=0; slot[NQ_S_IN]=in_dim; slot[NQ_S_OUT]=out_dim
  slot[NQ_S_NBLK]=in_dim/GQ_Q8_VALS; slot[NQ_S_RSTRIDE]=slot[NQ_S_NBLK]*GQ_Q8_BYTES; slot[NQ_S_W16]=0; slot[NQ_S_SW]=0
  let x: *i64 = sys_mmap(in_dim*8) as *i64
  var k: i64 = 0; while k < in_dim { x[k] = v[k] << vshift; k = k + 1 }
  nq_bind_buf(buf)
  nq_mm(x, slot, dst, shift)
  return 0
147}
148
149func gq_census(path: *u8, cnt: *i64) -> i64 {
  let len: *i64 = sys_mmap(8) as *i64
  let buf: *u8 = sys_map_file(path, len)
  if (buf as i64) == 0 { return 0 - 1 }
  let hdr: *NxGgufHeader = sys_mmap(NX_GGUF_HDR_BYTES) as *NxGgufHeader
  if nx_gguf_parse(buf, len[0], hdr) != NX_GGUF_OK { return 0 - 2 }
  var i: i64 = 0
  while i < hdr.tensor_count {
      let ti: *NxGgufTensorInfo = nx_gguf_tensor_at(hdr, i)
      if ti.ggml_type == NX_GGML_TYPE_Q8_0 { cnt[5]=cnt[5]+1 }   // R0s: counted beside the partition (it stays inside other=)
      if ti.ggml_type == NX_GGML_TYPE_Q4_K { cnt[0]=cnt[0]+1 } else {
          if ti.ggml_type == NX_GGML_TYPE_Q6_K { cnt[1]=cnt[1]+1 } else {
              if ti.ggml_type == NX_GGML_TYPE_Q5_K { cnt[2]=cnt[2]+1 } else { cnt[3]=cnt[3]+1 } } }
      i = i + 1
  }
  cnt[4] = hdr.tensor_count
  return 0
166}
167
168func main(argc: i64, argv: *i64) -> i64 {
  var model: *u8 = "/home/elderwesto/nx_stage/nx_15b_model.gguf" as *u8
  if argc >= 2 { model = argv[1] as *u8 }
  gv_head("NX-NOFLOAT-Q4K-GATE: resident-Q4_K matvec exactness, route decision, fallback identity, fixture census" as *u8)
  let ctr: *i64 = gv_ctr()
  g_gq_st = GQ_LCG_SEED
  nf_pool()
  nq_arena(GQ_WIDE_IN)
176
  // T1: exact matvec, Q24 input regime (rmsnorm output), 3 rows x 256
  let wref: *i64 = sys_mmap(GQ_OUT*GQ_IN*8) as *i64
  let buf: *u8 = gq_build_q4k(GQ_OUT, GQ_IN, wref)
  let v: *i64 = sys_mmap(GQ_IN*8) as *i64
  gq_fill_v(v, GQ_IN)
  let dst: *i64 = sys_mmap(GQ_OUT*8) as *i64
  gq_run(buf, GQ_OUT, GQ_IN, v, GQ_V_SHIFT24, NQ_SHIFT_Q24, dst)
  gv_puts("  T1 row0 got=" as *u8); gv_num(dst[0]); gv_puts(" ref=" as *u8); gv_num(gq_ref(wref, v, GQ_IN, 0)); gv_puts("\n" as *u8)
  gv_check("T1 Q24-input matvec equals the exact i64 reference on every row (fused dot + post-shift + dynamic i16 scale)" as *u8, gq_all_rows_match(dst, wref, v, GQ_IN, GQ_OUT), ctr)
  gv_check("T1 fixture-reached: reference is non-zero on every row (a zero weight matrix would pass trivially)" as *u8, (gq_ref(wref, v, GQ_IN, 0) != 0) & (gq_ref(wref, v, GQ_IN, 1) != 0) & (gq_ref(wref, v, GQ_IN, 2) != 0), ctr)
  // T2: Q16 input regime (attention concat / silu*up)
  gq_run(buf, GQ_OUT, GQ_IN, v, GQ_V_SHIFT16, NQ_SHIFT_Q16, dst)
  gv_check("T2 Q16-input matvec equals the exact i64 reference on every row" as *u8, gq_all_rows_match(dst, wref, v, GQ_IN, GQ_OUT), ctr)
  // T3: full 7B ffn_down width (74 super-blocks) -- the overflow-headroom case the pre-shift exists for
  let wwide: *i64 = sys_mmap(GQ_WIDE_OUT*GQ_WIDE_IN*8) as *i64
  let bwide: *u8 = gq_build_q4k(GQ_WIDE_OUT, GQ_WIDE_IN, wwide)
  let vw: *i64 = sys_mmap(GQ_WIDE_IN*8) as *i64
  gq_fill_v(vw, GQ_WIDE_IN)
  let dw: *i64 = sys_mmap(GQ_WIDE_OUT*8) as *i64
  gq_run(bwide, GQ_WIDE_OUT, GQ_WIDE_IN, vw, GQ_V_SHIFT16, NQ_SHIFT_Q16, dw)
  gv_puts("  T3 wide row0 got=" as *u8); gv_num(dw[0]); gv_puts(" ref=" as *u8); gv_num(gq_ref(wwide, vw, GQ_WIDE_IN, 0)); gv_puts("\n" as *u8)
  gv_check("T3 18944-wide row (7B ffn_down shape) equals the exact reference: no i64 overflow through the pre-shift" as *u8, gq_all_rows_match(dw, wwide, vw, GQ_WIDE_IN, GQ_WIDE_OUT), ctr)
  // T4 neg-control on the arithmetic: one post-shift off must NOT reproduce the reference
  let dot0: i64 = (gq_ref(wref, v, GQ_IN, 0) / GQ_REF_MUL) << GQ_Q24_BITS
  let sx24: i64 = nq_act_scale(GQ_V_MAX << GQ_V_SHIFT24)
  gv_check("neg-control-T4 a post-shift one bit off does NOT match the reference (the arithmetic tooth can fail)" as *u8, nq_scale_out(dot0, sx24, nq_post_shift(NQ_SHIFT_Q24)+1) != gq_ref(wref, v, GQ_IN, 0), ctr)
  gv_check("T4b the same helper with the right post-shift DOES match (the helper is the one the task uses)" as *u8, nq_scale_out(dot0, sx24, nq_post_shift(NQ_SHIFT_Q24)) == gq_ref(wref, v, GQ_IN, 0), ctr)
  // T5 route decision, every branch
  gv_check("T5a Q4_K with a 256-multiple width routes IN PLACE" as *u8, nq_kind_for(NX_GGML_TYPE_Q4_K, 3584) == NQ_KIND_Q4K, ctr)
  gv_check("T5b Q6_K routes to the i16 fallback" as *u8, nq_kind_for(NX_GGML_TYPE_Q6_K, 3584) == NQ_KIND_I16, ctr)
  gv_check("neg-control-T5c Q4_K with a non-256 width is NEVER read in place (fallback, not a silent stride error)" as *u8, nq_kind_for(NX_GGML_TYPE_Q4_K, 100) == NQ_KIND_I16, ctr)
  gv_check("T5d Q8_0 with a 32-multiple width routes BLOCK-NATIVE (search R0s: the model's own block scales, in place)" as *u8, nq_kind_for(NX_GGML_TYPE_Q8_0, 3584) == NQ_KIND_Q8_0, ctr)
  gv_check("neg-control-T5e Q8_0 with a non-32 width is NEVER read in place (fallback, not a silent stride error)" as *u8, nq_kind_for(NX_GGML_TYPE_Q8_0, 40) == NQ_KIND_I16, ctr)
  // T6 activation scale never lets max|x| wrap an i16 lane
  let xm: i64 = (GQ_V_MAX << GQ_V_SHIFT24) + 1
  gv_check("T6 dynamic scale keeps max|x|/sx inside the i16 lane at the boundary (ceil, not floor)" as *u8, (xm / nq_act_scale(xm)) <= GQ_V_MAX, ctr)
  gv_check("T6b a tiny activation gets scale 1 (never 0 -- division by the scale must be defined)" as *u8, nq_act_scale(5) == 1, ctr)
  // T7 the i16 fallback route equals mm_pool_i8 on the same inputs
  let Wq: *i64 = sys_mmap(GQ_SMALL_OUT*GQ_SMALL_IN*8) as *i64
  var wi: i64 = 0; while wi < GQ_SMALL_OUT*GQ_SMALL_IN { Wq[wi] = (gq_lcg() % (2*GQ_SMALL_W+1)) - GQ_SMALL_W; wi = wi + 1 }
  let xs: *i64 = sys_mmap(GQ_SMALL_IN*8) as *i64
  var xi: i64 = 0; while xi < GQ_SMALL_IN { xs[xi] = (gq_lcg() % (2*GQ_SMALL_X+1)) - GQ_SMALL_X; xi = xi + 1 }
  let fslot: *i64 = sys_mmap(NQ_SLOT_WORDS*8) as *i64
  nq_slot_from_q16(Wq, fslot, GQ_SMALL_IN, GQ_SMALL_OUT)
  let d1: *i64 = sys_mmap(GQ_SMALL_OUT*8) as *i64
  let d2: *i64 = sys_mmap(GQ_SMALL_OUT*8) as *i64
  nq_mm(xs, fslot, d1, NQ_SHIFT_Q24)
  mm_pool_i8(xs, fslot[NQ_S_W16] as *u8, fslot[NQ_S_SW] as *i64, d2, GQ_SMALL_IN, GQ_SMALL_OUT, NQ_SHIFT_Q24)
  gv_check("T7 the i16 fallback route through nq_mm equals mm_pool_i8 on the same slot and input (one fallback ruler)" as *u8, (d1[0]==d2[0]) & (d1[1]==d2[1]) & (d1[2]==d2[2]), ctr)
  gv_check("T7 fixture-reached: the fallback output is non-zero" as *u8, (d1[0] != 0) | (d1[1] != 0), ctr)
  // T8 (search R0s, 2026-09-17): the Q8_0 BLOCK-NATIVE route. d=1.0 per block and int8 codes from the LCG make every
  // weight EXACTLY its code, so nq_mm's Q16 output has ONE correct value the same exact i64 reference computes;
  // both shift regimes, the 18944-wide overflow case, and a neg-control that edits one code byte in the file bytes.
  let wref8: *i64 = sys_mmap(GQ_OUT*GQ_IN*8) as *i64
  let buf8: *u8 = gq_build_q8(GQ_OUT, GQ_IN, wref8)
  let v8: *i64 = sys_mmap(GQ_IN*8) as *i64
  gq_fill_v(v8, GQ_IN)
  let dst8: *i64 = sys_mmap(GQ_OUT*8) as *i64
  gq_run_q8(buf8, GQ_OUT, GQ_IN, v8, GQ_V_SHIFT24, NQ_SHIFT_Q24, dst8)
  gv_puts("  T8 row0 got=" as *u8); gv_num(dst8[0]); gv_puts(" ref=" as *u8); gv_num(gq_ref(wref8, v8, GQ_IN, 0)); gv_puts("\n" as *u8)
  gv_check("T8a Q8_0 block-native Q24-input matvec equals the exact i64 reference on every row (block scales + i16 lanes + post-shift)" as *u8, gq_all_rows_match(dst8, wref8, v8, GQ_IN, GQ_OUT), ctr)
  gv_check("T8a fixture-reached: the Q8_0 reference is non-zero on row 0" as *u8, gq_ref(wref8, v8, GQ_IN, 0) != 0, ctr)
  gq_run_q8(buf8, GQ_OUT, GQ_IN, v8, GQ_V_SHIFT16, NQ_SHIFT_Q16, dst8)
  gv_check("T8b Q8_0 block-native Q16-input matvec equals the exact i64 reference on every row" as *u8, gq_all_rows_match(dst8, wref8, v8, GQ_IN, GQ_OUT), ctr)
  let wrefw8: *i64 = sys_mmap(GQ_WIDE_OUT*GQ_WIDE_IN*8) as *i64
  let bufw8: *u8 = gq_build_q8(GQ_WIDE_OUT, GQ_WIDE_IN, wrefw8)
  let vw8: *i64 = sys_mmap(GQ_WIDE_IN*8) as *i64
  gq_fill_v(vw8, GQ_WIDE_IN)
  let dstw8: *i64 = sys_mmap(GQ_WIDE_OUT*8) as *i64
  gq_run_q8(bufw8, GQ_WIDE_OUT, GQ_WIDE_IN, vw8, GQ_V_SHIFT24, NQ_SHIFT_Q24, dstw8)
  gv_check("T8c 18944-wide Q8_0 row (592 blocks) equals the exact reference: no i64 overflow through the block accumulation" as *u8, gq_all_rows_match(dstw8, wrefw8, vw8, GQ_WIDE_IN, GQ_WIDE_OUT), ctr)
  let q0: i64 = (buf8[GQ_Q8_SCALE_BYTES] as i64) & 0xff
  buf8[GQ_Q8_SCALE_BYTES] = ((q0 + 1) & 0xff) as u8
  gq_run_q8(buf8, GQ_OUT, GQ_IN, v8, GQ_V_SHIFT24, NQ_SHIFT_Q24, dst8)
  gv_check("neg-control-T8d one code byte changed in the file bytes changes row 0 (the route reads the blocks, not a cache)" as *u8, dst8[0] != gq_ref(wref8, v8, GQ_IN, 0), ctr)
  buf8[GQ_Q8_SCALE_BYTES] = (q0 & 0xff) as u8
  gq_run_q8(buf8, GQ_OUT, GQ_IN, v8, GQ_V_SHIFT24, NQ_SHIFT_Q24, dst8)
  gv_check("T8e the byte restored, row 0 matches again (the neg-control mutated only what it said)" as *u8, gq_all_rows_match(dst8, wref8, v8, GQ_IN, GQ_OUT), ctr)
  // T8f-T8h (search R0s-b, 2026-09-17): the CONSUMER-side proof of the __q8blk_i16dot builtin. The compiler side
  // (nx_cc_equiv_gate + the feature program) proved planted lanes and the extreme blocks; here the builtin route
  // (nq8_dot_row) and the scalar sign-extend twin (nq8_dot_row_scalar) read the SAME block stream through the same
  // signature and must agree on every row -- on the small fixture and across the 592-block wide rows, so every
  // 32-code block lands in the two 16-lane halves. T8h moves one activation lane and requires the builtin's
  // answer to move, so the agreement teeth cannot pass by both twins returning a constant.
  let col16s: *u8 = sys_mmap(GQ_IN*2)
  var kk: i64 = 0
  while kk < GQ_IN { nf_pack2(col16s, kk, v8[kk]); kk = kk + 1 }
  let w16s: *u8 = sys_mmap(GQ_Q8_VALS*2)
  let nblk8: i64 = GQ_IN/GQ_Q8_VALS
  var agree8: i64 = 1
  var firstdot: i64 = 0
  var rr: i64 = 0
  while rr < GQ_OUT {
      let ds: i64 = nq8_dot_row_scalar(buf8, rr*nblk8*GQ_Q8_BYTES, nblk8, col16s, w16s)
      let db: i64 = nq8_dot_row(buf8, rr*nblk8*GQ_Q8_BYTES, nblk8, col16s, w16s)
      if rr == 0 { firstdot = ds }
      if ds != db { agree8 = 0 }
      rr = rr + 1
  }
  gv_puts("  T8f row0 scalar_dot=" as *u8); gv_num(firstdot); gv_puts(" rows=" as *u8); gv_num(GQ_OUT); gv_puts(" blocks_per_row=" as *u8); gv_num(nblk8); gv_puts("\n" as *u8)
  gv_check("T8f __q8blk_i16dot builtin block dot equals the scalar sign-extend twin on every small-fixture row" as *u8, agree8, ctr)
  gv_check("T8f fixture-reached: the row-0 block dot is non-zero" as *u8, firstdot != 0, ctr)
  let col16w: *u8 = sys_mmap(GQ_WIDE_IN*2)
  kk = 0
  while kk < GQ_WIDE_IN { nf_pack2(col16w, kk, vw8[kk]); kk = kk + 1 }
  let nblkw: i64 = GQ_WIDE_IN/GQ_Q8_VALS
  var agreew: i64 = 1
  rr = 0
  while rr < GQ_WIDE_OUT {
      let dsw: i64 = nq8_dot_row_scalar(bufw8, rr*nblkw*GQ_Q8_BYTES, nblkw, col16w, w16s)
      let dbw: i64 = nq8_dot_row(bufw8, rr*nblkw*GQ_Q8_BYTES, nblkw, col16w, w16s)
      if dsw != dbw { agreew = 0 }
      rr = rr + 1
  }
  gv_check("T8g builtin equals the scalar twin across the 592-block wide rows (every block through the two 16-lane halves)" as *u8, agreew, ctr)
  nf_pack2(col16s, 5, v8[5] + 1)
  let dmoved: i64 = nq8_dot_row(buf8, 0, nblk8, col16s, w16s)
  gv_check("neg-control-T8h one activation lane changed moves the builtin row-0 dot (the twin comparison is not vacuous)" as *u8, dmoved != firstdot, ctr)
295
  // T0 fixture census (model-level teeth live in the serve gate; here only: can the fused path be exercised at all?)
  let have: i64 = gk_exists(model)
  gv_need("resident fixture model present (Q4_K_M or Q8_0)" as *u8, have, ctr)
  if have == 1 {
      let cnt: *i64 = sys_mmap(8*8) as *i64
      let crc: i64 = gq_census(model, cnt)
      gv_puts("  T0 census tensors=" as *u8); gv_num(cnt[4]); gv_puts(" q4k=" as *u8); gv_num(cnt[0]); gv_puts(" q6k=" as *u8); gv_num(cnt[1]); gv_puts(" q5k=" as *u8); gv_num(cnt[2]); gv_puts(" other=" as *u8); gv_num(cnt[3]); gv_puts(" q8_0=" as *u8); gv_num(cnt[5]); gv_puts("\n" as *u8)
      gv_check("T0 fixture parses through the file map (sys_map_file + nx_gguf_parse)" as *u8, crc == 0, ctr)
      gv_check("T0 fixture carries Q4_K or Q8_0 tensors, so an in-place route is reachable on a real model" as *u8, (cnt[0] + cnt[5]) > 0, ctr)
      gv_check("T0 census partition sums to tensor_count" as *u8, cnt[0]+cnt[1]+cnt[2]+cnt[3] == cnt[4], ctr)
  }
  return gv_verdict("nx_nofloat_q4k_gate" as *u8, ctr, "resident-Q4_K matvec exact on both shift regimes and the 7B ffn width; route decision and fallback identity proven; census is the fixture-reached witness for the serve gate" as *u8)
308}
nx_nofloat_q4k_gate.nx source

`nx_nofloat_q4k_gate.nx` source
