Dafny proves false using some complicated loop invariants

[anthowan]

Dafny version

both 4.10.0 and nightly-2025-03-17-2473d8d

Code to produce this issue

// Largest power of 2 that divides i
function lsb(i: nat): nat
    requires i > 0
    ensures 0 < lsb(i) <= i
{
    if i % 2 == 1 then 1 else 2 * lsb(i / 2)
}

opaque ghost function sum(s: seq<int>): int
{
    if |s| == 0 then 0 else s[0] + sum(s[1..])
}

class fenwick {
    var N: nat
    ghost var A: seq<int>
    var F: array<int>

    constructor (A': seq<int>)
        ensures F.Length == |A'| + 1
        ensures F.Length > 0
        ensures F.Length > 0 ==> false
        ensures false
    {
        N := |A'|;
        A := A';
        F := new int[|A'| + 1](i => if 0 < i <= |A'| then A'[i - 1] else 0);
        new;

        for i := 1 to F.Length
            modifies F
            // These invariants are complete garbage and wrong
            invariant forall j :: i < j <= N && j - lsb(j) / 2 >= i ==> F[j] == A[j - 1]
            invariant forall j :: 0 < j <= i <= N ==> lsb(j) > 0 && F[j] == sum(A[j - lsb(j)..j])
            invariant forall j :: 0 < j < i && i <= j + lsb(j) <= N ==> lsb(j) <= lsb(j + lsb(j)) && F[j + lsb(j)] == A[j + lsb(j) - 1] + sum(A[j + lsb(j) - lsb(j + lsb(j))..j])
            invariant i > 0 ==> false
        {
            var j := i + lsb(i);
            if j < F.Length {
                F[j] := F[j] + F[i];
                assert F[j] == A[j - 1];
                assert false;
            }
            assert false;
        }
        assert F.Length > 0 ==> false;
    }
}

method Main()
    ensures false
{
    var FT := new fenwick([0]);
    assert false;
    assert 0 == 1;

    assert FT.N == 69;
    print FT.N; // Actually prints 1
}

Command to run and resulting output

Both dafny verify and dafny run -t py claim that the program verifies without any errors.

What happened?

I was trying to formally verify Fenwick trees and somehow managed to write some weird and complicated loop invariants that cause Dafny to get very confused and prove false, which should not happen.

Even dafny verify --analyze-proofs main.dfy doesn't produce errors and only produces a bunch of warnings:

false.dfy(20,16): Warning: ensures clause proved using contradictory assumptions
   |
20 |         ensures F.Length == |A'| + 1
   |                 ^^^^^^^^^^^^^^^^^^^^

false.dfy(21,16): Warning: ensures clause proved using contradictory assumptions
   |
21 |         ensures F.Length > 0
   |                 ^^^^^^^^^^^^

false.dfy(22,33): Warning: ensures clause proved using contradictory assumptions
   |
22 |         ensures F.Length > 0 ==> false
   |                                  ^^^^^

false.dfy(23,16): Warning: ensures clause proved using contradictory assumptions
   |
23 |         ensures false
   |                 ^^^^^

false.dfy(39,25): Warning: proved using contradictory assumptions: function precondition satisfied
   |
39 |             var j := i + lsb(i);
   |                          ^^^^^^

false.dfy(39,29): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
   |
39 |             var j := i + lsb(i);
   |                              ^

false.dfy(40,19): Warning: proved using contradictory assumptions: target object is never null
   |
40 |             if j < F.Length {
   |                    ^^^^^^^^

false.dfy(41,16): Warning: proved using contradictory assumptions: array is never null
   |
41 |                 F[j] := F[j] + F[i];
   |                 ^

false.dfy(41,16): Warning: proved using contradictory assumptions: an array element is in the enclosing context's modifies clause
   |
41 |                 F[j] := F[j] + F[i];
   |                 ^^^^

false.dfy(41,16): Warning: proved using contradictory assumptions: index in range
   |
41 |                 F[j] := F[j] + F[i];
   |                 ^^^^

false.dfy(41,24): Warning: proved using contradictory assumptions: array is never null
   |
41 |                 F[j] := F[j] + F[i];
   |                         ^

false.dfy(41,24): Warning: proved using contradictory assumptions: index in range
   |
41 |                 F[j] := F[j] + F[i];
   |                         ^^^^

false.dfy(41,31): Warning: proved using contradictory assumptions: array is never null
   |
41 |                 F[j] := F[j] + F[i];
   |                                ^

false.dfy(41,31): Warning: proved using contradictory assumptions: index in range
   |
41 |                 F[j] := F[j] + F[i];
   |                                ^^^^

false.dfy(42,16): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
   |
42 |                 assert F[j] == A[j - 1];
   |                 ^^^^^^^^^^^^^^^^^^^^^^^^

false.dfy(42,23): Warning: proved using contradictory assumptions: array is never null
   |
42 |                 assert F[j] == A[j - 1];
   |                        ^

false.dfy(42,23): Warning: proved using contradictory assumptions: index in range
   |
42 |                 assert F[j] == A[j - 1];
   |                        ^^^^

false.dfy(42,31): Warning: proved using contradictory assumptions: index in range
   |
42 |                 assert F[j] == A[j - 1];
   |                                ^^^^^^^^

false.dfy(47,15): Warning: proved using contradictory assumptions: target object is never null
   |
47 |         assert F.Length > 0 ==> false;
   |                ^^^^^^^^

false.dfy(47,15): Warning: unnecessary (or partly unnecessary) assert statement
   |
47 |         assert F.Length > 0 ==> false;
   |                ^^^^^^^^^^^^^^^^^^^^^^

false.dfy(47,32): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
   |
47 |         assert F.Length > 0 ==> false;
   |                                 ^^^^^

false.dfy(52,12): Warning: ensures clause proved using contradictory assumptions
   |
52 |     ensures false
   |             ^^^^^

false.dfy(56,4): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
   |
56 |     assert 0 == 1;
   |     ^^^^^^^^^^^^^^

false.dfy(58,4): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)
   |
58 |     assert FT.N == 69;
   |     ^^^^^^^^^^^^^^^^^^

false.dfy(58,11): Warning: proved using contradictory assumptions: target object is never null
   |
58 |     assert FT.N == 69;
   |            ^^^^

false.dfy(59,10): Warning: proved using contradictory assumptions: target object is never null
   |
59 |     print FT.N; // Actually prints 1
   |           ^^^^


Dafny program verifier finished with 5 verified, 0 errors
Compilation failed because warnings were found and --allow-warnings is false

What type of operating system are you experiencing the problem on?

Linux

[RustanLeino]

Thanks for the bug report!

I'm looking into this issue. I'm not yet sure what's causing the problem, because small (and seemingly irrelevant) changes to the program text cause errors to be reported as expected. For example, while dafny verify exhibits the unsoundness, dafny run detects it, as does dafny verify --relax-definite-assignment, but I don't see why they would make any difference.

For now, I'm recording here a shorter repro:

function lsb(i: nat): nat
  requires i > 0
  ensures 0 < lsb(i) <= i
{
  if i % 2 == 1 then 1 else 2 * lsb(i / 2)
}

opaque ghost function sum(s: seq<int>): int
{
  if |s| == 0 then 0 else s[0] + sum(s[1..])
}

method MMM(A': seq<int>)
  ensures false
{
  var A: seq<int> := A';
  var N: nat := |A|;
  var F: array<int>;

  F := new int[|A| + 1](i => if 0 < i <= |A| then A[i - 1] else 0);

  for i := 1 to F.Length
    // These invariants are complete garbage and wrong
    invariant forall j :: i < j <= N && j - lsb(j) / 2 >= i ==> F[j] == A[j - 1]
    invariant forall j :: 0 < j <= i <= N ==> lsb(j) > 0 && F[j] == sum(A[j - lsb(j)..j])
    invariant forall j :: 0 < j < i && i <= j + lsb(j) <= N ==>
      lsb(j) <= lsb(j + lsb(j)) &&
      F[j + lsb(j)] == A[j + lsb(j) - 1] + sum(A[j + lsb(j) - lsb(j + lsb(j))..j])
    invariant i > 0 ==> false
  {
    var j := lsb(i);
  }
}```