Feature Request: Function Contracts

[JustusAdam]

By adding contracts support (requires/ensures/assigns/frees) to Kani we can unlock modular verification.

The RFC for Function Contracts is now live.

[celinval]

Let's keep this open until stabilization.

[BusyBeaver-42]

Hello, I have a couple of issues with function contracts. This is not about incorrect behavior, but about features that could improve Kani's integration into a codebase.

Note: The examples in this post are simple on purpose. In practice, the use-cases are complex functions that need a contract and are used with stub_verified because otherwise kani takes too long to verify.

Multiple contracts for the same function

Let's say I have a safe function foo and I want to prove both its safety and its correctness.

fn foo<F: Fn(i32) -> i32>(f: &F) -> i32 {
    f(0)
}

The function foo assumes that f(0) == 0. However, since it is a safe function, it cannot rely on this assumption to guarantee safety. Therefore, to check safety only, I would proceed as follows.

#[requires(true)]
fn foo<F>(f: &F) -> i32
where
    F: Fn(i32) -> i32,
{
    f(0)
}


fn over_approximation(_:i32) -> i32 {
    kani::any()
}

#[proof_for_contract(foo)]
fn check_safety_only() {
    foo(&over_approximation);
}

However, I also would like to express the correctness in the function contract as follows.

#[ensures(|res: &i32| implies!(f(0) == 0 => *res == 0))]
fn foo<F>(f: &F) -> i32
where
    F: Fn(i32) -> i32,
{
    f(0)
}

#[proof_for_contract(foo)]
fn check_safety_and_correctness() {
    foo(&over_approximation);
}

But in this case, the harness with over_approximation would fail. One solution is to check safety only, then create another function wraps_foo and verify correctness using this function.

#[requires(true)]
fn foo<F>(f: &F) -> i32
where
    F: Fn(i32) -> i32,
{
    f(0)
}

#[requires(f(0) == 0)]
#[ensures(*res == 0)]
fn wraps_foo<F>(f: &F) -> i32
where
    F: Fn(i32) -> i32,
{
    f(0)
}

fn over_approximation(_:i32) -> i32 {
    kani::any()
}

#[proof_for_contract(foo)]
fn check_safety_only() {
    foo(&over_approximation);
}

#[proof_for_contract(wraps_foo)]
fn check_correctness_only() {
    foo(&any_valid_f);
}

However, this is not ideal, as I would also need to re-export the wrappers if users want to reuse the correctness contracts. A potential solution would be the possibility to have several contracts for the same function and annotate them (for instance using the same syntax as for loop annotations 'safety, 'correctness).

An additional feature would be to say that a contract 'first is a "super-contract" (kind of like super traits) of another contract 'second and automatically apply the requires and ensures clauses of 'first to the 'second. Note: An option to discard in 'second the modifies clause of 'first is needed because with stronger assumptions it may be possible to be more precise.

Pre-conditions on a function with an FnOnce argument

Let's say I have a function foo which takes an FnOnce argument with the following contract.

#[requires(f(0) == 0)]
#[ensures(|res: &i32| *res == 0)]
fn foo<F>(f: F) -> i32
where
    F: FnOnce(i32) -> i32,
{
    f(0)
}

The issue is that I cannot impose pre-conditions on f even if the actual f in the harness implements Fn. Indeed, since f in foo implements FnOnce it is moved while evaluating the pre-condition. If I want to verify partial correctness for f: Fn, I have to introduce a wrapper function as follows.

fn foo<F>(f: F) -> i32
where
    F: FnOnce(i32) -> i32,
{
    f(0)
}

#[requires(f(0) == 0)]
#[ensures(|res: &i32| *res == 0)]
fn wraps_foo<F>(f: F) -> i32
where
    F: Fn(i32) -> i32,
{
    foo(f)
}

#[proof_for_contract(wraps_foo)]
fn check_foo() {
    wraps_foo(any_valid_f);
}

Function determinism

Let's say I have once again a function foo that takes an FnMut argument f. I would like to express the fact that f is deterministic in the requires clause. By deterministic, I mean that if I assign let x = f(42); at some point and later let y = f(42);, then x == y holds (although I do not care about the actual value). I understand that this is in practice impossible to check as soon as f is a bit complicated, so this can be something that the user declares.

A similar thing might be to add a "non-deterministic". Indeed, let's say a user makes an oversight while writing foo and writes code that assumes implicitly that the f argument will always be deterministic. When writing the harness, the user might make the same mistake when creating any_f. Requiring the user to explicitely annotate their any_f as non-deterministic (unless foo requires f to be derministic) would prevent them from making this mistake.

Code expansion of the modifies macro

Let's say I want to express in a contract that a function may modify everything in a range of pointers start..end. Currently, I express this as follows.

#[requires(/*
    (begin as isize) < (tail as isize)
        && all the pointers are within the same allocation
        && can write at all pointers in the range
*/)]
#[modifies(slice::from_raw_parts_mut(start, tail.offset_from(end) as usize))]
fn f(start: *mut i32, end: *mut i32) {
    ...
}

I have the two following questions.

• Is there a cleaner way to express the modifies clause?
• If not, are the safety requirements for slice::from_raw_parts respected after macro expansion? My question is mostly about this caveat.

[zhassan-aws]

Hi @BusyBeaver-42. Thanks for the suggested features. For the first question, for the harness that checks safety, you can perhaps use kani::stub? For example:

#[kani::stub(f, over_approximation)]
#[kani::proof]
fn check_foo_safety() { ... }

The harness that checks the correctness of foo would not use that stub.

For the second question:

Now I cannot impose pre-conditions on f.

Can you clarify why?

For the third question, you can specify that start and end are within the same allocation using kani::mem::same_allocation.

[BusyBeaver-42]

I've updated my previous message, I had written it in a rush and it wasn't really clear. Here's what I modified:

• First point: more complete examples and added the concept of "super-contracts" (kind of like super-traits).
• Second point: I had made a mistake and misinterpreted the error message, I was indeed able to impose pre-conditions on f. However, while thinking about it, I thought of a related use-case: FnOnce. I re-wrote the section to talk about that.
• Third point: I added a section about determinism.
• Fourth point (former third point): Tried to make it clearer.

About the first point, I did not think about stubbing the argument itself, that's clever! However, I think this does not really fit my use-case. It does work, but it does not really feel clean because I have several levels of nesting: foo is called by bar which is called by baz which is called by qux, and f is an argument of qux and is passed down with each call. over_approximation does not satisfies the correctness requirements for neither foo nor bar nor baz nor qux so I need separate safety and correctness proofs for all these functions. foo is actually called within a loop inside bar and foo already takes a lot of time to verify, that's why I want to write conctracts and use stub_verified.

About the former third point (now fourth), the problem is not about being within the same allocation (I had not included the requires clause in the example). The pointers start and end refer to a range of elements in memory (similar to how you can express that in C++). In the function contract, I have to declare that the function may modify everything that is pointed at by a pointer in the range start..end. To do that, I currently create (inside the modifies clause) a slice from the pointers (with slice::from_raw_parts). I have the two following questions.

• Is there a cleaner way to achieve this?
• If not, are the safety requirements for slice::from_raw_parts respected after macro expansion? My question is mostly about this caveat.

[zhassan-aws]

@BusyBeaver-42 would #3567 address the issue with specifying safety and correctness contracts?

[BusyBeaver-42]

Thanks, @zhassan-aws , for pointing me to this issue. I actually needed something similar for another function. However, it does not address the issue of specifying safety and correctness contracts.

The problem lies in the over-approximation I use to verify safety. While it satisfies the correctness pre-conditions, it does not satisfy the correctness post-conditions. This may seem nonsensical at first glance, but it is related to the point about function determinism in my first comment.

One of the arguments of the function f I want to verify is a callable c provided by the user. From a correctness perspective, providing a non-deterministic c makes no sense. However, from a safety perspective, f must remain safe even with a non-deterministic c. Since the correctness contract cannot specify that c must be deterministic, a single contract for both safety and correctness, as shown below, would not work:

#[requires(safety_pre_conditions)]
#[ensures(implies!(correctness_pre_conditions => correctness_post_conditions))]

Indeed, the safety check must be done with a non-deterministic c. Such a c might output a sequence of values that satisfy correctness_pre_conditions but not correctness_post_conditions because calling c twice with the same arguments might not return the same thing. As a result, the contract verification would fail.