From 5ebb27769fbd361370a3f2cfe89e70ab8c28bf2b Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 23 Jan 2025 16:07:19 -0600 Subject: [PATCH 1/6] Add documentation for loop contracts --- .../reference/experimental/loop-contracts.md | 102 ++++++++++++++++++ 1 file changed, 102 insertions(+) create mode 100644 docs/src/reference/experimental/loop-contracts.md diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md new file mode 100644 index 000000000000..46dfcff49b93 --- /dev/null +++ b/docs/src/reference/experimental/loop-contracts.md @@ -0,0 +1,102 @@ +# Loop Contracts + +Loop contract are used to specify invariants for loops for the sake of extending Kani's *bounded proofs* to *unbounded proofs*. +A [loop invariant](https://en.wikipedia.org/wiki/Loop_invariant) is an expression that holds upon entering a loop and after every execution of the loop body. +It captures something that does not change about every step of the loop. + +It is worth revisiting the discussion about [bounded proof](../../tutorial-loop-unwinding.md#bounded-proof) and +[loop unwinding](../../tutorial-loop-unwinding.md#loops-unwinding-and-bounds). In short, bounds of number of time Kani unwinding loops also bound the size of inputs, +and hence result in a bounded proof. +Loop contracts are used to abstract out loops as non-loop blocks to avoid loop unwinding, and hence remove the bounds on the inputs. + +Consider the following example: + +``` Rust +fn simple_loop() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + while x > 1 { + x = x - 1; + }; + + assert!(x == 1); +} +``` + +In this program, the loop repeatedly decrements `x` until it equals `1`. Because we haven't specify an upper bound for `x`, to verify this function, +Kani needs to unwind the loop for `u64::MAX` iterations, which is computationally expensive. Loop contracts allow us to abstract the loop behavior, significantly reducing the verification cost. + +With loop contracts, we can specify the loop’s behavior using invariants. For example: + +``` Rust +fn simple_loop_with_loop_contracts() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + #[kani::loop_invariant(x >= 1)] + while x > 1 { + x = x - 1; + }; + + assert!(x == 1); +} +``` + +Here, the loop invariant `#[kani::loop_invariant(x >= 1)]` specifies that the condition `x >= 1` must hold true at the start of each iteration before the loop guard is + checked. Once Kani verifies that the loop invariant is inductive, it will use the invariant to abstract the loop and avoid unwinding. + + +## Loop Contracts for `while` Loops + +> **Syntax** +> \#\[kani::loop_invariant\( [_Expression_](https://doc.rust-lang.org/reference/expressions.html) \)\] +> `while` [_Expression_](https://doc.rust-lang.org/reference/expressions.html)_except struct expression_ [_BlockExpression_](https://doc.rust-lang.org/reference/expressions/block-expr.html) + + +An invariant contract `#[kani::loop_invariant(cond)]` accepts a valid Boolean expression `cond` over the variables visible at the same scope as the loop. + +### Semantic +A loop invariant contract expands to several assumptions and assertions: +1. The invariant is asserted just before the first iteration. +2. The invariant is assumed on a non-deterministic state to model a non-deterministic iteration. +3. The invariant is finally asserted again to establish its inductiveness. + +Mathematical induction is the working principle here. (1) establishes the base case for induction, and (2) & (3) establish the inductive case. +Therefore, the invariant must hold after the loop execution for any number of iterations. The invariant, together with the negation of the loop guard, +must be sufficient to establish subsequent assertions. If it is not, the abstraction is too imprecise and the user must supply a stronger invariant. + +To illustrate the key idea, we show how Kani abstract the loop in `simple_loop_with_loop_contracts` as a non-loop block: +``` Rust +assert!(x >= 1) // check loop invariant for the base case. +x = kani:any(); +assume!(x >= 1); +if x > 1{ + // proof path 1: + // both loop guard and loop invariant are satisfied. + x = x - 1; + assert!(x >= 1); // check that loop invariant is inductive. + assume!(false) // kill this proof path. +} +// proof path 2: +// loop invariant is satisfied and loop guard is violated. +assert!(x == 1); +``` +That is, we assume that we are in an arbitrary iteration after checking that the loop invariant holds for the base case. With the inductive hypothesis (`assume!(x >= 1);`), +we will either enter the loop (proof path 1) and leave the loop (proof path 2). We prove the two paths separately by killing the path 1 with `assume!(false);`. +Note that all assertions after `assume!(false)` will be ignored as `false => p` can be deduced as `true` for any `p`. + +In the proof path 1, we prove properties inside the loop and at last check that the loop invariant is inductive. + +In the proof path 2, we prove properties after leaving the loop. As we leave the loop only when the loop guard is violated, the post condition of the loop can be expressed as +`!guard && inv`, which is `x <= 1 && x >= 1` in the example. The postcondition implies `x == 1`---the property we want to prove at the end of `simple_loop_with_loop_contracts`. + + +## Limitations + +Loop contracts comes with the following limitations. + +1. Besides `while` loops, there are three other kinds of loops that we don't support loop contracts for: [`loop` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#infinite-loops) + , [`while let` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#predicate-pattern-loops), and [`for` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#iterator-loops). +2. Kani infer *loop modifies* with alias analysis. Loop modifies are those variables we assume to be arbitrary in the inductive hypothesis, and should cover all memory locations that are written to during the execution of the loops. Proof will fail if the inferred loop modifies miss some targets written in the loops. + We observes this happen when some fields of structs are modified by some other functions called in the loops. +3. Kani doesn't check if a loop will always terminate in proofs with loop contracts. So it could be that some properties are proved successfully with Kani but actually are unreachable due to the non-termination of some loops. +4. We don't check if loop invariants are side-effect free. A loop invariant with side-effect could lead to unsound proof result. Be sure that the specified loop contracts are side-effect free. \ No newline at end of file From 411ebe5b8a5e67a39ce85eab21e10b4a5f0ef41d Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 23 Jan 2025 16:09:57 -0600 Subject: [PATCH 2/6] Update loop-contracts.md --- docs/src/reference/experimental/loop-contracts.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md index 46dfcff49b93..b26fb0ca3236 100644 --- a/docs/src/reference/experimental/loop-contracts.md +++ b/docs/src/reference/experimental/loop-contracts.md @@ -48,7 +48,9 @@ Here, the loop invariant `#[kani::loop_invariant(x >= 1)]` specifies that the co ## Loop Contracts for `while` Loops > **Syntax** +> > \#\[kani::loop_invariant\( [_Expression_](https://doc.rust-lang.org/reference/expressions.html) \)\] +> > `while` [_Expression_](https://doc.rust-lang.org/reference/expressions.html)_except struct expression_ [_BlockExpression_](https://doc.rust-lang.org/reference/expressions/block-expr.html) @@ -99,4 +101,4 @@ Loop contracts comes with the following limitations. 2. Kani infer *loop modifies* with alias analysis. Loop modifies are those variables we assume to be arbitrary in the inductive hypothesis, and should cover all memory locations that are written to during the execution of the loops. Proof will fail if the inferred loop modifies miss some targets written in the loops. We observes this happen when some fields of structs are modified by some other functions called in the loops. 3. Kani doesn't check if a loop will always terminate in proofs with loop contracts. So it could be that some properties are proved successfully with Kani but actually are unreachable due to the non-termination of some loops. -4. We don't check if loop invariants are side-effect free. A loop invariant with side-effect could lead to unsound proof result. Be sure that the specified loop contracts are side-effect free. \ No newline at end of file +4. We don't check if loop invariants are side-effect free. A loop invariant with side-effect could lead to unsound proof result. Be sure that the specified loop contracts are side-effect free. From 904d449f4686ac05841e0249a22e4c277d3844c4 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 23 Jan 2025 16:14:49 -0600 Subject: [PATCH 3/6] Add usage of loop contracts --- docs/src/reference/experimental/loop-contracts.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md index b26fb0ca3236..52c6d6be2622 100644 --- a/docs/src/reference/experimental/loop-contracts.md +++ b/docs/src/reference/experimental/loop-contracts.md @@ -44,8 +44,13 @@ fn simple_loop_with_loop_contracts() { Here, the loop invariant `#[kani::loop_invariant(x >= 1)]` specifies that the condition `x >= 1` must hold true at the start of each iteration before the loop guard is checked. Once Kani verifies that the loop invariant is inductive, it will use the invariant to abstract the loop and avoid unwinding. + Now let's run the proof with loop contracts through kani: + ``` bash +kani simple_loop_with_loop_contracts.rs -Z loop-contracts + ``` -## Loop Contracts for `while` Loops + +## Loop contracts for `while` loops > **Syntax** > From 4648abffcd07ea4d17bd521d081b3a54ba61352b Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 28 Jan 2025 14:24:13 -0600 Subject: [PATCH 4/6] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- .../reference/experimental/loop-contracts.md | 30 +++++++++---------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md index 52c6d6be2622..4f216ef75f0d 100644 --- a/docs/src/reference/experimental/loop-contracts.md +++ b/docs/src/reference/experimental/loop-contracts.md @@ -5,7 +5,7 @@ A [loop invariant](https://en.wikipedia.org/wiki/Loop_invariant) is an expressio It captures something that does not change about every step of the loop. It is worth revisiting the discussion about [bounded proof](../../tutorial-loop-unwinding.md#bounded-proof) and -[loop unwinding](../../tutorial-loop-unwinding.md#loops-unwinding-and-bounds). In short, bounds of number of time Kani unwinding loops also bound the size of inputs, +[loop unwinding](../../tutorial-loop-unwinding.md#loops-unwinding-and-bounds). In short, bounds on the number of times Kani unwinds loops also bound the size of inputs, and hence result in a bounded proof. Loop contracts are used to abstract out loops as non-loop blocks to avoid loop unwinding, and hence remove the bounds on the inputs. @@ -61,7 +61,7 @@ kani simple_loop_with_loop_contracts.rs -Z loop-contracts An invariant contract `#[kani::loop_invariant(cond)]` accepts a valid Boolean expression `cond` over the variables visible at the same scope as the loop. -### Semantic +### Semantics A loop invariant contract expands to several assumptions and assertions: 1. The invariant is asserted just before the first iteration. 2. The invariant is assumed on a non-deterministic state to model a non-deterministic iteration. @@ -71,39 +71,39 @@ Mathematical induction is the working principle here. (1) establishes the base c Therefore, the invariant must hold after the loop execution for any number of iterations. The invariant, together with the negation of the loop guard, must be sufficient to establish subsequent assertions. If it is not, the abstraction is too imprecise and the user must supply a stronger invariant. -To illustrate the key idea, we show how Kani abstract the loop in `simple_loop_with_loop_contracts` as a non-loop block: +To illustrate the key idea, we show how Kani abstracts the loop in `simple_loop_with_loop_contracts` as a non-loop block: ``` Rust assert!(x >= 1) // check loop invariant for the base case. -x = kani:any(); -assume!(x >= 1); -if x > 1{ +x = kani::any(); +kani::assume(x >= 1); +if x > 1 { // proof path 1: // both loop guard and loop invariant are satisfied. x = x - 1; assert!(x >= 1); // check that loop invariant is inductive. - assume!(false) // kill this proof path. + kani::assume(false) // block this proof path. } // proof path 2: // loop invariant is satisfied and loop guard is violated. assert!(x == 1); ``` That is, we assume that we are in an arbitrary iteration after checking that the loop invariant holds for the base case. With the inductive hypothesis (`assume!(x >= 1);`), -we will either enter the loop (proof path 1) and leave the loop (proof path 2). We prove the two paths separately by killing the path 1 with `assume!(false);`. +we will either enter the loop (proof path 1) or leave the loop (proof path 2). We prove the two paths separately by killing path 1 with `assume!(false);`. Note that all assertions after `assume!(false)` will be ignored as `false => p` can be deduced as `true` for any `p`. -In the proof path 1, we prove properties inside the loop and at last check that the loop invariant is inductive. +In proof path 1, we prove properties inside the loop and at last check that the loop invariant is inductive. -In the proof path 2, we prove properties after leaving the loop. As we leave the loop only when the loop guard is violated, the post condition of the loop can be expressed as -`!guard && inv`, which is `x <= 1 && x >= 1` in the example. The postcondition implies `x == 1`---the property we want to prove at the end of `simple_loop_with_loop_contracts`. +In proof path 2, we prove properties after leaving the loop. As we leave the loop only when the loop guard is violated, the post condition of the loop can be expressed as +`!guard && inv`, which is `x <= 1 && x >= 1` in the example. The postcondition implies `x == 1`—the property we want to prove at the end of `simple_loop_with_loop_contracts`. ## Limitations Loop contracts comes with the following limitations. -1. Besides `while` loops, there are three other kinds of loops that we don't support loop contracts for: [`loop` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#infinite-loops) +1. Only `while` loops are supported. The other three kinds of loops are not supported: [`loop` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#infinite-loops) , [`while let` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#predicate-pattern-loops), and [`for` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#iterator-loops). -2. Kani infer *loop modifies* with alias analysis. Loop modifies are those variables we assume to be arbitrary in the inductive hypothesis, and should cover all memory locations that are written to during the execution of the loops. Proof will fail if the inferred loop modifies miss some targets written in the loops. - We observes this happen when some fields of structs are modified by some other functions called in the loops. +2. Kani infers *loop modifies* with alias analysis. Loop modifies are those variables we assume to be arbitrary in the inductive hypothesis, and should cover all memory locations that are written to during the execution of the loops. A proof will fail if the inferred loop modifies misses some targets written in the loops. + We observed this happens when some fields of structs are modified by some other functions called in the loops. 3. Kani doesn't check if a loop will always terminate in proofs with loop contracts. So it could be that some properties are proved successfully with Kani but actually are unreachable due to the non-termination of some loops. -4. We don't check if loop invariants are side-effect free. A loop invariant with side-effect could lead to unsound proof result. Be sure that the specified loop contracts are side-effect free. +4. We don't check if loop invariants are side-effect free. A loop invariant with a side effect could lead to an unsound proof result. Make sure that the specified loop contracts are side-effect free. From f42c48a9b5aa89cfe1007f134a6e57c43c160051 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 28 Jan 2025 14:51:18 -0600 Subject: [PATCH 5/6] Add Kani's output to loop contracts' reference --- .../reference/experimental/loop-contracts.md | 65 ++++++++++++++++--- 1 file changed, 55 insertions(+), 10 deletions(-) diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md index 4f216ef75f0d..c55040b12963 100644 --- a/docs/src/reference/experimental/loop-contracts.md +++ b/docs/src/reference/experimental/loop-contracts.md @@ -29,6 +29,9 @@ Kani needs to unwind the loop for `u64::MAX` iterations, which is computationall With loop contracts, we can specify the loop’s behavior using invariants. For example: ``` Rust +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + fn simple_loop_with_loop_contracts() { let mut x: u64 = kani::any_where(|i| *i >= 1); @@ -42,17 +45,57 @@ fn simple_loop_with_loop_contracts() { ``` Here, the loop invariant `#[kani::loop_invariant(x >= 1)]` specifies that the condition `x >= 1` must hold true at the start of each iteration before the loop guard is - checked. Once Kani verifies that the loop invariant is inductive, it will use the invariant to abstract the loop and avoid unwinding. +checked. Once Kani verifies that the loop invariant is inductive, it will use the invariant to abstract the loop and avoid unwinding. - Now let's run the proof with loop contracts through kani: - ``` bash +Now let's run the proof with loop contracts through kani: +``` bash kani simple_loop_with_loop_contracts.rs -Z loop-contracts - ``` +``` +The output reported by Kani on the example will be +``` +... + + +Check 10: simple_loop_with_loop_contracts.loop_invariant_base.1 + - Status: SUCCESS + - Description: "Check invariant before entry for loop simple_loop_with_loop_contracts.0" + - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts + +Check 11: simple_loop_with_loop_contracts.loop_assigns.1 + - Status: SUCCESS + - Description: "Check assigns clause inclusion for loop simple_loop_with_loop_contracts.0" + - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts + +Check 13: simple_loop_with_loop_contracts.assigns.1 + - Status: SUCCESS + - Description: "Check that x is assignable" + - Location: simple_while_loop.rs:17:9 in function simple_loop_with_loop_contracts + +Check 14: simple_loop_with_loop_contracts.loop_invariant_step.1 + - Status: SUCCESS + - Description: "Check invariant after step for loop simple_loop_with_loop_contracts.0" + - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts + +Check 15: simple_loop_with_loop_contracts.loop_invariant_step.2 + - Status: SUCCESS + - Description: "Check invariant after step for loop simple_loop_with_loop_contracts.0" + - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts + +... + +SUMMARY: + ** 0 of 99 failed + +VERIFICATION:- SUCCESSFUL +Verification Time: 0.3897019s + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. +``` ## Loop contracts for `while` loops -> **Syntax** +### Syntax > > \#\[kani::loop_invariant\( [_Expression_](https://doc.rust-lang.org/reference/expressions.html) \)\] > @@ -87,9 +130,9 @@ if x > 1 { // loop invariant is satisfied and loop guard is violated. assert!(x == 1); ``` -That is, we assume that we are in an arbitrary iteration after checking that the loop invariant holds for the base case. With the inductive hypothesis (`assume!(x >= 1);`), -we will either enter the loop (proof path 1) or leave the loop (proof path 2). We prove the two paths separately by killing path 1 with `assume!(false);`. -Note that all assertions after `assume!(false)` will be ignored as `false => p` can be deduced as `true` for any `p`. +That is, we assume that we are in an arbitrary iteration after checking that the loop invariant holds for the base case. With the inductive hypothesis (`kani::assume(x >= 1);`), +we will either enter the loop (proof path 1) or leave the loop (proof path 2). We prove the two paths separately by killing path 1 with `kani::assume(false);`. +Note that all assertions after `kani::assume(false)` will be ignored as `false => p` can be deduced as `true` for any `p`. In proof path 1, we prove properties inside the loop and at last check that the loop invariant is inductive. @@ -103,7 +146,9 @@ Loop contracts comes with the following limitations. 1. Only `while` loops are supported. The other three kinds of loops are not supported: [`loop` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#infinite-loops) , [`while let` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#predicate-pattern-loops), and [`for` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#iterator-loops). -2. Kani infers *loop modifies* with alias analysis. Loop modifies are those variables we assume to be arbitrary in the inductive hypothesis, and should cover all memory locations that are written to during the execution of the loops. A proof will fail if the inferred loop modifies misses some targets written in the loops. +2. Kani infers *loop modifies* with alias analysis. Loop modifies are those variables we assume to be arbitrary in the inductive hypothesis, and should cover all memory locations that are written to during + the execution of the loops. A proof will fail if the inferred loop modifies misses some targets written in the loops. We observed this happens when some fields of structs are modified by some other functions called in the loops. -3. Kani doesn't check if a loop will always terminate in proofs with loop contracts. So it could be that some properties are proved successfully with Kani but actually are unreachable due to the non-termination of some loops. +3. Kani doesn't check if a loop will always terminate in proofs with loop contracts. So it could be that some properties are proved successfully with Kani but actually are unreachable due to the + non-termination of some loops. 4. We don't check if loop invariants are side-effect free. A loop invariant with a side effect could lead to an unsound proof result. Make sure that the specified loop contracts are side-effect free. From bf05956f35634ae7ff55e34c8fe4a09e3b4a6d83 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 29 Jan 2025 10:19:38 -0600 Subject: [PATCH 6/6] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- docs/src/reference/experimental/loop-contracts.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md index c55040b12963..3cf5ecd429cc 100644 --- a/docs/src/reference/experimental/loop-contracts.md +++ b/docs/src/reference/experimental/loop-contracts.md @@ -17,13 +17,13 @@ fn simple_loop() { while x > 1 { x = x - 1; - }; + } assert!(x == 1); } ``` -In this program, the loop repeatedly decrements `x` until it equals `1`. Because we haven't specify an upper bound for `x`, to verify this function, +In this program, the loop repeatedly decrements `x` until it equals `1`. Because we haven't specified an upper bound for `x`, to verify this function, Kani needs to unwind the loop for `u64::MAX` iterations, which is computationally expensive. Loop contracts allow us to abstract the loop behavior, significantly reducing the verification cost. With loop contracts, we can specify the loop’s behavior using invariants. For example: @@ -38,7 +38,7 @@ fn simple_loop_with_loop_contracts() { #[kani::loop_invariant(x >= 1)] while x > 1 { x = x - 1; - }; + } assert!(x == 1); }