nx_nofloat_q6k_gate.nx source
↩ module page · 155 lines · 8668 B
1// nx_nofloat_q6k_gate.nx -- sovereign Q6_K -> Q16 integer dequant (unlocks Qwen embeddings + LM head).
2// Q4_K_M stores token_embd.weight and output.weight as Q6_K, which the substrate didn't ship -- so a faithful
3// no-float forward needs this dequant. GGML Q6_K super-block = 256 values in 210 bytes: ql[128] (low 4 bits),
4// qh[64] (high 2 bits), scales[16] (int8 per-16 sub-scale), d (f16 super-scale). value = d * scale * (q-32),
5// q the assembled 6-bit quant -- done PURE INTEGER (f16->Q16 by bit-decode, then integer mults) so no float
6// touches the weights (deterministic). Proven: (a) KAT scale path (scales=0 -> 0; scales=1 -> uniform -32);
7// (b) KAT 6-bit unpack (ql=0x0F,qh=0x03 -> q=31 at y[0]); (c) the REAL Qwen Q6_K tensor dequants to sane
8// integer weights; (d) deterministic. No hw writes (Rule 26). expect_exit: 0 license_tier: ORIGINAL
9import "nx_syscalls.nx"
10import "nx_tier.nx"
11import "nx_le.nx"
12import "nx_tensor.nx"
13import "nx_gguf.nx"
14import "nx_gguf_load.nx"
15import "nx_gate_verdict.nx"
16
17func q6_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
18func q6_num(v: i64) -> i64 { let b: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(1,"-" as *u8,1)} 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 }
19
20// f16 -> Q16 fixed-point (pure-integer bit-decode). f16 = sign(1) exp(5) mant(10), bias 15.
21func q6_f16_to_q16(h: i64) -> i64 {
22 let sign: i64 = (h>>15)&1
23 let exp: i64 = (h>>10)&31
24 let mant: i64 = h&1023
25 var v: i64 = 0
26 if exp==0 { v = mant >> 8 }
27 else { if exp==31 { v = 2147483647 } else { let m: i64=1024+mant; let e: i64=exp-9; if e>=0 { v=m<<e } else { v=m>>(0-e) } } }
28 if sign==1 { v = 0-v }
29 return v
30}
31func q6_i8(buf: *u8, off: i64) -> i64 { let v: i64 = nx_le_read_u8(buf, off); if v>=128 { return v-256 } return v }
32
33// Dequant one Q6_K super-block (210 bytes at super_off) -> up to n_values Q16 ints into out.
34func q6k_block_to_q16(buf: *u8, super_off: i64, n_values: i64, out: *i64) -> i64 {
35 let d_q16: i64 = q6_f16_to_q16(nx_le_read_u16(buf, super_off + 208))
36 var half: i64 = 0
37 while half < 2 {
38 let bql: i64 = super_off + half*64
39 let bqh: i64 = super_off + 128 + half*32
40 let bsc: i64 = super_off + 192 + half*8
41 let yb: i64 = half*128
42 var l: i64 = 0
43 while l < 32 {
44 let is: i64 = l/16
45 let ql_l: i64 = nx_le_read_u8(buf, bql + l)
46 let ql_l32: i64 = nx_le_read_u8(buf, bql + l + 32)
47 let qh_l: i64 = nx_le_read_u8(buf, bqh + l)
48 let q1: i64 = ((ql_l & 15) | (((qh_l >> 0) & 3) << 4)) - 32
49 let q2: i64 = ((ql_l32 & 15) | (((qh_l >> 2) & 3) << 4)) - 32
50 let q3: i64 = ((ql_l >> 4) | (((qh_l >> 4) & 3) << 4)) - 32
51 let q4: i64 = ((ql_l32 >> 4) | (((qh_l >> 6) & 3) << 4)) - 32
52 let sc1: i64 = q6_i8(buf, bsc + is + 0)
53 let sc2: i64 = q6_i8(buf, bsc + is + 2)
54 let sc3: i64 = q6_i8(buf, bsc + is + 4)
55 let sc4: i64 = q6_i8(buf, bsc + is + 6)
56 if yb+l+0 < n_values { out[yb+l+0] = d_q16 * sc1 * q1 }
57 if yb+l+32 < n_values { out[yb+l+32] = d_q16 * sc2 * q2 }
58 if yb+l+64 < n_values { out[yb+l+64] = d_q16 * sc3 * q3 }
59 if yb+l+96 < n_values { out[yb+l+96] = d_q16 * sc4 * q4 }
60 l = l + 1
61 }
62 half = half + 1
63 }
64 return 0
65}
66
67func main() -> i64 {
68 q6_puts("Sovereign Q6_K -> Q16 integer dequant (unlocks Qwen embeddings + LM head)\n\n" as *u8)
69
70 // ===== KAT on a synthetic 210-byte Q6_K block =====
71 let blk: *u8 = sys_mmap(256)
72 let outk: *i64 = sys_mmap(256*8) as *i64
73 var i: i64=0
74 // config A: d=1.0, scales=0, ql/qh=0 -> all outputs 0 (scale multiply)
75 while i<210 { blk[i]=0 as u8; i=i+1 }
76 nx_le_write_u16(blk, 208, 0x3C00) // d = 1.0 (f16)
77 q6k_block_to_q16(blk, 0, 256, outk)
78 var a_ok: i64=0
79 if outk[0]==0 { if outk[100]==0 { if outk[255]==0 { a_ok=1 } } }
80 // config B: scales=1 (all 16), ql/qh=0 -> every q=-32, value = d*1*(-32) = -2097152
81 i=0; while i<16 { blk[192+i]=1 as u8; i=i+1 }
82 q6k_block_to_q16(blk, 0, 256, outk)
83 var b_ok: i64=0
84 if outk[0]==(0-2097152) { if outk[128]==(0-2097152) { if outk[255]==(0-2097152) { b_ok=1 } } }
85 // config C: scales=1, ql[0]=0x0F, qh[0]=0x03 -> y[0] q1=(15|48)-32=31 -> 31*65536=2031616
86 blk[0]=0x0F as u8; blk[128]=0x03 as u8
87 q6k_block_to_q16(blk, 0, 256, outk)
88 var c_ok: i64=0
89 if outk[0]==2031616 { if outk[1]==(0-2097152) { if outk[32]==(0-2097152) { c_ok=1 } } }
90
91 // ===== REAL model: dequant the first Q6_K tensor (embeddings/output in Q4_K_M) =====
92 let path: *u8 = "/home/elderwesto/nx_stage/nx_real_model.gguf\x00" as *u8
93 let len_out: *i64 = sys_mmap(8) as *i64
94 len_out[0]=0
95 let buf: *u8 = sys_read_file(path, len_out)
96 var q6_idx: i64 = 0 - 1
97 var q6_dim0: i64 = 0
98 var q6_dim1: i64 = 0
99 var nz: i64 = 0
100 var maxabs: i64 = 0
101 var det_ok: i64 = 0
102 let outr: *i64 = sys_mmap(256*8) as *i64
103 let outr2: *i64 = sys_mmap(256*8) as *i64
104 if buf != (0 as *u8) { if len_out[0] > 1000 {
105 let hdr: *NxGgufHeader = sys_mmap(NX_GGUF_HDR_BYTES) as *NxGgufHeader
106 if nx_gguf_parse(buf, len_out[0], hdr) == NX_GGUF_OK {
107 var j: nx_int = 0
108 while j < hdr.n_tensors {
109 let ti: *NxGgufTensorInfo = nx_gguf_tensor_at(hdr, j)
110 if ti.ggml_type == NX_GGML_TYPE_Q6_K { if q6_idx < 0 { q6_idx = j } }
111 j = j + 1
112 }
113 if q6_idx >= 0 {
114 let tq: *NxGgufTensorInfo = nx_gguf_tensor_at(hdr, q6_idx)
115 q6_dim0 = tq.dim_0
116 q6_dim1 = tq.dim_1
117 let dq_off: i64 = hdr.data_off + tq.offset
118 q6k_block_to_q16(buf, dq_off, 256, outr)
119 q6k_block_to_q16(buf, dq_off, 256, outr2)
120 var d2: i64 = 0
121 var p: i64 = 0
122 while p < 256 {
123 if outr[p] != 0 { nz = nz + 1 }
124 var av: i64 = outr[p]; if av<0 { av=0-av }
125 if av > maxabs { maxabs = av }
126 if outr[p] != outr2[p] { d2 = d2 + 1 }
127 p = p + 1
128 }
129 if d2 == 0 { det_ok = 1 }
130 }
131 }
132 } }
133
134 q6_puts(" KAT: scales=0 -> all 0 ("); q6_num(a_ok); q6_puts(") scales=1 -> all -2097152 ("); q6_num(b_ok); q6_puts(") unpack ql=0x0F,qh=0x03 -> y0="); q6_num(outk[0]); q6_puts(" (want 2031616, ok="); q6_num(c_ok); q6_puts(")\n");
135 q6_puts(" REAL Q6_K tensor: idx="); q6_num(q6_idx); q6_puts(" dims=["); q6_num(q6_dim0); q6_puts(","); q6_num(q6_dim1); q6_puts("] nonzero="); q6_num(nz); q6_puts("/256 maxabs="); q6_num(maxabs); q6_puts("\n");
136 q6_puts(" real weights (Q16) [0..6] = ["); var w: i64=0; while w<6 { q6_num(outr[w]); if w<5 { q6_puts(", ") } w=w+1 } q6_puts("]\n\n");
137
138 var pass: i64=0
139 var ttl: i64=0
140 ttl=ttl+1; q6_puts(" T1 KAT scale path correct (scales=0 -> all 0; scales=1 -> uniform d*(-32)): "); if a_ok==1 { if b_ok==1 { pass=pass+1; q6_puts("PASS\n") } else { q6_puts("FAIL\n") } } else { q6_puts("FAIL\n") }
141 ttl=ttl+1; q6_puts(" T2 KAT 6-bit unpack correct (ql/qh assemble to q=31 at y[0] = 2031616): "); if c_ok==1 { pass=pass+1; q6_puts("PASS\n") } else { q6_puts("FAIL\n") }
142 ttl=ttl+1; q6_puts(" T3 REAL Qwen Q6_K tensor dequantized to sane integer weights (nonzero>=128, bounded): "); if q6_idx>=0 { if nz>=128 { if maxabs<1073741824 { pass=pass+1; q6_puts("PASS\n") } else { q6_puts("FAIL\n") } } else { q6_puts("FAIL\n") } } else { q6_puts("FAIL\n") }
143 ttl=ttl+1; q6_puts(" T4 DETERMINISTIC (pure-integer dequant, re-run bit-identical): "); if det_ok==1 { pass=pass+1; q6_puts("PASS\n") } else { q6_puts("FAIL\n") }
144
145 q6_puts("NX-NOFLOAT-Q6K-GATE passed "); q6_num(pass); q6_puts("/"); q6_num(ttl)
146 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
147 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
148 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
149 let ctr__dry: *i64 = gv_ctr()
150 ctr__dry[0] = pass
151 ctr__dry[1] = ttl
152 let rc__dry: i64 = gv_verdict("NOFLOAT-Q6K-GATE" as *u8, ctr__dry, "sovereign Q6_K->Q16 dequant, KAT-correct + real Qwen embedding loads -- embeddings/LM-head unlocked)" as *u8)
153 sys_exit(rc__dry)
154 return rc__dry
155}