nx_gguf_dequant_kat_gate.nx source
↩ module page · 180 lines · 8786 B
1// nx_gguf_dequant_kat_gate.nx -- KATs for the DEBT-EATEN quant family (2026-07-15): every newly added
2// block dequant (Q4_0/Q4_1/Q5_1/Q5_K/Q3_K/Q2_K/F16/BF16) is checked against HAND-DERIVED expected values
3// on hand-constructed blocks (known bits in -> exact Q16 out), plus the loud-fail contract and the
4// canonical stride table. The fleet's live types (F32/Q5_0/Q8_0/Q4_K/Q6_K) keep their existing gates;
5// this gate covers the types no current model ships -- so the NEXT model never hits a silent hole.
6// T1 Q4_0 / Q4_1 / Q5_1 KATs exact T2 F16 / BF16 KATs exact
7// T3 Q5_K KAT exact (scale-pair unpack + qh high-bit + dmin) T4 Q3_K KAT exact (6-bit scales, hmask -4)
8// T5 Q2_K KAT exact (sc/min nibbles) T6 LOUD-FAIL: unknown type -> -1 from stride/to_q16/row
9// expect_exit: 0 license_tier: ORIGINAL No hw writes (Rule 26).
10import "nx_syscalls.nx"
11import "nx_tier.nx"
12import "nx_le.nx"
13import "nx_tensor.nx"
14import "nx_gguf.nx"
15import "nx_gguf_load.nx"
16import "nx_gguf_meta.nx"
17import "nx_nofloat_llm.nx"
18import "nx_gate_verdict.nx"
19
20func kq_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
21func kq_n(v: i64) -> i64 {
22 var m: i64 = v
23 if m < 0 { kq_w("-" as *u8); m = 0 - m }
24 let t: *u8 = sys_mmap(24)
25 var k: i64 = 0
26 if m == 0 { t[0] = 48 as u8; k = 1 }
27 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
28 let o: *u8 = sys_mmap(24)
29 var i: i64 = 0
30 while i < k { o[i] = t[k - 1 - i]; i = i + 1 }
31 sys_write(1, o, k)
32 return 0
33}
34func kq_chk(name: *u8, got: i64, want: i64, fails: *i64) -> i64 {
35 if got != want {
36 fails[0] = fails[0] + 1
37 kq_w(" MISMATCH " as *u8); kq_w(name); kq_w(": got " as *u8); kq_n(got); kq_w(" want " as *u8); kq_n(want); kq_w("\n" as *u8)
38 }
39 return 0
40}
41
42func main() -> i64 {
43 kq_w("=== NX-GGUF-DEQUANT-KAT -- hand-derived KATs for the eaten quant-family debt ===\n" as *u8)
44 let blk: *u8 = sys_mmap(512)
45 let out: *i64 = sys_mmap(512*8) as *i64
46 let f: *i64 = sys_mmap(8) as *i64
47 f[0] = 0
48 var pass: i64 = 0
49 var ttl: i64 = 0
50
51 // ---- T1: Q4_0 / Q4_1 / Q5_1 ----
52 var z: i64 = 0
53 while z < 512 { blk[z] = 0 as u8; z = z + 1 }
54 blk[0] = 0 as u8
55 blk[1] = 60 as u8 // f16 1.0 = 0x3C00 (LE: 00 3C)
56 blk[2] = 33 as u8 // qs[0] = 0x21
57 blk[17] = 255 as u8 // qs[15] = 0xFF
58 q4_0_block(blk, 0, 32, out)
59 kq_chk("q4_0 out[0]" as *u8, out[0], 0-458752, f) // (1-8)*65536
60 kq_chk("q4_0 out[16]" as *u8, out[16], 0-393216, f) // (2-8)*65536
61 kq_chk("q4_0 out[15]" as *u8, out[15], 458752, f) // (15-8)*65536
62 kq_chk("q4_0 out[31]" as *u8, out[31], 458752, f)
63 z = 0
64 while z < 512 { blk[z] = 0 as u8; z = z + 1 }
65 blk[1] = 60 as u8 // d=1.0
66 blk[3] = 60 as u8 // m=1.0
67 blk[4] = 33 as u8 // qs[0]=0x21
68 q4_1_block(blk, 0, 32, out)
69 kq_chk("q4_1 out[0]" as *u8, out[0], 131072, f) // 1*65536+65536
70 kq_chk("q4_1 out[16]" as *u8, out[16], 196608, f) // 2*65536+65536
71 z = 0
72 while z < 512 { blk[z] = 0 as u8; z = z + 1 }
73 blk[1] = 60 as u8 // d=1.0, m=0
74 blk[4] = 255 as u8
75 blk[5] = 255 as u8
76 blk[6] = 255 as u8
77 blk[7] = 255 as u8 // qh = 0xFFFFFFFF -> +16 everywhere
78 blk[8] = 33 as u8 // qs[0]=0x21
79 q5_1_block(blk, 0, 32, out)
80 kq_chk("q5_1 out[0]" as *u8, out[0], 1114112, f) // (1|16)*65536
81 kq_chk("q5_1 out[16]" as *u8, out[16], 1179648, f) // (2|16)*65536
82 ttl = ttl + 1
83 if f[0] == 0 { pass = pass + 1; kq_w(" T1 Q4_0/Q4_1/Q5_1 KATs: PASS\n" as *u8) } else { kq_w(" T1: FAIL\n" as *u8) }
84
85 // ---- T2: F16 / BF16 rows through dequant_to_q16 ----
86 f[0] = 0
87 blk[0] = 0 as u8
88 blk[1] = 60 as u8 // f16 1.0
89 blk[2] = 0 as u8
90 blk[3] = 192 as u8 // f16 0xC000 = -2.0
91 dequant_to_q16(blk, 0, NX_GGML_TYPE_F16, 2, out)
92 kq_chk("f16 1.0" as *u8, out[0], 65536, f)
93 kq_chk("f16 -2.0" as *u8, out[1], 0-131072, f)
94 blk[0] = 128 as u8
95 blk[1] = 63 as u8 // bf16 0x3F80 = 1.0
96 blk[2] = 0 as u8
97 blk[3] = 192 as u8 // bf16 0xC000 = -2.0
98 dequant_to_q16(blk, 0, NX_GGML_TYPE_BF16, 2, out)
99 kq_chk("bf16 1.0" as *u8, out[0], 65536, f)
100 kq_chk("bf16 -2.0" as *u8, out[1], 0-131072, f)
101 ttl = ttl + 1
102 if f[0] == 0 { pass = pass + 1; kq_w(" T2 F16/BF16 KATs: PASS\n" as *u8) } else { kq_w(" T2: FAIL\n" as *u8) }
103
104 // ---- T3: Q5_K (d=1.0, dmin=0; scales[0]=1 scales[1]=2; qh[0] bit0; qs[0]=0x53) ----
105 f[0] = 0
106 z = 0
107 while z < 512 { blk[z] = 0 as u8; z = z + 1 }
108 blk[1] = 60 as u8 // d = 1.0 -> d24 = 16777216
109 blk[4] = 1 as u8 // scales[0]: is0 sc=1
110 blk[5] = 2 as u8 // scales[1]: is1 sc=2
111 blk[16] = 1 as u8 // qh[0] bit0 set (u1=1 for j=0)
112 blk[48] = 83 as u8 // qs[0] = 0x53: lo=3 hi=5
113 q5k_block(blk, 0, 256, out)
114 kq_chk("q5k out[0]" as *u8, out[0], 1245184, f) // 1*(3+16)*65536
115 kq_chk("q5k out[32]" as *u8, out[32], 655360, f) // 2*5*65536 (u2 bit clear)
116 kq_chk("q5k out[64]" as *u8, out[64], 0, f) // scales[2]=0
117 ttl = ttl + 1
118 if f[0] == 0 { pass = pass + 1; kq_w(" T3 Q5_K KAT: PASS\n" as *u8) } else { kq_w(" T3: FAIL\n" as *u8) }
119
120 // ---- T4: Q3_K (d=1.0; sc(0)=33 via b0=1,b8=2 -> sc-32=1; sc(1)=1 -> -31; hmask bits) ----
121 f[0] = 0
122 z = 0
123 while z < 512 { blk[z] = 0 as u8; z = z + 1 }
124 blk[109] = 60 as u8 // d @108 f16 1.0 (LE 00 3C)
125 blk[96] = 1 as u8 // scales b[0]=1 (is0 lo=1)
126 blk[104] = 2 as u8 // scales b[8]=2 (is0 hb=2) -> sc0 = 1|(2<<4) = 33 -> sc-32 = 1
127 blk[97] = 1 as u8 // scales b[1]=1 -> is1 (k=1): lo=b[1]&15=1, hb=b[9]&3=0 -> sc=1 -> -31
128 blk[0] = 1 as u8 // hmask[0] bit0 SET -> no -4 for y[0]
129 blk[32] = 2 as u8 // qs[0] = 2 -> q=2 at shift 0
130 blk[48] = 1 as u8 // qs[16] = 1 -> q=1 for the second 16-group
131 blk[16] = 1 as u8 // hmask[16] bit0 SET -> no -4 for y[16]
132 q3k_block(blk, 0, 256, out)
133 kq_chk("q3k out[0]" as *u8, out[0], 131072, f) // 1*2*65536 (hbit set)
134 kq_chk("q3k out[1]" as *u8, out[1], 0-262144, f) // 1*(0-4)*65536 (hbit clear)
135 kq_chk("q3k out[16]" as *u8, out[16], 0-2031616, f) // (-31)*1*65536
136 ttl = ttl + 1
137 if f[0] == 0 { pass = pass + 1; kq_w(" T4 Q3_K KAT: PASS\n" as *u8) } else { kq_w(" T4: FAIL\n" as *u8) }
138
139 // ---- T5: Q2_K (d=1.0 dmin=1.0; scales[0]=0x21 -> sc=1 m=2; scales[1]=0x01 -> sc=1 m=0) ----
140 f[0] = 0
141 z = 0
142 while z < 512 { blk[z] = 0 as u8; z = z + 1 }
143 blk[81] = 60 as u8 // d @80 = 1.0
144 blk[83] = 60 as u8 // dmin @82 = 1.0
145 blk[0] = 33 as u8 // scales[0] = 0x21: sc=1 m=2
146 blk[1] = 1 as u8 // scales[1] = 0x01: sc=1 m=0
147 blk[16] = 3 as u8 // qs[0] = 3
148 blk[32] = 2 as u8 // qs[16] = 2
149 q2k_block(blk, 0, 256, out)
150 kq_chk("q2k out[0]" as *u8, out[0], 65536, f) // 1*3*65536 - 2*65536
151 kq_chk("q2k out[16]" as *u8, out[16], 131072, f) // 1*2*65536 - 0
152 ttl = ttl + 1
153 if f[0] == 0 { pass = pass + 1; kq_w(" T5 Q2_K KAT: PASS\n" as *u8) } else { kq_w(" T5: FAIL\n" as *u8) }
154
155 // ---- T6: loud-fail + stride table ----
156 f[0] = 0
157 kq_chk("to_q16 ty99" as *u8, dequant_to_q16(blk, 0, 99, 4, out), 0-1, f)
158 let tmp6: *i64 = sys_mmap(4096*8) as *i64
159 kq_chk("row ty99" as *u8, dequant_row(blk, 0, 99, 0, 32, out, tmp6), 0-1, f)
160 let vb: *i64 = sys_mmap(16) as *i64
161 kq_chk("stride ty99" as *u8, nf_type_stride(99, vb), 0-1, f)
162 nf_type_stride(NX_GGML_TYPE_Q5_K, vb)
163 kq_chk("stride q5k vpb" as *u8, vb[0], 256, f)
164 kq_chk("stride q5k bpb" as *u8, vb[1], 176, f)
165 nf_type_stride(NX_GGML_TYPE_Q2_K, vb)
166 kq_chk("stride q2k bpb" as *u8, vb[1], 84, f)
167 ttl = ttl + 1
168 if f[0] == 0 { pass = pass + 1; kq_w(" T6 loud-fail + stride table: PASS\n" as *u8) } else { kq_w(" T6: FAIL\n" as *u8) }
169
170 kq_w("NX-GGUF-DEQUANT-KAT passed " as *u8); kq_n(pass); kq_w("/" as *u8); kq_n(ttl)
171 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
172 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
173 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
174 let ctr__dry: *i64 = gv_ctr()
175 ctr__dry[0] = pass
176 ctr__dry[1] = ttl
177 let rc__dry: i64 = gv_verdict("GGUF-DEQUANT-KAT-GATE" as *u8, ctr__dry, "mainstream quant family covered, unknown types fail LOUD)" as *u8)
178 sys_exit(rc__dry)
179 return rc__dry
180}