Proofs for containers read/constructed in rule bodies (Eval step) (#9)

* Add validators for container reader primitives

Give vec-get/vec-length/vec-contains, map-get/map-length/map-contains,
and multiset-length/multiset-contains validators so the proof checker can
recompute them when these primitives are used to read a matched container
in a rule body.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* Prove container side conditions with an Eval marker

A container built by a primitive in a rule body (e.g. (vec-of e)) has no
anchored term-proof. Treat it as a side condition:

- Proof normal form lifts a container-producing primitive out of any
  constructor into its own `(= v (prim ...))` binding, so every container
  primitive is a standalone side condition.
- The proof of a container side condition is a contentless `Eval` marker.
- The checker re-evaluates each container side condition against the rule body
  with the rule's typed primitive validator (`check_side_condition`), binding
  its output for later facts and checking comparisons — it never inspects the
  marker. It also rejects rule bodies not in proof normal form (a primitive
  with a constructor argument, or a container primitive used outside a side
  condition).

A container side condition has no carryable proof, so it cannot be used in an
action; such a rule is rejected (ContainerCreatedInQueryUsedInAction).
Covered by container-proofs.egg across plain/proof/proof_testing modes.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

---------

Co-authored-by: Oliver Flatt <oflatt@gmail.com>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: 3 people

CHANGELOG.md

@@ -17,7 +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). 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. See `src/proofs/proof_encoding.md`.
+- **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. 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. See `src/proofs/proof_encoding.md`.
 
 ## [2.0.0] - 2026-02-11
 

src/proofs/proof_checker.rs

@@ -20,6 +20,25 @@ use crate::{
 };
 use thiserror::Error;
 
+/// A side condition is a rule-body fact that is just a container-producing
+/// primitive applied to bound variables — `(= v (vec-of e))`, `(= (set-of a)
+/// (set-of b))`, etc. Its proof is a bare [`Justification::Eval`] marker and it
+/// is verified by re-evaluation in [`ProofStore::check_side_condition`] rather
+/// than by matching a premise proposition.
+pub(super) fn is_container_side_condition(fact: &ResolvedFact) -> bool {
+    fn is_container_primitive(expr: &ResolvedExpr) -> bool {
+        matches!(
+            expr,
+            ResolvedExpr::Call(_, ResolvedCall::Primitive(p), _)
+                if p.output().is_eq_container_sort()
+        )
+    }
+    match fact {
+        ResolvedFact::Eq(_, lhs, rhs) => is_container_primitive(lhs) || is_container_primitive(rhs),
+        ResolvedFact::Fact(expr) => is_container_primitive(expr),
+    }
+}
+
 /// Result of processing actions: terms bound to variables and propositions
 #[derive(Debug, Clone)]
 pub(crate) struct ActionContext {
@@ -448,6 +467,30 @@ pub enum ProofCheckErrorKind {
         proof_rhs: TermId,
         lhs_ok: bool,
     },
+    /// Eval marker appeared outside a container side condition
+    #[error("Proof {proof_id}: Eval marker used outside a container side condition")]
+    EvalOutsideSideCondition { proof_id: ProofId },
+    /// A container side condition's two sides evaluate to different containers
+    #[error("Rule '{rule_name}': side condition {fact} does not hold ({lhs:?} != {rhs:?})")]
+    SideConditionMismatch {
+        rule_name: String,
+        fact: String,
+        lhs: TermId,
+        rhs: TermId,
+    },
+    /// A container side condition has no determined side to evaluate
+    #[error("Rule '{rule_name}': side condition {fact} has no bound side to evaluate")]
+    SideConditionUnbound { rule_name: String, fact: String },
+    /// Not in proof normal form: a primitive has a constructor/function argument
+    #[error(
+        "Rule '{rule_name}': primitive argument {arg} is not a variable, literal, or primitive (not in proof normal form)"
+    )]
+    PrimitiveNonNormalArg { rule_name: String, arg: String },
+    /// Not in proof normal form: a container primitive is not a side condition
+    #[error(
+        "Rule '{rule_name}': container primitive {prim} appears nested rather than as a side condition (not in proof normal form)"
+    )]
+    ContainerPrimitiveNotSideCondition { rule_name: String, prim: String },
 }
 
 /// Context needed for proof checking
@@ -580,35 +623,33 @@ impl ProofStore {
                     .into());
                 }
 
-                // Check each premise proof
-                let mut premise_propositions = Vec::new();
-                for &premise_id in premise_proofs {
-                    let prop = self.check_proof_with_context(premise_id, program, ctx)?;
-                    premise_propositions.push(prop);
-                }
-
-                let substitution_with_globals = ctx
+                let mut working_subst = ctx
                     .global_bindings
                     .iter()
                     .map(|(k, v)| (k.clone(), *v))
                     .chain(substitution.iter().map(|(k, v)| (k.clone(), *v)))
                     .collect::<HashMap<_, _>>();
 
-                // Verify that premises match the rule body under the substitution
-                for (fact, prop) in rule.body.iter().zip(premise_propositions.iter()) {
-                    self.check_fact_matches_proposition(
-                        fact,
-                        prop,
-                        &substitution_with_globals,
-                        name,
-                    )?;
+                // Verify each premise in order. A container side condition carries
+                // only an `Eval` marker, so re-evaluate it here with the rule's
+                // typed validator — this binds its output into the substitution for
+                // later facts. Every other fact is matched against its premise
+                // proposition.
+                for (fact, &premise_id) in rule.body.iter().zip(premise_proofs.iter()) {
+                    self.assert_body_proof_normal_form(fact, name)?;
+                    if is_container_side_condition(fact) {
+                        self.check_side_condition(fact, &mut working_subst, name)?;
+                    } else {
+                        let prop = self.check_proof_with_context(premise_id, program, ctx)?;
+                        self.check_fact_matches_proposition(fact, &prop, &working_subst, name)?;
+                    }
                 }
 
                 // Verify that the conclusion matches what the rule produces
                 self.check_rule_produces_equality(
                     rule,
                     substitution,
-                    &substitution_with_globals,
+                    &working_subst,
                     proof.proposition(),
                     name,
                 )?;
@@ -872,6 +913,14 @@ impl ProofStore {
                 }
                 Ok(Proposition::new(proof.lhs(), proof.rhs()))
             }
+
+            Justification::Eval => {
+                // The `Eval` marker is the proof of a container side condition and
+                // is checked by re-evaluation in `check_side_condition` (driven by
+                // the rule body), never on its own. Reaching it here means it
+                // appeared outside a side condition, which is malformed.
+                Err(ProofCheckErrorKind::EvalOutsideSideCondition { proof_id }.into())
+            }
         };
 
         // Cache the result
@@ -882,7 +931,121 @@ impl ProofStore {
         result
     }
 
-    /// Check that a fact matches a proposition under a substitution  
+    /// Check a container side condition by re-evaluating it against the rule
+    /// body, rather than against a premise proposition. An unbound side is the
+    /// side condition's output and is bound; otherwise both sides must evaluate
+    /// to the same container. Extends `subst` with any bound output.
+    fn check_side_condition(
+        &mut self,
+        fact: &ResolvedFact,
+        subst: &mut HashMap<String, TermId>,
+        rule_name: &str,
+    ) -> Result<(), ProofCheckError> {
+        let ResolvedFact::Eq(_, lhs, rhs) = fact else {
+            // `is_container_side_condition` only flags `Eq` facts.
+            return Ok(());
+        };
+        let lhs_val = self.eval_side(lhs, subst, rule_name)?;
+        let rhs_val = self.eval_side(rhs, subst, rule_name)?;
+        match (lhs, lhs_val, rhs, rhs_val) {
+            // One side is an unbound variable: it is the side condition's output.
+            (ResolvedExpr::Var(_, v), None, _, Some(val))
+            | (_, Some(val), ResolvedExpr::Var(_, v), None) => {
+                subst.insert(v.name.clone(), val);
+                Ok(())
+            }
+            // Both sides determined: they must be the same container.
+            (_, Some(l), _, Some(r)) => {
+                if l != r {
+                    return Err(ProofCheckErrorKind::SideConditionMismatch {
+                        rule_name: rule_name.to_string(),
+                        fact: format!("{fact}"),
+                        lhs: l,
+                        rhs: r,
+                    }
+                    .into());
+                }
+                Ok(())
+            }
+            _ => Err(ProofCheckErrorKind::SideConditionUnbound {
+                rule_name: rule_name.to_string(),
+                fact: format!("{fact}"),
+            }
+            .into()),
+        }
+    }
+
+    /// Evaluate one side of a side condition: an unbound variable yields `None`
+    /// (it is an output to bind), anything else is evaluated with the rule's
+    /// typed primitive validators.
+    fn eval_side(
+        &mut self,
+        expr: &ResolvedExpr,
+        subst: &HashMap<String, TermId>,
+        rule_name: &str,
+    ) -> Result<Option<TermId>, ProofCheckError> {
+        match expr {
+            ResolvedExpr::Var(_, v) => Ok(subst.get(&v.name).copied()),
+            _ => {
+                let (term, _) = eval_expr_with_subst(rule_name, expr, &mut self.term_dag, subst)?;
+                Ok(Some(term))
+            }
+        }
+    }
+
+    /// Reject a rule-body fact that isn't in proof normal form: a primitive must
+    /// not have a constructor/function argument, and a container-producing
+    /// primitive must not appear nested (it must be its own side condition).
+    fn assert_body_proof_normal_form(
+        &self,
+        fact: &ResolvedFact,
+        rule_name: &str,
+    ) -> Result<(), ProofCheckError> {
+        fn check(expr: &ResolvedExpr, rule_name: &str) -> Result<(), ProofCheckError> {
+            let ResolvedExpr::Call(_, head, args) = expr else {
+                return Ok(());
+            };
+            for arg in args {
+                match head {
+                    ResolvedCall::Primitive(_)
+                        if matches!(arg, ResolvedExpr::Call(_, ResolvedCall::Func(_), _)) =>
+                    {
+                        return Err(ProofCheckErrorKind::PrimitiveNonNormalArg {
+                            rule_name: rule_name.to_string(),
+                            arg: format!("{arg}"),
+                        }
+                        .into());
+                    }
+                    ResolvedCall::Func(_)
+                        if matches!(
+                            arg,
+                            ResolvedExpr::Call(_, ResolvedCall::Primitive(p), _)
+                                if p.output().is_eq_container_sort()
+                        ) =>
+                    {
+                        return Err(ProofCheckErrorKind::ContainerPrimitiveNotSideCondition {
+                            rule_name: rule_name.to_string(),
+                            prim: format!("{arg}"),
+                        }
+                        .into());
+                    }
+                    _ => {}
+                }
+                check(arg, rule_name)?;
+            }
+            Ok(())
+        }
+        match fact {
+            ResolvedFact::Eq(_, lhs, rhs) => {
+                check(lhs, rule_name)?;
+                check(rhs, rule_name)?;
+            }
+            ResolvedFact::Fact(expr) => check(expr, rule_name)?,
+        }
+        Ok(())
+    }
+
+    /// Check that a fact matches a proposition under a substitution
     fn check_fact_matches_proposition(
         &mut self,
         fact: &ResolvedFact,

src/proofs/proof_encoding.rs

@@ -866,13 +866,34 @@ impl<'a> ProofInstrumentor<'a> {
                 }
             }
             ResolvedFact::Eq(_span, left_expr, right_expr) => {
-                let (v1, p1) = self.instrument_fact_expr(left_expr, res, action_lookups);
-                let (v2, p2) = self.instrument_fact_expr(right_expr, res, action_lookups);
-                res.push(format!("(= {v1} {v2})"));
-                let sym = &self.proof_names().eq_sym_constructor;
-                let trans = &self.proof_names().eq_trans_constructor;
+                let is_container_prim = |e: &ResolvedExpr| {
+                    matches!(
+                        e,
+                        ResolvedExpr::Call(_, ResolvedCall::Primitive(p), _)
+                            if p.output().is_eq_container_sort()
+                    )
+                };
+                // A container side condition: a fact that builds a container with
+                // a primitive (`(= xs (vec-of e))`, `(= (set-of a) (set-of b))`).
+                // The container has no carryable proof — emit just the `Eval`
+                // marker and the query bindings; the checker re-evaluates the side
+                // condition (see `check_side_condition`).
+                if is_container_prim(left_expr) || is_container_prim(right_expr) {
+                    // A container side condition: emit the fact as-is so the
+                    // e-graph computes the container (its arguments are already
+                    // bound). Its proof is the `Eval` marker, checked by
+                    // re-evaluation (see `check_side_condition`).
+                    res.push(fact.to_string());
+                    format!("({})", self.proof_names().eval_constructor)
+                } else {
+                    let (v1, p1) = self.instrument_fact_expr(left_expr, res, action_lookups);
+                    let (v2, p2) = self.instrument_fact_expr(right_expr, res, action_lookups);
+                    res.push(format!("(= {v1} {v2})"));
+                    let sym = &self.proof_names().eq_sym_constructor;
+                    let trans = &self.proof_names().eq_trans_constructor;
 
-                format!("({trans} ({sym} {p1}) {p2})",)
+                    format!("({trans} ({sym} {p1}) {p2})",)
+                }
             }
             ResolvedFact::Fact(generic_expr) => {
                 let (_, proof) = self.instrument_fact_expr(generic_expr, res, action_lookups);
@@ -1001,14 +1022,17 @@ impl<'a> ProofInstrumentor<'a> {
 
                         let proof = if !self.proofs_enabled() {
                             "()".to_string()
-                        } else if specialized_primitive.output().is_eq_sort()
-                            || specialized_primitive.output().is_eq_container_sort()
-                        {
-                            // An eq-sort/eq-container result is an `App`, not a
-                            // literal, so a reflexive `Fiat` would be rejected by
-                            // the checker. Anchor it on the sort's term-proof
-                            // table (the `<CSort>Proof` reflexive proof for
-                            // containers), emitted as an action lookup.
+                        } else if specialized_primitive.output().is_eq_container_sort() {
+                            // A container computed in the query/rule body has no
+                            // carryable proof. It only ever appears in a container
+                            // side condition, whose proof is the `Eval` marker
+                            // emitted at the fact level (see `instrument_fact`);
+                            // this per-expression proof is unused.
+                            "()".to_string()
+                        } else if specialized_primitive.output().is_eq_sort() {
+                            // An eq-sort (datatype) result is an existing anchored
+                            // term (e.g. an identity primitive returning its
+                            // input); reuse its term-proof, fetched in the action.
                             let term_proof_name =
                                 self.term_proof_name(specialized_primitive.output().name());
                             let fresh_proof = self.fresh_var();