LoopElim should be a phase, not built in into the partial evaluator#748
Merged
MikaelMayer merged 13 commits intomainfrom Apr 4, 2026
Merged
Conversation
…uator (#747) Remove loop elimination from Procedure.eval (the partial evaluator) and add it as an independent program transformation phase that runs after other transforms (PrecondElim, CallElim) but before type checking and partial evaluation. - Remove removeLoopsM call and LoopElim import from ProcedureEval.lean - Add Core.loopElim function in Verifier.lean as a reusable helper - Call loopElim in Core.verify before typeCheckAndPartialEval - Call loopElim in MetaVerifier.genVCs for the MetaVerifier path - Delegate SimpleAPI.loopElimUsingContract to Core.loopElim
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Moving loop elimination out of ProcedureEval removed the transitive public import chain that made PipelinePhase types available in Verifier.lean. Add a direct public import to restore access to AbstractedPhase, PipelinePhase, and related definitions.
This comment was marked as resolved.
This comment was marked as resolved.
loopElimPipelinePhase now performs the actual loop elimination transform instead of being an identity. This ensures the pipeline phase system properly tracks that loop elimination is an over-approximation that should demote SAT models to unknown. - Moved loopElim to LoopElim.lean alongside its pipeline phase - Updated loopElimPipelinePhase.transform to use the real transform - Integrated loop elimination into both verify code paths via pipeline - Removed the separate loopElim step that ran outside the pipeline
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
MikaelMayer
commented
Apr 3, 2026
MikaelMayer
commented
Apr 3, 2026
Both the none and some procs paths now use corePipelinePhases to run transforms, eliminating the duplicated manual transform logic. callElimPipelinePhase is conditional on procs being provided. Removed outdated comment justifying loop elimination placement.
atomb
approved these changes
Apr 3, 2026
Contributor
atomb
left a comment
atomb
left a comment
There was a problem hiding this comment.
Nice improvement! One small nit: could you change the title of the PR to state what it changes rather than what the problem used to be? The current title makes it look like an issue rather than a PR.
tautschnig
approved these changes
Apr 3, 2026
MikaelMayer
deleted the
issue-747-loopelim-should-be-a-phase-not-built-in
branch
Contributor
Author
That title made me uneasy but thanks for pointing out why. I'll be more careful next time. Feel free next time to deactivate auto-merge so that I can react accordingly. |
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
3 participants
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.
Loop elimination was tightly coupled with the partial evaluator (
Procedure.eval), making it harder to prove soundness, compose with other optimizations, or replace with alternative strategies (e.g., loop unrolling).This PR extracts loop elimination into a standalone program transformation phase (
Core.loopElim) that runs after other transforms but before type checking and partial evaluation. The phase is integrated into thePipelinePhasesystem so that:loopElimPipelinePhase.transformperforms the actual loop eliminationloopElimPipelinePhase.phase.getValidationdemotes SAT models to unknown for obligations whose path includes loop-elimination labels, since loop elimination is an over-approximationPipelinePhaseBoth verification paths (all procedures and targeted verification) now use the same
corePipelinePhaseslist to run transforms, eliminating duplicated manual transform logic. Each phase determines its own applicability via the phase list construction.The partial evaluator no longer needs to know about loops — it expects them to be eliminated beforehand.
All existing tests pass.
Fixes #747