Proof support for containers by oflatt · Pull Request #927 · egraphs-good/egglog

oflatt · 2026-06-22T20:22:56Z

No description provided.

Programs using container sorts (Vec, Set, Map, MultiSet, Pair) now participate in the term encoding and proof production, where they were previously rejected (SortWithPresort). During rebuilding, a per-container rebuild primitive canonicalizes a container's eq-sort elements to their union-find leaders, recursing through nested containers (e.g. (Vec (Vec Math))). In proof mode it produces a Congr-chain proof that the old container equals the rebuilt one, anchored on a per-sort <Sort>Proof reflexive table (set at creation and re-anchored on each rebuilt container). This reuses the existing Congr justification, with no proof-format or proof-checker changes. - Container constructor primitives (vec-of, pair, set-of, multiset-of, map-insert, ...) gained proof validators producing their s-expr term form. - New ContainerValues::rebuild_val_with rebuilds one container against an explicit value remapping. - Container primitives in rule queries look up <CSort>Proof instead of an invalid Fiat reflexive proof. Follow-ups: proof for the Set/Map/MultiSet collapse case (term-only works), and the desugar round-trip is skipped for container files. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Add proof-mode (proof-checked) tests confirming that container rebuilds check in proof mode for the arity-preserving cases: - MultiSet merges (counts are preserved as repeated elements), - Set/Map rebuilds that do not merge elements/keys. These pass because canonicalization keeps the term arity, so the flat Congr chain lines up. The remaining gap is narrowed to Set/Map *collapse* (two elements/keys merging into one reduces arity, which a flat Congr chain can't express). Term-only rebuild still handles every case. CHANGELOG and proof_encoding.md updated to scope this precisely. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Add a general `ContainerAxiom` proof justification so containers whose canonical form reorders or merges elements (Set, Map, MultiSet) get sound rebuild proofs. A flat `Congr` chain produces the rebuilt term with children replaced in place, which may be unordered or contain duplicate/ clobbering entries; `ContainerAxiom` normalizes that term to the canonical form the value actually interns to. Normalization is a single shared `TermDag` operation (`normalize_container_term`) ordered by a new deterministic structural `TermDag::ast_cmp`, and is used by `reconstruct_termdag`, the container constructor validators, and the proof checker, so all three agree on the canonical term. As a result `set-of`/`map-insert`/`multiset-of` terms now extract in deterministic AST order rather than value-id order. Working in proof mode (with check_proof): Set collapse + reorder, MultiSet merge (counts preserved as repeats), Vec/Pair, and non-collapsing Set/Map. Remaining: Map *key collapse* (nested map-insert term form makes the rebuild Congr indices nested) — term-only Map handles it. Touches proof_format.rs + proof_checker.rs (one new general justification + a registry-free term-normalization the checker recomputes for soundness). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Switch maps to a flat `(map-of k0 v0 k1 v1 ...)` term form (a new `map-of` constructor with a custom alternating key/value type constraint), analogous to `set-of`/`vec-of`, instead of nested `map-insert`s. The nested form made the rebuild proof's `Congr` indices nested (deep keys/values had no flat index, and the key-sorted prefix sub-maps it needed often were never created since a map value loses its construction order). Flat `map-of` makes the Congr indices flat, so map rebuild proofs — including key collapse (last-write-wins) — check via the same ContainerAxiom path as the other containers. `TermDag::normalize_container_term` now canonicalizes map terms (from either `map-of` or a `map-insert`/`map-empty` spine) to flat `map-of` in sorted key order with last-write-wins. Maps now extract as `(map-of ...)`. All container rebuilds now produce checkable proofs: Vec, Pair, Set (collapse + reorder), Map (collapse), MultiSet (count merge). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The container rebuild primitives are registered programmatically with fresh names during proof/term encoding, so a re-parse of the desugared output could not resolve them. Serialize their configuration (primitive names, per-element UF_<E>f index names, and in proof mode the <CSort>Proof tables and proof constructors) onto the container `(sort …)` declaration as an `:internal-container-rebuild` annotation, and re-register the primitives from that spec when the Sort command is typechecked. This works both during the original encoding and on re-parse, so the proof-encoding desugar round-trip now runs for container programs; the `uses_container` skip in tests/files.rs is removed. Also fix a latent shadowing bug exposed by un-gating container files: the UF maintenance rules used literal query-variable names `a`/`b`/`c`, which collide with a user-defined global constructor of the same name (e.g. `(constructor b () E)`) when the encoded program is re-parsed. Use gensym'd names instead. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

- Condense the container-support CHANGELOG bullet to user-visible facts (encoding support, the two extraction behavior changes, ContainerAxiom + rebuild_val_with), deferring mechanism to proof_encoding.md instead of duplicating it. - set/multiset reconstruct_termdag now call the shared normalize_container_term (as map already does) rather than re-implementing sort+dedup inline. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

tests/proofs/ had no container coverage. This .egg unions two elements of a Set so it collapses, and the snapshotted proof shows the container rebuild path end to end: a Congr chain rebuilds the element to its leader (set-of A A) and the ContainerAxiom normalizes it to set-of A. Also remove a stray untracked tests/proofs/out.log build log. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

codecov-commenter · 2026-06-22T20:39:28Z

Codecov Report

❌ Patch coverage is 82.38095% with 148 lines in your changes missing coverage. Please review.
✅ Project coverage is 86.57%. Comparing base (5e655ca) to head (fdef9fb).

Files with missing lines	Patch %	Lines
src/sort/map.rs	32.14%	57 Missing ⚠️
core-relations/src/containers/mod.rs	53.33%	21 Missing ⚠️
src/proofs/proof_encoding.rs	95.45%	20 Missing ⚠️
src/sort/mod.rs	0.00%	11 Missing ⚠️
src/sort/pair.rs	55.00%	9 Missing ⚠️
src/proofs/proof_checker.rs	50.00%	8 Missing ⚠️
src/proofs/proof_simplification.rs	63.63%	8 Missing ⚠️
src/termdag.rs	93.82%	5 Missing ⚠️
src/ast/parse.rs	76.92%	3 Missing ⚠️
src/sort/vec.rs	76.92%	3 Missing ⚠️
... and 2 more

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #927      +/-   ##
==========================================
+ Coverage   86.51%   86.57%   +0.05%     
==========================================
  Files          88       88              
  Lines       26739    27521     +782     
==========================================
+ Hits        23133    23825     +692     
- Misses       3606     3696      +90

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

codspeed-hq · 2026-06-22T20:39:51Z

Merging this PR will not alter performance

✅ 29 untouched benchmarks
⏩ 219 skipped benchmarks¹

_{Comparing oflatt:oflatt-container-proofs (fdef9fb) with main (5e655ca)}

219 benchmarks were skipped, so the baseline results were used instead. If they were deleted from the codebase, click here and archive them to remove them from the performance reports. ↩

Replaces the per-container `proof_normalizes()` flag with an always-mint-then-simplify scheme, so container authors implement nothing extra: - The proof-mode rebuild mints a `ContainerAxiom` for every container, unconditionally (removing `proof_normalizes()` from `Sort` / `ContainerSort` and the Set/Map/MultiSet overrides). - The proof simplifier gains `opt_redundant_container_axiom`, which drops a `ContainerAxiom` whose normalization left the term unchanged — always the case for order/arity-preserving Vec/Pair, and for already-canonical sets/maps/multisets. Also names the axiom (the earlier TODO): `Justification::ContainerAxiom` carries an `Option<String>` name (`set-dedup` / `multiset-sort` / `map-last-write-wins`) derived from the term head via the new `TermDag::container_axiom_name`, and the printed proof shows it as `(name "...")`. The name needs no separate soundness check — it is derived from the same head `normalize_container_term` dispatches on, which the checker already recomputes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

# Conflicts: # src/proofs/proof_encoding.rs

Copilot

Pull request overview

Adds end-to-end proof/term-encoding support for built-in container sorts (Vec/Set/Map/MultiSet/Pair) by introducing deterministic container term normalization and container-aware rebuild/proof generation, enabling previously-unsupported programs to participate in proof production and checking.

Changes:

Add deterministic AST-structural ordering (TermDag::ast_cmp) and shared container canonicalization (normalize_container_term) used by reconstruction, validators, and proof checking.
Extend proof encoding to rebuild container columns (including nested containers) and introduce a ContainerNormalize proof justification to bridge reorder/merge canonicalization steps.
Add new container rebuild tests and proof snapshots; update unsupported-proof-file snapshot list and document the feature in the changelog/docs.

Reviewed changes

Copilot reviewed 25 out of 25 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
tests/snapshots/files__shared_snapshot_container_set_collapse.snap	New snapshot covering a proof involving collapsing set normalization.
tests/snapshots/files__proof_unsupported_files.snap	Updates list of files considered unsupported in proof mode (now fewer).
tests/proofs/container-set-collapse.egg	New proof-focused `.egg` program exercising collapsing set rebuild/normalization.
tests/container_rebuild.rs	New end-to-end Rust tests for container rebuild behavior in term-only and proof modes.
src/typechecking.rs	Registers container rebuild primitives from serialized sort annotations during typechecking.
src/termdag.rs	Adds `ast_cmp` and `normalize_container_term` (set/multiset/map canonicalization) plus tests.
src/sort/vec.rs	Adds proof validators for vec term forms (`vec-of`/`vec-empty`).
src/sort/set.rs	Adds proof validators and canonical reconstruction for sets via shared normalization.
src/sort/pair.rs	Adds proof validators for `pair`/`pair-first`/`pair-second`.
src/sort/multiset.rs	Adds proof validators and canonical reconstruction for multisets via shared normalization.
src/sort/mod.rs	Adds `Sort::rebuild_container_with_leaders` hook for value-level container rebuilds.
src/sort/map.rs	Introduces canonical flat `(map-of ...)` form, validator support, and custom typing for `map-of`.
src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap	Snapshot update reflecting new UF variable naming in encoded rules.
src/proofs/proof_simplification.rs	Adds simplification to drop redundant `ContainerNormalize` and updates term mapping logic.
src/proofs/proof_format.rs	Adds `ContainerNormalize` to proof format parsing/printing and conversion pipeline.
src/proofs/proof_encoding.rs	Implements container rebuild primitives/spec serialization and container-aware rebuild rules in encoding.
src/proofs/proof_encoding.md	Documents container participation in term/proof encoding and normalization mechanism.
src/proofs/proof_encoding_helpers.rs	Extends proof header and proof-encoding support checks to include built-in container presorts.
src/proofs/proof_checker.rs	Adds checker support and a dedicated error for `ContainerNormalize` proof verification.
src/prelude.rs	Implements generic container rebuild via `ContainerValues::rebuild_val_with` for container sorts.
src/ast/parse.rs	Parses `:internal-container-rebuild` option on container sort declarations.
src/ast/mod.rs	Threads `container_rebuild` through AST commands and ensures it round-trips in formatting.
src/ast/desugar.rs	Propagates `container_rebuild` field through desugaring paths.
core-relations/src/containers/mod.rs	Adds `ContainerValues::rebuild_val_with` and a closure-based rebuilder helper.
CHANGELOG.md	Documents new container support in term/proof encoding and associated user-visible extraction changes.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

+use crate::exec_state::{Internal, RegistrySealed};
 use crate::proofs::proof_encoding_helpers::{EncodingNames, Justification};


[codex] Add set proof validators for containers

Follow-up cleanups for "Proof support for containers", addressing review comments from saulshanabrook, Copilot, and oflatt: - pair-first/pair-second validators: guard argument arity with `let [pair] = args else { return None }` before indexing, matching the other validators (Copilot). - map-of: reject odd-arity argument lists in the validator, and leave malformed map terms unchanged during normalization instead of silently dropping the unpaired key/value (Copilot). - ast_cmp: document why the Lit/Var arms are spelled out rather than delegating to `l.cmp(r)` -- Term intentionally has no derived Ord, and a derived Ord on App would order children by insertion order, which is the thing ast_cmp exists to avoid (saulshanabrook). - typechecking: `use` register_container_rebuild_from_spec instead of calling it via an absolute crate path (oflatt). - termdag: replace the hard-coded head-name match in normalize_container_term with a ContainerNormalization strategy + a single builtin_container_normalization(head) source of truth, and extract a reusable `sort_terms_by_ast` helper that custom container sorts can call after e.g. their own dedup (oflatt/saulshanabrook). - proof_encoding: build and parse the :internal-container-rebuild spec as an egglog s-expression via the existing parser (SexpParser / Sexp::expect_*) instead of pushing and re-splitting space-separated tokens (oflatt). - core-relations: split Rebuilder into a value-level ValueRebuilder supertrait plus the table-level Rebuilder. ContainerValue::rebuild_contents now takes &dyn ValueRebuilder, so ClosureRebuilder (the single-container rebuilder) drops its two unreachable!() table-level methods entirely (oflatt). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Follow-up cleanups for "Proof support for containers", addressing review comments from saulshanabrook, Copilot, and oflatt: - pair-first/pair-second validators: guard argument arity with `let [pair] = args else { return None }` before indexing, matching the other validators (Copilot). - map-of: reject odd-arity argument lists in the validator, and leave malformed map terms unchanged during normalization instead of silently dropping the unpaired key/value (Copilot). - ast_cmp: document why the Lit/Var arms are spelled out rather than delegating to `l.cmp(r)` -- Term intentionally has no derived Ord, and a derived Ord on App would order children by insertion order, which is the thing ast_cmp exists to avoid (saulshanabrook). - typechecking: `use` register_container_rebuild_from_spec instead of calling it via an absolute crate path (oflatt). - normalization is now per-container, with no "built-in container" special casing: TermDag carries no container knowledge (only the generic `ast_cmp` and a reusable `sort_terms_by_ast` helper). Each container sort normalizes its own term form in its constructor validator (set: sort+dedup; multiset: sort; map: collapse to flat `map-of`), exactly as a user-defined container would. The proof checker recomputes a container's canonical form by applying the validator registered for the term's head (collected from the e-graph's primitives), so built-in and user containers are handled identically (oflatt/saulshanabrook). - proof_encoding: build and parse the :internal-container-rebuild spec as an egglog s-expression via the existing parser (SexpParser / Sexp::expect_*) instead of pushing and re-splitting space-separated tokens (oflatt). - core-relations: split Rebuilder into a value-level ValueRebuilder supertrait plus the table-level Rebuilder. ContainerValue::rebuild_contents now takes &dyn ValueRebuilder, so ClosureRebuilder (the single-container rebuilder) drops its two unreachable!() table-level methods entirely (oflatt). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Follow-up cleanups for "Proof support for containers", addressing review comments from saulshanabrook, Copilot, and oflatt: - pair-first/pair-second validators: guard argument arity with `let [pair] = args else { return None }` before indexing, matching the other validators (Copilot). - map-of: reject odd-arity argument lists in the validator, and leave malformed map terms unchanged during normalization instead of silently dropping the unpaired key/value (Copilot). - ast_cmp: document why the Lit/Var arms are spelled out rather than delegating to `l.cmp(r)` -- Term intentionally has no derived Ord, and a derived Ord on App would order children by insertion order, which is the thing ast_cmp exists to avoid (saulshanabrook). - typechecking: `use` register_container_rebuild_from_spec instead of calling it via an absolute crate path (oflatt). - normalization is now per-container, with no "built-in container" special casing: TermDag carries no container knowledge (only the generic `ast_cmp` and a reusable `sort_terms_by_ast` helper). Each container sort normalizes its own term form in its constructor validator (set: sort+dedup; multiset: sort; map: collapse to flat `map-of`), exactly as a user-defined container would. The proof checker recomputes a container's canonical form by applying the validator registered for the term's head (collected from the e-graph's primitives), so built-in and user containers are handled identically (oflatt/saulshanabrook). - proof_encoding: build and parse the :internal-container-rebuild spec as an egglog s-expression via the existing parser (SexpParser / Sexp::expect_*) instead of pushing and re-splitting space-separated tokens (oflatt). - move the container-rebuild primitives + their runtime + the spec decoder out of proof_encoding.rs (2027 -> 1674 lines) into a new proofs/proof_container_rebuild.rs; proof_encoding.rs keeps only the encoder-side spec build. Pure relocation, no behavior change. - core-relations: split Rebuilder into a value-level ValueRebuilder supertrait plus the table-level Rebuilder. ContainerValue::rebuild_contents now takes &dyn ValueRebuilder, so ClosureRebuilder (the single-container rebuilder) drops its two unreachable!() table-level methods entirely (oflatt). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Follow-up cleanups for "Proof support for containers", addressing review comments from saulshanabrook, Copilot, and oflatt: - pair-first/pair-second validators: guard argument arity with `let [pair] = args else { return None }` before indexing, matching the other validators (Copilot). - map-of: reject odd-arity argument lists in the validator, and leave malformed map terms unchanged during normalization instead of silently dropping the unpaired key/value (Copilot). - ast_cmp: document why the Lit/Var arms are spelled out rather than delegating to `l.cmp(r)` -- Term intentionally has no derived Ord, and a derived Ord on App would order children by insertion order, which is the thing ast_cmp exists to avoid (saulshanabrook). - typechecking: `use` register_container_rebuild_from_spec instead of calling it via an absolute crate path (oflatt). - normalization is now per-container, with no "built-in container" special casing: TermDag carries no container knowledge (only the generic `ast_cmp` and a reusable `sort_terms_by_ast` helper). Each container sort normalizes its own term form in its constructor validator (set: sort+dedup; multiset: sort; map: collapse to flat `map-of`), exactly as a user-defined container would. The proof checker recomputes a container's canonical form by applying the validator registered for the term's head (collected from the e-graph's primitives), so built-in and user containers are handled identically (oflatt/saulshanabrook). - :internal-container-rebuild is a typed AST field (ast::ContainerRebuildSpec) rather than an opaque string: the egglog parser parses it once into the struct (ast/parse.rs) and Display serializes it, so register_container_rebuild_from_spec just reads the struct — no hand-rolled tokenizing or re-parsing in the proof pass; build constructs the struct directly (oflatt). - move the container-rebuild primitives + their runtime + the spec decoder out of proof_encoding.rs (2027 -> 1674 lines) into a new proofs/proof_container_rebuild.rs; proof_encoding.rs keeps only the encoder-side spec build. Pure relocation, no behavior change. - core-relations: split Rebuilder into a value-level ValueRebuilder supertrait plus the table-level Rebuilder. ContainerValue::rebuild_contents now takes &dyn ValueRebuilder, so ClosureRebuilder (the single-container rebuilder) drops its two unreachable!() table-level methods entirely (oflatt). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Follow-up cleanups for "Proof support for containers", addressing review comments from saulshanabrook, Copilot, and oflatt: - pair-first/pair-second validators: guard argument arity with `let [pair] = args else { return None }` before indexing, matching the other validators (Copilot). - map-of: reject odd-arity argument lists in the validator, and leave malformed map terms unchanged during normalization instead of silently dropping the unpaired key/value (Copilot). - ast_cmp: document why the Lit/Var arms are spelled out rather than delegating to `l.cmp(r)` -- Term intentionally has no derived Ord, and a derived Ord on App would order children by insertion order, which is the thing ast_cmp exists to avoid (saulshanabrook). - typechecking: `use` register_container_rebuild_from_spec instead of calling it via an absolute crate path (oflatt). - normalization is now per-container, with no "built-in container" special casing: TermDag carries no container knowledge (only the generic `ast_cmp` and a reusable `sort_terms_by_ast` helper). Each container sort normalizes its own term form in its constructor validator (set: sort+dedup; multiset: sort; map: collapse to flat `map-of`), exactly as a user-defined container would. The proof checker recomputes a container's canonical form by applying the validator registered for the term's head (collected from the e-graph's primitives), so built-in and user containers are handled identically (oflatt/saulshanabrook). - :internal-container-rebuild is a typed AST field (ast::ContainerRebuildSpec) rather than an opaque string: the egglog parser parses it once into the struct (ast/parse.rs) and Display serializes it, so register_container_rebuild_from_spec just reads the struct — no hand-rolled tokenizing or re-parsing in the proof pass; build constructs the struct directly (oflatt). - trim the spec to the minimum (oflatt): the per-element UF index names are dropped from every container's spec and recovered at register time from each element sort's :internal-uf (now `:internal-uf <constructor> [<index>]`, repopulating proof_state on re-parse). value_prim renamed internal_rebuild_prim. - move the container-rebuild primitives + their runtime + the spec decoder out of proof_encoding.rs (2027 -> 1674 lines) into a new proofs/proof_container_rebuild.rs; proof_encoding.rs keeps only the encoder-side spec build. Pure relocation, no behavior change. - core-relations: split Rebuilder into a value-level ValueRebuilder supertrait plus the table-level Rebuilder. ContainerValue::rebuild_contents now takes &dyn ValueRebuilder, so ClosureRebuilder (the single-container rebuilder) drops its two unreachable!() table-level methods entirely (oflatt). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Follow-up cleanups for "Proof support for containers", addressing review comments from saulshanabrook, Copilot, and oflatt: - pair-first/pair-second validators: guard argument arity with `let [pair] = args else { return None }` before indexing, matching the other validators (Copilot). - map-of: reject odd-arity argument lists in the validator, and leave malformed map terms unchanged during normalization instead of silently dropping the unpaired key/value (Copilot). - ast_cmp: document why the Lit/Var arms are spelled out rather than delegating to `l.cmp(r)` -- Term intentionally has no derived Ord, and a derived Ord on App would order children by insertion order, which is the thing ast_cmp exists to avoid (saulshanabrook). - typechecking: `use` register_container_rebuild_from_spec instead of calling it via an absolute crate path (oflatt). - normalization is now per-container, with no "built-in container" special casing: TermDag carries no container knowledge (only the generic `ast_cmp` and a reusable `sort_terms_by_ast` helper). Each container sort normalizes its own term form in its constructor validator (set: sort+dedup; multiset: sort; map: collapse to flat `map-of`), exactly as a user-defined container would. The proof checker recomputes a container's canonical form by applying the validator registered for the term's head (collected from the e-graph's primitives), so built-in and user containers are handled identically (oflatt/saulshanabrook). - :internal-container-rebuild is a typed AST field (ast::ContainerRebuildSpec) rather than an opaque string: the egglog parser parses it once into the struct (ast/parse.rs) and Display serializes it, so register_container_rebuild_from_spec just reads the struct — no hand-rolled tokenizing or re-parsing in the proof pass; build constructs the struct directly (oflatt). - trim the spec to the minimum (oflatt): the per-element UF index names and the per-container `<CSort>Proof` table names are dropped from every container's spec and recovered at register time from proof_state, which is repopulated on re-parse from existing per-sort annotations -- element sorts' :internal-uf (now `:internal-uf <constructor> [<index>]`) and container sorts' :internal-proof-func (now emitted for containers too). value_prim renamed internal_rebuild_prim. - move the container-rebuild primitives + their runtime + the spec decoder out of proof_encoding.rs (2027 -> 1674 lines) into a new proofs/proof_container_rebuild.rs; proof_encoding.rs keeps only the encoder-side spec build. Pure relocation, no behavior change. - core-relations: split Rebuilder into a value-level ValueRebuilder supertrait plus the table-level Rebuilder. ContainerValue::rebuild_contents now takes &dyn ValueRebuilder, so ClosureRebuilder (the single-container rebuilder) drops its two unreachable!() table-level methods entirely (oflatt). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Follow-up cleanups for "Proof support for containers", addressing review comments from saulshanabrook, Copilot, and oflatt: - pair-first/pair-second validators: guard argument arity with `let [pair] = args else { return None }` before indexing, matching the other validators (Copilot). - map-of: reject odd-arity argument lists in the validator, and leave malformed map terms unchanged during normalization instead of silently dropping the unpaired key/value (Copilot). - ast_cmp: document why the Lit/Var arms are spelled out rather than delegating to `l.cmp(r)` -- Term intentionally has no derived Ord, and a derived Ord on App would order children by insertion order, which is the thing ast_cmp exists to avoid (saulshanabrook). - typechecking: `use` register_container_rebuild_from_spec instead of calling it via an absolute crate path (oflatt). - normalization is now per-container, with no "built-in container" special casing: TermDag carries no container knowledge (only the generic `ast_cmp` and a reusable `sort_terms_by_ast` helper). Each container sort normalizes its own term form in its constructor validator (set: sort+dedup; multiset: sort; map: collapse to flat `map-of`), exactly as a user-defined container would. The proof checker recomputes a container's canonical form by applying the validator registered for the term's head (collected from the e-graph's primitives), so built-in and user containers are handled identically (oflatt/saulshanabrook). - :internal-container-rebuild is a typed AST field (ast::ContainerRebuildSpec) rather than an opaque string: the egglog parser parses it once into the struct (ast/parse.rs) and Display serializes it, so register_container_rebuild_from_spec just reads the struct — no hand-rolled tokenizing or re-parsing in the proof pass; build constructs the struct directly (oflatt). - trim the spec to the minimum (oflatt): it is now just `(container-rebuild-spec <prim> [<proof-prim>])`. Everything else is recovered at register time from proof_state, repopulated on re-parse from per-sort/global annotations rather than listed per-container: * per-element UF index names <- element sorts' :internal-uf (now `:internal-uf <constructor> [<index>]`); * per-container `<CSort>Proof` tables <- container sorts' :internal-proof-func (now emitted for containers too); * the global Congr/Trans/Sym/ContainerNormalize/Proof names <- a single :internal-proof-names record on the `Proof` sort. value_prim renamed internal_rebuild_prim. - proof extraction: parse_proof recognizes each extracted proof term's head by exact match against the recorded constructor names (EncodingNames) instead of fragile `head.contains("Congr")`-style substring guessing (oflatt). - move the container-rebuild primitives + their runtime + the spec decoder out of proof_encoding.rs (2027 -> 1674 lines) into a new proofs/proof_container_rebuild.rs; proof_encoding.rs keeps only the encoder-side spec build. Pure relocation, no behavior change. - core-relations: split Rebuilder into a value-level ValueRebuilder supertrait plus the table-level Rebuilder. ContainerValue::rebuild_contents now takes &dyn ValueRebuilder, so ClosureRebuilder (the single-container rebuilder) drops its two unreachable!() table-level methods entirely (oflatt). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Follow-up cleanups for "Proof support for containers", addressing review comments from saulshanabrook, Copilot, and oflatt: - pair-first/pair-second validators: guard argument arity with `let [pair] = args else { return None }` before indexing, matching the other validators (Copilot). - map-of: reject odd-arity argument lists in the validator, and leave malformed map terms unchanged during normalization instead of silently dropping the unpaired key/value (Copilot). - ast_cmp: document why the Lit/Var arms are spelled out rather than delegating to `l.cmp(r)` -- Term intentionally has no derived Ord, and a derived Ord on App would order children by insertion order, which is the thing ast_cmp exists to avoid (saulshanabrook). - typechecking: `use` register_container_rebuild_from_spec instead of calling it via an absolute crate path (oflatt). - normalization is now per-container, with no "built-in container" special casing: TermDag carries no container knowledge (only the generic `ast_cmp` and a reusable `sort_terms_by_ast` helper). Each container sort normalizes its own term form in its constructor validator (set: sort+dedup; multiset: sort; map: collapse to flat `map-of`), exactly as a user-defined container would. The proof checker recomputes a container's canonical form by applying the validator registered for the term's head (collected from the e-graph's primitives), so built-in and user containers are handled identically (oflatt/saulshanabrook). - :internal-container-rebuild is a typed AST field (ast::ContainerRebuildSpec) rather than an opaque string: the egglog parser parses it once into the struct (ast/parse.rs) and Display serializes it, so register_container_rebuild_from_spec just reads the struct — no hand-rolled tokenizing or re-parsing in the proof pass; build constructs the struct directly (oflatt). - trim the spec to the minimum (oflatt): it is now just `(container-rebuild-spec <prim> [<proof-prim>])`. Everything else is recovered at register time from proof_state, repopulated on re-parse from per-sort/global annotations rather than listed per-container: * per-element UF index names <- element sorts' :internal-uf (now `:internal-uf <constructor> [<index>]`); * per-container `<CSort>Proof` tables <- container sorts' :internal-proof-func (now emitted for containers too); * the global Congr/Trans/Sym/ContainerNormalize/Proof names <- a single :internal-proof-names record on the `Proof` sort. value_prim renamed internal_rebuild_prim. - proof extraction: parse_proof recognizes each extracted proof term's head by exact match against the recorded constructor names (EncodingNames) instead of fragile `head.contains("Congr")`-style substring guessing (oflatt). - move the container-rebuild primitives + their runtime + the spec decoder out of proof_encoding.rs (2027 -> 1674 lines) into a new proofs/proof_container_rebuild.rs; proof_encoding.rs keeps only the encoder-side spec build. Pure relocation, no behavior change. - core-relations: split Rebuilder into a value-level ValueRebuilder supertrait plus the table-level Rebuilder. ContainerValue::rebuild_contents now takes &dyn ValueRebuilder, so ClosureRebuilder (the single-container rebuilder) drops its two unreachable!() table-level methods entirely (oflatt). - docs: concision pass over the proof/term-encoding docs -- tightened proof_encoding.md (kept structure + examples) and shortened verbose doc comments throughout, and fixed two pre-existing broken intra-doc links (`Fact`, `Propostion`) in proof_format.rs (oflatt). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Address review feedback on container proof support

* Pare back out-of-scope doc churn from the review cleanup The container-proof review cleanup (PR #5) bundled a doc-concision pass that overreached: it rewrote prose in docs that only needed targeted updates, and reworded a doc comment unrelated to the PR. Restore those to their originals, keeping only the content the code actually forced. - proof_encoding.md: revert the Term Encoding / Globals / Proof Tracking prose rewrite. The net change vs the original doc is now +9/-10 lines -- the two paragraphs the code forced (per-container normalization replacing the shared normalize_container_term, and the trimmed :internal-container-rebuild annotation) -- instead of a 100/190 rewrite. - proof_format.rs: revert Justification::Rule's doc comment (unrelated to container proofs) to the original verbatim. - containers/mod.rs: shorten the verbose rebuild_val_with doc comment. Doc comments / markdown only; no code changes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Trim the container CHANGELOG entry to user-visible changes Drop the redundant proof phrasing (proofs shipped in 2.0.0) and the internal ContainerNormalize / rebuild_val_with details; keep the two user-visible extraction changes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Collect container proof normalizers from the sort trait Containers now declare their canonicalization validator via a new `container_term_normalizer` trait method instead of the proof extractor scanning every registered primitive for a validator. The method is optional (`None`, the default), so a future container does not have to support proofs right away. - Add `Sort::container_term_normalizer` (default None) and the same on the `ContainerSort` trait, delegated by `ContainerSortImpl`. - Implement it for Set/Map/Vec/MultiSet/Pair, returning the canonical constructor head and the same validator already registered for that constructor (reusing each sort's normalize helper). - Replace `TypeInfo::primitive_validators` (which scanned all primitives) with `TypeInfo::container_term_normalizers`, collecting only container sorts' declared normalizers. The proof checker still reads primitive validators directly via `prim.validator()`; this only changes how the container-normalize map handed to the proof format layer is built. 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>

oflatt and others added 7 commits June 8, 2026 15:55

oflatt and others added 6 commits June 22, 2026 13:52

remove container thing

5c09edc

rename

6fd3774

more rename

9ad16d2

fmt

6370bda

Merge remote-tracking branch 'origin/main' into pr-927-merge

fdef9fb

# Conflicts: # src/proofs/proof_encoding.rs

oflatt marked this pull request as ready for review June 23, 2026 16:46

oflatt requested a review from a team as a code owner June 23, 2026 16:46

oflatt requested review from Copilot and saulshanabrook and removed request for a team June 23, 2026 16:46

Copilot started reviewing on behalf of oflatt June 23, 2026 16:47 View session

Copilot AI reviewed Jun 23, 2026

View reviewed changes

saulshanabrook reviewed Jun 24, 2026

View reviewed changes

Comment thread src/proofs/proof_encoding_helpers.rs Outdated

Add set proof validators for containers

aaea8f8

This was referenced Jun 24, 2026

[codex] Add set proof validators for containers oflatt/egglog-duckdb#4

Merged

Allow hidden proof RHS lookups without forcing naive rules #931

Closed

saulshanabrook added 2 commits June 24, 2026 16:23

Use container sort predicate for proof support

e1e8652

Merge pull request #4 from saulshanabrook/codex/container-proof-followup

50f219c

[codex] Add set proof validators for containers