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?

[remi-delmas-3000]

should, may, are both indicating the behaviour is optional. I find this misleading

[celinval]

Thanks @tautschnig

[celinval]

I'm wondering if this should be part of the function contracts RFC since it hasn't been stabilized yet.

Users would also be able to reuse -Z function-contracts?

[carolynzech]

+1 to using the same unstable flag. I could take or leave it being part of the function contracts RFC--I like it separate I think.

[celinval]

I think this RFC contradicts the function contracts one. We have never restricted requires to safety conditions. If this is the way we want to go, the contracts RFC should be updated and we should consider at least warning users that add requires to safe functions.

[carolynzech]

I don't know that it's a contradiction--we have enabled modular safety verification, that's just not all that we've enabled (i.e., you can write preconditions for safe functions too).
It so happens that we've found preconditions most useful for unsafe functions, but if people want to use it differently (perhaps as a form of documentation on a safe function), I have no issue with that, and I don't think anything in this RFC contradicts that?

[celinval]

How will this affect stubbing with contracts?

[remi-delmas-3000]

Naming this "may" makes it seem like panic may also not happen.

[remi-delmas-3000]

should, may, are both indicating the behaviour is optional. I find this misleading