Separate safety contract from correctness / panic freedom

[celinval]

Users should be able to annotate their unsafe functions with safety conditions and to differentiate between safety and panic freedom / correctness properties.

For example, the Index function index and the slice get_unchecked have the same pre-conditions, however, violating these conditions have very different consequences. Many users of index rely on the fact that it will panic if their assumptions about the index is incorrect. Thus, their contracts should reflect this difference.

[zhassan-aws]

Since panic conditions are part of a function specification and documentation (see example), I think we might need to create a new attribute for describing a function's panic condition (e.g. kani::panics_if. With this attribute, Kani should:

1. Verify that the function must panic under the specified condition
2. Verify that there is no UB and the post-condition holds under the non-panicking condition

For example, for unwrap, the contract would be along the lines of:

#[kani::requires(true)] // the function is safe
#[kani::panics_if(self.is_none())]
#[kani::ensures(|result| if let Some(x) = self { result == x })]

[BusyBeaver-42]

I need to express something similar, but I believe this use case is not covered by panics_if. The idea I want to express is panics_or, meaning: "The function either panics, or the program is in a consistent state when it returns."

Example: Sorting a slice

The function bidirectional_merge (in the smallsort module of the Rust standard library) might be called with a user-provided comparison function when sorting a slice. Since the slice sorting methods are safe, they cannot rely on the correctness of the comparison function to guarantee safety. In particular, the safety of bidirectional_merge cannot depend on the correctness of is_less.

If is_less is incorrect, bidirectional_merge might lead to an inconsistent state and will panic only if such a state is reached. The issue is that whether an inconsistent state is reached depends on the program's execution path. I do not see how this can be expressed with panics_if, as it would need to reference local variables that are neither arguments nor outputs of bidirectional_merge.

This limitation arises because the behavior of bidirectional_merge cannot always be determined solely from its inputs. For example, if is_less simply returns a random boolean, then regardless of any pre-conditions, any execution path is possible. As a result, given the same observable input state, bidirectional_merge may or may not panic.

[gmorenz]

I experimented with this on top of creusot a few years ago with quite a bit of success (though I eventually abandoned the project due to unrelated pain of handling creusot's WIP research prototype state).

I specifically went with a model where the annotation was may_panic(condition) (equivalent to BusyBeaver-42's panics_or suggestion) as in if condition is true it might or might not panic. In practice I found this worked quite well.

For many "standard library" style functions it was equivalent to a panics_if model, because there was no way to satisfy the postcondition clause without panicking given the inputs. For example

// @ syntax here meaning convert u32's to proper unbounded Integers in creusot's proof language
#[ensures(result@ == x@ + y@)] 
#[may_panic(x@ + y@ > i32::MAX@
fn add(x: u32, y: u32) -> u32;

guarantees that it will panic whenever it is allowed to panic, because there is no other way to satisfy the postcondition. And it's worth noting it's always possible to implement panic_if in terms of may_panic and ensures (#[panics_if(cond)] is equivalent to #[may_panic(cond)] #[ensures(!cond)]) so if there's a strong desire for both it's not significantly more work than simply having the permissive variant.

For many functions in the projects I was testing this on, it was very convenient to set liberal bounds (often #[may_panic(true)]) and not worry about panics. The contract I was guaranteeing then wasn't "this function will always work" but "this function will never return a wrong result" - which is still a very powerful guarantee, and a lot easier to prove because you don't have to figure out exactly when arithmetic overflows or so on.

[gmorenz]

Or to use the example from above instead of integer overflow, unwrap becomes

#[kani::requires(true)] // the function is safe
#[kani::panics_or(self.is_none())]
#[kani::ensures(|result| Some(result) == self)]

It can panic if self is None, but it also can't return if self is None, so really the only option is to panic.