nx_opt_eqsat_pass_gate.nx source

1// nx_opt_eqsat_pass_gate.nx -- proves opt_eqsat_pass REWRITES REAL IR, and that it reaches an 2// expression the shipping pipeline structurally cannot. 3// 4// THE MONEY TOOTH is a head-to-head on ONE function: build `x ^ x` where x is a runtime parameter, 5// run the INCUMBENT opt_const_fold first and require it to fold NOTHING (it needs both operands 6// constant, so it cannot see this), then run opt_eqsat_pass and require it to fold exactly one 7// instruction to the constant 0. A pass that merely duplicated the incumbent would fail that pair. 8// 9// WHY THIS IS NOT A STUB CARRYING A CONTRACT NAME: the flip law says a completion signal keyed on a 10// symbol rewards writing the symbol. So this gate does not ask whether opt_eqsat_pass EXISTS -- it 11// asks whether a Value that was an XOR instruction is a CONSTANT afterwards, and whether the number 12// the incumbent folded on the same input was zero. Those are properties of the program, not the name. 13// license_tier: ORIGINAL expect_exit: 0 14 15import "nx_gate_verdict.nx" 16import "nx_opt.nx" 17import "nx_opt_eqsat_pass.nx" 18 19func main() -> i64 { 20 gv_head("opt_eqsat_pass gate -- equality saturation rewriting real IR, head to head with the incumbent" as *u8) 21 let ctr: *i64 = gv_ctr() 22 23 let i64t: *Type = ir_type_i64() 24 25 // ================= CASE 1: x ^ x, x a runtime parameter ================= 26 let m1: *Module = ir_module_new("t1" as *u8) 27 let f1: *Function = ir_function_new(m1, "f1" as *u8, 2, i64t) 28 let bb1: *BasicBlock = ir_block_new(f1) 29 let x1: i64 = ir_param(f1, 0, i64t) 30 let r1: i64 = ir_emit_binop(bb1, OP_XOR, x1, x1, i64t) 31 // INCUMBENT FIRST, on the untouched function. 32 let incumbent1: i64 = opt_const_fold(f1) 33 let eq1: i64 = opt_eqsat_pass(f1) 34 let rv1: *Value = val_at(f1, r1) 35 36 // ================= CASE 2: POSITIVE CONTROL, both operands constant ===== 37 // Without this, a pass that folded ONLY xor-self would look complete while being unable to do the 38 // ordinary job at all. 39 let m2: *Module = ir_module_new("t2" as *u8) 40 let f2: *Function = ir_function_new(m2, "f2" as *u8, 2, i64t) 41 let bb2: *BasicBlock = ir_block_new(f2) 42 let c2a: i64 = ir_const_i64(f2, 2) 43 let c2b: i64 = ir_const_i64(f2, 3) 44 let r2: i64 = ir_emit_binop(bb2, OP_ADD, c2a, c2b, i64t) 45 let eq2: i64 = opt_eqsat_pass(f2) 46 let rv2: *Value = val_at(f2, r2) 47 48 // ================= CASE 3: NEGATIVE CONTROL, genuinely irreducible ====== 49 // x + y for two DISTINCT runtime parameters has no constant value. A pass that folded this would 50 // be miscompiling, and every tooth above would still pass -- which is exactly why this is here. 51 let m3: *Module = ir_module_new("t3" as *u8) 52 let f3: *Function = ir_function_new(m3, "f3" as *u8, 2, i64t) 53 let bb3: *BasicBlock = ir_block_new(f3) 54 let x3: i64 = ir_param(f3, 0, i64t) 55 let y3: i64 = ir_param(f3, 1, i64t) 56 let r3: i64 = ir_emit_binop(bb3, OP_ADD, x3, y3, i64t) 57 let eq3: i64 = opt_eqsat_pass(f3) 58 let rv3: *Value = val_at(f3, r3) 59 60 // ================= CASE 4: NEGATIVE CONTROL, unmapped operator ========= 61 // Division has no faithful cell in the gate simulator, so the engine refuses to fold it and this 62 // pass declines the opcode outright. Folding 12/3 here would mean the refusal boundary leaked. 63 let m4: *Module = ir_module_new("t4" as *u8) 64 let f4: *Function = ir_function_new(m4, "f4" as *u8, 2, i64t) 65 let bb4: *BasicBlock = ir_block_new(f4) 66 let c4a: i64 = ir_const_i64(f4, 12) 67 let c4b: i64 = ir_const_i64(f4, 3) 68 let r4: i64 = ir_emit_binop(bb4, OP_DIV_S, c4a, c4b, i64t) 69 let eq4: i64 = opt_eqsat_pass(f4) 70 let rv4: *Value = val_at(f4, r4) 71 72 // ---------------- THE HEAD TO HEAD ---------------- 73 gv_check("the INCUMBENT const-fold pass folds NOTHING in x xor x" as *u8, incumbent1 == 0, ctr) 74 gv_check("opt_eqsat_pass folds exactly one instruction in the same function" as *u8, eq1 == 1, ctr) 75 gv_check("the rewritten Value is now a CONSTANT" as *u8, rv1.kind == 0, ctr) 76 gv_check("and its constant value is 0, which is what x xor x equals" as *u8, rv1.const_int == 0, ctr) 77 78 // ---------------- ORDINARY CAPABILITY ---------------- 79 gv_check("it also folds an ordinary both-constant expression" as *u8, eq2 == 1, ctr) 80 gv_check("2 plus 3 folds to exactly 5" as *u8, rv2.const_int == 5, ctr) 81 82 // ---------------- THE CONTROLS ---------------- 83 gv_check("neg-control-two-distinct-parameters-are-NOT-folded" as *u8, eq3 == 0, ctr) 84 gv_check("neg-control-the-irreducible-result-stays-a-non-constant" as *u8, rv3.kind != 0, ctr) 85 gv_check("neg-control-an-operator-with-no-faithful-oracle-cell-is-DECLINED" as *u8, eq4 == 0, ctr) 86 gv_check("neg-control-the-declined-division-result-stays-a-non-constant" as *u8, rv4.kind != 0, ctr) 87 88 return gv_verdict("nx_opt_eqsat_pass_gate" as *u8, ctr, 89 "equality saturation rewriting real IR: it folds x-xor-x which the incumbent const-fold provably cannot, folds ordinary constants, and declines both an irreducible expression and an operator whose semantics the engine refuses to model" as *u8) 90}