saulshanabrook · oflatt-claude · Jul 15, 2026 · Jul 15, 2026 · Jul 15, 2026 · Jul 15, 2026
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/egglog-experimental/dd/src/dd_native.rs b/egglog-experimental/dd/src/dd_native.rs
diff --git a/egglog-experimental/dd/src/interpret.rs b/egglog-experimental/dd/src/interpret.rs
diff --git a/egglog-experimental/dd/src/lib.rs b/egglog-experimental/dd/src/lib.rs
diff --git a/egglog-experimental/dd/tests/files.rs b/egglog-experimental/dd/tests/files.rs
@@ -66,16 +66,24 @@ const DEBUG_SUBSET: &[&str] = &[
 /// - container rebuild read primitives (registered through egglog's
 ///   `ActionRegistry`; DD has direct container storage but no registry
 ///   execution state for read primitives over its term-encoded mirror):
-///   `container-proofs`, `datatypes`, `nested-container-dirty-propagation`,
-///   `repro-querybug3`.
+///   `container-proofs`, `container-fail`, `datatypes`,
+///   `nested-container-dirty-propagation`, `hardboiled_conv1d_32`.
+/// - `input` from an external CSV whose path is relative to the corpus dir; the
+///   DD harness runs from the `dd` crate root, so the file cannot be found:
+///   `string_quotes`.
 const KNOWN_UNSUPPORTED: &[(&str, &str)] = &[
     ("container-proofs.egg", "requires a backend action registry"),
+    ("container-fail.egg", "requires a backend action registry"),
     ("datatypes.egg", "requires a backend action registry"),
     (
         "nested-container-dirty-propagation.egg",
         "requires a backend action registry",
     ),
-    ("repro-querybug3.egg", "requires a backend action registry"),
+    (
+        "hardboiled_conv1d_32.egg",
+        "requires a backend action registry",
+    ),
+    ("string_quotes.egg", "string_quotes.csv"),
 ];
 
 /// Run `program` on DD and render its outputs with the SAME normalization

diff --git a/egglog-experimental/src/set_cost.rs b/egglog-experimental/src/set_cost.rs
@@ -125,6 +125,7 @@ impl Macro<Vec<Command>> for SetCostDeclarations {
                             term_constructor: None,
                             unextractable: false,
                             identity_vals: None,
+                            cost: None,
                         });
                     }
                 }
@@ -159,6 +160,7 @@ fn generate_cost_table_commands_from_variants(variants: &[Variant]) -> Vec<Comma
                 term_constructor: None,
                 unextractable: false,
                 identity_vals: None,
+                cost: None,
             }
         })
         .collect::<Vec<_>>()

diff --git a/egglog-experimental/tests/eggcc_2mm_proof.rs b/egglog-experimental/tests/eggcc_2mm_proof.rs
@@ -45,8 +45,14 @@ fn eggcc_2mm_bounded_export_uses_container_helpers() {
         );
     }
 
+    // `:no-merge` is unsupported by the term/proof encoding, so the bounded export
+    // rewrites its no-merge functions to `:merge old` to stay proof-supported.
     assert!(
-        non_comment_program.contains(":no-merge"),
-        "bounded eggcc export should preserve native no-merge declarations"
+        non_comment_program.contains(":merge old"),
+        "bounded eggcc export should use `:merge old` for its former no-merge functions"
+    );
+    assert!(
+        !non_comment_program.contains(":no-merge"),
+        "`:no-merge` is unsupported by the encoding; the bounded export must not use it"
     );
 }
diff --git a/egglog-experimental/tests/fixtures/eggcc-2mm-pass1.egg b/egglog-experimental/tests/fixtures/eggcc-2mm-pass1.egg
@@ -2,7 +2,9 @@
 ; egraphs-good/eggcc#796 (https://github.com/egraphs-good/eggcc/pull/796).
 ; The fixture was checked into egraphs-good/egglog-experimental#56
 ; (https://github.com/egraphs-good/egglog-experimental/pull/56). Its original
-; :no-merge declarations are preserved now that proof mode supports them.
+; no-merge declarations are rewritten to `:merge old` here: the term/proof
+; encoding does not support no-merge functions, and these length/succ functions
+; are deterministic so keeping the old value on a (non-occurring) conflict is sound.
 
 ; Prologue
 (datatype Expr)
@@ -93,7 +95,7 @@
 (constructor TLConcat (TypeList TypeList) TypeList :unextractable)
 (rewrite (TLConcat (TNil) r) r :ruleset type-helpers)
 (rewrite (TLConcat (TCons hd tl) r) (TCons hd (TLConcat tl r)) :ruleset type-helpers)
-(function TypeList-length (TypeList) i64 :no-merge)
+(function TypeList-length (TypeList) i64 :merge old)
 (constructor TypeList-ith (TypeList i64) BaseType :unextractable)
 (rule () ((set (TypeList-length (TNil)) 0)) :ruleset type-helpers)
 (rule ((= lst (TCons hd tl)) (= len (TypeList-length tl))) ((set (TypeList-length lst) (+ 1 len))) :ruleset type-helpers)
@@ -218,7 +220,7 @@
 (rule ((TupleT tylist) (PureTypeList tylist)) ((PureType (TupleT tylist))) :ruleset type-analysis)
 (rule ((TNil)) ((PureTypeList (TNil))) :ruleset type-analysis)
 (rule ((TCons hd tl) (PureBaseType hd) (PureTypeList tl)) ((PureTypeList (TCons hd tl))) :ruleset type-analysis)
-(function ListExpr-length (ListExpr) i64 :no-merge)
+(function ListExpr-length (ListExpr) i64 :merge old)
 (constructor ListExpr-ith (ListExpr i64) Expr :unextractable)
 (constructor ListExpr-suffix (ListExpr i64) ListExpr :unextractable)
 (constructor Append (ListExpr Expr) ListExpr :unextractable)
@@ -227,7 +229,7 @@
 (rule ((= (ListExpr-suffix list n) (Nil))) ((set (ListExpr-length list) n)) :ruleset always-run)
 (rewrite (Append (Cons a b) e) (Cons a (Append b e)) :ruleset always-run)
 (rewrite (Append (Nil) e) (Cons e (Nil)) :ruleset always-run)
-(function tuple-length (Expr) i64 :no-merge)
+(function tuple-length (Expr) i64 :merge old)
 (rule ((HasType expr (TupleT tl)) (= len (TypeList-length tl))) ((set (tuple-length expr) len)) :ruleset always-run)
 (relation leading-Expr (Expr))
 (relation leading-Expr-list (ListExpr))
@@ -649,7 +651,7 @@
 (constructor AddIntInterval (IntInterval IntInterval) IntInterval)
 (rewrite (AddIntInterval (MkIntInterval lo1 hi1) (MkIntInterval lo2 hi2)) (MkIntInterval (AddIntOrInfinity lo1 lo2) (AddIntOrInfinity hi1 hi2)) :ruleset always-run)
 (datatype List<i64+IntInterval> (Nil-List<i64+IntInterval>) (Cons-List<i64+IntInterval> i64 IntInterval List<i64+IntInterval>))
-(function Length-List<i64+IntInterval> (List<i64+IntInterval>) i64 :no-merge)
+(function Length-List<i64+IntInterval> (List<i64+IntInterval>) i64 :merge old)
 (rule ((= x (Nil-List<i64+IntInterval>))) ((set (Length-List<i64+IntInterval> x) 0)) :ruleset always-run)
 (rule ((= x (Cons-List<i64+IntInterval> hd0 hd1 tl)) (= l (Length-List<i64+IntInterval> tl))) ((set (Length-List<i64+IntInterval> x) (+ l 1))) :ruleset always-run)
 (rule ((= x (Nil-List<i64+IntInterval>))) ((set (Length-List<i64+IntInterval> x) 0)) :ruleset memory-helpers)
@@ -715,7 +717,7 @@
 (relation PointsNowhere-PtrPointees (PtrPointees))
 (rule ((= f (PointsTo x)) (IsEmpty-List<i64+IntInterval> x)) ((PointsNowhere-PtrPointees f)) :ruleset always-run)
 (datatype List<PtrPointees> (Nil-List<PtrPointees>) (Cons-List<PtrPointees> PtrPointees List<PtrPointees>))
-(function Length-List<PtrPointees> (List<PtrPointees>) i64 :no-merge)
+(function Length-List<PtrPointees> (List<PtrPointees>) i64 :merge old)
 (rule ((= x (Nil-List<PtrPointees>))) ((set (Length-List<PtrPointees> x) 0)) :ruleset always-run)
 (rule ((= x (Cons-List<PtrPointees> hd0 tl)) (= l (Length-List<PtrPointees> tl))) ((set (Length-List<PtrPointees> x) (+ l 1))) :ruleset always-run)
 (rule ((= x (Nil-List<PtrPointees>))) ((set (Length-List<PtrPointees> x) 0)) :ruleset memory-helpers)
@@ -753,7 +755,7 @@
 (rewrite (ExprSet-union (ES set1) (ES set2)) (ES (set-union set1 set2)) :ruleset memory-helpers)
 (constructor ExprSet-insert (ExprSet Expr) ExprSet)
 (rewrite (ExprSet-insert (ES set1) x) (ES (set-insert set1 x)) :ruleset memory-helpers)
-(function ExprSet-length (ExprSet) i64 :no-merge)
+(function ExprSet-length (ExprSet) i64 :merge old)
 (rule ((ES set1)) ((set (ExprSet-length (ES set1)) (set-length set1))) :ruleset memory-helpers)
 (datatype Pointees (TuplePointsTo List<PtrPointees>) (PtrPointsTo PtrPointees))
 (constructor UnwrapPtrPointsTo (Pointees) PtrPointees)
@@ -829,7 +831,7 @@
 (rewrite (PointsToCells (Alloc id sz state ty) aps) (TuplePointsTo (Cons-List<PtrPointees> (PointsTo (Cons-List<i64+IntInterval> id (MkIntInterval (I 0) (I 0)) (Nil-List<i64+IntInterval>))) (Cons-List<PtrPointees> (PointsTo (Nil-List<i64+IntInterval>)) (Nil-List<PtrPointees>)))) :ruleset memory-helpers)
 (constructor PointsToCellsAtIter (Pointees Expr Expr i64) Pointees)
 (rule ((= e (DoWhile inputs pred-body)) (PointsToCells e aps)) ((union (PointsToCellsAtIter aps inputs pred-body 0) (PointsToCells inputs aps)) (union (PointsToCellsAtIter aps inputs pred-body 1) (UnionPointees (PointsToCellsAtIter aps inputs pred-body 0) (PointeesDropFirst (PointsToCells pred-body (PointsToCellsAtIter aps inputs pred-body 0)))))) :ruleset memory-helpers)
-(function succ (i64) i64 :no-merge)
+(function succ (i64) i64 :merge old)
 (rule ((PointsToCellsAtIter aps inputs pred-body i)) ((set (succ i) (+ i 1))) :ruleset memory-helpers)
 (rule ((= pointees0 (PointsToCellsAtIter aps inputs pred-body i)) (= pointees1 (PointsToCellsAtIter aps inputs pred-body (succ i))) (Resolved-Pointees pointees0) (Resolved-Pointees pointees1) (!= pointees0 pointees1)) ((union (PointsToCellsAtIter aps inputs pred-body (+ i 2)) (UnionPointees pointees1 (PointeesDropFirst (PointsToCells pred-body pointees1))))) :ruleset memory)
 (rule ((= pointees (PointsToCellsAtIter aps inputs pred-body i)) (= pointees (PointsToCellsAtIter aps inputs pred-body (succ i)))) ((union (PointsToCells (DoWhile inputs pred-body) aps) pointees)) :ruleset memory)

diff --git a/egglog-experimental/tests/snapshots/files__proofs__with_ruleset_proof_testing.snap b/egglog-experimental/tests/snapshots/files__proofs__with_ruleset_proof_testing.snap
@@ -11,11 +11,8 @@ expression: snapshot
   (premises)
   (substitution))
 (let t0 (Add (Num 2) (Num 3)))
-(let t1 (Add (Num 3) (Num 2)))
-(Sym
-  (= t0 t1)
-  (Rule
-    (= t1 t0)
-    (name "(rewrite (Add a b) (Add b a) :ruleset optimization)")
-    (premises (Fiat (= t0 t0)))
-    (substitution (a (Num 2)) (b (Num 3)) (@rewrite_var__ t0))))
+(Rule
+  (= t0 (Add (Num 3) (Num 2)))
+  (name "(rewrite (Add a b) (Add b a) :ruleset optimization)")
+  (premises (Fiat (= t0 t0)))
+  (substitution (a (Num 2)) (b (Num 3)) (@rewrite_var__ t0)))
diff --git a/egglog/CHANGELOG.md b/egglog/CHANGELOG.md
@@ -2,11 +2,24 @@
 
 ## [Unreleased] - ReleaseDate
 
+- The term/proof encoding supports `:no-merge` functions with a primitive or `Unit` output (encoded as an FD view declared native `:no-merge` with an identity-column guard on the output), but no longer supports `:no-merge` functions with an eq-sort output (whose conflict check needs union-find leaders). An eq-sort `:no-merge` program is reported unsupported and must run on the native backend, or give the function a `:merge` (e.g. `:merge old`). This removes the rule/`current`-helper machinery the encoding previously used to emulate `:no-merge`.
+- `(fail <command>+)` now accepts multiple commands, running them in order and succeeding if any one fails (previously it wrapped a single command). Desugaring, global removal, and proof encoding keep the whole expansion of a wrapped command inside the `fail`, so `fail` now works over commands that expand to several — including `(fail (set …))` under the term/proof encoding.
+- In the term/proof encoding, load `(input …)` for custom functions (with or without `:merge`, including `:no-merge` `Unit`-output ones) natively via `EGraph::native_input`, the same path already used for constructors and relations. This removes the per-input bodyless "loader rule" (and its fresh ruleset) that custom-function inputs used to compile to.
+- Make proof extraction deterministic so proof-mode snapshot tests no longer flake on backends with nondeterministic row order (the differential-dataflow backend).
+- Speed up freeing external functions, which was quadratic in the number of short-lived one-shot rules created (e.g. under the term/proof encoding).
+- Speed up `core-relations`' `merge_all` by resetting only the tables that changed during the call instead of every table.
+- Desugar global variables as functions instead of constructor + `union` in the term/proof encoding, and skip rebuilding after non-`union` top-level actions (removing a per-definition rebuild cost).
 - Fix user-defined primitives (registered through the Rust API after construction) being reported as unbound under term encoding / proofs: primitive registration now also reaches the term-encoding typechecker, so the encoder can typecheck the encoded program. Previously callers had to manually register the primitive on `proof_state.original_typechecking` as well.
 - **Pluggable backend SPI.** `EGraph::with_backend(Box<dyn Backend>)` lets a third party drive the egglog frontend with their own backend (see the `egglog-backend-trait` crate and the `egglog-experimental-dd` example). A backend without a native union-find declares `Backend::requires_term_encoding()`; `EGraph::with_term_encoding()` opts such an e-graph into the term-encoding pipeline (congruence and rebuild lower to rules over `@uf` tables), and running a term-encoding-only backend without it now errors with `Error::BackendRequiresTermEncoding` instead of silently dropping `union`s.
+- Route the term/proof encoding's `get-fresh!` (id minting) and `set-if-empty` (view canonicalization) primitives through the backend SPI (`Backend::register_get_fresh` / `register_set_if_empty` / `register_view_proof`), so a backend can service them against its own storage instead of reaching into core-relations tables. The differential-dataflow backend implements them over its host-side mirror and now runs eq-sort programs under term/proof encoding.
 - Add `make nightly` and `scripts/nightly_bench.py`, a hyperfine-based benchmark harness that measures every `tests/**/*.egg` program at 1/2/4/8 threads and (where supported) in proof-testing mode, caps each run at a 2-minute timeout, skips sub-50ms programs, and emits an HTML dashboard (one row per benchmark, one column per configuration) for nightly.cs.washington.edu. The dashboard uses [eval-live](https://github.com/oflatt/eval-live) for interactive filtering and sorting.
 - Rework the term/proof encoding's union-find and congruence maintenance,
   substantially reducing proof-mode time and memory.
+- In the term/proof encoding, run a custom function's `:merge` in its
+  functional-dependency view's own `:merge` (like constructor congruence) instead
+  of a separate rule plus a `current` helper table. This computes the merge once
+  rather than twice, so encoded runs no longer mint over-merged extra term rows,
+  and the merged value is justified by a proper merge-function proof.
 - **Tuple-output functions.** A function may declare more than one output sort, e.g.
   `(function interval (Math) (i64 i64) :merge (values (max old0 new0) (min old1 new1)))`. Such a
   function stores its outputs as separate value columns; the functional dependency is