Fix proof-test coverage for computed-value verifier failures

[saulshanabrook]

Summary

• make proof-support detection reuse the existing term-encoding resolver, which checks each command against the live scoped TypeInfo
• add a six-line computed-BigRat verifier reproducer and an equivalent positive i64 control
• run the reduced BigRat case and full Herbie as direct expected-failure regressions, so neither can be silently excluded by the support gate
• retain direct Math proof testing while omitting its separate desugared replay failure

Why the tests missed Herbie

The file harness previously resolved a complete source file with a normal e-graph and then checked every command against the final TypeInfo. Information introduced inside push/pop scopes had already been discarded, so proof-compatible files such as Herbie were classified as unsupported and their proof-testing trials were never generated.

The implementation change is intentionally small: enable the existing term-encoding path while probing support and return whether that resolver succeeds. That path already performs the live-scope proof-support checks. Across all current core and experimental fixtures, its classification matches the intended proof-testing inventory.

Remaining verifier bug

Once selected, Herbie reaches an existing fail-closed verifier error. Primitive BigRat values reconstruct as application-shaped terms, while the encoder gives the result a reflexive Fiat proof that the checker accepts only for literals or values established by globals.

This PR does not weaken the verifier to accept arbitrary application-shaped Fiat proofs. A narrow future repair could preserve authenticated sort information and allow only canonical BigInt/BigRat representations that exactly round-trip through their sort normalizers. A general repair would need a checked Compute certificate carrying the concrete overloaded primitive signature, typed arguments, child proof evidence, and claimed result, followed by deterministic validator replay.

That broader change is difficult because the current proof conversion discards typed wrappers, primitive names are overloaded, child provenance must be authenticated, and the new evidence would have to survive proof printing, simplification, child traversal, and term remapping.

PR #22 comparison

PR #22 fixes a distinct desugared Math scoped-global replay bug by changing global representation and making witness-row extraction deterministic. Its head still fails both the reduced BigRat case and full Herbie with the same InvalidFiat class, so those broader changes are not ported here.

Validation

• make proof-tests
• make check
• git diff --check

Summary by CodeRabbit

• Documentation

  • Updated the Files workload table to clarify that all 14 Herbie workload checks pass and that proof testing is covered separately.

• Bug Fixes

  • Improved proof-support detection to provide more reliable proof-testing results.
  • Added handling for known proof-testing failures and unsupported replay scenarios.

• Tests

  • Expanded proof-testing coverage with expected-failure checks.
  • Added validation to ensure proof failures report the expected error type.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro

Run ID: 6362940b-e773-481f-bce1-277f5ee80117

📥 Commits

Reviewing files that changed from the base of the PR and between 1cc0e8a and b085479.

⛔ Files ignored due to path filters (4)

• egglog/tests/proofs/bigrat-primitive-result.egg is excluded by !**/*.egg
• egglog/tests/proofs/i64-primitive-result.egg is excluded by !**/*.egg
• egglog/tests/snapshots/files__proof_unsupported_files.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proofs__i64_primitive_result_proof_testing.snap is excluded by !**/*.snap

📒 Files selected for processing (3)

• README.md
• egglog/src/proofs/proof_encoding_helpers.rs
• egglog/tests/files.rs

---

📝 Walkthrough

Walkthrough

Proof support detection now enables term encoding during resolution. File-based tests skip known proof-testing failures, validate their panic messages, and update proof snapshot coverage. The Herbie workload description now separates workload checks from proof-testing coverage.

Changes

Proof-testing behavior

Layer / File(s)	Summary
Proof support resolution egglog/src/proofs/proof_encoding_helpers.rs	Proof support is determined by resolving the program with term encoding enabled.
Fixture scheduling and expected-failure validation egglog/tests/files.rs, README.md	Known failures and selected desugared replay cases are excluded from generated proof-testing runs; dedicated tests assert the Fiat proof claims panic, and the Herbie workload description reflects separate proof-testing coverage.

Estimated code review effort: 2 (Simple) | ~10 minutes

Possibly related PRs

• saulshanabrook/egglog-encoding#14: Updates the overlapping proof snapshot-disabled fixture list.

Suggested reviewers: oflatt

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title accurately reflects the main change: fixing proof-test coverage around computed-value verifier failures.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[codspeed-hq]

Merging this PR will not alter performance

✅ 6 untouched benchmarks

---

_{Comparing codex/herbie-proof-test-gap (b085479) with main (1cc0e8a)}