From d8458dcd71cf434ef3f7089fec8dde867a7f2e27 Mon Sep 17 00:00:00 2001 From: Oliver Flatt Date: Mon, 27 Jul 2026 17:53:35 +0000 Subject: [PATCH 1/5] Rebuild eq-sort children with one UF-driven rule + a materialized index Replace the per-column eq-sort rebuild fan-out with a single rule per child eq-sort, driven by an @UF edge joined against a materialized term->row index. This mirrors how a native rebuild iterates the e-nodes referencing a changed e-class, instead of matching the view once per column. - Index: one hidden `(function Index_ (S key...) Unit :merge old)` per distinct child eq-sort, maintained wherever the view is written or deleted. Leading with the term makes "which rows mention this term" a key-prefix lookup. Container children are not indexed: they carry no @UF row and are canonicalized structurally. - uf_canon / uf_canon_proof: per-eq-sort canonicalization primitives, expressed as the generic view-column read over the two-output @UF_ table so every backend (including Differential Dataflow) services them against its own storage. Registered from the sort's Sort command, so they survive re-parse. Each takes a fallback, making them leader-or-self and proof-or-reflexive. - The rule re-canonicalizes every eq-sort child of the row in its action, so one firing fixes the whole row. It reads @UF there, so it is :unsafe-seminaive; the driving @UF delta in the body makes that read sound. - Container children keep their per-column :naive rule, and the FD view's value column keeps its own rule. instrument_construct_into wrote the view with a raw `set`, bypassing update_fd_view; it now goes through update_fd_view so its rows get index entries. Without this those rows were unreachable from the rebuild rule and stayed stale, which unsafe_seminaive_matches_naive caught. Regenerated the proof snapshots: the different rebuild order yields different (checker-validated) proof derivations, plus fresh-var renumbering. Co-Authored-By: Claude Opus 5 --- egglog/src/proofs/proof_container_rebuild.rs | 99 ++++++ egglog/src/proofs/proof_encoding.rs | 146 +++++++- egglog/src/proofs/proof_encoding_rebuild.rs | 318 ++++++++++++------ egglog/src/typechecking.rs | 10 +- .../files__proofs__array_proof_testing.snap | 111 +++--- .../files__proofs__calc_proof_testing.snap | 32 +- ...es__proofs__combinators_proof_testing.snap | 115 +++---- ...roofs__container_proofs_proof_testing.snap | 16 +- ...ontainer_reorder_proofs_proof_testing.snap | 20 +- ...ontainer_output_rebuild_proof_testing.snap | 4 +- ...oofs__eqsat_basic_proof_proof_testing.snap | 64 ++-- ...es__proofs__eqsat_basic_proof_testing.snap | 64 ++-- ...ofs__filter_or_bool_neq_proof_testing.snap | 2 +- ...s__proofs__intersection_proof_testing.snap | 2 +- .../files__proofs__matrix_proof_testing.snap | 28 +- ...ainer_dirty_propagation_proof_testing.snap | 2 +- ...__unification_points_to_proof_testing.snap | 4 +- .../files__proofs__until_proof_testing.snap | 4 +- 18 files changed, 690 insertions(+), 351 deletions(-) diff --git a/egglog/src/proofs/proof_container_rebuild.rs b/egglog/src/proofs/proof_container_rebuild.rs index 263c48fd..183a33c3 100644 --- a/egglog/src/proofs/proof_container_rebuild.rs +++ b/egglog/src/proofs/proof_container_rebuild.rs @@ -7,6 +7,10 @@ //! proof mode, prove the rebuild). Also holds the encoder-side spec bookkeeping //! ([`ProofInstrumentor::build_container_rebuild_spec`] and the primitive-name //! lookups). +//! +//! The eq-sort counterparts `uf_canon` / `uf_canon_proof` ([`register_uf_canon`]) +//! live here too: they canonicalize one eq-sort term against its `@UF` table, +//! letting the rebuild rules canonicalize a whole row in their action. use super::proof_encoding::ProofInstrumentor; use crate::exec_state::{Internal, RegistrySealed}; @@ -31,6 +35,101 @@ fn mint_proof_row( out } +/// Name of an eq-sort's `uf_canon` primitive, derived from its `@UF_` table +/// name. Both the encoder and the typechecker compute it the same way, so the +/// desugared program needs no extra annotation to find it. +pub(crate) fn uf_canon_prim_name(uf_name: &str) -> String { + format!("{uf_name}_canon") +} + +/// Name of an eq-sort's `uf_canon_proof` primitive. See [`uf_canon_prim_name`]. +pub(crate) fn uf_canon_proof_prim_name(uf_name: &str) -> String { + format!("{uf_name}_canon_proof") +} + +/// Register an eq-sort's single-term canonicalization primitives, so a rebuild +/// rule can canonicalize a child in its action: +/// +/// * `uf_canon : (S S) -> S` — `(term fallback)`, the term's `@UF_` leader, or +/// `fallback` when it has no row. Callers pass the term itself, making this +/// leader-or-self. +/// * `uf_canon_proof : (S Proof) -> Proof` (proof mode) — `(term fallback)`, the +/// `@UF_` row's proof `term = leader`, or `fallback`. Callers pass the +/// reflexive `Proof(term)`. +/// +/// Both are the generic view-column read over the two-output `@UF_` table, so +/// each backend services them against its own storage. They read `@UF_`, so +/// they are only sound in the action of a rule whose body joins the driving +/// `@UF` delta. Called from the eq-sort's Sort command in typechecking, so they +/// exist both during encoding and on re-parse. +pub(crate) fn register_uf_canon( + eg: &mut EGraph, + sort_name: &str, + uf_name: &str, + proofs_enabled: bool, +) { + let Some(sort) = eg.get_sort_by_name(sort_name).cloned() else { + return; + }; + let canon = UfCanonCol { + name: uf_canon_prim_name(uf_name), + key_sort: sort.clone(), + out_sort: sort.clone(), + }; + let table = uf_name.to_string(); + eg.add_backend_op_primitive(canon, WriteState::valid_contexts(), move |backend, _| { + backend.register_view_column_read(table.clone(), 1, 0) + }); + + // The proof column is only meaningful in proof mode; in term mode `@UF_` + // carries `Unit` there and no rebuild rule reads it. + if proofs_enabled { + let proof_sort: ArcSort = std::sync::Arc::new(EqSort { + name: eg.proof_state.proof_names.proof_datatype.clone(), + }); + let canon_proof = UfCanonCol { + name: uf_canon_proof_prim_name(uf_name), + key_sort: sort, + out_sort: proof_sort, + }; + let table = uf_name.to_string(); + eg.add_backend_op_primitive( + canon_proof, + WriteState::valid_contexts(), + move |backend, _| backend.register_view_column_read(table.clone(), 1, 1), + ); + } +} + +/// One column of an eq-sort's `@UF_` row, read by term with a fallback (see +/// [`register_uf_canon`]). +#[derive(Clone)] +struct UfCanonCol { + name: String, + key_sort: ArcSort, + out_sort: ArcSort, +} + +impl Primitive for UfCanonCol { + fn name(&self) -> &str { + &self.name + } + + fn get_type_constraints(&self, span: &Span) -> Box { + // (term fallback) -> column + SimpleTypeConstraint::new( + &self.name, + vec![ + self.key_sort.clone(), + self.out_sort.clone(), + self.out_sort.clone(), + ], + span.clone(), + ) + .into_box() + } +} + /// Register a container sort's rebuild primitives from its /// [`ContainerRebuildSpec`]. Called when a container Sort command carrying an /// `:internal-container-rebuild` annotation is typechecked, so the primitives diff --git a/egglog/src/proofs/proof_encoding.rs b/egglog/src/proofs/proof_encoding.rs index e6c6b0d5..1ddd15e4 100644 --- a/egglog/src/proofs/proof_encoding.rs +++ b/egglog/src/proofs/proof_encoding.rs @@ -98,6 +98,19 @@ enum CarriedProofs { EclassToTerm, } +/// A materialized rebuild index on one function's view, covering the view's key +/// columns of a single eq-sort. The table is `(term, ) -> Unit` +/// and holds one row per indexed key column, with that column's term leading. +/// `positions` are those key-column indices. Leading with the term makes "which +/// rows mention this term" a key-prefix lookup, which is how the `@UF`-driven +/// rebuild rule finds the rows it must re-canonicalize. +#[derive(Clone)] +pub(crate) struct ViewIndex { + pub name: String, + pub sort_name: String, + pub positions: Vec, +} + // TODO refactor so that encoding state is optional on the e-graph, ProofNames not optional on EncodingState. Then we don't have to clone proof names everywhere. #[derive(Clone)] pub(crate) struct EncodingState { @@ -117,6 +130,9 @@ pub(crate) struct EncodingState { /// Maps container sort name -> the name of its registered proof-producing /// container-rebuild primitive (`ContainerRebuildProof`). Proof mode only. pub container_rebuild_proof_name: HashMap, + /// Function name -> the materialized rebuild indexes on its view, one per + /// distinct eq-sort among the view's key columns (see [`ViewIndex`]). + pub view_index: HashMap>, pub term_header_added: bool, // TODO this is very ugly- we should separate out a typechecking struct // since we didn't need an entire e-graph @@ -141,6 +157,7 @@ impl EncodingState { proof_func_parent: HashMap::default(), container_rebuild_name: HashMap::default(), container_rebuild_proof_name: HashMap::default(), + view_index: HashMap::default(), term_header_added: false, original_typechecking: None, proofs_enabled: false, @@ -513,7 +530,6 @@ impl<'a> ProofInstrumentor<'a> { let proof_sort = self.proof_sort(); let trans = self.proof_names().eq_trans_constructor.clone(); let sym = self.proof_names().eq_sym_constructor.clone(); - let view = self.view_name(&ctor_name); let (dedup_args, fv_nat, nat_prf, nat_to_dedup) = self.build_natural_with_congr( res, &ctor_name, @@ -539,10 +555,7 @@ impl<'a> ProofInstrumentor<'a> { // the target. Emitting `(F dedup_args target)` would add the guest's // shape to `target`'s term relation, making `target`'s `@Ast` ambiguous // during proof reconstruction (which reads term rows, not views). - let dedup_disp = ListDisplay(&dedup_args, " ").to_string(); - res.push(format!( - "(set ({view} {dedup_disp}) (values {target} {view_proof}))" - )); + res.push(self.update_fd_view(&ctor_name, &dedup_args, target, &view_proof)); res.push(format!("(let {guest} {target})")); let sv = self.mint(res, &sym, &view_proof, &proof_sort); let guest_conn = self.mint(res, &trans, &format!("{nat_to_dedup} {sv}"), &proof_sort); @@ -758,6 +771,9 @@ impl<'a> ProofInstrumentor<'a> { let view_name = self.view_name(&fdecl.name); let in_sorts = ListDisplay(schema.input.clone(), " "); let fresh_sort = self.egraph.parser.symbol_gen.fresh("view"); + // Register the rebuild indexes before instrumenting any view write for + // this function, so every write site can emit its index maintenance. + let index_decls = self.declare_view_indexes(fdecl); let delete_rule = self.delete_and_subsume(fdecl); let to_delete_name = self.delete_name(&fdecl.name); let subsumed_name = self.subsumed_name(&fdecl.name); @@ -880,6 +896,7 @@ impl<'a> ProofInstrumentor<'a> { {view_decl} (function {to_delete_name} ({in_sorts}) Unit :no-merge :internal-hidden) (function {subsumed_name} ({in_sorts}) Unit :no-merge :internal-hidden) + {index_decls} {delete_rule}", )) } @@ -1098,8 +1115,9 @@ impl<'a> ProofInstrumentor<'a> { } /// Write a row into a functional-dependency view - /// `(set (@FView children) (values eclass proof))`. Re-setting an existing `children` key with a - /// different `eclass` triggers the view's `:merge`. + /// `(set (@FView children) (values eclass proof))`, plus the row's rebuild-index + /// entries. Re-setting an existing `children` key with a different `eclass` + /// triggers the view's `:merge`. pub(super) fn update_fd_view( &mut self, fname: &str, @@ -1108,12 +1126,115 @@ impl<'a> ProofInstrumentor<'a> { proof: &str, ) -> String { let view_name = self.view_name(fname); + let index_inserts = self.view_index_inserts(fname, children); format!( - "(set ({view_name} {}) (values {value} {proof}))", + "(set ({view_name} {}) (values {value} {proof}))\n{index_inserts}", ListDisplay(children, " ") ) } + /// Declare one materialized rebuild index per distinct eq-sort among a view's + /// key columns, record them in [`EncodingState::view_index`], and return the + /// declarations. Container key columns get none: they carry no `@UF` row to + /// drive a lookup and are canonicalized structurally instead. + /// + /// Must run before any view write for this function is instrumented, so the + /// metadata is present when [`Self::view_index_inserts`] / + /// [`Self::view_index_deletes`] are consulted. + fn declare_view_indexes(&mut self, fdecl: &ResolvedFunctionDecl) -> String { + let types = fdecl.resolved_schema.view_types(); + let n_keys = types.len() - 1; + let key_sorts = types[..n_keys] + .iter() + .map(|t| t.name().to_string()) + .collect::>() + .join(" "); + let mut by_sort: Vec<(String, Vec)> = Vec::new(); + for i in Self::view_index_positions(&types, n_keys) { + let sort = types[i].name().to_string(); + match by_sort.iter_mut().find(|(s, _)| *s == sort) { + Some((_, positions)) => positions.push(i), + None => by_sort.push((sort, vec![i])), + } + } + let mut decls = String::new(); + let mut entries = Vec::new(); + for (sort_name, positions) in by_sort { + let index_name = self + .egraph + .parser + .symbol_gen + .fresh(&format!("{}Index_{sort_name}", fdecl.name)); + decls.push_str(&format!( + "(function {index_name} ({sort_name} {key_sorts}) Unit :merge old :internal-hidden :unextractable)\n" + )); + entries.push(ViewIndex { + name: index_name, + sort_name, + positions, + }); + } + self.egraph + .proof_state + .view_index + .insert(fdecl.name.clone(), entries); + decls + } + + /// The view key positions that get a rebuild index: the non-container + /// eq-sort ones. Every such position is indexed, including the first, since + /// the rebuild rule is driven by an `@UF` delta on any child. + fn view_index_positions(types: &[ArcSort], n_keys: usize) -> Vec { + (0..n_keys) + .filter(|&i| !types[i].is_eq_container_sort() && types[i].is_eq_sort()) + .collect() + } + + /// [`Self::view_index_inserts`], appended to `res` only when the view has + /// indexes (so a view with no eq-sort children emits no blank statement). + fn push_view_index_inserts(&mut self, res: &mut Stmts, fname: &str, key: &[String]) { + let inserts = self.view_index_inserts(fname, key); + if !inserts.is_empty() { + res.push(inserts); + } + } + + /// Insert a view row into each of its rebuild indexes: one entry per indexed + /// key column, `(set ( key[pos] ) ())`. `key` is the view's + /// key columns (the children). + pub(super) fn view_index_inserts(&mut self, fname: &str, key: &[String]) -> String { + self.view_index_ops(fname, key, |name, term, whole| { + format!("(set ({name} {term} {whole}) ())") + }) + } + + /// Remove a view row from each of its rebuild indexes, mirroring + /// [`Self::view_index_inserts`]. Emitted wherever a view row is deleted. + pub(super) fn view_index_deletes(&mut self, fname: &str, key: &[String]) -> String { + self.view_index_ops(fname, key, |name, term, whole| { + format!("(delete ({name} {term} {whole}))") + }) + } + + fn view_index_ops( + &mut self, + fname: &str, + key: &[String], + op: impl Fn(&str, &str, &str) -> String, + ) -> String { + let Some(indexes) = self.egraph.proof_state.view_index.get(fname).cloned() else { + return String::new(); + }; + let whole = format!("{}", ListDisplay(key, " ")); + let mut out = Vec::new(); + for vi in &indexes { + for &pos in &vi.positions { + out.push(op(&vi.name, &key[pos], &whole)); + } + } + out.join("\n") + } + /// Intern the term/proof/AST/proof-list node `{name}(args_joined)` and return /// its id. Every such node table is hash-consed (see [`Self::hash_cons`]), so /// building the same node twice reuses one id instead of piling up @@ -1285,6 +1406,8 @@ impl<'a> ProofInstrumentor<'a> { "(let {canon} ({set_if_empty} {} {fv} ()))", ListDisplay(args, " ") )); + // `set-if-empty` writes the view row itself, so index its key here. + self.push_view_index_inserts(res, &func_type.name, args); canon } @@ -1384,13 +1507,16 @@ impl<'a> ProofInstrumentor<'a> { let dedup = self.fresh_var(); let vprf = self.fresh_var(); let view_proof = crate::proofs::proof_fresh::view_proof_prim_name(&view); - let dedup_args = ListDisplay(&dedup_args, " "); res.push(format!( "(set ({term_proof_constructor} {fv_nat}) {nat_prf})" )); res.push(format!( - "(let {dedup} ({set_if_empty} {dedup_args} {fv_nat} {nat_to_dedup_term}))" + "(let {dedup} ({set_if_empty} {} {fv_nat} {nat_to_dedup_term}))", + ListDisplay(&dedup_args, " ") )); + // `set-if-empty` writes the view row itself, so index its key here. + self.push_view_index_inserts(res, &func_type.name, &dedup_args); + let dedup_args = ListDisplay(&dedup_args, " "); res.push(format!( "(let {vprf} ({view_proof} {dedup_args} {nat_to_dedup_term}))" )); diff --git a/egglog/src/proofs/proof_encoding_rebuild.rs b/egglog/src/proofs/proof_encoding_rebuild.rs index 61af67b9..edfa1b6c 100644 --- a/egglog/src/proofs/proof_encoding_rebuild.rs +++ b/egglog/src/proofs/proof_encoding_rebuild.rs @@ -3,10 +3,29 @@ //! that execute requested deletes/subsumptions. (`@UF` path compression stays //! in [`super::proof_encoding`].) -use super::proof_encoding::{ProofInstrumentor, Stmts}; +use super::proof_encoding::{ProofInstrumentor, Stmts, ViewIndex}; use crate::typechecking::FuncType; use crate::*; +/// How a maintenance-rebuild rule is evaluated. +/// +/// `EncodingState::force_proof_naive` does not apply to these rules. It swaps an +/// RHS-reading rule for a `:naive` equivalent so tests can compare the two, which +/// only holds for a rule that does not write the tables its own body joins. A +/// rebuild rule re-keys the very view and index rows it matches, so its `:naive` +/// form stops after one pass per match instead of iterating that feedback to a +/// fixpoint, and the two forms saturate at different databases. +enum RebuildEval { + /// The rule's body sees every atom it depends on. + Seminaive, + /// A primitive in the rule reads `@UF` tables the body does not join on, and + /// no delta on them drives the rule. + Naive, + /// A primitive in the rule's *action* reads `@UF`, but the body joins the + /// driving `@UF` delta, which makes that read sound. + UnsafeSeminaive, +} + /// Which FD-view value column [`ProofInstrumentor::fd_value_rebuild_rule`] rebuilds. enum ValueRebuild { /// The value is the term's e-class (constructors and globals). @@ -22,14 +41,10 @@ enum ValueRebuild { impl ProofInstrumentor<'_> { /// Rules that execute deletion and subsumption based on the tables requesting the deletion/subsumption. pub(super) fn delete_and_subsume(&mut self, fdecl: &ResolvedFunctionDecl) -> String { - let child_names = fdecl - .schema - .input - .iter() - .enumerate() - .map(|(i, _)| format!("c{i}_")) - .collect::>() - .join(" "); + let child_vars: Vec = (0..fdecl.schema.input.len()) + .map(|i| format!("c{i}_")) + .collect(); + let child_names = child_vars.join(" "); let to_delete_name = self.delete_name(&fdecl.name); let subsumed_name = self.subsumed_name(&fdecl.name); let view_name = self.view_name(&fdecl.name); @@ -38,17 +53,19 @@ impl ProofInstrumentor<'_> { // The view is keyed by children only, so match its value tuple to // delete/subsume by key (the bridge re-reads every value column when - // subsuming a tuple-output view). Deletion removes the row by key; - // subsumption marks it subsumed (kept for size/proofs but excluded from - // matching). + // subsuming a tuple-output view). Deletion removes the row by key, taking + // its rebuild-index entries with it; subsumption keeps the row (excluded + // from matching but retained for size/proofs), so the index is untouched. let e = self.fresh_var(); let pf = self.fresh_var(); let e2 = self.fresh_var(); let pf2 = self.fresh_var(); + let index_deletes = self.view_index_deletes(&fdecl.name, &child_vars); format!( "(rule (({to_delete_name} {child_names}) (= (values {e} {pf}) ({view_name} {child_names}))) ((delete ({view_name} {child_names})) + {index_deletes} (delete ({to_delete_name} {child_names}))) :ruleset {delete_subsume_ruleset} :name \"{fresh_name}\") @@ -62,29 +79,36 @@ impl ProofInstrumentor<'_> { /// Wrap one maintenance-rebuild rule (`facts` -> `actions`) with the rebuilding /// ruleset, a fresh name, and `:internal-include-subsumed` (so stale rows are - /// rebuilt too). `naive` marks rules whose primitives read `@UF` tables the rule - /// body doesn't join on. - fn rebuild_rule(&mut self, facts: &str, actions: &str, naive: bool) -> String { + /// rebuilt too). + fn rebuild_rule(&mut self, facts: &str, actions: &str, eval: RebuildEval) -> String { let ruleset = self.proof_names().rebuilding_ruleset_name.clone(); let fresh_name = self.egraph.parser.symbol_gen.fresh("rebuild_rule"); - let naive = if naive { ":naive " } else { "" }; + let eval = match eval { + RebuildEval::Seminaive => "", + RebuildEval::Naive => ":naive ", + RebuildEval::UnsafeSeminaive => ":unsafe-seminaive ", + }; format!( - "(rule ({facts})\n ({actions})\n :ruleset {ruleset} {naive}:name \"{fresh_name}\" :internal-include-subsumed)\n" + "(rule ({facts})\n ({actions})\n :ruleset {ruleset} {eval}:name \"{fresh_name}\" :internal-include-subsumed)\n" ) } - /// Rebuild rules that keep a view canonical: one rule per rebuildable child - /// column (a canonical column has no `@UF` row, so the rule simply doesn't - /// match), plus a rule for the FD view's value column. A stale eq-sort column is - /// replaced by its `@UF` leader, a stale container by its rebuilt value. + /// Rebuild rules that keep a view canonical, plus a rule for the FD view's + /// value column. + /// + /// The view's eq-sort children are canonicalized by one rule per distinct + /// child eq-sort ([`Self::eq_sort_rebuild_rule`]), driven by an `@UF` delta + /// joined against that sort's rebuild index. Container children keep a + /// per-column `:naive` rule ([`Self::container_child_rebuild_rule`]): a + /// container has no `@UF` row to drive a rule, and its rebuild primitive + /// reads `@UF` tables the body does not join on. The value column is + /// canonicalized by [`Self::fd_value_rebuild_rule`]. /// /// A child update re-keys the row (`set` at the canonicalized children, then - /// `delete`); a collision on the new key runs the view's `:merge`. The value - /// column is canonicalized by [`Self::fd_value_rebuild_rule`]. In proof mode - /// each rule composes the updated view proof, and a container update records the - /// rebuilt container's `Proof`. + /// `delete`, index entries following the row); a collision on the new key runs + /// the view's `:merge`. In proof mode each rule composes the updated view + /// proof, and a container update records the rebuilt container's `Proof`. pub(super) fn rebuilding_rules(&mut self, fdecl: &ResolvedFunctionDecl) -> Vec { - let proofs = self.proofs_enabled(); // A global's output *is* its e-class (like a constructor's), so it takes the // e-class rebuild below (union-tracking) — not the custom-output rebuild // (congruence), which would emit a nonsensical `Congr` on its nullary term. @@ -95,93 +119,22 @@ impl ProofInstrumentor<'_> { // Key columns of the view row: the children (the value tuple is unkeyed). let n_keys = n - 1; let key_vars: Vec = (0..n_keys).map(child).collect(); - let view_name = self.view_name(&fdecl.name); - let keys_str = format!("{}", ListDisplay(&key_vars, " ")); let mut rules = String::new(); - // One rule per rebuildable key column (re-keys the row via set + delete). for (i, ty) in types[..n_keys].iter().enumerate() { - let is_container = ty.is_eq_container_sort(); - if !is_container && !ty.is_eq_sort() { - continue; + if ty.is_eq_container_sort() { + rules.push_str(&self.container_child_rebuild_rule(fdecl, &key_vars, i, ty)); } - let ci = child(i); - let canon = format!("c{i}_canon_"); - let (query_view, value_var, view_prf) = self.query_fd_view(&fdecl.name, &key_vars); - // Canonicalize the column with the container rebuild primitive or a `@UF` - // lookup, and build the proof pieces. Container-reading rules are `:naive` - // (the primitive reads `@UF` tables the rule doesn't join on). - let (canon_fact, proof_lets, pf_arg, cproof_set) = if is_container { - let value_prim = self.container_rebuild_prim(ty); - let canon_fact = format!("(= {canon} ({value_prim} {ci}))"); - if proofs { - let congr = self.proof_names().congr_constructor.clone(); - let trans = self.proof_names().eq_trans_constructor.clone(); - let sym = self.proof_names().eq_sym_constructor.clone(); - let proof_sort = self.proof_sort(); - let proof_prim = self.container_rebuild_proof_prim(ty); - let rebuild_pf = self.fresh_var(); - let cproof = self.term_proof_name(ty.name()); - // proof_lets: bind the container rebuild proof, then mint the congr proof. - let mut lets = Stmts::new(); - lets.push(format!("(let {rebuild_pf} ({proof_prim} {ci}))")); - let new_pf = self.mint( - &mut lets, - &congr, - &format!("{view_prf} {i} {rebuild_pf}"), - &proof_sort, - ); - // cproof_set: mint (Sym rebuild_pf), (Trans .. rebuild_pf), then record it. - let mut cproof_stmts = Stmts::new(); - let sym_pf = self.mint(&mut cproof_stmts, &sym, &rebuild_pf, &proof_sort); - let trans_pf = self.mint( - &mut cproof_stmts, - &trans, - &format!("{sym_pf} {rebuild_pf}"), - &proof_sort, - ); - cproof_stmts.push(format!("(set ({cproof} {canon}) {trans_pf})")); - ( - canon_fact, - lets.join("\n "), - new_pf, - cproof_stmts.join("\n "), - ) - } else { - (canon_fact, String::new(), "()".to_string(), String::new()) - } - } else { - let uf_name = self.uf_name(ty.name()); - let uf_prf = self.fresh_var(); - let canon_fact = format!("(= (values {canon} {uf_prf}) ({uf_name} {ci}))"); - if proofs { - let congr = self.proof_names().congr_constructor.clone(); - let proof_sort = self.proof_sort(); - let mut lets = Stmts::new(); - let new_pf = self.mint( - &mut lets, - &congr, - &format!("{view_prf} {i} {uf_prf}"), - &proof_sort, - ); - ( - canon_fact, - lets.join("\n "), - new_pf, - String::new(), - ) - } else { - (canon_fact, String::new(), "()".to_string(), String::new()) - } - }; - let mut updated = key_vars.clone(); - updated[i] = canon.clone(); - let updated_view = self.update_fd_view(&fdecl.name, &updated, &value_var, &pf_arg); - let facts = format!("{query_view}\n{canon_fact}\n(!= {ci} {canon})"); - let actions = format!( - "{proof_lets}\n{updated_view}\n{cproof_set}\n(delete ({view_name} {keys_str}))" - ); - rules.push_str(&self.rebuild_rule(&facts, &actions, is_container)); + } + let indexes = self + .egraph + .proof_state + .view_index + .get(&fdecl.name) + .cloned() + .unwrap_or_default(); + for vi in &indexes { + rules.push_str(&self.eq_sort_rebuild_rule(fdecl, &key_vars, &types, vi)); } // FD view value column (see [`Self::fd_value_rebuild_rule`]). A // constructor/global's value *is* its e-class; a custom function's @@ -207,6 +160,149 @@ impl ProofInstrumentor<'_> { self.parse_program(&rules) } + /// The `:naive` per-column rebuild for a container child at key position `i`: + /// rebuild the container with its primitive, then re-key the row (`set` at the + /// rebuilt children, `delete` the old key) and move the row's index entries + /// with it. In proof mode the row proof gains a `Congr` at position `i` and + /// the rebuilt container gets its reflexive `Proof` anchor. + fn container_child_rebuild_rule( + &mut self, + fdecl: &ResolvedFunctionDecl, + key_vars: &[String], + i: usize, + ty: &ArcSort, + ) -> String { + let view_name = self.view_name(&fdecl.name); + let keys_str = format!("{}", ListDisplay(key_vars, " ")); + let index_deletes = self.view_index_deletes(&fdecl.name, key_vars); + let ci = &key_vars[i]; + let canon = format!("c{i}_canon_"); + let (query_view, value_var, view_prf) = self.query_fd_view(&fdecl.name, key_vars); + let value_prim = self.container_rebuild_prim(ty); + let canon_fact = format!("(= {canon} ({value_prim} {ci}))"); + let (proof_lets, pf_arg, cproof_set) = if self.proofs_enabled() { + let congr = self.proof_names().congr_constructor.clone(); + let trans = self.proof_names().eq_trans_constructor.clone(); + let sym = self.proof_names().eq_sym_constructor.clone(); + let proof_sort = self.proof_sort(); + let proof_prim = self.container_rebuild_proof_prim(ty); + let rebuild_pf = self.fresh_var(); + let cproof = self.term_proof_name(ty.name()); + // proof_lets: bind the container rebuild proof, then mint the congr proof. + let mut lets = Stmts::new(); + lets.push(format!("(let {rebuild_pf} ({proof_prim} {ci}))")); + let new_pf = self.mint( + &mut lets, + &congr, + &format!("{view_prf} {i} {rebuild_pf}"), + &proof_sort, + ); + // cproof_set: mint (Sym rebuild_pf), (Trans .. rebuild_pf), then record it. + let mut cproof_stmts = Stmts::new(); + let sym_pf = self.mint(&mut cproof_stmts, &sym, &rebuild_pf, &proof_sort); + let trans_pf = self.mint( + &mut cproof_stmts, + &trans, + &format!("{sym_pf} {rebuild_pf}"), + &proof_sort, + ); + cproof_stmts.push(format!("(set ({cproof} {canon}) {trans_pf})")); + ( + lets.join("\n "), + new_pf, + cproof_stmts.join("\n "), + ) + } else { + (String::new(), "()".to_string(), String::new()) + }; + let mut updated = key_vars.to_vec(); + updated[i] = canon.clone(); + let updated_view = self.update_fd_view(&fdecl.name, &updated, &value_var, &pf_arg); + let facts = format!("{query_view}\n{canon_fact}\n(!= {ci} {canon})"); + let actions = format!( + "{proof_lets}\n{updated_view}\n{cproof_set}\n(delete ({view_name} {keys_str}))\n{index_deletes}" + ); + self.rebuild_rule(&facts, &actions, RebuildEval::Naive) + } + + /// The single rule that canonicalizes every eq-sort child of a view row, for + /// the child sort `vi` indexes. + /// + /// An `@UF_` edge on some term is joined against `vi`'s index to reach the + /// rows mentioning that term by key lookup — the same access pattern a native + /// rebuild uses when it walks the e-nodes referencing a changed e-class. The + /// action then re-canonicalizes *all* the row's eq-sort children with + /// `uf_canon`, so one firing fixes the whole row rather than one column of it. + /// In proof mode it folds one `@Congr` per eq-sort child onto the row proof; + /// the steps for children that did not move are reflexive and collapse in the + /// proof simplifier. + fn eq_sort_rebuild_rule( + &mut self, + fdecl: &ResolvedFunctionDecl, + key_vars: &[String], + types: &[ArcSort], + vi: &ViewIndex, + ) -> String { + let proofs = self.proofs_enabled(); + let view_name = self.view_name(&fdecl.name); + let keys_str = format!("{}", ListDisplay(key_vars, " ")); + let index_deletes = self.view_index_deletes(&fdecl.name, key_vars); + + // Body: an `@UF_` edge on the referenced term, the index entry naming a + // row that mentions it, and that row's value tuple. + let follower = self.fresh_var(); + let leader = self.fresh_var(); + let leader_pf = self.fresh_var(); + let uf_name = self.uf_name(&vi.sort_name); + let uf_atom = format!("(= (values {leader} {leader_pf}) ({uf_name} {follower}))"); + let index_atom = format!("({} {follower} {keys_str})", vi.name); + let (query_view, value_var, view_prf) = self.query_fd_view(&fdecl.name, key_vars); + + // Action: canonicalize every eq-sort key column, folding its congruence + // step onto the row proof. Other columns carry over unchanged. + let mut lets = Stmts::new(); + let mut updated = key_vars.to_vec(); + let mut proof_acc = view_prf; + for j in 0..key_vars.len() { + if !types[j].is_eq_sort() || types[j].is_eq_container_sort() { + continue; + } + let canon = format!("c{j}_canon_"); + let cj = &key_vars[j]; + let uf_j = self.uf_name(types[j].name()); + let canon_prim = crate::proofs::proof_container_rebuild::uf_canon_prim_name(&uf_j); + // Fallback `cj`: a child with no `@UF` row is already a root. + lets.push(format!("(let {canon} ({canon_prim} {cj} {cj}))")); + if proofs { + let proof_prim = + crate::proofs::proof_container_rebuild::uf_canon_proof_prim_name(&uf_j); + let congr = self.proof_names().congr_constructor.clone(); + let proof_sort = self.proof_sort(); + // Fallback: the reflexive `cj = cj`, anchored when `cj` was built. + let term_proof = self.term_proof_name(types[j].name()); + let refl_pf = self.fresh_var(); + let step_pf = self.fresh_var(); + lets.push(format!("(let {refl_pf} ({term_proof} {cj}))")); + lets.push(format!("(let {step_pf} ({proof_prim} {cj} {refl_pf}))")); + proof_acc = self.mint( + &mut lets, + &congr, + &format!("{proof_acc} {j} {step_pf}"), + &proof_sort, + ); + } + updated[j] = canon; + } + let pf_arg = if proofs { proof_acc } else { "()".to_string() }; + let updated_view = self.update_fd_view(&fdecl.name, &updated, &value_var, &pf_arg); + let facts = format!("{uf_atom}\n(!= {follower} {leader})\n{index_atom}\n{query_view}"); + let actions = format!( + "{}\n{updated_view}\n(delete ({view_name} {keys_str}))\n{index_deletes}", + lets.join("\n ") + ); + self.rebuild_rule(&facts, &actions, RebuildEval::UnsafeSeminaive) + } + /// One rule that canonicalizes an FD view's stale value column. /// /// * [`ValueRebuild::Eclass`] (constructors/globals): the value *is* the @@ -278,7 +374,7 @@ impl ProofInstrumentor<'_> { let facts = format!( "{query_view}\n(= (values {canon} {uf_prf}) ({value_uf_name} {value_var}))\n(!= {value_var} {canon})" ); - self.rebuild_rule(&facts, &actions, false) + self.rebuild_rule(&facts, &actions, RebuildEval::Seminaive) } /// The [`ValueRebuild::ContainerOutput`] arm of @@ -337,7 +433,7 @@ impl ProofInstrumentor<'_> { let facts = format!("{query_view}\n{canon_fact}\n(!= {value_var} {canon})"); let actions = format!("{proof_lets}\n(delete ({view_name} {keys_str}))\n{set_canon}\n{cproof_set}"); - self.rebuild_rule(&facts, &actions, true) + self.rebuild_rule(&facts, &actions, RebuildEval::Naive) } /// Rules that update the to_subsume tables when children change. One rule per diff --git a/egglog/src/typechecking.rs b/egglog/src/typechecking.rs index 0ed95d7d..40f73cdf 100644 --- a/egglog/src/typechecking.rs +++ b/egglog/src/typechecking.rs @@ -1,7 +1,9 @@ use std::hash::Hasher; use crate::Context; -use crate::proofs::proof_container_rebuild::register_container_rebuild_from_spec; +use crate::proofs::proof_container_rebuild::{ + register_container_rebuild_from_spec, register_uf_canon, +}; use crate::{ core::{CoreActionContext, CoreRule, GenericActionsExt, QueryConstraints, ResolvedCall}, *, @@ -568,6 +570,12 @@ impl EGraph { if let Some(spec) = container_rebuild { register_container_rebuild_from_spec(self, name, spec); } + // An eq-sort under the encoding registers the single-term + // canonicalization primitives its rebuild rules call, derived + // from its `@UF_` table. + if let Some((uf_ctor, _uf_index)) = uf { + register_uf_canon(self, name, uf_ctor, proof_func.is_some()); + } ResolvedNCommand::Sort { span: span.clone(), name: name.clone(), diff --git a/egglog/tests/snapshots/files__proofs__array_proof_testing.snap b/egglog/tests/snapshots/files__proofs__array_proof_testing.snap index 01ffa3fe..9823228d 100644 --- a/egglog/tests/snapshots/files__proofs__array_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__array_proof_testing.snap @@ -1,6 +1,5 @@ --- source: egglog/tests/files.rs -assertion_line: 279 expression: proof_snapshot --- (let t0 (select (store (AVar "mem1") (Var "r1") (Num 42)) (Var "r1"))) @@ -121,7 +120,7 @@ expression: proof_snapshot (Congr (= t9 (neq t0 t4)) (Congr - (= t9 (neq t2 t4)) + (= t9 (neq t0 t8)) (Rule (= t9 t9) (name @@ -131,16 +130,16 @@ expression: proof_snapshot )") (premises (Fiat (= t10 t10)) (Fiat (= t2 t2))) (substitution (z (Var "r1")) (e t2) (y (Var "r3")) (x (Var "r2")))) - (Sym - (= t8 t4) - (Rule - (= t4 t8) - (name "(rewrite (add x y) (add y x))") - (premises (Fiat (= t4 t4))) - (substitution (@rewrite_var__2 t4) (x (Var "r1")) (y (Var "r3"))))) - 1) - prf0 - 0)) + prf0 + 0) + (Sym + (= t8 t4) + (Rule + (= t4 t8) + (name "(rewrite (add x y) (add y x))") + (premises (Fiat (= t4 t4))) + (substitution (@rewrite_var__2 t4) (x (Var "r1")) (y (Var "r3"))))) + 1)) (substitution (mem (AVar "mem1")) (e1 t5) (e (Num 2)) (i1 t0) (i2 t4))) (let t0 (add (Num 1) (Var "r1"))) (let t1 (add (Num 1) t0)) @@ -206,24 +205,24 @@ expression: proof_snapshot (let t17 (add (Num 1) (Num -3))) (let prf1 (Rule - (= t17 (Num -2)) - (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") - (premises - (Rule - (= t17 t17) - (name "(rewrite (add (add x y) z) (add x (add y z)))") - (premises - (Congr - (= t2 (add t12 (Num -3))) - (Fiat (= t2 t2)) - prf0 - 0)) - (substitution - (z (Num -3)) - (y (Num 1)) - (@rewrite_var__3 t2) - (x t0)))) - (substitution (@rewrite_var__4 t17) (x 1) (y -3)))) + (= t17 (Num -2)) + (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") + (premises + (Rule + (= t17 t17) + (name "(rewrite (add (add x y) z) (add x (add y z)))") + (premises + (Congr + (= t2 (add t12 (Num -3))) + (Fiat (= t2 t2)) + prf0 + 0)) + (substitution + (z (Num -3)) + (y (Num 1)) + (@rewrite_var__3 t2) + (x t0)))) + (substitution (@rewrite_var__4 t17) (x 1) (y -3)))) (Rule (= t3 (Var "r1")) (name "(rewrite (add x (Num 0)) x)") @@ -244,37 +243,37 @@ expression: proof_snapshot (Congr (= t6 (add (Num 2) t17)) (Congr - (= t6 (add t4 t17)) + (= t6 (add (Num 2) t5)) (Rule (= t6 t6) (name "(rewrite (add (add x y) z) (add x (add y z)))") t15 t16) - (Trans - (= t5 t17) - (Rule - (= t5 (Num -2)) - (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") - (premises - (Rule - (= t5 t5) - (name "(rewrite (add (add x y) z) (add x (add y z)))") - t8 - t10)) - (substitution (@rewrite_var__4 t5) (x -3) (y 1))) - (Sym (= (Num -2) t17) prf1)) - 1) - (Rule - (= t4 (Num 2)) - (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") - (premises - (Rule - (= t4 t4) - (name "(rewrite (add (add x y) z) (add x (add y z)))") - t13 - t14)) - (substitution (@rewrite_var__4 t4) (x 1) (y 1))) - 0) + (Rule + (= t4 (Num 2)) + (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") + (premises + (Rule + (= t4 t4) + (name "(rewrite (add (add x y) z) (add x (add y z)))") + t13 + t14)) + (substitution (@rewrite_var__4 t4) (x 1) (y 1))) + 0) + (Trans + (= t5 t17) + (Rule + (= t5 (Num -2)) + (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") + (premises + (Rule + (= t5 t5) + (name "(rewrite (add (add x y) z) (add x (add y z)))") + t8 + t10)) + (substitution (@rewrite_var__4 t5) (x -3) (y 1))) + (Sym (= (Num -2) t17) prf1)) + 1) prf1 1)) (substitution (@rewrite_var__4 t6) (x 2) (y -2))) diff --git a/egglog/tests/snapshots/files__proofs__calc_proof_testing.snap b/egglog/tests/snapshots/files__proofs__calc_proof_testing.snap index 3fd74f44..dde3990e 100644 --- a/egglog/tests/snapshots/files__proofs__calc_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__calc_proof_testing.snap @@ -17,26 +17,36 @@ expression: proof_snapshot (b (g* (AConst) (AConst))) (@rewrite_var__ t1))) (let t0 (g* (inv (aConst)) (aConst))) -(let t1 (g* (bConst) t0)) -(let t2 (g* t1 (inv (bConst)))) +(let t1 (g* (g* (bConst) t0) (inv (bConst)))) +(let t2 (g* t0 (inv (bConst)))) +(let t3 (premises (Fiat (= t1 t1)))) +(let t4 (substitution (c (inv (bConst))) (a (bConst)) (b t0) (@rewrite_var__ t1))) (Congr - (= t2 (g* (bConst) (inv (bConst)))) - (Fiat (= t2 t2)) + (= t1 (g* (bConst) (inv (bConst)))) (Rule - (= t1 (bConst)) - (name "(rewrite (g* a $I) a)") + (= t1 (g* (bConst) t2)) + (name "(birewrite (g* (g* a b) c) (g* a (g* b c)))=>") + t3 + t4) + (Rule + (= t2 (inv (bConst))) + (name "(rewrite (g* $I a) a)") (premises (Congr - (= t1 (g* (bConst) (IConst))) - (Fiat (= t1 t1)) + (= t2 (g* (IConst) (inv (bConst)))) + (Rule + (= t2 t2) + (name "(birewrite (g* (g* a b) c) (g* a (g* b c)))=>") + t3 + t4) (Rule (= t0 (IConst)) (name "(rewrite (g* (inv a) a) $I)") (premises (Fiat (= t0 t0))) (substitution (@rewrite_var__4 t0) (a (aConst)))) - 1)) - (substitution (a (bConst)) (@rewrite_var__3 t1))) - 0) + 0)) + (substitution (@rewrite_var__2 t2) (a (inv (bConst))))) + 1) (let t0 (g* (bConst) (inv (bConst)))) (Rule (= t0 (IConst)) diff --git a/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap b/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap index eaa5de35..26c568e7 100644 --- a/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap @@ -1,6 +1,5 @@ --- source: egglog/tests/files.rs -assertion_line: 279 expression: proof_snapshot --- (let t0 (If (Var "x") (N 0) (N 1))) @@ -411,13 +410,13 @@ expression: proof_snapshot (v "x") (n 0))) (let t76 (cx (Comb (N 0)))) -(let t77 (CApp (CAbs "x" (CIfConst)) (CFConst))) -(let t78 (CAbs "x" (Comb (Var "x")))) -(let t79 (CApp t78 (CFConst))) +(let t77 (CAbs "x" (Comb (Var "x")))) +(let t78 (CApp t77 (CFConst))) +(let t79 (CApp (CAbs "x" (CIfConst)) (CFConst))) (let t80 (CApp (CApp (SConst) (CAbs "x" (CIfConst))) - t78)) + t77)) (let t81 (premises (Rule @@ -454,7 +453,7 @@ expression: proof_snapshot (cz (CFConst)) (cx (CAbs "x" (CIfConst))) (@rewrite_var__16 t64) - (cy t78))) + (cy t77))) (let t85 (premises (Congr @@ -546,19 +545,21 @@ expression: proof_snapshot (Congr (= t64 (CApp (CIfConst) (CFConst))) (Congr - (= t64 (CApp t77 (CFConst))) + (= t64 (CApp (CIfConst) t78)) (Rule - (= t64 (CApp t77 t79)) + (= t64 (CApp t79 t78)) (name "(rewrite (CApp (CApp (CApp $S cx) cy) cz) (CApp (CApp cx cz) (CApp cy cz)))") t83 t84) (Rule - (= t79 (CFConst)) - (name "(rewrite (CApp $I cx) cx)") + (= t79 (CIfConst)) + (name "(rewrite (CApp (CApp $K cx) cy) cx)") (premises (Congr - (= t79 (CApp (IConst) (CFConst))) + (= + t79 + (CApp (CApp (KConst) (CIfConst)) (CFConst))) (Rule (= t79 t79) (name @@ -566,65 +567,65 @@ expression: proof_snapshot t83 t84) (Rule - (= t78 (IConst)) - (name "(rewrite (CAbs v (CVar v)) $I)") + (= + (CAbs "x" (CIfConst)) + (CApp (KConst) (CIfConst))) + (name "(rewrite (CAbs v $CIf) (CApp $K $CIf))") (premises - (Congr - (= t78 (CAbs "x" (CVar "x"))) - (Rule - (= t78 t78) - (name - "(rewrite (CAbs v (CApp x y)) (CApp (CApp $S (CAbs v x)) (CAbs v y)))") - t81 - t82) - (Rule - (= (Comb (Var "x")) (CVar "x")) - (name - "(rule ((= x (Var v))) - ((union (Comb x) (CVar v))) - )") - (premises (Fiat (= (Var "x") (Var "x")))) - (substitution (v "x") (x (Var "x")))) - 1)) - (substitution (@rewrite_var__2 t78) (v "x"))) + (Rule + (= + (CAbs "x" (CIfConst)) + (CAbs "x" (CIfConst))) + (name + "(rewrite (CAbs v (CApp x y)) (CApp (CApp $S (CAbs v x)) (CAbs v y)))") + t81 + t82)) + (substitution + (@rewrite_var__7 (CAbs "x" (CIfConst))) + (v "x"))) 0)) - (substitution (@rewrite_var__14 t79) (cx (CFConst)))) - 1) + (substitution + (@rewrite_var__15 t79) + (cx (CIfConst)) + (cy (CFConst)))) + 0) (Rule - (= t77 (CIfConst)) - (name "(rewrite (CApp (CApp $K cx) cy) cx)") + (= t78 (CFConst)) + (name "(rewrite (CApp $I cx) cx)") (premises (Congr - (= t77 (CApp (CApp (KConst) (CIfConst)) (CFConst))) + (= t78 (CApp (IConst) (CFConst))) (Rule - (= t77 t77) + (= t78 t78) (name "(rewrite (CApp (CApp (CApp $S cx) cy) cz) (CApp (CApp cx cz) (CApp cy cz)))") t83 t84) (Rule - (= - (CAbs "x" (CIfConst)) - (CApp (KConst) (CIfConst))) - (name "(rewrite (CAbs v $CIf) (CApp $K $CIf))") + (= t77 (IConst)) + (name "(rewrite (CAbs v (CVar v)) $I)") (premises - (Rule - (= - (CAbs "x" (CIfConst)) - (CAbs "x" (CIfConst))) - (name - "(rewrite (CAbs v (CApp x y)) (CApp (CApp $S (CAbs v x)) (CAbs v y)))") - t81 - t82)) - (substitution - (@rewrite_var__7 (CAbs "x" (CIfConst))) - (v "x"))) + (Congr + (= t77 (CAbs "x" (CVar "x"))) + (Rule + (= t77 t77) + (name + "(rewrite (CAbs v (CApp x y)) (CApp (CApp $S (CAbs v x)) (CAbs v y)))") + t81 + t82) + (Rule + (= (Comb (Var "x")) (CVar "x")) + (name + "(rule ((= x (Var v))) + ((union (Comb x) (CVar v))) + )") + (premises (Fiat (= (Var "x") (Var "x")))) + (substitution (v "x") (x (Var "x")))) + 1)) + (substitution (@rewrite_var__2 t77) (v "x"))) 0)) - (substitution - (@rewrite_var__15 t77) - (cx (CIfConst)) - (cy (CFConst)))) - 0) + (substitution (@rewrite_var__14 t78) (cx (CFConst)))) + 1) 0) 0))) (let t86 diff --git a/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap b/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap index 569927db..364b6591 100644 --- a/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap @@ -9,7 +9,7 @@ expression: proof_snapshot (= (@ExistsConstructor) (@ExistsConstructor)) (name "@prove_exists_rule") (premises prf0 (Fiat (= (Z) (Z))) prf0 (Eval) (Fiat (= t1 t1))) - (substitution (@v117 (Z)) (@v116 (S (Z))) (@v119 t0) (@v118 (S (Z))))) + (substitution (@v122 (S (Z))) (@v120 (S (Z))) (@v121 (Z)) (@v123 t0))) (let t0 (pair (Z) (S (Z)))) (let t1 (HasPair t0)) (Rule @@ -20,7 +20,7 @@ expression: proof_snapshot (Fiat (= (S (Z)) (S (Z)))) (Eval) (Fiat (= t1 t1))) - (substitution (@v278 t0) (@v276 (Z)) (@v277 (S (Z))))) + (substitution (@v282 t0) (@v280 (Z)) (@v281 (S (Z))))) (let t0 (vec-of (Z) (S (Z)))) (let t1 (HasVec t0)) (Rule @@ -31,7 +31,7 @@ expression: proof_snapshot (Fiat (= (S (Z)) (S (Z)))) (Eval) (Fiat (= t1 t1))) - (substitution (@v422 (Z)) (@v424 t0) (@v423 (S (Z))))) + (substitution (@v427 (S (Z))) (@v426 (Z)) (@v428 t0))) (let t0 (map-of (Z) (S (Z)))) (let t1 (HasMap t0)) (Rule @@ -42,7 +42,7 @@ expression: proof_snapshot (Fiat (= (S (Z)) (S (Z)))) (Eval) (Fiat (= t1 t1))) - (substitution (@v575 (Z)) (@v576 (S (Z))) (@v577 t0))) + (substitution (@v580 (S (Z))) (@v579 (Z)) (@v581 t0))) (let prf0 (Fiat (= (Z) (Z)))) (let t0 (multiset-of (S (Z)) (Z) (Z))) (let t1 (HasMS t0)) @@ -50,7 +50,7 @@ expression: proof_snapshot (= (@ExistsConstructor4) (@ExistsConstructor4)) (name "@prove_exists_rule4") (premises prf0 (Fiat (= (S (Z)) (S (Z)))) prf0 (Eval) (Fiat (= t1 t1))) - (substitution (@v722 (S (Z))) (@v721 (Z)) (@v724 t0) (@v723 (Z)))) + (substitution (@v725 (Z)) (@v726 (S (Z))) (@v728 t0) (@v727 (Z)))) (let t0 (vec-of (Z) (S (Z)))) (let t1 (HasVec t0)) (Rule @@ -94,7 +94,7 @@ expression: proof_snapshot ((MapGet w)) )") (premises (Fiat (= t1 t1)) (Fiat (= (Z) (Z))) (Fiat (= (S (Z)) (S (Z))))) - (substitution (m t0) (@v1079 (Z)) (w (S (Z))))) + (substitution (m t0) (@v1091 (Z)) (w (S (Z))))) (let t0 (multiset-of (S (Z)) (Z) (Z))) (let t1 (HasMS t0)) (Rule @@ -195,5 +195,5 @@ expression: proof_snapshot ((OutWrap w)) )") (premises (Fiat (= (HasElem (Z)) (HasElem (Z)))) (Eval) (Fiat (= t0 t0))) - (substitution (a (Z)) (w t0) (@v2050 (vec-of (Z) (Z)))))) - (substitution (@v2086 (Z)) (@v2087 (vec-of (Z) (Z))) (@v2085 (Z)))) + (substitution (a (Z)) (@v2081 (vec-of (Z) (Z))) (w t0)))) + (substitution (@v2117 (Z)) (@v2116 (Z)) (@v2118 (vec-of (Z) (Z))))) diff --git a/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap b/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap index 3f653318..7c28b1a4 100644 --- a/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap @@ -100,7 +100,7 @@ expression: proof_snapshot (substitution (x (N 2)) (@rewrite_var__ (Id (N 2))))) 1)) 0)) - (substitution (@v1106 (N 2)) (@v1107 t3) (@v1105 (N 1)))) + (substitution (@v1112 (N 1)) (@v1114 t3) (@v1113 (N 2)))) (let t0 (Add (Num 51) (Num 52))) (let t1 (Add (Num 52) (Num 51))) (let t2 (premises (Fiat (= (Go) (Go))))) @@ -147,7 +147,7 @@ expression: proof_snapshot prf0 0) 0)) - (substitution (@v1169 t1) (@v1170 t5))) + (substitution (@v1176 t1) (@v1177 t5))) (let t0 (premises (Fiat (= (Go) (Go))))) (let prf0 (Rule @@ -249,7 +249,7 @@ expression: proof_snapshot (substitution (x (N 12)) (@rewrite_var__ (Id (N 12))))) 1)) 0)) - (substitution (@v1231 (N 11)) (@v1232 (N 11)) (@v1234 t3) (@v1233 (N 12)))) + (substitution (@v1239 (N 11)) (@v1241 t3) (@v1240 (N 12)) (@v1238 (N 11)))) (let t0 (premises (Fiat (= (Go) (Go))))) (let prf0 (Rule @@ -344,11 +344,11 @@ expression: proof_snapshot 0)) 0)) (substitution - (@v1308 (N 23)) - (@v1307 (N 22)) - (@v1305 (N 21)) - (@v1306 (N 23)) - (@v1309 t3))) + (@v1316 t3) + (@v1312 (N 21)) + (@v1314 (N 22)) + (@v1315 (N 23)) + (@v1313 (N 23)))) (let t0 (premises (Fiat (= (Go) (Go))))) (let prf0 (Rule @@ -418,7 +418,7 @@ expression: proof_snapshot prf1 1) 0)) - (substitution (@v1389 (N 31)) (@v1390 (N 31)) (@v1391 (N 32)) (@v1392 t3))) + (substitution (@v1396 (N 31)) (@v1399 t3) (@v1397 (N 31)) (@v1398 (N 32)))) (let t0 (premises (Fiat (= (Go) (Go))))) (let prf0 (Rule @@ -526,4 +526,4 @@ expression: proof_snapshot 0) 1) 0)) - (substitution (@v1465 (N 41)) (@v1463 (N 41)) (@v1464 (N 42)) (@v1466 t5))) + (substitution (@v1473 t5) (@v1471 (N 42)) (@v1472 (N 41)) (@v1470 (N 41)))) diff --git a/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap b/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap index 01496689..f75d855e 100644 --- a/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap @@ -21,7 +21,7 @@ expression: proof_snapshot (Trans (= t0 t0) (Sym (= t0 t1) prf0) prf0) (Fiat (= (N 1) (N 1))) (Eval)) - (substitution (@n (set-of (N 1))) (@v136 (N 1)))) + (substitution (@v140 (N 1)) (@n (set-of (N 1))))) (let t0 (set-of (N 1) (N 3))) (let t1 (freer (N 0) t0)) (let t2 (freer (N 0) (set-of (N 1)))) @@ -49,4 +49,4 @@ expression: proof_snapshot (Fiat (= (N 1) (N 1))) (Fiat (= (N 3) (N 3))) (Eval)) - (substitution (@v235 (N 1)) (@v236 (N 3)) (@n1 t0))) + (substitution (@v240 (N 3)) (@v239 (N 1)) (@n1 t0))) diff --git a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap index fee6d239..3fe9c1ee 100644 --- a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap @@ -1,38 +1,38 @@ --- source: egglog/tests/files.rs -assertion_line: 279 expression: proof_snapshot --- (let t0 (Mul (Num 2) (Add (Var "x") (Num 3)))) (let t1 (Mul (Num 2) (Var "x"))) -(let t2 (Mul (Num 2) (Num 3))) -(let t3 (premises (Fiat (= t0 t0)))) -(let t4 - (substitution - (@rewrite_var__1 t0) - (a (Num 2)) - (b (Var "x")) - (c (Num 3)))) -(Congr - (= t0 (Add (Num 6) t1)) - (Rule - (= t0 (Add t2 t1)) - (name "(rewrite (Add a b) (Add b a))") - (premises - (Rule - (= t0 (Add t1 t2)) - (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") - t3 - t4)) - (substitution (a t1) (b t2) (@rewrite_var__ t0))) - (Rule - (= t2 (Num 6)) - (name "(rewrite (Mul (Num a) (Num b)) (Num (* a b)))") - (premises - (Rule - (= t2 t2) - (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") - t3 - t4)) - (substitution (a 2) (b 3) (@rewrite_var__3 t2))) - 0) +(let t2 (Add (Num 6) t1)) +(let t3 (Add t1 (Num 6))) +(let t4 (Mul (Num 2) (Num 3))) +(let t5 (premises (Fiat (= t0 t0)))) +(let t6 (substitution (@rewrite_var__1 t0) (a (Num 2)) (b (Var "x")) (c (Num 3)))) +(Trans + (= t0 t2) + (Congr + (= t0 t3) + (Rule + (= t0 (Add t1 t4)) + (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") + t5 + t6) + (Rule + (= t4 (Num 6)) + (name "(rewrite (Mul (Num a) (Num b)) (Num (* a b)))") + (premises + (Rule + (= t4 t4) + (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") + t5 + t6)) + (substitution (a 2) (b 3) (@rewrite_var__3 t4))) + 1) + (Sym + (= t3 t2) + (Rule + (= t2 t3) + (name "(rewrite (Add a b) (Add b a))") + (premises (Fiat (= t2 t2))) + (substitution (a (Num 6)) (b t1) (@rewrite_var__ t2))))) diff --git a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap index fee6d239..3fe9c1ee 100644 --- a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap @@ -1,38 +1,38 @@ --- source: egglog/tests/files.rs -assertion_line: 279 expression: proof_snapshot --- (let t0 (Mul (Num 2) (Add (Var "x") (Num 3)))) (let t1 (Mul (Num 2) (Var "x"))) -(let t2 (Mul (Num 2) (Num 3))) -(let t3 (premises (Fiat (= t0 t0)))) -(let t4 - (substitution - (@rewrite_var__1 t0) - (a (Num 2)) - (b (Var "x")) - (c (Num 3)))) -(Congr - (= t0 (Add (Num 6) t1)) - (Rule - (= t0 (Add t2 t1)) - (name "(rewrite (Add a b) (Add b a))") - (premises - (Rule - (= t0 (Add t1 t2)) - (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") - t3 - t4)) - (substitution (a t1) (b t2) (@rewrite_var__ t0))) - (Rule - (= t2 (Num 6)) - (name "(rewrite (Mul (Num a) (Num b)) (Num (* a b)))") - (premises - (Rule - (= t2 t2) - (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") - t3 - t4)) - (substitution (a 2) (b 3) (@rewrite_var__3 t2))) - 0) +(let t2 (Add (Num 6) t1)) +(let t3 (Add t1 (Num 6))) +(let t4 (Mul (Num 2) (Num 3))) +(let t5 (premises (Fiat (= t0 t0)))) +(let t6 (substitution (@rewrite_var__1 t0) (a (Num 2)) (b (Var "x")) (c (Num 3)))) +(Trans + (= t0 t2) + (Congr + (= t0 t3) + (Rule + (= t0 (Add t1 t4)) + (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") + t5 + t6) + (Rule + (= t4 (Num 6)) + (name "(rewrite (Mul (Num a) (Num b)) (Num (* a b)))") + (premises + (Rule + (= t4 t4) + (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") + t5 + t6)) + (substitution (a 2) (b 3) (@rewrite_var__3 t4))) + 1) + (Sym + (= t3 t2) + (Rule + (= t2 t3) + (name "(rewrite (Add a b) (Add b a))") + (premises (Fiat (= t2 t2))) + (substitution (a (Num 6)) (b t1) (@rewrite_var__ t2))))) diff --git a/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap b/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap index 2509796c..bf2f4e71 100644 --- a/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap @@ -23,4 +23,4 @@ expression: proof_snapshot (= (@ExistsConstructor16) (@ExistsConstructor16)) (name "@prove_exists_rule16") (premises prf0 (Fiat (= (Val 2) (Val 2))) prf0 prf0 (Fiat (= () ()))) - (substitution (@v991 (Val 1)) (@v990 (Val 2)) (@v989 (Val 1)) (@v992 (Val 1)))) + (substitution (@v998 (Val 1)) (@v996 (Val 2)) (@v997 (Val 1)) (@v995 (Val 1)))) diff --git a/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap b/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap index 06d47a79..a1db2740 100644 --- a/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap @@ -165,4 +165,4 @@ expression: proof_snapshot (x3 (Var "b3")) t2))) (Fiat (= () ()))) - (substitution (@v834 t3) (@v833 t0))) + (substitution (@v840 t0) (@v841 t3))) diff --git a/egglog/tests/snapshots/files__proofs__matrix_proof_testing.snap b/egglog/tests/snapshots/files__proofs__matrix_proof_testing.snap index c6583938..be988f50 100644 --- a/egglog/tests/snapshots/files__proofs__matrix_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__matrix_proof_testing.snap @@ -63,8 +63,8 @@ expression: proof_snapshot (let t2 (MMul t0 t1)) (let prop0 (= t2 t2)) (let t3 (Kron (NamedMat "A") (NamedMat "B"))) -(let t4 (MMul (Id (NamedDim "n")) (NamedMat "A"))) -(let t5 (MMul (NamedMat "B") (Id (NamedDim "m")))) +(let t4 (MMul (NamedMat "B") (Id (NamedDim "m")))) +(let t5 (MMul (Id (NamedDim "n")) (NamedMat "A"))) (let t6 (ncols (Id (NamedDim "n")))) (let t7 (A (Id (NamedDim "n")))) (let t8 (nrows (Id (NamedDim "m")))) @@ -127,16 +127,16 @@ expression: proof_snapshot (Congr (= t2 t3) (Congr - (= t2 (Kron t4 (NamedMat "B"))) + (= t2 (Kron (NamedMat "A") t4)) (Rule - (= t2 (Kron t4 t5)) + (= t2 (Kron t5 t4)) (name "(rewrite (MMul (Kron A B) (Kron C D)) (Kron (MMul A C) (MMul B D)) :when ((= (ncols A) (nrows C)) (= (ncols B) (nrows D))))") t9 t10) (Rule - (= t5 (NamedMat "B")) - (name "(rewrite (MMul A (Id n)) A)") + (= t5 (NamedMat "A")) + (name "(rewrite (MMul (Id n) A) A)") (premises (Rule (= t5 t5) @@ -145,13 +145,13 @@ expression: proof_snapshot t9 t10)) (substitution - (n (NamedDim "m")) - (@rewrite_var__11 t5) - (A (NamedMat "B")))) - 1) + (@rewrite_var__10 t5) + (A (NamedMat "A")) + (n (NamedDim "n")))) + 0) (Rule - (= t4 (NamedMat "A")) - (name "(rewrite (MMul (Id n) A) A)") + (= t4 (NamedMat "B")) + (name "(rewrite (MMul A (Id n)) A)") (premises (Rule (= t4 t4) @@ -159,6 +159,6 @@ expression: proof_snapshot "(rewrite (MMul (Kron A B) (Kron C D)) (Kron (MMul A C) (MMul B D)) :when ((= (ncols A) (nrows C)) (= (ncols B) (nrows D))))") t9 t10)) - (substitution (@rewrite_var__10 t4) (A (NamedMat "A")) (n (NamedDim "n")))) - 0)) + (substitution (n (NamedDim "m")) (@rewrite_var__11 t4) (A (NamedMat "B")))) + 1)) (Trans prop0 prf0 (Sym (= t3 t2) prf0)) diff --git a/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap b/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap index c9786285..52a7576a 100644 --- a/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap @@ -27,4 +27,4 @@ expression: proof_snapshot 0) 0) 0)) - (substitution (@rewrite_var__1 t1) (@v80 (vec-of (vec-of (b)))) (@v79 (b)))) + (substitution (@rewrite_var__1 t1) (@v83 (b)) (@v84 (vec-of (vec-of (b)))))) diff --git a/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap b/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap index b12cb48a..4ce77fe5 100644 --- a/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap @@ -257,5 +257,5 @@ expression: proof_snapshot (t1 (Type "struct s*"))))) (Fiat (= () ()))) (substitution - (@v3842 (expr-points-to (Expr "u"))) - (@v3843 (expr-points-to (Expr "sp"))))) + (@v4154 (expr-points-to (Expr "sp"))) + (@v4153 (expr-points-to (Expr "u"))))) diff --git a/egglog/tests/snapshots/files__proofs__until_proof_testing.snap b/egglog/tests/snapshots/files__proofs__until_proof_testing.snap index e4408b9a..37fb5045 100644 --- a/egglog/tests/snapshots/files__proofs__until_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__until_proof_testing.snap @@ -25,9 +25,9 @@ expression: proof_snapshot (premises (Congr (= t1 (g* (IConst) (IConst))) - (Congr (= t1 (g* t0 (IConst))) (Fiat (= t1 t1)) prf0 1) + (Congr (= t1 (g* (IConst) t0)) (Fiat (= t1 t1)) prf0 0) prf0 - 0)) + 1)) (substitution (@rewrite_var__2 t1) (a (IConst)))) (Fiat (= () ())) (Fiat (= () ())) From e3f69e16ec52373594694ccd634c9b08716d934b Mon Sep 17 00:00:00 2001 From: Oliver Flatt Date: Mon, 27 Jul 2026 18:03:53 +0000 Subject: [PATCH 2/5] Document the rebuild index and test that it covers every view row proof_encoding.md's rebuilding section now shows the index-driven rule that replaced the per-column eq-sort fan-out, plus a CHANGELOG entry. rebuild_index_covers_every_view_row asserts the invariant the rule depends on: a view row missing its index entries is unreachable from the @UF-driven rebuild and silently stays stale. Verified non-vacuous by reverting the instrument_construct_into fix, which the test then catches. Co-Authored-By: Claude Opus 5 --- egglog/CHANGELOG.md | 1 + egglog/src/proofs/proof_encoding.md | 52 +++++++++++++++++++---- egglog/src/proofs/proof_tests.rs | 65 +++++++++++++++++++++++++++++ 3 files changed, 111 insertions(+), 7 deletions(-) diff --git a/egglog/CHANGELOG.md b/egglog/CHANGELOG.md index 24dddf61..1a62afb4 100644 --- a/egglog/CHANGELOG.md +++ b/egglog/CHANGELOG.md @@ -2,6 +2,7 @@ ## [Unreleased] - ReleaseDate +- In the term/proof encoding, rebuild a view's eq-sort children with a single `UF`-driven rule instead of a per-column fan-out. Each view gets one hidden `:merge` term→row index per distinct child eq-sort, and one rule — a `UF` edge joined against that index — re-canonicalizes the whole row with a `uf_canon` primitive, mirroring how a native rebuild iterates the e-nodes referencing a changed e-class rather than matching the view once per column. `uf_canon` is the generic view-column read over the two-output `UF_` table, so every backend services it against its own storage. - Add a `(begin *)` command and a `(let (begin * ))` form that run a block of actions once, immediately, with a shared *local* scope (`let`s bind local variables, not global functions); `let`-begin additionally binds the global `` to the block's trailing value. In the term/proof encoding, each top-level action's minted temporaries — and the shared `let`s introduced by the common-subexpression prepass — now run inside one such block instead of as separate top-level `let`s, so a temporary no longer becomes its own global function/table. This removes the per-proof-node table blow-up that made building a large static graph under the encoding slow (dominant cost on graphs with many top-level terms). A *user-written* `begin` block is reported unsupported under the term/proof encoding for now (proof checking models top-level actions individually, so a block's local bindings have no checkable representation); the encoding's own generated blocks are unaffected. - Common-subexpression prepass for the term/proof encoding (`ast::cse`, run over the program before encoding): within an action scope, a constructor application occurring more than once is bound to a shared `let` and its occurrences rewritten to that variable, so it is interned once. A top-level action that gains shared `let`s becomes a `begin` block, so they stay local rather than adding a global table per hoisted subterm. - In the term/proof encoding, when a `union` operand is a freshly-built constructor term, build it directly into the other operand's e-class instead of minting a fresh id and unioning it away: a plain view `set` points the constructor's children at the other operand's (target) e-class, and the view's congruence `:merge` handles the case where the term already exists. This reuses ids and drops the corresponding `@UF` rows (union-heavy workloads run substantially faster and use less memory in both term and proof mode). In proof mode the view row carries the equality proof `target = f(children)`, composed from the union's rule justification and a `Congr` chain over canonicalized children, with the built-in operand's term kept on its own id so proof reconstruction stays unambiguous. diff --git a/egglog/src/proofs/proof_encoding.md b/egglog/src/proofs/proof_encoding.md index 8a09329a..c359cedb 100644 --- a/egglog/src/proofs/proof_encoding.md +++ b/egglog/src/proofs/proof_encoding.md @@ -486,13 +486,51 @@ with the leader (the view's `:merge` keeps the smaller). :ruleset rebuilding :name "rebuild_rule" :internal-include-subsumed) ``` -A rule for an **eq-sort child** instead re-keys the row: it `set`s the view at the -canonicalized children and deletes the stale row (proof mode composes a `Congr` at -that child index). Because `UF_` has no row for a canonical term -(identity-on-miss), a column already at its leader simply does not match, so no -self-loops or default lookups are needed. Subsumption markers -(`to_subsume_`) are likewise re-keyed to their leaders so a subsumed -row stays subsumed after its children move. +The **eq-sort children** are handled by a single rule per distinct child sort, +driven by a `UF_` edge rather than by matching the view. Each view gets one +hidden *rebuild index* per distinct child eq-sort, + +```text +(function MulIndex_Math (Math Math Math) Unit :merge old :internal-hidden :unextractable) +``` + +holding, for every view row, one entry per `Math` child: that child first, then +the row's whole key. Leading with the child makes "which rows mention this term" +a key-prefix lookup — the same access pattern a native rebuild uses when it walks +the e-nodes referencing a changed e-class. The rule joins a `UF_Math` edge +against the index to reach those rows: + +```text +(rule ((= (values leader plf) (UF_Math follower)) + (!= follower leader) + (MulIndex_Math follower c0 c1) + (= (values e pe) (MulView c0 c1))) + ((let c0_canon_ (UF_Math_canon c0 c0)) + (let c1_canon_ (UF_Math_canon c1 c1)) + (set (MulView c0_canon_ c1_canon_) (values e ())) + (set (MulIndex_Math c0_canon_ c0_canon_ c1_canon_) ()) + (set (MulIndex_Math c1_canon_ c0_canon_ c1_canon_) ()) + (delete (MulView c0 c1)) + (delete (MulIndex_Math c0 c0 c1)) + (delete (MulIndex_Math c1 c0 c1))) + :ruleset rebuilding :unsafe-seminaive :name "rebuild_rule" :internal-include-subsumed) +``` + +`UF__canon` is the row's leader column read by term, with the term itself +as the fallback — so a child already at its leader canonicalizes to itself. The +action re-canonicalizes *every* eq-sort child, so one firing fixes the whole row +instead of one column of it; in proof mode it folds one `Congr` per child onto +the row proof, and the steps for children that did not move are reflexive and +collapse in the proof simplifier. Reading `UF_` in the action is what makes +the rule `:unsafe-seminaive`; the driving `UF_` delta in the body is what +makes that read sound. + +The index is maintained wherever a view row is written or deleted, so it tracks +the view exactly. Container children are not indexed — they have no `UF_` +row to drive a lookup — and keep the per-column `:naive` rule below. Subsumption +markers (`to_subsume_`) are re-keyed to their leaders by their own +per-column rules, so a subsumed row stays subsumed after its children move; +subsuming a view row keeps it, so it leaves the index untouched. # Globals diff --git a/egglog/src/proofs/proof_tests.rs b/egglog/src/proofs/proof_tests.rs index bce43ac5..a372d729 100644 --- a/egglog/src/proofs/proof_tests.rs +++ b/egglog/src/proofs/proof_tests.rs @@ -71,6 +71,71 @@ mod tests { } } + /// Every view row must carry its rebuild-index entries. The single + /// `@UF`-driven rebuild rule reaches the rows mentioning a term only through + /// that index, so a row missing its entries is never re-canonicalized and + /// silently stays stale. + #[test] + fn rebuild_index_covers_every_view_row() { + use crate::util::HashSet; + use egglog_backend_trait::BackendExt; + + let files = [ + "tests/calc.egg", + "tests/integer_math.egg", + "tests/web-demo/eqsat-basic.egg", + "tests/web-demo/unification-points-to.egg", + ]; + + for file in files { + let source = std::fs::read_to_string(file) + .unwrap_or_else(|e| panic!("couldn't read {file}: {e}")); + let mut egraph = crate::EGraph::new_with_proofs(); + egraph + .parse_and_run_program(Some(file.to_string()), &source) + .unwrap_or_else(|e| panic!("{file} failed: {e}")); + + let view_index = egraph.proof_state.view_index.clone(); + for (fname, indexes) in &view_index { + let Some(view_name) = egraph.proof_state.proof_names.view_name.get(fname) else { + continue; + }; + let Some(view) = egraph.functions.get(view_name) else { + continue; + }; + let (view_id, n_keys) = (view.backend_id, view.schema.input.len()); + let mut keys = Vec::new(); + egraph.backend.for_each_while(view_id, |row| { + keys.push(row.vals[..n_keys].to_vec()); + true + }); + + for vi in indexes { + let Some(index) = egraph.functions.get(&vi.name) else { + continue; + }; + let mut entries = HashSet::default(); + egraph.backend.for_each_while(index.backend_id, |row| { + entries.insert(row.vals[..n_keys + 1].to_vec()); + true + }); + for key in &keys { + for &pos in &vi.positions { + let mut want = vec![key[pos]]; + want.extend_from_slice(key); + assert!( + entries.contains(&want), + "{file}: {} row {key:?} is missing its {} entry at position {pos}", + view_name, + vi.name, + ); + } + } + } + } + } + } + /// A user rule marked `:naive` must stay `:naive` through proof encoding; /// dropping it would silently switch the rule to seminaive evaluation. #[test] From e325fc86cfbaba640c274bf7b363c584dc509211 Mon Sep 17 00:00:00 2001 From: Oliver Flatt Date: Mon, 27 Jul 2026 18:35:30 +0000 Subject: [PATCH 3/5] Read the rebuild row's value tuple on the RHS, not in the rule body MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The index atom already binds the view row's key, so joining the view for its (eclass, proof) was a third body atom the search had to plan. Read those columns in the action instead, leaving the body as the @UF delta plus the index lookup. The read is fallback-free: Backend::register_view_column_lookup returns None on an absent key, and ExternalFunction::invoke halts the calling rule when no value comes back — the same outcome as a body join that fails to match. The existing register_view_column_read keeps its fallback for set-if-empty's connector proof, where the caller does have a meaningful default. The DD interpreter cannot abandon an action mid-flight, so it reports an absent key instead of inventing a value; the index witnesses the row, so it never fires. Co-Authored-By: Claude Opus 5 --- egglog-experimental/dd/src/interpret.rs | 17 +++-- egglog-experimental/dd/src/lib.rs | 71 +++++++++++++------ .../egglog-backend-trait/src/backend_impl.rs | 9 +++ egglog/egglog-backend-trait/src/lib.rs | 16 +++++ egglog/egglog-bridge/src/lib.rs | 20 ++++++ egglog/src/proofs/proof_encoding_rebuild.rs | 21 ++++-- egglog/src/proofs/proof_fresh.rs | 45 +++++++++++- 7 files changed, 168 insertions(+), 31 deletions(-) diff --git a/egglog-experimental/dd/src/interpret.rs b/egglog-experimental/dd/src/interpret.rs index 00831dda..bca4fe74 100644 --- a/egglog-experimental/dd/src/interpret.rs +++ b/egglog-experimental/dd/src/interpret.rs @@ -690,11 +690,18 @@ fn view_column_read_apply( .get(&op.view_name) .ok_or_else(|| anyhow!("view-column read view `{}` is not registered", op.view_name))?; let keys = &args[..op.n_keys]; - let fallback = args[op.n_keys]; - Ok(match lookup_existing(eg, view, keys, index) { - Some(values) => Value::new(values[op.col_idx]), - None => fallback, - }) + match lookup_existing(eg, view, keys, index) { + Some(values) => Ok(Value::new(values[op.col_idx])), + None if op.has_fallback => Ok(args[op.n_keys]), + // A fallback-free lookup halts the rule on the reference backend. This + // interpreter has no way to abandon one action mid-flight, so report it + // instead of inventing a value; callers only use it where another table + // already witnesses the row. + None => Err(anyhow!( + "view-column lookup on `{}` found no row for its key", + op.view_name + )), + } } #[cfg(test)] diff --git a/egglog-experimental/dd/src/lib.rs b/egglog-experimental/dd/src/lib.rs index d91c7d07..994bf3f1 100644 --- a/egglog-experimental/dd/src/lib.rs +++ b/egglog-experimental/dd/src/lib.rs @@ -197,6 +197,10 @@ pub(crate) struct ViewOp { pub(crate) out_arity: usize, /// Output column to read (view-column read only). pub(crate) col_idx: usize, + /// Whether the reader takes a trailing fallback argument used when the key is + /// absent. A fallback-free reader has no answer for an absent key, so the DD + /// path reports it rather than inventing one. + pub(crate) has_fallback: bool, } #[derive(Clone, Copy, Debug, PartialEq, Eq)] @@ -232,6 +236,34 @@ impl Default for EGraph { } impl EGraph { + /// Register a view-column reader the DD interpreter intercepts (the db-path + /// external function only panics). `has_fallback` selects the reader's + /// absent-key behavior; see [`ViewOp::has_fallback`]. + fn register_view_column_op( + &mut self, + view_name: String, + n_keys: usize, + col_idx: usize, + has_fallback: bool, + ) -> ExternalFunctionId { + let id = Backend::new_panic( + self, + format!("view-column read for `{view_name}` reached the db path; DD must intercept it"), + ); + self.view_column_read_ops.insert( + id, + ViewOp { + view_name, + n_keys, + // A view-column reader never inserts, so out_arity is unused. + out_arity: 0, + col_idx, + has_fallback, + }, + ); + id + } + /// Construct a fresh Differential Dataflow backend. Rule bodies run on the /// in-process DD join; body primitives and head actions are applied /// host-side into the mirror. Pass this backend to @@ -1042,11 +1074,14 @@ impl<'a> MergeTransaction<'a> { let view = self.view_op_table(op)?; let n_keys = op.n_keys; let key: Row = args[..n_keys].into(); - let fallback = args[n_keys]; - Ok(match self.current_row(view, n_keys, &key) { - Some(current) => current.values[op.col_idx], - None => fallback, - }) + match self.current_row(view, n_keys, &key) { + Some(current) => Ok(current.values[op.col_idx]), + None if op.has_fallback => Ok(args[n_keys]), + None => Err(anyhow!( + "view-column lookup on `{}` found no row for its key", + op.view_name + )), + } } fn view_op_table(&self, op: &ViewOp) -> Result { @@ -2620,6 +2655,7 @@ impl Backend for EGraph { n_keys, out_arity, col_idx: 0, + has_fallback: false, }, ); id @@ -2631,21 +2667,16 @@ impl Backend for EGraph { n_keys: usize, col_idx: usize, ) -> ExternalFunctionId { - let id = Backend::new_panic( - self, - format!("view-column read for `{view_name}` reached the db path; DD must intercept it"), - ); - self.view_column_read_ops.insert( - id, - ViewOp { - view_name, - n_keys, - // A view-column reader never inserts, so out_arity is unused. - out_arity: 0, - col_idx, - }, - ); - id + self.register_view_column_op(view_name, n_keys, col_idx, true) + } + + fn register_view_column_lookup( + &mut self, + view_name: String, + n_keys: usize, + col_idx: usize, + ) -> ExternalFunctionId { + self.register_view_column_op(view_name, n_keys, col_idx, false) } // -- capability flags --------------------------------------------------- diff --git a/egglog/egglog-backend-trait/src/backend_impl.rs b/egglog/egglog-backend-trait/src/backend_impl.rs index 8e1fe862..b1e16c5e 100644 --- a/egglog/egglog-backend-trait/src/backend_impl.rs +++ b/egglog/egglog-backend-trait/src/backend_impl.rs @@ -252,6 +252,15 @@ impl Backend for EGraph { EGraph::register_view_column_read(self, view_name, n_keys, col_idx) } + fn register_view_column_lookup( + &mut self, + view_name: String, + n_keys: usize, + col_idx: usize, + ) -> ExternalFunctionId { + EGraph::register_view_column_lookup(self, view_name, n_keys, col_idx) + } + fn set_report_level(&mut self, level: ReportLevel) { EGraph::set_report_level(self, level); } diff --git a/egglog/egglog-backend-trait/src/lib.rs b/egglog/egglog-backend-trait/src/lib.rs index c5d7bb50..b4eb8036 100644 --- a/egglog/egglog-backend-trait/src/lib.rs +++ b/egglog/egglog-backend-trait/src/lib.rs @@ -427,6 +427,22 @@ pub trait Backend: Send + Sync { )) } + /// Like [`Backend::register_view_column_read`], but with no fallback: + /// `(keys) -> column`, and an absent key halts the rule that called it. Lets a + /// rule read a row it has already established exists — via another table that + /// tracks the view — without joining the view itself, and without inventing a + /// value for a row that is not there. The default registers a panic. + fn register_view_column_lookup( + &mut self, + view_name: String, + _n_keys: usize, + _col_idx: usize, + ) -> ExternalFunctionId { + self.new_panic(format!( + "this backend does not support view-column lookups for view `{view_name}`" + )) + } + // -- diagnostics -------------------------------------------------------- /// Set the verbosity of the per-iteration timing report. diff --git a/egglog/egglog-bridge/src/lib.rs b/egglog/egglog-bridge/src/lib.rs index 31542e5c..e0b6df1d 100644 --- a/egglog/egglog-bridge/src/lib.rs +++ b/egglog/egglog-bridge/src/lib.rs @@ -384,6 +384,26 @@ impl EGraph { ))) } + /// Fallback-free view-column read: `(keys) -> column`. Returning `None` on an + /// absent key halts the calling rule, so a caller that cannot name a + /// meaningful default simply does nothing for that row. + pub fn register_view_column_lookup( + &mut self, + view_name: String, + n_keys: usize, + col_idx: usize, + ) -> ExternalFunctionId { + let registry = self.action_registry.clone(); + self.register_external_func(Box::new(make_external_func( + move |state: &mut ExecutionState, args: &[Value]| { + let registry = registry.read().unwrap(); + let action = registry.lookup_table(&view_name)?.clone(); + let vals = action.lookup_values(state, &args[..n_keys])?; + Some(vals[col_idx]) + }, + ))) + } + pub fn free_external_func(&mut self, func: ExternalFunctionId) { // A cached panic with more than one reference is kept alive (just // decrement); one at its last reference — or any func that is not a diff --git a/egglog/src/proofs/proof_encoding_rebuild.rs b/egglog/src/proofs/proof_encoding_rebuild.rs index edfa1b6c..c80020bd 100644 --- a/egglog/src/proofs/proof_encoding_rebuild.rs +++ b/egglog/src/proofs/proof_encoding_rebuild.rs @@ -248,15 +248,25 @@ impl ProofInstrumentor<'_> { let keys_str = format!("{}", ListDisplay(key_vars, " ")); let index_deletes = self.view_index_deletes(&fdecl.name, key_vars); - // Body: an `@UF_` edge on the referenced term, the index entry naming a - // row that mentions it, and that row's value tuple. + // Body: an `@UF_` edge on the referenced term, and the index entry + // naming a row that mentions it. The index already binds the row's key, so + // the row's value tuple is read in the action rather than joined here — + // one fewer atom to search. Those reads are fallback-free: if the row is + // gone they halt the rule, exactly as a body join would fail to match. let follower = self.fresh_var(); let leader = self.fresh_var(); let leader_pf = self.fresh_var(); let uf_name = self.uf_name(&vi.sort_name); let uf_atom = format!("(= (values {leader} {leader_pf}) ({uf_name} {follower}))"); let index_atom = format!("({} {follower} {keys_str})", vi.name); - let (query_view, value_var, view_prf) = self.query_fd_view(&fdecl.name, key_vars); + let value_var = self.fresh_var(); + let view_prf = self.fresh_var(); + let mut row_reads = Stmts::new(); + let col = |i| crate::proofs::proof_fresh::view_col_prim_name(&view_name, i); + row_reads.push(format!("(let {value_var} ({} {keys_str}))", col(0))); + if proofs { + row_reads.push(format!("(let {view_prf} ({} {keys_str}))", col(1))); + } // Action: canonicalize every eq-sort key column, folding its congruence // step onto the row proof. Other columns carry over unchanged. @@ -295,9 +305,10 @@ impl ProofInstrumentor<'_> { } let pf_arg = if proofs { proof_acc } else { "()".to_string() }; let updated_view = self.update_fd_view(&fdecl.name, &updated, &value_var, &pf_arg); - let facts = format!("{uf_atom}\n(!= {follower} {leader})\n{index_atom}\n{query_view}"); + let facts = format!("{uf_atom}\n(!= {follower} {leader})\n{index_atom}"); let actions = format!( - "{}\n{updated_view}\n(delete ({view_name} {keys_str}))\n{index_deletes}", + "{}\n{}\n{updated_view}\n(delete ({view_name} {keys_str}))\n{index_deletes}", + row_reads.join("\n "), lets.join("\n ") ); self.rebuild_rule(&facts, &actions, RebuildEval::UnsafeSeminaive) diff --git a/egglog/src/proofs/proof_fresh.rs b/egglog/src/proofs/proof_fresh.rs index 7bc9d9a5..e9729691 100644 --- a/egglog/src/proofs/proof_fresh.rs +++ b/egglog/src/proofs/proof_fresh.rs @@ -34,6 +34,13 @@ pub(crate) fn view_proof_prim_name(view_name: &str) -> String { format!("view-proof-{view_name}") } +/// Deterministic name of an FD view's fallback-free reader for output column +/// `col`: `(keys) -> column`, halting the calling rule when the key is absent. +/// See [`set_if_empty_prim_name`] for why the prefix carries no internal marker. +pub(crate) fn view_col_prim_name(view_name: &str, col: usize) -> String { + format!("view-col{col}-{view_name}") +} + /// Register an FD view's `set-if-empty` primitive and (in proof mode) its /// proof-column reader, so the encoding can canonicalize a freshly-built term /// to the view's canonical e-class at insertion time. `out_sorts` is the view's @@ -65,7 +72,7 @@ pub(crate) fn register_set_if_empty( if out_sorts.len() >= 2 { let view_proof = ViewProof { name: view_proof_prim_name(view_name), - key_sorts, + key_sorts: key_sorts.clone(), proof_sort: out_sorts[1].clone(), }; let name = view_name.to_string(); @@ -77,6 +84,42 @@ pub(crate) fn register_set_if_empty( move |backend, _| backend.register_view_column_read(name.clone(), n_keys, 1), ); } + + // Fallback-free readers, one per output column, for a rule that has already + // established the row exists and only needs its values (see + // `Backend::register_view_column_lookup`). + for (col, out) in out_sorts.iter().enumerate() { + let view_col = ViewCol { + name: view_col_prim_name(view_name, col), + key_sorts: key_sorts.clone(), + out_sort: out.clone(), + }; + let name = view_name.to_string(); + eg.add_backend_op_primitive(view_col, WriteState::valid_contexts(), move |backend, _| { + backend.register_view_column_lookup(name.clone(), n_keys, col) + }); + } +} + +/// Reads one output column of an FD view by key, with no fallback: an absent key +/// halts the calling rule (see [`view_col_prim_name`]). +#[derive(Clone)] +struct ViewCol { + name: String, + key_sorts: Vec, + out_sort: ArcSort, +} + +impl Primitive for ViewCol { + fn name(&self) -> &str { + &self.name + } + fn get_type_constraints(&self, span: &Span) -> Box { + // (keys…) -> column + let mut sig = self.key_sorts.clone(); + sig.push(self.out_sort.clone()); + SimpleTypeConstraint::new(&self.name, sig, span.clone()).into_box() + } } /// `set-if-empty`: get-or-insert-with-default on an FD view. Looks up From 811a3ff6c1f706d914dd9093b2b1b041f7dad1da Mon Sep 17 00:00:00 2001 From: Oliver Flatt Date: Mon, 27 Jul 2026 18:47:56 +0000 Subject: [PATCH 4/5] Drive the rebuild from a known child position instead of uf_canon Binding the moved term at a known key position in the index atom makes its leader a static substitution, so the action re-keys the row and composes one Congr at that position from the edge proof the body already bound. This drops the whole-row recanon: no uf_canon read per eq-sort child, no reflexive Proof lookup per child, and no Congr mint for children that did not move (which the simplifier only discarded later anyway). A row with k stale children now takes k firings, as it did before this branch. Proof derivations move back to the baseline's shapes, so most of the regenerated snapshots revert; the 11 that remain differ only by fresh-var renumbering. Co-Authored-By: Claude Opus 5 --- egglog/src/proofs/proof_encoding_rebuild.rs | 119 ++++++++---------- .../files__proofs__array_proof_testing.snap | 110 ++++++++-------- .../files__proofs__calc_proof_testing.snap | 32 ++--- ...es__proofs__combinators_proof_testing.snap | 114 +++++++++-------- ...roofs__container_proofs_proof_testing.snap | 16 +-- ...ontainer_reorder_proofs_proof_testing.snap | 20 +-- ...ontainer_output_rebuild_proof_testing.snap | 4 +- ...oofs__eqsat_basic_proof_proof_testing.snap | 63 +++++----- ...es__proofs__eqsat_basic_proof_testing.snap | 63 +++++----- ...ofs__filter_or_bool_neq_proof_testing.snap | 6 +- ...s__proofs__intersection_proof_testing.snap | 2 +- .../files__proofs__matrix_proof_testing.snap | 28 ++--- ...ainer_dirty_propagation_proof_testing.snap | 2 +- ...__unification_points_to_proof_testing.snap | 4 +- .../files__proofs__until_proof_testing.snap | 4 +- 15 files changed, 280 insertions(+), 307 deletions(-) diff --git a/egglog/src/proofs/proof_encoding_rebuild.rs b/egglog/src/proofs/proof_encoding_rebuild.rs index c80020bd..9a381f1c 100644 --- a/egglog/src/proofs/proof_encoding_rebuild.rs +++ b/egglog/src/proofs/proof_encoding_rebuild.rs @@ -134,7 +134,9 @@ impl ProofInstrumentor<'_> { .cloned() .unwrap_or_default(); for vi in &indexes { - rules.push_str(&self.eq_sort_rebuild_rule(fdecl, &key_vars, &types, vi)); + for pos in vi.positions.clone() { + rules.push_str(&self.eq_sort_rebuild_rule(fdecl, &key_vars, vi, pos)); + } } // FD view value column (see [`Self::fd_value_rebuild_rule`]). A // constructor/global's value *is* its e-class; a custom function's @@ -225,93 +227,74 @@ impl ProofInstrumentor<'_> { self.rebuild_rule(&facts, &actions, RebuildEval::Naive) } - /// The single rule that canonicalizes every eq-sort child of a view row, for - /// the child sort `vi` indexes. + /// The rebuild rule for eq-sort child position `pos`, reached through `vi`'s + /// index. + /// + /// An `@UF_` edge on some term is joined against the index to find the rows + /// holding that term at `pos` — a key-prefix lookup, the same access pattern a + /// native rebuild uses when it walks the e-nodes referencing a changed + /// e-class, rather than matching the view once per row. Binding the moved term + /// at a known position makes its leader a static substitution, so the action + /// re-keys the row and (proof mode) composes one `@Congr` at `pos` from the + /// edge proof the body already bound — no per-child union-find reads and no + /// reflexive steps for children that did not move. /// - /// An `@UF_` edge on some term is joined against `vi`'s index to reach the - /// rows mentioning that term by key lookup — the same access pattern a native - /// rebuild uses when it walks the e-nodes referencing a changed e-class. The - /// action then re-canonicalizes *all* the row's eq-sort children with - /// `uf_canon`, so one firing fixes the whole row rather than one column of it. - /// In proof mode it folds one `@Congr` per eq-sort child onto the row proof; - /// the steps for children that did not move are reflexive and collapse in the - /// proof simplifier. + /// The row's value tuple is read in the action rather than joined in the body: + /// the index entry already binds the key, and the reads are fallback-free, so + /// a row that is gone halts the rule exactly as a failing body join would. fn eq_sort_rebuild_rule( &mut self, fdecl: &ResolvedFunctionDecl, key_vars: &[String], - types: &[ArcSort], vi: &ViewIndex, + pos: usize, ) -> String { let proofs = self.proofs_enabled(); let view_name = self.view_name(&fdecl.name); - let keys_str = format!("{}", ListDisplay(key_vars, " ")); - let index_deletes = self.view_index_deletes(&fdecl.name, key_vars); + let uf_name = self.uf_name(&vi.sort_name); - // Body: an `@UF_` edge on the referenced term, and the index entry - // naming a row that mentions it. The index already binds the row's key, so - // the row's value tuple is read in the action rather than joined here — - // one fewer atom to search. Those reads are fallback-free: if the row is - // gone they halt the rule, exactly as a body join would fail to match. + // The moved term occupies key position `pos`, so it is the same variable in + // the `@UF` edge and in the index entry. let follower = self.fresh_var(); let leader = self.fresh_var(); let leader_pf = self.fresh_var(); - let uf_name = self.uf_name(&vi.sort_name); + let mut keys = key_vars.to_vec(); + keys[pos] = follower.clone(); + let keys_str = format!("{}", ListDisplay(&keys, " ")); + let index_deletes = self.view_index_deletes(&fdecl.name, &keys); let uf_atom = format!("(= (values {leader} {leader_pf}) ({uf_name} {follower}))"); let index_atom = format!("({} {follower} {keys_str})", vi.name); + let value_var = self.fresh_var(); let view_prf = self.fresh_var(); - let mut row_reads = Stmts::new(); + let mut actions = Stmts::new(); let col = |i| crate::proofs::proof_fresh::view_col_prim_name(&view_name, i); - row_reads.push(format!("(let {value_var} ({} {keys_str}))", col(0))); - if proofs { - row_reads.push(format!("(let {view_prf} ({} {keys_str}))", col(1))); - } + actions.push(format!("(let {value_var} ({} {keys_str}))", col(0))); + let pf_arg = if proofs { + actions.push(format!("(let {view_prf} ({} {keys_str}))", col(1))); + let congr = self.proof_names().congr_constructor.clone(); + let proof_sort = self.proof_sort(); + self.mint( + &mut actions, + &congr, + &format!("{view_prf} {pos} {leader_pf}"), + &proof_sort, + ) + } else { + "()".to_string() + }; + let mut updated = keys.clone(); + updated[pos] = leader.clone(); + actions.push(self.update_fd_view(&fdecl.name, &updated, &value_var, &pf_arg)); + actions.push(format!("(delete ({view_name} {keys_str}))")); + actions.push(index_deletes); - // Action: canonicalize every eq-sort key column, folding its congruence - // step onto the row proof. Other columns carry over unchanged. - let mut lets = Stmts::new(); - let mut updated = key_vars.to_vec(); - let mut proof_acc = view_prf; - for j in 0..key_vars.len() { - if !types[j].is_eq_sort() || types[j].is_eq_container_sort() { - continue; - } - let canon = format!("c{j}_canon_"); - let cj = &key_vars[j]; - let uf_j = self.uf_name(types[j].name()); - let canon_prim = crate::proofs::proof_container_rebuild::uf_canon_prim_name(&uf_j); - // Fallback `cj`: a child with no `@UF` row is already a root. - lets.push(format!("(let {canon} ({canon_prim} {cj} {cj}))")); - if proofs { - let proof_prim = - crate::proofs::proof_container_rebuild::uf_canon_proof_prim_name(&uf_j); - let congr = self.proof_names().congr_constructor.clone(); - let proof_sort = self.proof_sort(); - // Fallback: the reflexive `cj = cj`, anchored when `cj` was built. - let term_proof = self.term_proof_name(types[j].name()); - let refl_pf = self.fresh_var(); - let step_pf = self.fresh_var(); - lets.push(format!("(let {refl_pf} ({term_proof} {cj}))")); - lets.push(format!("(let {step_pf} ({proof_prim} {cj} {refl_pf}))")); - proof_acc = self.mint( - &mut lets, - &congr, - &format!("{proof_acc} {j} {step_pf}"), - &proof_sort, - ); - } - updated[j] = canon; - } - let pf_arg = if proofs { proof_acc } else { "()".to_string() }; - let updated_view = self.update_fd_view(&fdecl.name, &updated, &value_var, &pf_arg); let facts = format!("{uf_atom}\n(!= {follower} {leader})\n{index_atom}"); - let actions = format!( - "{}\n{}\n{updated_view}\n(delete ({view_name} {keys_str}))\n{index_deletes}", - row_reads.join("\n "), - lets.join("\n ") - ); - self.rebuild_rule(&facts, &actions, RebuildEval::UnsafeSeminaive) + self.rebuild_rule( + &facts, + &actions.join("\n "), + RebuildEval::UnsafeSeminaive, + ) } /// One rule that canonicalizes an FD view's stale value column. diff --git a/egglog/tests/snapshots/files__proofs__array_proof_testing.snap b/egglog/tests/snapshots/files__proofs__array_proof_testing.snap index 9823228d..e82d28f3 100644 --- a/egglog/tests/snapshots/files__proofs__array_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__array_proof_testing.snap @@ -120,7 +120,7 @@ expression: proof_snapshot (Congr (= t9 (neq t0 t4)) (Congr - (= t9 (neq t0 t8)) + (= t9 (neq t2 t4)) (Rule (= t9 t9) (name @@ -130,16 +130,16 @@ expression: proof_snapshot )") (premises (Fiat (= t10 t10)) (Fiat (= t2 t2))) (substitution (z (Var "r1")) (e t2) (y (Var "r3")) (x (Var "r2")))) - prf0 - 0) - (Sym - (= t8 t4) - (Rule - (= t4 t8) - (name "(rewrite (add x y) (add y x))") - (premises (Fiat (= t4 t4))) - (substitution (@rewrite_var__2 t4) (x (Var "r1")) (y (Var "r3"))))) - 1)) + (Sym + (= t8 t4) + (Rule + (= t4 t8) + (name "(rewrite (add x y) (add y x))") + (premises (Fiat (= t4 t4))) + (substitution (@rewrite_var__2 t4) (x (Var "r1")) (y (Var "r3"))))) + 1) + prf0 + 0)) (substitution (mem (AVar "mem1")) (e1 t5) (e (Num 2)) (i1 t0) (i2 t4))) (let t0 (add (Num 1) (Var "r1"))) (let t1 (add (Num 1) t0)) @@ -205,24 +205,24 @@ expression: proof_snapshot (let t17 (add (Num 1) (Num -3))) (let prf1 (Rule - (= t17 (Num -2)) - (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") - (premises - (Rule - (= t17 t17) - (name "(rewrite (add (add x y) z) (add x (add y z)))") - (premises - (Congr - (= t2 (add t12 (Num -3))) - (Fiat (= t2 t2)) - prf0 - 0)) - (substitution - (z (Num -3)) - (y (Num 1)) - (@rewrite_var__3 t2) - (x t0)))) - (substitution (@rewrite_var__4 t17) (x 1) (y -3)))) + (= t17 (Num -2)) + (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") + (premises + (Rule + (= t17 t17) + (name "(rewrite (add (add x y) z) (add x (add y z)))") + (premises + (Congr + (= t2 (add t12 (Num -3))) + (Fiat (= t2 t2)) + prf0 + 0)) + (substitution + (z (Num -3)) + (y (Num 1)) + (@rewrite_var__3 t2) + (x t0)))) + (substitution (@rewrite_var__4 t17) (x 1) (y -3)))) (Rule (= t3 (Var "r1")) (name "(rewrite (add x (Num 0)) x)") @@ -243,37 +243,37 @@ expression: proof_snapshot (Congr (= t6 (add (Num 2) t17)) (Congr - (= t6 (add (Num 2) t5)) + (= t6 (add t4 t17)) (Rule (= t6 t6) (name "(rewrite (add (add x y) z) (add x (add y z)))") t15 t16) - (Rule - (= t4 (Num 2)) - (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") - (premises - (Rule - (= t4 t4) - (name "(rewrite (add (add x y) z) (add x (add y z)))") - t13 - t14)) - (substitution (@rewrite_var__4 t4) (x 1) (y 1))) - 0) - (Trans - (= t5 t17) - (Rule - (= t5 (Num -2)) - (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") - (premises - (Rule - (= t5 t5) - (name "(rewrite (add (add x y) z) (add x (add y z)))") - t8 - t10)) - (substitution (@rewrite_var__4 t5) (x -3) (y 1))) - (Sym (= (Num -2) t17) prf1)) - 1) + (Trans + (= t5 t17) + (Rule + (= t5 (Num -2)) + (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") + (premises + (Rule + (= t5 t5) + (name "(rewrite (add (add x y) z) (add x (add y z)))") + t8 + t10)) + (substitution (@rewrite_var__4 t5) (x -3) (y 1))) + (Sym (= (Num -2) t17) prf1)) + 1) + (Rule + (= t4 (Num 2)) + (name "(rewrite (add (Num x) (Num y)) (Num (+ x y)))") + (premises + (Rule + (= t4 t4) + (name "(rewrite (add (add x y) z) (add x (add y z)))") + t13 + t14)) + (substitution (@rewrite_var__4 t4) (x 1) (y 1))) + 0) prf1 1)) (substitution (@rewrite_var__4 t6) (x 2) (y -2))) diff --git a/egglog/tests/snapshots/files__proofs__calc_proof_testing.snap b/egglog/tests/snapshots/files__proofs__calc_proof_testing.snap index dde3990e..3fd74f44 100644 --- a/egglog/tests/snapshots/files__proofs__calc_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__calc_proof_testing.snap @@ -17,36 +17,26 @@ expression: proof_snapshot (b (g* (AConst) (AConst))) (@rewrite_var__ t1))) (let t0 (g* (inv (aConst)) (aConst))) -(let t1 (g* (g* (bConst) t0) (inv (bConst)))) -(let t2 (g* t0 (inv (bConst)))) -(let t3 (premises (Fiat (= t1 t1)))) -(let t4 (substitution (c (inv (bConst))) (a (bConst)) (b t0) (@rewrite_var__ t1))) +(let t1 (g* (bConst) t0)) +(let t2 (g* t1 (inv (bConst)))) (Congr - (= t1 (g* (bConst) (inv (bConst)))) + (= t2 (g* (bConst) (inv (bConst)))) + (Fiat (= t2 t2)) (Rule - (= t1 (g* (bConst) t2)) - (name "(birewrite (g* (g* a b) c) (g* a (g* b c)))=>") - t3 - t4) - (Rule - (= t2 (inv (bConst))) - (name "(rewrite (g* $I a) a)") + (= t1 (bConst)) + (name "(rewrite (g* a $I) a)") (premises (Congr - (= t2 (g* (IConst) (inv (bConst)))) - (Rule - (= t2 t2) - (name "(birewrite (g* (g* a b) c) (g* a (g* b c)))=>") - t3 - t4) + (= t1 (g* (bConst) (IConst))) + (Fiat (= t1 t1)) (Rule (= t0 (IConst)) (name "(rewrite (g* (inv a) a) $I)") (premises (Fiat (= t0 t0))) (substitution (@rewrite_var__4 t0) (a (aConst)))) - 0)) - (substitution (@rewrite_var__2 t2) (a (inv (bConst))))) - 1) + 1)) + (substitution (a (bConst)) (@rewrite_var__3 t1))) + 0) (let t0 (g* (bConst) (inv (bConst)))) (Rule (= t0 (IConst)) diff --git a/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap b/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap index 26c568e7..327e7679 100644 --- a/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap @@ -410,13 +410,13 @@ expression: proof_snapshot (v "x") (n 0))) (let t76 (cx (Comb (N 0)))) -(let t77 (CAbs "x" (Comb (Var "x")))) -(let t78 (CApp t77 (CFConst))) -(let t79 (CApp (CAbs "x" (CIfConst)) (CFConst))) +(let t77 (CApp (CAbs "x" (CIfConst)) (CFConst))) +(let t78 (CAbs "x" (Comb (Var "x")))) +(let t79 (CApp t78 (CFConst))) (let t80 (CApp (CApp (SConst) (CAbs "x" (CIfConst))) - t77)) + t78)) (let t81 (premises (Rule @@ -453,7 +453,7 @@ expression: proof_snapshot (cz (CFConst)) (cx (CAbs "x" (CIfConst))) (@rewrite_var__16 t64) - (cy t77))) + (cy t78))) (let t85 (premises (Congr @@ -545,21 +545,19 @@ expression: proof_snapshot (Congr (= t64 (CApp (CIfConst) (CFConst))) (Congr - (= t64 (CApp (CIfConst) t78)) + (= t64 (CApp t77 (CFConst))) (Rule - (= t64 (CApp t79 t78)) + (= t64 (CApp t77 t79)) (name "(rewrite (CApp (CApp (CApp $S cx) cy) cz) (CApp (CApp cx cz) (CApp cy cz)))") t83 t84) (Rule - (= t79 (CIfConst)) - (name "(rewrite (CApp (CApp $K cx) cy) cx)") + (= t79 (CFConst)) + (name "(rewrite (CApp $I cx) cx)") (premises (Congr - (= - t79 - (CApp (CApp (KConst) (CIfConst)) (CFConst))) + (= t79 (CApp (IConst) (CFConst))) (Rule (= t79 t79) (name @@ -567,65 +565,65 @@ expression: proof_snapshot t83 t84) (Rule - (= - (CAbs "x" (CIfConst)) - (CApp (KConst) (CIfConst))) - (name "(rewrite (CAbs v $CIf) (CApp $K $CIf))") + (= t78 (IConst)) + (name "(rewrite (CAbs v (CVar v)) $I)") (premises - (Rule - (= - (CAbs "x" (CIfConst)) - (CAbs "x" (CIfConst))) - (name - "(rewrite (CAbs v (CApp x y)) (CApp (CApp $S (CAbs v x)) (CAbs v y)))") - t81 - t82)) - (substitution - (@rewrite_var__7 (CAbs "x" (CIfConst))) - (v "x"))) + (Congr + (= t78 (CAbs "x" (CVar "x"))) + (Rule + (= t78 t78) + (name + "(rewrite (CAbs v (CApp x y)) (CApp (CApp $S (CAbs v x)) (CAbs v y)))") + t81 + t82) + (Rule + (= (Comb (Var "x")) (CVar "x")) + (name + "(rule ((= x (Var v))) + ((union (Comb x) (CVar v))) + )") + (premises (Fiat (= (Var "x") (Var "x")))) + (substitution (v "x") (x (Var "x")))) + 1)) + (substitution (@rewrite_var__2 t78) (v "x"))) 0)) - (substitution - (@rewrite_var__15 t79) - (cx (CIfConst)) - (cy (CFConst)))) - 0) + (substitution (@rewrite_var__14 t79) (cx (CFConst)))) + 1) (Rule - (= t78 (CFConst)) - (name "(rewrite (CApp $I cx) cx)") + (= t77 (CIfConst)) + (name "(rewrite (CApp (CApp $K cx) cy) cx)") (premises (Congr - (= t78 (CApp (IConst) (CFConst))) + (= t77 (CApp (CApp (KConst) (CIfConst)) (CFConst))) (Rule - (= t78 t78) + (= t77 t77) (name "(rewrite (CApp (CApp (CApp $S cx) cy) cz) (CApp (CApp cx cz) (CApp cy cz)))") t83 t84) (Rule - (= t77 (IConst)) - (name "(rewrite (CAbs v (CVar v)) $I)") + (= + (CAbs "x" (CIfConst)) + (CApp (KConst) (CIfConst))) + (name "(rewrite (CAbs v $CIf) (CApp $K $CIf))") (premises - (Congr - (= t77 (CAbs "x" (CVar "x"))) - (Rule - (= t77 t77) - (name - "(rewrite (CAbs v (CApp x y)) (CApp (CApp $S (CAbs v x)) (CAbs v y)))") - t81 - t82) - (Rule - (= (Comb (Var "x")) (CVar "x")) - (name - "(rule ((= x (Var v))) - ((union (Comb x) (CVar v))) - )") - (premises (Fiat (= (Var "x") (Var "x")))) - (substitution (v "x") (x (Var "x")))) - 1)) - (substitution (@rewrite_var__2 t77) (v "x"))) + (Rule + (= + (CAbs "x" (CIfConst)) + (CAbs "x" (CIfConst))) + (name + "(rewrite (CAbs v (CApp x y)) (CApp (CApp $S (CAbs v x)) (CAbs v y)))") + t81 + t82)) + (substitution + (@rewrite_var__7 (CAbs "x" (CIfConst))) + (v "x"))) 0)) - (substitution (@rewrite_var__14 t78) (cx (CFConst)))) - 1) + (substitution + (@rewrite_var__15 t77) + (cx (CIfConst)) + (cy (CFConst)))) + 0) 0) 0))) (let t86 diff --git a/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap b/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap index 364b6591..c3a89f99 100644 --- a/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap @@ -9,7 +9,7 @@ expression: proof_snapshot (= (@ExistsConstructor) (@ExistsConstructor)) (name "@prove_exists_rule") (premises prf0 (Fiat (= (Z) (Z))) prf0 (Eval) (Fiat (= t1 t1))) - (substitution (@v122 (S (Z))) (@v120 (S (Z))) (@v121 (Z)) (@v123 t0))) + (substitution (@v121 t0) (@v119 (Z)) (@v118 (S (Z))) (@v120 (S (Z))))) (let t0 (pair (Z) (S (Z)))) (let t1 (HasPair t0)) (Rule @@ -20,7 +20,7 @@ expression: proof_snapshot (Fiat (= (S (Z)) (S (Z)))) (Eval) (Fiat (= t1 t1))) - (substitution (@v282 t0) (@v280 (Z)) (@v281 (S (Z))))) + (substitution (@v278 (Z)) (@v279 (S (Z))) (@v280 t0))) (let t0 (vec-of (Z) (S (Z)))) (let t1 (HasVec t0)) (Rule @@ -31,7 +31,7 @@ expression: proof_snapshot (Fiat (= (S (Z)) (S (Z)))) (Eval) (Fiat (= t1 t1))) - (substitution (@v427 (S (Z))) (@v426 (Z)) (@v428 t0))) + (substitution (@v424 (Z)) (@v425 (S (Z))) (@v426 t0))) (let t0 (map-of (Z) (S (Z)))) (let t1 (HasMap t0)) (Rule @@ -42,7 +42,7 @@ expression: proof_snapshot (Fiat (= (S (Z)) (S (Z)))) (Eval) (Fiat (= t1 t1))) - (substitution (@v580 (S (Z))) (@v579 (Z)) (@v581 t0))) + (substitution (@v578 (S (Z))) (@v577 (Z)) (@v579 t0))) (let prf0 (Fiat (= (Z) (Z)))) (let t0 (multiset-of (S (Z)) (Z) (Z))) (let t1 (HasMS t0)) @@ -50,7 +50,7 @@ expression: proof_snapshot (= (@ExistsConstructor4) (@ExistsConstructor4)) (name "@prove_exists_rule4") (premises prf0 (Fiat (= (S (Z)) (S (Z)))) prf0 (Eval) (Fiat (= t1 t1))) - (substitution (@v725 (Z)) (@v726 (S (Z))) (@v728 t0) (@v727 (Z)))) + (substitution (@v725 (Z)) (@v726 t0) (@v724 (S (Z))) (@v723 (Z)))) (let t0 (vec-of (Z) (S (Z)))) (let t1 (HasVec t0)) (Rule @@ -94,7 +94,7 @@ expression: proof_snapshot ((MapGet w)) )") (premises (Fiat (= t1 t1)) (Fiat (= (Z) (Z))) (Fiat (= (S (Z)) (S (Z))))) - (substitution (m t0) (@v1091 (Z)) (w (S (Z))))) + (substitution (m t0) (@v1085 (Z)) (w (S (Z))))) (let t0 (multiset-of (S (Z)) (Z) (Z))) (let t1 (HasMS t0)) (Rule @@ -195,5 +195,5 @@ expression: proof_snapshot ((OutWrap w)) )") (premises (Fiat (= (HasElem (Z)) (HasElem (Z)))) (Eval) (Fiat (= t0 t0))) - (substitution (a (Z)) (@v2081 (vec-of (Z) (Z))) (w t0)))) - (substitution (@v2117 (Z)) (@v2116 (Z)) (@v2118 (vec-of (Z) (Z))))) + (substitution (a (Z)) (@v2068 (vec-of (Z) (Z))) (w t0)))) + (substitution (@v2104 (Z)) (@v2103 (Z)) (@v2105 (vec-of (Z) (Z))))) diff --git a/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap b/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap index 7c28b1a4..af4759dc 100644 --- a/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap @@ -100,7 +100,7 @@ expression: proof_snapshot (substitution (x (N 2)) (@rewrite_var__ (Id (N 2))))) 1)) 0)) - (substitution (@v1112 (N 1)) (@v1114 t3) (@v1113 (N 2)))) + (substitution (@v1112 (N 2)) (@v1111 (N 1)) (@v1113 t3))) (let t0 (Add (Num 51) (Num 52))) (let t1 (Add (Num 52) (Num 51))) (let t2 (premises (Fiat (= (Go) (Go))))) @@ -147,7 +147,7 @@ expression: proof_snapshot prf0 0) 0)) - (substitution (@v1176 t1) (@v1177 t5))) + (substitution (@v1176 t5) (@v1175 t1))) (let t0 (premises (Fiat (= (Go) (Go))))) (let prf0 (Rule @@ -249,7 +249,7 @@ expression: proof_snapshot (substitution (x (N 12)) (@rewrite_var__ (Id (N 12))))) 1)) 0)) - (substitution (@v1239 (N 11)) (@v1241 t3) (@v1240 (N 12)) (@v1238 (N 11)))) + (substitution (@v1239 (N 12)) (@v1240 t3) (@v1237 (N 11)) (@v1238 (N 11)))) (let t0 (premises (Fiat (= (Go) (Go))))) (let prf0 (Rule @@ -344,11 +344,11 @@ expression: proof_snapshot 0)) 0)) (substitution - (@v1316 t3) - (@v1312 (N 21)) - (@v1314 (N 22)) - (@v1315 (N 23)) - (@v1313 (N 23)))) + (@v1312 (N 23)) + (@v1314 (N 23)) + (@v1311 (N 21)) + (@v1315 t3) + (@v1313 (N 22)))) (let t0 (premises (Fiat (= (Go) (Go))))) (let prf0 (Rule @@ -418,7 +418,7 @@ expression: proof_snapshot prf1 1) 0)) - (substitution (@v1396 (N 31)) (@v1399 t3) (@v1397 (N 31)) (@v1398 (N 32)))) + (substitution (@v1396 (N 31)) (@v1395 (N 31)) (@v1397 (N 32)) (@v1398 t3))) (let t0 (premises (Fiat (= (Go) (Go))))) (let prf0 (Rule @@ -526,4 +526,4 @@ expression: proof_snapshot 0) 1) 0)) - (substitution (@v1473 t5) (@v1471 (N 42)) (@v1472 (N 41)) (@v1470 (N 41)))) + (substitution (@v1469 (N 41)) (@v1471 (N 41)) (@v1470 (N 42)) (@v1472 t5))) diff --git a/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap b/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap index f75d855e..fe1ff58c 100644 --- a/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap @@ -21,7 +21,7 @@ expression: proof_snapshot (Trans (= t0 t0) (Sym (= t0 t1) prf0) prf0) (Fiat (= (N 1) (N 1))) (Eval)) - (substitution (@v140 (N 1)) (@n (set-of (N 1))))) + (substitution (@n (set-of (N 1))) (@v138 (N 1)))) (let t0 (set-of (N 1) (N 3))) (let t1 (freer (N 0) t0)) (let t2 (freer (N 0) (set-of (N 1)))) @@ -49,4 +49,4 @@ expression: proof_snapshot (Fiat (= (N 1) (N 1))) (Fiat (= (N 3) (N 3))) (Eval)) - (substitution (@v240 (N 3)) (@v239 (N 1)) (@n1 t0))) + (substitution (@v237 (N 1)) (@v238 (N 3)) (@n1 t0))) diff --git a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap index 3fe9c1ee..7d68eaca 100644 --- a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap @@ -4,35 +4,34 @@ expression: proof_snapshot --- (let t0 (Mul (Num 2) (Add (Var "x") (Num 3)))) (let t1 (Mul (Num 2) (Var "x"))) -(let t2 (Add (Num 6) t1)) -(let t3 (Add t1 (Num 6))) -(let t4 (Mul (Num 2) (Num 3))) -(let t5 (premises (Fiat (= t0 t0)))) -(let t6 (substitution (@rewrite_var__1 t0) (a (Num 2)) (b (Var "x")) (c (Num 3)))) -(Trans - (= t0 t2) - (Congr - (= t0 t3) - (Rule - (= t0 (Add t1 t4)) - (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") - t5 - t6) - (Rule - (= t4 (Num 6)) - (name "(rewrite (Mul (Num a) (Num b)) (Num (* a b)))") - (premises - (Rule - (= t4 t4) - (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") - t5 - t6)) - (substitution (a 2) (b 3) (@rewrite_var__3 t4))) - 1) - (Sym - (= t3 t2) - (Rule - (= t2 t3) - (name "(rewrite (Add a b) (Add b a))") - (premises (Fiat (= t2 t2))) - (substitution (a (Num 6)) (b t1) (@rewrite_var__ t2))))) +(let t2 (Mul (Num 2) (Num 3))) +(let t3 (premises (Fiat (= t0 t0)))) +(let t4 + (substitution + (@rewrite_var__1 t0) + (a (Num 2)) + (b (Var "x")) + (c (Num 3)))) +(Congr + (= t0 (Add (Num 6) t1)) + (Rule + (= t0 (Add t2 t1)) + (name "(rewrite (Add a b) (Add b a))") + (premises + (Rule + (= t0 (Add t1 t2)) + (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") + t3 + t4)) + (substitution (a t1) (b t2) (@rewrite_var__ t0))) + (Rule + (= t2 (Num 6)) + (name "(rewrite (Mul (Num a) (Num b)) (Num (* a b)))") + (premises + (Rule + (= t2 t2) + (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") + t3 + t4)) + (substitution (a 2) (b 3) (@rewrite_var__3 t2))) + 0) diff --git a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap index 3fe9c1ee..7d68eaca 100644 --- a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap @@ -4,35 +4,34 @@ expression: proof_snapshot --- (let t0 (Mul (Num 2) (Add (Var "x") (Num 3)))) (let t1 (Mul (Num 2) (Var "x"))) -(let t2 (Add (Num 6) t1)) -(let t3 (Add t1 (Num 6))) -(let t4 (Mul (Num 2) (Num 3))) -(let t5 (premises (Fiat (= t0 t0)))) -(let t6 (substitution (@rewrite_var__1 t0) (a (Num 2)) (b (Var "x")) (c (Num 3)))) -(Trans - (= t0 t2) - (Congr - (= t0 t3) - (Rule - (= t0 (Add t1 t4)) - (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") - t5 - t6) - (Rule - (= t4 (Num 6)) - (name "(rewrite (Mul (Num a) (Num b)) (Num (* a b)))") - (premises - (Rule - (= t4 t4) - (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") - t5 - t6)) - (substitution (a 2) (b 3) (@rewrite_var__3 t4))) - 1) - (Sym - (= t3 t2) - (Rule - (= t2 t3) - (name "(rewrite (Add a b) (Add b a))") - (premises (Fiat (= t2 t2))) - (substitution (a (Num 6)) (b t1) (@rewrite_var__ t2))))) +(let t2 (Mul (Num 2) (Num 3))) +(let t3 (premises (Fiat (= t0 t0)))) +(let t4 + (substitution + (@rewrite_var__1 t0) + (a (Num 2)) + (b (Var "x")) + (c (Num 3)))) +(Congr + (= t0 (Add (Num 6) t1)) + (Rule + (= t0 (Add t2 t1)) + (name "(rewrite (Add a b) (Add b a))") + (premises + (Rule + (= t0 (Add t1 t2)) + (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") + t3 + t4)) + (substitution (a t1) (b t2) (@rewrite_var__ t0))) + (Rule + (= t2 (Num 6)) + (name "(rewrite (Mul (Num a) (Num b)) (Num (* a b)))") + (premises + (Rule + (= t2 t2) + (name "(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))") + t3 + t4)) + (substitution (a 2) (b 3) (@rewrite_var__3 t2))) + 0) diff --git a/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap b/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap index bf2f4e71..40116635 100644 --- a/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap @@ -23,4 +23,8 @@ expression: proof_snapshot (= (@ExistsConstructor16) (@ExistsConstructor16)) (name "@prove_exists_rule16") (premises prf0 (Fiat (= (Val 2) (Val 2))) prf0 prf0 (Fiat (= () ()))) - (substitution (@v998 (Val 1)) (@v996 (Val 2)) (@v997 (Val 1)) (@v995 (Val 1)))) + (substitution + (@v998 (Val 2)) + (@v997 (Val 1)) + (@v999 (Val 1)) + (@v1000 (Val 1)))) diff --git a/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap b/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap index a1db2740..63b11f13 100644 --- a/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap @@ -165,4 +165,4 @@ expression: proof_snapshot (x3 (Var "b3")) t2))) (Fiat (= () ()))) - (substitution (@v840 t0) (@v841 t3))) + (substitution (@v840 t3) (@v839 t0))) diff --git a/egglog/tests/snapshots/files__proofs__matrix_proof_testing.snap b/egglog/tests/snapshots/files__proofs__matrix_proof_testing.snap index be988f50..c6583938 100644 --- a/egglog/tests/snapshots/files__proofs__matrix_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__matrix_proof_testing.snap @@ -63,8 +63,8 @@ expression: proof_snapshot (let t2 (MMul t0 t1)) (let prop0 (= t2 t2)) (let t3 (Kron (NamedMat "A") (NamedMat "B"))) -(let t4 (MMul (NamedMat "B") (Id (NamedDim "m")))) -(let t5 (MMul (Id (NamedDim "n")) (NamedMat "A"))) +(let t4 (MMul (Id (NamedDim "n")) (NamedMat "A"))) +(let t5 (MMul (NamedMat "B") (Id (NamedDim "m")))) (let t6 (ncols (Id (NamedDim "n")))) (let t7 (A (Id (NamedDim "n")))) (let t8 (nrows (Id (NamedDim "m")))) @@ -127,16 +127,16 @@ expression: proof_snapshot (Congr (= t2 t3) (Congr - (= t2 (Kron (NamedMat "A") t4)) + (= t2 (Kron t4 (NamedMat "B"))) (Rule - (= t2 (Kron t5 t4)) + (= t2 (Kron t4 t5)) (name "(rewrite (MMul (Kron A B) (Kron C D)) (Kron (MMul A C) (MMul B D)) :when ((= (ncols A) (nrows C)) (= (ncols B) (nrows D))))") t9 t10) (Rule - (= t5 (NamedMat "A")) - (name "(rewrite (MMul (Id n) A) A)") + (= t5 (NamedMat "B")) + (name "(rewrite (MMul A (Id n)) A)") (premises (Rule (= t5 t5) @@ -145,13 +145,13 @@ expression: proof_snapshot t9 t10)) (substitution - (@rewrite_var__10 t5) - (A (NamedMat "A")) - (n (NamedDim "n")))) - 0) + (n (NamedDim "m")) + (@rewrite_var__11 t5) + (A (NamedMat "B")))) + 1) (Rule - (= t4 (NamedMat "B")) - (name "(rewrite (MMul A (Id n)) A)") + (= t4 (NamedMat "A")) + (name "(rewrite (MMul (Id n) A) A)") (premises (Rule (= t4 t4) @@ -159,6 +159,6 @@ expression: proof_snapshot "(rewrite (MMul (Kron A B) (Kron C D)) (Kron (MMul A C) (MMul B D)) :when ((= (ncols A) (nrows C)) (= (ncols B) (nrows D))))") t9 t10)) - (substitution (n (NamedDim "m")) (@rewrite_var__11 t4) (A (NamedMat "B")))) - 1)) + (substitution (@rewrite_var__10 t4) (A (NamedMat "A")) (n (NamedDim "n")))) + 0)) (Trans prop0 prf0 (Sym (= t3 t2) prf0)) diff --git a/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap b/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap index 52a7576a..3da9a16b 100644 --- a/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap @@ -27,4 +27,4 @@ expression: proof_snapshot 0) 0) 0)) - (substitution (@rewrite_var__1 t1) (@v83 (b)) (@v84 (vec-of (vec-of (b)))))) + (substitution (@v81 (b)) (@rewrite_var__1 t1) (@v82 (vec-of (vec-of (b)))))) diff --git a/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap b/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap index 4ce77fe5..10986590 100644 --- a/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap @@ -257,5 +257,5 @@ expression: proof_snapshot (t1 (Type "struct s*"))))) (Fiat (= () ()))) (substitution - (@v4154 (expr-points-to (Expr "sp"))) - (@v4153 (expr-points-to (Expr "u"))))) + (@v3936 (expr-points-to (Expr "u"))) + (@v3937 (expr-points-to (Expr "sp"))))) diff --git a/egglog/tests/snapshots/files__proofs__until_proof_testing.snap b/egglog/tests/snapshots/files__proofs__until_proof_testing.snap index 37fb5045..e4408b9a 100644 --- a/egglog/tests/snapshots/files__proofs__until_proof_testing.snap +++ b/egglog/tests/snapshots/files__proofs__until_proof_testing.snap @@ -25,9 +25,9 @@ expression: proof_snapshot (premises (Congr (= t1 (g* (IConst) (IConst))) - (Congr (= t1 (g* (IConst) t0)) (Fiat (= t1 t1)) prf0 0) + (Congr (= t1 (g* t0 (IConst))) (Fiat (= t1 t1)) prf0 1) prf0 - 1)) + 0)) (substitution (@rewrite_var__2 t1) (a (IConst)))) (Fiat (= () ())) (Fiat (= () ())) From ceb52d18bb01dabbc9358b6fbcfca495a8b5bbd1 Mon Sep 17 00:00:00 2001 From: Oliver Flatt Date: Mon, 27 Jul 2026 18:59:15 +0000 Subject: [PATCH 5/5] Drop the now-unused uf_canon primitives; document the final rule Driving the rebuild from a known child position removed every caller of uf_canon / uf_canon_proof, so stop registering two primitives per eq-sort. Co-Authored-By: Claude Opus 5 --- egglog/CHANGELOG.md | 3 +- egglog/src/proofs/proof_container_rebuild.rs | 99 -------------------- egglog/src/proofs/proof_encoding.md | 45 +++++---- egglog/src/typechecking.rs | 10 +- 4 files changed, 25 insertions(+), 132 deletions(-) diff --git a/egglog/CHANGELOG.md b/egglog/CHANGELOG.md index 1a62afb4..430f9541 100644 --- a/egglog/CHANGELOG.md +++ b/egglog/CHANGELOG.md @@ -2,7 +2,8 @@ ## [Unreleased] - ReleaseDate -- In the term/proof encoding, rebuild a view's eq-sort children with a single `UF`-driven rule instead of a per-column fan-out. Each view gets one hidden `:merge` term→row index per distinct child eq-sort, and one rule — a `UF` edge joined against that index — re-canonicalizes the whole row with a `uf_canon` primitive, mirroring how a native rebuild iterates the e-nodes referencing a changed e-class rather than matching the view once per column. `uf_canon` is the generic view-column read over the two-output `UF_` table, so every backend services it against its own storage. +- In the term/proof encoding, drive a view's eq-sort child rebuild from a `UF` edge instead of from the view. Each view gets one hidden `:merge` term→row index per distinct child eq-sort, and each indexed child position gets a rule joining a `UF` edge against that index — mirroring how a native rebuild iterates the e-nodes referencing a changed e-class rather than matching the view. The index entry already binds the row's key, so the row's value tuple is read on the rule's right-hand side rather than joined in its body. +- New backend SPI `Backend::register_view_column_lookup`: a fallback-free `(keys) -> column` read of an FD view. An absent key returns no value, which halts the calling rule — letting a rule read a row another table already witnesses without inventing a value when it is missing. - Add a `(begin *)` command and a `(let (begin * ))` form that run a block of actions once, immediately, with a shared *local* scope (`let`s bind local variables, not global functions); `let`-begin additionally binds the global `` to the block's trailing value. In the term/proof encoding, each top-level action's minted temporaries — and the shared `let`s introduced by the common-subexpression prepass — now run inside one such block instead of as separate top-level `let`s, so a temporary no longer becomes its own global function/table. This removes the per-proof-node table blow-up that made building a large static graph under the encoding slow (dominant cost on graphs with many top-level terms). A *user-written* `begin` block is reported unsupported under the term/proof encoding for now (proof checking models top-level actions individually, so a block's local bindings have no checkable representation); the encoding's own generated blocks are unaffected. - Common-subexpression prepass for the term/proof encoding (`ast::cse`, run over the program before encoding): within an action scope, a constructor application occurring more than once is bound to a shared `let` and its occurrences rewritten to that variable, so it is interned once. A top-level action that gains shared `let`s becomes a `begin` block, so they stay local rather than adding a global table per hoisted subterm. - In the term/proof encoding, when a `union` operand is a freshly-built constructor term, build it directly into the other operand's e-class instead of minting a fresh id and unioning it away: a plain view `set` points the constructor's children at the other operand's (target) e-class, and the view's congruence `:merge` handles the case where the term already exists. This reuses ids and drops the corresponding `@UF` rows (union-heavy workloads run substantially faster and use less memory in both term and proof mode). In proof mode the view row carries the equality proof `target = f(children)`, composed from the union's rule justification and a `Congr` chain over canonicalized children, with the built-in operand's term kept on its own id so proof reconstruction stays unambiguous. diff --git a/egglog/src/proofs/proof_container_rebuild.rs b/egglog/src/proofs/proof_container_rebuild.rs index 183a33c3..263c48fd 100644 --- a/egglog/src/proofs/proof_container_rebuild.rs +++ b/egglog/src/proofs/proof_container_rebuild.rs @@ -7,10 +7,6 @@ //! proof mode, prove the rebuild). Also holds the encoder-side spec bookkeeping //! ([`ProofInstrumentor::build_container_rebuild_spec`] and the primitive-name //! lookups). -//! -//! The eq-sort counterparts `uf_canon` / `uf_canon_proof` ([`register_uf_canon`]) -//! live here too: they canonicalize one eq-sort term against its `@UF` table, -//! letting the rebuild rules canonicalize a whole row in their action. use super::proof_encoding::ProofInstrumentor; use crate::exec_state::{Internal, RegistrySealed}; @@ -35,101 +31,6 @@ fn mint_proof_row( out } -/// Name of an eq-sort's `uf_canon` primitive, derived from its `@UF_` table -/// name. Both the encoder and the typechecker compute it the same way, so the -/// desugared program needs no extra annotation to find it. -pub(crate) fn uf_canon_prim_name(uf_name: &str) -> String { - format!("{uf_name}_canon") -} - -/// Name of an eq-sort's `uf_canon_proof` primitive. See [`uf_canon_prim_name`]. -pub(crate) fn uf_canon_proof_prim_name(uf_name: &str) -> String { - format!("{uf_name}_canon_proof") -} - -/// Register an eq-sort's single-term canonicalization primitives, so a rebuild -/// rule can canonicalize a child in its action: -/// -/// * `uf_canon : (S S) -> S` — `(term fallback)`, the term's `@UF_` leader, or -/// `fallback` when it has no row. Callers pass the term itself, making this -/// leader-or-self. -/// * `uf_canon_proof : (S Proof) -> Proof` (proof mode) — `(term fallback)`, the -/// `@UF_` row's proof `term = leader`, or `fallback`. Callers pass the -/// reflexive `Proof(term)`. -/// -/// Both are the generic view-column read over the two-output `@UF_` table, so -/// each backend services them against its own storage. They read `@UF_`, so -/// they are only sound in the action of a rule whose body joins the driving -/// `@UF` delta. Called from the eq-sort's Sort command in typechecking, so they -/// exist both during encoding and on re-parse. -pub(crate) fn register_uf_canon( - eg: &mut EGraph, - sort_name: &str, - uf_name: &str, - proofs_enabled: bool, -) { - let Some(sort) = eg.get_sort_by_name(sort_name).cloned() else { - return; - }; - let canon = UfCanonCol { - name: uf_canon_prim_name(uf_name), - key_sort: sort.clone(), - out_sort: sort.clone(), - }; - let table = uf_name.to_string(); - eg.add_backend_op_primitive(canon, WriteState::valid_contexts(), move |backend, _| { - backend.register_view_column_read(table.clone(), 1, 0) - }); - - // The proof column is only meaningful in proof mode; in term mode `@UF_` - // carries `Unit` there and no rebuild rule reads it. - if proofs_enabled { - let proof_sort: ArcSort = std::sync::Arc::new(EqSort { - name: eg.proof_state.proof_names.proof_datatype.clone(), - }); - let canon_proof = UfCanonCol { - name: uf_canon_proof_prim_name(uf_name), - key_sort: sort, - out_sort: proof_sort, - }; - let table = uf_name.to_string(); - eg.add_backend_op_primitive( - canon_proof, - WriteState::valid_contexts(), - move |backend, _| backend.register_view_column_read(table.clone(), 1, 1), - ); - } -} - -/// One column of an eq-sort's `@UF_` row, read by term with a fallback (see -/// [`register_uf_canon`]). -#[derive(Clone)] -struct UfCanonCol { - name: String, - key_sort: ArcSort, - out_sort: ArcSort, -} - -impl Primitive for UfCanonCol { - fn name(&self) -> &str { - &self.name - } - - fn get_type_constraints(&self, span: &Span) -> Box { - // (term fallback) -> column - SimpleTypeConstraint::new( - &self.name, - vec![ - self.key_sort.clone(), - self.out_sort.clone(), - self.out_sort.clone(), - ], - span.clone(), - ) - .into_box() - } -} - /// Register a container sort's rebuild primitives from its /// [`ContainerRebuildSpec`]. Called when a container Sort command carrying an /// `:internal-container-rebuild` annotation is typechecked, so the primitives diff --git a/egglog/src/proofs/proof_encoding.md b/egglog/src/proofs/proof_encoding.md index c359cedb..0041a7d5 100644 --- a/egglog/src/proofs/proof_encoding.md +++ b/egglog/src/proofs/proof_encoding.md @@ -486,9 +486,9 @@ with the leader (the view's `:merge` keeps the smaller). :ruleset rebuilding :name "rebuild_rule" :internal-include-subsumed) ``` -The **eq-sort children** are handled by a single rule per distinct child sort, -driven by a `UF_` edge rather than by matching the view. Each view gets one -hidden *rebuild index* per distinct child eq-sort, +A rule for an **eq-sort child** is driven by a `UF_` edge rather than by +matching the view. Each view gets one hidden *rebuild index* per distinct child +eq-sort, ```text (function MulIndex_Math (Math Math Math) Unit :merge old :internal-hidden :unextractable) @@ -497,33 +497,32 @@ hidden *rebuild index* per distinct child eq-sort, holding, for every view row, one entry per `Math` child: that child first, then the row's whole key. Leading with the child makes "which rows mention this term" a key-prefix lookup — the same access pattern a native rebuild uses when it walks -the e-nodes referencing a changed e-class. The rule joins a `UF_Math` edge -against the index to reach those rows: +the e-nodes referencing a changed e-class. One rule per indexed child position +joins a `UF_Math` edge against the index; here, position 0 of `Mul`: ```text (rule ((= (values leader plf) (UF_Math follower)) (!= follower leader) - (MulIndex_Math follower c0 c1) - (= (values e pe) (MulView c0 c1))) - ((let c0_canon_ (UF_Math_canon c0 c0)) - (let c1_canon_ (UF_Math_canon c1 c1)) - (set (MulView c0_canon_ c1_canon_) (values e ())) - (set (MulIndex_Math c0_canon_ c0_canon_ c1_canon_) ()) - (set (MulIndex_Math c1_canon_ c0_canon_ c1_canon_) ()) - (delete (MulView c0 c1)) - (delete (MulIndex_Math c0 c0 c1)) - (delete (MulIndex_Math c1 c0 c1))) + (MulIndex_Math follower follower c1)) + ((let e (view-col0-MulView follower c1)) + (set (MulView leader c1) (values e ())) + (set (MulIndex_Math leader leader c1) ()) + (set (MulIndex_Math c1 leader c1) ()) + (delete (MulView follower c1)) + (delete (MulIndex_Math follower follower c1)) + (delete (MulIndex_Math c1 follower c1))) :ruleset rebuilding :unsafe-seminaive :name "rebuild_rule" :internal-include-subsumed) ``` -`UF__canon` is the row's leader column read by term, with the term itself -as the fallback — so a child already at its leader canonicalizes to itself. The -action re-canonicalizes *every* eq-sort child, so one firing fixes the whole row -instead of one column of it; in proof mode it folds one `Congr` per child onto -the row proof, and the steps for children that did not move are reflexive and -collapse in the proof simplifier. Reading `UF_` in the action is what makes -the rule `:unsafe-seminaive`; the driving `UF_` delta in the body is what -makes that read sound. +The moved term is bound at a known position, so its leader is a plain +substitution and proof mode composes a single `Congr` at that position from +`plf`, the edge proof the body already bound. + +The index entry also binds the row's key, so the row's value tuple is read in the +*action* (`view-col-`) instead of joining the view as a third body atom. +Those readers take no fallback: an absent key halts the rule, exactly as a failing +body join would. Reading the view in the action is what makes the rule +`:unsafe-seminaive`. The index is maintained wherever a view row is written or deleted, so it tracks the view exactly. Container children are not indexed — they have no `UF_` diff --git a/egglog/src/typechecking.rs b/egglog/src/typechecking.rs index 40f73cdf..0ed95d7d 100644 --- a/egglog/src/typechecking.rs +++ b/egglog/src/typechecking.rs @@ -1,9 +1,7 @@ use std::hash::Hasher; use crate::Context; -use crate::proofs::proof_container_rebuild::{ - register_container_rebuild_from_spec, register_uf_canon, -}; +use crate::proofs::proof_container_rebuild::register_container_rebuild_from_spec; use crate::{ core::{CoreActionContext, CoreRule, GenericActionsExt, QueryConstraints, ResolvedCall}, *, @@ -570,12 +568,6 @@ impl EGraph { if let Some(spec) = container_rebuild { register_container_rebuild_from_spec(self, name, spec); } - // An eq-sort under the encoding registers the single-term - // canonicalization primitives its rebuild rules call, derived - // from its `@UF_` table. - if let Some((uf_ctor, _uf_index)) = uf { - register_uf_canon(self, name, uf_ctor, proof_func.is_some()); - } ResolvedNCommand::Sort { span: span.clone(), name: name.clone(),