nx_nofloat_blockfloat_gate.nx source
↩ module page · 118 lines · 6312 B
1// nx_nofloat_blockfloat_gate.nx -- BLOCK-FLOAT quant rung: per-block power-of-2-scaled integer = MXFP8's
2// dynamic-range fix, but DETERMINISTIC. "Use it for building": grounded in the operator's banked arithmetic
3// (knowledge/research/2026-06-24-arithmetic-grounding-blockfloat.md + knowledge/library/arith_fp8_training.txt --
4// FP8's case against INT8 is dynamic range; MXFP8's fix is per-block(32) power-of-2 scale in E8M0). Power-of-2 =
5// integer shift = exact + associative, so we get FP8's range advantage WHILE keeping the bit-exact determinism moat.
6// Proves the FORMAT UPGRADE per-tensor INT8 -> per-block float:
7// criteria:
8// 1 block-float round-trips the small block EXACTLY (its block scale e=0): reconstructed == original
9// 2 EXCEED (MEASURED): total reconstruction error block-float < per-tensor on a mixed-magnitude tensor
10// 3 DETERMINISTIC: quantize twice -> bit-identical mantissas + scales (vs float MXFP8 non-determinism)
11// 4 per-tensor scaling DESTROYED the small block (-> all 0); block-float PRESERVED it (the super-weight fix)
12// expect_exit: 0 license_tier: ORIGINAL
13import "nx_syscalls.nx"
14import "nx_gate_verdict.nx"
15
16func bf_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
17func bf_putn(v: i64) -> i64 {
18 let b: *u8 = sys_mmap(28); var m: i64 = v
19 if m < 0 { m = 0 - m; sys_write(1, "-" as *u8, 1) }
20 let t: *u8 = sys_mmap(28); var k: i64 = 0
21 if m == 0 { t[0] = 48 as u8; k = 1 }
22 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
23 var i: i64 = 0
24 while i < k { b[i] = t[k - 1 - i]; i = i + 1 }
25 sys_write(1, b, k); return 0
26}
27func bf_chk(name: *u8, ok: i64) -> i64 {
28 if ok == 1 { bf_puts(" PASS " as *u8); bf_puts(name); bf_puts("\n" as *u8); return 1 }
29 bf_puts(" FAIL " as *u8); bf_puts(name); bf_puts("\n" as *u8); return 0
30}
31func bf_bitlen(x: i64) -> i64 { var b: i64 = 0; var m: i64 = x; while m > 0 { m = m >> 1; b = b + 1 } return b }
32func bf_absdiff(a: i64, b: i64) -> i64 { if a >= b { return a - b } return b - a }
33
34// power-of-2 scale exponent for a block of B non-negative ints: amax >> e fits in M mantissa bits (E8M0 idea).
35func bf_scale(v: *i64, off: i64, B: i64, M: i64) -> i64 {
36 var amax: i64 = 0; var i: i64 = 0
37 while i < B { if v[off + i] > amax { amax = v[off + i] } i = i + 1 }
38 var e: i64 = bf_bitlen(amax) - M
39 if e < 0 { e = 0 }
40 return e
41}
42
43func main() -> i64 {
44 let N: i64 = 8
45 let B: i64 = 4
46 let M: i64 = 4
47 bf_puts("=== BLOCK-FLOAT quant -- per-block power-of-2 scale (MXFP8's range fix, DETERMINISTIC) vs per-tensor INT8 ===\n" as *u8)
48
49 let v: *i64 = sys_mmap(8 * N) as *i64
50 v[0] = 3; v[1] = 5; v[2] = 7; v[3] = 9 // small-magnitude block (fits 4 bits -> e=0)
51 v[4] = 100; v[5] = 200; v[6] = 150; v[7] = 120 // large-magnitude block (needs scaling)
52
53 // ---- BLOCK-FLOAT: per-block scale ----
54 let q_bf: *i64 = sys_mmap(8 * N) as *i64
55 let r_bf: *i64 = sys_mmap(8 * N) as *i64
56 let e_bf: *i64 = sys_mmap(8 * (N / B)) as *i64
57 var blk: i64 = 0
58 while blk < N / B {
59 let off: i64 = blk * B
60 let e: i64 = bf_scale(v, off, B, M)
61 e_bf[blk] = e
62 var i: i64 = 0
63 while i < B { q_bf[off + i] = v[off + i] >> e; r_bf[off + i] = q_bf[off + i] << e; i = i + 1 }
64 blk = blk + 1
65 }
66
67 // ---- PER-TENSOR INT8-style: ONE global scale ----
68 let r_pt: *i64 = sys_mmap(8 * N) as *i64
69 let eg: i64 = bf_scale(v, 0, N, M)
70 var i2: i64 = 0
71 while i2 < N { let q: i64 = v[i2] >> eg; r_pt[i2] = q << eg; i2 = i2 + 1 }
72
73 // ---- reconstruction errors ----
74 var err_bf: i64 = 0
75 var err_pt: i64 = 0
76 var k: i64 = 0
77 while k < N { err_bf = err_bf + bf_absdiff(v[k], r_bf[k]); err_pt = err_pt + bf_absdiff(v[k], r_pt[k]); k = k + 1 }
78
79 bf_puts(" block scales e_bf = [" as *u8); bf_putn(e_bf[0]); bf_puts(", " as *u8); bf_putn(e_bf[1]); bf_puts("] per-tensor scale eg = " as *u8); bf_putn(eg); bf_puts("\n" as *u8)
80 bf_puts(" reconstruction error: BLOCK-FLOAT=" as *u8); bf_putn(err_bf); bf_puts(" PER-TENSOR=" as *u8); bf_putn(err_pt); bf_puts("\n" as *u8)
81 bf_puts(" small block r_bf=[" as *u8); var p: i64 = 0; while p < B { bf_putn(r_bf[p]); bf_puts(" " as *u8); p = p + 1 } bf_puts("] r_pt=[" as *u8); p = 0; while p < B { bf_putn(r_pt[p]); bf_puts(" " as *u8); p = p + 1 } bf_puts("]\n" as *u8)
82
83 // ---- determinism: quantize block-float AGAIN, compare bit-for-bit ----
84 var det_ok: i64 = 1
85 var blk2: i64 = 0
86 while blk2 < N / B {
87 let off2: i64 = blk2 * B
88 let e2: i64 = bf_scale(v, off2, B, M)
89 if e2 != e_bf[blk2] { det_ok = 0 }
90 var j: i64 = 0
91 while j < B { if (v[off2 + j] >> e2) != q_bf[off2 + j] { det_ok = 0 } j = j + 1 }
92 blk2 = blk2 + 1
93 }
94
95 var t1: i64 = 1; var s: i64 = 0
96 while s < B { if r_bf[s] != v[s] { t1 = 0 } s = s + 1 }
97 var t2: i64 = 0; if err_bf < err_pt { t2 = 1 }
98 var t4: i64 = 1; var u: i64 = 0
99 while u < B { if r_pt[u] != 0 { t4 = 0 } u = u + 1 }
100
101 var pass: i64 = 0
102 var total: i64 = 0
103 total = total + 1; pass = pass + bf_chk("T1 block-float round-trips the small block EXACTLY (e=0)" as *u8, t1)
104 total = total + 1; pass = pass + bf_chk("T2 EXCEED: block-float error < per-tensor error (dynamic-range win)" as *u8, t2)
105 total = total + 1; pass = pass + bf_chk("T3 DETERMINISTIC: quantize twice == bit-identical (vs float MXFP8)" as *u8, det_ok)
106 total = total + 1; pass = pass + bf_chk("T4 per-tensor DESTROYED small block (->0); block-float PRESERVED it" as *u8, t4)
107
108 bf_puts("NX-NOFLOAT-BLOCKFLOAT-GATE " as *u8); bf_putn(pass); bf_puts(" / " as *u8); bf_putn(total)
109 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
110 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
111 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
112 let ctr__dry: *i64 = gv_ctr()
113 ctr__dry[0] = pass
114 ctr__dry[1] = total
115 let rc__dry: i64 = gv_verdict("NOFLOAT-BLOCKFLOAT-GATE" as *u8, ctr__dry, "block-float = FP8 dynamic range + bit-exact determinism; the format upgrade)" as *u8)
116 sys_exit(rc__dry)
117 return rc__dry
118}