_q8blkdot_minrepro.nx source

1// _q8blkdot_minrepro.nx -- the feature program for __q8blk_i16dot (search R0s-b, 2026-09-17): one Q8_0 block's dot, 2// codes:*i8[32] . x:*i16[32] -> i64, the int8 codes sign-extended IN REGISTER (vpmovsxbw) so the block-native kernel 3// never stores an i16 copy of the weights. 4// 5// nx_cc_equiv_gate builds this with the CHALLENGER only (a baseline that lacks the builtin cannot), runs it, and 6// requires exit 0. Every arm is checked against an exact scalar reference read back from the same bytes: 7// exit 1 = the 32-lane signed ramp disagrees with the scalar sum 8// exit 2 = a planted +1 in one code lane does not move the dot by exactly that lane of x (a lane was skipped) 9// exit 3 = a planted +1 in one x lane does not move the dot by exactly that lane's code (the other operand) 10// exit 4 = the reference is zero (a vacuous fixture; the ramps are built so it cannot be) 11// exit 5 = the widest legal block (every code 127, every x 32767) disagrees: 32 * 127 * 32767 = 133,153,088 12// exit 6 = the most negative code (-128) against the most negative x (-32768) disagrees: the sign extension is 13// two's complement on both sides, 32 * 4,194,304 = 134,217,728 14// The contract the builtin holds the caller to: exactly 32 lanes, codes are int8 two's complement, x is i16. 15// 16// expect_exit: 0 17// license_tier: ORIGINAL 18 19import "nx_syscalls.nx" 20 21const MR_LANES: i64 = 32 22const MR_HALF: i64 = 16 23const MR_PLANT: i64 = 21 24const MR_I16_MOD: i64 = 65536 25const MR_I16_HALF: i64 = 32768 26const MR_BYTE: i64 = 256 27const MR_I8_HALF: i64 = 128 28const MR_CODE_MAX: i64 = 127 29const MR_CODE_MIN: i64 = 0 - 128 30const MR_X_MAX: i64 = 32767 31const MR_X_MIN: i64 = 0 - 32768 32const MR_X_STEP: i64 = 1000 33 34func mr_put16(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 } 35func mr_get16(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 } 36func mr_put8(p: *u8, i: i64, v: i64) -> i64 { var u: i64 = v; if u < 0 { u = u + MR_BYTE } p[i] = (u % MR_BYTE) as u8; return 0 } 37func mr_get8(p: *u8, i: i64) -> i64 { var u: i64 = (p[i] as i64) & 0xff; if u >= MR_I8_HALF { u = u - MR_BYTE } return u } 38func mr_ref(codes: *u8, x: *u8) -> i64 { var s: i64 = 0; var i: i64 = 0; while i < MR_LANES { s = s + mr_get8(codes, i) * mr_get16(x, i); i = i + 1 } return s } 39 40func main() -> i64 { 41 let codes: *u8 = sys_mmap(MR_LANES) 42 let x: *u8 = sys_mmap(MR_LANES * 2) 43 var i: i64 = 0 44 while i < MR_LANES { mr_put8(codes, i, i - MR_HALF + 1); mr_put16(x, i, (MR_HALF - i) * MR_X_STEP + 7); i = i + 1 } 45 let ref: i64 = mr_ref(codes, x) 46 if ref == 0 { return 4 } 47 let got: i64 = __q8blk_i16dot(codes, x) 48 if got != ref { return 1 } 49 mr_put8(codes, MR_PLANT, mr_get8(codes, MR_PLANT) + 1) 50 if __q8blk_i16dot(codes, x) - got != mr_get16(x, MR_PLANT) { return 2 } 51 let got2: i64 = __q8blk_i16dot(codes, x) 52 mr_put16(x, MR_PLANT, mr_get16(x, MR_PLANT) + 1) 53 if __q8blk_i16dot(codes, x) - got2 != mr_get8(codes, MR_PLANT) { return 3 } 54 i = 0 55 while i < MR_LANES { mr_put8(codes, i, MR_CODE_MAX); mr_put16(x, i, MR_X_MAX); i = i + 1 } 56 if __q8blk_i16dot(codes, x) != MR_LANES * MR_CODE_MAX * MR_X_MAX { return 5 } 57 i = 0 58 while i < MR_LANES { mr_put8(codes, i, MR_CODE_MIN); mr_put16(x, i, MR_X_MIN); i = i + 1 } 59 if __q8blk_i16dot(codes, x) != MR_LANES * MR_CODE_MIN * MR_X_MIN { return 6 } 60 return 0 61}