nx_eqsat_bw_witness_gate.nx source

1// nx_eqsat_bw_witness_gate.nx -- the BOUNDED-WIDTH TRUNCATION GATE underneath the whole mul_pow2 rule. 2// 3// CLAIM, proven exhaustively: for a W-bit machine with mask = 2^W - 1, 4// ((x * 2^k) & mask) == ((x << k) & mask) for ALL x in [0, 2^W) and ALL k in [0, W). 5// That is the mul-to-shl identity in mod-2^W arithmetic, which is the form the shipping optimizer 6// actually needs: real registers truncate, so an identity holding only over the integers is not the 7// one being relied on. 8// 9// PROMOTED FROM A THROWAWAY 2026-08-14 and RENAMED in the same pass. Its own header called it a 10// throwaway witness, it had NEVER BEEN COMPILED, and its verdict was an exit code nothing could read. 11// A 1,048,576-vector exhaustive check of the semantics every other eqsat proof leans on is not 12// throwaway work -- it is the floor those proofs stand on, and it was treated as scaffolding because 13// of a word in a comment. 14// 15// WHY THE NAME CHANGED: /api/gate_run executes verifiers ONLY and requires a name ending in gate, 16// test or kat -- the bound that stops that route reaching a daemon or deployer. The old name could be 17// built and promoted but never RUN through the gate door, so it would have joined the 18// promoted-but-uninvokable pile. The predecessor path is retired, not deleted. 19// 20// ANTI-VACUITY, WHICH THE ORIGINAL LACKED: `agree == total` is TRUE OVER AN EMPTY SWEEP, and also for 21// a degenerate run where every value is zero -- an equality between two always-zero quantities proves 22// nothing about multiplying or shifting. So the sweep length is asserted against its own arithmetic 23// AND the run must produce non-zero values that COULD have differed. 24// license_tier: ORIGINAL expect_exit: 0 25 26import "nx_syscalls.nx" 27import "nx_gate_verdict.nx" 28 29// Modelled machine width. 16 keeps the exhaustive sweep near 1M vectors (fast) while wide enough that 30// truncation genuinely bites; the identity being proven is width-generic. 31const BW_WIDTH_BITS: i64 = 16 32 33func main() -> i64 { 34 gv_head("nx_eqsat bounded-width gate -- mul-to-shl holds under mod-2^W truncation, exhaustively" as *u8) 35 let ctr: *i64 = gv_ctr() 36 37 var ws: i64 = 0 38 var nn: i64 = 1 39 while ws < BW_WIDTH_BITS { nn = nn * 2; ws = ws + 1 } // nn = 2^W 40 let mask: i64 = nn - 1 41 // Sweep size is DERIVED from the width, never guessed. 42 let expect_total: i64 = nn * BW_WIDTH_BITS 43 44 var total: i64 = 0 45 var agree: i64 = 0 46 var nonzero: i64 = 0 47 var x: i64 = 0 48 while x < nn { 49 var k: i64 = 0 50 while k < BW_WIDTH_BITS { 51 let pw: i64 = (1 << k) 52 let lhs: i64 = (x * pw) & mask // mul x 2^k (truncated) 53 let rhs: i64 = (x << k) & mask // shl x k (truncated) 54 total = total + 1 55 if lhs == rhs { agree = agree + 1 } 56 // A non-zero result is a vector where the two sides had something to disagree about. 57 if lhs != 0 { nonzero = nonzero + 1 } 58 k = k + 1 59 } 60 x = x + 1 61 } 62 63 gv_check("every swept vector agrees under mod-2^W truncation" as *u8, agree == total, ctr) 64 gv_check("the sweep covered the full x-cross-k domain, derived not assumed" as *u8, total == expect_total, ctr) 65 gv_check("the sweep produced non-zero values, so the equality had something to prove" as *u8, nonzero > 0, ctr) 66 // Nor non-zero EVERYWHERE: x=0 and high-k truncations genuinely vanish, so an all-non-zero run 67 // would mean the mask never applied. 68 gv_check("truncation really does zero some vectors, so the mask is load-bearing" as *u8, nonzero < total, ctr) 69 70 return gv_verdict("nx_eqsat_bw_witness_gate" as *u8, ctr, 71 "exhaustive mod-2^W proof of the mul-to-shl identity over the full x-cross-k domain, with denominator and non-vacuity teeth so a million agreements cannot come from an unexercised sweep" as *u8) 72}