Add loop-contracts support for for loop

[thanhnguyen-aws]

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

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

for pat in expr {
    body
}

is transformed into a while loop:

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

Note that

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

2. The init_index_stmt and init_pat_stmt support writing the loop-invariant properties that involve pat and kaniindex

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

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

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

[zhassan-aws]

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.

[tautschnig]

Should we really make all these changes from "invariant" to "contract"? I'm making a suggestion to explain how "loop contracts" and "loop invariants" are related, but I don't know whether others share my view on this matter.

[rod-chapman]

In short:

1. Can this be done without the "clone" of a? I see no need for it, and possibly huge performance impact.
2. The "60" bounds on b is wrong surely? b should have the same size as a.len(), right?
3. Please demonstrate how auto-harness generation works on these functions, so the harness functions are not required.

[tautschnig]

We may still need to follow up this work with some refinement, but this should be ready for broader evaluation.

Stale review.