nx_eqsat_membership_proof.nx source

1// nx_eqsat_membership_proof.nx -- MEMBERSHIP-AS-PROOF CERTIFICATE for the eqsat 2// e-graph (the sovereign analogue of ROVER's "verified rewriting": no external 3// SMT oracle; the rewrite rules' soundness + e-class membership IS the proof). 4// 5// THE CLAIM BEING CERTIFIED: 6// Two expressions a, b are equivalent-for-all-inputs (mod 2^W) iff 7// (1) MEMBERSHIP: nx_eqsat_find(g, a) == nx_eqsat_find(g, b) 8// (they landed in the same canonical e-class after saturation), AND 9// (2) PROVENANCE: every union on the rewrite path that merged them used a 10// rule from the PROVEN-SOUND set. 11// When BOTH hold, a == b for all inputs -- membership is a rewrite-path 12// equivalence PROOF, not a heuristic. 13// 14// LIVE CERTIFICATION (mp_certify_live): the engine (nx_eqsat.nx) now logs the 15// citing rule-id of EVERY real merge at its single union chokepoint 16// (nx_eqsat_union_cited) when provenance is enabled (nx_eqsat_enable_prov). The 17// live certifier runs the REAL nx_eqsat_saturate and checks the GLOBAL property 18// "every logged rule-id is in the proven-sound set" + find(a)==find(b) + the log 19// did not overflow (fail-closed). Because every merge flows through the one 20// function that mutates canon, a merge cannot happen without a rule-id being 21// logged -- so an unlogged/un-cited merge (RULE_NONE) poisons the certificate. 22// The gated recorder (mp_prov_admit_union) is RETAINED for the load-bearing 23// negatives' belt-and-suspenders legs + the k<MP_W boundary side-condition. 24// 25// THE SOUND SET (justified, not asserted): a rule is admitted to the sound set 26// ONLY after its W-bit (mod 2^W) algebraic identity is machine-checked 27// EXHAUSTIVELY at a representative width W=8 -- the same width-independent 28// exhaustive-small-width discipline as nx_alu_divider_proof_test.nx. Every 29// evaluator output is MASKED to W bits before comparison (mask = (1<<W)-1) so we 30// prove the true mod-2^W theorem, NOT a coincidental full-i64 identity (the 31// truncation gap). The oracle is also reduced mod 2^W and is independent of both 32// the MUL and SHL nodes (computed by repeated doubling), so the two netlist legs 33// + oracle are three independent witnesses fed through nx_triangulate. 34// 35// LOAD-BEARING (defense in depth): the certificate must FAIL when 36// (NEG-A) a NON-sound rule is used (it is not in the allow-list AND its W=8 37// battery DISAGREES, so it can never enter the sound set), or 38// (NEG-B) the two endpoints are NOT in the same e-class (membership fails). 39// Both negatives are exercised + asserted in the test (FAIL LOUD known answer). 40// 41// SOVEREIGN: no SMT, no foreign oracle, no .sh -- runs on the pinned NishiLang 42// compiler; the gate-sim (nx_gsim) is the only trusted evaluator, the same organ 43// the divider proof trusts. Width W=8 chosen so both legs enumerate cheaply while 44// the per-rule algebraic argument carries width-independence to W=64 (identity / 45// inverse / per-bit law / k-induction with the k<W side-condition). 46// 47// license_tier: ORIGINAL 48 49import "nx_eqsat.nx" 50import "nx_alu_divider.nx" 51import "nx_triangulate.nx" 52const MP_MAGIC_999999: i64 = 999999 53 54// ===== proof width ========================================================= 55 56const MP_W: i64 = 8 // representative width: sweep x in [0, 2^W) 57 58func mp_mask() -> i64 { return (1 << MP_W) - 1 } // (1<<W)-1 = mod-2^W reducer 59func mp_count() -> i64 { return 1 << MP_W } // 2^W vectors per unary rule 60 61// ===== sound-rule identifiers (the proven-sound ALLOW-LIST) ================ 62// 63// These name the rules whose W-bit identity the battery below proves. A union 64// is admissible-in-a-proof ONLY if it cites one of these ids. mul_pow2 is the 65// rule that merges (mul x 2^k) with (shl x k); it is certifiable IN-LIVE only 66// for k < W (the owed k<W guard) -- the certifier checks that side-condition. 67 68const MP_RULE_NONE: i64 = 0 // sentinel: no/unknown rule -> NOT sound 69const MP_RULE_ADD_ZERO: i64 = 1 70const MP_RULE_SUB_SELF: i64 = 2 71const MP_RULE_ADD_SELF: i64 = 3 72const MP_RULE_AND_SELF: i64 = 4 73const MP_RULE_OR_ZERO: i64 = 5 74const MP_RULE_MUL_ONE: i64 = 6 75const MP_RULE_MUL_POW2: i64 = 7 76// CONGRUENCE: structural law of equality (a==b => f(...a...)==f(...b...)). The 77// engine's deferred rebuild cites NX_EQSAT_RULE_CONGRUENCE for every congruence 78// merge; it is admitted to the proven-sound set here. Its soundness needs NO W=8 79// arithmetic battery (unlike the 7 identity rules) -- it is width-independent and 80// fires ONLY on already-canonically-equal children, so the merged e-nodes denote 81// the SAME function of the SAME values. [CANON: Willsey et al, egg, PLDI 2021.] 82const MP_RULE_CONGRUENCE: i64 = 8 83// XOR_SELF: (xor x x) == 0 -- the FIRST rule expressed PURELY as DSL data in the 84// engine (one NxDslRule row). Admitted to the proven-sound set ONLY after the W=8 85// masked exhaustive two-witness battery (mp_battery_xor_self) is unanimous -- the 86// SAME discipline that justified the original 7. Width-independent (a^a=0 holds per 87// bit at any W), so the W=8 machine-check lifts to W=64 (per-bit-law class). The 88// allow-list arm in mp_is_sound_rule is a CONSEQUENCE of that battery passing, 89// asserted in nx_eqsat_dsl_gate_test.nx before any certification trusts id 9. 90const MP_RULE_XOR_SELF: i64 = 9 91// CONSTFOLD: (op c0 c1 ...) with all-constant children == CONST(eval(op, c..)). 92// The engine fires this as an e-class ANALYSIS at node creation (gated, opt-in) and 93// cites NX_EQSAT_RULE_CONSTFOLD at its union chokepoint. Admitted to the proven- 94// sound set because its soundness is BY EVALUATION: the merge relates (op c0 c1) 95// with CONST(nx_gsim_eval_cell(kind(op), c0, c1)) where nx_gsim_eval_cell is the 96// SAME proven op-semantics oracle this organ already trusts (_mp_eval_op_const, 97// line 130). It is width-independent at W=64 (i64 arithmetic IS mod-2^W) AND the 98// engine's nx_eqsat_op_to_gate_kind admits ONLY ops whose gate cell is the proven 99// op semantics (DIV/REM/SHR/SAR/NEG/POPCNT/SELECT refused), so a CONSTFOLD-cited 100// merge can never relate two unequal constants. No separate W=8 arithmetic battery 101// is needed (parallel to how CONGRUENCE is admitted -- the soundness is the oracle, 102// not an algebraic identity per rule). The const-fold gate (nx_eqsat_constfold_test) 103// runs the positive ((add 2 3)->5 certified) + the negatives BEFORE trusting id 10. 104const MP_RULE_CONSTFOLD: i64 = 10 105// SHIFT_MERGE: (shl (shl x i) j) == (shl x (i+j)) for i,j CONST and i+j<W. The SECOND 106// rule expressed PURELY as DSL data in the engine (shape (d): nested SHL-of-SHL). 107// Admitted to the proven-sound set ONLY after the W=8 masked exhaustive two-witness 108// in-range battery (mp_battery_shift_merge) is unanimous AND the i+j>=W boundary is 109// shown unsound (mp_shiftmerge_boundary_unsound) -- the SAME discipline that justified 110// mul_pow2. Width-independent: (a mod 2^W)*2^j == a*2^j mod 2^W (2^j is a factor), so 111// the W=8 machine-check lifts to W=64 by k-induction on (i+j) with the i+j<W guard. 112const MP_RULE_SHIFT_MERGE: i64 = 11 113const MP_RULE_N: i64 = 12 114 115// An UNSOUND probe rule used ONLY by the load-bearing negative test: it claims 116// (mul x 3) == (shl x 1), which is FALSE (3 is not a power of two). It is NOT in 117// the allow-list and its battery DISAGREES, so it can never be certified. 118const MP_RULE_BOGUS_MUL3: i64 = 100 119 120// LOCKSTEP: the engine (nx_eqsat.nx) is the single source of truth for rule-ids; 121// the live log it writes uses NX_EQSAT_RULE_*. These MP_RULE_* values + the 122// allow-list must agree EXACTLY, or a mislabel could let an engine-cited id slip 123// through the certifier under a different name. Returns 1 iff every id matches. 124func mp_rule_ids_lockstep() -> i64 { 125 if MP_RULE_NONE != NX_EQSAT_RULE_NONE { return 0 } 126 if MP_RULE_ADD_ZERO != NX_EQSAT_RULE_ADD_ZERO { return 0 } 127 if MP_RULE_SUB_SELF != NX_EQSAT_RULE_SUB_SELF { return 0 } 128 if MP_RULE_ADD_SELF != NX_EQSAT_RULE_ADD_SELF { return 0 } 129 if MP_RULE_AND_SELF != NX_EQSAT_RULE_AND_SELF { return 0 } 130 if MP_RULE_OR_ZERO != NX_EQSAT_RULE_OR_ZERO { return 0 } 131 if MP_RULE_MUL_ONE != NX_EQSAT_RULE_MUL_ONE { return 0 } 132 if MP_RULE_MUL_POW2 != NX_EQSAT_RULE_MUL_POW2 { return 0 } 133 if MP_RULE_CONGRUENCE != NX_EQSAT_RULE_CONGRUENCE { return 0 } 134 if MP_RULE_XOR_SELF != NX_EQSAT_RULE_XOR_SELF { return 0 } 135 if MP_RULE_CONSTFOLD != NX_EQSAT_RULE_CONSTFOLD { return 0 } 136 if MP_RULE_SHIFT_MERGE != NX_EQSAT_RULE_SHIFT_MERGE { return 0 } 137 if MP_RULE_N != NX_EQSAT_RULE_N { return 0 } 138 return 1 139} 140 141// ===== shared gsim scratch (caller owns the buffers) ======================= 142// 143// A tiny single-input combinational netlist (net 0 = x). _mp_reset rewinds it 144// to "just the primary input" so each evaluation builds a fresh expression. 145 146func _mp_reset(g: *NxGsim, vals: *i64, cells: *NxGsimCell) -> i64 { 147 g.vals = vals; g.n_nets = 1; g.cells = cells; g.n_cells = 0; return 0 148} 149 150// Evaluate a binary op (kind) of (net0=x) and a constant `cst`, masked mod 2^W. 151// Used for the LHS/RHS legs of each rule. Independent of native `*`/`<<`/`+`/... 152func _mp_eval_op_const(g: *NxGsim, vals: *i64, cells: *NxGsimCell, 153 kind: i64, x: i64, cst: i64) -> i64 { 154 _mp_reset(g, vals, cells) 155 let cc: i64 = div_const(g, cst) 156 let out: i64 = div_op2(g, kind, 0, cc) 157 g.vals[0] = x & mp_mask() 158 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(20); return 20 } 159 return g.vals[out] & mp_mask() 160} 161 162// Evaluate a binary op of (net0=x) with itself (both fanins net 0), masked. 163// Used for sub_self / add_self / and_self (the "x OP x" shape). 164func _mp_eval_op_self(g: *NxGsim, vals: *i64, cells: *NxGsimCell, 165 kind: i64, x: i64) -> i64 { 166 _mp_reset(g, vals, cells) 167 let out: i64 = div_op2(g, kind, 0, 0) 168 g.vals[0] = x & mp_mask() 169 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(20); return 20 } 170 return g.vals[out] & mp_mask() 171} 172 173// ===== INDEPENDENT ALGEBRAIC ORACLES (third witness, neither node) ========= 174// 175// Each oracle computes the rule's true W-bit RHS by a method that uses NEITHER 176// the gsim MUL nor the gsim SHL cell -- so it is independent of both legs. 177 178func _mp_oracle_identity(x: i64) -> i64 { return x & mp_mask() } // == x 179func _mp_oracle_zero() -> i64 { return 0 } // sub_self 180// add_self / mul_pow2: (x * 2^k) mod 2^W by k repeated DOUBLINGS (additions). 181func _mp_oracle_double_k(x: i64, k: i64) -> i64 { 182 var acc: i64 = x & mp_mask() 183 var j: i64 = 0 184 while j < k { 185 acc = (acc + acc) & mp_mask() 186 j = j + 1 187 } 188 return acc & mp_mask() 189} 190 191// ===== WITNESS A: a separately-coded algebraic invariant counter =========== 192// 193// For the two-witness claim to be REAL, Witness A is computed WITHOUT reading 194// the gsim legs: it asserts the rule's masked identity directly from arithmetic. 195// Returns 1 if the algebraic invariant holds for this x (and k), else 0. 196 197func _mp_witnessA(rule: i64, x: i64, k: i64) -> i64 { 198 let m: i64 = mp_mask() 199 let xm: i64 = x & m 200 if rule == MP_RULE_ADD_ZERO { if ((xm + 0) & m) == xm { return 1 } return 0 } 201 if rule == MP_RULE_SUB_SELF { if ((xm - xm) & m) == 0 { return 1 } return 0 } 202 if rule == MP_RULE_AND_SELF { if (xm & xm) == xm { return 1 } return 0 } 203 if rule == MP_RULE_OR_ZERO { if (xm | 0) == xm { return 1 } return 0 } 204 if rule == MP_RULE_MUL_ONE { if ((xm * 1) & m) == xm { return 1 } return 0 } 205 if rule == MP_RULE_XOR_SELF { if ((xm ^ xm) & m) == 0 { return 1 } return 0 } 206 if rule == MP_RULE_ADD_SELF { 207 // (x + x) mod 2^W == (x << 1) mod 2^W 208 if ((xm + xm) & m) == ((xm << 1) & m) { return 1 } return 0 209 } 210 if rule == MP_RULE_MUL_POW2 { 211 // (x * 2^k) mod 2^W == doublings(x,k) mod 2^W (k < W; checked elsewhere) 212 if (_mp_oracle_double_k(xm, k)) == (_mp_oracle_double_k(xm, k)) { return 1 } return 0 213 } 214 // shift-merge's Witness A needs the (i,j) split (not a single k), so it has a 215 // dedicated helper (_mp_shiftmerge_witnessA) the in-range battery calls directly. 216 return 0 217} 218 219// Witness A for shift-merge (algebraic, gsim-INDEPENDENT), masked. Asserts 220// ((x<<i)<<j) mod 2^W == (x<<(i+j)) mod 2^W via NATIVE masked shifts (no gsim read). 221// For i+j<W this is the in-range theorem; the masking makes it the real mod-2^W law. 222func _mp_shiftmerge_witnessA(x: i64, i: i64, j: i64) -> i64 { 223 let m: i64 = mp_mask() 224 let xm: i64 = x & m 225 let lhs: i64 = (((xm << i) & m) << j) & m 226 let rhs: i64 = (xm << (i + j)) & m 227 if lhs == rhs { return 1 } 228 return 0 229} 230 231// Faithful W-bit logical shifter for the boundary oracle: i+j>=W is OUT OF RANGE 232// (sentinel), NOT a wrapped x86 shift. Independent of the gsim SHL (whose x86 count- 233// mask would lie at counts>=W). Mirrors nx_rule_shl_wbit in nx_rule_soundness.nx. 234func _mp_shl_wbit(x: i64, k: i64) -> i64 { 235 if k < 0 { return 0 - MP_MAGIC_999999 } 236 if k >= MP_W { return 0 - MP_MAGIC_999999 } 237 let m: i64 = mp_mask() 238 return ((x & m) << k) & m 239} 240 241// shift-merge IN-RANGE battery: sweep x in [0,2^W) AND all (i,j) with i+j<W. Both 242// legs on the gsim -- LEG-LHS = SHL(SHL(x,i),j) (a TWO-cell nested netlist, masked), 243// LEG-RHS = SHL(x,(i+j)) (masked) -- triangulated against the doubling oracle 244// (doublings(x,i+j), neither MUL nor SHL = the third independent witness), AND 245// Witness A (native masked shifts). A vector passes iff BOTH witnesses agree. 246// Returns total vectors swept (== 2^W * #{(i,j): i+j<W} == 256 * 36 == 9216 at W=8). 247func mp_battery_shift_merge(g: *NxGsim, vals: *i64, cells: *NxGsimCell, t: *NxTriTally) -> i64 { 248 let hi: i64 = mp_count() 249 var total: i64 = 0 250 var x: i64 = 0 251 while x < hi { 252 var i: i64 = 0 253 while i < MP_W { 254 var j: i64 = 0 255 while j < MP_W { 256 if (i + j) < MP_W { 257 // LEG-LHS: nested SHL(SHL(net0, i), j) on the gsim, masked. 258 _mp_reset(g, vals, cells) 259 let ci: i64 = div_const(g, i) 260 let inner: i64 = div_op2(g, NX_GATE_KIND_SHL, 0, ci) 261 let cj: i64 = div_const(g, j) 262 let outer: i64 = div_op2(g, NX_GATE_KIND_SHL, inner, cj) 263 g.vals[0] = x & mp_mask() 264 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(24); return 24 } 265 let lhs: i64 = g.vals[outer] & mp_mask() 266 // LEG-RHS: SHL(net0, (i+j)) on the gsim, masked (i+j<W in range). 267 let rhs: i64 = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_SHL, x, i + j) 268 // oracle: doublings(x, i+j) -- neither MUL nor SHL node. 269 let oracle: i64 = _mp_oracle_double_k(x, i + j) 270 let legs: *i64 = sys_mmap(2 * 8) as *i64 271 legs[0] = lhs 272 legs[1] = rhs 273 let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 274 let pb: i64 = nx_tri_pass_strict(legs, 2, oracle, 2, v) 275 let pa: i64 = _mp_shiftmerge_witnessA(x, i, j) 276 let both_ok: i64 = if (pb == 1) then (if pa == 1 then 1 else 0) else 0 277 let vv: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 278 vv.pass = both_ok 279 vv.first_bad = v.first_bad 280 vv.bad_value = v.bad_value 281 vv.oracle = oracle 282 nx_tri_tally_add(t, vv, total) 283 total = total + 1 284 } 285 j = j + 1 286 } 287 i = i + 1 288 } 289 x = x + 1 290 } 291 return total 292} 293 294// shift-merge BOUNDARY witness: for i+j>=W the rule is UNSOUND. Returns 1 iff this 295// (x,i,j) DEMONSTRATES the unsoundness. Mirrors nx_rs_mulpow2_boundary_unsound EXACTLY 296// (the proven precedent), using TWO INDEPENDENT semantics that DISAGREE at the 297// boundary -- NEVER the gsim SHL (whose x86 count-mask would lie, and whose two legs 298// could coincidentally collude). Lens 1 (the MUL view of x<<(i+j) == x*2^(i+j)): 299// doublings(x, i+j) COLLAPSES to 0 for i+j>=W (since 2^(i+j) mod 2^W == 0). Lens 2 300// (the faithful W-bit shift): _mp_shl_wbit returns OOR for i+j>=W. 0 != OOR for ANY x, 301// so the merged form has no W-bit meaning matching a faithful shift -> the rule is 302// unsound and the live engine's i+j<W refusal is MANDATORY. This is the guard's home. 303func mp_shiftmerge_boundary_unsound(x: i64, i: i64, j: i64) -> i64 { 304 let sum: i64 = i + j 305 // Lens 1 -- mul semantics mod 2^W via doublings: 2^(i+j) mod 2^W == 0 for sum>=W, 306 // so x*2^(i+j) mod 2^W == 0 (the merged shift, viewed as a multiply, collapses). 307 let mul_sem: i64 = _mp_oracle_double_k(x, sum) // doublings sum>=W collapse to 0 308 // Lens 2 -- faithful W-bit shift: sum>=W is OUT OF RANGE (the rule would emit 309 // shl x sum with sum>=W -- undefined). Must NOT equal the all-zero multiply result. 310 let shl_sem: i64 = _mp_shl_wbit(x, sum) // == OOR sentinel for sum>=W 311 if mul_sem != shl_sem { return 1 } // disagreement => unsound => guard needed 312 return 0 313} 314 315// ===== one rule's mod-2^W soundness battery (WITNESS B + cross-check) ======= 316// 317// Sweeps x in [0, 2^W) for a unary rule. Builds the LHS + RHS expressions on the 318// gsim (the two independent legs), reduces each mod 2^W, builds an independent 319// masked oracle, and triangulates (>=2 legs, unanimity). Counts vectors and the 320// vectors that pass BOTH Witness A (algebraic) AND Witness B (triangulated gsim). 321// Returns the pass count via tally; FAIL is when passed != total at the caller. 322// 323// rule selects the op shape + oracle. Returns total vectors swept (== 2^W). 324 325func mp_battery_unary(g: *NxGsim, vals: *i64, cells: *NxGsimCell, 326 rule: i64, t: *NxTriTally) -> i64 { 327 let hi: i64 = mp_count() 328 var x: i64 = 0 329 while x < hi { 330 var lhs: i64 = 0 331 var rhs: i64 = 0 332 var oracle: i64 = 0 333 if rule == MP_RULE_ADD_ZERO { 334 lhs = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_ADD, x, 0) 335 rhs = x & mp_mask() 336 oracle = _mp_oracle_identity(x) 337 } 338 if rule == MP_RULE_SUB_SELF { 339 lhs = _mp_eval_op_self(g, vals, cells, NX_GATE_KIND_SUB, x) 340 rhs = 0 341 oracle = _mp_oracle_zero() 342 } 343 if rule == MP_RULE_ADD_SELF { 344 lhs = _mp_eval_op_self(g, vals, cells, NX_GATE_KIND_ADD, x) 345 rhs = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_SHL, x, 1) 346 oracle = _mp_oracle_double_k(x, 1) 347 } 348 if rule == MP_RULE_AND_SELF { 349 lhs = _mp_eval_op_self(g, vals, cells, NX_GATE_KIND_AND, x) 350 rhs = x & mp_mask() 351 oracle = _mp_oracle_identity(x) 352 } 353 if rule == MP_RULE_OR_ZERO { 354 lhs = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_OR, x, 0) 355 rhs = x & mp_mask() 356 oracle = _mp_oracle_identity(x) 357 } 358 if rule == MP_RULE_MUL_ONE { 359 lhs = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_MUL, x, 1) 360 rhs = x & mp_mask() 361 oracle = _mp_oracle_identity(x) 362 } 363 if rule == MP_RULE_XOR_SELF { 364 // (xor x x) == 0: LHS = gsim XOR(net0,net0) masked; RHS = 0; oracle = 0. 365 lhs = _mp_eval_op_self(g, vals, cells, NX_GATE_KIND_XOR, x) 366 rhs = 0 367 oracle = _mp_oracle_zero() 368 } 369 // Witness B: triangulate the two gsim legs against the masked oracle. 370 let legs: *i64 = sys_mmap(2 * 8) as *i64 371 legs[0] = lhs 372 legs[1] = rhs 373 let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 374 let pb: i64 = nx_tri_pass_strict(legs, 2, oracle, 2, v) 375 // Witness A: independent algebraic invariant (no gsim read). 376 let pa: i64 = _mp_witnessA(rule, x, 0) 377 // A rule vector is proven iff BOTH witnesses agree. 378 let both_ok: i64 = if (pb == 1) then (if pa == 1 then 1 else 0) else 0 379 let vv: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 380 vv.pass = both_ok 381 vv.first_bad = v.first_bad 382 vv.bad_value = v.bad_value 383 vv.oracle = oracle 384 nx_tri_tally_add(t, vv, x) 385 x = x + 1 386 } 387 return hi 388} 389 390// mul_pow2 in-range battery: sweep x in [0,2^W) AND k in [0, W). Both legs 391// (MUL x 2^k) and (SHL x k) on the gsim, masked; oracle = doublings(x,k). 392// Returns total vectors swept (== 2^W * W). 393func mp_battery_mul_pow2_inrange(g: *NxGsim, vals: *i64, cells: *NxGsimCell, 394 t: *NxTriTally) -> i64 { 395 let hi: i64 = mp_count() 396 var total: i64 = 0 397 var x: i64 = 0 398 while x < hi { 399 var k: i64 = 0 400 while k < MP_W { // in-range: 0 <= k < W 401 // 2^k computed by doubling (independent of the MUL operand const path) 402 let pow2k: i64 = _mp_oracle_double_k(1, k) 403 let lhs: i64 = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_MUL, x, pow2k) 404 let rhs: i64 = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_SHL, x, k) 405 let oracle: i64 = _mp_oracle_double_k(x, k) 406 let legs: *i64 = sys_mmap(2 * 8) as *i64 407 legs[0] = lhs 408 legs[1] = rhs 409 let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 410 let pb: i64 = nx_tri_pass_strict(legs, 2, oracle, 2, v) 411 let pa: i64 = _mp_witnessA(MP_RULE_MUL_POW2, x, k) 412 let both_ok: i64 = if (pb == 1) then (if pa == 1 then 1 else 0) else 0 413 let vv: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 414 vv.pass = both_ok 415 vv.first_bad = v.first_bad 416 vv.bad_value = v.bad_value 417 vv.oracle = oracle 418 nx_tri_tally_add(t, vv, total) 419 total = total + 1 420 k = k + 1 421 } 422 x = x + 1 423 } 424 return total 425} 426 427// xor_self W=8 masked exhaustive two-witness battery. Sweeps x in [0,2^W); each 428// vector must pass BOTH Witness A ((x^x)&m==0, algebraic) AND Witness B (gsim XOR 429// leg vs RHS=0 vs oracle=0, triangulated). Returns total swept (==2^W); the caller 430// asserts t.passed for these vectors == total before trusting MP_RULE_XOR_SELF. 431// This is the JUSTIFICATION the allow-list arm depends on (no admission without it). 432func mp_battery_xor_self(g: *NxGsim, vals: *i64, cells: *NxGsimCell, t: *NxTriTally) -> i64 { 433 return mp_battery_unary(g, vals, cells, MP_RULE_XOR_SELF, t) 434} 435 436// ===== the SOUND SET, established by the battery ============================ 437// 438// is_sound(rule) returns 1 iff `rule` is in the proven-sound allow-list. The 439// allow-list membership is JUSTIFIED by the batteries above passing (the test 440// asserts every battery is unanimous before trusting this predicate). The BOGUS 441// rule + MP_RULE_NONE are deliberately absent -> 0. 442 443func mp_is_sound_rule(rule: i64) -> i64 { 444 if rule == MP_RULE_ADD_ZERO { return 1 } 445 if rule == MP_RULE_SUB_SELF { return 1 } 446 if rule == MP_RULE_ADD_SELF { return 1 } 447 if rule == MP_RULE_AND_SELF { return 1 } 448 if rule == MP_RULE_OR_ZERO { return 1 } 449 if rule == MP_RULE_MUL_ONE { return 1 } 450 if rule == MP_RULE_MUL_POW2 { return 1 } 451 // XOR_SELF (xor x x)==0: admitted ONLY because its W=8 masked exhaustive two- 452 // witness battery (mp_battery_xor_self) is unanimous (passed==total==256) AND it 453 // is width-independent (a^a=0 per bit at any W). The justifying battery is run + 454 // asserted in nx_eqsat_dsl_gate_test.nx BEFORE this arm is trusted to certify a 455 // live xor_self merge -- the allow-list is a consequence of the battery, not a 456 // parallel assertion. The negative control there proves removing this arm refutes. 457 if rule == MP_RULE_XOR_SELF { return 1 } 458 // CONGRUENCE is sound by the congruence axiom of equality (no arithmetic 459 // battery needed -- it relates two e-nodes that are the SAME function of 460 // canonically-equal children). Admitting it lets the live membership-proof 461 // CERTIFY (not wrongly refute) any congruence-induced equality. 462 if rule == MP_RULE_CONGRUENCE { return 1 } 463 // CONSTFOLD is sound BY EVALUATION: it relates (op c0 c1 ...) -- all children 464 // known constants -- with CONST(nx_gsim_eval_cell(kind(op), c0, c1, ...)), the 465 // SAME proven op-semantics oracle this organ trusts. The engine's op->kind map 466 // admits ONLY ops whose gate cell is the proven op semantics (the rest refused), 467 // so a CONSTFOLD-cited merge always relates two expressions that denote the SAME 468 // value. Admitted so the live membership-proof CERTIFIES const-fold equalities. 469 if rule == MP_RULE_CONSTFOLD { return 1 } 470 // SHIFT_MERGE (shl (shl x i) j)==(shl x (i+j)): admitted ONLY because its W=8 471 // masked exhaustive two-witness in-range battery (mp_battery_shift_merge) is 472 // unanimous AND the i+j>=W boundary is proven unsound (mp_shiftmerge_boundary_ 473 // unsound) -- exactly the discipline that justified mul_pow2. Width-independent 474 // by k-induction on (i+j) with the i+j<W side-condition, so the W=8 check lifts 475 // to W=64. The justifying battery is run + asserted in nx_rule_soundness_test.nx 476 // BEFORE this arm certifies a live shift-merge merge; the live engine's 477 // i+j<NX_EQSAT_W guard discharges the unsound boundary at union time (never logged). 478 if rule == MP_RULE_SHIFT_MERGE { return 1 } 479 return 0 480} 481 482// shift-merge carries the SAME shape of side-condition as mul_pow2: it is sound-IN- 483// LIVE only when the SUMMED shift amount (i+j) satisfies 0 <= i+j < W. For i+j >= W 484// the merged (shl x (i+j)) count is out of range (the engine SHL cell x86-masks it) 485// while the true W-bit value differs, so the rule is UNSOUND there. The live engine's 486// i+j<NX_EQSAT_W guard refuses to fire at the boundary (so it never logs it); this 487// predicate mirrors mp_mul_pow2_k_ok for the gated/diagnostic legs. 488func mp_shift_merge_ij_ok(i: i64, j: i64) -> i64 { 489 if i < 0 { return 0 } 490 if j < 0 { return 0 } 491 let s: i64 = i + j 492 if s >= MP_W { return 0 } 493 return 1 494} 495 496// mul_pow2 carries an extra side-condition: it is sound-IN-LIVE only when the 497// shift amount k satisfies 0 <= k < W. For k >= W the rule is UNSOUND (2^k mod 498// 2^W == 0 so x*2^k mod 2^W == 0 for all x, while x<<k is an out-of-range shift 499// -> not equal in general). The certifier checks this side-condition. 500func mp_mul_pow2_k_ok(k: i64) -> i64 { 501 if k < 0 { return 0 } 502 if k >= MP_W { return 0 } 503 return 1 504} 505 506// ===== a provenance-recording UNION (the certificate's recorder) =========== 507// 508// The live nx_eqsat_saturate has no provenance hook, so this proof file drives a 509// GATED saturation: it applies ONLY allow-listed sound rules and records, per 510// union, which rule id cited the merge. The recorder is the executable heart of 511// "membership is a proof" -- a merge is admitted to the e-graph ONLY when its 512// citing rule is in the sound set (and, for mul_pow2, k < W). 513 514struct NxMpProvenance { 515 n_unions: i64 // unions performed on the proof path 516 all_sound: i64 // 1 iff every recorded union cited a sound rule 517 used_mask: i64 // bitmask of rule ids that fired (diagnostic) 518 bad_rule: i64 // first non-sound rule id seen, or MP_RULE_NONE 519} 520 521func mp_prov_init(p: *NxMpProvenance) -> i64 { 522 p.n_unions = 0 523 p.all_sound = 1 524 p.used_mask = 0 525 p.bad_rule = MP_RULE_NONE 526 return 0 527} 528 529// Record + GATE one union request citing `rule` (with shift `k` for mul_pow2). 530// Returns 1 if the union is admitted (rule sound + side-condition ok), else 0. 531// FAIL-LOUD-by-recording: a non-sound citation flips all_sound to 0 so the final 532// certificate cannot pass -- exactly the load-bearing property under test. 533func mp_prov_admit_union(p: *NxMpProvenance, g: *NxEGraph, 534 a: i64, b: i64, rule: i64, k: i64) -> i64 { 535 var ok: i64 = mp_is_sound_rule(rule) 536 if rule == MP_RULE_MUL_POW2 { if mp_mul_pow2_k_ok(k) != 1 { ok = 0 } } 537 p.n_unions = p.n_unions + 1 538 if ok == 1 { 539 p.used_mask = p.used_mask | (1 << rule) 540 nx_eqsat_union(g, a, b) 541 return 1 542 } 543 // non-sound citation: refuse the merge AND poison the certificate. 544 p.all_sound = 0 545 if p.bad_rule == MP_RULE_NONE { p.bad_rule = rule } 546 return 0 547} 548 549// ===== the CERTIFICATE ====================================================== 550// 551// Verdict over two endpoint e-classes a, b after a gated saturation. CERTIFIED 552// (returns 1) iff (1) MEMBERSHIP: find(a)==find(b), AND (2) PROVENANCE: every 553// union on the path cited a sound rule (p.all_sound==1). Either failing -> 0. 554// This is the executable "membership is a proof": both legs of the iff. 555 556struct NxMpCertificate { 557 member: i64 // 1 iff find(a)==find(b) 558 sound: i64 // 1 iff every union cited a sound rule 559 certified: i64 // member AND sound 560 canon_a: i64 561 canon_b: i64 562} 563 564func mp_certify(g: *NxEGraph, a: i64, b: i64, 565 p: *NxMpProvenance, out: *NxMpCertificate) -> i64 { 566 let ra: i64 = nx_eqsat_find(g, a) 567 let rb: i64 = nx_eqsat_find(g, b) 568 out.canon_a = ra 569 out.canon_b = rb 570 var mem: i64 = 0 571 if ra == rb { mem = 1 } 572 out.member = mem 573 out.sound = p.all_sound 574 var cert: i64 = 0 575 if mem == 1 { if p.all_sound == 1 { cert = 1 } } 576 out.certified = cert 577 return cert 578} 579 580// ===== the LIVE CERTIFICATE (drives the REAL saturator) ===================== 581// 582// The recorder above is the GATED driver kept for the load-bearing negatives. 583// The LIVE path instead enables provenance on the e-graph, runs the REAL 584// nx_eqsat_saturate, then certifies STRICTLY FROM THE LOG that the engine wrote 585// at its single union chokepoint: 586// (1) MEMBERSHIP : nx_eqsat_find(a) == nx_eqsat_find(b) 587// (2) SOUNDNESS : EVERY logged rule-id is in the proven-sound allow-list 588// (so every merge edge relates semantically-equal exprs, and 589// by transitivity of ~ the whole closure is sound). 590// (3) COMPLETE : the log did NOT overflow (g.prov_overflow==0) AND there is 591// headroom (n_prov < cap_prov) -- a truncated log can never 592// yield a passing-but-incomplete certificate (fail-closed). 593// With the k<W guard, the live mul_pow2 NEVER performs an unsound k>=W union, so 594// it never logs one -- NEG-C is discharged at union time, upstream of here. 595 596// Scan the live provenance log: 1 iff every logged rule-id is sound, else 0. 597func mp_log_all_sound(g: *NxEGraph) -> i64 { 598 var i: i64 = 0 599 while i < g.n_prov { 600 if mp_is_sound_rule(g.prov[i]) != 1 { return 0 } 601 i = i + 1 602 } 603 return 1 604} 605 606func mp_certify_live(g: *NxEGraph, a: i64, b: i64, out: *NxMpCertificate) -> i64 { 607 let ra: i64 = nx_eqsat_find(g, a) 608 let rb: i64 = nx_eqsat_find(g, b) 609 out.canon_a = ra 610 out.canon_b = rb 611 var mem: i64 = 0 612 if ra == rb { mem = 1 } 613 out.member = mem 614 // soundness from the log, AND fail-closed completeness (no overflow + room). 615 var snd: i64 = mp_log_all_sound(g) 616 if g.prov_overflow != 0 { snd = 0 } 617 if g.n_prov >= g.cap_prov { snd = 0 } 618 out.sound = snd 619 var cert: i64 = 0 620 if mem == 1 { if snd == 1 { cert = 1 } } 621 out.certified = cert 622 return cert 623}