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