RFC: Attribute to distinguish safety preconditions from panic freedom #3893
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,75 @@ | ||
| - **Feature Name:** Attribute to distinguish safety preconditions from panic freedom (`may-panic-if-attribute`) | ||
| - **Feature Request Issue:** [#3567](https://github.com/model-checking/kani/issues/3567) | ||
| - **RFC PR:** [#3893](https://github.com/model-checking/kani/pull/3893) | ||
| - **Status:** Under Review | ||
| - **Version:** 0 | ||
| - **Proof-of-concept:** Not yet | ||
|
|
||
| ------------------- | ||
|
|
||
| ## Summary | ||
|
|
||
| Kani users want to prove absence of undefined behavior ("safety") while | ||
| distinguishing it from panic freedom. | ||
|
|
||
| ## User Impact | ||
|
|
||
| With the `requires` clauses of function contracts we have enabled modular safety | ||
| verification, permitting users to prove the absence of undefined behavior when | ||
| preconditions are met. | ||
| In some cases, however, users may want to go further and | ||
| 1. prove the absence of unexpected panics in presence of expected panics | ||
| (the presence of the latter can already be demonstrated with the | ||
| `should_panic` attribute); | ||
| 2. formally describe the conditions under which a panic is possible; | ||
| 3. prove total correctness by precisely describing the conditions under which a | ||
| panic occur, upon which the post-conditions are no longer guaranteed. | ||
|
|
||
| ## User Experience | ||
|
There was a problem hiding this comment. How will this affect stubbing with contracts? |
||
|
|
||
| Users will be able to add an attribute | ||
| `#[kani::may_panic_if(<Boolean expression>)]` | ||
| to any function that has a contract (i.e., at least one of `ensures` or | ||
| `requires`) clause. | ||
| When such an attribute is present, users will add `-Z may-panic-if-attribute` to | ||
|
There was a problem hiding this comment. 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 There was a problem hiding this comment. +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. |
||
| change Kani's verification behavior as follows: | ||
| 1. Kani will report successful verification when all properties hold and no | ||
| panic can occur. (This behavior is unchanged.) | ||
| 2. Kani will also report successful verification when all properties hold, no | ||
| panic occurs when the negation of the condition given with `may_panic_if` | ||
| holds, yet some panic occurs when the condition holds. | ||
| 3. Else Kani reports verification failure. (This behavior is unchanged.) | ||
|
|
||
| The following example describes what the overall contract for `unwrap` would | ||
| thus look like: | ||
| ```rust | ||
| #[kani::requires(true)] // the function is safe | ||
| #[kani::may_panic_if(self.is_none())] | ||
tautschnig marked this conversation as resolved.
Show resolved
Hide resolved
There was a problem hiding this comment. Naming this "may" makes it seem like panic may also not happen. |
||
| #[kani::ensures(|result| Some(result) == self)] | ||
| ``` | ||
|
|
||
| ## Software Design | ||
|
|
||
| **We recommend that you leave the Software Design section empty for the first version of your RFC**. | ||
|
|
||
| Initial implementation suggestion: we will run Kani twice for any such harness | ||
|
There was a problem hiding this comment. 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. |
||
| (unless the condition is trivially `true` or `false`), once while assuming the | ||
| condition (and then checking that no properties other than reachability checks | ||
| fail); if that run succeeded we remove the assumptions and, similarly to | ||
| `should_panic`, check that the only failing properties are panics and not safety | ||
| checks. | ||
|
|
||
| ## Rationale and alternatives | ||
|
|
||
| The linked issue contains suggestions for alternative means to describe panic | ||
| conditions, most notably `panic_if`. This was ruled out as it may at times not | ||
| be possible to exactly describe the conditions under which a panic _must_ occur | ||
|
There was a problem hiding this comment. Do you have an example? There was a problem hiding this comment. 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. There was a problem hiding this comment. Okay, so your argument is that it's better to introduce There was a problem hiding this comment. Also, per #3567 (comment):
There was a problem hiding this comment.
Which would be the same as the
I don't see how the two are equivalent since There was a problem hiding this comment.
Not quite, e.g.: #[kani::proof_for_contract(]
#[kani::should_panic]
fn prove_foo() {
foo();
}fails with: whereas with
We only check the postcondition if the function does not panic, so if we reach the point where we are enforcing the postcondition, #[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 })]There was a problem hiding this comment. Perhaps it needs to be There was a problem hiding this comment. should, may, are both indicating the behaviour is optional. I find this misleading |
||
| with the syntactic elements in scope at the point of stating the condition. | ||
carolynzech marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| ## Open questions | ||
|
|
||
| - Should we permit multiple occurrences of `may_panic_if`? | ||
carolynzech marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| ## Out of scope / Future Improvements | ||
|
|
||
| n/a | ||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this RFC contradicts the function contracts one. We have never restricted
requiresto 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 addrequiresto safe functions.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm rather confused now. What exactly are you proposing to be the semantic of
requiresandmay_panic? Do you expect themay_panicto be a subset of therequirescondition or do you expect that the correctness of the function to be described as a conjuction of both?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Note that in the only example of this PR implies that the correctness contract is a conjunction of
requiresandmay_panic. It has the following attributes:This is literally implying that
requiresshould always betruefor safe functions. I.e.,requiresspecifies only the safety contract, and it contradicts all the examples from the contracts RFC.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am quite confused now as well, and I'm not optimistic that we're going to sort this out in Github discussion comments. I would recommend that perhaps @tautschnig schedules an optional meeting to discuss this RFC further--I think we'll make a lot more progress in a discussion than in Github comments. (Alternatively, we can block out more time at the Tuesday meeting for this RFC).