proof: remove the lemma-discovery enumerator, keep the committed-lemma consumer#587
Merged
Conversation
…a consumer The brute-force discovery enumerator (`aver proof --discover` / `--emit-laws`) never earned its keep: it closes none of the hard unproven tasks directly, the proof-corpus coverage metric never invokes it, and the agent-driven Method path deliberately forbids it (proposed laws must close self-contained, not via enumeration). Everything it "delivered" was actually the consumer's work — it only guessed a helper lemma that a human or the Method writes by hand. Cut the enumerator and everything exclusive to it: the term/equation enumerator, the VM refutation filter, the structural-brick generator, the born-as-Aver `--emit-laws` sidecar, the candidate ranking/report, and the `--discover` / `--emit-laws` / `--emit-laws-to` flags plus their proof-command plumbing. The discovery corpus test and the enumerator unit tests go with them. Keep the consumer (`committed.rs` + the surface hash + the SimpOverLemmas hook in `cmd_proof`): the piece that actually flips a law to `universal` by re-pinning an earlier proven law (or any committed lemma file) as a simp rule. It has zero dependency on the enumerator and is the substrate the Method feeds, so a normal `aver proof` and the law-feeds-law / dependency-module / decomposed-task proofs are unchanged (proof_spec stays green). The full enumerator (including the unreleased `calculate.rs` Lemma-Calculation seed) is preserved at tag `archive/lemma-discovery-enumerator` for revival. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`LawProofCone::types` (the field, its `compute` population, the `types()` accessor, and the `collect_named_types_in_annotation` helper) existed only to feed the type-directed candidate generator inside the discovery enumerator. With the enumerator removed, all of it is dead — `cargo clippy --lib -- -D warnings` (the CI gate) rejects the never-read field and never-used method. The kept consumer (`law_helper_unfolds` / SimpOverLemmas) uses only `pure_fns`. Remove the whole `types` chain; `LawProofCone` now carries just `pure_fns`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Removes the brute-force discovery enumerator and everything exclusive to it; keeps the consumer that actually closes laws. −7,471 / +55 LOC.
Why
--discover— so its contribution to any reported number is unmeasured-and-zero.--discover(proposed laws must close self-contained). So the enumerator is dead weight to the strategy actually being pursued, not a dependency of it.decomposed/already carries those lemmas inline, no discovery).Cut (enumerator source + tests)
lemma_discovery/{enumerate,vm_filter,bricks,emit_laws,calculate,render}.rs, the--discover/--emit-laws/--emit-laws-toflags, theircmd_proofplumbing (prove_discovered_lemmas_lean,cmd_proof_emit_laws,lake_reverify_appended), the discovery corpus test, the enumerator unit tests, theDISCOVER=1corpus path, and the docs/CHANGELOG mentions.Kept (the consumer — load-bearing)
committed.rs+ the surface hash + theSimpOverLemmashook incmd_proof: the piece that flips a law touniversalby re-pinning an earlier proven law (or any committed lemma file) as a simp rule. Zero dependency on the enumerator; it is the substrate the Method feeds.Verification
Normal
aver proofis unchanged; the law-feeds-law, dependency-module, and decomposed-task proofs all still pass.cargo build,cargo build --features wasm,wasip2,clippy --features wasm,wasip2, andcargo test --test proof_spec(172 passed, 0 failed) are all green. All test targets compile.Reversible
The full enumerator (incl. the unreleased
calculate.rsLemma-Calculation seed) is preserved at tagarchive/lemma-discovery-enumerator.🤖 Generated with Claude Code