Attribute Macro invariant 

#[invariant]

A loop invariant

A loop invariant is an assertion (in pearlite) which must be true at every iteration of the loop.

See the guide: Loop invariants.

Not to be confused with type invariants or resource invariants.

produced

If the loop is a for loop, you have access to a special variable produced, that holds a sequence of all the (logical representations of) items the iterator yielded so far.

Example

let mut v = Vec::new();
#[invariant(v@.len() == produced.len())]
#[invariant(forall<j> 0 <= j && j < produced.len() ==> v@[j]@ == j)]
for i in 0..10 {
    v.push(i);
}