Attribute Macro loop_invariant

#[loop_invariant]

Add a loop invariant to this loop.

The contents of the attribute is a condition that should be satisfied at the beginning of every iteration of the loop. All Rust syntax is supported, even calling other functions, but the computations must be side effect free, e.g. it cannot perform I/O or use mutable memory.