Add loop-contracts support for `for` loop #4143

thanhnguyen-aws · 2025-06-06T20:47:01Z

This PR adds loop-contracts support for for loop for 10 types: array, slice, Iter, Vec, Range, StepBy, Map, Chain, Zip, Enumerate.

Main ideas:
for loop implementation:
A for loop of the form

for pat in expr {
    body
}

is transformed into a while loop:

let kaniiter = kani::KaniIntoIter::kani_into_iter(expr); \\ init_iter_stmt
let kaniiterlen = kani::KaniIter::len(&kaniiter); \\ init_len_stmt
if kaniiterlen > 0 {
    let mut kaniindex = 0; \\ init_index_stmt
    kani::assume (kani::KaniIter::assumption(&kaniiter)); \\ iter_assume_stmt
    let pat = kani::KaniIter::first(&kaniiter); \\ init_pat_stmt
    while kaniindex < kaniiterlen {
        kani::assume (kani::KaniIter::assumption(&kaniiter)); \\ iter_assume_stmt
        let pat = kani::KaniIter::indexing(&kaniiter, kaniindex); \\ pat_assign_stmt
        kaniindex = kaniindex + 1; \\ increase_iter_stmt
        body
    }
}

Note that

expr's type is required to impl KaniIntoIter trait, which is the override impl of Rust's IntoIter (see library/kani_core/src/iter.rs).
Reason:
a) Reduce stack-call
b) Avoid types that cannot be havoc effectively (user cannot state the type invariant in the loop invariant due to private fields)
c) There is no generic way to handle Rust's into_iter().
The init_index_stmt and init_pat_stmt support writing the loop-invariant properties that involve pat and kaniindex
The iter_assume_stmt assumes some truths about allocation, so that the user does not need to specify them in the loop invariant

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

carolynzech

I haven't reviewed the implementation yet, these are just some nits. I have two requests to make reviewing on my end easier:

This is a big PR, and it'd be much easier to review if each new piece of functionality was separated into its own commit along with its tests. I'm envisioning something like:

commit 1: code to support iter & expected tests
commit 2: code to support array & expected tests
commit 3: code to support slice & expected tests
commit 4: code to support vec & expected tests

Can you do an interactive rebase to make it look like this? It doesn't need to be exactly this--I'd just appreciate if 1) changes are committed with their tests and 2) commits irrelevant to the review (e.g., fix clippy, merges) are kept to a minimum. FWIW, I have a pre-commit hook that runs clippy, our formatting check, and copyright check so that I can't even commit unless those checks pass; I'd recommend it.

Can you add more comments? I added some places that I think need some. I'd like to see each function (unless it's super simple) have a doc comment that describes 1) what it does and 2) why it exists (i.e., why we need it in the first place)

library/kani_macros/src/sysroot/loop_contracts/mod.rs

library/kani_core/src/iter.rs

library/kani/src/iter.rs

library/kani_macros/src/sysroot/loop_contracts/mod.rs

rod-chapman · 2025-06-16T21:12:47Z

tests/expected/loop-contract/for_loop_with_quantifier.rs

+    let a: [u8; 10] = kani::any();
+    kani::assume(kani::forall!(|i in (0,10)| a[i] <= 10));
+
+    #[kani::loop_invariant( kaniindex <= 10 && sum <= (kaniindex as u32 * 10) )]


What is "kaniindex" here? Is that supposed to be connected to the value of the loop counter "i"? If so, why not just write "i"?

zhassan-aws · 2025-06-16T23:44:17Z

Can you expand the PR description and/or the comments in library/kani_macros/src/sysroot/loop_contracts/mod.rs to explain the idea behind the implementation? It is hard to infer what this is doing just through reading the code.

rod-chapman

Please address my documentation requests.

rod-chapman · 2025-06-19T08:46:05Z

docs/src/reference/experimental/loop-contracts.md

@@ -168,7 +168,7 @@ Kani automatically contracts (instead of unwinds) all loops in the functions tha

 Loop contracts comes with the following limitations.

-1. `while` loops and `loop` loops are supported. The other kinds of loops are not supported: [`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).
+1. `while` loops, `loop` loops are supported. `for` loops are supported for array, slice, Iter, Vec, Range, StepBy, Chain, Zip, Map, and Enumerate. The other kinds of loops are not supported: [`while let` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#predicate-pattern-loops).


You also need to document:

The use and meaning of the "kaniindex" name.

How iter().enumerate() can be used to get the index number of a for loop so it can be used in an invariant. Please illustrate this with a full example.

Please give a full example of a nested loop with invariants - for example, forming the sum of a two-dimemsional array of integers, and proving the upper-bound of the result.

Give an example of how to an iterator is applied with a for loop to iterate over a dynamic slice (i.e. a slice whose bounds are not known at compile time which is passed into a function as a formal parameter).

As you write the examples, add them as new tests cases obviously.

I would also like to see test cases where functions are declared inside a module with full pre/post-conditions contracts, rather than the "assume/assert test harness" style. We'll be using the former style in Crypto work, so you need to convince me that it really does work that way.

Hello, thank you very much for your suggestion.

I updated the document (loop-contracts.md file), which includes the kaniindex.

You can find the example in this file too.

The nested loop for for loop needs one extra component: the loop_assign clause because sometimes CBMC cannot infer it for the inner loop. I am implementing it and expect to finish next week. I will add that example after both PRs are merged.

Currently, Kani does not support fully unbounded slices, but it supports slices of arbitrary length. Please take a look at the file for_loop_for_slice, we consider a slice (s) unbounded when we set the length of a to be isize::MAX. However, until array theory is supported (we are working on it), the performance is unscalable w.r.t array size (slice length).

You can find examples of function-contracts in tests/expected/function-contracts.

Iteration and quantification over unbounded slices will be required for crypto work (e.g. where we're computing a function over a potentially very large array of bytes, such as a user-supplied message.)

I do not see the need for a scaling problem. The proofs can be generated in a fashion that is entirely symbolic with respect to the bounds of the slice. This is how it works in tools like Frama-C and SPARK Pro.

If I have a slice parameter - something like
fn f(a : &[u8]) -> i32
but I have a pre-condition something like
a.len <= 100

Why is that a problem?

@thanhnguyen-aws can you add @rod-chapman's example program here as a test (or a fixme test if it doesn't work?)

@carolynzech Which program are you referring to?

This one: #4143 (comment)

library/kani_macros/src/sysroot/loop_contracts/mod.rs

…into forloopnew1

docs/src/reference/experimental/loop-contracts.md

carolynzech · 2025-07-22T14:01:29Z

docs/src/reference/experimental/loop-contracts.md

+1. `kaniindex` : the position (index) of the current iteration in the iterator.
+2. `kaniiterlen` : the length of the iterator.


What is the point of exposing these values? I don't find the example compelling; I feel like if people want the position of the iterator they should just call enumerate and write assertions about i instead of us exposing a value?
Same goes for the length of the iterator; what's an example of something we might want to express but couldn't without exposing this value?

Also, what happens if someone tries to use kaniindex or kaniiterlen as local variables in their loop, like let kaniindex = ...?

We don't want to change user code in order to write a loop invariant. kaniiter and kaniindex are useful variables for loop-invariant, so I think it is helpful to provide them to the users. In case the users use enumerate, the index of the Enumerate Iterator is also different from kaniindex as only kaniindex is updated at the end of the loop body as demonstrated in [nested_forloop_for_enumerate.rs].

All extra variables are put together with a loop inside a block {} (by the proc macro) , so if the user defines variables with similar names, the loop-invariant always takes the ones that is generated by kani. I don't think user may name their variables that way unless they want to "hack" kani.

I tend to agree with @carolynzech here. It is customary to modify code for verification purposes, e.g. through adding "ghost" variables that are only used in invariants. I would vote for not exposing those variables.

But if we don't expose those variables, how are people going to express those loop invariants? Above, Thanh already explained how the approach with enumerate() wouldn't work.

I discussed with @thanhnguyen-aws offline and the reason enumerate wouldn't work is because of how we implemented it, but it should be possible to fix the implementation to make it work (@thanhnguyen-aws please correct me if I misunderstood).

One concern I raised with @thanhnguyen-aws is that exposing those variables means that we're committing to providing them for all possible iterator types. While an "index" shouldn't be an issue, "len" might not be easy to provide for all iterators (e.g. the Chars iterator). So if we decide to drop one of those variables in the future, this would break user code.

library/kani_core/src/iter.rs

carolynzech · 2025-07-22T14:11:46Z

library/kani_core/src/iter.rs

+                unsafe { &*self.ptr.wrapping_add(i) }
+            }
+            fn first(&self) -> Self::Item {
+                unsafe { &*self.ptr }
+            }
+            fn assumption(&self) -> bool {
+                unsafe { mem::is_allocated(self.ptr as *const (), self.len) }
+            }


Can you write // SAFETY comments above all of the unsafe code to explain why it's safe, c.f. the safety docs:

Whenever we write an unsafe function, it is idiomatic to write a comment starting with SAFETY and explaining what the caller needs to do to call the function safely. Likewise, whenever we perform an unsafe operation, it is idiomatic to write a comment starting with SAFETY to explain how the safety rules are upheld.

carolynzech · 2025-07-22T15:54:27Z

library/kani_core/src/iter.rs

+        use core_path::ops::Range;
+        use core_path::slice::Iter;
+
+        pub trait KaniIter


Can you put doc comments throughout this macro describing the purpose of each trait and the method in each trait? I'm having trouble telling if these implementations are correct when I'm not sure of the purpose of each thing.

carolynzech · 2025-07-22T15:55:56Z

docs/src/reference/experimental/loop-contracts.md

@@ -168,7 +168,7 @@ Kani automatically contracts (instead of unwinds) all loops in the functions tha

 Loop contracts comes with the following limitations.

-1. `while` loops and `loop` loops are supported. The other kinds of loops are not supported: [`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).
+1. `while` loops, `loop` loops are supported. `for` loops are supported for array, slice, Iter, Vec, Range, StepBy, Chain, Zip, Map, and Enumerate. The other kinds of loops are not supported: [`while let` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#predicate-pattern-loops).


@thanhnguyen-aws can you add @rod-chapman's example program here as a test (or a fixme test if it doesn't work?)

carolynzech · 2025-07-22T16:07:39Z

rfc/src/rfcs/0012-loop-contracts.md

@@ -214,6 +214,104 @@ the name of its `kani::any()` function, and add the map to the loop latch too.
 On the CBMC site, `goto-instrument` will extract the map and instrument the customized
 havocing functions for the modifies targets.

+### For-loop rewrite 


I just noticed this RFC has a section on loop-decreases that seems to imply that decreases will always be required to prove termination, but we've written plenty of loops without it. Can you update that text to reflect the current implementation? Can be in a separate PR if you prefer. Also the status field at the top should be changed to unstable.

loop-decrease is not supported yet. As mentioned Limitation section of loop-contract.md : "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." .

carolynzech · 2025-07-22T16:10:28Z

rfc/src/rfcs/0012-loop-contracts.md

@@ -214,6 +214,104 @@ the name of its `kani::any()` function, and add the map to the loop latch too.
 On the CBMC site, `goto-instrument` will extract the map and instrument the customized
 havocing functions for the modifies targets.

+### For-loop rewrite 
+
+When there is loop-invariant for `for-loop`, the `loop_invariant` procedural macros 


This is a really nice explanation; thank you for writing it!

Co-authored-by: Carolyn Zech <carolynzech@gmail.com>

tautschnig · 2025-07-25T13:46:11Z

The PR description says "for loop for 4 types: array, slice, Iter, Vec, Range, StepBy, Map, Chain, Zip, Enumerate." -- that's 10 items enumerated here, not 4?

tautschnig

Looks good to me!

rfc/src/rfcs/0012-loop-contracts.md

Co-authored-by: Michael Tautschnig <mt@debian.org>

zhassan-aws · 2025-07-25T17:03:51Z

docs/src/reference/experimental/loop-contracts.md

@@ -1,13 +1,15 @@
-# Loop Contracts
+# Loop Invariants


Why the name change?

If the renaming is something that was agreed on, it should be done in a separate PR. Adding support for "for" loops already requires so many changes, so we should avoid convoluting it with other unrelated changes.

docs/src/reference/experimental/loop-contracts.md

zhassan-aws · 2025-07-25T21:19:34Z

docs/src/reference/experimental/loop-contracts.md

 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 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.
+Loop-invariants are used to abstract out loops as non-loop blocks to avoid loop unwinding, and hence remove the bounds on the inputs.


Please replace all occurrences of "Loop-invariants" with "Loop invariants" (i.e. remove the dash).

docs/src/reference/experimental/loop-contracts.md

zhassan-aws · 2025-07-25T21:24:03Z

docs/src/reference/experimental/loop-contracts.md


-Check 11: simple_loop_with_loop_contracts.loop_modifies.1
+Check 11: simple_loop_with_loop_invariants.loop_assigns.1


Was loop_modifies renamed to loop_assigns in this PR? I'm not clear where this is done.

It was an accident when I replace all loop_assigns to loop_modifies, I will correct it.

zhassan-aws · 2025-07-25T21:37:17Z

rfc/src/rfcs/0012-loop-contracts.md

+
+```Rust
+let a : [u8,10] = kani::any();
+let kani_iter_xxxx = kani::kani_into_iter(a);


Why the _xxxx suffix?

_xxxx is a hash code that is generated from the position of the loop. It is a technique to hide proc-macro generated variables from user. We would apply the same technique to kani_index and kani_iter_len if we decide to hide them.

zhassan-aws · 2025-07-25T21:38:03Z

rfc/src/rfcs/0012-loop-contracts.md

+```Rust
+let a : [u8,10] = kani::any();
+let kani_iter_xxxx = kani::kani_into_iter(a);
+let kaniiterlen = kani_iter_xxxx.len();


Use snake case for variable names, e.g. kani_iter_len.

zhassan-aws · 2025-07-25T21:38:20Z

rfc/src/rfcs/0012-loop-contracts.md

+let kani_iter_xxxx = kani::kani_into_iter(a);
+let kaniiterlen = kani_iter_xxxx.len();
+let mut i = kani_iter_xxxx.first()
+let mut kaniindex = 0;


Same here: kaniindex -> kani_index.

zhassan-aws · 2025-07-25T21:38:41Z

rfc/src/rfcs/0012-loop-contracts.md

+let mut i = kani_iter_xxxx.first()
+let mut kaniindex = 0;
+#[kani::loop_invariant(...)]
+while (kaniindex < kaniiterlen) {


There are no parentheses for while/if conditions in Rust

zhassan-aws · 2025-07-25T21:39:09Z

rfc/src/rfcs/0012-loop-contracts.md

+let mut kaniindex = 0;
+#[kani::loop_invariant(...)]
+while (kaniindex < kaniiterlen) {
+  i = kani_iter_xxxx.indexing(kaniindex);


What does the indexing method do? Where is it defined?

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

thanhnguyen-aws requested a review from a team as a code owner June 6, 2025 20:47

github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jun 6, 2025

carolynzech marked this pull request as draft June 10, 2025 02:09

tautschnig assigned thanhnguyen-aws Jun 11, 2025

thanhnguyen-aws force-pushed the forloopnew1 branch from 1dc30e6 to a5d568b Compare June 11, 2025 18:25

thanhnguyen-aws marked this pull request as ready for review June 11, 2025 19:15

thanhnguyen-aws force-pushed the forloopnew1 branch from 6377782 to 1a8dceb Compare June 12, 2025 17:20

carolynzech requested changes Jun 16, 2025

View reviewed changes

rod-chapman reviewed Jun 16, 2025

View reviewed changes

thanhnguyen-aws added 8 commits June 18, 2025 11:48

add for loop transformation

ded56d8

add support for array, slice and Iter + expected tests

2f782bf

add support for Range, StepBy + expected tests

d0a902e

add support for Vec + expected tests

32e978c

add expected tests for quantifiers and tuples

8529488

add support for Zip, Chain, Map + expected tests

d028bb0

add support for Enumerate + expected tests

3fc2abc

edit loop-contract docs

8e69667

thanhnguyen-aws force-pushed the forloopnew1 branch from 2a22aaf to 8e69667 Compare June 18, 2025 22:26

rod-chapman reviewed Jun 19, 2025

View reviewed changes

thanhnguyen-aws requested a review from carolynzech June 19, 2025 15:42

edit doc and some typos

746311a

thanhnguyen-aws force-pushed the forloopnew1 branch from 33b34b2 to 746311a Compare June 19, 2025 16:19

Merge branch 'main' into forloopnew1

475718e

github-actions bot added the Z-CompilerBenchCI Tag a PR to run benchmark CI label Jun 24, 2025

thanhnguyen-aws added 2 commits July 1, 2025 09:12

merge origin

09f5dcc

restore mod.rs after merge

ded103c

tautschnig assigned tautschnig and unassigned thanhnguyen-aws Jul 11, 2025

tautschnig reviewed Jul 11, 2025

View reviewed changes

library/kani_macros/src/sysroot/loop_contracts/mod.rs Show resolved Hide resolved

tautschnig assigned zhassan-aws Jul 11, 2025

thanhnguyen-aws added 3 commits July 14, 2025 08:23

Merge branch 'main' into forloopnew1

418f4f3

handling StorageLive/StorageDead for forloop variables

2712069

add expected tests for nested forloop

da1666d

thanhnguyen-aws force-pushed the forloopnew1 branch from 91423cf to 184eb14 Compare July 17, 2025 19:45

fix clippy

f9a3c2f

thanhnguyen-aws force-pushed the forloopnew1 branch from 184eb14 to f9a3c2f Compare July 17, 2025 20:19

thanhnguyen-aws requested a review from tautschnig July 17, 2025 21:36

thanhnguyen-aws added 3 commits July 18, 2025 07:34

Merge branch 'main' into forloopnew1

f8e2232

add for-loop rewrite method in loop-contract rfc

8eb51e6

Merge branch 'forloopnew1' of https://github.com/thanhnguyen-aws/kani …

b4f470d

…into forloopnew1

carolynzech reviewed Jul 22, 2025

View reviewed changes

thanhnguyen-aws and others added 3 commits July 22, 2025 13:19

Update docs/src/reference/experimental/loop-contracts.md

6c3e159

Co-authored-by: Carolyn Zech <carolynzech@gmail.com>

Merge branch 'main' into forloopnew1

fa5436e

add more docs

ceaed0b

tautschnig reviewed Jul 25, 2025

View reviewed changes

rfc/src/rfcs/0012-loop-contracts.md Outdated Show resolved Hide resolved

rfc/src/rfcs/0012-loop-contracts.md Outdated Show resolved Hide resolved

rfc/src/rfcs/0012-loop-contracts.md Outdated Show resolved Hide resolved

tautschnig assigned thanhnguyen-aws and unassigned tautschnig Jul 25, 2025

thanhnguyen-aws and others added 3 commits July 25, 2025 09:35

Update rfc/src/rfcs/0012-loop-contracts.md

cbcc7c3

Co-authored-by: Michael Tautschnig <mt@debian.org>

Update rfc/src/rfcs/0012-loop-contracts.md

8618f55

Co-authored-by: Michael Tautschnig <mt@debian.org>

Update rfc/src/rfcs/0012-loop-contracts.md

42e6fc6

Co-authored-by: Michael Tautschnig <mt@debian.org>

zhassan-aws reviewed Jul 25, 2025

View reviewed changes

thanhnguyen-aws and others added 7 commits July 28, 2025 08:59

Update rfc/src/rfcs/0012-loop-contracts.md

1e4ffdd

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update rfc/src/rfcs/0012-loop-contracts.md

bb3f439

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update rfc/src/rfcs/0012-loop-contracts.md

b716b97

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update docs/src/reference/experimental/loop-contracts.md

e67148d

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update docs/src/reference/experimental/loop-contracts.md

860430f

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update rfc/src/rfcs/0012-loop-contracts.md

64833dd

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update rfc/src/rfcs/0012-loop-contracts.md

202880e

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

		1. `kaniindex` : the position (index) of the current iteration in the iterator.
		2. `kaniiterlen` : the length of the iterator.


		Check 11: simple_loop_with_loop_contracts.loop_modifies.1
		Check 11: simple_loop_with_loop_invariants.loop_assigns.1

Add loop-contracts support for for loop #4143

Are you sure you want to change the base?

Add loop-contracts support for for loop #4143

Uh oh!

Conversation

thanhnguyen-aws commented Jun 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

carolynzech left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

zhassan-aws commented Jun 16, 2025

Uh oh!

rod-chapman left a comment

Choose a reason for hiding this comment

Uh oh!

rod-chapman Jun 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jul 25, 2025

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Add loop-contracts support for `for` loop #4143

Add loop-contracts support for `for` loop #4143

thanhnguyen-aws commented Jun 6, 2025 •

edited

Loading

rod-chapman Jun 19, 2025 •

edited

Loading

zhassan-aws Jul 25, 2025 •

edited

Loading