E8008

Error · Contract/Verification

E8008 — A loop invariant that the prover cannot show to hold when the loop starts

What the compiler reports

Error[E8008] at {{.*}}loop_inv_fail.vx:[[@LINE+1]]:30: this loop invariant `N == 1` may not hold when the loop starts
Error[E8008] at {{.*}}loop_inv_fail.vx:[[@LINE+1]]:29: this loop invariant `N > 10` may not hold when the loop starts

The fragments the test suite holds the compiler to. An ellipsis marks text the test does not constrain; the emitted message also carries a source location.

A program that triggers it

fn test_loop_increment_fail(N : i32) -> i32
requires N == 0
ensures return == 0 {
  // FAILS because the invariant demands N == 1, which is not true initially.
  for i in 0..10 invariant(N == 1) {
    let x = N;
  }
  return N;
}

fn test_loop_range_fail(N : i32) -> i32
requires N > 5 && N < 15 ensures return > 5
{
  // FAILS because invariant N > 10 is not guaranteed initially.
  for i in 0..5 invariant(N > 10) {
    let dummy = N;
  }
  return N;
}

fn main() -> i32 {
  return 0;
}

From tests/frontend/fail/formal_verification/loop_inv_fail.vx, which asserts this diagnostic on every commit.

Related