Skip to content
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

Fix the bug: Loop contracts are not composable with function contracts #3979

Open
wants to merge 15 commits into
base: main
Choose a base branch
from
Open

Fix the bug: Loop contracts are not composable with function contracts #3979

wants to merge 15 commits into from

Conversation

thanhnguyen-aws
Copy link
Contributor

This PR fixes the bug of loop contracts are not composable with function contracts.
Previously, using loop-contract inside a function with contract may result in unwinding the loop instead of contracting it.

Resolves #3910

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 April 2, 2025 21:34
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Apr 2, 2025
carolynzech
carolynzech requested changes Apr 3, 2025
View reviewed changes
Copy link
Contributor

@carolynzech carolynzech left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for fixing this! Can you also update our loop contracts documentation in our book to talk about this change, and more generally, explain when to use #[kani::proof] vs. #[kani::proof_for_contract]? If I just have a loop contract without a function contract, can I use #[kani::proof_for_contract]?

(I haven't reviewed the code, I'm leaving that to @qinheping).

@thanhnguyen-aws
Copy link
Contributor Author

Thanks for fixing this! Can you also update our loop contracts documentation in our book to talk about this change, and more generally, explain when to use #[kani::proof] vs. #[kani::proof_for_contract]? If I just have a loop contract without a function contract, can I use #[kani::proof_for_contract]?

(I haven't reviewed the code, I'm leaving that to @qinheping).

Using #[kani::proof] or #[kani::proof_for_contract] is irrelevant to the loop or its contract, so we just use it as normal. I added the tests just to make sure there is no bug in both cases.

@carolynzech
Copy link
Contributor

Using #[kani::proof] or #[kani::proof_for_contract] is irrelevant to the loop or its contract, so we just use it as normal. I added the tests just to make sure there is no bug in both cases.

Thanks for the test, but please also update the book documentation so that our users know how to use this feature. I find it confusing that the annotation is irrelevant--why would we have both be acceptable if they do the same thing? Can you do some more thinking about the UX here before we merge this? We want to make sure that our users are set up to use this correctly.

@thanhnguyen-aws
Copy link
Contributor Author

thanhnguyen-aws commented Apr 3, 2025 •
edited
Loading

Using #[kani::proof] or #[kani::proof_for_contract] is irrelevant to the loop or its contract, so we just use it as normal. I added the tests just to make sure there is no bug in both cases.

Thanks for the test, but please also update the book documentation so that our users know how to use this feature. I find it confusing that the annotation is irrelevant--why would we have both be acceptable if they do the same thing? Can you do some more thinking about the UX here before we merge this? We want to make sure that our users are set up to use this correctly.

Let me explain it more clearly. This PR does not add any new feature, it just fixed the bug that when a function has contract, then the loop inside it will be unwinded instead of contracted even if there is a loop invariant and kani flag -Z loop-contracts is enabled. There is no change in the definitions of #[kani::proof] or #[kani::proof_for_contract] whether there are loops/loop-invariants inside the function or not, and the two harnesses are different. As you can see the verification results (in two expected files) are different, #[kani::proof_for_contract] succeed because it assumes the requires clause, while #[kani::proof] failed because it asserts (not assumes) the requires clause. Therefore, I think that the users need no additional knowledge in this case.

@carolynzech
Copy link
Contributor

As you can see the verification results (in two expected files) are different, #[kani::proof_for_contract] succeed because it assumes the requires clause, while #[kani::proof] failed because it asserts (not assumes) the requires clause.

That makes sense.

There is no change in the definitions of #[kani::proof] or #[kani::proof_for_contract] whether there are loops/loop-invariants inside the function or not, and the two harnesses are different.

I'm not sure that's true. This PR changes the behavior of Kani such that you can use #[kani::proof_for_contract] on code with loop invariants. This would change the meaning of #[kani::proof_for_contract]--can we use it to prove loop invariants now, whereas before we could just use #[kani::proof]? Can I use #[kani::proof_for_contract] if we just have a loop contract, and not function contracts? If not, then it's confusing that we call it "loop contract" and we can't use a #[kani::proof_for_contract] to prove it, and we should make that clear in our documentation.

Therefore, I think that the users need no additional knowledge in this case.

I think our documentation does need some kind of example about composing loop contracts with function contracts, since there's nothing in our book to suggest that this is even possible (all of our loop contract examples use #[kani::proof]).

What I really want is documentation that tells users which kind of harness they should use for each case:

  • If my function just has a loop contract, should I use #[kani::proof] or #[kani::proof_for_contract]?
  • If my function has both a loop contract and a function contract, should I use #[kani::proof] or #[kani::proof_for_contract]?
  • How do the answers to the above questions change if I pass --no-assert-contracts?

@thanhnguyen-aws
Copy link
Contributor Author

This PR changes the behavior of Kani such that you can use #[kani::proof_for_contract] on code with loop invariants. This would change the meaning of #[kani::proof_for_contract]--can we use it to prove loop invariants now, whereas before we could just use #[kani::proof]? Can I use #[kani::proof_for_contract] if we just have a loop contract, and not function contracts?

This PR does not change the behavior of Kani for #[kani::proof_for_contract(funcname)]: even with loop invariants, Kani will throw an error if the function does not have contract. I think what is confusing here is the name #[kani::proof_for_contract (function name)]: contract here means function contract, not loop contract. We do not have a harness attribute to enable checking loop-contract, the only way is using -Z loop-contract flag.

If not, then it's confusing that we call it "loop contract" and we can't use a #[kani::proof_for_contract] to prove it, and we should make that clear in our documentation.

I strongly agree that the easiest way to get rid of the confusion is removing the name "loop contract" and consistently calling it "loop-invariant". If everyone else agree, we can create a separate PR to change the flag name and all related tests.

@carolynzech
Copy link
Contributor

carolynzech commented Apr 7, 2025 •
edited
Loading

I strongly agree that the easiest way to get rid of the confusion is removing the name "loop contract" and consistently calling it "loop-invariant". If everyone else agree, we can create a separate PR to change the flag name and all related tests.

I strongly agree that this is the right move. Since this is a breaking change, maybe bring it up at staff meeting before making a PR. Also cc @qinheping.

This PR does not change the behavior of Kani for #[kani::proof_for_contract(funcname)]

It does change the behavior--you can now use #[kani::proof_for_contract(funcname)] to prove and use a loop invariant, whereas before you couldn't. Your point is well-taken that you also need a function contract for the proof to go through, but the fact remains that before you couldn't use loop invariants at all with #[kani::proof_for_contract(funcname)], and now you can. I think we should update our function contracts documentation in the book to reflect this change.

carolynzech
carolynzech reviewed Apr 7, 2025
View reviewed changes
Copy link
Contributor

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you also add this test?

// -Z loop-contracts -Z function-contracts --no-assert-contracts

#![feature(proc_macro_hygiene)]
#![feature(stmt_expr_attributes)]

#[kani::requires(i>=2)]
#[kani::ensures(|ret| *ret == 2)]
pub fn has_loop(mut i: u16) -> u16 {
    #[kani::loop_invariant(i>=2)]
    while i > 2 {
        i = i - 1
    }
    i
}

#[kani::proof]
fn contract_proof() {
    let i: u16 = kani::any();
    let j = has_loop(i);
}

This proof should let you just prove the loop invariant while ignoring the contract.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@carolynzech carolynzech carolynzech requested changes

Requested changes must be addressed to merge this pull request.

Assignees

@qinheping qinheping

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

Successfully merging this pull request may close these issues.

Loop contracts are not composable with function contracts
3 participants
@thanhnguyen-aws @carolynzech @qinheping