Address review feedback on container proof support

[oflatt-claude]

Follow-up cleanups for egraphs-good#927 ("Proof support for containers"), addressing review comments from @saulshanabrook, Copilot, and @oflatt. Targets the oflatt-container-proofs branch so it stacks on top of the PR.

Correctness / defensive (Copilot)

• pair-first / pair-second validators (src/sort/pair.rs): guard arity with let [pair] = args else { return None } before indexing, matching pair_validator and the other validators. Can't trigger today (arity is enforced by typechecking), but no longer relies on that.
• odd-arity map-of (src/sort/map.rs, src/termdag.rs): map_of_validator now rejects odd-length argument lists, and normalization leaves a malformed map term unchanged rather than silently dropping the unpaired key/value (collect_map_entries returns None on a malformed spine instead of truncating via chunks(2)).

Cleanup (saulshanabrook / oflatt)

• ast_cmp docs (src/termdag.rs): explain why the Lit/Var arms are spelled out instead of l.cmp(r) — Term intentionally has no derived Ord, and a derived Ord on App would order children by insertion order, which is exactly what ast_cmp exists to avoid. Only the App arm needs the DAG recursion.
• normalization (src/termdag.rs): replaced the hard-coded head-name match in normalize_container_term with a ContainerNormalization strategy enum + a single builtin_container_normalization(head) source of truth, and extracted a reusable sort_terms_by_ast helper that custom container sorts can call (e.g. after their own dedup). Behavior is unchanged for the built-ins.
  • Note: the proof checker is deliberately sort-agnostic (it works on a TermDag + the program, no Sorts), so normalization stays keyed by head rather than dispatched through a per-sort trait method. Supporting a user-defined canonicalizing container in proofs would mean threading a head→strategy map into the checker; documented as future work.
• absolute path (src/typechecking.rs): use crate::proofs::proof_encoding::register_container_rebuild_from_spec; instead of the inline crate::… path.
• :internal-container-rebuild spec (src/proofs/proof_encoding.rs): build and parse the spec as an egglog s-expression through the existing parser (SexpParser / Sexp::expect_*), like the rest of the proof pass, instead of pushing and re-splitting space-separated tokens with positional next(&mut i) / count prefixes. Pairs are sorted for a deterministic spec.

Rebuilder simplification (oflatt)

• core-relations: split Rebuilder into a value-level ValueRebuilder supertrait (rebuild_val + defaulted rebuild_slice) and the table-level Rebuilder: ValueRebuilder (hint_col / rebuild_buf / rebuild_subset). ContainerValue::rebuild_contents now takes &dyn ValueRebuilder, so ClosureRebuilder (the single-container rebuilder) drops both of its unreachable!() table-level methods — the "value-level only" guarantee is now type-level. Canonicalizer (union-find) implements both; the call sites in apply_rebuild_* upcast &dyn Rebuilder → &dyn ValueRebuilder automatically.

Testing

• cargo test --release --workspace (+ doctests): pass.
• cargo clippy --tests -- -D warnings: clean.
• cargo fmt --check: clean.
• No snapshot changes (the normalization refactor is behavior-preserving and the spec string isn't snapshotted).

🤖 Generated with Claude Code

[Copilot]

Pull request overview

This PR is a follow-up cleanup to the container proof support work (stacked on egraphs-good#927), focusing on making container rebuild/proof metadata round-trip reliably through parsing/serialization, tightening validator defensiveness, and simplifying rebuild trait boundaries (value-level vs table-level).

Changes:

• Refactors container rebuild registration/spec handling: moves registration into a dedicated module, stores rebuild metadata as a structured ContainerRebuildSpec s-expression, and restores needed UF/proof constructor metadata via proof_state.
• Reworks container-term canonicalization to be validator-driven (plus small shared helpers like TermDag::sort_terms_by_ast), including rejecting malformed map-of terms rather than truncating.
• Splits Rebuilder into ValueRebuilder + Rebuilder to make “value-only rebuilders” type-safe and remove unreachable table-level methods from single-container rebuild paths.

Reviewed changes

Copilot reviewed 30 out of 30 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
src/typechecking.rs	Restores UF/proof metadata into proof_state during sort typechecking; adds TypeInfo::primitive_validators; uses new container rebuild registration path.
src/termdag.rs	Removes hard-coded container normalization; adds sort_terms_by_ast helper and clarifies ast_cmp docs.
src/sort/vec.rs	Switches container rebuild hook to &dyn ValueRebuilder.
src/sort/set.rs	Implements explicit canonical set term normalization using sort_terms_by_ast + dedup; updates validators/canonical form.
src/sort/pair.rs	Switches to ValueRebuilder; makes pair-first/pair-second validators arity-safe.
src/sort/multiset.rs	Switches to ValueRebuilder; adds explicit multiset term normalization helper.
src/sort/mod.rs	Re-exports ValueRebuilder instead of Rebuilder from core_relations.
src/sort/map.rs	Switches to ValueRebuilder; refactors and hardens map term normalization (rejects malformed spines/odd arity).
src/sort/fn.rs	Switches container rebuild hook to &dyn ValueRebuilder.
src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap	Updates snapshot for new :internal-uf annotation shape including UF index table.
src/proofs/proof_simplification.rs	Uses new ProofStore::normalize_container instead of TermDag::normalize_container_term.
src/proofs/proof_format.rs	Stores encoding names in RawProofStore; switches proof constructor recognition to exact match; threads container normalizers and adds normalize_container.
src/proofs/proof_extraction.rs	Passes primitive_validators() into proof store creation for container normalization in checking/simplification.
src/proofs/proof_encoding.rs	Removes in-file container rebuild registration/primitive implementations; emits richer UF/proof-func metadata for re-parse.
src/proofs/proof_encoding.md	Updates/condenses documentation and aligns container normalization explanation with validator-driven approach.
src/proofs/proof_encoding_helpers.rs	Records global proof constructor names on the Proof sort via :internal-proof-names.
src/proofs/proof_container_rebuild.rs	New module containing container rebuild registration and the rebuild primitives (value + proof).
src/proofs/proof_checker.rs	Recomputes container normalization via ProofStore::normalize_container (validator-driven) when checking ContainerNormalize.
src/proofs/mod.rs	Exposes new proof_container_rebuild module.
src/prelude.rs	Threads new proof_constructors field when constructing Sort commands.
src/lib.rs	Restores UF ctor/index and global proof constructor names into proof_state when running sort commands.
src/ast/parse.rs	Parses :internal-container-rebuild as a structured s-expression; parses :internal-uf as ctor + optional index; adds :internal-proof-names.
src/ast/mod.rs	Introduces ContainerRebuildSpec + ProofConstructorNames; extends sort command representation and printing accordingly.
src/ast/desugar.rs	Threads proof_constructors through desugaring pipeline.
egglog-bridge/src/tests.rs	Updates tests for ValueRebuilder rename/split.
core-relations/src/uf/mod.rs	Makes Canonicalizer implement ValueRebuilder; updates Rebuilder impl to rely on the supertrait for value rebuild.
core-relations/src/table_spec.rs	Introduces ValueRebuilder; makes Rebuilder: ValueRebuilder and provides default rebuild_slice.
core-relations/src/lib.rs	Re-exports ValueRebuilder.
core-relations/src/containers/tests.rs	Updates fake rebuilders/tests to the ValueRebuilder + Rebuilder split.
core-relations/src/containers/mod.rs	Updates ContainerValue::rebuild_contents to accept &dyn ValueRebuilder; simplifies closure-based rebuilder to value-level only.

---

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