nx_rule_soundness.nx source

1// nx_rule_soundness.nx -- SOVEREIGN soundness prover for the nx_eqsat rewrite 2// rules. Each rule in nx_eqsat.nx does a union that ASSERTS an algebraic 3// equivalence; this organ PROVES that equivalence holds for ALL inputs in W-bit 4// (mod 2^W) arithmetic, via the winning strategy: 5// 6// (1) WIDTH-INDEPENDENT INDUCTION (reuses the nx_alu_divider_proof_test.nx 7// template): prove a per-element invariant EXHAUSTIVELY at a representative 8// width W, plus a width-independence argument (per_rule comments) that 9// lifts the W=8 machine-check to ANY W. For the SIX width-trivial unary 10// rules {add_zero, sub_self, add_self, and_self, or_zero, mul_one} the 11// lift is genuine: identity-element / group-inverse / per-bit-idempotence / 12// k=1-shift laws DO NOT depend on W. For mul_pow2 it is k-induction with 13// the side-condition k+1<W (base k=0, step *2 == <<1 mod 2^W). 14// 15// (2) EXHAUSTIVE SMALL-WIDTH: enumerate every x in [0,2^W) (and, for mul_pow2, 16// every k in [0,W)) -- a real proof over the rule's full local operand 17// space at W, NOT sampling. 18// 19// (3) nx_triangulate AS INDEPENDENT CROSS-CHECK: two independent gsim legs 20// (LHS-eval, RHS-eval) plus an independent oracle, fed to nx_tri_pass_strict 21// (unanimity, k_min = n_legs). Defense in depth. 22// 23// TWO INDEPENDENT WITNESSES, ANDed (honoring the design's two-witness claim): 24// - WITNESS A (algebraic, SEPARATELY CODED): a NishiLang-native masked-arith 25// computation of the rule's invariant, computed WITHOUT reading the gsim legs 26// (so it is independent of the gsim truncation behavior). Asserts the masked 27// identity directly. 28// - WITNESS B (triangulation over gsim legs): the two netlist evaluators must 29// BOTH equal the masked oracle. 30// A rule vector is CERTIFIED iff WITNESS A holds AND WITNESS B passes. 31// 32// TRUNCATION-GAP DEFENSE (adversarial trap #1): nx_gsim_eval_cell computes a*b, 33// a<<b, a+b, a-b in FULL i64 with ZERO truncation. So this organ MASKS every 34// evaluator output (and the oracle) to (1<<W)-1 BEFORE comparison -- the check 35// then tests the real mod-2^W identity, not a coincidental i64 identity. The 36// algebraic witness also masks. No rule is certified on raw unmasked i64. 37// 38// k>=W BOUNDARY DEFENSE (adversarial trap #2): mul_pow2 fires unbounded in 39// nx_eqsat.nx (NO k<W guard -- owed). For k>=W the identity is FALSE 40// (2^k mod 2^W == 0 so x*2^k mod 2^W == 0 for all x, but x<<k is an out-of-range 41// shift). Masked equality at the boundary is a deceptive 0==0, so the boundary 42// is proven via a SEMANTIC out-of-range witness (nx_rule_shl_wbit returns an 43// out-of-range sentinel for k>=W) that DISAGREES with the all-zero multiply 44// result -- proving the guard is real and locating where it belongs. The gsim's 45// own SHL is NEVER used at k>=W (its x86 count-mask would wrongly return a<<0). 46// 47// SOVEREIGN: no SMT, no foreign oracle, no .sh; evaluates on the trusted gsim 48// organ + native masked arithmetic, all through the pinned NishiLang compiler. 49// license_tier: ORIGINAL 50 51import "nx_alu_divider.nx" 52import "nx_triangulate.nx" 53 54// Rule ids (data-driven dispatch; no magic numbers at call sites). 55const NX_RS_ADD_ZERO: i64 = 1 56const NX_RS_SUB_SELF: i64 = 2 57const NX_RS_ADD_SELF: i64 = 3 58const NX_RS_AND_SELF: i64 = 4 59const NX_RS_OR_ZERO: i64 = 5 60const NX_RS_MUL_ONE: i64 = 6 61 62// Sentinel for an out-of-range W-bit shift (k >= W). Distinct from any real 63// masked value in [0, 2^W), so it can never coincide with a multiply result. 64const NX_RS_OOR: i64 = 0 - 999999 65 66// width-mask helper: (1<<W) - 1 for W in [1,62]. 67func nx_rs_mask(w: i64) -> i64 { return (1 << w) - 1 } 68 69// Reset a single-input gsim with net 0 = x (primary input). Mirrors the green 70// nx_eqsat_rule_proof_test.nx _mk so the proof maps 1:1 onto the template. 71func nx_rs_mk(vals: *i64, cells: *NxGsimCell, g: *NxGsim) -> i64 { 72 g.vals = vals; g.n_nets = 1; g.cells = cells; g.n_cells = 0; return 0 73} 74 75// ---- WITNESS A: native, masked, gsim-INDEPENDENT algebraic invariant. -------- 76// Returns 1 iff the rule's masked identity holds for this x (computed with 77// native `*`/`+`/`-`/`<<`/`&`/`|` reduced mod 2^W). This is a SEPARATE proof 78// path from the gsim legs -- it does not read g.vals at all. 79func nx_rs_witness_a(rule: i64, x: i64, w: i64) -> i64 { 80 let m: i64 = nx_rs_mask(w) 81 let xm: i64 = x & m 82 if rule == NX_RS_ADD_ZERO { 83 if ((xm + 0) & m) == xm { return 1 } return 0 84 } 85 if rule == NX_RS_SUB_SELF { 86 if ((xm - xm) & m) == 0 { return 1 } return 0 87 } 88 if rule == NX_RS_ADD_SELF { 89 // (x + x) mod 2^W == (x << 1) mod 2^W 90 if ((xm + xm) & m) == ((xm << 1) & m) { return 1 } return 0 91 } 92 if rule == NX_RS_AND_SELF { 93 if (xm & xm) == xm { return 1 } return 0 94 } 95 if rule == NX_RS_OR_ZERO { 96 if (xm | 0) == xm { return 1 } return 0 97 } 98 if rule == NX_RS_MUL_ONE { 99 if ((xm * 1) & m) == xm { return 1 } return 0 100 } 101 return 0 102} 103 104// Independent oracle (third source, neither LHS nor RHS netlist), masked. 105// add_zero/and_self/or_zero/mul_one -> x (literal x) 106// sub_self -> 0 (constant) 107// add_self -> 2x by repeated addition (independent of <<) 108func nx_rs_oracle(rule: i64, x: i64, w: i64) -> i64 { 109 let m: i64 = nx_rs_mask(w) 110 let xm: i64 = x & m 111 if rule == NX_RS_SUB_SELF { return 0 } 112 if rule == NX_RS_ADD_SELF { 113 var acc: i64 = 0 114 acc = acc + xm 115 acc = acc + xm // 2x by repeated addition, NOT << and NOT * 116 return acc & m 117 } 118 return xm // add_zero / and_self / or_zero / mul_one 119} 120 121// Build LHS netlist for a unary rule on net 0 = x, run it, return the MASKED out. 122func nx_rs_eval_lhs(rule: i64, x: i64, w: i64, vals: *i64, cells: *NxGsimCell, g: *NxGsim) -> i64 { 123 let m: i64 = nx_rs_mask(w) 124 nx_rs_mk(vals, cells, g) 125 var outn: i64 = 0 126 if rule == NX_RS_ADD_ZERO { 127 let c0: i64 = div_const(g, 0) 128 outn = div_op2(g, NX_GATE_KIND_ADD, 0, c0) 129 } 130 if rule == NX_RS_SUB_SELF { 131 outn = div_op2(g, NX_GATE_KIND_SUB, 0, 0) // x - x (same net) 132 } 133 if rule == NX_RS_ADD_SELF { 134 outn = div_op2(g, NX_GATE_KIND_ADD, 0, 0) // x + x (same net) 135 } 136 if rule == NX_RS_AND_SELF { 137 outn = div_op2(g, NX_GATE_KIND_AND, 0, 0) // x & x 138 } 139 if rule == NX_RS_OR_ZERO { 140 let c0b: i64 = div_const(g, 0) 141 outn = div_op2(g, NX_GATE_KIND_OR, 0, c0b) 142 } 143 if rule == NX_RS_MUL_ONE { 144 let c1: i64 = div_const(g, 1) 145 outn = div_op2(g, NX_GATE_KIND_MUL, 0, c1) 146 } 147 g.vals[0] = x & m 148 if nx_gsim_run(g) != NX_GSIM_OK { return NX_RS_OOR } 149 return g.vals[outn] & m 150} 151 152// Build RHS netlist for a unary rule on net 0 = x, run it, return the MASKED out. 153func nx_rs_eval_rhs(rule: i64, x: i64, w: i64, vals: *i64, cells: *NxGsimCell, g: *NxGsim) -> i64 { 154 let m: i64 = nx_rs_mask(w) 155 nx_rs_mk(vals, cells, g) 156 var outn: i64 = 0 157 if rule == NX_RS_ADD_ZERO { outn = 0 } // RHS = x 158 if rule == NX_RS_AND_SELF { outn = 0 } // RHS = x 159 if rule == NX_RS_OR_ZERO { outn = 0 } // RHS = x 160 if rule == NX_RS_MUL_ONE { outn = 0 } // RHS = x 161 if rule == NX_RS_SUB_SELF { 162 outn = div_const(g, 0) // RHS = const 0 163 } 164 if rule == NX_RS_ADD_SELF { 165 let c1: i64 = div_const(g, 1) 166 outn = div_op2(g, NX_GATE_KIND_SHL, 0, c1) // RHS = x << 1 167 } 168 g.vals[0] = x & m 169 if nx_gsim_run(g) != NX_GSIM_OK { return NX_RS_OOR } 170 return g.vals[outn] & m 171} 172 173// Certify ONE unary-rule vector. Returns 1 iff WITNESS A holds AND WITNESS B 174// (triangulation of the two gsim legs vs the oracle) passes -- BOTH required. 175// The verdict v is written for the 5W1H diagnostic on the first failure. 176func nx_rs_certify_unary(rule: i64, x: i64, w: i64, 177 vals: *i64, cells: *NxGsimCell, g: *NxGsim, 178 legs: *i64, v: *NxTriVerdict) -> i64 { 179 let oracle: i64 = nx_rs_oracle(rule, x, w) 180 let lhs: i64 = nx_rs_eval_lhs(rule, x, w, vals, cells, g) 181 let rhs: i64 = nx_rs_eval_rhs(rule, x, w, vals, cells, g) 182 // WITNESS B: both netlist legs must equal the independent oracle. 183 legs[0] = lhs 184 legs[1] = rhs 185 let b_pass: i64 = nx_tri_pass_strict(legs, 2, oracle, 2, v) 186 // WITNESS A: independent algebraic invariant. 187 let a_ok: i64 = nx_rs_witness_a(rule, x, w) 188 if a_ok != 1 { return 0 } 189 if b_pass != 1 { return 0 } 190 return 1 191} 192 193// ---- mul_pow2 (k-parameterised) --------------------------------------------- 194// In-range theorem: for 0<=k<W, (x * 2^k) mod 2^W == (x << k) mod 2^W. 195// 2^k by repeated doubling (independent of native shift), masked. 196func nx_rs_pow2(k: i64, w: i64) -> i64 { 197 let m: i64 = nx_rs_mask(w) 198 var p: i64 = 1 199 var j: i64 = 0 200 while j < k { p = (p * 2) & m; j = j + 1 } 201 return p & m 202} 203 204// Independent oracle for mul_pow2: (x * 2^k) mod 2^W by k DOUBLINGS of x 205// (neither the MUL node nor the SHL node). 206func nx_rs_mulpow2_oracle(x: i64, k: i64, w: i64) -> i64 { 207 let m: i64 = nx_rs_mask(w) 208 var acc: i64 = x & m 209 var j: i64 = 0 210 while j < k { acc = (acc + acc) & m; j = j + 1 } // double k times 211 return acc & m 212} 213 214// WITNESS A for mul_pow2 (algebraic, gsim-independent), masked. 215func nx_rs_mulpow2_witness_a(x: i64, k: i64, w: i64) -> i64 { 216 let m: i64 = nx_rs_mask(w) 217 let xm: i64 = x & m 218 let pw: i64 = nx_rs_pow2(k, w) 219 if ((xm * pw) & m) == ((xm << k) & m) { return 1 } 220 return 0 221} 222 223// A faithful W-bit logical shifter: k>=W is OUT OF RANGE (sentinel), NOT a 224// wrapped x86 shift. This is the semantic ground truth the boundary witness 225// compares against (NEVER the gsim SHL, whose count mask would lie at k>=W). 226func nx_rule_shl_wbit(x: i64, k: i64, w: i64) -> i64 { 227 if k < 0 { return NX_RS_OOR } 228 if k >= w { return NX_RS_OOR } 229 let m: i64 = nx_rs_mask(w) 230 return ((x & m) << k) & m 231} 232 233// Certify ONE in-range mul_pow2 vector (0<=k<W). WITNESS A (algebraic) AND 234// WITNESS B (gsim legs MUL vs SHL vs oracle) must BOTH hold. 235func nx_rs_certify_mulpow2(x: i64, k: i64, w: i64, 236 vals: *i64, cells: *NxGsimCell, g: *NxGsim, 237 legs: *i64, v: *NxTriVerdict) -> i64 { 238 let m: i64 = nx_rs_mask(w) 239 let pw: i64 = nx_rs_pow2(k, w) 240 let oracle: i64 = nx_rs_mulpow2_oracle(x, k, w) 241 242 // LEG A: MUL x 2^k via netlist. 243 nx_rs_mk(vals, cells, g) 244 let cpw: i64 = div_const(g, pw) 245 let prod: i64 = div_op2(g, NX_GATE_KIND_MUL, 0, cpw) 246 g.vals[0] = x & m 247 if nx_gsim_run(g) != NX_GSIM_OK { return 0 } 248 let lhs: i64 = g.vals[prod] & m 249 250 // LEG B: SHL x k via netlist (k<W so the gsim count is in range). 251 nx_rs_mk(vals, cells, g) 252 let ck: i64 = div_const(g, k) 253 let shft: i64 = div_op2(g, NX_GATE_KIND_SHL, 0, ck) 254 g.vals[0] = x & m 255 if nx_gsim_run(g) != NX_GSIM_OK { return 0 } 256 let rhs: i64 = g.vals[shft] & m 257 258 legs[0] = lhs 259 legs[1] = rhs 260 let b_pass: i64 = nx_tri_pass_strict(legs, 2, oracle, 2, v) 261 let a_ok: i64 = nx_rs_mulpow2_witness_a(x, k, w) 262 if a_ok != 1 { return 0 } 263 if b_pass != 1 { return 0 } 264 return 1 265} 266 267// Boundary witness: for k>=W the rule is UNSOUND. Returns 1 iff this (x,k) 268// DEMONSTRATES the unsoundness, i.e. the true semantic multiply result 269// ((x*2^k) mod 2^W, which is 0 since 2^k mod 2^W == 0) DISAGREES with a 270// faithful W-bit shift of x by k (which is OUT OF RANGE). This is where the 271// owed k<W guard belongs. Does NOT use the gsim SHL (count-mask would lie). 272func nx_rs_mulpow2_boundary_unsound(x: i64, k: i64, w: i64) -> i64 { 273 let m: i64 = nx_rs_mask(w) 274 // True semantic multiply mod 2^W: 2^k mod 2^W == 0 for k>=W -> product is 0. 275 let mul_sem: i64 = nx_rs_mulpow2_oracle(x, k, w) // doublings k>=W collapse to 0 276 // Faithful W-bit shift: k>=W is out of range (the rule would emit shl x k 277 // with k>=W -- undefined). It must NOT equal the all-zero multiply result. 278 let shl_sem: i64 = nx_rule_shl_wbit(x, k, w) // == NX_RS_OOR for k>=W 279 if mul_sem != shl_sem { return 1 } // disagreement => unsound => guard needed 280 return 0 281}