E0038

Warning name: missing_invariant

当需要进行证明检查的 for 循环没有 proof_invariant 子句时，会发出此警告。循环不变量记录了每次迭代前后都必须成立的事实，使验证器能够推理循环体和 nobreak 结果。

错误案例

循环缺少 proof_invariant 子句。

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

  } else {
    b
  }
}

建议

添加一些证明不变量。

///|
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,
  }
}