Loop invariants

[W95Psp]

This PR recognizes and transforms in a particular way the following loops. It also injects invariants.

fn range() {
    let mut count = 0u64;
    for i in 0u8..10u8 {
        hax_lib::loop_invariant!(|i: u8| i <= 10);
        count += 1;
    }
}
fn range_step_by() {
    let mut count = 0u64;
    for i in (0u8..10u8).step_by(2) {
        hax_lib::loop_invariant!(|i: u8| i <= 10);
        count += 1;
    }
}
fn enumerated_slice<T>(slice: &[T]) {
    let mut count = 0u64;
    for i in slice.into_iter().enumerate() {
        hax_lib::loop_invariant!(|i: usize| i <= 10);
        count += 2;
    }
}
fn enumerated_chunked_slice<T>(slice: &[T]) {
    let mut count = 0u64;
    for i in slice.chunks_exact(3).enumerate() {
        hax_lib::loop_invariant!(|i: usize| { fstar!("$i <= ${slice.len()}") });
        count += 3;
    }
}

Open this code snippet in the playground

The design is not great, I copy paste here the documentation of loop_invariant:

/// Add an invariant to a loop which deals with an index. The
/// invariant cannot refer to any variable introduced within the
/// loop. An invariant is a closure that takes one argument, the
/// index, and returns a boolean.
///
/// Note that loop invariants are unstable (this will be handled in a
/// better way in the future, see
/// https://github.com/hacspec/hax/issues/858) and only supported on
/// specific `for` loops with specific iterators:
///
///  - `for i in start..end {...}`
///  - `for i in (start..end).step_by(n) {...}`
///  - `for i in slice.enumerate() {...}`
///  - `for i in slice.chunks_exact(n).enumerate() {...}`
///
/// This function must be called on the first line of a loop body to
/// be effective. Note that in the invariant expression, `forall`,
/// `exists`, and `BACKEND!` (`BACKEND` can be `fstar`, `proverif`,
/// `coq`...) are in scope.

This fixes #605.

Things left to do:

• add F* definitions