Add support for void loop invariant functions with ensures#537
Merged
andreistefanescu merged 17 commits intomainfrom Feb 26, 2026
Merged
Add support for void loop invariant functions with ensures#537andreistefanescu merged 17 commits intomainfrom
andreistefanescu merged 17 commits intomainfrom
Conversation
Loop invariant functions can now be void and express invariants via ensures() calls instead of returning a bool. The void function's bytecodes are inlined into the target function so that ensures/requires substitution in the loop analysis transform works unchanged. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Mark spec functions (requires, ensures, asserts) as non-aborting in the no-abort analysis, and substitute ensures/asserts to requires in translate_function_no_abort so they become assumptions during abort checking. Also revert the is_loop_invariant_function guard in check_abort_check_scope. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Remove pre-extracted void_inv_data map and instead look up invariant function data directly from targets inside inline_void_invariant. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Only generate a jump label and emit it when there are multiple Ret bytecodes (early returns). The last Ret is always dropped rather than converted to a jump. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Skip offsets never contain Ret bytecodes and the last Ret is always the final instruction, so just count Rets directly. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Find the last Ret by position rather than assuming it is the last instruction, so the logic is correct even if void functions omit a trailing Ret. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Check for Ret instructions before the last instruction using a slice instead of tracking indices. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Put targets as the 3rd argument after func_env and data. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
andreistefanescu
requested review from
andrii-a8c,
Copilot,
danilych and
msaaltink
Contributor
There was a problem hiding this comment.
Pull request overview
This PR adds support for void loop invariant functions that express invariants through ensures() calls instead of returning a boolean value. The implementation inlines the bytecodes of void invariant functions into the target function, allowing the existing ensures/requires substitution logic in the loop analysis transform to work unchanged.
Changes:
- Loop invariant functions can now return void (0 return values) in addition to bool
- Void invariant functions are inlined into target functions rather than called
- Boogie backend substitutes ensures/asserts with requires for no_abort function translations
Reviewed changes
Copilot reviewed 8 out of 8 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| crates/move-stackless-bytecode/src/move_loop_invariants.rs | Core implementation: handles void invariant validation, inlining logic with bytecode remapping, temp allocation, and label substitution |
| crates/move-stackless-bytecode/src/stackless_bytecode.rs | Adds replace_attr_id method to support attribute replacement during bytecode inlining |
| crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs | Substitutes ensures/asserts operations with requires in no_abort translations to support inlined void invariants |
| crates/sui-prover/tests/inputs/loop_invariant/external_void.ok.move | Test cases for valid void invariant functions with various scenarios (simple, multiple ensures, old values, loop constructs) |
| crates/sui-prover/tests/inputs/loop_invariant/external_void_wrong.fail.move | Test case for incorrect void invariant that should fail verification |
| crates/sui-prover/tests/snapshots/loop_invariant/external_void.ok.move.snap | Snapshot showing successful verification for void invariants |
| crates/sui-prover/tests/snapshots/loop_invariant/external_void_wrong.fail.move.snap | Snapshot showing expected verification errors for incorrect void invariants |
| crates/sui-prover/tests/snapshots/loop_invariant/external_returns.fail.move.snap | Updated error message to reflect "at most one" instead of "exactly one" return value |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
When the target function has a &mut T arg and the invariant function expects &T (eliminated to T by EliminateImmRefs), emit ReadRef inside the invariant's attr range so loop analysis properly duplicates it in the assert-havoc-assume pattern. Adds test4 with &mut u128. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
EliminateImmRefs already removes ReadRef from the invariant's bytecodes, so there are no ReadRef instructions on dereferenced args to skip. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Return empty vec instead of panicking when all bytecodes are param-copy Assigns (skipped) and a trailing Ret (skipped). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Collaborator
|
What happens if loop invariant returns a bool but also has some ensures clauses? whether that's an error or allowed, a test case would be useful. |
Contributor
Author
|
@msaaltink good catch, it shouldn't be allowed, but currently there's no check |
Bool invariants must not transitively call requires, ensures, or asserts. Void invariants must not transitively call requires or asserts (only ensures is allowed). Adds failing tests for both cases. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Contributor
Author
|
@msaaltink fixed, I think you may like this. |
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
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 invariant functions can now be void and express invariants via ensures() calls instead of returning a bool. The void function's bytecodes are inlined into the target function so that ensures/requires substitution in the loop analysis transform works unchanged.