Add eggcc container benchmark and proof coverage

Stacked on the subtree-sync branch. This preserves the final reviewed tree from codex/eggcc-container-benchmark while separating local benchmark, proof, CI, and review-fix changes from the subtree merge commits. The hash index ordering fix from egraphs-good/egglog#914 lives in the subtree-sync branch.

Author: saulshanabrook

.github/workflows/build.yml

@@ -41,7 +41,6 @@ jobs:
       - run: rustup component add clippy
       - uses: Swatinem/rust-cache@v2
       - run: cargo test --workspace
-      - run: cargo test --workspace proof
       - run: cargo clippy --workspace --all-targets -- -D warnings
 
   benchmark-smoke:
@@ -59,22 +58,29 @@ jobs:
       - run: uv run --locked ./bench.py --rounds 1 --treatments off --timeout-sec 120 --report .reports.ci.jsonl egglog/tests/integer_math.egg
 
   codspeed:
+    name: codspeed (${{ matrix.mode }})
     permissions:
       contents: read
       id-token: write
     runs-on: ubuntu-latest
     timeout-minutes: 20
+    strategy:
+      fail-fast: false
+      matrix:
+        mode:
+          - simulation
+          - memory
     steps:
       - run: echo "CARGO_INCREMENTAL=0" >> "$GITHUB_ENV"
       - uses: actions/checkout@v4
         with:
           persist-credentials: false
       - uses: taiki-e/install-action@v2
         with:
-          tool: cargo-codspeed@4.0.1
+          tool: cargo-codspeed@5.0.1
       - uses: Swatinem/rust-cache@v2
-      - run: cargo codspeed build -p egglog-experimental --bench files
+      - run: cargo codspeed build --measurement-mode ${{ matrix.mode }} -p egglog-experimental --bench files
       - uses: CodSpeedHQ/action@v4
         with:
-          run: cargo codspeed run files
-          mode: simulation
+          run: cargo codspeed run --measurement-mode ${{ matrix.mode }} files
+          mode: ${{ matrix.mode }}

AGENTS.md

@@ -17,11 +17,10 @@ session's `xhigh` reasoning effort instead.
 
 ## Tests
 
-Use this order for normal changes:
+Use this order for normal full validation:
 
 ```bash
 cargo test --workspace
-cargo test --workspace proof
 cargo clippy --workspace --all-targets -- -D warnings
 uv lock --check
 uv run --locked ruff format --check bench.py test_bench.py
@@ -30,31 +29,38 @@ uv run --locked mypy bench.py test_bench.py
 uv run --locked pytest -q
 ```
 
-For benchmark-runner changes, also smoke the CLI with a temporary report:
+For proof-focused changes, the filtered proof snapshot test is useful while
+iterating or when you want a focused proof rerun:
 
 ```bash
-uv run --locked ./bench.py --rounds 1 --treatments off --report .reports.smoke.jsonl \
-  egglog/tests/integer_math.egg
+cargo test --workspace --test files 'proofs/'
 ```
 
-For agent-readable benchmark smoke output, pipe report rows from stdout and keep
-runner status and build diagnostics on stderr:
+`proofs/` runs explicit `(prove ...)` fixtures under `tests/proofs` and every
+proof-compatible file under proof-testing mode, snapshotting generated proofs.
+It is a name-filtered subset of `cargo test --workspace`, so do not run it after
+a full workspace test unless you want a focused proof rerun.
+
+For benchmark-runner changes, smoke the public CLI entrypoint with a temporary,
+machine-readable report. Use stdout report mode so the run does not read or
+append to the default benchmark cache; runner status and build diagnostics stay
+on stderr.
 
 ```bash
-uv run --locked ./bench.py --rounds 1 --treatments off --report - \
+./bench.py --rounds 1 --treatments off --report - \
   egglog/tests/integer_math.egg > /tmp/egglog-encoding-bench-smoke.jsonl
 ```
 
 ## Benchmarking
 
 - Use `./bench.py` as the public benchmark entrypoint.
-- Do not pass egglog's `--save-report` during timed benchmark collection; it
-  changes the measured work.
 - Keep `.reports.jsonl` append-only and ignored by git.
 - Use `--report -` when report rows should be streamed to stdout instead of
   appended to a cache file.
 - Runner status output always goes to stderr, including Rich progress and
   summary tables.
+- Benchmark inputs should not contain executable `(prove ...)` commands; use
+  `(check ...)` in benchmark fixtures and cover proof extraction in proof tests.
 - Benchmark files are resolved relative to the command invocation directory,
   not relative to comparison targets.
 - Cache reuse is decided by binary SHA-256, file SHA-256, treatment, and

Cargo.lock

@@ -19,7 +19,7 @@ The development loop is:
 cargo test --workspace
 
 # Run proof-focused tests while iterating.
-cargo test --workspace proof
+cargo test --workspace --test files 'proofs/'
 
 # Run lint checks across the workspace.
 cargo clippy --workspace --all-targets
@@ -35,6 +35,15 @@ The root workspace includes both `egglog` and `egglog-experimental`.
 `egglog-experimental` depends on the workspace `egglog` crate, which keeps proof
 changes and downstream experimental behavior in the same reviewable unit.
 
+Proof-specific file tests use one filter prefix:
+
+- `proofs/`: explicit `(prove ...)` fixtures under `tests/proofs` plus every
+  proof-compatible file under proof-testing mode. Checks are treated as prove
+  commands and generated proofs are saved as snapshots.
+
+This filter is a subset of the full workspace test run. Use it for fast proof
+iteration and reserve `cargo test --workspace` for the final compatibility gate.
+
 ## Benchmarking
 
 The public benchmark entrypoint is an executable Python script:
@@ -120,10 +129,12 @@ If no files are provided, the default target benchmark suite is:
 - `egglog/tests/web-demo/rw-analysis.egg`
 - `egglog/tests/integer_math.egg`
 - `egglog/tests/web-demo/resolution.egg`
+- `egglog-experimental/tests/fixtures/eggcc-2mm-pass1-merge-old.egg`
 
-These four files are proof-compatible representative examples under the current
+These five files are proof-compatible representative examples under the current
 `egglog-experimental` CLI and run under the default `off`, `term`, and `proofs`
-treatment matrix.
+treatment matrix. The eggcc fixture is the heavy container/proof benchmark in
+the default suite.
 Relative file paths are resolved relative to the directory where `./bench.py`
 was invoked, not relative to each target checkout. The same file contents are
 used for every target, and `file.sha256` records the exact benchmark input.
@@ -513,17 +524,19 @@ Each benchmark report row records the binary hash used for that observation.
 
 ## CI
 
-CI runs on pull requests, manual dispatch, and pushes to `main`. It runs four
-jobs:
+CI runs on pull requests, manual dispatch, and pushes to `main`. It runs these
+job groups:
 
-- `python`: `uv lock --check`, ruff formatting, ruff linting, mypy, and pytest.
+- `python`: `uv lock --check`, ruff/mypy checks for the top-level benchmark
+  runner files, and pytest.
 - `rust`: workspace tests, proof-focused tests, and clippy.
 - `benchmark-smoke`: a one-round `./bench.py` run on
   `egglog/tests/integer_math.egg`.
 - `codspeed`: an in-process, proofs-only `egglog-experimental` benchmark
-  harness over a smaller representative file set. CodSpeed tracks proof-mode
-  movement without invoking `./bench.py`; the CLI benchmark report remains the
-  source for the full off/term/proofs comparison.
+  harness over a smaller representative file set, run through CodSpeed in both
+  simulation and memory modes. CodSpeed tracks proof-mode movement without
+  invoking `./bench.py`; the CLI benchmark report remains the source for the
+  full off/term/proofs comparison.
 
 Python checks are run as separate commands:
 

README.md

@@ -50,6 +50,7 @@
     "egglog/tests/web-demo/rw-analysis.egg",
     "egglog/tests/integer_math.egg",
     "egglog/tests/web-demo/resolution.egg",
+    "egglog-experimental/tests/fixtures/eggcc-2mm-pass1-merge-old.egg",
 )
 TARGET_SPEED_CAPTION = (
     "Ratio is target / baseline. Values below 1x are faster; above 1x are slower. Intervals are 95% CIs."
@@ -434,6 +435,25 @@ def resolve_files(raw_files: Sequence[str], invocation_cwd: Path) -> tuple[FileS
     return tuple(files)
 
 
+def file_contains_executable_prove_command(path: Path) -> bool:
+    for line in path.read_text(encoding="utf-8").splitlines():
+        stripped = line.lstrip()
+        if stripped.startswith(";"):
+            continue
+        if re.match(r"\(prove(?:\s|\))", stripped):
+            return True
+    return False
+
+
+def validate_spec(spec: BenchmarkSpec) -> None:
+    for file_spec in spec.files:
+        if file_contains_executable_prove_command(file_spec.absolute_path):
+            raise ValueError(
+                f"{file_spec.display_path} contains an explicit prove command; "
+                "benchmark files should use check so proof extraction is not included in timed runs"
+            )
+
+
 def resolve_report_destination(raw_report: str, invocation_cwd: Path) -> ReportDestination:
     if raw_report == "-":
         return ReportDestination(path=None, stream=sys.stdout)
@@ -1779,6 +1799,7 @@ def main(argv: Sequence[str] | None = None) -> int:
             rounds=args.rounds,
             timeout_sec=args.timeout_sec,
         )
+        validate_spec(spec)
         target_specs = args.target if args.target is not None else ["."]
         target_requests = tuple(parse_target(raw) for raw in target_specs)
         rows = load_report(report_destination)

bench.py

@@ -32,4 +32,5 @@ log = "0.4"
 [dev-dependencies]
 divan = { workspace = true }
 glob = "0.3.1"
+insta = "1.40"
 libtest-mimic = "0.8.1"

egglog-experimental/Cargo.toml

@@ -190,6 +190,22 @@ enum BoundMergeKind {
     Max,
 }
 
+impl BoundMergeKind {
+    fn keep_i64_old(self, old: i64, new: i64) -> bool {
+        match self {
+            BoundMergeKind::Min => old <= new,
+            BoundMergeKind::Max => old >= new,
+        }
+    }
+
+    fn keep_bool_old(self, old: bool, new: bool) -> bool {
+        match self {
+            BoundMergeKind::Min => !old || new,
+            BoundMergeKind::Max => old || !new,
+        }
+    }
+}
+
 fn bound_merge<'a, 'db>(
     state: PureState<'a, 'db>,
     args: &[Value],
@@ -225,19 +241,13 @@ fn bound_merge<'a, 'db>(
         (EitherData::Left(old_int), EitherData::Left(new_int)) => {
             let old_int = state.base_values().unwrap::<i64>(old_int);
             let new_int = state.base_values().unwrap::<i64>(new_int);
-            let keep_old = match kind {
-                BoundMergeKind::Min => old_int <= new_int,
-                BoundMergeKind::Max => old_int >= new_int,
-            };
+            let keep_old = kind.keep_i64_old(old_int, new_int);
             Some(if keep_old { args[0] } else { args[1] })
         }
         (EitherData::Right(old_bool), EitherData::Right(new_bool)) => {
             let old_bool = state.base_values().unwrap::<bool>(old_bool);
             let new_bool = state.base_values().unwrap::<bool>(new_bool);
-            let keep_old = match kind {
-                BoundMergeKind::Min => !old_bool || new_bool,
-                BoundMergeKind::Max => old_bool || !new_bool,
-            };
+            let keep_old = kind.keep_bool_old(old_bool, new_bool);
             Some(if keep_old { args[0] } else { args[1] })
         }
         _ => None,
@@ -313,17 +323,11 @@ fn validate_maybe_either_i64_bool_merge(
         (BoundTerm::Dead, _) => Some(*old),
         (_, BoundTerm::Dead) => Some(*new),
         (BoundTerm::Int(old_int), BoundTerm::Int(new_int)) => {
-            let keep_old = match kind {
-                BoundMergeKind::Min => old_int <= new_int,
-                BoundMergeKind::Max => old_int >= new_int,
-            };
+            let keep_old = kind.keep_i64_old(old_int, new_int);
             Some(if keep_old { *old } else { *new })
         }
         (BoundTerm::Bool(old_bool), BoundTerm::Bool(new_bool)) => {
-            let keep_old = match kind {
-                BoundMergeKind::Min => !old_bool || new_bool,
-                BoundMergeKind::Max => old_bool || !new_bool,
-            };
+            let keep_old = kind.keep_bool_old(old_bool, new_bool);
             Some(if keep_old { *old } else { *new })
         }
         _ => None,

egglog-experimental/src/container_primitives.rs

@@ -82,15 +82,15 @@ fn new_experimental_egraph_with_options(extended_run_schedule: bool) -> EGraph {
 }
 
 pub fn new_experimental_egraph_with_term_encoding() -> EGraph {
-    let mut egraph = EGraph::new_with_term_encoding();
-    add_experimental_extensions(&mut egraph, false);
-    egraph
+    new_experimental_egraph_for_proofs().with_term_encoding_enabled()
 }
 
 pub fn new_experimental_egraph_with_proofs() -> EGraph {
-    let mut egraph = EGraph::new_with_proofs();
-    add_experimental_extensions(&mut egraph, false);
-    egraph
+    new_experimental_egraph_for_proofs().with_proofs_enabled()
+}
+
+pub fn new_experimental_egraph_with_proof_testing() -> EGraph {
+    new_experimental_egraph_with_proofs().with_proof_testing()
 }
 
 fn add_experimental_extensions(egraph: &mut EGraph, extended_run_schedule: bool) {

egglog-experimental/src/lib.rs

@@ -190,13 +190,7 @@ impl ContainerSort for MaybeSort {
                         (Some(old_value), Some(new_value)) => {
                             let old_f = state.base_values().unwrap::<F>(old_value).0.0;
                             let new_f = state.base_values().unwrap::<F>(new_value).0.0;
-                            let tolerance = tol.0.0.abs();
-                            let merged =
-                                old_f == new_f ||
-                                (old_f == 0.0 && new_f == -0.0) ||
-                                (old_f == -0.0 && new_f == 0.0) ||
-                                (old_f - new_f).abs() <= tolerance;
-                            merged.then_some(old)
+                            maybe_f64_values_merge_with_tol(old_f, new_f, tol.0.0).then_some(old)
                         }
                     }
                 }},
@@ -253,16 +247,19 @@ fn validate_maybe_f64_merge_with_tol(termdag: &mut TermDag, args: &[TermId]) ->
             let Term::Lit(Literal::Float(tolerance)) = termdag.get(*tol) else {
                 return None;
             };
-            let tolerance = tolerance.0.abs();
-            let merged = old_f == new_f
-                || (old_f == 0.0 && new_f == -0.0)
-                || (old_f == -0.0 && new_f == 0.0)
-                || (old_f - new_f).abs() <= tolerance;
-            merged.then_some(*old)
+            maybe_f64_values_merge_with_tol(old_f, new_f, tolerance.0).then_some(*old)
         }
     }
 }
 
+fn maybe_f64_values_merge_with_tol(old_f: f64, new_f: f64, tolerance: f64) -> bool {
+    let tolerance = tolerance.abs();
+    old_f == new_f
+        || (old_f == 0.0 && new_f == -0.0)
+        || (old_f == -0.0 && new_f == 0.0)
+        || (old_f - new_f).abs() <= tolerance
+}
+
 fn maybe_f64(termdag: &TermDag, term: TermId) -> Option<Option<f64>> {
     match termdag.get(term) {
         Term::App(head, children) if head == "maybe-none" && children.is_empty() => Some(None),

egglog-experimental/src/maybe.rs

@@ -31,6 +31,12 @@ fn run_fixture_with_proofs(fixture_name: &str) -> String {
 fn eggcc_2mm_full_export_uses_container_helpers() {
     let (_fixture, program) = read_fixture("eggcc-2mm-pass1-merge-old.egg");
 
+    let non_comment_program = program
+        .lines()
+        .filter(|line| !line.trim_start().starts_with(';'))
+        .collect::<Vec<_>>()
+        .join("\n");
+
     for required in [
         "pair-min-by-second-i64",
         "maybe-either-i64-bool-min",
@@ -40,16 +46,27 @@ fn eggcc_2mm_full_export_uses_container_helpers() {
         "either-right",
         "either-unwrap-left",
         "either-unwrap-right",
+        "(check (FunctionHasType \"main\"",
     ] {
         assert!(
-            program.contains(required),
+            non_comment_program.contains(required),
             "fixture should exercise {required}"
         );
     }
 
+    for required in [
+        "https://github.com/egraphs-good/eggcc/pull/796",
+        "https://github.com/egraphs-good/egglog-experimental/pull/56",
+    ] {
+        assert!(
+            program.contains(required),
+            "fixture should document {required}"
+        );
+    }
+
     assert!(
-        !program.contains(":no-merge"),
-        "full eggcc export should not use :no-merge"
+        !non_comment_program.contains(":no-merge"),
+        "full eggcc export should not use :no-merge declarations"
     );
     assert!(
         program.contains(":merge old"),