nx_eqsat_congruence_test.nx source

1// nx_eqsat_congruence_test.nx -- STRUCTURAL-WITNESS GATE for the egg-style 2// deferred CONGRUENCE CLOSURE newly integrated into nx_eqsat.nx. 3// 4// THE PROOF (the new organ actually MEETS egg's congruence rebuild): 5// Congruence axiom of equality: if a == b (same canonical e-class) then for any 6// deterministic function f, f(...a...) == f(...b...). The pre-MEET engine had a 7// real hashcons-by-linear-scan + union-find, but NO rebuild: after a union it 8// never re-merged congruent PARENTS, so f(a) and f(b) stayed in distinct classes. 9// This gate builds exactly that witness and proves the rebuild closes it. 10// 11// CASE 1 (POSITIVE -- congruence FIRES, cited + logged sound): 12// Build a, b as two DISTINCT vars; build g_a = NEG(a) and g_b = NEG(b) (so the 13// two parent e-nodes are genuinely different nodes). Pre-merge a~b via the SOUND 14// mul_pow2 path is overkill; instead we drive the canonical congruence trigger 15// through the real saturator: a=(mul x 8), b=(shl x 3) -> mul_pow2 merges them, 16// then NEG(a) and NEG(b) MUST become congruent via the rebuild (same op NEG, 17// same payload, canonically-equal child). Assert: 18// (1a) find(NEG a) == find(NEG b) -- congruence detected 19// (1b) the prov log contains id 8 (CONGRUENCE) -- the merge was CITED 20// (1c) every logged id is in the proven-sound allow-list (0..8, !=NONE-as-bad) 21// (1d) RULE_NONE (id 0) count == 0 -- no back-door (2-arg) merge 22// 23// CASE 2 (NEGATIVE control -- WITHOUT rebuild the gap is REAL): 24// Same graph, but provenance/meet OFF on a plain engine run (rebuild disabled): 25// mul_pow2 still merges (mul x 8)~(shl x 3), but the parents NEG(mul8)/NEG(shl3) 26// are NOT merged -> find(NEG a) != find(NEG b). This proves the rebuild is the 27// load-bearing organ (a passing CASE 1 is not vacuous). 28// 29// CASE 3 (NEGATIVE -- non-congruent nodes are NOT merged): 30// NEG(a) vs NOT(a): same single child class but DIFFERENT op -> distinct 31// fingerprints -> never congruence-merged. Asserts the fingerprint folds op 32// (a fingerprint that ignored op would wrongly merge them and cite CONGRUENCE). 33// 34// KNOWN ANSWER (FAIL LOUD), one line: 35// "<case1_member> <cong_logged> <none_count> <case2_member> <case3_member>" 36// = "1 1 0 0 0 " exit 0 iff every assertion holds. 37// 38// SOVEREIGN: no SMT, no .sh; runs on the pinned NishiLang compiler. The exit code 39// IS the verdict. license_tier: ORIGINAL 40 41import "nx_eqsat.nx" 42 43func _emit_num(v: i64) -> i64 { 44 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 45 let t2: *u8 = sys_mmap(28); var t: i64 = 0 46 if n == 0 { t2[0] = 48; t = 1 } 47 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 48 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 49 b[t] = 32; sys_write(1, b, t + 1); return 0 50} 51func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 52 53// Count logged ids equal to `want`; also assert every logged id is allow-listed. 54// Returns (count of `want`); writes 1 to bad_out[0] if any id is NOT in 0..RULE_N 55// or is the NONE sentinel used as a non-sound id (defense vs RULE_NONE bypass). 56func _scan_log(g: *NxEGraph, want: i64, none_out: *i64, anybad_out: *i64) -> i64 { 57 var cnt_want: i64 = 0 58 var cnt_none: i64 = 0 59 var anybad: i64 = 0 60 var i: i64 = 0 61 while i < g.n_prov { 62 let id: i64 = g.prov[i] 63 if id == want { cnt_want = cnt_want + 1 } 64 if id == NX_EQSAT_RULE_NONE { cnt_none = cnt_none + 1 } 65 // allow-listed sound ids: the 7 identity rules + CONGRUENCE (NOT NONE). 66 var ok: i64 = 0 67 if id == NX_EQSAT_RULE_ADD_ZERO { ok = 1 } 68 if id == NX_EQSAT_RULE_SUB_SELF { ok = 1 } 69 if id == NX_EQSAT_RULE_ADD_SELF { ok = 1 } 70 if id == NX_EQSAT_RULE_AND_SELF { ok = 1 } 71 if id == NX_EQSAT_RULE_OR_ZERO { ok = 1 } 72 if id == NX_EQSAT_RULE_MUL_ONE { ok = 1 } 73 if id == NX_EQSAT_RULE_MUL_POW2 { ok = 1 } 74 if id == NX_EQSAT_RULE_CONGRUENCE { ok = 1 } 75 if ok != 1 { anybad = 1 } 76 i = i + 1 77 } 78 none_out[0] = cnt_none 79 anybad_out[0] = anybad 80 return cnt_want 81} 82 83func main() -> i64 { 84 let cap_nodes: i64 = 256 85 let cap_cls: i64 = 256 86 87 // ===================== CASE 1: POSITIVE (congruence fires) ================ 88 let nodes: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 89 let classes: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 90 let g: *NxEGraph = sys_mmap(128) as *NxEGraph 91 if nx_eqsat_init(g, nodes, cap_nodes, classes, cap_cls) != NX_EQSAT_OK { sys_exit(10); return 10 } 92 93 // MEET scratch (caller-owned). hashcons sized power-of-2 with headroom. 94 let hc: *HashMap = nx_hmap_alloc(256) 95 if (hc as i64) == 0 { sys_exit(11); return 11 } 96 let par_node: *i64 = sys_mmap(1024 * 8) as *i64 97 let par_cls: *i64 = sys_mmap(1024 * 8) as *i64 98 let worklist: *i64 = sys_mmap(1024 * 8) as *i64 99 if nx_eqsat_enable_meet(g, hc, par_node, par_cls, 1024, worklist, 1024) != NX_EQSAT_OK { sys_exit(12); return 12 } 100 101 // provenance ON so we can certify the congruence merge was CITED + sound. 102 let plog: *i64 = sys_mmap(256 * 8) as *i64 103 if nx_eqsat_enable_prov(g, plog, 256) != NX_EQSAT_OK { sys_exit(13); return 13 } 104 105 let x: i64 = nx_eqsat_add_var(g, 0) 106 let c8: i64 = nx_eqsat_add_const(g, 8) 107 let c3: i64 = nx_eqsat_add_const(g, 3) 108 let mul8: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_MUL, x, c8) // a 109 let shl3: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_SHL, x, c3) // b (becomes ~ a) 110 // PARENTS: f(a)=NEG(mul8), f(b)=NEG(shl3) -- distinct e-nodes, same op NEG. 111 let neg_a: i64 = nx_eqsat_add_unary(g, NX_EQ_OP_NEG, mul8) 112 let neg_b: i64 = nx_eqsat_add_unary(g, NX_EQ_OP_NEG, shl3) 113 114 // Pre-state: parents must be in DIFFERENT classes (no congruence yet). 115 if nx_eqsat_find(g, neg_a) == nx_eqsat_find(g, neg_b) { sys_exit(14); return 14 } 116 117 // Run the REAL saturator: mul_pow2 merges mul8~shl3; the deferred rebuild then 118 // re-fingerprints the NEG parents -> both canonicalize to NEG(same class) -> 119 // congruence-merges them, citing NX_EQSAT_RULE_CONGRUENCE. 120 let sat: i64 = nx_eqsat_saturate(g, 32) 121 if sat != NX_EQSAT_SATURATED { sys_exit(15); return 15 } 122 123 var case1_member: i64 = 0 124 if nx_eqsat_find(g, neg_a) == nx_eqsat_find(g, neg_b) { case1_member = 1 } 125 126 let none_out: *i64 = sys_mmap(8) as *i64 127 let bad_out: *i64 = sys_mmap(8) as *i64 128 let cong_count: i64 = _scan_log(g, NX_EQSAT_RULE_CONGRUENCE, none_out, bad_out) 129 var cong_logged: i64 = 0 130 if cong_count >= 1 { cong_logged = 1 } 131 let none_count: i64 = none_out[0] 132 let any_bad: i64 = bad_out[0] 133 134 // ===================== CASE 2: NEGATIVE control (no rebuild) ============== 135 // Same graph, plain engine (meet OFF) -> mul_pow2 still fires but parents NOT 136 // re-merged: find(NEG a) != find(NEG b). Proves the rebuild is load-bearing. 137 let nodes2: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 138 let classes2: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 139 let g2: *NxEGraph = sys_mmap(128) as *NxEGraph 140 if nx_eqsat_init(g2, nodes2, cap_nodes, classes2, cap_cls) != NX_EQSAT_OK { sys_exit(20); return 20 } 141 let x2: i64 = nx_eqsat_add_var(g2, 0) 142 let c8b: i64 = nx_eqsat_add_const(g2, 8) 143 let c3b: i64 = nx_eqsat_add_const(g2, 3) 144 let mul8b: i64 = nx_eqsat_add_binary(g2, NX_EQ_OP_MUL, x2, c8b) 145 let shl3b: i64 = nx_eqsat_add_binary(g2, NX_EQ_OP_SHL, x2, c3b) 146 let neg_a2: i64 = nx_eqsat_add_unary(g2, NX_EQ_OP_NEG, mul8b) 147 let neg_b2: i64 = nx_eqsat_add_unary(g2, NX_EQ_OP_NEG, shl3b) 148 nx_eqsat_saturate(g2, 32) 149 // sanity: the children DID merge (mul_pow2), so the gap is purely congruence. 150 if nx_eqsat_find(g2, mul8b) != nx_eqsat_find(g2, shl3b) { sys_exit(21); return 21 } 151 var case2_member: i64 = 0 152 if nx_eqsat_find(g2, neg_a2) == nx_eqsat_find(g2, neg_b2) { case2_member = 1 } 153 154 // ===================== CASE 3: NEGATIVE (non-congruent: diff op) ========== 155 // NEG(a) vs NOT(a): same child class, DIFFERENT op -> distinct fingerprints -> 156 // never merged. Proves the fingerprint folds op (no false CONGRUENCE merge). 157 let nodes3: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 158 let classes3: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 159 let g3: *NxEGraph = sys_mmap(128) as *NxEGraph 160 if nx_eqsat_init(g3, nodes3, cap_nodes, classes3, cap_cls) != NX_EQSAT_OK { sys_exit(30); return 30 } 161 let hc3: *HashMap = nx_hmap_alloc(256) 162 let pn3: *i64 = sys_mmap(1024 * 8) as *i64 163 let pc3: *i64 = sys_mmap(1024 * 8) as *i64 164 let wl3: *i64 = sys_mmap(1024 * 8) as *i64 165 if nx_eqsat_enable_meet(g3, hc3, pn3, pc3, 1024, wl3, 1024) != NX_EQSAT_OK { sys_exit(31); return 31 } 166 let x3: i64 = nx_eqsat_add_var(g3, 0) 167 let neg3: i64 = nx_eqsat_add_unary(g3, NX_EQ_OP_NEG, x3) 168 let not3: i64 = nx_eqsat_add_unary(g3, NX_EQ_OP_NOT, x3) 169 nx_eqsat_saturate(g3, 32) 170 var case3_member: i64 = 0 171 if nx_eqsat_find(g3, neg3) == nx_eqsat_find(g3, not3) { case3_member = 1 } 172 173 // ===================== known answer + FAIL-LOUD ========================== 174 _emit_num(case1_member); _emit_num(cong_logged); _emit_num(none_count); 175 _emit_num(case2_member); _emit_num(case3_member); _nl() 176 177 if case1_member != 1 { sys_exit(1); return 1 } // congruence DETECTED f(a)==f(b) 178 if cong_logged != 1 { sys_exit(2); return 2 } // the merge was CITED (id 8 in log) 179 if any_bad != 0 { sys_exit(3); return 3 } // every logged id is allow-listed 180 if none_count != 0 { sys_exit(4); return 4 } // NO back-door RULE_NONE merge 181 if g.prov_overflow != 0 { sys_exit(5); return 5 } // log complete (fail-closed) 182 if case2_member != 0 { sys_exit(6); return 6 } // WITHOUT rebuild the gap is real 183 if case3_member != 0 { sys_exit(7); return 7 } // non-congruent (diff op) NOT merged 184 sys_exit(0); return 0 185}