nx_f32_matmul_gate.nx source

1// nx_f32_matmul_gate.nx -- KAT proving the SOVEREIGN f32 GEMM is correct (the math-axis foothold). 2// 3// nx_f32_matmul is a bits-up f32 GEMM (no BLAS, no SIMD). For small integers f32 is bit-exact, so a 4// hand-computed integer reference is the exact expected output. This gate is the EVIDENCE that the 5// genesis "math" axis is NOT bare-locked: a sovereign CPU matmul exists + is correct (BLAS-level 6// PERFORMANCE is the remaining open rung). 7// 8// T1 kat-correct : [[1,2],[3,4]] @ [[5,6],[7,8]] == [[19,22],[43,50]] bit-exact 9// N1 teeth : the result does NOT equal a deliberately-wrong matrix (compare has teeth) 10// N2 bad-dim : m=0 -> NX_F32_MM_ERR_BAD_DIM (error handling) 11// 12// GREEN only if all three hold. Evidence -> knowledge/status/f32_matmul_gate.log. 13// Sovereign: imports nx_f32_matmul (-> nx_f32, nx_tier) + nx_framed_append + nx_syscalls. license_tier: ORIGINAL 14import "nx_f32_matmul.nx" 15import "nx_framed_append.nx" 16import "nx_syscalls.nx" 17 18const MMG_LOG: *u8 = "knowledge/status/f32_matmul_gate.log" 19 20func mm_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != 0 as u8 { n = n + 1 } sys_write(1, s, n); return 0 } 21func mm_cat(dst: *u8, off: i64, s: *u8) -> i64 { var i: i64 = 0; while s[i] != 0 as u8 { dst[off + i] = s[i]; i = i + 1 } return off + i } 22func mm_catn(dst: *u8, off: i64, v: i64) -> i64 { 23 var m: i64 = v; var o: i64 = off 24 if m < 0 { m = 0 - m } 25 let t: *u8 = sys_mmap(28); 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 var i: i64 = 0 29 while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 } 30 return o + k 31} 32func mm_eq4(c: *i64, e: *i64) -> i64 { var i: i64 = 0; while i < 4 { if c[i] != e[i] { return 0 } i = i + 1 } return 1 } 33func mm_row(name: *u8, pass: i64) -> i64 { 34 let buf: *u8 = sys_mmap(528) 35 var o: i64 = 0 36 o = mm_cat(buf, o, "MMG row=\x00" as *u8) 37 o = mm_cat(buf, o, name) 38 if pass == 1 { o = mm_cat(buf, o, " verdict=PASS\x00" as *u8) } else { o = mm_cat(buf, o, " verdict=FAIL\x00" as *u8) } 39 buf[o] = 0 as u8 40 fa_appendz(MMG_LOG, buf, 512) 41 mm_puts(" "); mm_puts(name) 42 if pass == 1 { mm_puts(" PASS\n") } else { mm_puts(" FAIL\n") } 43 return 0 44} 45 46func main() -> i64 { 47 mm_puts("f32-matmul gate (sovereign GEMM KAT: the math-axis foothold)\n") 48 // IEEE-754 f32 bit patterns for small ints (bit-exact GEMM): 49 // 1=0x3F800000 2=0x40000000 3=0x40400000 4=0x40800000 50 // 5=0x40A00000 6=0x40C00000 7=0x40E00000 8=0x41000000 51 let A: *i64 = sys_mmap(4 * 8) as *i64 52 A[0] = 0x3F800000; A[1] = 0x40000000; A[2] = 0x40400000; A[3] = 0x40800000 53 let B: *i64 = sys_mmap(4 * 8) as *i64 54 B[0] = 0x40A00000; B[1] = 0x40C00000; B[2] = 0x40E00000; B[3] = 0x41000000 55 let C: *i64 = sys_mmap(4 * 8) as *i64 56 // expected [[19,22],[43,50]]: 19=0x41980000 22=0x41B00000 43=0x422C0000 50=0x42480000 57 let E: *i64 = sys_mmap(4 * 8) as *i64 58 E[0] = 0x41980000; E[1] = 0x41B00000; E[2] = 0x422C0000; E[3] = 0x42480000 59 // wrong: last entry 51.0=0x424C0000 instead of 50.0 60 let W: *i64 = sys_mmap(4 * 8) as *i64 61 W[0] = 0x41980000; W[1] = 0x41B00000; W[2] = 0x422C0000; W[3] = 0x424C0000 62 63 let rc: i64 = nx_f32_matmul(A, B, C, 2, 2, 2) 64 var t1: i64 = 0; if rc == NX_F32_MM_OK { if mm_eq4(C, E) == 1 { t1 = 1 } } 65 var n1: i64 = 0; if mm_eq4(C, W) == 0 { n1 = 1 } 66 let rc2: i64 = nx_f32_matmul(A, B, C, 0, 2, 2) 67 var n2: i64 = 0; if rc2 == NX_F32_MM_ERR_BAD_DIM { n2 = 1 } 68 69 var passes: i64 = 0 70 if t1 == 1 { passes = passes + 1 } 71 if n1 == 1 { passes = passes + 1 } 72 if n2 == 1 { passes = passes + 1 } 73 var green: i64 = 0 74 if passes == 3 { green = 1 } 75 76 mm_row("T1-kat-correct \x00" as *u8, t1) 77 mm_row("N1-compare-teeth\x00" as *u8, n1) 78 mm_row("N2-bad-dim-error\x00" as *u8, n2) 79 80 let vb: *u8 = sys_mmap(528) 81 var o: i64 = 0 82 o = mm_cat(vb, o, "F32-MATMUL verdict=\x00" as *u8) 83 if green == 1 { o = mm_cat(vb, o, "GREEN\x00" as *u8) } else { o = mm_cat(vb, o, "RED\x00" as *u8) } 84 o = mm_cat(vb, o, " passes=\x00" as *u8); o = mm_catn(vb, o, passes); o = mm_cat(vb, o, "/3 END\x00" as *u8) 85 vb[o] = 0 as u8 86 fa_appendz(MMG_LOG, vb, 512) 87 mm_puts(vb); mm_puts("\n") 88 89 if green == 1 { return 0 } 90 return 1 91}