RFC: Attribute to distinguish safety preconditions from panic freedom

[tautschnig]

This is to discuss the proposed solution for #3567 (Separate safety contract from correctness / panic freedom).

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 writing this up!

[carolynzech]

This seems sound to me, which is obviously our first priority -- I would love if we could come up with something that didn't require running twice, but I don't currently have any ideas.

[zhassan-aws]

Rendered version: https://github.com/tautschnig/kani/blob/rfc-may-panic/rfc/src/rfcs/0014-may-panic-if-attr.md

[zhassan-aws]

Do you have an example?

[carolynzech]

#3567 (comment)

[zhassan-aws]

This sounds to me like a corner case. The more common case is that a function's documentation includes a section of the panic condition (e.g. https://doc.rust-lang.org/std/string/struct.String.html#panics), and thus is clearly defined in terms of the function's input parameters.

[carolynzech]

Okay, so your argument is that it's better to introduce #[panics_if(cond)] that provides a stronger guarantee that it must panic, with the tradeoff that it's not applicable to cases like the linked issue?
Also, there isn't fundamentally a reason we can't just have both #[panics_if(cond)] and #[may_panic_if(cond)], as long as we document the differences well. Although at that point it may make more sense to just have #[panics_if(cond)] and #[may_panic], where #[may_panic] just says "if it panics, succeed; otherwise, succeed iff the postcondition holds.

[carolynzech]

Also, per #3567 (comment):

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.

[zhassan-aws]

#[may_panic], where #[may_panic] just says "if it panics, succeed; otherwise, succeed iff the postcondition holds.

Which would be the same as the #[should_panic] that harnesses can be annotated with?

(#[panics_if(cond)] is equivalent to #[may_panic(cond)] #[ensures(!cond)])

I don't see how the two are equivalent since cond is essentially a pre-condition, so its not clear to me how adding #[ensures(!cond)] would provide the stronger guarantee that #[panics_if] provides.

[carolynzech]

Which would be the same as the #[should_panic] that harnesses can be annotated with?

Not quite, e.g.:

#[kani::proof_for_contract(]
#[kani::should_panic]
fn prove_foo() {
    foo();
}

fails with:

VERIFICATION:- FAILED (encountered no panics, but at least one was expected)

whereas with #[may_panic], it would succeed. (If I could go back and bikeshed, I would have named #[should_panic] #[must_panic] instead 😄 )

I don't see how the two are equivalent since cond is essentially a pre-condition, so its not clear to me how adding #[ensures(!cond)] would provide the stronger guarantee that #[panics_if] provides.

We only check the postcondition if the function does not panic, so if we reach the point where we are enforcing the postcondition, cond must not hold. (If it does hold, then we should have panicked).
Taking your example from #3567 (comment),

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

would become

#[kani::requires(true)] // the function is safe
#[kani::may_panic_if(self.is_none())]
// `panic_if(cond)` semantics imply that we check the postcondition iff !cond,
// so if are checking the `#[ensures]`, `cond = self.is_none()` cannot hold
#[kani::ensures(|| !self.is_none())]
#[kani::ensures(|result| if let Some(x) = self { result == x })]

[zhassan-aws]

Perhaps it needs to be #[ensures(old(!cond))] instead in case the function mutates self?