feat(Core): add loop termination checking via decreases measure annotations#581
feat(Core): add loop termination checking via decreases measure annotations#581
decreases measure annotations#581Conversation
Previously, the entry invariant assert was placed inside the `ite guard` then-branch, so when the guard was false at loop entry (0-iteration path) the invariant was never checked — a soundness bug. Fix: emit assert(I) unconditionally before the ite, followed by assume(I) to make I an explicit path condition on the 0-iteration path. Also replaces the brief module comment with a detailed passive encoding recipe documenting the two-phase (VC1/VC2) inductive invariant check. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…otations Introduces support for `decreases` clauses on `while` loops in the Core language: concrete syntax, passive encoding, CFG visualization, and verification condition generation. - Loop termination VCs (LoopElim.lean) - `decreases` concrete syntax (DDMTransform) - New generic abstractions (DL/Imperative layer): `HasIntOrder`, `HasIdent`, `HasInit` - CFG visualization of measures (StructuredToUnstructured.lean) - PrecondElim support (PrecondElim.lean) Also added a format instance for Core's experssions that shadows the generic `LExpr` formatter with `Core.formatExprs`. ## Tests updated in Loops.lean - New `measureFailExamplePgm`: `decreases n` on a `countUp` loop (wrong measure); confirms `measure_decrease_0` fails while other VCs pass. - `gaussPgm` and `nestedPgm` annotated with measures. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
|
Can the Goto conversion code please also be updated to include translation of these |
I thought that's already implemented here. Am I missing something? Before this PR, Core's AST supported the provision of a measure for a loop, but didn't expose it (no concrete syntax) and didn't check loop termination. My understanding was that the Goto conversion was future-proof for the decreases clause, but LMK if I misunderstood. |
My apologies, I indeed thought I had taken care of this, but then misunderstood the PR description as a new AST node. All good, no need for any Goto work then. |
… decreases clause Demonstrates that when a `decreases` measure uses integer division (`i / d`, which compiles to `Int.SafeDiv`), the verifier generates a division-by-zero precondition check for the measure expression, discharged by `requires (d > 0)`. Also adds a negative example showing the failures when the precondition is absent. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Previously, precondition assertions for partial functions in a `decreases` measure were only inserted before the loop. If the loop body mutates a variable used in the measure expression (e.g. `while e decreases y / x` with `x := ...` in the body), the precondition of the measure had to be re-checked after each iteration but wasn't, leaving a gap in verification. Apply the same treatment as guard preconditions: emit `loop_measure_end` assertions at the end of the loop body in addition to `loop_measure` assertions before the loop. Add a test (`precondElimMeasureBodyMutatesPgm`) that demonstrates the failure when the divisor is decremented in the body. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The loop termination feature (PR #581) added HasIdent, HasFvar, HasIntOrder, and HasNot constraints to stmtsToCFG, but the CFGToCProverGOTO test was not updated with the required instances. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
4 participants
Introduces support for
decreasesclauses onwhileloops in the Corelanguage: concrete syntax, passive encoding, CFG visualization, and verification
condition generation.
Before this PR, Core's AST supported the provision of a measure for a loop,
but didn't expose it (no concrete syntax) and the analysis didn't check
loop termination.
decreasesconcrete syntax (DDMTransform)HasIntOrder,HasIdent,HasInitAlso added a format instance for Core's experssions that shadows the generic
LExprformatter withCore.formatExprs.Tests updated in Loops.lean
measureFailExamplePgm:decreases non acountUploop (wrongmeasure); confirms
measure_decrease_0fails while other VCs pass.gaussPgmandnestedPgmannotated with measures.Co-Authored-By: Claude Sonnet 4.6 noreply@anthropic.com