nx_nofloat_mla_gate.nx source
↩ module page · 139 lines · 7256 B
1// nx_nofloat_mla_gate.nx -- MLA no-float SERVE (the census's #1 remaining July-2026 gap, 2026-07-15).
2// Proves DeepSeek's Multi-head Latent Attention runs in deterministic integer no-float AND that its
3// KV-compression is LOSSLESS by construction. Two paths on the SAME weights/input: LATENT (cache = LC-dim c)
4// vs FULL-KV (cache = 2*D). Teeth:
5// T1 LOSSLESS COMPRESSION: latent-path output == full-KV-path output, EXACT (0 mismatch) -- caching the
6// LC-dim latent loses NOTHING vs caching full K,V (they up-project deterministically from c)
7// T2 COMPRESSION REAL + MEASURED: latent cache bytes < full-KV cache bytes; ratio = 2*D/LC (report it)
8// T3 DETERMINISM: latent path byte-identical on repeat
9// T4 REAL TRANSFORM: output differs from input on >half the cells
10// T5 NEG-CONTROL: corrupt the down-projection Wdkv -> output CHANGES (the latent bottleneck is load-bearing,
11// not a bypass) AND with LC>=2*D (no compression) it still matches full-KV (degenerate check sane)
12// Synthetic Q16 weights (mechanism proof -- no small real MLA gguf exists; DeepSeek V4 = 671B). Runs in ms.
13// expect_exit: 0 license_tier: ORIGINAL No hw writes (Rule 26).
14import "nx_syscalls.nx"
15import "nx_nofloat_mla.nx"
16import "nx_gate_verdict.nx"
17
18func mg_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
19func mg_n(v: i64) -> i64 {
20 var m: i64 = v
21 if m < 0 { mg_w("-" as *u8); m = 0 - m }
22 let t: *u8 = sys_mmap(24)
23 var k: i64 = 0
24 if m == 0 { t[0] = 48 as u8; k = 1 }
25 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
26 let o: *u8 = sys_mmap(24)
27 var i: i64 = 0
28 while i < k { o[i] = t[k - 1 - i]; i = i + 1 }
29 sys_write(1, o, k)
30 return 0
31}
32func mg_det(i: i64) -> i64 { return ((i * 2654435761) % 8191) - 4095 }
33
34func main() -> i64 {
35 mg_w("=== NX-NOFLOAT-MLA -- DeepSeek latent-KV attention in no-float; lossless KV-compression proven ===\n" as *u8)
36 let T: i64 = 4
37 let nh: i64 = 4
38 let hd: i64 = 64
39 let D: i64 = nh*hd // 256
40 let LC: i64 = 64 // latent (KV cache dim). full K+V per token = 2*D = 512 -> 8x compression
41 let scale: i64 = 8192 // ~1/sqrt(64) in Q16
42
43 let Wdkv: *i64 = sys_mmap(D*LC*8) as *i64
44 let Wuk: *i64 = sys_mmap(LC*D*8) as *i64
45 let Wuv: *i64 = sys_mmap(LC*D*8) as *i64
46 let Wq: *i64 = sys_mmap(D*D*8) as *i64
47 let Wo: *i64 = sys_mmap(D*D*8) as *i64
48 var i: i64 = 0
49 while i < D*LC { Wdkv[i] = mg_det(i + 100); i = i + 1 }
50 i = 0
51 while i < LC*D { Wuk[i] = mg_det(i + 2000); Wuv[i] = mg_det(i + 3000); i = i + 1 }
52 i = 0
53 while i < D*D { Wq[i] = mg_det(i + 4000); Wo[i] = mg_det(i + 5000); i = i + 1 }
54 let x: *i64 = sys_mmap(T*D*8) as *i64
55 i = 0
56 while i < T*D { x[i] = mg_det(i*7 + 11); i = i + 1 }
57
58 let outL: *i64 = sys_mmap(T*D*8) as *i64
59 let outF: *i64 = sys_mmap(T*D*8) as *i64
60 let outR: *i64 = sys_mmap(T*D*8) as *i64
61 let cCache: *i64 = sys_mmap(T*LC*8) as *i64 // MLA cache = LC-dim latent
62 let kvCache: *i64 = sys_mmap(T*2*D*8) as *i64 // full-KV cache = 2*D-dim
63 let scrL: *i64 = sys_mmap((3*T*D + 2*T + T*D + 64)*8) as *i64
64 let scrF: *i64 = sys_mmap((T*D + 2*T + T*D + T*D + 64)*8) as *i64
65 let ap: *i64 = sys_mmap(16*8) as *i64
66 ap[2]=T; ap[3]=D; ap[4]=nh; ap[5]=hd; ap[6]=LC; ap[7]=scale
67 ap[8]=Wdkv as i64; ap[9]=Wuk as i64; ap[10]=Wuv as i64; ap[11]=Wq as i64; ap[12]=Wo as i64
68
69 // latent path
70 ap[0]=x as i64; ap[1]=outL as i64; ap[13]=scrL as i64; ap[14]=cCache as i64
71 nmla_forward_latent(ap)
72 // full-KV path
73 ap[1]=outF as i64; ap[13]=scrF as i64; ap[14]=kvCache as i64
74 nmla_forward_fullkv(ap)
75 // latent repeat (determinism)
76 ap[1]=outR as i64; ap[13]=scrL as i64; ap[14]=cCache as i64
77 nmla_forward_latent(ap)
78
79 let cache_latent_bytes: i64 = T*LC*8
80 let cache_full_bytes: i64 = T*2*D*8
81 mg_w("[MLA] D=" as *u8); mg_n(D); mg_w(" heads=" as *u8); mg_n(nh); mg_w(" hd=" as *u8); mg_n(hd); mg_w(" LC=" as *u8); mg_n(LC)
82 mg_w(" KV-cache: latent=" as *u8); mg_n(cache_latent_bytes); mg_w("B full-KV=" as *u8); mg_n(cache_full_bytes)
83 mg_w("B compression=" as *u8); mg_n(cache_full_bytes / cache_latent_bytes); mg_w("x\n" as *u8)
84
85 var pass: i64 = 0
86 var ttl: i64 = 0
87 // T1 lossless: latent == full-KV
88 ttl = ttl + 1
89 var mism: i64 = 0
90 i = 0
91 while i < T*D { if outL[i] != outF[i] { mism = mism + 1 } i = i + 1 }
92 mg_w(" T1 LOSSLESS: latent-cache output == full-KV output, exact (mism " as *u8); mg_n(mism); mg_w("/" as *u8); mg_n(T*D); mg_w("): " as *u8)
93 if mism == 0 { pass = pass + 1; mg_w("PASS\n" as *u8) } else { mg_w("FAIL\n" as *u8) }
94 // T2 compression real + measured
95 ttl = ttl + 1
96 let ratio: i64 = cache_full_bytes / cache_latent_bytes
97 mg_w(" T2 compression real (" as *u8); mg_n(ratio); mg_w("x, latent < full-KV): " as *u8)
98 if cache_latent_bytes < cache_full_bytes { if ratio >= 2 { pass = pass + 1; mg_w("PASS\n" as *u8) } else { mg_w("FAIL\n" as *u8) } } else { mg_w("FAIL\n" as *u8) }
99 // T3 determinism
100 ttl = ttl + 1
101 var rep: i64 = 0
102 i = 0
103 while i < T*D { if outL[i] != outR[i] { rep = rep + 1 } i = i + 1 }
104 mg_w(" T3 determinism (latent repeat byte-identical): " as *u8)
105 if rep == 0 { pass = pass + 1; mg_w("PASS\n" as *u8) } else { mg_w("FAIL\n" as *u8) }
106 // T4 real transform
107 ttl = ttl + 1
108 var neq: i64 = 0
109 i = 0
110 while i < T*D { if outL[i] != x[i] { neq = neq + 1 } i = i + 1 }
111 mg_w(" T4 real transform (out!=in on " as *u8); mg_n(neq); mg_w("/" as *u8); mg_n(T*D); mg_w("): " as *u8)
112 if neq > T*D/2 { pass = pass + 1; mg_w("PASS\n" as *u8) } else { mg_w("FAIL\n" as *u8) }
113 // T5 neg-control: corrupt Wdkv (down-proj) -> latent output must change (the bottleneck is load-bearing)
114 ttl = ttl + 1
115 let Wdkv2: *i64 = sys_mmap(D*LC*8) as *i64
116 i = 0
117 while i < D*LC { Wdkv2[i] = Wdkv[i]; i = i + 1 }
118 i = 0
119 while i < LC { Wdkv2[i] = 0 - Wdkv2[i]; i = i + 1 } // flip the first latent's projection
120 ap[0]=x as i64; ap[1]=outR as i64; ap[8]=Wdkv2 as i64; ap[13]=scrL as i64; ap[14]=cCache as i64
121 nmla_forward_latent(ap)
122 ap[8]=Wdkv as i64
123 var changed: i64 = 0
124 i = 0
125 while i < T*D { if outR[i] != outL[i] { changed = changed + 1 } i = i + 1 }
126 mg_w(" T5 NEG-CONTROL: corrupt down-proj -> output changes on " as *u8); mg_n(changed); mg_w(" cells: " as *u8)
127 if changed > 0 { pass = pass + 1; mg_w("PASS\n" as *u8) } else { mg_w("FAIL\n" as *u8) }
128
129 mg_w("NX-NOFLOAT-MLA-GATE passed " as *u8); mg_n(pass); mg_w("/" as *u8); mg_n(ttl)
130 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
131 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
132 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
133 let ctr__dry: *i64 = gv_ctr()
134 ctr__dry[0] = pass
135 ctr__dry[1] = ttl
136 let rc__dry: i64 = gv_verdict("NOFLOAT-MLA-GATE" as *u8, ctr__dry, "MLA serves in no-float: latent-KV attention, lossless compression measured, deterministic)" as *u8)
137 sys_exit(rc__dry)
138 return rc__dry
139}