Annotations for loop invariants

[W95Psp]

Requires #394

[mamonet]

It would be great if we can define loop invariant to keep track on updated variable inside the loop body for each iteration. Here is a use case for the feature
In the following loop body, we need to have invariant for updated variable zeta_i to tell the resolver that its value is still inside the boundaries https://github.com/cryspen/libcrux/blob/ml-kem-lax-check/libcrux-ml-kem/src/ntt.rs#L61-L63

The feature can replace the assumptions in this code https://github.com/cryspen/libcrux/blob/ml-kem-panic-free/libcrux-ml-kem/src/ntt.rs#L66-L69 to make it verify.

[mamonet]

One more instance of this issue, in situations where we use enumerate(), we have to make assumptions around the index that should happen be default in case Core.Iter.Traits.Iterator.f_enumerate maintains the index through iterations. e.g. for this loop we need to tell assist the resolver by assuming the index is inside the boundaries https://github.com/cryspen/libcrux/blob/ml-kem-panic-free/libcrux-ml-kem/src/serialize.rs#L65-L67

[franziskuskiefer]

We may not tackle #394 right away but use workarounds for now.

Next step: make design