E0038

Warning name: missing_invariant

This warning is emitted for a proof-checked for loop that has no proof_invariant clause. A loop invariant records the facts that must hold before and after every iteration, so the verifier can reason about the loop body and the nobreak result.

Erroneous example

The loop does not have a proof_invariant clause.

///|
fn fib(n : Int) -> UInt64 {
  for i = 0, a = 0UL, b = 1UL; i < n; i = i + 1, a = b, b = a + b {

  } nobreak {
    b
  }
}

Suggestion

Add some proof invariants.

///|
fn fib(n : Int) -> UInt64 {
  for i = 0, a = 0UL, b = 1UL; i < n; i = i + 1, a = b, b = a + b {

  } nobreak {
    b
  } where {
    proof_invariant: a <= b,
  }
}