egglog Container Proofs

egglog is a Rust engine combining equality saturation with Datalog. Programs declare terms, rules and rewrites; the engine grows an e-graph until it can answer queries or extract the best equivalent term. Its proof mode gives every derived fact a proof an independent checker can replay, but until upstream #927 it rejected container sorts (Vec, Set, Map, MultiSet, Pair). The e-graph never unions containers directly: it rebuilds them into normal form whenever their elements' equivalence classes merge. After a union of A and B, {A, B} as a set collapses to one element, and rows holding those containers become congruent. Proof mode must reproduce each consequence and justify it from terms alone.

The agent makes all five container sorts, including nested ones, work under term encoding, proof encoding and proof testing with the same observable results as the default e-graph. Containers work wherever the language allows them, including rule bodies, and every fact from container rebuilding needs a proof the existing checker accepts. The proof format is pinned: containers appear as constructor applications in canonical structural order independent of value ids, maps use a flat map-of primitive, and a normalization step proves each rebuilt container equal to its sorted and deduplicated form. No existing test may be removed or weakened.

The offline sandbox (4 CPUs, 16 GB, 8 hours) holds an egglog checkout at commit 4141a970, the pinned Rust 1.91.0 toolchain, cargo-nextest and every locked crate, a prebuilt release build and example programs. Upstream tests for the feature, the program generator and reference build are held out.

The committed tree is rebuilt from a clean checkout with existing integration tests and snapshots restored. The whole suite must pass, and hidden upstream tests must pass. Secret-seeded programs cover nine families, from each container sort and nesting to multi-round rules and containers in rule bodies. Each runs in default, term-encoding, proof and proof-testing modes, with results compared against the upstream implementation and every proof replayed by an independent checker. A pass requires every family to reach 90%.