Skip to content

Add support for loop assigns in loop contracts #4174

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 5 commits into from
Jun 30, 2025
Merged

Add support for loop assigns in loop contracts #4174

merged 5 commits into from
Jun 30, 2025

Conversation

thanhnguyen-aws
Copy link
Contributor

This PR adds support for loop assigns in loop contracts.

Resolves #3871
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@thanhnguyen-aws thanhnguyen-aws requested a review from a team as a code owner June 23, 2025 15:10
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jun 23, 2025
tautschnig
tautschnig approved these changes Jun 23, 2025
View reviewed changes
@carolynzech
Copy link
Contributor

Could you update our tutorial documentation along with this?

@carolynzech
Copy link
Contributor

carolynzech commented Jun 23, 2025 •
edited
Loading

Also, I'm curious why we're calling it loop_assigns rather than loop_modifies--I know CBMC says assigns, but IMO it's better to be consistent with our function contracts modifies clause.

@github-actions github-actions bot added the Z-CompilerBenchCI Tag a PR to run benchmark CI label Jun 26, 2025
@thanhnguyen-aws
Copy link
Contributor Author

Could you update our tutorial documentation along with this?

I did

@thanhnguyen-aws
Copy link
Contributor Author

Also, I'm curious why we're calling it loop_assigns rather than loop_modifies--I know CBMC says assigns, but IMO it's better to be consistent with our function contracts modifies clause.

It reminds me of the loop_invariant or loop_contract stuffs that we discussed long time ago. I think we should discuss with more team members to make the decision whether we should separate or unify loop and function terminologies. Then we may create a separate PR for it.

@carolynzech
Copy link
Contributor

It reminds me of the loop_invariant or loop_contract stuffs that we discussed long time ago. I think we should discuss with more team members to make the decision whether we should separate or unify loop and function terminologies. Then we may create a separate PR for it.

Hm, I disagree--the difference there was that the loop invariant vs loop contract disparity was already in our code, and we were discussing which term of those to choose and to try to stick to it. This change hasn't been merged yet, so I don't see a reason to do loop assigns when we've already established modifies for contracts. Seems needlessly confusing.

@thanhnguyen-aws thanhnguyen-aws added this pull request to the merge queue Jun 30, 2025
Merged via the queue into model-checking:main with commit b705ac5 Jun 30, 2025
25 of 28 checks passed
@carolynzech carolynzech mentioned this pull request Jul 3, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Jul 3, 2025
@carolynzech
Bump Kani version to 0.64.0 (#4198)
96f7e59 
Auto generated release notes:

## What's Changed
* Edit quantifiers' documentation. by @thanhnguyen-aws in
#4142
* Fix the bug of using multiple hidden variables for the prev of the
same Expr by @thanhnguyen-aws in
#4150
* Remove `assess` subcommand by @carolynzech in
#4111
* Optimize goto binary exporting in `cprover_bindings` by
@AlexanderPortland in #4148
* Add the option to generate performance flamegraphs by
@AlexanderPortland in #4138
* Fix the bug: Static union values can panic Kani by @thanhnguyen-aws in
#4112
* Update toolchain to 2025-06-13 by @carolynzech in
#4152
* Automatic cargo update to 2025-06-16 by @github-actions in
#4156
* Major-version update cargo dependencies by @tautschnig in
#4158
* Upgrade Rust toolchain to 2025-06-16 by @tautschnig in
#4157
* Bump tests/perf/s2n-quic from `3129ad5` to `c6e694e` by @dependabot in
#4160
* Bump tests/perf/s2n-quic from `c6e694e` to `b1b5bf8` by @dependabot in
#4164
* Upgrade Rust toolchain to 2025-06-17 by @tautschnig in
#4163
* Automatic cargo update to 2025-06-23 by @github-actions in
#4172
* Stub panics during MIR transformation by @AlexanderPortland in
#4169
* Bump tests/perf/s2n-quic from `b1b5bf8` to `32ba87d` by @dependabot in
#4175
* Handle enums with zero or one variants by @zhassan-aws in
#4171
* Introduce compiler timing script & CI job by @AlexanderPortland in
#4154
* Upgrade Rust toolchain to 2025-06-18 by @tautschnig in
#4166
* Cache dependencies for CI jobs by @AlexanderPortland in
#4181
* Autoharness: Derive `Arbitrary` for structs and enums by @carolynzech
in #4167
* Upgrade Rust toolchain to 2025-06-27 by @tautschnig in
#4182
* Include wget in dependencies by @zhassan-aws in
#4183
* Automatic cargo update to 2025-06-30 by @github-actions in
#4186
* Add support for loop assigns in loop contracts by @thanhnguyen-aws in
#4174
* Upgrade toolchain to 06/30 by @carolynzech in
#4188
* Optimize reachability with non-mutating global passes by
@AlexanderPortland in #4177
* Bump tests/perf/s2n-quic from `32ba87d` to `b8f8cca` by @dependabot in
#4190
* Bump ncipollo/release-action from 1.16.0 to 1.18.0 by @dependabot in
#4191
* Upgrade toolchain to 07/02 by @carolynzech in
#4195
* Automatic Derivation Fixes by @carolynzech in
#4194


**Full Changelog**:
kani-0.63.0...kani-0.64.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig approved these changes

Assignees

@carolynzech carolynzech

@thanhnguyen-aws thanhnguyen-aws

Labels
Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Support loop modifies in loop contracts
3 participants
@thanhnguyen-aws @carolynzech @tautschnig