nx_nofloat_mxfp4_gate.nx source

1// nx_nofloat_mxfp4_gate.nx -- gate for the no-float MXFP4 dequant (authored ON nx_gate_verdict). 2// Proves OCP MX v1.0 conformance in pure integer: E2M1 magnitude table, sign, E8M0 power-of-2 scale, 3// full 32-elem block, determinism. 4// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 5import "nx_nofloat_mxfp4.nx" 6import "nx_gate_verdict.nx" 7import "nx_syscalls.nx" 8 9func main() -> i64 { 10 let ctr: *i64 = gv_ctr() 11 gv_head("nx_nofloat_mxfp4 gate -- OCP MXFP4 (E2M1 + E8M0 shared scale) dequant, pure integer" as *u8) 12 13 // scale e=127 -> 2^0 = 1.0 14 // T1 magnitude table: 0010(idx2)=1.0=65536 ; 0111(idx7)=6.0=393216 ; 0001(idx1)=0.5=32768 ; 0000=0 15 var t1: i64 = 0 16 if mx_e2m1(2, 127) == 65536 { if mx_e2m1(7, 127) == 393216 { if mx_e2m1(1, 127) == 32768 { if mx_e2m1(0, 127) == 0 { t1 = 1 } } } } 17 gv_check("T1 E2M1 magnitude table {0,.5,1,1.5,2,3,4,6} exact in Q16" as *u8, t1, ctr) 18 19 // T2 sign bit: 1010 (sign=1, idx2=1.0) -> -65536 20 var t2: i64 = 0 21 if mx_e2m1(10, 127) == (0 - 65536) { if mx_e2m1(15, 127) == (0 - 393216) { t2 = 1 } } 22 gv_check("T2 sign bit negates (1010 -> -1.0, 1111 -> -6.0)" as *u8, t2, ctr) 23 24 // T3 E8M0 scale: e=128 (2^1) doubles 1.0->2.0=131072 ; e=126 (2^-1) halves 1.0->0.5=32768 ; e=129 -> 4.0 25 var t3: i64 = 0 26 if mx_e2m1(2, 128) == 131072 { if mx_e2m1(2, 126) == 32768 { if mx_e2m1(2, 129) == 262144 { t3 = 1 } } } 27 gv_check("T3 E8M0 shared scale = power-of-2 shift (e-127): doubles/halves correctly" as *u8, t3, ctr) 28 29 // T3b NaN scale (0xFF) -> 0 (uninitialised block) 30 var t3b: i64 = 0 31 if mx_e2m1(2, 255) == 0 { t3b = 1 } 32 gv_check("T3b E8M0 NaN scale (0xFF) -> 0 (fail-safe uninitialised)" as *u8, t3b, ctr) 33 34 // T4 full 32-elem block: 16 bytes each 0x21 (low nib 1=0.5, high nib 2=1.0), scale e=127 35 let buf: *u8 = sys_mmap(64) 36 var i: i64 = 0 37 while i < 16 { buf[i] = 0x21 as u8; i = i + 1 } 38 buf[16] = 127 as u8 39 let out: *i64 = sys_mmap(MX_BLK * 8) as *i64 40 mx_block(buf, 0, 16, out) 41 var t4: i64 = 0 42 // even idx = low nib (1 -> 0.5 = 32768), odd idx = high nib (2 -> 1.0 = 65536) 43 if out[0] == 32768 { if out[1] == 65536 { if out[30] == 32768 { if out[31] == 65536 { t4 = 1 } } } } 44 gv_check("T4 full 32-element block dequant (16 packed bytes + E8M0 scale)" as *u8, t4, ctr) 45 46 // T5 deterministic re-run 47 let out2: *i64 = sys_mmap(MX_BLK * 8) as *i64 48 mx_block(buf, 0, 16, out2) 49 var t5: i64 = 0 50 var d: i64 = 0 51 var k: i64 = 0 52 while k < MX_BLK { if out[k] != out2[k] { d = 1 } k = k + 1 } 53 if d == 0 { t5 = 1 } 54 gv_check("T5 deterministic (two block dequants bit-identical)" as *u8, t5, ctr) 55 56 let rc: i64 = gv_verdict("NOFLOAT-MXFP4-GATE" as *u8, ctr, "OCP MXFP4 E2M1+E8M0 pure-integer dequant: magnitude table, sign, power-of-2 scale, block, deterministic" as *u8) 57 sys_exit(rc) 58 return rc 59}