nx_f32_vec_gate.nx source

1// nx_f32_vec_gate.nx -- KAT for the hardware-f32 vec3 PART (R3), built + run through the 2// SOVEREIGN compiler (nx_cc_sovereign now carries f32). Multi-value KAT: a faked/constant 3// f32 implementation cannot produce 32, 25, 5, [0,0,1], 3 AND a signed -4 all at once, so 4// distinct-correct results = real hardware float composing into vec3. exit 0 = GREEN. AUTHOR=ORGAN. 5import "nx_syscalls.nx" 6import "nx_f32_hw.nx" 7import "nx_f32.nx" 8 9func main() -> i64 { 10 let d: i64 = v3_dot(f32_of(1), f32_of(2), f32_of(3), f32_of(4), f32_of(5), f32_of(6)) 11 if f32_int(d) != 32 { return 1 } // 4+10+18 12 if f32_int(v3_lensq(f32_of(3), f32_of(4), f32_of(0))) != 25 { return 2 } // 9+16+0 13 if f32_int(f32_sub(f32_of(7), f32_of(2))) != 5 { return 3 } // 7-2 14 let out: *i64 = sys_mmap(24) as *i64 15 v3_cross(f32_of(1), f32_of(0), f32_of(0), f32_of(0), f32_of(1), f32_of(0), out) 16 if f32_int(out[0]) != 0 { return 4 } 17 if f32_int(out[1]) != 0 { return 5 } 18 if f32_int(out[2]) != 1 { return 6 } // x cross y = z 19 if f32_int(f32_div(f32_of(6), f32_of(2))) != 3 { return 7 } // 6/2 20 // signed control: negate one component -> 4+10-18 = -4 (proves real SIGNED float, not magnitude) 21 let dn: i64 = v3_dot(f32_of(1), f32_of(2), f32_neg(f32_of(3)), f32_of(4), f32_of(5), f32_of(6)) 22 if f32_int(dn) != (0 - 4) { return 8 } 23 24 // DIFFERENTIAL: hardware SSE f32 (__f32_*) must equal the independent i64 soft-float 25 // IEEE-754 (nx_f32.nx) BIT-FOR-BIT (same binary32 layout). Two implementations agreeing 26 // = no-false-green proof the hardware path is conformant, not just self-consistent. 27 let x: i64 = f32_of(6) 28 let y: i64 = f32_of(7) 29 if __f32_mul(x, y) != nx_f32_mul(x, y) { return 9 } // 42.0f, both paths identical bits 30 if __f32_add(x, y) != nx_f32_add(x, y) { return 10 } // 13.0f 31 let half: i64 = __f32_div(f32_of(1), f32_of(2)) // 0.5f (fractional) 32 if __f32_mul(half, x) != nx_f32_mul(half, x) { return 11 } // 3.0f 33 34 // mat4 KAT (the projection workhorse): identity*v = v; diag(2,3,4,1)*[1,1,1,1] = [2,3,4,1]; 35 // diag * identity = diag (exercises m4_mul). 36 let m: *i64 = sys_mmap(128) as *i64 37 let v: *i64 = sys_mmap(32) as *i64 38 let r4: *i64 = sys_mmap(32) as *i64 39 m4_identity(m) 40 v[0] = f32_of(1); v[1] = f32_of(2); v[2] = f32_of(3); v[3] = f32_of(4) 41 m4_vec4(m, v, r4) 42 if f32_int(r4[0]) != 1 { return 12 } 43 if f32_int(r4[1]) != 2 { return 13 } 44 if f32_int(r4[2]) != 3 { return 14 } 45 if f32_int(r4[3]) != 4 { return 15 } 46 m[0] = f32_of(2); m[5] = f32_of(3); m[10] = f32_of(4) // -> diag(2,3,4,1) 47 v[0] = f32_of(1); v[1] = f32_of(1); v[2] = f32_of(1); v[3] = f32_of(1) 48 m4_vec4(m, v, r4) 49 if f32_int(r4[0]) != 2 { return 16 } 50 if f32_int(r4[1]) != 3 { return 17 } 51 if f32_int(r4[2]) != 4 { return 18 } 52 if f32_int(r4[3]) != 1 { return 19 } 53 let mi: *i64 = sys_mmap(128) as *i64 54 let mp: *i64 = sys_mmap(128) as *i64 55 m4_identity(mi) 56 m4_mul(m, mi, mp) // diag * identity = diag 57 if f32_int(mp[0]) != 2 { return 20 } 58 if f32_int(mp[5]) != 3 { return 21 } 59 if f32_int(mp[10]) != 4 { return 22 } 60 61 // ===== IEEE-CLASS DIFFERENTIAL (added 2026-08-23) ========================= 62 // WHY THIS SECTION EXISTS. The differential above was TRUE and NARROW: it 63 // compared the two paths on three tame values (6, 7, 0.5) and could not have 64 // seen an edge-class divergence. An exhaustive 16x16 probe over every IEEE 65 // class (_offc_probe_f32equiv.nx) measured 254/256 agreeing BIT-FOR-BIT and 66 // exactly 2 differing -- so the narrow green was not wrong, it was blind. 67 // These teeth assert the classes ELEMENT-WISE, never as a count: a count can 68 // pass while the wrong members agree. 69 let z_p: i64 = 0 // +0 0x00000000 70 let z_n: i64 = 2147483648 // -0 0x80000000 71 let one: i64 = 1065353216 // 1.0 0x3F800000 72 let inf_p: i64 = 2139095040 // +inf 0x7F800000 73 let inf_n: i64 = 4286578688 // -inf 0xFF800000 74 let nan_q: i64 = 2143289344 // qNaN 0x7FC00000 75 let sub_lo: i64 = 1 // min subnormal 0x00000001 76 let sub_hi: i64 = 8388607 // max subnormal 0x007FFFFF 77 let nrm_lo: i64 = 8388608 // min normal 0x00800000 78 let nrm_hi: i64 = 2139095039 // max normal 0x7F7FFFFF 79 let ulp24: i64 = 855638016 // 2^-24 0x33000000 80 let ulp23: i64 = 872415232 // 2^-23 0x34000000 81 82 // Rounding-sensitive: these two REFUTE the double-rounding hazard. If OP_FADD 83 // lowered through f64 (the `addsd` observation) and round-tripped, 1.0+2^-24 and 84 // 1.0+2^-23 would diverge. They must not. 85 if __f32_add(one, ulp24) != nx_f32_add(one, ulp24) { return 23 } 86 if __f32_add(one, ulp23) != nx_f32_add(one, ulp23) { return 24 } 87 // Subnormals: the other place an f64 detour or a flush-to-zero would show. 88 if __f32_add(sub_lo, sub_lo) != nx_f32_add(sub_lo, sub_lo) { return 25 } 89 if __f32_add(sub_hi, sub_lo) != nx_f32_add(sub_hi, sub_lo) { return 26 } 90 if __f32_add(sub_hi, nrm_lo) != nx_f32_add(sub_hi, nrm_lo) { return 27 } 91 // Signed zeros: +0 + -0 must be +0 under round-to-nearest on BOTH paths. 92 if __f32_add(z_p, z_n) != nx_f32_add(z_p, z_n) { return 28 } 93 if __f32_add(z_n, z_n) != nx_f32_add(z_n, z_n) { return 29 } 94 // Overflow to infinity. 95 if __f32_add(nrm_hi, nrm_hi) != nx_f32_add(nrm_hi, nrm_hi) { return 30 } 96 // Infinity with a finite operand, and NaN propagation. 97 if __f32_add(inf_p, one) != nx_f32_add(inf_p, one) { return 31 } 98 if __f32_add(nan_q, one) != nx_f32_add(nan_q, one) { return 32 } 99 100 // ===== THE ONE DECLARED DIVERGENCE, AND THE ANTI-VACUITY TOOTH ============ 101 // inf + (-inf) is NaN on BOTH paths but they differ in the NaN SIGN BIT: 102 // the soft-float returns a fixed POSITIVE qNaN (NX_F32_NAN_RAW = 0x7FC00000); 103 // x86 returns its default qNaN, which is NEGATIVE (0xFFC00000). 104 // IEEE-754 DOES NOT SPECIFY THE SIGN OF A NaN RESULT, so neither is wrong -- 105 // this is a difference that must be DECLARED rather than DISCOVERED. 106 let d_sw: i64 = nx_f32_add(inf_p, inf_n) 107 let d_hw: i64 = __f32_add(inf_p, inf_n) 108 // Both must be NaN by CLASS. nx_f32_classify reads only the exponent and 109 // mantissa fields -- it never touches the sign bit -- so every consumer that 110 // detects NaN through the estate's own classifier is structurally blind to 111 // this divergence. That is what makes the difference safe, and it is asserted 112 // here rather than assumed. 113 if nx_f32_classify(d_sw) != NX_F32_CLS_NAN { return 33 } 114 if nx_f32_classify(d_hw) != NX_F32_CLS_NAN { return 34 } 115 // ANTI-VACUITY. The two arms must be GENUINELY DIFFERENT IMPLEMENTATIONS. 116 // This tooth is the proof: if someone re-points nx_f32_add's body at 117 // __f32_add (the pending library swap), the two arms collapse into one, this 118 // divergence vanishes, and THIS TOOTH GOES RED -- which is exactly the 119 // intended behaviour. The swap then cannot ship silently: it must come with a 120 // deliberate edit here, which is the mechanism that makes it DECLARED. 121 // Without this tooth, "the paths agree" would be indistinguishable from 122 // "there is only one path". 123 if d_sw == d_hw { return 35 } 124 if nx_f32_sign(d_sw) != 0 { return 36 } // soft-float NaN is positive 125 if nx_f32_sign(d_hw) != 1 { return 37 } // x86 default NaN is negative 126 127 return 0 128}