nx_eqsat.nx source

1// nx_eqsat.nx -- equality-saturation framework (egg/SpEC family). 2// 3// Foundation for the superoptimization arc per ZERO_TO_ADVANCED.md M2: 4// "the system is the FASTEST possible at every layer". Equality 5// saturation is the 2026-research-grade approach -- developed by 6// Willsey/Tate/Bornholt (egg, 2021) + Tate et al (Equality Saturation 7// for Compiler Optimization, 2009), proven on Souper/Cranelift et al 8// production compilers. 9// 10// Why equality saturation vs traditional peephole: 11// Peephole: apply one rewrite, commit. If the rewrite was bad you 12// lose; if a better cascade existed but required first 13// un-doing a rewrite, you never find it. Phase-ordering 14// tyranny. 15// EqSat: keep ALL equivalent expressions in an e-graph. Apply 16// all rewrites breadth-first to saturation. Extract the 17// lowest-cost representative. Provably optimal under the 18// rule set + cost model. 19// 20// For RV64IM: lets the compiler find non-obvious wins like 21// (add x x) -> (shl x 1) (when shl is faster) 22// (shl (shl x a) b) -> (shl x (add a b)) (kill dependent chain) 23// (mul x 2^k) -> (shl x k) (strength reduction) 24// (and x (not (and ~a y))) -> ... (DeMorgan reroute) 25// 26// AND once silicon-feedback (rv64im_min_hot_report.nx) identifies hot 27// patterns, those become silicon-aware rewrites: 28// (popcount-naive-loop) -> (intrinsic popcount) when silicon has it 29// (gemm-inner-product) -> (vec mac fused) when SIMD lands 30// 31// Status: SEED. 2026-05-26. V1: e-class union-find + rule registry + 32// bounded saturation loop + greedy extractor. ~50 baseline rewrites 33// for RV64IM; extends per silicon-feedback findings. 34 35import "nx_syscalls.nx" 36import "nx_sketch_hash_map.nx" // sovereign (i64,i64) open-addressing primitive (DRY, Cardinal #15) -- the O(1) hashcons backing store 37import "nx_nxgate_sim.nx" // PROVEN op-semantics oracle (nx_gsim_eval_cell + NX_GATE_KIND_*) -- reused by the const-fold analysis (DRY). Import-dedup-safe (nx_import seen-set inlines it once; same organ nx_alu_divider already pulls it transitively). 38const NX_MAGIC_1024: i64 = 1024 39const NX_MAGIC_1000000000: i64 = 1000000000 40 41// ===== Expression node kinds (sealed enum) ================================================= 42// 43// Sealed at V1; extended as the rewrite set grows + new IR ops land. 44// Each kind has an arity (n_children) declared via nx_eqsat_arity_for. 45 46const NX_EQ_OP_CONST: i64 = 0 // 0 children; payload = i64 value 47const NX_EQ_OP_VAR: i64 = 1 // 0 children; payload = variable id 48const NX_EQ_OP_ADD: i64 = 2 // 2 children 49const NX_EQ_OP_SUB: i64 = 3 // 2 children 50const NX_EQ_OP_MUL: i64 = 4 // 2 children 51const NX_EQ_OP_DIV: i64 = 5 // 2 children 52const NX_EQ_OP_REM: i64 = 6 // 2 children 53const NX_EQ_OP_AND: i64 = 7 // 2 children 54const NX_EQ_OP_OR: i64 = 8 // 2 children 55const NX_EQ_OP_XOR: i64 = 9 // 2 children 56const NX_EQ_OP_NOT: i64 = 10 // 1 child 57const NX_EQ_OP_SHL: i64 = 11 // 2 children 58const NX_EQ_OP_SHR: i64 = 12 // 2 children (logical) 59const NX_EQ_OP_SAR: i64 = 13 // 2 children (arithmetic) 60const NX_EQ_OP_NEG: i64 = 14 // 1 child 61const NX_EQ_OP_EQ: i64 = 15 // 2 children 62const NX_EQ_OP_LT: i64 = 16 // 2 children (signed) 63const NX_EQ_OP_LTU: i64 = 17 // 2 children (unsigned) 64const NX_EQ_OP_SELECT: i64 = 18 // 3 children (mux) 65const NX_EQ_OP_POPCNT: i64 = 19 // 1 child (Zbb-equivalent) 66const NX_EQ_OP_N: i64 = 20 67 68func nx_eqsat_op_is_valid(op: i64) -> i64 { 69 if op < 0 { return 0 } 70 if op >= NX_EQ_OP_N { return 0 } 71 return 1 72} 73 74func nx_eqsat_arity_for(op: i64) -> i64 { 75 if op == NX_EQ_OP_CONST { return 0 } 76 if op == NX_EQ_OP_VAR { return 0 } 77 if op == NX_EQ_OP_NOT { return 1 } 78 if op == NX_EQ_OP_NEG { return 1 } 79 if op == NX_EQ_OP_POPCNT { return 1 } 80 if op == NX_EQ_OP_SELECT { return 3 } 81 return 2 82} 83 84// ===== E-node ================================================= 85// 86// An e-node is an op + a vector of e-class IDs (its children). Two 87// e-nodes are equivalent iff they have the same op + their children 88// resolve to the same e-classes (canonical reps). 89 90struct NxENode { 91 op: i64 92 n_kids: i64 93 kid0: i64 // e-class id; -1 if unused 94 kid1: i64 95 kid2: i64 96 payload: i64 // CONST value or VAR id 97 eclass: i64 // owning e-class id (canonicalised) 98} 99 100// ===== E-class ================================================= 101// 102// An equivalence class. Contains a set of equivalent e-nodes + a 103// canonical-id link for the union-find (egg-style). 104 105struct NxEClass { 106 canon: i64 // canonical id (this == self.id while not merged) 107 cost: i64 // best extraction cost in this class 108 best_node: i64 // node-array index of the cheapest 109 // ----- CONST-FOLD analysis lattice (egg e-class analysis) -- APPENDED ----- 110 // cf_val is the EXPLICIT const-analysis lattice element of this canonical class 111 // (egg's Analysis::Data = Option<i64>): NX_CF_NONE (i64 min) = "unknown/bottom" 112 // (no known constant); any other value = "this class is known-constant == cf_val". 113 // It is the MAKE/JOIN/MODIFY analysis store that replaces the old per-iteration 114 // full node-scan const-fold DISCOVERY with O(1)-amortized incremental work: 115 // MAKE (nx_eqsat_new_class / the add fast-path) -- born known for CONST nodes, 116 // computed once from children's cf_val for a foldable all-const op. 117 // JOIN (nx_eqsat_union_cited) -- lattice-meet flows the const 118 // along every union/congruence edge into VAR-rooted classes in O(1). 119 // MODIFY -- the NONE->known transition 120 // lazily materializes the CONST merge ONCE through the cited chokepoint. 121 // Appended AFTER best_node (no reorder; NxEClass 24B -> 32B, fits the 122 // pre-allocated cap_cls*32 stride EVERY gate harness mmaps). ALWAYS written in 123 // new_class; READ only when cf_on==1, so the cf_on==0 trajectory is byte-identical 124 // (dead state on the page-rounded class array, exactly like prov/meet/dsl slack). 125 cf_val: i64 126} 127 128// Const-analysis lattice SENTINEL: i64 minimum (0x8000000000000000) = "no known 129// constant / lattice bottom". Chosen as a value the gate-sim evaluator can in 130// principle produce, but the lattice tags by PRESENCE (a class whose true folded 131// value is i64-min still carries a real CONST best_node), so the sentinel collision 132// only means "MODIFY may re-run" which is idempotent + harmless (see make_join_modify). 133const NX_CF_NONE: i64 = 0 - 0x7FFFFFFFFFFFFFFF - 1 134 135// ===== RULE DSL (egg-style data-driven rewrite) ============================= 136// 137// A rewrite rule becomes a FLAT DATA RECORD (NxDslRule) interpreted by ONE 138// general e-matcher (nx_eqsat_apply_dsl_rule) -- the egg breadth path: many 139// rules cheaply + the SELF-AUTHORING hook (a new rule is just a data row the 140// invention loop can propose). The 7 hand-coded inline rules are RE-EXPRESSED as 141// a 7-row table (nx_eqsat_builtin_dsl_table) whose behavior is BYTE-IDENTICAL to 142// the inline functions (proven by the parity harness). The DSL path is OPT-IN 143// (NxEGraph.dsl null by default => the inline path runs verbatim). 144// 145// A rule's LHS is the shallow shape (lhs_op slotA slotB). Each slot is tagged: 146// DSL_VAR -- binds ?A/?B to ANY canonical e-class (a pattern variable) 147// DSL_CONST(val) -- the class's best_node must be a CONST whose payload == val 148// DSL_SAME_AS_A -- the class id must equal the already-bound ?A (the "x OP x") 149// The RHS is a CLOSED enum instantiated through the existing add* wrappers (no RHS 150// interpreter, no pointer pattern-tree, no allocator): 151// RHS_BIND_A | RHS_BIND_B | RHS_CONST(val) 152// RHS_SHL_A_BY_CONST(amt) | RHS_SHL_A_BY_LOG2B (strength-reduction shapes) 153// side_cond replays a width guard as DATA (SC_POW2_B_KLTW = the proven k<W 154// mul_pow2 guard). count_mode replays mul_pow2's real-merge counting (the only 155// mode that converges to SATURATED). dual_order replays firing both child 156// orderings (add_zero/or_zero) vs right-const-only (mul_one). 157 158const DSL_VAR:i64 = 0 159const DSL_CONST:i64 = 1 160const DSL_SAME_AS_A:i64 = 2 161 162const RHS_BIND_A:i64 = 0 163const RHS_BIND_B:i64 = 1 164const RHS_CONST:i64 = 2 165const RHS_SHL_A_BY_CONST:i64 = 3 166const RHS_SHL_A_BY_LOG2B:i64 = 4 167// RHS_SHL_A_BY_IADDED_J: emit (shl bindA (i+j)) where (i+j) is the COMPUTED summed 168// shift the shape-(d) shift-merge matcher hands to instantiate_rhs via `shamt` 169// (exactly as RHS_SHL_A_BY_LOG2B reuses shamt for the mul_pow2 log2). The DSL row 170// holds rhs_val=0 (the table is DATA -- it cannot carry the dynamic i+j); the 171// matcher reads i,j from the two CONST child classes and computes i+j itself. 172const RHS_SHL_A_BY_IADDED_J:i64 = 5 173 174const SC_NONE:i64 = 0 175const SC_POW2_B_KLTW:i64 = 1 176// SC_SHIFT_MERGE_IJW: the shift-merge side-condition carrying the i+j<W guard as 177// DATA (exactly as SC_POW2_B_KLTW=1 carries the mul_pow2 k<W guard). It also selects 178// the shape-(d) nested-SHL matcher: LHS is SHL(SHL(?x ?i) ?j), ?i,?j CONST, i+j<W. 179// At i+j>=W the merged (shl x (i+j)) count is out of range / x86-count-masked, so the 180// identity is UNSOUND (proven by nx_rs_shiftmerge_boundary_unsound) -- the matcher 181// refuses to fire there, mirroring mul_pow2's k<W refusal. 182const SC_SHIFT_MERGE_IJW:i64 = 2 183 184const CNT_EVERY:i64 = 0 // count every match (the 6 V1 rules' behavior) 185const CNT_REAL_MERGE:i64 = 1 // count only real find!=find merges (mul_pow2) 186 187// A rewrite rule as data. lhs is (lhs_op a_kind/a_val b_kind/b_val); rhs is the 188// closed-enum template (rhs_kind/rhs_val). side_cond + count_mode + dual_order 189// replay the per-rule behavioral knobs the inline functions hard-coded. 190struct NxDslRule { 191 rule_id: i64 192 lhs_op: i64 193 a_kind: i64 194 a_val: i64 195 b_kind: i64 196 b_val: i64 197 rhs_kind: i64 198 rhs_val: i64 199 side_cond: i64 200 count_mode: i64 201 dual_order: i64 202} 203 204// ===== E-graph ================================================= 205// 206// V1 fixed-capacity storage. Caller allocates the nodes + classes 207// arrays; the e-graph owns indices into them. 208 209// PROVENANCE FIELDS (prov..prov_overflow) are APPENDED -- never reorder 210// nodes..valid; every caller depends on those offsets. They default OFF (prov 211// null) so the four gated organs behave byte-identically. When enabled via 212// nx_eqsat_enable_prov, the single union chokepoint (nx_eqsat_union_cited) logs 213// the citing rule-id of EVERY real merge -- a merge cannot happen without a 214// rule-id flowing through the one function that mutates canon (no bypass). 215struct NxEGraph { 216 nodes: *NxENode 217 n_nodes: i64 218 cap_nodes: i64 219 classes: *NxEClass 220 n_classes: i64 221 cap_classes: i64 222 valid: i64 223 prov: *i64 // APPENDED: rule-id log buffer; null => provenance OFF 224 n_prov: i64 // APPENDED: # rule-ids logged so far 225 cap_prov: i64 // APPENDED: capacity of prov[] 226 prov_overflow: i64 // APPENDED: 1 iff a logged merge could not fit (fail-closed) 227 // ----- MEET fields (egg hashcons + congruence rebuild) -- APPENDED, opt-in ----- 228 // All default null/0 in nx_eqsat_init so EVERY existing caller + the four gated 229 // organs stay byte-identical (the linear-scan path runs when hc==null and the 230 // rebuild path is skipped when rebuild_on==0). Turned on per-e-graph via 231 // nx_eqsat_enable_meet, which hands the engine caller-owned scratch. 232 hc: *HashMap // hashcons: fingerprint(op,payload,canon kids) -> node-array idx; null => O(n) linear scan 233 par_node: *i64 // parent index: par_node[i] = a node that references par_cls[i] as a (canonical) child 234 par_cls: *i64 // parallel array: the canonical child-class of that parent edge 235 n_par: i64 // # parent edges recorded 236 cap_par: i64 // capacity of par_node/par_cls 237 par_overflow: i64 // 1 iff a parent edge could not fit (rebuild then falls back to full-scan -> still complete) 238 worklist: *i64 // dirty canonical e-class ids pending congruence repair 239 n_work: i64 // # entries in worklist 240 cap_work: i64 // capacity of worklist 241 rebuild_on: i64 // 1 => unions push dirty classes + saturate calls rebuild; 0 => original loop verbatim 242 // ----- DSL fields (egg data-driven rewrite) -- APPENDED, opt-in ----- 243 // All default null/0 in nx_eqsat_init so EVERY existing caller + the four gated 244 // organs stay BYTE-IDENTICAL: when dsl==null, nx_eqsat_saturate runs the verbatim 245 // 7 inline rule calls; when dsl!=null it runs the general e-matcher over the table. 246 // Turned on per-e-graph via nx_eqsat_enable_dsl (caller hands a *NxDslRule table). 247 // Appending here is safe: every test over-allocates NxEGraph via page-rounded 248 // sys_mmap (4096-byte page for a <200-byte struct), so the new fields fit. 249 dsl: *NxDslRule // rule table; null => DSL OFF (inline path runs) 250 n_dsl: i64 // # rules in the table 251 cap_dsl: i64 // capacity (diagnostic; n_dsl is authoritative) 252 // ----- CONST-FOLD field (egg e-class analysis) -- APPENDED, opt-in ----- 253 // The const-fold analysis hook in nx_eqsat_add is GATED on this flag (default 0 254 // in nx_eqsat_init, set only by nx_eqsat_enable_constfold), mirroring the 255 // prov/meet/dsl append-only + opt-in precedent. When cf_on==0 the hook is a 256 // no-op so EVERY existing caller's node/class/prov trajectory is byte-identical 257 // BY CONSTRUCTION. One i64 appended after the dsl block; NxENode (56B/64B stride) 258 // and NxEClass (24B) get ZERO new fields. NxEGraph is page-rounded via sys_mmap 259 // (4096-byte page for a <300-byte struct) so the new field fits with no reorder. 260 cf_on: i64 // 1 => const-fold fires at node creation; 0 => OFF (default) 261 // ----- CONST-VALUE INTERN CACHE (the O(1) MODIFY backing store) -- APPENDED ----- 262 // The const-fold MODIFY step materializes CONST(value) e-classes; the V1 263 // nx_eqsat_add_const did an O(n) linear node scan to hashcons each one, which -- 264 // doubled with the O(n) binop scan -- IS the measured ~10x const-fold-bench lapp 265 // (build phase = ~96% of the bench, profiled). cf_cache is a tiny open-addressing 266 // (value -> class-id) intern map so an interned CONST is O(1) instead of O(n), 267 // turning the whole eager-fold build into O(N) amortized (matches egg's interned 268 // Num leaves). Lazily mmap'd by nx_eqsat_enable_constfold (so default callers pay 269 // nothing); null => the cache is OFF and nx_cf_intern_const falls back to the 270 // O(n) nx_eqsat_add_const (always correct, just slower). Appended after cf_on 271 // (no reorder; NxEGraph is page-rounded via sys_mmap so the new fields fit). 272 cf_cache: *i64 // 2*cap entries: [value, class_id] pairs; null => cache OFF 273 cf_cache_cap: i64 // # slots (power-of-2); 0 => OFF 274 cf_cache_n: i64 // # live entries (for load-factor / fail-open-to-scan) 275 cf_poison: i64 // 1 iff a JOIN saw a contradiction (two unequal consts in 276 // one class) -> fail-CLOSED soft poison (NOT sys_exit; 277 // Global Rule #14 graceful degradation -- a library must 278 // not crash its host on internal state). Surfaced for a 279 // future certifier reject; never reached by a sound graph. 280 cf_scratch: *i64 // GRAPH-LIFETIME scratch (>=4 i64) for the fold child-value 281 // reads. Allocated ONCE in enable_constfold so the hot 282 // fold path needs ZERO per-node sys_mmap (the per-call 283 // sys_mmap(8) was the dominant build-phase cost -- each 284 // mmap is a syscall ~1us, x #ops x #iters). null => OFF. 285 // ----- WORKLIST-DRIVEN INCREMENTAL RULE MATCHING -- APPENDED, opt-in (4th layer) --- 286 // egg's keystone scheduler win: the saturate loop must NOT full-scan all n_nodes per 287 // rule per iteration (O(n*K*iters)). Instead it matches rules ONLY against worklist 288 // items: (a) newly-added nodes (tracked by the rising n_nodes frontier, so EVERY 289 // alloc site -- PATH A/B/constfold/RHS -- is covered with zero per-site hooks) and 290 // (b) parents of a class just merged (enqueued by nx_eqsat_union_cited via the parent 291 // back-index). Drained to fixpoint. PROVABLY complete: a shallow-LHS match becomes 292 // newly-possible ONLY when a node is created (a) or one of its children is re- 293 // canonicalized by a union (b) -- egg's rebuild theorem. mwl is a SEPARATE worklist 294 // from the congruence `worklist` (which rebuild clobbers at its top, line g.n_work=0), 295 // so the two never alias. Auto-armed by nx_eqsat_enable_meet (the par-index that (b) 296 // needs lives there, and meet forces hc!=null => ALL nodes go through PATH A => the 297 // par-index is complete -- closing the PATH-B parent-gap trap). match_on default 0 in 298 // nx_eqsat_init => every existing caller + the 6 non-meet certs run the VERBATIM 299 // full-scan saturate => byte-identical by construction. Appended at the tail (no 300 // reorder); NxEGraph is page-rounded via sys_mmap so the new i64s fit. 301 mwl: *i64 // match-worklist: NODE indices pending rule re-match; null => OFF 302 n_mwl: i64 // # entries in the match-worklist 303 cap_mwl: i64 // capacity of mwl 304 match_on: i64 // 1 => worklist-driven incremental match; 0 => verbatim full-scan 305 mwl_overflow: i64 // 1 iff a push could not fit -> saturate fail-OPENS to full-scan 306 // (provably complete fallback, just the old O(n) scan) 307} 308 309const NX_EQSAT_OK: i64 = 0 310const NX_EQSAT_BAD_OP: i64 = 1 311const NX_EQSAT_BAD_ARITY: i64 = 2 312const NX_EQSAT_OVERFLOW: i64 = 3 313const NX_EQSAT_SATURATED: i64 = 4 314const NX_EQSAT_STEP_BUDGET: i64 = 5 315 316// ===== Rule identifiers (SINGLE SOURCE OF TRUTH) ============================ 317// 318// The saturator cites one of these at each union site so the live provenance 319// log records WHICH rule created each merge edge. The membership-proof organ 320// imports + asserts MP_RULE_* == these (lockstep, no parallel namespace drift). 321// NX_EQSAT_RULE_NONE is the sentinel for any merge that did NOT cite a rule 322// (e.g. a direct nx_eqsat_union call) -- it is NOT in any proven-sound set, so 323// an unlogged-but-cited-NONE merge POISONS a certificate (fail-closed bypass). 324 325const NX_EQSAT_RULE_NONE: i64 = 0 326const NX_EQSAT_RULE_ADD_ZERO: i64 = 1 327const NX_EQSAT_RULE_SUB_SELF: i64 = 2 328const NX_EQSAT_RULE_ADD_SELF: i64 = 3 329const NX_EQSAT_RULE_AND_SELF: i64 = 4 330const NX_EQSAT_RULE_OR_ZERO: i64 = 5 331const NX_EQSAT_RULE_MUL_ONE: i64 = 6 332const NX_EQSAT_RULE_MUL_POW2: i64 = 7 333// CONGRUENCE: the structural law of equality -- if a==b (same canonical class) then 334// f(...a...)==f(...b...) because f is a deterministic function of its children. It is 335// width-independent and needs NO arithmetic battery (unlike the 7 identity rules); its 336// soundness proof IS the congruence axiom. Cited by the deferred rebuild ONLY, through 337// the same nx_eqsat_union_cited chokepoint, so it is logged + admitted to the 338// membership-proof's proven-sound allow-list (no RULE_NONE bypass). [CANON: Willsey 339// et al, egg, PLDI 2021 -- deferred rebuild + hashcons invariant.] 340const NX_EQSAT_RULE_CONGRUENCE: i64 = 8 341// XOR_SELF: (xor x x) == 0 -- self-cancellation. Width-independent (a^a=0 holds per 342// bit at ANY W, same per-bit-law class as and_self/or_zero), so the W=8 exhaustive 343// battery lifts to W=64. Admitted to the proven-sound set ONLY after the all-W 344// two-witness soundness battery certifies it (see nx_eqsat_membership_proof.nx 345// mp_battery_xor_self). It is the FIRST rule expressed PURELY as DSL data (one 346// NxDslRule row, zero new matcher control flow) -- the breadth-via-data proof. 347const NX_EQSAT_RULE_XOR_SELF: i64 = 9 348// CONSTFOLD: (op c0 c1 ...) where EVERY child class is a known constant => merge 349// with CONST(eval(op, c0, c1, ...)). This is egg's canonical e-class ANALYSIS 350// (constant folding / propagation): the analysis value of a class is "CONST V" 351// iff its best_node is a CONST node, and it lives IMPLICITLY in NxEClass.best_node 352// (no new struct field). Soundness = the PROVEN op-semantics evaluator 353// nx_gsim_eval_cell (the same oracle the divider/multiplier proofs + the 354// membership-proof's _mp_eval_op_const trust). Only ops whose gate-sim cell is the 355// proven semantics of the eqsat op are foldable (nx_eqsat_op_to_gate_kind admits 356// them; DIV/REM/SAR/SHR/NEG/POPCNT/SELECT are REFUSED -- no faithful cell, see the 357// map). Width-independent: the engine works at W=64 and i64 arithmetic IS mod-2^64, 358// so the raw evaluator output is exactly the W=64 value (no truncation gap). The 359// merge flows the single chokepoint (nx_eqsat_union_cited) citing this id, so it is 360// logged + certifiable. Admitted to the membership-proof allow-list + lockstep. 361const NX_EQSAT_RULE_CONSTFOLD: i64 = 10 362// SHIFT_MERGE: (shl (shl ?x ?i) ?j) == (shl ?x (?i+?j)) for ?i,?j CONST and i+j<W. 363// THEOREM: (x<<i)<<j == x<<(i+j) (mod 2^W) for all i,j>=0 with i+j<W -- left-shift 364// distributes over the mod (2^j is a factor), width-independent by k-induction on 365// (i+j) (the SAME inductive shape mul_pow2 uses), so the W=8 machine-check lifts to 366// W=64. Admitted to the proven-sound set ONLY after the all-W two-witness battery 367// certifies it in-range AND the i+j>=W boundary is shown unsound (the i+j<W guard's 368// home). It is the SECOND rule expressed PURELY as DSL data (one NxDslRule row, 369// shape (d): the LHS first child is itself a structural SHL, distinct from xor_self's 370// shape (a)/mul_pow2's shape (b)/add_zero's const-slot shape (c)). The merge flows 371// the single cited chokepoint (nx_eqsat_union_cited) so it is logged + certifiable. 372const NX_EQSAT_RULE_SHIFT_MERGE: i64 = 11 373const NX_EQSAT_RULE_N: i64 = 12 374 375// ===== Init ================================================= 376 377func nx_eqsat_init(g: *NxEGraph, 378 nodes: *NxENode, cap_nodes: i64, 379 classes: *NxEClass, cap_classes: i64) -> i64 { 380 if (g as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 381 if (nodes as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 382 if (classes as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 383 g.nodes = nodes 384 g.n_nodes = 0 385 g.cap_nodes = cap_nodes 386 g.classes = classes 387 g.n_classes = 0 388 g.cap_classes = cap_classes 389 g.valid = 1 390 // Provenance OFF by default (signature unchanged): null buffer => the union 391 // chokepoint's log call short-circuits, so all existing callers + the four 392 // gated organs are byte-identical. 393 g.prov = 0 as *i64 394 g.n_prov = 0 395 g.cap_prov = 0 396 g.prov_overflow = 0 397 // MEET fields OFF by default (null/0) => linear-scan add + no rebuild => byte-identical. 398 g.hc = 0 as *HashMap 399 g.par_node = 0 as *i64 400 g.par_cls = 0 as *i64 401 g.n_par = 0 402 g.cap_par = 0 403 g.par_overflow = 0 404 g.worklist = 0 as *i64 405 g.n_work = 0 406 g.cap_work = 0 407 g.rebuild_on = 0 408 // DSL OFF by default (null/0) => nx_eqsat_saturate runs the verbatim inline rules. 409 g.dsl = 0 as *NxDslRule 410 g.n_dsl = 0 411 g.cap_dsl = 0 412 // CONST-FOLD OFF by default (0) => the node-creation hook is a no-op => every 413 // existing caller is byte-identical. Turned on only via nx_eqsat_enable_constfold. 414 g.cf_on = 0 415 // CONST-VALUE intern cache OFF by default (null/0) => nx_cf_intern_const falls 416 // back to the O(n) add_const => byte-identical. Armed by enable_constfold. 417 g.cf_cache = 0 as *i64 418 g.cf_cache_cap = 0 419 g.cf_cache_n = 0 420 g.cf_poison = 0 421 g.cf_scratch = 0 as *i64 422 // INCREMENTAL MATCH OFF by default (null/0) => nx_eqsat_saturate runs the verbatim 423 // full-scan; the union (b)-hook + alloc (a)-frontier are inert => byte-identical. 424 g.mwl = 0 as *i64 425 g.n_mwl = 0 426 g.cap_mwl = 0 427 g.match_on = 0 428 g.mwl_overflow = 0 429 return NX_EQSAT_OK 430} 431 432// ===== Opt-in provenance ==================================================== 433// 434// Turn ON rule-id logging by handing the e-graph a caller-owned i64 buffer of 435// `cap` slots. After this, every REAL merge logs its citing rule-id. Existing 436// callers never call this, so prov stays null => byte-identical behavior. 437func nx_eqsat_enable_prov(g: *NxEGraph, buf: *i64, cap: i64) -> i64 { 438 if (g as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 439 if (buf as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 440 g.prov = buf 441 g.n_prov = 0 442 g.cap_prov = cap 443 g.prov_overflow = 0 444 return NX_EQSAT_OK 445} 446 447// Log one rule-id for a real merge. No-op when prov is OFF (null) -> returns 0 448// and never mutates the graph (the byte-identical guarantee). When ON, appends 449// rule_id; on capacity overflow it FAILS CLOSED -- sets prov_overflow so the 450// certifier can never pass on a truncated (incomplete) log. 451func nx_eqsat_log_rule(g: *NxEGraph, rule_id: i64) -> i64 { 452 if (g.prov as i64) == 0 { return 0 } 453 if g.n_prov >= g.cap_prov { 454 g.prov_overflow = 1 455 return 0 - NX_EQSAT_OVERFLOW 456 } 457 g.prov[g.n_prov] = rule_id 458 g.n_prov = g.n_prov + 1 459 return NX_EQSAT_OK 460} 461 462// ===== MEET: opt-in hashcons + congruence rebuild =========================== 463// 464// Turn ON the egg-style O(1) hashcons + deferred congruence closure by handing 465// the e-graph caller-owned scratch: 466// hc -- a *HashMap (nx_hmap_alloc'd, power-of-2, sized > nodes/0.7) used 467// as the (fingerprint -> node-idx) intern table (replaces the O(n) 468// linear scan in nx_eqsat_add with an O(1)-avg lookup). 469// par_node/par_cls (cap_par) -- the parent back-index: each new node registers 470// itself as a parent of each of its canonical child classes, so the 471// rebuild can enumerate f(a) when a merges. 472// worklist (cap_work) -- dirty canonical class ids pending congruence repair. 473// After this, rebuild_on=1: every real union pushes its winner onto the worklist 474// and nx_eqsat_saturate drains the worklist to a congruence fixpoint each 475// iteration. Existing callers never call this, so the engine is byte-identical. 476func nx_eqsat_enable_meet(g: *NxEGraph, hc: *HashMap, 477 par_node: *i64, par_cls: *i64, cap_par: i64, 478 worklist: *i64, cap_work: i64) -> i64 { 479 if (g as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 480 if (hc as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 481 if (par_node as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 482 if (par_cls as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 483 if (worklist as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 484 g.hc = hc 485 g.par_node = par_node 486 g.par_cls = par_cls 487 g.n_par = 0 488 g.cap_par = cap_par 489 g.par_overflow = 0 490 g.worklist = worklist 491 g.n_work = 0 492 g.cap_work = cap_work 493 g.rebuild_on = 1 494 // AUTO-ARM worklist-driven incremental rule matching: enable_meet is the natural 495 // (and only) place -- the parent back-index that the (b) re-match needs lives HERE, 496 // and meet forces hc!=null so EVERY node (incl rule-RHS) is allocated through PATH A. 497 // match_on=1 makes nx_eqsat_saturate match rules against ONLY the new-node frontier 498 // (enqueue (a)) while quiescent, and re-scan the node set ONCE per outer iteration 499 // when a merge dirtied children (enqueue (b), set by union_cited). This is a pure 500 // speed scheduler change: the merge multiset, provenance ids, and SATURATED return 501 // are unchanged -- it only prunes the no-change nodes the full-scan re-checked for 502 // nothing each iteration. The mwl_overflow flag doubles as the (b) "merge happened" 503 // signal; mwl/n_mwl/cap_mwl stay null/0 (the flag-based scheme needs no buffer). 504 g.match_on = 1 505 g.mwl_overflow = 0 506 return NX_EQSAT_OK 507} 508 509// ===== Opt-in DSL (egg data-driven rewrite) ================================= 510// 511// Turn ON the general e-matcher by handing the e-graph a caller-owned *NxDslRule 512// table of `n` rules. After this, nx_eqsat_saturate applies the DATA rules via 513// nx_eqsat_apply_dsl_rule (one e-matcher) instead of the 7 inline functions. 514// Existing callers never call this => dsl stays null => byte-identical engine. 515// The CALLER is responsible for only loading rules whose ids are in the 516// membership-proof's proven-sound allow-list (the certifier fail-closes on any 517// un-admitted id, so a wrong table cannot silently certify). 518func nx_eqsat_enable_dsl(g: *NxEGraph, table: *NxDslRule, n: i64, cap: i64) -> i64 { 519 if (g as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 520 if (table as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 521 g.dsl = table 522 g.n_dsl = n 523 g.cap_dsl = cap 524 return NX_EQSAT_OK 525} 526 527// ===== Opt-in CONST-FOLD (egg e-class analysis) ============================= 528// 529// Turn ON constant folding: when EVERY child of a newly-added arithmetic e-node is 530// a known constant, the node is evaluated via the PROVEN op-semantics oracle 531// (nx_gsim_eval_cell) and its e-class is merged with a CONST e-class of the result, 532// citing NX_EQSAT_RULE_CONSTFOLD through the single union chokepoint (logged + 533// certifiable). Existing callers never call this => cf_on stays 0 => the node- 534// creation hook is a no-op => the engine is byte-identical. The folded equality is 535// sound by EVALUATION (the gate-sim is the proven semantics), so no separate W-bit 536// battery is needed (parallel to how CONGRUENCE is admitted to the sound set). 537func nx_eqsat_enable_constfold(g: *NxEGraph) -> i64 { 538 if (g as i64) == 0 { return 0 - NX_EQSAT_BAD_OP } 539 g.cf_on = 1 540 // Arm the O(1) const-value intern cache (the MODIFY backing store). A power-of-2 541 // open-addressing map sized so the engine never linear-scans for a folded CONST; 542 // on miss/full it fail-OPENS to the correct O(n) add_const, so correctness never 543 // depends on the cache, only speed. CF_CACHE_CAP slots * 2 i64 (value, class+1). 544 // SYS_MMAP (MAP_PRIVATE|MAP_ANONYMOUS, flags 0x22) is KERNEL-ZERO-FILLED, so the 545 // slots start empty (stored class+1 == 0 => empty marker) with NO init loop -- 546 // the per-call zeroing was an 8192-write-per-iter regression; relying on the 547 // zero-fill guarantee makes enable_constfold O(1). cf_cache stays null on an 548 // mmap failure => nx_cf_intern_const fail-OPENS to add_const (correct, slower). 549 let cap: i64 = NX_MAGIC_1024 // >> #distinct consts in any V1 graph; 550 // 1024*2*8 = 16KB (4 pages) -- small 551 // enough to keep init page-fault cost 552 // negligible, big enough to stay sparse. 553 let buf: *i64 = sys_mmap(cap * 2 * 8) as *i64 554 if (buf as i64) != 0 { 555 g.cf_cache = buf 556 g.cf_cache_cap = cap 557 g.cf_cache_n = 0 558 } 559 g.cf_poison = 0 560 // ONE graph-lifetime scratch buffer for the hot fold path's child-value reads -- 561 // eliminates the per-node sys_mmap(8) (the syscall that dominated the build). 562 g.cf_scratch = sys_mmap(32) as *i64 563 return NX_EQSAT_OK 564} 565 566// Create a fresh CONST e-node + class WITHOUT the O(n) linear-scan hashcons (the 567// cache IS the const hashcons when armed, so a scan would be redundant). Used by the 568// intern map miss path + the add() CONST fast path. new_class sets cf_val=value (the 569// MAKE leaf base case). Returns the new class id, or an overflow code. 570func nx_cf_make_const_node(g: *NxEGraph, value: i64) -> i64 { 571 if g.n_nodes >= g.cap_nodes { return 0 - NX_EQSAT_OVERFLOW } 572 let nidx: i64 = g.n_nodes 573 g.nodes[nidx].op = NX_EQ_OP_CONST 574 g.nodes[nidx].n_kids = 0 575 g.nodes[nidx].kid0 = 0 - 1 576 g.nodes[nidx].kid1 = 0 - 1 577 g.nodes[nidx].kid2 = 0 - 1 578 g.nodes[nidx].payload = value 579 g.n_nodes = nidx + 1 580 return nx_eqsat_new_class(g, nidx, 0) // CONST cost == 0 581} 582 583// O(1) const-value intern map (the MODIFY materialization store + the CONST hashcons 584// when const-fold is armed). Returns the canonical class-id of CONST(value), reusing 585// an existing one when present so the engine never grows duplicate CONST nodes AND 586// never linear-scans for them -- killing the O(n^2) const-add term that (with the 587// per-fold mmap, now also removed) was the measured build-phase lapp. Open addressing 588// (mix-probe) keyed by value; slot[1] stores class+1, 0 == EMPTY (kernel-zero-filled 589// mmap). HIT => re-canonicalize via find (a merged const class stays addressable). 590// MISS => create the node once (NO scan) + record. FAIL-OPEN: cache OFF/full/mmap- 591// failed => delegate to nx_eqsat_add_const (correct, O(n)) so correctness never 592// depends on the cache, only speed. 593func nx_cf_intern_const(g: *NxEGraph, value: i64) -> i64 { 594 if (g.cf_cache as i64) == 0 { return nx_eqsat_add_const(g, value) } 595 let cap: i64 = g.cf_cache_cap 596 if cap <= 0 { return nx_eqsat_add_const(g, value) } 597 let mask: i64 = cap - 1 598 var h: i64 = nx_eqsat_mix(value + 1) & mask 599 var probes: i64 = 0 600 while probes < cap { 601 // slot stores class+1 in the second word; 0 == EMPTY (kernel-zero-filled mmap, 602 // no init loop). A real class 0 stores as 1, so 0 unambiguously means empty. 603 let enc: i64 = g.cf_cache[h * 2 + 1] 604 if enc == 0 { 605 // empty slot: MISS -> materialize the CONST once (NO scan), record, return. 606 let nc: i64 = nx_cf_make_const_node(g, value) 607 if nc < 0 { return nc } 608 g.cf_cache[h * 2] = value 609 g.cf_cache[h * 2 + 1] = nc + 1 // store class+1 (0 reserved for empty) 610 g.cf_cache_n = g.cf_cache_n + 1 611 return nc 612 } 613 if g.cf_cache[h * 2] == value { 614 // HIT: re-canonicalize (the const class may have merged). 615 return nx_eqsat_find(g, enc - 1) 616 } 617 h = (h + 1) & mask 618 probes = probes + 1 619 } 620 // table full (never reached for V1 graphs): fail-OPEN to the correct O(n) path. 621 return nx_eqsat_add_const(g, value) 622} 623 624// Fill `table` (caller-owned, >= 7 rows) with the 7 V1 rules RE-EXPRESSED as data. 625// This table, applied by the e-matcher, is BYTE-IDENTICAL to the inline saturate 626// (proven by nx_eqsat_dsl_parity_test.nx). The row order MATCHES the inline call 627// order in nx_eqsat_saturate (add_zero, sub_self, add_self, and_self, or_zero, 628// mul_one, mul_pow2) so the merge sequence -- and thus best_node/cost/log -- is 629// identical. Returns the number of rows written (7). A caller wanting the new 630// xor_self rule appends row 7 itself (see nx_eqsat_dsl_set_row). 631func nx_eqsat_builtin_dsl_table(table: *NxDslRule) -> i64 { 632 // add_zero: (add x 0)==x. dual_order (const may be on either side); count every. 633 table[0].rule_id = NX_EQSAT_RULE_ADD_ZERO; table[0].lhs_op = NX_EQ_OP_ADD 634 table[0].a_kind = DSL_VAR; table[0].a_val = 0 635 table[0].b_kind = DSL_CONST; table[0].b_val = 0 636 table[0].rhs_kind = RHS_BIND_A; table[0].rhs_val = 0 637 table[0].side_cond = SC_NONE; table[0].count_mode = CNT_EVERY; table[0].dual_order = 1 638 // sub_self: (sub x x)==0. b is SAME_AS_A; rhs const 0; count every. 639 table[1].rule_id = NX_EQSAT_RULE_SUB_SELF; table[1].lhs_op = NX_EQ_OP_SUB 640 table[1].a_kind = DSL_VAR; table[1].a_val = 0 641 table[1].b_kind = DSL_SAME_AS_A; table[1].b_val = 0 642 table[1].rhs_kind = RHS_CONST; table[1].rhs_val = 0 643 table[1].side_cond = SC_NONE; table[1].count_mode = CNT_EVERY; table[1].dual_order = 0 644 // add_self: (add x x)==(shl x 1). b SAME_AS_A; rhs shl A by const 1. 645 table[2].rule_id = NX_EQSAT_RULE_ADD_SELF; table[2].lhs_op = NX_EQ_OP_ADD 646 table[2].a_kind = DSL_VAR; table[2].a_val = 0 647 table[2].b_kind = DSL_SAME_AS_A; table[2].b_val = 0 648 table[2].rhs_kind = RHS_SHL_A_BY_CONST; table[2].rhs_val = 1 649 table[2].side_cond = SC_NONE; table[2].count_mode = CNT_EVERY; table[2].dual_order = 0 650 // and_self: (and x x)==x. b SAME_AS_A; rhs bind A. 651 table[3].rule_id = NX_EQSAT_RULE_AND_SELF; table[3].lhs_op = NX_EQ_OP_AND 652 table[3].a_kind = DSL_VAR; table[3].a_val = 0 653 table[3].b_kind = DSL_SAME_AS_A; table[3].b_val = 0 654 table[3].rhs_kind = RHS_BIND_A; table[3].rhs_val = 0 655 table[3].side_cond = SC_NONE; table[3].count_mode = CNT_EVERY; table[3].dual_order = 0 656 // or_zero: (or x 0)==x. dual_order; count every. 657 table[4].rule_id = NX_EQSAT_RULE_OR_ZERO; table[4].lhs_op = NX_EQ_OP_OR 658 table[4].a_kind = DSL_VAR; table[4].a_val = 0 659 table[4].b_kind = DSL_CONST; table[4].b_val = 0 660 table[4].rhs_kind = RHS_BIND_A; table[4].rhs_val = 0 661 table[4].side_cond = SC_NONE; table[4].count_mode = CNT_EVERY; table[4].dual_order = 1 662 // mul_one: (mul x 1)==x. RIGHT-const only (matches inline: only k1 checked). 663 table[5].rule_id = NX_EQSAT_RULE_MUL_ONE; table[5].lhs_op = NX_EQ_OP_MUL 664 table[5].a_kind = DSL_VAR; table[5].a_val = 0 665 table[5].b_kind = DSL_CONST; table[5].b_val = 1 666 table[5].rhs_kind = RHS_BIND_A; table[5].rhs_val = 0 667 table[5].side_cond = SC_NONE; table[5].count_mode = CNT_EVERY; table[5].dual_order = 0 668 // mul_pow2: (mul x 2^k)==(shl x k) for 1<=k<W. dual_order (const either side); 669 // side_cond = the k<W power-of-two guard; count only REAL merges (converges). 670 table[6].rule_id = NX_EQSAT_RULE_MUL_POW2; table[6].lhs_op = NX_EQ_OP_MUL 671 table[6].a_kind = DSL_VAR; table[6].a_val = 0 672 table[6].b_kind = DSL_CONST; table[6].b_val = 0 // b_val unused (matched by SC) 673 table[6].rhs_kind = RHS_SHL_A_BY_LOG2B; table[6].rhs_val = 0 674 table[6].side_cond = SC_POW2_B_KLTW; table[6].count_mode = CNT_REAL_MERGE; table[6].dual_order = 1 675 return 7 676} 677 678// Author one DSL row (used to append the new xor_self rule as DATA). 679func nx_eqsat_dsl_set_row(table: *NxDslRule, i: i64, rule_id: i64, lhs_op: i64, 680 a_kind: i64, a_val: i64, b_kind: i64, b_val: i64, 681 rhs_kind: i64, rhs_val: i64, 682 side_cond: i64, count_mode: i64, dual_order: i64) -> i64 { 683 table[i].rule_id = rule_id 684 table[i].lhs_op = lhs_op 685 table[i].a_kind = a_kind 686 table[i].a_val = a_val 687 table[i].b_kind = b_kind 688 table[i].b_val = b_val 689 table[i].rhs_kind = rhs_kind 690 table[i].rhs_val = rhs_val 691 table[i].side_cond = side_cond 692 table[i].count_mode = count_mode 693 table[i].dual_order = dual_order 694 return 0 695} 696 697// splitmix step (the same mix nx_hmap_hash applies to its key) -- one round. 698func nx_eqsat_mix(h: i64) -> i64 { 699 return (h * 0x9E3779B97F4A7C15) & 0xFFFFFFFFFFFFFFFF 700} 701 702// Fingerprint of an e-node = (op, payload, canonical kid0..2) folded to one i64. 703// +1/+2 sentinel offsets: the -1 "unused child" never aliases class 0, and CONST 0 704// vs CONST 1 differ via payload. Clamped away from 0/-1 which nx_sketch_hash_map 705// reserves as EMPTY/TOMBSTONE keys. Identity is ALWAYS re-verified against the node 706// array on a hashcons hit, so a 64-bit collision can never return/merge a wrong class. 707func nx_eqsat_fingerprint(op: i64, payload: i64, kc0: i64, kc1: i64, kc2: i64) -> i64 { 708 var fp: i64 = nx_eqsat_mix(op + 1) 709 fp = nx_eqsat_mix(fp ^ (payload + 1)) 710 fp = nx_eqsat_mix(fp ^ (kc0 + 2)) 711 fp = nx_eqsat_mix(fp ^ (kc1 + 2)) 712 fp = nx_eqsat_mix(fp ^ (kc2 + 2)) 713 if fp == 0 { fp = 0x1234567 } // never the EMPTY sentinel 714 if fp == 0 - 1 { fp = 0x7654321 } // never the TOMBSTONE sentinel 715 return fp 716} 717 718// Re-verify that node `nidx` really is the e-node (op,payload,kc0..2) -- the node 719// array is the source of truth; the hashcons is only a hint. Children compared by 720// CANONICAL class so union re-pointing is followed. Returns 1 iff a genuine match. 721func nx_eqsat_node_matches(g: *NxEGraph, nidx: i64, op: i64, payload: i64, 722 kc0: i64, kc1: i64, kc2: i64) -> i64 { 723 if g.nodes[nidx].op != op { return 0 } 724 if g.nodes[nidx].payload != payload { return 0 } 725 let arity: i64 = nx_eqsat_arity_for(op) 726 if g.nodes[nidx].n_kids != arity { return 0 } 727 var matched: i64 = 1 728 if arity >= 1 { if nx_eqsat_find(g, g.nodes[nidx].kid0) != kc0 { matched = 0 } } 729 if arity >= 2 { if nx_eqsat_find(g, g.nodes[nidx].kid1) != kc1 { matched = 0 } } 730 if arity >= 3 { if nx_eqsat_find(g, g.nodes[nidx].kid2) != kc2 { matched = 0 } } 731 return matched 732} 733 734// Record a parent edge (node `nidx` references canonical class `child_cls`). On 735// overflow set par_overflow -> rebuild then enumerates parents by full node scan 736// (provably complete, just slower). No-op when the parent index is OFF. 737func nx_eqsat_add_parent(g: *NxEGraph, nidx: i64, child_cls: i64) -> i64 { 738 if (g.par_node as i64) == 0 { return 0 } 739 if child_cls < 0 { return 0 } 740 if g.n_par >= g.cap_par { g.par_overflow = 1; return 0 - NX_EQSAT_OVERFLOW } 741 g.par_node[g.n_par] = nidx 742 g.par_cls[g.n_par] = child_cls 743 g.n_par = g.n_par + 1 744 return NX_EQSAT_OK 745} 746 747// Push a dirty canonical class onto the rebuild worklist (dedup is unnecessary -- 748// rebuild re-canonicalizes + the union strictly reduces class count, so it 749// converges regardless). No-op when rebuild is OFF or the worklist is full 750// (rebuild loops to fixpoint anyway because every union re-pushes its winner). 751func nx_eqsat_push_dirty(g: *NxEGraph, cls: i64) -> i64 { 752 if g.rebuild_on != 1 { return 0 } 753 if (g.worklist as i64) == 0 { return 0 } 754 if g.n_work >= g.cap_work { return 0 } 755 g.worklist[g.n_work] = cls 756 g.n_work = g.n_work + 1 757 return NX_EQSAT_OK 758} 759 760// Allocate a fresh e-class with one initial node. 761func nx_eqsat_new_class(g: *NxEGraph, node_idx: i64, initial_cost: i64) -> i64 { 762 if g.n_classes >= g.cap_classes { return 0 - NX_EQSAT_OVERFLOW } 763 let id: i64 = g.n_classes 764 g.classes[id].canon = id // points to self until merged 765 g.classes[id].cost = initial_cost 766 g.classes[id].best_node = node_idx 767 // MAKE (leaf): a class is born known-const iff its sole node is a CONST literal; 768 // every other class is born NX_CF_NONE (unknown). ALWAYS written (so the field is 769 // never uninitialized garbage); only READ when cf_on==1, so the cf_on==0 770 // trajectory is byte-identical (this store is dead state on the page-rounded 771 // class array). This is the egg `make(Num(n)) = Some(n)` base case. 772 if g.nodes[node_idx].op == NX_EQ_OP_CONST { 773 g.classes[id].cf_val = g.nodes[node_idx].payload 774 } else { 775 g.classes[id].cf_val = NX_CF_NONE 776 } 777 g.n_classes = id + 1 778 g.nodes[node_idx].eclass = id 779 return id 780} 781 782// ===== Union-find: find canonical e-class id ================================================= 783func nx_eqsat_find(g: *NxEGraph, id: i64) -> i64 { 784 var cur: i64 = id 785 while g.classes[cur].canon != cur { 786 cur = g.classes[cur].canon 787 } 788 // Path-compress (single-step; full compression is O(alpha) -- ok for V1) 789 g.classes[id].canon = cur 790 return cur 791} 792 793// Merge two e-classes, CITING the rule that justifies the merge. Cheaper class 794// wins; the more-expensive one repoints to the cheaper. This is the SINGLE 795// chokepoint that mutates canon, so logging the rule-id HERE (only on a real 796// merge, ra!=rb) makes a provenance bypass structurally impossible: no class can 797// be merged without a rule-id passing through this function. Logging is a no-op 798// when prov is OFF, so existing behavior is byte-identical. 799func nx_eqsat_union_cited(g: *NxEGraph, a: i64, b: i64, rule_id: i64) -> i64 { 800 let ra: i64 = nx_eqsat_find(g, a) 801 let rb: i64 = nx_eqsat_find(g, b) 802 if ra == rb { return ra } 803 nx_eqsat_log_rule(g, rule_id) 804 // JOIN (egg Analysis::merge), read BEFORE the canon re-point so both operands are 805 // still roots. Lattice-meet the two classes' const values; the meet is stored 806 // into the post-merge WINNER below (trap-1: write the const to the survivor that 807 // find() returns, never to a stale role). Gated on cf_on==1 so the cf_on==0 808 // trajectory is byte-identical. CONTRADICTION (two unequal known consts in one 809 // class) => fail-CLOSED SOFT poison (cf_poison=1), NOT sys_exit: a sound graph 810 // never reaches this, and a library must degrade gracefully (Global Rule #14) 811 // rather than crash its host. The meet only RISES (NONE->known, never falls), so 812 // the const propagates along union/congruence edges with no rescan (the genuine 813 // new JOIN capability over the old implicit-best_node passive lattice). 814 var meet: i64 = NX_CF_NONE 815 if g.cf_on == 1 { 816 let va: i64 = g.classes[ra].cf_val 817 let vb: i64 = g.classes[rb].cf_val 818 if va == NX_CF_NONE { meet = vb } 819 else { if vb == NX_CF_NONE { meet = va } 820 else { if va == vb { meet = va } 821 else { g.cf_poison = 1; meet = va } } } // contradiction: soft-poison 822 } 823 if g.classes[ra].cost <= g.classes[rb].cost { 824 g.classes[rb].canon = ra 825 if g.cf_on == 1 { g.classes[ra].cf_val = meet } // store meet into the WINNER (ra) 826 // MEET: a class merged -> its parents may now be congruent. Mark the 827 // surviving (winner) canonical class dirty for the deferred rebuild. 828 // No-op when rebuild is OFF, so the default path is byte-identical. 829 nx_eqsat_push_dirty(g, ra) 830 // INCREMENTAL MATCH (enqueue (b)): a merge changed a child's canonical class, 831 // so parents f(...child...) may now newly match a rule. We do NOT enumerate the 832 // parent index PER UNION here (that is O(n_par) per merge -> quadratic when a 833 // rebuild fires many congruence merges, the measured regression). Instead we set 834 // a single "merge happened" flag (mwl_overflow doubles as the dirty signal) and 835 // nx_eqsat_saturate re-matches the node frontier ONCE per outer iteration -- a 836 // single O(n) sweep, never per-union. No-op when match_on!=1. 837 if g.match_on == 1 { g.mwl_overflow = 1 } 838 return ra 839 } 840 g.classes[ra].canon = rb 841 if g.cf_on == 1 { g.classes[rb].cf_val = meet } // store meet into the WINNER (rb) 842 nx_eqsat_push_dirty(g, rb) 843 if g.match_on == 1 { g.mwl_overflow = 1 } 844 return rb 845} 846 847// Legacy 2-arg union (signature unchanged for all existing callers). Cites 848// NX_EQSAT_RULE_NONE -- which is NOT in any proven-sound set, so a merge made 849// through this back door logs an un-sound sentinel and POISONS any certificate 850// (fail-closed: an unlogged-reason merge can never silently certify). 851func nx_eqsat_union(g: *NxEGraph, a: i64, b: i64) -> i64 { 852 return nx_eqsat_union_cited(g, a, b, NX_EQSAT_RULE_NONE) 853} 854 855// ===== Cost model ================================================= 856// 857// Per-op cost. RV64IM micro-architecture approximate: 858// const/var: 0 859// add/sub/and/or/xor/shl/shr/sar/neg/not: 1 860// mul: 3 861// div/rem: 30 (non-restoring divider average) 862// eq/lt/ltu/select: 1 863// popcnt: 2 (1 if silicon has Zbb) 864// Tunable per silicon-target-generation; refined as silicon-feedback 865// loop (rv64im_min_hot_report.nx) feeds back measured cycle counts. 866 867func nx_eqsat_op_cost(op: i64) -> i64 { 868 if op == NX_EQ_OP_CONST { return 0 } 869 if op == NX_EQ_OP_VAR { return 0 } 870 if op == NX_EQ_OP_MUL { return 3 } 871 if op == NX_EQ_OP_DIV { return 30 } 872 if op == NX_EQ_OP_REM { return 30 } 873 if op == NX_EQ_OP_POPCNT { return 2 } 874 return 1 875} 876 877// Compute the cost of an expression rooted at e-class id by 878// summing op cost + child best-costs. Recursive; bounded by 879// e-graph depth. 880func nx_eqsat_class_cost(g: *NxEGraph, class_id: i64) -> i64 { 881 let canon: i64 = nx_eqsat_find(g, class_id) 882 let node_idx: i64 = g.classes[canon].best_node 883 let op: i64 = g.nodes[node_idx].op 884 let arity: i64 = nx_eqsat_arity_for(op) 885 var cost: i64 = nx_eqsat_op_cost(op) 886 if arity >= 1 { cost = cost + nx_eqsat_class_cost(g, g.nodes[node_idx].kid0) } 887 if arity >= 2 { cost = cost + nx_eqsat_class_cost(g, g.nodes[node_idx].kid1) } 888 if arity >= 3 { cost = cost + nx_eqsat_class_cost(g, g.nodes[node_idx].kid2) } 889 return cost 890} 891 892// ===== Node construction ================================================= 893// 894// Add an e-node + optionally create / find its e-class. V1: linear 895// search for existing node (no hash-cons yet); fine for graphs <1000 896// nodes. Future: per-op hash table for O(1) lookup. 897 898// ===== CONST-FOLD analysis (egg e-class analysis: constant folding) ========= 899// 900// THE LATTICE IS IMPLICIT IN best_node. A class is "CONST V" iff its canonical 901// best_node is a CONST node (op==NX_EQ_OP_CONST, payload==V) -- exact at class 902// creation (nx_eqsat_new_class sets best_node to the just-added node) and never 903// demoted for THIS minimal lattice (CONST cost==0 is strictly cheapest, line 904// "if op == NX_EQ_OP_CONST { return 0 }" in nx_eqsat_op_cost, so recompute_best 905// never moves a const class off its CONST node). So we read the analysis off 906// best_node -- zero new struct fields, zero per-class analysis buffer. 907// 908// Map an eqsat op to the gate-sim cell kind whose semantics are the PROVEN 909// semantics of that op. -1 => fold REFUSED (no faithful cell -> NEVER evaluated). 910// REFUSALS are the soundness boundary, each a confirmed silent-miscompile if mapped: 911// DIV/REM -- gsim has NO div/rem cell (would hit eval_cell's silent `return 0`). 912// SHR -- eqsat SHR is LOGICAL >>; gsim SHR cell is `a >> b` = ARITHMETIC in 913// NishiLang (verified: (0-8)>>1 == -4), so it disagrees for negatives. 914// SAR -- no SAR cell in gsim's eval switch. 915// NEG -- no gate kind; the NEG->NOT temptation is WRONG (NOT(a)=a^-1 != -a). 916// POPCNT -- gsim has no popcount cell. 917// SELECT -- maps to MUX, but SELECT is arity-3 and deferred (kept simple). 918func nx_eqsat_op_to_gate_kind(op: i64) -> i64 { 919 if op == NX_EQ_OP_ADD { return NX_GATE_KIND_ADD } // 2->7 920 if op == NX_EQ_OP_SUB { return NX_GATE_KIND_SUB } // 3->8 921 if op == NX_EQ_OP_MUL { return NX_GATE_KIND_MUL } // 4->9 922 if op == NX_EQ_OP_AND { return NX_GATE_KIND_AND } // 7->0 923 if op == NX_EQ_OP_OR { return NX_GATE_KIND_OR } // 8->1 924 if op == NX_EQ_OP_XOR { return NX_GATE_KIND_XOR } // 9->3 925 if op == NX_EQ_OP_NOT { return NX_GATE_KIND_NOT } // 10->2 926 if op == NX_EQ_OP_SHL { return NX_GATE_KIND_SHL } // 11->11 927 if op == NX_EQ_OP_EQ { return NX_GATE_KIND_EQ } // 15->14 928 if op == NX_EQ_OP_LT { return NX_GATE_KIND_LT } // 16->16 929 if op == NX_EQ_OP_LTU { return NX_GATE_KIND_LTU } // 17->17 930 return 0 - 1 // DIV/REM/SHR/SAR/NEG/POPCNT/SELECT/CONST/VAR -> REFUSED 931} 932 933// Read the const-lattice value of canonical class `cls` into out_v[0]. Returns 1 934// iff `cls` is a known constant (its canonical best_node is a CONST node). A VAR 935// class returns 0 (best_node.op==VAR; its payload is a var id, NEVER read as a 936// value -> "fold on VARs refused" structurally). best_node is re-canonicalized via 937// find first, so a stale (pre-rebuild) link cannot feed a wrong operand. 938func nx_eqsat_class_const(g: *NxEGraph, cls: i64, out_v: *i64) -> i64 { 939 let canon: i64 = nx_eqsat_find(g, cls) 940 let bn: i64 = g.classes[canon].best_node 941 if g.nodes[bn].op != NX_EQ_OP_CONST { return 0 } 942 if g.nodes[bn].n_kids != 0 { return 0 } // a CONST is arity-0 (re-verify shape) 943 out_v[0] = g.nodes[bn].payload 944 return 1 945} 946 947// O(1) const-lattice read via the EXPLICIT cf_val field (the incremental analysis 948// store) -- the fast path used by the add-time MAKE. Returns 1 + writes the const 949// into out_v[0] iff canonical class `cls` is known-const (cf_val != NX_CF_NONE). No 950// node-array walk (unlike nx_eqsat_class_const, which dereferences best_node). Only 951// meaningful when cf_on==1 (cf_val is maintained by MAKE/JOIN); read through find so 952// a merged/interior class self-canonicalizes to the survivor that carries the value 953// (trap-1 defense: never trust a non-canonical id's field). 954func nx_eqsat_class_cf(g: *NxEGraph, cls: i64, out_v: *i64) -> i64 { 955 let canon: i64 = nx_eqsat_find(g, cls) 956 let v: i64 = g.classes[canon].cf_val 957 if v == NX_CF_NONE { return 0 } 958 out_v[0] = v 959 return 1 960} 961 962// Drive const-fold for a NEWLY-created e-node (e-class new_cls, op, canonical kids 963// kc0..kc2). Returns 1 iff a fold fired (a CONST merge was performed), else 0. 964// Steps: (1) refuse CONST/VAR + any op with no faithful gate cell; (2) require 965// EVERY child class be a known constant (else no fire -> the backward-compat 966// guarantee on VAR graphs); (3) guard out-of-range shift amounts; (4) GUARD the 967// evaluator against its silent default (nx_gsim_kind_supported) so an unsupported 968// kind can NEVER fold a wrong 0; (5) evaluate via the PROVEN nx_gsim_eval_cell at 969// W=64 (i64 arithmetic IS mod-2^64 -> raw output is the exact W=64 value); (6) 970// merge new_cls with CONST(folded) through the single cited chokepoint. 971func nx_eqsat_try_constfold(g: *NxEGraph, new_cls: i64, op: i64, 972 kc0: i64, kc1: i64, kc2: i64) -> i64 { 973 if op == NX_EQ_OP_CONST { return 0 } 974 if op == NX_EQ_OP_VAR { return 0 } 975 let kind: i64 = nx_eqsat_op_to_gate_kind(op) 976 if kind < 0 { return 0 } // unmapped op -> REFUSED 977 // Defend the silent-default trap: only fold kinds the evaluator actually 978 // handles (reuse the simulator's own loud guard instead of bypassing it). 979 if nx_gsim_kind_supported(kind) != 1 { return 0 } 980 let arity: i64 = nx_eqsat_arity_for(op) 981 var v0: i64 = 0 982 var v1: i64 = 0 983 var v2: i64 = 0 984 let pv: *i64 = sys_mmap(8) as *i64 985 if arity >= 1 { if nx_eqsat_class_const(g, kc0, pv) != 1 { return 0 } v0 = pv[0] } 986 if arity >= 2 { if nx_eqsat_class_const(g, kc1, pv) != 1 { return 0 } v1 = pv[0] } 987 if arity >= 3 { if nx_eqsat_class_const(g, kc2, pv) != 1 { return 0 } v2 = pv[0] } 988 // shift-amount guard: an out-of-range shift is UB / not what i64 << does 989 // portably -> refuse rather than fold a value the proof never validated. 990 if op == NX_EQ_OP_SHL { if v1 < 0 { return 0 } if v1 >= NX_EQSAT_W { return 0 } } 991 let folded: i64 = nx_gsim_eval_cell(kind, v0, v1, v2) 992 let cst: i64 = nx_eqsat_add_const(g, folded) 993 if cst < 0 { return 0 } // allocation overflow -> no fold 994 nx_eqsat_union_cited(g, new_cls, cst, NX_EQSAT_RULE_CONSTFOLD) 995 return 1 996} 997 998// ===== INCREMENTAL FOLD (the egg MAKE/MODIFY fast path) ===================== 999// 1000// nx_eqsat_fold_value: the MAKE oracle as O(1) FIELD reads. Returns 1 + writes the 1001// folded constant to out_v[0] iff op is foldable (faithful gate cell + evaluator 1002// support, the EXISTING soundness boundary) AND every canonical child class is 1003// known-const via the explicit cf_val lattice (NO best_node node-array walk). This 1004// is the incremental analysis: instead of re-DISCOVERING constness by scanning the 1005// whole node array each saturate iteration (the old O(N*K*M) lapp), the const flows 1006// through cf_val and a fold is a constant-time field-read + one evaluator call. 1007// Refusals (kind<0, unsupported, SHL out-of-range, any non-const child) leave the 1008// node un-folded -- IDENTICAL to nx_eqsat_try_constfold so backward-compat holds. 1009// Writes the folded constant to out_v[0] iff foldable + all children known-const. 1010// Reads child cf_val DIRECTLY off the canonical class field (no scratch pointer, no 1011// node walk) so the hot path makes ZERO sys_mmap calls. NX_CF_NONE is the "unknown" 1012// sentinel; a child carrying it (a VAR-touching class) refuses the fold. 1013func nx_eqsat_fold_value(g: *NxEGraph, op: i64, kc0: i64, kc1: i64, kc2: i64, out_v: *i64) -> i64 { 1014 if op == NX_EQ_OP_CONST { return 0 } 1015 if op == NX_EQ_OP_VAR { return 0 } 1016 let kind: i64 = nx_eqsat_op_to_gate_kind(op) 1017 if kind < 0 { return 0 } 1018 if nx_gsim_kind_supported(kind) != 1 { return 0 } 1019 let arity: i64 = nx_eqsat_arity_for(op) 1020 var v0: i64 = 0 1021 var v1: i64 = 0 1022 var v2: i64 = 0 1023 if arity >= 1 { let c0: i64 = nx_eqsat_find(g, kc0); let x0: i64 = g.classes[c0].cf_val; if x0 == NX_CF_NONE { return 0 } v0 = x0 } 1024 if arity >= 2 { let c1: i64 = nx_eqsat_find(g, kc1); let x1: i64 = g.classes[c1].cf_val; if x1 == NX_CF_NONE { return 0 } v1 = x1 } 1025 if arity >= 3 { let c2: i64 = nx_eqsat_find(g, kc2); let x2: i64 = g.classes[c2].cf_val; if x2 == NX_CF_NONE { return 0 } v2 = x2 } 1026 if op == NX_EQ_OP_SHL { if v1 < 0 { return 0 } if v1 >= NX_EQSAT_W { return 0 } } 1027 out_v[0] = nx_gsim_eval_cell(kind, v0, v1, v2) 1028 return 1 1029} 1030 1031func nx_eqsat_add(g: *NxEGraph, op: i64, k0: i64, k1: i64, k2: i64, payload: i64) -> i64 { 1032 if nx_eqsat_op_is_valid(op) != 1 { return 0 - NX_EQSAT_BAD_OP } 1033 let arity: i64 = nx_eqsat_arity_for(op) 1034 // Check children for arity. 1035 if arity == 0 { if k0 != 0 - 1 { return 0 - NX_EQSAT_BAD_ARITY } } 1036 if arity == 1 { if k0 < 0 { return 0 - NX_EQSAT_BAD_ARITY } } 1037 if arity == 2 { if k0 < 0 { return 0 - NX_EQSAT_BAD_ARITY } } 1038 if arity == 3 { if k0 < 0 { return 0 - NX_EQSAT_BAD_ARITY } } 1039 1040 // CONST FAST PATH: when const-fold is armed (cf_on + cache, default linear-scan 1041 // store hc==0), the value->class cache IS the const hashcons -- an O(1) intern 1042 // replaces the O(n) linear node scan for EVERY const add (leaf + folded). This 1043 // removes the last O(n^2) term in an all-const build (the leaf consts the caller 1044 // adds directly). Discipline: enable_constfold is called before any const is 1045 // added (both gated callers do), so the cache sees every const from graph birth 1046 // -> hashcons-equivalent. A pre-enable/post-enable value mix would at worst make 1047 // a duplicate CONST node (same value, congruent, same folded value) -- harmless 1048 // (no soundness loss). cf_on==0 OR cache OFF OR meet-on(hc!=0) => skip => the 1049 // original linear-scan path runs => byte-identical for every existing caller. 1050 if op == NX_EQ_OP_CONST { if g.cf_on == 1 { if (g.cf_cache as i64) != 0 { if (g.hc as i64) == 0 { 1051 return nx_cf_intern_const(g, payload) 1052 } } } } 1053 1054 // Canonical children (shared by BOTH the linear-scan and hashcons paths). 1055 let kc0: i64 = if k0 >= 0 then nx_eqsat_find(g, k0) else 0 - 1 1056 let kc1: i64 = if k1 >= 0 then nx_eqsat_find(g, k1) else 0 - 1 1057 let kc2: i64 = if k2 >= 0 then nx_eqsat_find(g, k2) else 0 - 1 1058 1059 // ===== EARLY-FOLD FAST PATH (incremental MAKE + MODIFY) ================== 1060 // When const-fold is ON (and we are on the default linear-scan store, hc==0 -- 1061 // the MEET hashcons path keeps its own existing try_constfold hook below so that 1062 // organ is untouched), and EVERY canonical child is known-const via the O(1) 1063 // cf_val lattice, the result is a known constant. The OLD path would (a) linear- 1064 // SCAN the whole node array to hashcons the binop node, then (b) linear-SCAN 1065 // AGAIN inside add_const to hashcons the folded CONST -- two O(n) scans per node 1066 // = the measured ~10x build-phase lapp. Here we INTERN the folded const in O(1) 1067 // (the value cache = egg's interned Num) and create the binop node WITHOUT the 1068 // O(n) scan, because a foldable all-const binop ALWAYS collapses into the const 1069 // class anyway: even if a structurally-identical binop node already exists, both 1070 // denote the SAME value and merging the fresh one is idempotent/harmless (no 1071 // soundness loss -- congruence would have merged them too). The CONSTFOLD merge 1072 // still flows the single cited chokepoint => logged + membership-certifiable, 1073 // and the returned class find()s to the const (cost-0 winner) => extraction + 1074 // the cert test (find(top)==find(const), log has CONSTFOLD, best_node==CONST) 1075 // are byte-identical to the old eager path. This is the egg make-on-add + 1076 // modify-materialize collapsed to O(1) amortized -- the lapp-closing lever. 1077 if g.cf_on == 1 { if (g.hc as i64) == 0 { if (g.cf_scratch as i64) != 0 { 1078 let fv: *i64 = g.cf_scratch // graph-lifetime scratch -> NO per-node mmap 1079 if nx_eqsat_fold_value(g, op, kc0, kc1, kc2, fv) == 1 { 1080 // intern the folded const in O(1) (no node scan) 1081 let cst_f: i64 = nx_cf_intern_const(g, fv[0]) 1082 if cst_f >= 0 { 1083 // MODIFY-PRUNE (egg's `modify` retains only leaf nodes): when no one 1084 // is RECORDING the rewrite path (provenance OFF), there is no 1085 // observable difference between "create the binop node, fold-merge it 1086 // to the const, return the binop class" and "return the const class 1087 // directly" -- both yield a class that find()s to the SAME interned 1088 // CONST with the SAME extracted value. So we PRUNE the dominated binop 1089 // node + its union entirely (egg drops the non-leaf nodes too), which 1090 // is the lapp-closing lever: the all-const chain collapses to ~N leaf 1091 // CONSTs (no lingering binop nodes for recompute_best to rescan). This 1092 // is a pure speed prune, never a soundness change (the folded value is 1093 // identical, computed by the SAME proven oracle). 1094 if (g.prov as i64) == 0 { 1095 return cst_f 1096 } 1097 // CERTIFICATION PATH (provenance ON): keep the full cited MODIFY so the 1098 // CONSTFOLD merge is LOGGED + membership-certifiable. Allocate the binop 1099 // node WITHOUT the linear scan (it collapses into the const anyway: even 1100 // if a structurally-identical binop exists, both denote the same value 1101 // and merging the fresh one is idempotent/harmless -- congruence would 1102 // merge them too). The merge flows the single cited chokepoint and the 1103 // returned class find()s to the const (cost-0 winner) => the cert test 1104 // (find(top)==find(const), log has CONSTFOLD, best_node==CONST) holds. 1105 if g.n_nodes >= g.cap_nodes { return 0 - NX_EQSAT_OVERFLOW } 1106 let nf: i64 = g.n_nodes 1107 g.nodes[nf].op = op 1108 g.nodes[nf].n_kids = arity 1109 g.nodes[nf].kid0 = kc0 1110 g.nodes[nf].kid1 = kc1 1111 g.nodes[nf].kid2 = kc2 1112 g.nodes[nf].payload = payload 1113 g.n_nodes = nf + 1 1114 let icf: i64 = nx_eqsat_op_cost(op) 1115 let bcls: i64 = nx_eqsat_new_class(g, nf, icf) 1116 if bcls < 0 { return bcls } 1117 // MODIFY: materialize the equality through the cited chokepoint ONCE 1118 // (logged + certifiable). JOIN inside flows cf_val into the winner. 1119 nx_eqsat_union_cited(g, bcls, cst_f, NX_EQSAT_RULE_CONSTFOLD) 1120 return bcls 1121 } 1122 } 1123 } } } 1124 1125 // PATH A (MEET, hc != null): O(1)-avg hashcons lookup. The hashmap value is a 1126 // node-array INDEX; on a hit we re-VERIFY against the node array (a 64-bit 1127 // collision can never return a wrong class -> it degrades to allocate). The 1128 // returned id is the SAME canonical e-class id the linear scan would return. 1129 if (g.hc as i64) != 0 { 1130 let fp: i64 = nx_eqsat_fingerprint(op, payload, kc0, kc1, kc2) 1131 if nx_hmap_has(g.hc, fp) == 1 { 1132 let hit_idx: i64 = nx_hmap_get(g.hc, fp) 1133 if nx_eqsat_node_matches(g, hit_idx, op, payload, kc0, kc1, kc2) == 1 { 1134 return nx_eqsat_find(g, g.nodes[hit_idx].eclass) 1135 } 1136 // collision / stale key: fall through to allocate (never trust the hit). 1137 } 1138 if g.n_nodes >= g.cap_nodes { return 0 - NX_EQSAT_OVERFLOW } 1139 let nidx2: i64 = g.n_nodes 1140 g.nodes[nidx2].op = op 1141 g.nodes[nidx2].n_kids = arity 1142 g.nodes[nidx2].kid0 = kc0 1143 g.nodes[nidx2].kid1 = kc1 1144 g.nodes[nidx2].kid2 = kc2 1145 g.nodes[nidx2].payload = payload 1146 g.n_nodes = nidx2 + 1 1147 nx_hmap_put(g.hc, fp, nidx2) // intern (restore the hashcons invariant) 1148 // parent back-index: this node references each canonical child class. 1149 if arity >= 1 { nx_eqsat_add_parent(g, nidx2, kc0) } 1150 if arity >= 2 { nx_eqsat_add_parent(g, nidx2, kc1) } 1151 if arity >= 3 { nx_eqsat_add_parent(g, nidx2, kc2) } 1152 let ic2: i64 = nx_eqsat_op_cost(op) 1153 let newcls2: i64 = nx_eqsat_new_class(g, nidx2, ic2) 1154 // CONST-FOLD hook (opt-in; no-op + byte-identical when cf_on==0). Fires once 1155 // per DISTINCT node (hashcons-HIT path above returns before here). The folded 1156 // merge flows nx_eqsat_union_cited so it is logged + certifiable. We return 1157 // newcls2 (the new node's class), which the union may repoint to the const's 1158 // canonical class -- callers re-canonicalize via find, so this is correct. 1159 if g.cf_on == 1 { if newcls2 >= 0 { nx_eqsat_try_constfold(g, newcls2, op, kc0, kc1, kc2) } } 1160 return newcls2 1161 } 1162 1163 // PATH B (default, byte-identical): hash-cons by linear scan. Two nodes are 1164 // equal iff op + payload + canonical children agree. 1165 var i: i64 = 0 1166 while i < g.n_nodes { 1167 if g.nodes[i].op == op { 1168 if g.nodes[i].payload == payload { 1169 let n_arity: i64 = g.nodes[i].n_kids 1170 if n_arity == arity { 1171 var matched: i64 = 1 1172 if arity >= 1 { if nx_eqsat_find(g, g.nodes[i].kid0) != kc0 { matched = 0 } } 1173 if arity >= 2 { if nx_eqsat_find(g, g.nodes[i].kid1) != kc1 { matched = 0 } } 1174 if arity >= 3 { if nx_eqsat_find(g, g.nodes[i].kid2) != kc2 { matched = 0 } } 1175 if matched == 1 { 1176 return g.nodes[i].eclass 1177 } 1178 } 1179 } 1180 } 1181 i = i + 1 1182 } 1183 // Allocate a new node. 1184 if g.n_nodes >= g.cap_nodes { return 0 - NX_EQSAT_OVERFLOW } 1185 let nidx: i64 = g.n_nodes 1186 g.nodes[nidx].op = op 1187 g.nodes[nidx].n_kids = arity 1188 g.nodes[nidx].kid0 = kc0 1189 g.nodes[nidx].kid1 = kc1 1190 g.nodes[nidx].kid2 = kc2 1191 g.nodes[nidx].payload = payload 1192 g.n_nodes = nidx + 1 1193 // Allocate the e-class with initial cost from this single node. 1194 let init_cost: i64 = nx_eqsat_op_cost(op) 1195 let newcls: i64 = nx_eqsat_new_class(g, nidx, init_cost) 1196 // CONST-FOLD hook (opt-in; no-op + byte-identical when cf_on==0). Fires once per 1197 // DISTINCT node (the linear-scan HIT path above returns before here). Same single 1198 // cited chokepoint => logged + certifiable. 1199 if g.cf_on == 1 { if newcls >= 0 { nx_eqsat_try_constfold(g, newcls, op, kc0, kc1, kc2) } } 1200 return newcls 1201} 1202 1203// Convenience wrappers (omit unused children). 1204func nx_eqsat_add_const(g: *NxEGraph, value: i64) -> i64 { 1205 return nx_eqsat_add(g, NX_EQ_OP_CONST, 0 - 1, 0 - 1, 0 - 1, value) 1206} 1207func nx_eqsat_add_var(g: *NxEGraph, var_id: i64) -> i64 { 1208 return nx_eqsat_add(g, NX_EQ_OP_VAR, 0 - 1, 0 - 1, 0 - 1, var_id) 1209} 1210func nx_eqsat_add_binary(g: *NxEGraph, op: i64, a: i64, b: i64) -> i64 { 1211 return nx_eqsat_add(g, op, a, b, 0 - 1, 0) 1212} 1213func nx_eqsat_add_unary(g: *NxEGraph, op: i64, a: i64) -> i64 { 1214 return nx_eqsat_add(g, op, a, 0 - 1, 0 - 1, 0) 1215} 1216 1217// ===== Baseline rewrite rules ================================================= 1218// 1219// V1 ships ~10 canonical algebraic identities for RV64IM. Each is 1220// a hand-coded "if you see pattern X, union it with class Y". Real 1221// egg-style rule DSL is a future commit (parses rules from a text 1222// format); V1 keeps it inline for clarity. 1223 1224func nx_eqsat_apply_rule_add_zero(g: *NxEGraph) -> i64 { 1225 // (add x 0) == x 1226 var unions: i64 = 0 1227 var i: i64 = 0 1228 while i < g.n_nodes { 1229 if g.nodes[i].op == NX_EQ_OP_ADD { 1230 let k0: i64 = nx_eqsat_find(g, g.nodes[i].kid0) 1231 let k1: i64 = nx_eqsat_find(g, g.nodes[i].kid1) 1232 let k0_node: i64 = g.classes[k0].best_node 1233 let k1_node: i64 = g.classes[k1].best_node 1234 if g.nodes[k0_node].op == NX_EQ_OP_CONST { 1235 if g.nodes[k0_node].payload == 0 { 1236 nx_eqsat_union_cited(g, g.nodes[i].eclass, k1, NX_EQSAT_RULE_ADD_ZERO) 1237 unions = unions + 1 1238 } 1239 } 1240 if g.nodes[k1_node].op == NX_EQ_OP_CONST { 1241 if g.nodes[k1_node].payload == 0 { 1242 nx_eqsat_union_cited(g, g.nodes[i].eclass, k0, NX_EQSAT_RULE_ADD_ZERO) 1243 unions = unions + 1 1244 } 1245 } 1246 } 1247 i = i + 1 1248 } 1249 return unions 1250} 1251 1252func nx_eqsat_apply_rule_sub_self(g: *NxEGraph) -> i64 { 1253 // (sub x x) == 0 1254 var unions: i64 = 0 1255 var i: i64 = 0 1256 while i < g.n_nodes { 1257 if g.nodes[i].op == NX_EQ_OP_SUB { 1258 let k0: i64 = nx_eqsat_find(g, g.nodes[i].kid0) 1259 let k1: i64 = nx_eqsat_find(g, g.nodes[i].kid1) 1260 if k0 == k1 { 1261 let zero_class: i64 = nx_eqsat_add_const(g, 0) 1262 nx_eqsat_union_cited(g, g.nodes[i].eclass, zero_class, NX_EQSAT_RULE_SUB_SELF) 1263 unions = unions + 1 1264 } 1265 } 1266 i = i + 1 1267 } 1268 return unions 1269} 1270 1271func nx_eqsat_apply_rule_add_self(g: *NxEGraph) -> i64 { 1272 // (add x x) == (shl x 1) -- strength reduction 1273 var unions: i64 = 0 1274 var i: i64 = 0 1275 while i < g.n_nodes { 1276 if g.nodes[i].op == NX_EQ_OP_ADD { 1277 let k0: i64 = nx_eqsat_find(g, g.nodes[i].kid0) 1278 let k1: i64 = nx_eqsat_find(g, g.nodes[i].kid1) 1279 if k0 == k1 { 1280 let one: i64 = nx_eqsat_add_const(g, 1) 1281 let shifted: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_SHL, k0, one) 1282 nx_eqsat_union_cited(g, g.nodes[i].eclass, shifted, NX_EQSAT_RULE_ADD_SELF) 1283 unions = unions + 1 1284 } 1285 } 1286 i = i + 1 1287 } 1288 return unions 1289} 1290 1291func nx_eqsat_apply_rule_and_self(g: *NxEGraph) -> i64 { 1292 // (and x x) == x -- idempotence 1293 var unions: i64 = 0 1294 var i: i64 = 0 1295 while i < g.n_nodes { 1296 if g.nodes[i].op == NX_EQ_OP_AND { 1297 let k0: i64 = nx_eqsat_find(g, g.nodes[i].kid0) 1298 let k1: i64 = nx_eqsat_find(g, g.nodes[i].kid1) 1299 if k0 == k1 { 1300 nx_eqsat_union_cited(g, g.nodes[i].eclass, k0, NX_EQSAT_RULE_AND_SELF) 1301 unions = unions + 1 1302 } 1303 } 1304 i = i + 1 1305 } 1306 return unions 1307} 1308 1309func nx_eqsat_apply_rule_or_zero(g: *NxEGraph) -> i64 { 1310 // (or x 0) == x 1311 var unions: i64 = 0 1312 var i: i64 = 0 1313 while i < g.n_nodes { 1314 if g.nodes[i].op == NX_EQ_OP_OR { 1315 let k0: i64 = nx_eqsat_find(g, g.nodes[i].kid0) 1316 let k1: i64 = nx_eqsat_find(g, g.nodes[i].kid1) 1317 let k0_node: i64 = g.classes[k0].best_node 1318 let k1_node: i64 = g.classes[k1].best_node 1319 if g.nodes[k0_node].op == NX_EQ_OP_CONST { 1320 if g.nodes[k0_node].payload == 0 { 1321 nx_eqsat_union_cited(g, g.nodes[i].eclass, k1, NX_EQSAT_RULE_OR_ZERO) 1322 unions = unions + 1 1323 } 1324 } 1325 if g.nodes[k1_node].op == NX_EQ_OP_CONST { 1326 if g.nodes[k1_node].payload == 0 { 1327 nx_eqsat_union_cited(g, g.nodes[i].eclass, k0, NX_EQSAT_RULE_OR_ZERO) 1328 unions = unions + 1 1329 } 1330 } 1331 } 1332 i = i + 1 1333 } 1334 return unions 1335} 1336 1337func nx_eqsat_apply_rule_mul_one(g: *NxEGraph) -> i64 { 1338 // (mul x 1) == x 1339 var unions: i64 = 0 1340 var i: i64 = 0 1341 while i < g.n_nodes { 1342 if g.nodes[i].op == NX_EQ_OP_MUL { 1343 let k0: i64 = nx_eqsat_find(g, g.nodes[i].kid0) 1344 let k1: i64 = nx_eqsat_find(g, g.nodes[i].kid1) 1345 let k1_node: i64 = g.classes[k1].best_node 1346 if g.nodes[k1_node].op == NX_EQ_OP_CONST { 1347 if g.nodes[k1_node].payload == 1 { 1348 nx_eqsat_union_cited(g, g.nodes[i].eclass, k0, NX_EQSAT_RULE_MUL_ONE) 1349 unions = unions + 1 1350 } 1351 } 1352 } 1353 i = i + 1 1354 } 1355 return unions 1356} 1357 1358// Operating width: (mul x 2^k)==(shl x k) is sound only for k in [0, W). At k>=W, 1359// 2^k mod 2^W == 0 so x*2^k collapses to 0 while x<<k is out of range -- proven 1360// UNSOUND by nx_rule_soundness (k>=W 2048/2048). The rule refuses to fire there. 1361const NX_EQSAT_W: i64 = 64 1362 1363func nx_eqsat_apply_rule_mul_pow2(g: *NxEGraph) -> i64 { 1364 // (mul x 2^k) == (shl x k) for 1<=k<W -- strength reduction (cost 3 -> 1). 1365 // Counts only REAL merges (idempotent re-application), so the saturation 1366 // loop can actually converge to NX_EQSAT_SATURATED -- the V1 rules count 1367 // every attempt, so they never report saturation; this one does it right. 1368 var unions: i64 = 0 1369 var i: i64 = 0 1370 while i < g.n_nodes { 1371 if g.nodes[i].op == NX_EQ_OP_MUL { 1372 let ka: i64 = nx_eqsat_find(g, g.nodes[i].kid0) 1373 let kb: i64 = nx_eqsat_find(g, g.nodes[i].kid1) 1374 let ka_node: i64 = g.classes[ka].best_node 1375 let kb_node: i64 = g.classes[kb].best_node 1376 var base: i64 = 0 - 1 1377 var cval: i64 = 0 1378 // const on the right (x * C); then const on the left (C * x) 1379 if g.nodes[kb_node].op == NX_EQ_OP_CONST { base = ka; cval = g.nodes[kb_node].payload } 1380 if g.nodes[ka_node].op == NX_EQ_OP_CONST { base = kb; cval = g.nodes[ka_node].payload } 1381 if base >= 0 { 1382 if cval > 1 { 1383 // power-of-two test + log2 by repeated halving (no bit-ops needed) 1384 var k: i64 = 0 1385 var t: i64 = cval 1386 var is_pow2: i64 = 1 1387 while t > 1 { 1388 if (t % 2) != 0 { is_pow2 = 0 } 1389 t = t / 2 1390 k = k + 1 1391 } 1392 // k<W GUARD: refuse the union where the identity is unsound. 1393 if is_pow2 == 1 { if k < NX_EQSAT_W { 1394 let kconst: i64 = nx_eqsat_add_const(g, k) 1395 let shifted: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_SHL, base, kconst) 1396 if nx_eqsat_find(g, g.nodes[i].eclass) != nx_eqsat_find(g, shifted) { 1397 nx_eqsat_union_cited(g, g.nodes[i].eclass, shifted, NX_EQSAT_RULE_MUL_POW2) 1398 unions = unions + 1 1399 } 1400 } } 1401 } 1402 } 1403 } 1404 i = i + 1 1405 } 1406 return unions 1407} 1408 1409// ===== PER-NODE INLINE MATCHER (the incremental-match entry) ================= 1410// 1411// nx_eqsat_match_node_inline applies the SAME 7 inline rule bodies as the full-scan 1412// appliers above, but to a SINGLE node `nidx` (dispatched on its op), in the SAME 1413// FIXED ORDER the full-scan visits them per node within one saturate pass (add_zero 1414// -> sub_self -> add_self -> and_self -> or_zero -> mul_one -> mul_pow2). Each rule 1415// body is COPIED VERBATIM from its applier's loop body (same find/best_node reads, 1416// same union_cited cites, same CNT_EVERY vs CNT_REAL_MERGE counting), so a node that 1417// the full-scan would fire on fires here identically. Returns the union count for 1418// this node (summed across all applicable rules). This is the incremental analogue 1419// of one full-scan iteration restricted to the changed/new nodes. 1420func nx_eqsat_match_node_inline(g: *NxEGraph, nidx: i64) -> i64 { 1421 var unions: i64 = 0 1422 let op: i64 = g.nodes[nidx].op 1423 // ---- add_zero + add_self (op == ADD) ---- 1424 if op == NX_EQ_OP_ADD { 1425 let k0: i64 = nx_eqsat_find(g, g.nodes[nidx].kid0) 1426 let k1: i64 = nx_eqsat_find(g, g.nodes[nidx].kid1) 1427 // add_zero: (add x 0) == x (dual order, count every) 1428 let k0_node: i64 = g.classes[k0].best_node 1429 let k1_node: i64 = g.classes[k1].best_node 1430 if g.nodes[k0_node].op == NX_EQ_OP_CONST { 1431 if g.nodes[k0_node].payload == 0 { 1432 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, k1, NX_EQSAT_RULE_ADD_ZERO) 1433 unions = unions + 1 1434 } 1435 } 1436 if g.nodes[k1_node].op == NX_EQ_OP_CONST { 1437 if g.nodes[k1_node].payload == 0 { 1438 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, k0, NX_EQSAT_RULE_ADD_ZERO) 1439 unions = unions + 1 1440 } 1441 } 1442 // add_self: (add x x) == (shl x 1) (re-read finds: a prior union above may 1443 // have repointed the class, exactly as the full-scan re-finds per applier) 1444 let a0: i64 = nx_eqsat_find(g, g.nodes[nidx].kid0) 1445 let a1: i64 = nx_eqsat_find(g, g.nodes[nidx].kid1) 1446 if a0 == a1 { 1447 let one: i64 = nx_eqsat_add_const(g, 1) 1448 let shifted: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_SHL, a0, one) 1449 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, shifted, NX_EQSAT_RULE_ADD_SELF) 1450 unions = unions + 1 1451 } 1452 } 1453 // ---- sub_self (op == SUB) ---- 1454 if op == NX_EQ_OP_SUB { 1455 let k0: i64 = nx_eqsat_find(g, g.nodes[nidx].kid0) 1456 let k1: i64 = nx_eqsat_find(g, g.nodes[nidx].kid1) 1457 if k0 == k1 { 1458 let zero_class: i64 = nx_eqsat_add_const(g, 0) 1459 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, zero_class, NX_EQSAT_RULE_SUB_SELF) 1460 unions = unions + 1 1461 } 1462 } 1463 // ---- and_self (op == AND) ---- 1464 if op == NX_EQ_OP_AND { 1465 let k0: i64 = nx_eqsat_find(g, g.nodes[nidx].kid0) 1466 let k1: i64 = nx_eqsat_find(g, g.nodes[nidx].kid1) 1467 if k0 == k1 { 1468 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, k0, NX_EQSAT_RULE_AND_SELF) 1469 unions = unions + 1 1470 } 1471 } 1472 // ---- or_zero (op == OR) ---- 1473 if op == NX_EQ_OP_OR { 1474 let k0: i64 = nx_eqsat_find(g, g.nodes[nidx].kid0) 1475 let k1: i64 = nx_eqsat_find(g, g.nodes[nidx].kid1) 1476 let k0_node: i64 = g.classes[k0].best_node 1477 let k1_node: i64 = g.classes[k1].best_node 1478 if g.nodes[k0_node].op == NX_EQ_OP_CONST { 1479 if g.nodes[k0_node].payload == 0 { 1480 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, k1, NX_EQSAT_RULE_OR_ZERO) 1481 unions = unions + 1 1482 } 1483 } 1484 if g.nodes[k1_node].op == NX_EQ_OP_CONST { 1485 if g.nodes[k1_node].payload == 0 { 1486 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, k0, NX_EQSAT_RULE_OR_ZERO) 1487 unions = unions + 1 1488 } 1489 } 1490 } 1491 // ---- mul_one + mul_pow2 (op == MUL) ---- 1492 if op == NX_EQ_OP_MUL { 1493 // mul_one: (mul x 1) == x (RIGHT-const only, exactly as the inline applier) 1494 let k0: i64 = nx_eqsat_find(g, g.nodes[nidx].kid0) 1495 let k1: i64 = nx_eqsat_find(g, g.nodes[nidx].kid1) 1496 let k1_node: i64 = g.classes[k1].best_node 1497 if g.nodes[k1_node].op == NX_EQ_OP_CONST { 1498 if g.nodes[k1_node].payload == 1 { 1499 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, k0, NX_EQSAT_RULE_MUL_ONE) 1500 unions = unions + 1 1501 } 1502 } 1503 // mul_pow2: (mul x 2^k) == (shl x k) for 1<=k<W (count REAL merges only) 1504 let ka: i64 = nx_eqsat_find(g, g.nodes[nidx].kid0) 1505 let kb: i64 = nx_eqsat_find(g, g.nodes[nidx].kid1) 1506 let ka_node: i64 = g.classes[ka].best_node 1507 let kb_node: i64 = g.classes[kb].best_node 1508 var base: i64 = 0 - 1 1509 var cval: i64 = 0 1510 if g.nodes[kb_node].op == NX_EQ_OP_CONST { base = ka; cval = g.nodes[kb_node].payload } 1511 if g.nodes[ka_node].op == NX_EQ_OP_CONST { base = kb; cval = g.nodes[ka_node].payload } 1512 if base >= 0 { 1513 if cval > 1 { 1514 var k: i64 = 0 1515 var t: i64 = cval 1516 var is_pow2: i64 = 1 1517 while t > 1 { 1518 if (t % 2) != 0 { is_pow2 = 0 } 1519 t = t / 2 1520 k = k + 1 1521 } 1522 if is_pow2 == 1 { if k < NX_EQSAT_W { 1523 let kconst: i64 = nx_eqsat_add_const(g, k) 1524 let shifted: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_SHL, base, kconst) 1525 if nx_eqsat_find(g, g.nodes[nidx].eclass) != nx_eqsat_find(g, shifted) { 1526 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, shifted, NX_EQSAT_RULE_MUL_POW2) 1527 unions = unions + 1 1528 } 1529 } } 1530 } 1531 } 1532 } 1533 return unions 1534} 1535 1536// ===== GENERAL E-MATCHER (the egg data-driven rewrite path) ================= 1537// 1538// nx_eqsat_apply_dsl_rule applies ONE NxDslRule over the whole e-graph, replacing 1539// all 7 inline rule loops with a single data-interpreted matcher. It is proven 1540// BYTE-IDENTICAL to the inline path by nx_eqsat_dsl_parity_test.nx; the row order 1541// in nx_eqsat_builtin_dsl_table mirrors the inline call order so the merge 1542// sequence (and thus best_node/cost/provenance log) is the same. 1543// 1544// SAFETY (defends the wrong-class-binding trap): every bound variable is a 1545// CANONICAL class id via nx_eqsat_find (never best_node, which can be stale). A 1546// DSL_CONST slot uses best_node ONLY as a read-only value probe (exactly as the 1547// inline rules do, e.g. add_zero lines 553-556). The merge ALWAYS flows through 1548// the single chokepoint nx_eqsat_union_cited (provenance log + worklist-dirty + 1549// the RULE_NONE fail-closed poison are preserved -- no bypass). 1550// 1551// log2-by-repeated-halving helper for the mul_pow2 side-condition: returns the 1552// exponent k if `c` is 2^k with 1<k... else returns -1 (not a usable power-of-two). 1553// Mirrors the inline mul_pow2 loop (lines 879-882) so the guard is the SAME. 1554func nx_eqsat_dsl_log2_pow2(c: i64) -> i64 { 1555 if c <= 1 { return 0 - 1 } 1556 var k: i64 = 0 1557 var t: i64 = c 1558 var is_pow2: i64 = 1 1559 while t > 1 { 1560 if (t % 2) != 0 { is_pow2 = 0 } 1561 t = t / 2 1562 k = k + 1 1563 } 1564 if is_pow2 != 1 { return 0 - 1 } 1565 return k 1566} 1567 1568// Is the class `cls`'s best_node a CONST whose payload == want? (value probe only, 1569// exactly as the inline const-zero/const-one rules test g.classes[k].best_node.) 1570func nx_eqsat_dsl_class_is_const(g: *NxEGraph, cls: i64, want: i64) -> i64 { 1571 let bn: i64 = g.classes[cls].best_node 1572 if g.nodes[bn].op != NX_EQ_OP_CONST { return 0 } 1573 if g.nodes[bn].payload != want { return 0 } 1574 return 1 1575} 1576 1577// Read the const payload of canonical class `cls` into out_v[0] iff its best_node is 1578// a CONST (re-verified shape). Returns 1 on success, 0 otherwise. A CONST class's 1579// best_node is cost-stable (cost 0 is strictly cheapest, never displaced -- the same 1580// lattice invariant nx_eqsat_class_const relies on), so this read is safe to bind a 1581// rule variable from (trap-3 defense: ?i/?j come from CONST classes ONLY). 1582func nx_eqsat_dsl_const_val(g: *NxEGraph, cls: i64, out_v: *i64) -> i64 { 1583 let bn: i64 = g.classes[cls].best_node 1584 if g.nodes[bn].op != NX_EQ_OP_CONST { return 0 } 1585 if g.nodes[bn].n_kids != 0 { return 0 } 1586 out_v[0] = g.nodes[bn].payload 1587 return 1 1588} 1589 1590// ---- shape (d) shift-merge matcher: (shl (shl ?x ?i) ?j) -> (shl ?x (i+j)) ---- 1591// Given an OUTER node `nidx` already known to be op==SHL with canonical children 1592// k0=find(kid0), k1=find(kid1): require k1 to be a CONST (=?j) AND k0's best_node to 1593// be a structural SHL whose own kid1's canonical class is a CONST (=?i) and whose 1594// kid0 binds ?x = find(inner.kid0). Guard i,j>=0 and i+j<W (SC_SHIFT_MERGE_IJW: the 1595// boundary is UNSOUND). On a fire, instantiate (shl ?x (i+j)) and union the outer 1596// class with it citing rule_id, CNT_REAL_MERGE (find!=find) so it converges to 1597// SATURATED. Returns 1 iff a REAL merge happened, else 0. FAIL-CLOSED: any ambiguous 1598// binding (k0 not a SHL, inner kid1 not const, j not const, out-of-range) => no fire. 1599// 1600// trap-3 defense: ?i and ?j are bound from CONST classes ONLY (cost-0, best_node- 1601// stable); ?x is bound as a CANONICAL class id via find. We never read a shift amount 1602// off a non-const class's best_node, so a saturation-displaced best_node cannot feed 1603// a wrong shift amount. The inner SHL node is located via k0.best_node, and its kid1 1604// is re-canonicalized + re-verified CONST before its value is trusted. 1605func nx_eqsat_dsl_shift_merge(g: *NxEGraph, table: *NxDslRule, ri: i64, 1606 eclass: i64, k0: i64, k1: i64) -> i64 { 1607 // ?j: the OUTER shift amount must be a known constant. 1608 let pj: *i64 = sys_mmap(8) as *i64 1609 if nx_eqsat_dsl_const_val(g, k1, pj) != 1 { return 0 } 1610 let j: i64 = pj[0] 1611 // the OUTER's first child must itself be a structural SHL (the nested shape). 1612 let inner_n: i64 = g.classes[k0].best_node 1613 if g.nodes[inner_n].op != NX_EQ_OP_SHL { return 0 } 1614 if g.nodes[inner_n].n_kids != 2 { return 0 } 1615 // ?i: the INNER shift amount (its kid1's canonical class) must be a known const. 1616 let in_kc1: i64 = nx_eqsat_find(g, g.nodes[inner_n].kid1) 1617 let pi: *i64 = sys_mmap(8) as *i64 1618 if nx_eqsat_dsl_const_val(g, in_kc1, pi) != 1 { return 0 } 1619 let i_amt: i64 = pi[0] 1620 // ?x: the INNER's first child, bound as a CANONICAL class id (never a value). 1621 let bx: i64 = nx_eqsat_find(g, g.nodes[inner_n].kid0) 1622 // GUARD (SC_SHIFT_MERGE_IJW): i,j>=0 and i+j<W -- refuse the unsound boundary. 1623 if i_amt < 0 { return 0 } 1624 if j < 0 { return 0 } 1625 let sum: i64 = i_amt + j 1626 if sum >= NX_EQSAT_W { return 0 } 1627 // instantiate (shl ?x (i+j)) and merge (CNT_REAL_MERGE: count only real merges). 1628 let rhs: i64 = nx_eqsat_dsl_instantiate_rhs(g, table, ri, bx, sum) 1629 if nx_eqsat_find(g, eclass) != nx_eqsat_find(g, rhs) { 1630 nx_eqsat_union_cited(g, eclass, rhs, table[ri].rule_id) 1631 return 1 1632 } 1633 return 0 1634} 1635 1636// Instantiate the RHS template of rule `r` given the bound canonical class `bindA` 1637// and (for the mul_pow2 shape) the log2 shift `shamt`. Returns the RHS e-class id 1638// through the existing self-canonicalizing add* wrappers. RHS_BIND_A returns the 1639// bound class verbatim (the (..)==x identities); RHS_CONST adds a const; the SHL 1640// forms add (shl bindA <amt|log2>). No RHS interpreter -- a closed switch. 1641func nx_eqsat_dsl_instantiate_rhs(g: *NxEGraph, table: *NxDslRule, ri: i64, bindA: i64, shamt: i64) -> i64 { 1642 if table[ri].rhs_kind == RHS_BIND_A { return bindA } 1643 if table[ri].rhs_kind == RHS_CONST { return nx_eqsat_add_const(g, table[ri].rhs_val) } 1644 if table[ri].rhs_kind == RHS_SHL_A_BY_CONST { 1645 let kc: i64 = nx_eqsat_add_const(g, table[ri].rhs_val) 1646 return nx_eqsat_add_binary(g, NX_EQ_OP_SHL, bindA, kc) 1647 } 1648 if table[ri].rhs_kind == RHS_SHL_A_BY_LOG2B { 1649 let kc2: i64 = nx_eqsat_add_const(g, shamt) 1650 return nx_eqsat_add_binary(g, NX_EQ_OP_SHL, bindA, kc2) 1651 } 1652 // shift-merge: emit (shl bindA (i+j)) where the COMPUTED sum was handed in as 1653 // `shamt` (the matcher summed the two CONST shift amounts). Same single-SHL 1654 // shape as RHS_SHL_A_BY_LOG2B, just sourced from the i+j computation. 1655 if table[ri].rhs_kind == RHS_SHL_A_BY_IADDED_J { 1656 let kc3: i64 = nx_eqsat_add_const(g, shamt) 1657 return nx_eqsat_add_binary(g, NX_EQ_OP_SHL, bindA, kc3) 1658 } 1659 return 0 - 1 1660} 1661 1662func nx_eqsat_apply_dsl_rule(g: *NxEGraph, table: *NxDslRule, ri: i64) -> i64 { 1663 var unions: i64 = 0 1664 var i: i64 = 0 1665 while i < g.n_nodes { 1666 if g.nodes[i].op == table[ri].lhs_op { 1667 let k0: i64 = nx_eqsat_find(g, g.nodes[i].kid0) 1668 let k1: i64 = nx_eqsat_find(g, g.nodes[i].kid1) 1669 1670 // ---- shape (a) "x OP x": b_kind == DSL_SAME_AS_A ---- 1671 // sub_self / add_self / and_self (CNT_EVERY, byte-identical to inline) and 1672 // xor_self (CNT_REAL_MERGE so it converges to SATURATED -- the new rule's 1673 // (xor x x)==0 is idempotent, like mul_pow2). Single ordering; fire on 1674 // k0==k1. CNT_REAL_MERGE counts ONLY when the union actually merges two 1675 // distinct classes (find!=find), so re-application is a no-op for `total`. 1676 if table[ri].b_kind == DSL_SAME_AS_A { 1677 if k0 == k1 { 1678 let rhs: i64 = nx_eqsat_dsl_instantiate_rhs(g, table, ri, k0, 0) 1679 if table[ri].count_mode == CNT_REAL_MERGE { 1680 if nx_eqsat_find(g, g.nodes[i].eclass) != nx_eqsat_find(g, rhs) { 1681 nx_eqsat_union_cited(g, g.nodes[i].eclass, rhs, table[ri].rule_id) 1682 unions = unions + 1 1683 } 1684 } else { 1685 nx_eqsat_union_cited(g, g.nodes[i].eclass, rhs, table[ri].rule_id) 1686 unions = unions + 1 1687 } 1688 } 1689 } 1690 1691 // ---- shape (b) mul_pow2: SC_POW2_B_KLTW + RHS_SHL_A_BY_LOG2B ---- 1692 // Const on either side (left overrides right, as inline). One union per 1693 // node; guarded by pow2 & k<W; counts ONLY real merges (find!=find). 1694 if table[ri].side_cond == SC_POW2_B_KLTW { 1695 let k0n: i64 = g.classes[k0].best_node 1696 let k1n: i64 = g.classes[k1].best_node 1697 var base: i64 = 0 - 1 1698 var cval: i64 = 0 1699 if g.nodes[k1n].op == NX_EQ_OP_CONST { base = k0; cval = g.nodes[k1n].payload } 1700 if g.nodes[k0n].op == NX_EQ_OP_CONST { base = k1; cval = g.nodes[k0n].payload } 1701 if base >= 0 { 1702 let sh: i64 = nx_eqsat_dsl_log2_pow2(cval) 1703 if sh >= 0 { if sh < NX_EQSAT_W { 1704 let rhsm: i64 = nx_eqsat_dsl_instantiate_rhs(g, table, ri, base, sh) 1705 if nx_eqsat_find(g, g.nodes[i].eclass) != nx_eqsat_find(g, rhsm) { 1706 nx_eqsat_union_cited(g, g.nodes[i].eclass, rhsm, table[ri].rule_id) 1707 unions = unions + 1 1708 } 1709 } } 1710 } 1711 } 1712 1713 // ---- shape (c) const-slot rules: b_kind == DSL_CONST, no SC ---- 1714 // add_zero / or_zero (dual_order=1, fire both orderings) and mul_one 1715 // (dual_order=0, right-const only). The bound var is the OTHER child. 1716 if table[ri].b_kind == DSL_CONST { if table[ri].side_cond == SC_NONE { 1717 // RIGHT-const ordering: test k1 == CONST(b_val), bind A=k0. 1718 if nx_eqsat_dsl_class_is_const(g, k1, table[ri].b_val) == 1 { 1719 let rhsR: i64 = nx_eqsat_dsl_instantiate_rhs(g, table, ri, k0, 0) 1720 nx_eqsat_union_cited(g, g.nodes[i].eclass, rhsR, table[ri].rule_id) 1721 unions = unions + 1 1722 } 1723 // LEFT-const ordering (only when dual_order): test k0 == CONST, bind A=k1. 1724 if table[ri].dual_order == 1 { 1725 if nx_eqsat_dsl_class_is_const(g, k0, table[ri].b_val) == 1 { 1726 let rhsL: i64 = nx_eqsat_dsl_instantiate_rhs(g, table, ri, k1, 0) 1727 nx_eqsat_union_cited(g, g.nodes[i].eclass, rhsL, table[ri].rule_id) 1728 unions = unions + 1 1729 } 1730 } 1731 } } 1732 1733 // ---- shape (d) shift-merge: SC_SHIFT_MERGE_IJW (nested SHL-of-SHL) ---- 1734 // (shl (shl ?x ?i) ?j) -> (shl ?x (i+j)), ?i,?j CONST, i+j<W. The LHS first 1735 // child is itself a structural SHL (distinct from (a)/(b)/(c) leaf shapes); 1736 // a real merge converges to SATURATED (CNT_REAL_MERGE, idempotent). 1737 if table[ri].side_cond == SC_SHIFT_MERGE_IJW { 1738 unions = unions + nx_eqsat_dsl_shift_merge(g, table, ri, g.nodes[i].eclass, k0, k1) 1739 } 1740 } 1741 i = i + 1 1742 } 1743 return unions 1744} 1745 1746// Apply the whole DSL table in row order (the egg "run every rule" pass). Indexes 1747// g.dsl[ri] by struct stride (compiler-computed) -- no magic byte offset. 1748func nx_eqsat_apply_dsl_table(g: *NxEGraph) -> i64 { 1749 var total: i64 = 0 1750 var ri: i64 = 0 1751 while ri < g.n_dsl { 1752 total = total + nx_eqsat_apply_dsl_rule(g, g.dsl, ri) 1753 ri = ri + 1 1754 } 1755 return total 1756} 1757 1758// PER-NODE DSL matcher (incremental-match entry for the data-driven path). Applies 1759// EVERY row of g.dsl to the SINGLE node `nidx`, in row order, with the SAME shape-(a) 1760// /(b)/(c) bodies as nx_eqsat_apply_dsl_rule (copied verbatim, indexed by nidx instead 1761// of the scan cursor `i`). Returns the union count for this node. Defensive: no 1762// current organ combines meet (which arms match_on) with the DSL table, but supporting 1763// both keeps the incremental path complete if they are ever composed. 1764func nx_eqsat_match_node_dsl(g: *NxEGraph, nidx: i64) -> i64 { 1765 var unions: i64 = 0 1766 var ri: i64 = 0 1767 while ri < g.n_dsl { 1768 if g.nodes[nidx].op == g.dsl[ri].lhs_op { 1769 let k0: i64 = nx_eqsat_find(g, g.nodes[nidx].kid0) 1770 let k1: i64 = nx_eqsat_find(g, g.nodes[nidx].kid1) 1771 // shape (a) "x OP x" 1772 if g.dsl[ri].b_kind == DSL_SAME_AS_A { 1773 if k0 == k1 { 1774 let rhs: i64 = nx_eqsat_dsl_instantiate_rhs(g, g.dsl, ri, k0, 0) 1775 if g.dsl[ri].count_mode == CNT_REAL_MERGE { 1776 if nx_eqsat_find(g, g.nodes[nidx].eclass) != nx_eqsat_find(g, rhs) { 1777 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, rhs, g.dsl[ri].rule_id) 1778 unions = unions + 1 1779 } 1780 } else { 1781 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, rhs, g.dsl[ri].rule_id) 1782 unions = unions + 1 1783 } 1784 } 1785 } 1786 // shape (b) mul_pow2 1787 if g.dsl[ri].side_cond == SC_POW2_B_KLTW { 1788 let k0n: i64 = g.classes[k0].best_node 1789 let k1n: i64 = g.classes[k1].best_node 1790 var base: i64 = 0 - 1 1791 var cval: i64 = 0 1792 if g.nodes[k1n].op == NX_EQ_OP_CONST { base = k0; cval = g.nodes[k1n].payload } 1793 if g.nodes[k0n].op == NX_EQ_OP_CONST { base = k1; cval = g.nodes[k0n].payload } 1794 if base >= 0 { 1795 let sh: i64 = nx_eqsat_dsl_log2_pow2(cval) 1796 if sh >= 0 { if sh < NX_EQSAT_W { 1797 let rhsm: i64 = nx_eqsat_dsl_instantiate_rhs(g, g.dsl, ri, base, sh) 1798 if nx_eqsat_find(g, g.nodes[nidx].eclass) != nx_eqsat_find(g, rhsm) { 1799 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, rhsm, g.dsl[ri].rule_id) 1800 unions = unions + 1 1801 } 1802 } } 1803 } 1804 } 1805 // shape (c) const-slot rules 1806 if g.dsl[ri].b_kind == DSL_CONST { if g.dsl[ri].side_cond == SC_NONE { 1807 if nx_eqsat_dsl_class_is_const(g, k1, g.dsl[ri].b_val) == 1 { 1808 let rhsR: i64 = nx_eqsat_dsl_instantiate_rhs(g, g.dsl, ri, k0, 0) 1809 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, rhsR, g.dsl[ri].rule_id) 1810 unions = unions + 1 1811 } 1812 if g.dsl[ri].dual_order == 1 { 1813 if nx_eqsat_dsl_class_is_const(g, k0, g.dsl[ri].b_val) == 1 { 1814 let rhsL: i64 = nx_eqsat_dsl_instantiate_rhs(g, g.dsl, ri, k1, 0) 1815 nx_eqsat_union_cited(g, g.nodes[nidx].eclass, rhsL, g.dsl[ri].rule_id) 1816 unions = unions + 1 1817 } 1818 } 1819 } } 1820 // shape (d) shift-merge (nested SHL-of-SHL); same matcher as the full-scan. 1821 if g.dsl[ri].side_cond == SC_SHIFT_MERGE_IJW { 1822 unions = unions + nx_eqsat_dsl_shift_merge(g, g.dsl, ri, g.nodes[nidx].eclass, k0, k1) 1823 } 1824 } 1825 ri = ri + 1 1826 } 1827 return unions 1828} 1829 1830// Dispatch one node to the active matcher: DSL table when loaded, else the 7 inline 1831// rules. Mirrors nx_eqsat_saturate's full-scan branch so the incremental path fires 1832// exactly the rules the full-scan would. 1833func nx_eqsat_match_node(g: *NxEGraph, nidx: i64) -> i64 { 1834 if (g.dsl as i64) != 0 { return nx_eqsat_match_node_dsl(g, nidx) } 1835 return nx_eqsat_match_node_inline(g, nidx) 1836} 1837 1838// ===== MEET: deferred congruence rebuild (egg's "rebuild") ================== 1839// 1840// Restore the hashcons invariant after a batch of unions and propagate the 1841// congruence closure: re-canonicalize every e-node's children, re-fingerprint it, 1842// and if a DISTINCT node is already interned under that fingerprint then the two 1843// are CONGRUENT (same op, same payload, canonically-equal children) and get merged 1844// -- ALWAYS through nx_eqsat_union_cited citing NX_EQSAT_RULE_CONGRUENCE (never the 1845// 2-arg back door). Each such union re-dirties classes, so we loop to FIXPOINT. 1846// Convergence: every congruence union strictly reduces the live class count 1847// (union-find monotone), so the worklist empties; guard_max bounds it like 1848// nx_eqsat_recompute_best. Returns the number of congruence unions performed. 1849// 1850// Enumeration: this landing scans ALL nodes per drain pass (provably COMPLETE -- 1851// it cannot miss a congruent parent), and the re-canonicalization writes the new 1852// canonical children back into the node + re-interns under the new fingerprint 1853// (deleting the stale key first), so the hashcons never points at a dead 1854// representative. The parent back-index (par_node/par_cls) is maintained for a 1855// future incremental variant; correctness here does not depend on it. 1856func nx_eqsat_rebuild(g: *NxEGraph) -> i64 { 1857 if g.rebuild_on != 1 { return 0 } 1858 if (g.hc as i64) == 0 { return 0 } 1859 var cong_unions: i64 = 0 1860 var guard: i64 = 0 1861 let guard_max: i64 = g.n_nodes + g.n_classes + 8 1862 // Drain to fixpoint: while there is dirt OR a pass produced a new merge. 1863 var more: i64 = 1 1864 while more == 1 { 1865 more = 0 1866 guard = guard + 1 1867 if guard > guard_max { return cong_unions } 1868 g.n_work = 0 // consume the current dirt; new merges re-arm `more` 1869 // One complete pass over the node array: re-canonicalize + re-intern, and 1870 // congruence-merge any two distinct nodes that collapse to one fingerprint. 1871 var n: i64 = 0 1872 while n < g.n_nodes { 1873 let op: i64 = g.nodes[n].op 1874 let arity: i64 = nx_eqsat_arity_for(op) 1875 let payload: i64 = g.nodes[n].payload 1876 // current (possibly stale) canonical children of THIS node 1877 let nk0: i64 = if arity >= 1 then nx_eqsat_find(g, g.nodes[n].kid0) else 0 - 1 1878 let nk1: i64 = if arity >= 2 then nx_eqsat_find(g, g.nodes[n].kid1) else 0 - 1 1879 let nk2: i64 = if arity >= 3 then nx_eqsat_find(g, g.nodes[n].kid2) else 0 - 1 1880 // re-canonicalize the children in place (so future finds are O(1) here) 1881 if arity >= 1 { g.nodes[n].kid0 = nk0 } 1882 if arity >= 2 { g.nodes[n].kid1 = nk1 } 1883 if arity >= 3 { g.nodes[n].kid2 = nk2 } 1884 let fp: i64 = nx_eqsat_fingerprint(op, payload, nk0, nk1, nk2) 1885 if nx_hmap_has(g.hc, fp) == 1 { 1886 let other: i64 = nx_hmap_get(g.hc, fp) 1887 // re-VERIFY identity (collision-proof) AND that `other` is a 1888 // DISTINCT node in a DIFFERENT canonical class than `n`. 1889 if other != n { 1890 if nx_eqsat_node_matches(g, other, op, payload, nk0, nk1, nk2) == 1 { 1891 let cn: i64 = nx_eqsat_find(g, g.nodes[n].eclass) 1892 let co: i64 = nx_eqsat_find(g, g.nodes[other].eclass) 1893 if cn != co { 1894 // CONGRUENT: merge through the cited chokepoint ONLY. 1895 nx_eqsat_union_cited(g, g.nodes[n].eclass, 1896 g.nodes[other].eclass, 1897 NX_EQSAT_RULE_CONGRUENCE) 1898 cong_unions = cong_unions + 1 1899 more = 1 1900 } 1901 } 1902 } 1903 } 1904 // restore/refresh the hashcons invariant: this fingerprint maps to a 1905 // live representative for this canonical shape. Re-key (delete stale 1906 // then put) so dead representatives never accumulate. 1907 nx_hmap_remove(g.hc, fp) 1908 nx_hmap_put(g.hc, fp, n) 1909 n = n + 1 1910 } 1911 // If the union side-effect pushed fresh dirt, drain again. 1912 if g.n_work > 0 { more = 1 } 1913 } 1914 return cong_unions 1915} 1916 1917// ===== Saturation loop ================================================= 1918// 1919// Apply every rule in fixed order; repeat until no rule produces a 1920// new union OR step budget exhausted. V1 is sequential; egg's 1921// concurrent variant ships when ZERO_TO_ADVANCED.md M2 fleshes out. 1922 1923func nx_eqsat_saturate(g: *NxEGraph, max_iters: i64) -> i64 { 1924 // ===== INCREMENTAL PATH (worklist-driven; match_on==1, auto-armed by enable_meet) = 1925 // Removes the per-iteration full node scan while QUIESCENT: each outer iteration 1926 // matches rules ONLY against (a) the rising node frontier [next_node, n_nodes) -- 1927 // which captures EVERY newly-added node (initial build + RHS/fold nodes created 1928 // during firing) with zero per-alloc-site hooks. (b) When a merge changed some 1929 // node's canonical children (union_cited sets mwl_overflow), the NEXT iteration 1930 // re-matches the full node set ONCE -- a single O(n) sweep that is a SUPERSET of 1931 // every changed parent (provably complete, never the O(n_par)-per-union quadratic). 1932 // After matching, the congruence rebuild drains exactly as the full-scan path. 1933 // `total` accumulates the SAME real merges, so the `total==0 => SATURATED` return 1934 // fires at the equivalent fixpoint (same return code). Complete (egg rebuild 1935 // theorem -- a shallow-LHS match becomes newly-possible only on node-add (a) or a 1936 // child re-canonicalization (b), both covered) + bounded (finite unions, union-find 1937 // monotone, guarded by max_iters). The genuine save: a graph that reaches quiescence 1938 // and then only grows by a few RHS nodes re-matches those FEW, not all n every iter. 1939 if g.match_on == 1 { 1940 // next_node = the new-node frontier cursor (enqueue (a)): every node from here 1941 // to n_nodes is freshly added (initial build on the first iteration, or RHS/ 1942 // fold nodes created during firing) and has not yet been matched. 1943 var next_node: i64 = 0 1944 var iter_i: i64 = 0 1945 while iter_i < max_iters { 1946 var total: i64 = 0 1947 // enqueue (b): mwl_overflow is set by union_cited whenever a class merged 1948 // this run -> some node's canonical children changed, so its parents may now 1949 // match a rule. Rather than enumerate the parent index PER union (O(n_par) 1950 // per merge => quadratic, the measured regression), we re-match the FULL node 1951 // set ONCE here (a single O(n) sweep that is a superset of every changed 1952 // parent -- provably complete, mirroring the full-scan's own per-iteration 1953 // node walk). When NO merge is pending we match ONLY the new-node frontier 1954 // (the genuine incremental save). next_node is reset so the re-scan also 1955 // re-covers the frontier. 1956 if g.mwl_overflow == 1 { 1957 g.mwl_overflow = 0 1958 var fn: i64 = 0 1959 while fn < g.n_nodes { total = total + nx_eqsat_match_node(g, fn); fn = fn + 1 } 1960 next_node = g.n_nodes 1961 } else { 1962 while next_node < g.n_nodes { 1963 let nx: i64 = next_node 1964 next_node = next_node + 1 1965 total = total + nx_eqsat_match_node(g, nx) 1966 } 1967 } 1968 // congruence rebuild (unchanged); its unions set mwl_overflow via the 1969 // union (b)-hook so the NEXT iteration re-scans. Counted into total so a 1970 // congruence-only round does not report premature SATURATED. 1971 total = total + nx_eqsat_rebuild(g) 1972 // True fixpoint: nothing matched/merged, no pending (b)-dirt, no new nodes. 1973 if total == 0 { if g.mwl_overflow == 0 { if next_node >= g.n_nodes { 1974 return NX_EQSAT_SATURATED 1975 } } } 1976 iter_i = iter_i + 1 1977 } 1978 return 0 - NX_EQSAT_STEP_BUDGET 1979 } 1980 // ===== FULL-SCAN PATH (verbatim; match_on==0 for every existing caller + the 6 1981 // non-meet certs) -- byte-identical by construction. ============================ 1982 var iter: i64 = 0 1983 while iter < max_iters { 1984 var total: i64 = 0 1985 // DSL path (egg data-driven) when a rule table is loaded; else the verbatim 1986 // 7 inline calls. g.dsl is null for every existing caller + the four gated 1987 // organs => the inline else-branch runs => byte-identical by construction. 1988 if (g.dsl as i64) != 0 { 1989 total = total + nx_eqsat_apply_dsl_table(g) 1990 } else { 1991 total = total + nx_eqsat_apply_rule_add_zero(g) 1992 total = total + nx_eqsat_apply_rule_sub_self(g) 1993 total = total + nx_eqsat_apply_rule_add_self(g) 1994 total = total + nx_eqsat_apply_rule_and_self(g) 1995 total = total + nx_eqsat_apply_rule_or_zero(g) 1996 total = total + nx_eqsat_apply_rule_mul_one(g) 1997 total = total + nx_eqsat_apply_rule_mul_pow2(g) 1998 } 1999 // MEET: after the 7 rules, drain the congruence rebuild to a fixpoint and 2000 // count its unions into `total` so a congruence-only round does NOT report 2001 // premature SATURATED. No-op (returns 0) when rebuild is OFF -> the loop is 2002 // byte-identical for every existing caller + the four gated organs. 2003 total = total + nx_eqsat_rebuild(g) 2004 if total == 0 { return NX_EQSAT_SATURATED } 2005 iter = iter + 1 2006 } 2007 return 0 - NX_EQSAT_STEP_BUDGET 2008} 2009 2010// ===== Extraction ================================================= 2011// 2012// Pick the lowest-cost representative from each e-class. V1 reads 2013// the cached `cost` + `best_node` fields; future variant runs 2014// dataflow over the saturated graph for tighter cost (egg's 2015// "Extractor" pattern). 2016 2017func nx_eqsat_extract_best_node(g: *NxEGraph, class_id: i64) -> i64 { 2018 let canon: i64 = nx_eqsat_find(g, class_id) 2019 return g.classes[canon].best_node 2020} 2021 2022// ===== Real bottom-up extractor (egg "Extractor" pattern) =================== 2023// 2024// V1's best_node/cost are fixed at class-CREATION and never recomputed against 2025// the cost model over the SATURATED graph, so nx_eqsat_extract_best_node can 2026// return a costlier representative -- e.g. it keeps a wasted `(add C 0)` as the 2027// canonical class's best_node instead of extracting the cheaper `C`. This 2028// recomputes each canonical class's best cost = min over its member nodes of 2029// (op_cost + sum of children's best class cost), iterated to a FIXPOINT (costs 2030// only decrease, so it converges). A class reachable only through itself never 2031// resolves below the sentinel, so the acyclic cheaper form always wins. Call 2032// AFTER nx_eqsat_saturate; afterwards nx_eqsat_extract_best_node returns the 2033// truly-cheapest node. (5W1H feedback hook: a future variant logs WHICH node 2034// won each class + WHY -- the cost breakdown -- for the invention loop.) 2035 2036func nx_eqsat_recompute_best(g: *NxEGraph) -> i64 { 2037 let big: i64 = NX_MAGIC_1000000000 2038 var ci: i64 = 0 2039 while ci < g.n_classes { 2040 if g.classes[ci].canon == ci { g.classes[ci].cost = big } 2041 ci = ci + 1 2042 } 2043 var changed: i64 = 1 2044 var guard: i64 = 0 2045 let guard_max: i64 = g.n_nodes + g.n_classes + 8 2046 while changed == 1 { 2047 changed = 0 2048 guard = guard + 1 2049 if guard > guard_max { return 0 - NX_EQSAT_STEP_BUDGET } 2050 var n: i64 = 0 2051 while n < g.n_nodes { 2052 let cls: i64 = nx_eqsat_find(g, g.nodes[n].eclass) 2053 let op: i64 = g.nodes[n].op 2054 let arity: i64 = nx_eqsat_arity_for(op) 2055 var c: i64 = nx_eqsat_op_cost(op) 2056 var ok: i64 = 1 2057 if arity >= 1 { 2058 let cc0: i64 = g.classes[nx_eqsat_find(g, g.nodes[n].kid0)].cost 2059 if cc0 >= big { ok = 0 } 2060 if cc0 < big { c = c + cc0 } 2061 } 2062 if arity >= 2 { 2063 let cc1: i64 = g.classes[nx_eqsat_find(g, g.nodes[n].kid1)].cost 2064 if cc1 >= big { ok = 0 } 2065 if cc1 < big { c = c + cc1 } 2066 } 2067 if arity >= 3 { 2068 let cc2: i64 = g.classes[nx_eqsat_find(g, g.nodes[n].kid2)].cost 2069 if cc2 >= big { ok = 0 } 2070 if cc2 < big { c = c + cc2 } 2071 } 2072 if ok == 1 { 2073 if c < g.classes[cls].cost { 2074 g.classes[cls].cost = c 2075 g.classes[cls].best_node = n 2076 changed = 1 2077 } 2078 } 2079 n = n + 1 2080 } 2081 } 2082 return NX_EQSAT_OK 2083} 2084 2085// Best cost of an e-class after nx_eqsat_recompute_best (canonical lookup). 2086func nx_eqsat_best_cost(g: *NxEGraph, class_id: i64) -> i64 { 2087 let canon: i64 = nx_eqsat_find(g, class_id) 2088 return g.classes[canon].cost 2089} 2090 2091// ===== Program-emitting extractor ========================================== 2092// 2093// nx_eqsat_extract_best_node only returns a node INDEX -- it cannot hand a 2094// backend the actual optimized PROGRAM (the "can't emit a program" gap). This 2095// emits the cost-minimal expression as a flat, topologically-ordered DAG: each 2096// NxEmitNode references its children by their out-array index, children before 2097// parents (post-order), so a code generator can consume it directly. Call 2098// AFTER nx_eqsat_recompute_best. The extraction is acyclic by construction 2099// (the cost-minimal best_node never closes a cycle), so the recursion 2100// terminates; overflow past `cap` returns 0 - NX_EQSAT_OVERFLOW. 2101 2102struct NxEmitNode { 2103 op: i64 2104 payload: i64 2105 c0: i64 // out-array index of child 0; -1 if none 2106 c1: i64 2107 c2: i64 2108} 2109 2110func nx_eqsat_emit(g: *NxEGraph, class_id: i64, out: *NxEmitNode, cap: i64, count: *i64) -> i64 { 2111 let canon: i64 = nx_eqsat_find(g, class_id) 2112 let node_idx: i64 = g.classes[canon].best_node 2113 let op: i64 = g.nodes[node_idx].op 2114 let arity: i64 = nx_eqsat_arity_for(op) 2115 var e0: i64 = 0 - 1 2116 var e1: i64 = 0 - 1 2117 var e2: i64 = 0 - 1 2118 if arity >= 1 { 2119 e0 = nx_eqsat_emit(g, g.nodes[node_idx].kid0, out, cap, count) 2120 if e0 < 0 { return e0 } 2121 } 2122 if arity >= 2 { 2123 e1 = nx_eqsat_emit(g, g.nodes[node_idx].kid1, out, cap, count) 2124 if e1 < 0 { return e1 } 2125 } 2126 if arity >= 3 { 2127 e2 = nx_eqsat_emit(g, g.nodes[node_idx].kid2, out, cap, count) 2128 if e2 < 0 { return e2 } 2129 } 2130 let idx: i64 = count[0] 2131 if idx >= cap { return 0 - NX_EQSAT_OVERFLOW } 2132 out[idx].op = op 2133 out[idx].payload = g.nodes[node_idx].payload 2134 out[idx].c0 = e0 2135 out[idx].c1 = e1 2136 out[idx].c2 = e2 2137 count[0] = idx + 1 2138 return idx 2139}