E0039

Warning name: missing_reasoning

This warning is emitted for a proof-checked for loop that has no proof_reasoning clause. Proof reasoning records the argument that explains why the loop invariants are maintained and why the loop result satisfies the surrounding contract.

Erroneous example

The loop does not have a proof_reasoning 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 reasoning.

///|
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_reasoning: (
      #|The variables `a` and `b` represent consecutive Fibonacci numbers, 
      #|so `a` is always less than or equal to `b`.
      #|
    ),
  }
}