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_gate_verdict.nx" 42import "nx_eqsat.nx" 43 44func _emit_num(v: i64) -> i64 { 45 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 46 let t2: *u8 = sys_mmap(28); var t: i64 = 0 47 if n == 0 { t2[0] = 48; t = 1 } 48 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 49 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 50 b[t] = 32; sys_write(1, b, t + 1); return 0 51} 52func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 53 54// Count logged ids equal to `want`; also assert every logged id is allow-listed. 55// Returns (count of `want`); writes 1 to bad_out[0] if any id is NOT in 0..RULE_N 56// or is the NONE sentinel used as a non-sound id (defense vs RULE_NONE bypass). 57func _scan_log(g: *NxEGraph, want: i64, none_out: *i64, anybad_out: *i64) -> i64 { 58 var cnt_want: i64 = 0 59 var cnt_none: i64 = 0 60 var anybad: i64 = 0 61 var i: i64 = 0 62 while i < g.n_prov { 63 let id: i64 = g.prov[i] 64 if id == want { cnt_want = cnt_want + 1 } 65 if id == NX_EQSAT_RULE_NONE { cnt_none = cnt_none + 1 } 66 // allow-listed sound ids: the 7 identity rules + CONGRUENCE (NOT NONE). 67 var ok: i64 = 0 68 if id == NX_EQSAT_RULE_ADD_ZERO { ok = 1 } 69 if id == NX_EQSAT_RULE_SUB_SELF { ok = 1 } 70 if id == NX_EQSAT_RULE_ADD_SELF { ok = 1 } 71 if id == NX_EQSAT_RULE_AND_SELF { ok = 1 } 72 if id == NX_EQSAT_RULE_OR_ZERO { ok = 1 } 73 if id == NX_EQSAT_RULE_MUL_ONE { ok = 1 } 74 if id == NX_EQSAT_RULE_MUL_POW2 { ok = 1 } 75 if id == NX_EQSAT_RULE_CONGRUENCE { ok = 1 } 76 if ok != 1 { anybad = 1 } 77 i = i + 1 78 } 79 none_out[0] = cnt_none 80 anybad_out[0] = anybad 81 return cnt_want 82} 83 84func main() -> i64 { 85 let cap_nodes: i64 = 256 86 let cap_cls: i64 = 256 87 88 // MIGRATED OFF A HAND-ROLLED VERDICT 2026-08-14, and NEVER COMPILED BEFORE THAT DAY: nx_eqsat.nx 89 // itself did not compile (a module const was read 470 lines above its declaration, which nx_cc 90 // refuses because the reader would silently see 0), so this proof and every sibling in the eqsat 91 // family had sat on disk unbuilt. The teeth below were already excellent -- two real negative 92 // controls -- they simply had no way to say so to anything outside the process. 93 gv_head("nx_eqsat congruence-closure gate -- deferred rebuild merges congruent parents, and only congruent ones" as *u8) 94 let ctr: *i64 = gv_ctr() 95 96 // ===================== CASE 1: POSITIVE (congruence fires) ================ 97 let nodes: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 98 let classes: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 99 let g: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph 100 if nx_eqsat_init(g, nodes, cap_nodes, classes, cap_cls) != NX_EQSAT_OK { sys_exit(10); return 10 } 101 102 // MEET scratch (caller-owned). hashcons sized power-of-2 with headroom. 103 let hc: *HashMap = nx_hmap_alloc(256) 104 if (hc as i64) == 0 { sys_exit(11); return 11 } 105 let par_node: *i64 = sys_mmap(1024 * 8) as *i64 106 let par_cls: *i64 = sys_mmap(1024 * 8) as *i64 107 let worklist: *i64 = sys_mmap(1024 * 8) as *i64 108 if nx_eqsat_enable_meet(g, hc, par_node, par_cls, 1024, worklist, 1024) != NX_EQSAT_OK { sys_exit(12); return 12 } 109 110 // provenance ON so we can certify the congruence merge was CITED + sound. 111 let plog: *i64 = sys_mmap(256 * 8) as *i64 112 if nx_eqsat_enable_prov(g, plog, 256) != NX_EQSAT_OK { sys_exit(13); return 13 } 113 114 let x: i64 = nx_eqsat_add_var(g, 0) 115 let c8: i64 = nx_eqsat_add_const(g, 8) 116 let c3: i64 = nx_eqsat_add_const(g, 3) 117 let mul8: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_MUL, x, c8) // a 118 let shl3: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_SHL, x, c3) // b (becomes ~ a) 119 // PARENTS: f(a)=NEG(mul8), f(b)=NEG(shl3) -- distinct e-nodes, same op NEG. 120 let neg_a: i64 = nx_eqsat_add_unary(g, NX_EQ_OP_NEG, mul8) 121 let neg_b: i64 = nx_eqsat_add_unary(g, NX_EQ_OP_NEG, shl3) 122 123 // Pre-state: parents must be in DIFFERENT classes (no congruence yet). THIS IS THE ANTI-VACUITY 124 // TOOTH -- if the parents were already merged before saturation, CASE 1 would prove nothing at all. 125 var pre_distinct: i64 = 1 126 if nx_eqsat_find(g, neg_a) == nx_eqsat_find(g, neg_b) { pre_distinct = 0 } 127 128 // Run the REAL saturator: mul_pow2 merges mul8~shl3; the deferred rebuild then 129 // re-fingerprints the NEG parents -> both canonicalize to NEG(same class) -> 130 // congruence-merges them, citing NX_EQSAT_RULE_CONGRUENCE. 131 let sat: i64 = nx_eqsat_saturate(g, 32) 132 var reached_fixpoint: i64 = 0 133 if sat == NX_EQSAT_SATURATED { reached_fixpoint = 1 } 134 135 var case1_member: i64 = 0 136 if nx_eqsat_find(g, neg_a) == nx_eqsat_find(g, neg_b) { case1_member = 1 } 137 138 let none_out: *i64 = sys_mmap(8) as *i64 139 let bad_out: *i64 = sys_mmap(8) as *i64 140 let cong_count: i64 = _scan_log(g, NX_EQSAT_RULE_CONGRUENCE, none_out, bad_out) 141 var cong_logged: i64 = 0 142 if cong_count >= 1 { cong_logged = 1 } 143 let none_count: i64 = none_out[0] 144 let any_bad: i64 = bad_out[0] 145 146 // ===================== CASE 2: NEGATIVE control (no rebuild) ============== 147 // Same graph, plain engine (meet OFF) -> mul_pow2 still fires but parents NOT 148 // re-merged: find(NEG a) != find(NEG b). Proves the rebuild is load-bearing. 149 let nodes2: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 150 let classes2: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 151 let g2: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph 152 if nx_eqsat_init(g2, nodes2, cap_nodes, classes2, cap_cls) != NX_EQSAT_OK { sys_exit(20); return 20 } 153 let x2: i64 = nx_eqsat_add_var(g2, 0) 154 let c8b: i64 = nx_eqsat_add_const(g2, 8) 155 let c3b: i64 = nx_eqsat_add_const(g2, 3) 156 let mul8b: i64 = nx_eqsat_add_binary(g2, NX_EQ_OP_MUL, x2, c8b) 157 let shl3b: i64 = nx_eqsat_add_binary(g2, NX_EQ_OP_SHL, x2, c3b) 158 let neg_a2: i64 = nx_eqsat_add_unary(g2, NX_EQ_OP_NEG, mul8b) 159 let neg_b2: i64 = nx_eqsat_add_unary(g2, NX_EQ_OP_NEG, shl3b) 160 nx_eqsat_saturate(g2, 32) 161 // sanity: the children DID merge (mul_pow2), so the gap is purely congruence. 162 var children_merged_without_meet: i64 = 0 163 if nx_eqsat_find(g2, mul8b) == nx_eqsat_find(g2, shl3b) { children_merged_without_meet = 1 } 164 var case2_member: i64 = 0 165 if nx_eqsat_find(g2, neg_a2) == nx_eqsat_find(g2, neg_b2) { case2_member = 1 } 166 167 // ===================== CASE 3: NEGATIVE (non-congruent: diff op) ========== 168 // NEG(a) vs NOT(a): same child class, DIFFERENT op -> distinct fingerprints -> 169 // never merged. Proves the fingerprint folds op (no false CONGRUENCE merge). 170 let nodes3: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 171 let classes3: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 172 let g3: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph 173 if nx_eqsat_init(g3, nodes3, cap_nodes, classes3, cap_cls) != NX_EQSAT_OK { sys_exit(30); return 30 } 174 let hc3: *HashMap = nx_hmap_alloc(256) 175 let pn3: *i64 = sys_mmap(1024 * 8) as *i64 176 let pc3: *i64 = sys_mmap(1024 * 8) as *i64 177 let wl3: *i64 = sys_mmap(1024 * 8) as *i64 178 if nx_eqsat_enable_meet(g3, hc3, pn3, pc3, 1024, wl3, 1024) != NX_EQSAT_OK { sys_exit(31); return 31 } 179 let x3: i64 = nx_eqsat_add_var(g3, 0) 180 let neg3: i64 = nx_eqsat_add_unary(g3, NX_EQ_OP_NEG, x3) 181 let not3: i64 = nx_eqsat_add_unary(g3, NX_EQ_OP_NOT, x3) 182 nx_eqsat_saturate(g3, 32) 183 var case3_member: i64 = 0 184 if nx_eqsat_find(g3, neg3) == nx_eqsat_find(g3, not3) { case3_member = 1 } 185 186 // ===================== known answer + FAIL-LOUD ========================== 187 _emit_num(case1_member); _emit_num(cong_logged); _emit_num(none_count); 188 _emit_num(case2_member); _emit_num(case3_member); _nl() 189 190 gv_check("pre-state: the two NEG parents start in DIFFERENT classes" as *u8, pre_distinct == 1, ctr) 191 gv_check("saturation reached a fixpoint rather than hitting the iteration bound" as *u8, reached_fixpoint == 1, ctr) 192 gv_check("congruence DETECTED: after the deferred rebuild f(a) and f(b) share a class" as *u8, case1_member == 1, ctr) 193 gv_check("the congruence merge was CITED in the provenance log" as *u8, cong_logged == 1, ctr) 194 gv_check("every logged merge cites an allow-listed rule id" as *u8, any_bad == 0, ctr) 195 gv_check("no back-door RULE_NONE merge slipped in uncited" as *u8, none_count == 0, ctr) 196 gv_check("the provenance log is complete, not overflowed (fail-closed)" as *u8, g.prov_overflow == 0, ctr) 197 // THE TWO CONTROLS THAT MAKE THE POSITIVE MEAN SOMETHING. 198 // Without them, an engine that merged EVERYTHING would score full marks above. 199 gv_check("control: the children DO merge without meet, so the gap is purely congruence" as *u8, children_merged_without_meet == 1, ctr) 200 gv_check("neg-control-without-the-rebuild-the-parents-are-NOT-merged" as *u8, case2_member == 0, ctr) 201 gv_check("neg-control-same-child-DIFFERENT-op-NEG-vs-NOT-is-never-merged" as *u8, case3_member == 0, ctr) 202 203 return gv_verdict("nx_eqsat_congruence_test" as *u8, ctr, 204 "egg-style deferred congruence closure: cited, fail-closed provenance, with controls proving the rebuild is load-bearing and the fingerprint folds the operator" as *u8) 205}