From 7d0d342ad6b8cb9a53ae3a31138a31ec273304d6 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 7 Jun 2024 17:45:22 -0400 Subject: [PATCH 1/4] RFC: Quantifiers Signed-off-by: Felipe R. Monteiro --- rfc/src/SUMMARY.md | 1 + rfc/src/rfcs/0010-quantifiers.md | 207 +++++++++++++++++++++++++++++++ 2 files changed, 208 insertions(+) create mode 100644 rfc/src/rfcs/0010-quantifiers.md diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index f8d5dc5639f5..e0b31761ae62 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -15,3 +15,4 @@ - [0007-global-conditions](rfcs/0007-global-conditions.md) - [0008-line-coverage](rfcs/0008-line-coverage.md) - [0009-function-contracts](rfcs/0009-function-contracts.md) +- [0010-quantifiers](rfcs/0010-quantifiers.md) diff --git a/rfc/src/rfcs/0010-quantifiers.md b/rfc/src/rfcs/0010-quantifiers.md new file mode 100644 index 000000000000..28b3ad9ff9d6 --- /dev/null +++ b/rfc/src/rfcs/0010-quantifiers.md @@ -0,0 +1,207 @@ +- **Feature Name:** Quantifiers +- **Feature Request Issue:** [#2546](https://github.com/model-checking/kani/issues/2546) and [#836](https://github.com/model-checking/kani/issues/836) +- **RFC PR:** [#](https://github.com/model-checking/kani/pull/) +- **Status:** Unstable +- **Version:** 1 + +------------------- + +## Summary + +Quantifiers are like logic-level loops and a powerful reasoning helper, which allow us to express statements about objects in a domain that satisfy a given condition. There are two primary quantifiers: the existential quantifier (∃) and the universal quantifier (∀). + +1. The existential quantifier (∃): represents the statement "there exists." We use to express that there is at least one object in the domain that satisfies a given condition. For example, "∃x P(x)" means "there exists an x such that P(x) is true." + +2. The universal quantifier (∀): represents the statement "for all" or "for every." We use it to express that a given condition is true for every object in the domain. For example, "∀x P(x)" means "for every x, P(x) is true." + +## User Impact + +Quantifiers enhance users' expressive capabilities, enabling the verification of more intricate properties in a concise manner. +Rather than exhaustively listing all elements in a domain, quantifiers enable users to make statements about the entire domain at once. This compact representation is crucial when dealing with large or unbounded inputs. Quantifiers also facilitate abstraction and generalization of properties. Instead of specifying properties for specific instances, quantified properties can capture general patterns and behaviors that hold across different objects in a domain. Additionally, by replacing loops in the specification with quantifiers, Kani can encode the properties more efficiently within the specified bounds, making the verification process more manageable and computationally feasible. + +This new feature doesn't introduce any breaking changes to users. It will only allow them to write properites using the existential (∃) and universal (∀) quantifiers. + +## User Experience + +We propose a syntax inspired by [Prusti](https://viperproject.github.io/prusti-dev/user-guide/syntax.html?highlight=quanti#quantifiers). Quantifiers must have only one bound variable (restriction imposed today by CBMC). The syntax of existential (i.e., `kani::exists`) and universal (i.e., `kani::forall`) quantifiers are: + +```rust +kani::exists(|: | && ) +kani::forall(|: | ==> ) +``` + +where `` is an expression of the form + +```rust + <= && < +``` + +where `lower bound` and `upper bound` are constants. The bound predicates could be strict (e.g., ` < `), or non-strict (e.g., ` <= `), but both the bounds must be **constants**. CBMC's SAT backend only supports bounded quantification under **constant** lower and upper bounds. + +Consider the following example adapted from the documentation for the [from_raw_parts](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.from_raw_parts) function: + +```rust +use std::ptr; +use std::mem; + +#[kani::proof] +fn main() { + let v = vec![kani::any::(); 100]; + + // Prevent running `v`'s destructor so we are in complete control + // of the allocation. + let mut v = mem::ManuallyDrop::new(v); + + // Pull out the various important pieces of information about `v` + let p = v.as_mut_ptr(); + let len = v.len(); + let cap = v.capacity(); + + unsafe { + // Overwrite memory + for i in 0..len { + *p.add(i) += 1; + } + + // Put everything back together into a Vec + let rebuilt = Vec::from_raw_parts(p, len, cap); + } +} +``` + +Given the `v` vector has non-deterministic values, there are potential arithmetic overflows that might happen in the for loop. So we need to constrain all values of the array. We may also want to check all values of `rebuilt` after the operation. Without quantifiers, we might be tempt to use loops as follows: + +```rust +use std::ptr; +use std::mem; + +#[kani::proof] +fn main() { + let original_v = vec![kani::any::(); 100]; + let v = original_v.clone(); + for i in 0..v.len() { + kani::assume(v[i] < 5); + } + + // Prevent running `v`'s destructor so we are in complete control + // of the allocation. + let mut v = mem::ManuallyDrop::new(v); + + // Pull out the various important pieces of information about `v` + let p = v.as_mut_ptr(); + let len = v.len(); + let cap = v.capacity(); + + unsafe { + // Overwrite memory + for i in 0..len { + *p.add(i) += 1; + } + + // Put everything back together into a Vec + let rebuilt = Vec::from_raw_parts(p, len, cap); + for i in 0..len { + assert_eq!(rebuilt[i], original_v[i]+1); + } + } +} +``` + +This, however, might unnecessary increase the complexity of the verication process. We can achieve the same effect using quantifiers as shown below. + +```rust +use std::ptr; +use std::mem; + +#[kani::proof] +fn main() { + let original_v = vec![kani::any::(); 3]; + let v = original_v.clone(); + kani::assume(kani::forall(|i: usize| (i < v.len()) ==> (v[i] < 5))); + + // Prevent running `v`'s destructor so we are in complete control + // of the allocation. + let mut v = mem::ManuallyDrop::new(v); + + // Pull out the various important pieces of information about `v` + let p = v.as_mut_ptr(); + let len = v.len(); + let cap = v.capacity(); + + unsafe { + // Overwrite memory + for i in 0..len { + *p.add(i) += 1; + } + + // Put everything back together into a Vec + let rebuilt = Vec::from_raw_parts(p, len, cap); + assert!(kani::forall(|i: usize| (i < len) ==> (rebuilt[i] == original_v[i]+1))); + } +} +``` + +The same principle applies if we want to use the existential quantifier. + +```rust +use std::ptr; +use std::mem; + +#[kani::proof] +fn main() { + let original_v = vec![kani::any::(); 3]; + let v = original_v.clone(); + kani::assume(kani::forall(|i: usize| (i < v.len()) ==> (v[i] < 5))); + + // Prevent running `v`'s destructor so we are in complete control + // of the allocation. + let mut v = mem::ManuallyDrop::new(v); + + // Pull out the various important pieces of information about `v` + let p = v.as_mut_ptr(); + let len = v.len(); + let cap = v.capacity(); + + unsafe { + // Overwrite memory + for i in 0..len { + *p.add(i) += 1; + if i == 10 { + *p.add(i) = 0; + } + } + + // Put everything back together into a Vec + let rebuilt = Vec::from_raw_parts(p, len, cap); + assert!(kani::exists(|i: usize| (i < len) && (rebuilt[i] == 0))); + } +} +``` + +The usage of quantifiers should be valid in any part of the Rust code analysed by Kani. + +## Detailed Design + + + +Kani should have the same support that CBMC has for quantifiers with its SAT backend. For more details, see [Quantifiers](https://github.com/diffblue/cbmc/blob/0a69a64e4481473d62496f9975730d24f194884a/doc/cprover-manual/contracts-quantifiers.md). + + +## Open questions + + +- **Function Contracts RFC** - CBMC has support for both `exists` and `forall`, but the + code generation is difficult. The most ergonomic and easy way to implement + quantifiers on the Rust side is as higher-order functions taking `Fn(T) -> + bool`, where `T` is some arbitrary type that can be quantified over. This + interface is familiar to developers, but the code generation is tricky, as + CBMC level quantifiers only allow certain kinds of expressions. This + necessitates a rewrite of the `Fn` closure to a compliant expression. + + +## Future possibilities + + +- CBMC has an SMT backend which allow the use of quantifiers with arbitrary Boolean expressions. Kani must include an option for users to experiment with this backend. + +--- From 32e746805d235719cb16434af30390ad062f6411 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Wed, 26 Jun 2024 18:18:13 -0400 Subject: [PATCH 2/4] Consider Pattern Type style Signed-off-by: Felipe R. Monteiro --- rfc/src/rfcs/0010-quantifiers.md | 35 ++++++++++++++------------------ 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/rfc/src/rfcs/0010-quantifiers.md b/rfc/src/rfcs/0010-quantifiers.md index 28b3ad9ff9d6..78adbcaadb12 100644 --- a/rfc/src/rfcs/0010-quantifiers.md +++ b/rfc/src/rfcs/0010-quantifiers.md @@ -8,35 +8,30 @@ ## Summary -Quantifiers are like logic-level loops and a powerful reasoning helper, which allow us to express statements about objects in a domain that satisfy a given condition. There are two primary quantifiers: the existential quantifier (∃) and the universal quantifier (∀). +Quantifiers are logical operators that allow users to express that a property or condition applies to some or all objects within a given domain. -1. The existential quantifier (∃): represents the statement "there exists." We use to express that there is at least one object in the domain that satisfies a given condition. For example, "∃x P(x)" means "there exists an x such that P(x) is true." +## User Impact -2. The universal quantifier (∀): represents the statement "for all" or "for every." We use it to express that a given condition is true for every object in the domain. For example, "∀x P(x)" means "for every x, P(x) is true." +There are two primary quantifiers: the existential quantifier (∃) and the universal quantifier (∀). -## User Impact +1. The existential quantifier (∃): represents the statement "there exists." We use to express that there is at least one object in the domain that satisfies a given condition. For example, "∃x P(x)" means "there exists a value x such that P(x) is true." + +2. The universal quantifier (∀): represents the statement "for all" or "for every." We use it to express that a given condition is true for every object in the domain. For example, "∀x P(x)" means "for every value x, P(x) is true." -Quantifiers enhance users' expressive capabilities, enabling the verification of more intricate properties in a concise manner. Rather than exhaustively listing all elements in a domain, quantifiers enable users to make statements about the entire domain at once. This compact representation is crucial when dealing with large or unbounded inputs. Quantifiers also facilitate abstraction and generalization of properties. Instead of specifying properties for specific instances, quantified properties can capture general patterns and behaviors that hold across different objects in a domain. Additionally, by replacing loops in the specification with quantifiers, Kani can encode the properties more efficiently within the specified bounds, making the verification process more manageable and computationally feasible. This new feature doesn't introduce any breaking changes to users. It will only allow them to write properites using the existential (∃) and universal (∀) quantifiers. ## User Experience -We propose a syntax inspired by [Prusti](https://viperproject.github.io/prusti-dev/user-guide/syntax.html?highlight=quanti#quantifiers). Quantifiers must have only one bound variable (restriction imposed today by CBMC). The syntax of existential (i.e., `kani::exists`) and universal (i.e., `kani::forall`) quantifiers are: - -```rust -kani::exists(|: | && ) -kani::forall(|: | ==> ) -``` - -where `` is an expression of the form +We propose a syntax inspired by ["Pattern Types"](https://github.com/rust-lang/rust/pull/120131). The syntax of existential (i.e., `kani::exists`) and universal (i.e., `kani::forall`) quantifiers are: ```rust - <= && < +kani::exists(|: is | ) +kani::forall(|: is | ) ``` -where `lower bound` and `upper bound` are constants. The bound predicates could be strict (e.g., ` < `), or non-strict (e.g., ` <= `), but both the bounds must be **constants**. CBMC's SAT backend only supports bounded quantification under **constant** lower and upper bounds. +CBMC's SAT backend only supports bounded quantification under **constant** lower and upper bounds (for more details, see the [documentation for quantifiers in CBMC](https://diffblue.github.io/cbmc/contracts-quantifiers.html)). In contracts, the SMT backend supports arbitrary Boolean expressions. Consider the following example adapted from the documentation for the [from_raw_parts](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.from_raw_parts) function: @@ -117,7 +112,7 @@ use std::mem; fn main() { let original_v = vec![kani::any::(); 3]; let v = original_v.clone(); - kani::assume(kani::forall(|i: usize| (i < v.len()) ==> (v[i] < 5))); + kani::assume(kani::forall(|i: usize is ..v.len() | v[i] < 5)); // Prevent running `v`'s destructor so we are in complete control // of the allocation. @@ -136,7 +131,7 @@ fn main() { // Put everything back together into a Vec let rebuilt = Vec::from_raw_parts(p, len, cap); - assert!(kani::forall(|i: usize| (i < len) ==> (rebuilt[i] == original_v[i]+1))); + assert!(kani::forall(|i: usize is ..len | rebuilt[i] == original_v[i]+1)); } } ``` @@ -151,7 +146,7 @@ use std::mem; fn main() { let original_v = vec![kani::any::(); 3]; let v = original_v.clone(); - kani::assume(kani::forall(|i: usize| (i < v.len()) ==> (v[i] < 5))); + kani::assume(kani::forall(|i: usize is ..v.len() | v[i] < 5)); // Prevent running `v`'s destructor so we are in complete control // of the allocation. @@ -173,7 +168,7 @@ fn main() { // Put everything back together into a Vec let rebuilt = Vec::from_raw_parts(p, len, cap); - assert!(kani::exists(|i: usize| (i < len) && (rebuilt[i] == 0))); + assert!(kani::exists(|i: usize is ..len | rebuilt[i] == 0)); } } ``` @@ -202,6 +197,6 @@ Kani should have the same support that CBMC has for quantifiers with its SAT bac ## Future possibilities -- CBMC has an SMT backend which allow the use of quantifiers with arbitrary Boolean expressions. Kani must include an option for users to experiment with this backend. +- CBMC has an SMT backend which allows the use of quantifiers with arbitrary Boolean expressions. Kani must include an option for users to experiment with this backend. --- From 970203f5b44f7c2fc279e7e2be1874a465211329 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 27 Jun 2024 02:41:55 -0400 Subject: [PATCH 3/4] Final tweaks Signed-off-by: Felipe R. Monteiro --- rfc/src/rfcs/0010-quantifiers.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/rfc/src/rfcs/0010-quantifiers.md b/rfc/src/rfcs/0010-quantifiers.md index 78adbcaadb12..d036bb988efc 100644 --- a/rfc/src/rfcs/0010-quantifiers.md +++ b/rfc/src/rfcs/0010-quantifiers.md @@ -2,7 +2,7 @@ - **Feature Request Issue:** [#2546](https://github.com/model-checking/kani/issues/2546) and [#836](https://github.com/model-checking/kani/issues/836) - **RFC PR:** [#](https://github.com/model-checking/kani/pull/) - **Status:** Unstable -- **Version:** 1 +- **Version:** 1.0 ------------------- @@ -27,11 +27,11 @@ This new feature doesn't introduce any breaking changes to users. It will only a We propose a syntax inspired by ["Pattern Types"](https://github.com/rust-lang/rust/pull/120131). The syntax of existential (i.e., `kani::exists`) and universal (i.e., `kani::forall`) quantifiers are: ```rust -kani::exists(|: is | ) -kani::forall(|: is | ) +kani::exists(|: [is ] | ) +kani::forall(|: [is ] | ) ``` -CBMC's SAT backend only supports bounded quantification under **constant** lower and upper bounds (for more details, see the [documentation for quantifiers in CBMC](https://diffblue.github.io/cbmc/contracts-quantifiers.html)). In contracts, the SMT backend supports arbitrary Boolean expressions. +If `` is not provided, we assume `` can range over all possible values of the given `` (i.e., syntactic sugar for full range `|: as .. |`). CBMC's SAT backend only supports bounded quantification under **constant** lower and upper bounds (for more details, see the [documentation for quantifiers in CBMC](https://diffblue.github.io/cbmc/contracts-quantifiers.html)). The SMT backend, on the other hand, supports arbitrary Boolean expressions. In any case, `` should not have side effects, as the purpose of quantifiers is to assert a condition over a domain of objects without altering the state. Consider the following example adapted from the documentation for the [from_raw_parts](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.from_raw_parts) function: @@ -179,7 +179,7 @@ The usage of quantifiers should be valid in any part of the Rust code analysed b -Kani should have the same support that CBMC has for quantifiers with its SAT backend. For more details, see [Quantifiers](https://github.com/diffblue/cbmc/blob/0a69a64e4481473d62496f9975730d24f194884a/doc/cprover-manual/contracts-quantifiers.md). +Kani should have the same support that CBMC has for quantifiers. For more details, see [Quantifiers](https://github.com/diffblue/cbmc/blob/0a69a64e4481473d62496f9975730d24f194884a/doc/cprover-manual/contracts-quantifiers.md). ## Open questions @@ -192,6 +192,7 @@ Kani should have the same support that CBMC has for quantifiers with its SAT bac interface is familiar to developers, but the code generation is tricky, as CBMC level quantifiers only allow certain kinds of expressions. This necessitates a rewrite of the `Fn` closure to a compliant expression. + - Which kind of expressions should be accepted as a "compliant expression"? ## Future possibilities From cae0f44d8a22754022422d847048e3542393941e Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 27 Jun 2024 02:48:10 -0400 Subject: [PATCH 4/4] Fix typos Signed-off-by: Felipe R. Monteiro --- rfc/src/rfcs/0010-quantifiers.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0010-quantifiers.md b/rfc/src/rfcs/0010-quantifiers.md index d036bb988efc..07a5f7548974 100644 --- a/rfc/src/rfcs/0010-quantifiers.md +++ b/rfc/src/rfcs/0010-quantifiers.md @@ -64,7 +64,7 @@ fn main() { } ``` -Given the `v` vector has non-deterministic values, there are potential arithmetic overflows that might happen in the for loop. So we need to constrain all values of the array. We may also want to check all values of `rebuilt` after the operation. Without quantifiers, we might be tempt to use loops as follows: +Given the `v` vector has non-deterministic values, there are potential arithmetic overflows that might happen in the for loop. So we need to constrain all values of the array. We may also want to check all values of `rebuilt` after the operation. Without quantifiers, we might be tempted to use loops as follows: ```rust use std::ptr; @@ -161,7 +161,7 @@ fn main() { // Overwrite memory for i in 0..len { *p.add(i) += 1; - if i == 10 { + if i == 1 { *p.add(i) = 0; } }