From 673f67980bba393b47c626eab73792d003ac0dfa Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 17 Feb 2025 15:26:26 +0000 Subject: [PATCH 1/4] RFC: Attribute to distinguish safety preconditions from panic freedom This is to discuss the proposed solution for #3567 (Separate safety contract from correctness / panic freedom). --- rfc/src/SUMMARY.md | 1 + rfc/src/rfcs/0014-may-panic-if-attr.md | 75 ++++++++++++++++++++++++++ 2 files changed, 76 insertions(+) create mode 100644 rfc/src/rfcs/0014-may-panic-if-attr.md diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index 2fb7d0b133cd..720f4622b7ba 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -19,3 +19,4 @@ - [0011-source-coverage](rfcs/0011-source-coverage.md) - [0012-loop-contracts](rfcs/0012-loop-contracts.md) - [0013-list](rfcs/0013-list.md) +- [0013-may-panic-if-attr](rfcs/0014-may-panic-if-attr.md) diff --git a/rfc/src/rfcs/0014-may-panic-if-attr.md b/rfc/src/rfcs/0014-may-panic-if-attr.md new file mode 100644 index 000000000000..ef75a80da4cd --- /dev/null +++ b/rfc/src/rfcs/0014-may-panic-if-attr.md @@ -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:** *Link to original PR* +- **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 + +Users will be able to add an attribute +`#[kani::may_panic_if()]` +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 +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 condition given with `may_pani_if` holds, yet some + panic occurs when the condition does not hold. +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())] +#[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 +(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_fail`, 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 +with the syntactic elements in scope at the point of stating the condition. + +## Open questions + +- Should we permit multiple occurrences of `may_panic_if`? + +## Out of scope / Future Improvements + +n/a From 600d95a3168c1fa85e2a385947ee4e4ee3494921 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 18 Feb 2025 11:13:00 +0100 Subject: [PATCH 2/4] Apply suggestions from code review Co-authored-by: Carolyn Zech --- rfc/src/SUMMARY.md | 2 +- rfc/src/rfcs/0014-may-panic-if-attr.md | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index 720f4622b7ba..0c63cd4242aa 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -19,4 +19,4 @@ - [0011-source-coverage](rfcs/0011-source-coverage.md) - [0012-loop-contracts](rfcs/0012-loop-contracts.md) - [0013-list](rfcs/0013-list.md) -- [0013-may-panic-if-attr](rfcs/0014-may-panic-if-attr.md) +- [0014-may-panic-if-attr](rfcs/0014-may-panic-if-attr.md) diff --git a/rfc/src/rfcs/0014-may-panic-if-attr.md b/rfc/src/rfcs/0014-may-panic-if-attr.md index ef75a80da4cd..24d9e0540dca 100644 --- a/rfc/src/rfcs/0014-may-panic-if-attr.md +++ b/rfc/src/rfcs/0014-may-panic-if-attr.md @@ -1,6 +1,6 @@ - **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:** *Link to original PR* +- **RFC PR:** [#3893](https://github.com/model-checking/kani/pull/3893) - **Status:** Under Review - **Version:** 0 - **Proof-of-concept:** Not yet @@ -36,7 +36,7 @@ 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 condition given with `may_pani_if` holds, yet some + panic occurs when the condition given with `may_panic_if` holds, yet some panic occurs when the condition does not hold. 3. Else Kani reports verification failure. (This behavior is unchanged.) @@ -56,7 +56,7 @@ Initial implementation suggestion: we will run Kani twice for any such harness (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_fail`, check that the only failing properties are panics and not safety +`should_panic`, check that the only failing properties are panics and not safety checks. ## Rationale and alternatives From f75f27ad1ebae73ad616459a17f677a9e4534a63 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 18 Feb 2025 10:23:48 +0000 Subject: [PATCH 3/4] Fix item 2 --- rfc/src/rfcs/0014-may-panic-if-attr.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0014-may-panic-if-attr.md b/rfc/src/rfcs/0014-may-panic-if-attr.md index 24d9e0540dca..3480ee42d86d 100644 --- a/rfc/src/rfcs/0014-may-panic-if-attr.md +++ b/rfc/src/rfcs/0014-may-panic-if-attr.md @@ -36,8 +36,9 @@ 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 condition given with `may_panic_if` holds, yet some - panic occurs when the condition does not hold. + panic occurs when the negation of the condition given with `may_panic_if` + holds, yet some panic occurs when the negation of the condition does not + hold. 3. Else Kani reports verification failure. (This behavior is unchanged.) The following example describes what the overall contract for `unwrap` would From 398e9cf48ec1668fd7d29cf9597c448185519ac2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 18 Feb 2025 17:19:32 +0100 Subject: [PATCH 4/4] Update rfc/src/rfcs/0014-may-panic-if-attr.md Co-authored-by: Carolyn Zech --- rfc/src/rfcs/0014-may-panic-if-attr.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0014-may-panic-if-attr.md b/rfc/src/rfcs/0014-may-panic-if-attr.md index 3480ee42d86d..e4d5ad159f1c 100644 --- a/rfc/src/rfcs/0014-may-panic-if-attr.md +++ b/rfc/src/rfcs/0014-may-panic-if-attr.md @@ -37,8 +37,7 @@ change Kani's verification behavior as follows: 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 negation of the condition does not - hold. + 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