Proof support for containers

CHANGELOG.md

@@ -17,6 +17,7 @@
 - Expose `Read::table_size(name)` and `Read::table_sizes()` so read-capable primitives can inspect row counts without raw execution-state access, while avoiding an all-table scan when only one table is needed.
 - **`:naive` and `:unsafe-seminaive` rule options** (mutually exclusive). Both compile a rule under the permissive `Read`/`Full` contexts so its RHS can read the database (read-primitives and function-table lookups). `:naive` matches the whole database every iteration; `:unsafe-seminaive` keeps seminaive (delta) matching, which is faster but **unsafe** — an RHS read observes the database mid-iteration, so results can depend on evaluation order. `:unsafe-seminaive` is rejected by the term/proof encoding.
 - **Name-indexed e-graph access from primitives and `rust_rule` callbacks (#745, #751).** New `Read` / `Write` capability traits on the state wrappers let primitive bodies and rule callbacks read/write tables by name (`fs.lookup`, `fs.set`, `fs.add`, `fs.union`, `fs.function_entries`, `fs.constructor_enodes`, etc.) instead of through raw `FunctionId` + `&[Value]`; `EGraph::update(|fs| ...)` gives the same surface outside a rule, and `EGraph::function_entries` / `EGraph::constructor_enodes` expose the table scans directly at the top level. Misuse (wrong subtype, wrong arity, unknown table) surfaces as `Error::ApiError`.
+- **Container support in the term/proof encoding.** Programs using container sorts (`Vec`, `Set`, `Map`, `MultiSet`, `Pair`) now work under the term/proof encoding (previously rejected), including containers read (`vec-get`, `map-get`, …) or constructed (`vec-of`, `set-of`, …) in a rule body (`set-get` excepted: it indexes an internal runtime order that proofs cannot reproduce). A container built in the body is a *side condition* with no carryable proof: it is marked with an `Eval` proof step and re-evaluated against the typed rule when checked, so it can be read or matched in the query but not carried into an action (that is rejected). Two user-visible extraction changes: container terms extract in a deterministic, reproducible order rather than value-id order, and maps extract in a flat `(map-of k0 v0 …)` form (new `map-of` constructor) instead of nested `map-insert`s.
 
 ## [2.0.0] - 2026-02-11
 

core-relations/src/containers/mod.rs

@@ -28,7 +28,7 @@ use crate::{
     WrappedTable,
     common::{DashMap, IndexSet, SubsetTracker},
     parallel_heuristics::{parallelize_inter_container_op, parallelize_intra_container_op},
-    table_spec::Rebuilder,
+    table_spec::{Rebuilder, ValueRebuilder},
 };
 
 #[cfg(test)]
@@ -162,6 +162,31 @@ impl ContainerValues {
         env.get_or_insert(&container, exec_state)
     }
 
+    /// Rebuild a single container value by remapping each contained value
+    /// through `remap`, returning the (possibly new) interned value, or `value`
+    /// unchanged if it is not a registered container of the type behind
+    /// `type_id`.
+    ///
+    /// Unlike [`ContainerValues::rebuild_all`], which drives rebuilds off the
+    /// backend union-find, the caller supplies the remapping explicitly and
+    /// identifies the container type dynamically by its [`TypeId`].
+    pub fn rebuild_val_with(
+        &self,
+        type_id: TypeId,
+        value: Value,
+        exec_state: &mut ExecutionState,
+        remap: &(dyn Fn(Value) -> Value + Send + Sync),
+    ) -> Value {
+        let Some(id) = self.container_ids.get(&type_id) else {
+            return value;
+        };
+        let Some(env) = self.data.get(id) else {
+            return value;
+        };
+        env.rebuild_val_with(value, exec_state, remap)
+            .unwrap_or(value)
+    }
+
     /// Apply the given rebuild to the contents of each container.
     pub fn rebuild_all(
         &mut self,
@@ -262,11 +287,11 @@ impl ContainerValues {
 /// rebuilding of container contents and merging containers that become equal after a rebuild pass
 /// has taken place.
 pub trait ContainerValue: Hash + Eq + Clone + Send + Sync + 'static {
-    /// Rebuild an additional container in place according the the given [`Rebuilder`].
+    /// Rebuild an additional container in place according the the given [`ValueRebuilder`].
     ///
     /// If this method returns `false` then the container must not have been modified (i.e. it must
     /// hash to the same value, and compare equal to a copy of itself before the call).
-    fn rebuild_contents(&mut self, rebuilder: &dyn Rebuilder) -> bool;
+    fn rebuild_contents(&mut self, rebuilder: &dyn ValueRebuilder) -> bool;
 
     /// Iterate over the contents of the container.
     ///
@@ -292,6 +317,15 @@ pub trait DynamicContainerEnv: Any + dyn_clone::DynClone + Send + Sync {
     /// [`ContainerValue::iter`] and lets callers climb from dirty child ids to
     /// all directly containing parent container ids.
     fn extend_containers_containing(&self, values: &IndexSet<Value>, out: &mut IndexSet<Value>);
+    /// Rebuild the single container `value` by remapping each contained value
+    /// through `remap`, returning the (possibly new) interned value, or `None`
+    /// if `value` is not registered in this environment.
+    fn rebuild_val_with(
+        &self,
+        value: Value,
+        exec_state: &mut ExecutionState,
+        remap: &(dyn Fn(Value) -> Value + Send + Sync),
+    ) -> Option<Value>;
 }
 
 // Implements `Clone` for `Box<dyn DynamicContainerEnv>`.
@@ -350,6 +384,19 @@ impl<C: ContainerValue> DynamicContainerEnv for ContainerEnv<C> {
             }
         }
     }
+
+    fn rebuild_val_with(
+        &self,
+        value: Value,
+        exec_state: &mut ExecutionState,
+        remap: &(dyn Fn(Value) -> Value + Send + Sync),
+    ) -> Option<Value> {
+        // Clone out of the guard before re-interning to avoid deadlocking on
+        // the underlying map.
+        let mut container = self.get_container(value)?.clone();
+        container.rebuild_contents(&ClosureRebuilder { remap });
+        Some(self.get_or_insert(&container, exec_state))
+    }
 }
 
 impl<C: ContainerValue> ContainerEnv<C> {
@@ -737,3 +784,16 @@ fn incremental_rebuild(uf_size: usize, table_size: usize, parallel: bool) -> boo
         table_size > 1000 && uf_size * 8 <= table_size
     }
 }
+
+/// A [`ValueRebuilder`] that remaps individual values through a caller-supplied
+/// closure. Used by [`ContainerValues::rebuild_val_with`] to rebuild a single
+/// container against an explicit value mapping rather than a backend union-find.
+struct ClosureRebuilder<'a> {
+    remap: &'a (dyn Fn(Value) -> Value + Send + Sync),
+}
+
+impl ValueRebuilder for ClosureRebuilder<'_> {
+    fn rebuild_val(&self, val: Value) -> Value {
+        (self.remap)(val)
+    }
+}

core-relations/src/containers/tests.rs

@@ -9,8 +9,8 @@ use crate::numeric_id::NumericId;
 use egglog_concurrency::Notification;
 
 use crate::{
-    ColumnId, Database, ExecutionState, Rebuilder, RowId, Value, row_buffer::RowBuffer,
-    table_spec::WrappedTableRef,
+    ColumnId, Database, ExecutionState, Rebuilder, RowId, Value, ValueRebuilder,
+    row_buffer::RowBuffer, table_spec::WrappedTableRef,
 };
 
 use super::{ContainerEnv, ContainerRebuildSummary, ContainerValue, hash_container};
@@ -23,7 +23,7 @@ fn cont<const N: usize>(values: [usize; N]) -> VecContainer {
 }
 
 impl ContainerValue for VecContainer {
-    fn rebuild_contents(&mut self, rebuilder: &dyn Rebuilder) -> bool {
+    fn rebuild_contents(&mut self, rebuilder: &dyn ValueRebuilder) -> bool {
         rebuilder.rebuild_slice(&mut self.0)
     }
 
@@ -41,18 +41,35 @@ struct FakeRebuilder {
     new_inner_val: Option<Value>,
 }
 
-impl Rebuilder for FakeRebuilder {
-    fn hint_col(&self) -> Option<ColumnId> {
-        None
-    }
-
+impl ValueRebuilder for FakeRebuilder {
     fn rebuild_val(&self, val: Value) -> Value {
         match (self.old_outer_id, self.new_outer_id) {
             (Some(old), Some(new)) if val == old => new,
             _ => val,
         }
     }
 
+    fn rebuild_slice(&self, vals: &mut [Value]) -> bool {
+        let mut changed = false;
+        for val in vals {
+            if let (Some(old), Some(new)) = (self.old_inner_val, self.new_inner_val)
+                && *val == old
+            {
+                *val = new;
+                changed = true;
+            }
+        }
+        changed
+    }
+}
+
+// Also exercised via the table-level rebuild path, so it implements the full
+// `Rebuilder`; that path only calls the value-level methods for containers.
+impl Rebuilder for FakeRebuilder {
+    fn hint_col(&self) -> Option<ColumnId> {
+        None
+    }
+
     fn rebuild_buf(
         &self,
         _buf: &RowBuffer,
@@ -73,19 +90,6 @@ impl Rebuilder for FakeRebuilder {
     ) {
         unreachable!("FakeRebuilder does not support rebuild_subset")
     }
-
-    fn rebuild_slice(&self, vals: &mut [Value]) -> bool {
-        let mut changed = false;
-        for val in vals {
-            if let (Some(old), Some(new)) = (self.old_inner_val, self.new_inner_val)
-                && *val == old
-            {
-                *val = new;
-                changed = true;
-            }
-        }
-        changed
-    }
 }
 
 #[test]

core-relations/src/lib.rs

@@ -40,7 +40,7 @@ pub use row_buffer::TaggedRowBuffer;
 pub use table::{MergeFn, SortedWritesTable};
 pub use table_spec::{
     ColumnId, Constraint, MutationBuffer, Offset, Rebuilder, Row, Table, TableChange, TableSpec,
-    TableVersion, WrappedTable,
+    TableVersion, ValueRebuilder, WrappedTable,
 };
 pub use uf::DisplacedTable;
 

core-relations/src/table_spec.rs

@@ -100,19 +100,43 @@ pub enum Constraint {
     GeConst { col: ColumnId, val: Value },
 }
 
+/// Remap individual values (e.g. to their union-find leaders) — the value-level
+/// half of rebuilding, enough to rebuild a single container's contents (see
+/// [`crate::ContainerValue::rebuild_contents`]).
+pub trait ValueRebuilder: Send + Sync {
+    /// Rebuild a single value.
+    fn rebuild_val(&self, val: Value) -> Value;
+    /// Rebuild a slice of values in place, returning true if any values were changed.
+    ///
+    /// Defaults to mapping each value through [`ValueRebuilder::rebuild_val`];
+    /// implementors may override for efficiency.
+    fn rebuild_slice(&self, vals: &mut [Value]) -> bool {
+        let mut changed = false;
+        for val in vals.iter_mut() {
+            let new = self.rebuild_val(*val);
+            if new != *val {
+                *val = new;
+                changed = true;
+            }
+        }
+        changed
+    }
+}
+
 /// Custom functions used for tables that encode a bulk value-level rebuild of other tables.
 ///
+/// Extends [`ValueRebuilder`] with table-level (bulk) operations.
+///
 /// The initial use-case for this trait is to support optimized implementations of rebuilding,
 /// where `Rebuilder` is implemented as a Union-find.
 ///
 /// Value-level rebuilds are difficult to implement efficiently using rules as they require
 /// searching for changes to any column for a table: while it is possible to do, implementing this
 /// custom is more efficient in the case of rebuilding.
-pub trait Rebuilder: Send + Sync {
+pub trait Rebuilder: ValueRebuilder {
     /// The column that contains values that should be rebuilt. If this is set, callers can use
     /// this functionality to perform rebuilds incrementally.
     fn hint_col(&self) -> Option<ColumnId>;
-    fn rebuild_val(&self, val: Value) -> Value;
     /// Rebuild a contiguous slice of rows in the table.
     fn rebuild_buf(
         &self,
@@ -130,8 +154,6 @@ pub trait Rebuilder: Send + Sync {
         out: &mut TaggedRowBuffer,
         exec_state: &mut ExecutionState,
     );
-    /// Rebuild a slice of values in place, returning true if any values were changed.
-    fn rebuild_slice(&self, vals: &mut [Value]) -> bool;
 }
 
 /// A row in a table.

core-relations/src/uf/mod.rs

@@ -18,7 +18,7 @@ use crate::{
     row_buffer::RowBuffer,
     table_spec::{
         ColumnId, Constraint, Generation, MutationBuffer, Offset, Rebuilder, Row, Table, TableSpec,
-        TableVersion, WrappedTableRef,
+        TableVersion, ValueRebuilder, WrappedTableRef,
     },
 };
 
@@ -64,13 +64,17 @@ struct Canonicalizer<'a> {
     table: &'a DisplacedTable,
 }
 
+impl ValueRebuilder for Canonicalizer<'_> {
+    fn rebuild_val(&self, val: Value) -> Value {
+        self.table.uf.find_naive(val)
+    }
+    // `rebuild_slice` uses the default (per-value `rebuild_val`).
+}
+
 impl Rebuilder for Canonicalizer<'_> {
     fn hint_col(&self) -> Option<ColumnId> {
         Some(ColumnId::new(0))
     }
-    fn rebuild_val(&self, val: Value) -> Value {
-        self.table.uf.find_naive(val)
-    }
     fn rebuild_buf(
         &self,
         buf: &RowBuffer,
@@ -184,15 +188,6 @@ impl Rebuilder for Canonicalizer<'_> {
             }
         }
     }
-    fn rebuild_slice(&self, vals: &mut [Value]) -> bool {
-        let mut changed = false;
-        for val in vals {
-            let canon = self.table.uf.find_naive(*val);
-            changed |= canon != *val;
-            *val = canon;
-        }
-        changed
-    }
 }
 
 impl Default for DisplacedTable {

egglog-bridge/src/tests.rs

@@ -11,7 +11,7 @@ use std::{
 
 use crate::core_relations;
 use crate::core_relations::{
-    ContainerValue, ExternalFunctionId, Rebuilder, Value, make_external_func,
+    ContainerValue, ExternalFunctionId, Value, ValueRebuilder, make_external_func,
 };
 use crate::numeric_id::NumericId;
 use log::debug;
@@ -449,7 +449,7 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
 #[derive(Clone, Debug, Hash, Eq, PartialEq)]
 struct VecContainer(Vec<Value>);
 impl ContainerValue for VecContainer {
-    fn rebuild_contents(&mut self, rebuilder: &dyn Rebuilder) -> bool {
+    fn rebuild_contents(&mut self, rebuilder: &dyn ValueRebuilder) -> bool {
         rebuilder.rebuild_slice(&mut self.0)
     }
     fn iter(&self) -> impl Iterator<Item = Value> + '_ {

src/ast/desugar.rs

@@ -71,6 +71,8 @@ pub(crate) fn desugar_command(
                         presort_and_args: None,
                         uf: None,
                         proof_func: None,
+                        container_rebuild: None,
+                        proof_constructors: None,
                         unionable: true,
                     });
                 }
@@ -91,6 +93,8 @@ pub(crate) fn desugar_command(
                     presort_and_args: Some((sort, args)),
                     uf: None,
                     proof_func: None,
+                    container_rebuild: None,
+                    proof_constructors: None,
                     unionable: true,
                 });
             }
@@ -144,13 +148,17 @@ pub(crate) fn desugar_command(
             presort_and_args,
             uf,
             proof_func,
+            container_rebuild,
+            proof_constructors,
             unionable,
         } => vec![NCommand::Sort {
             span,
             name,
             presort_and_args,
             uf,
             proof_func,
+            container_rebuild,
+            proof_constructors,
             unionable,
         }],
         Command::AddRuleset(span, name) => vec![NCommand::AddRuleset(span, name)],
@@ -234,6 +242,8 @@ fn desugar_prove(parser: &mut Parser, span: Span, query: Vec<Fact>) -> Vec<NComm
             presort_and_args: None,
             uf: None,
             proof_func: None,
+            container_rebuild: None,
+            proof_constructors: None,
             unionable: false,
         },
         NCommand::Function(FunctionDecl::constructor(
@@ -284,6 +294,8 @@ fn desugar_datatype(span: Span, name: String, variants: Vec<Variant>) -> Vec<NCo
         presort_and_args: None,
         uf: None,
         proof_func: None,
+        container_rebuild: None,
+        proof_constructors: None,
         unionable: true,
     }]
     .into_iter()
@@ -410,6 +422,8 @@ fn desugar_relation(
             presort_and_args: None,
             uf: None,
             proof_func: None,
+            container_rebuild: None,
+            proof_constructors: None,
             unionable: false,
         },
         NCommand::Function(FunctionDecl::constructor(