WIP: Materialized rebuild index + single-rule UF rebuild, rebuilt on #36

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)]

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<FunctionId> {
@@ -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 ---------------------------------------------------

egglog/CHANGELOG.md

@@ -2,6 +2,8 @@
 
 ## [Unreleased] - ReleaseDate
 
+- 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 <action>*)` command and a `(let <var> (begin <action>* <expr>))` 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 `<var>` 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.

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);
     }

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.

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

egglog/src/proofs/proof_encoding.md

@@ -486,13 +486,50 @@ 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_<Sort>` 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_<Constructor>`) are likewise re-keyed to their leaders so a subsumed
-row stays subsumed after its children move.
+A rule for an **eq-sort child** is driven by a `UF_<Sort>` 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. 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 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)
+```
+
+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<i>-<View>`) 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_<Sort>`
+row to drive a lookup — and keep the per-column `:naive` rule below. Subsumption
+markers (`to_subsume_<Constructor>`) 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