_i16dot_minrepro.nx source

1// _i16dot_minrepro.nx -- the feature program for __i16_dot (R0r-b, 2026-09-17): the compiler's whole-chunk integer 2// dot, a:*i16[n] . b:*i16[n] -> i64 with the int32x8 accumulator register-resident and one horizontal sum per call. 3// 4// nx_cc_equiv_gate builds this with the CHALLENGER only (a baseline that lacks the builtin cannot), runs it, and 5// requires exit 0. Every arm is checked against an exact scalar reference read back from the same bytes: 6// exit 1 = the 1024-lane signed ramp disagrees with the scalar sum 7// exit 2 = the smallest legal call (one 16-lane trip) disagrees 8// exit 3 = a planted +1 in one lane of a does not move the dot by exactly that lane of b (a lane was skipped) 9// exit 4 = the reference is zero (a vacuous fixture; the ramp is built so it cannot be) 10// exit 5 = the sum of eight int32 lanes exceeds int32 and the builtin's int64 horizontal sum lost it 11// The contract the builtin holds the caller to: n is a POSITIVE multiple of 16, and n is bounded so no int32 lane 12// overflows (nx_nofloat_llm keeps n at NF_CHUNK_K = 1024 lanes of 12-bit values). 13// 14// expect_exit: 0 15// license_tier: ORIGINAL 16 17import "nx_syscalls.nx" 18 19const MR_N: i64 = 1024 20const MR_HALF: i64 = 512 21const MR_PLANT: i64 = 777 22const MR_W: i64 = 16 23const MR_I16_MOD: i64 = 65536 24const MR_I16_HALF: i64 = 32768 25const MR_BYTE: i64 = 256 26const MR_BIG: i64 = 32767 // the widest i16: 1024 lanes of 32767*32767 sum past int32 (exit 5 guards the hsum) 27 28func mr_put(p: *u8, i: i64, v: i64) -> i64 { var u: i64 = v; if u < 0 { u = u + MR_I16_MOD } p[i*2] = (u % MR_BYTE) as u8; p[i*2+1] = ((u / MR_BYTE) % MR_BYTE) as u8; return 0 } 29func mr_get(p: *u8, i: i64) -> i64 { var u: i64 = (p[i*2] as i64) + (p[i*2+1] as i64) * MR_BYTE; if u >= MR_I16_HALF { u = u - MR_I16_MOD } return u } 30func mr_ref(a: *u8, b: *u8, n: i64) -> i64 { var s: i64 = 0; var i: i64 = 0; while i < n { s = s + mr_get(a, i) * mr_get(b, i); i = i + 1 } return s } 31 32func main() -> i64 { 33 let a: *u8 = sys_mmap(MR_N * 2) 34 let b: *u8 = sys_mmap(MR_N * 2) 35 var i: i64 = 0 36 while i < MR_N { mr_put(a, i, i + 1 - MR_HALF); mr_put(b, i, MR_HALF - i); i = i + 1 } 37 let ref: i64 = mr_ref(a, b, MR_N) 38 if ref == 0 { return 4 } 39 let got: i64 = __i16_dot(a, b, MR_N) 40 if got != ref { return 1 } 41 if __i16_dot(a, b, MR_W) != mr_ref(a, b, MR_W) { return 2 } 42 mr_put(a, MR_PLANT, mr_get(a, MR_PLANT) + 1) 43 if __i16_dot(a, b, MR_N) - got != mr_get(b, MR_PLANT) { return 3 } 44 // one 16-lane trip of the widest i16 puts two products of MR_BIG*MR_BIG in each int32 lane (2,147,352,578, just 45 // under 2^31), and the eight-lane total, 16 * MR_BIG^2 = 17,178,820,624, only fits in int64: the hsum must widen. 46 i = 0 47 while i < MR_W { mr_put(a, i, MR_BIG); mr_put(b, i, MR_BIG); i = i + 1 } 48 if __i16_dot(a, b, MR_W) != MR_W * MR_BIG * MR_BIG { return 5 } 49 return 0 50}