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

[thanhnguyen-aws]

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.

[carolynzech]

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]

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]

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]

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]

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]

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]

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]

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.

[thanhnguyen-aws]

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.

I added it

[qinheping]

LGTM, thank you!

[carolynzech]

Thanks!