Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

RFC: Attribute to distinguish safety preconditions from panic freedom #3893

Open
wants to merge 5 commits into
base: main
Choose a base branch
from
+76 −0
Open

RFC: Attribute to distinguish safety preconditions from panic freedom #3893

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
673f679
RFC: Attribute to distinguish safety preconditions from panic freedom
tautschnig Feb 17, 2025
600d95a
Apply suggestions from code review
tautschnig Feb 18, 2025
f7278e8
Merge remote-tracking branch 'origin/main' into rfc-may-panic
tautschnig Feb 18, 2025
f75f27a
Fix item 2
tautschnig Feb 18, 2025
398e9cf
Update rfc/src/rfcs/0014-may-panic-if-attr.md
tautschnig Feb 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions rfc/src/SUMMARY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
75 changes: 75 additions & 0 deletions rfc/src/rfcs/0014-may-panic-if-attr.md
View file
Open in desktop
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:** *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
Copy link
Contributor

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 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.

Copy link
Contributor

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?

Copy link
Contributor

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 requires and may_panic? Do you expect the may_panic to be a subset of the requires condition or do you expect that the correctness of the function to be described as a conjuction of both?

Copy link
Contributor

@celinval celinval Feb 27, 2025 •
edited
Loading

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 requires and may_panic. It has the following attributes:

#[kani::requires(true)] // the function is safe
#[kani::may_panic_if(self.is_none())]

This is literally implying that requires should always be true for safe functions. I.e., requires specifies only the safety contract, and it contradicts all the examples from the contracts RFC.

Copy link
Contributor

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).

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor

@carolynzech carolynzech Feb 25, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

+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 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())]
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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_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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you have an example?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#3567 (comment)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

@carolynzech carolynzech Feb 20, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#[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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 })]

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

## Open questions

- Should we permit multiple occurrences of `may_panic_if`?

## Out of scope / Future Improvements

n/a
Loading