Add support to type invariants #3095
Assignees
Labels
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
Comments
celinval
added
the
[C] Feature / Enhancement
adpaco-aws
added a commit
that referenced
this issue
Jun 6, 2024
This PR reintroduces the `Invariant` trait as a mechanism for the specification of type safety invariants. The trait is defined in the Kani library where we also provide `Invariant` implementations for primitive types. In contrast to the previous `Invariant` trait, this version doesn't require the `Arbitrary` bound (i.e., it has the same requirements as `Arbitrary`). This way, the user isn't required to provide an `Arbitrary` implementation in addition to the `Invariant` one. Related #3095
celinval
pushed a commit
to celinval/kani-dev
that referenced
this issue
Jun 6, 2024
This PR reintroduces the `Invariant` trait as a mechanism for the specification of type safety invariants. The trait is defined in the Kani library where we also provide `Invariant` implementations for primitive types. In contrast to the previous `Invariant` trait, this version doesn't require the `Arbitrary` bound (i.e., it has the same requirements as `Arbitrary`). This way, the user isn't required to provide an `Arbitrary` implementation in addition to the `Invariant` one. Related model-checking#3095
adpaco-aws
added a commit
that referenced
this issue
Jun 13, 2024
This PR adds a `#[derive(Invariant)]` macro for structs which allows
users to automatically derive the `Invariant` implementations for any
struct. The derived implementation determines the invariant for the
struct as the conjunction of invariants of its fields. In other words,
the invariant is derived as `true && self.field1.is_safe() &&
self.field2.is_safe() && ..`.
For example, for the struct
```rs
#[derive(kani::Invariant)]
struct Point<X, Y> {
x: X,
y: Y,
}
```
we derive the `Invariant` implementation as
```rs
impl<X: kani::Invariant, Y: kani::Invariant> kani::Invariant for Point<X, Y> {
fn is_safe(&self) -> bool {
true && self.x.is_safe() && self.y.is_safe()
}
}
```
Related #3095
This was referenced Jun 17, 2024
adpaco-aws
added a commit
that referenced
this issue
Jul 22, 2024
…rary` and `Invariant` macros (#3283) This PR enables an `#[safety_constraint(...)]` attribute helper for the `#[derive(Arbitrary)]` and `#[derive(Invariant)]` macro. For the `Invariant` derive macro, this allows users to derive more sophisticated invariants for their data types by annotating individual named fields with the `#[safety_constraint(<cond>)]` attribute, where `<cond>` represents the predicate to be evaluated for the corresponding field. In addition, the implementation always checks `#field.is_safe()` for each field. For example, let's say we are working with the `Point` type from #3250 ```rs #[derive(kani::Invariant)] struct Point<X, Y> { x: X, y: Y, } ``` and we need to extend it to only allow positive values for both `x` and `y`. With the `[safety_constraint(...)]` attribute, we can achieve this without explicitly writing the `impl Invariant for ...` as follows: ```rs #[derive(kani::Invariant)] struct PositivePoint { #[safety_constraint(*x >= 0)] x: i32, #[safety_constraint(*y >= 0)] y: i32, } ``` For the `Arbitrary` derive macro, this allows users to derive more sophisticated `kani::any()` generators that respect the specified invariants. In other words, the `kani::any()` will assume any invariants specified through the `#[safety_constraint(...)]` attribute helper. Going back to the `PositivePoint` example, we'd expect this harness to be successful: ```rs #[kani::proof] fn check_invariant_helper_ok() { let pos_point: PositivePoint = kani::any(); assert!(pos_point.x >= 0); assert!(pos_point.y >= 0); } ``` The PR includes tests to ensure it's working as expected, in addition to UI tests checking for cases where the arguments provided to the macro are incorrect. Happy to add any other cases that you feel are missing. Related #3095
tautschnig
pushed a commit
that referenced
this issue
Aug 2, 2024
… attribute for structs (#3405) This PR updates the crates documentation we already had for the `#[safety_constraint(...)]` attribute to account for the changes in #3270. The proposal includes notes/guidelines on where to use the attribute (i.e., the struct or its fields) depending on the type safety condition to be specified. Also, it removes the `rs` annotations on the code blocks that appear in the documentation because they don't seem to have the intended effect (the blocks are not being highlighted at all). The current version of this documentation can be found [here](https://model-checking.github.io/kani/crates/doc/kani/derive.Arbitrary.html) and [here](https://model-checking.github.io/kani/crates/doc/kani/derive.Invariant.html). Related #3095
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Requested feature: Users should be able to specify and verify type safety invariants.
Use case: Users often encode safety of a type as a relationship between its internal variables, and Kani should provide a mechanism for users to specify the invariants and verify them.
Link to relevant documentation (Rust reference, Nomicon, RFC): https://www.ralfj.de/blog/2018/08/22/two-kinds-of-invariants.html
The text was updated successfully, but these errors were encountered: