Opaque least predicate with existential does not verify in some cases

[ymherklotz]

Dafny version

3.11.0.50201

Code to produce this issue

// Case 1 verifies
least predicate {:opaque} Spec1(i: int) {
    exists j :: Spec1(j)
}

lemma L1() {
    reveal Spec1();
    assume Spec1(200);
    assert exists j :: Spec1(j);
    assert Spec1(100);
}

// Case 2 does not verify
least predicate Rule2(i: int, j: int) {
    Spec2(j)
}

least predicate {:opaque} Spec2(i: int) {
    exists j :: Rule2(i, j)
}

lemma L2() {
    reveal Spec2();
    assume Spec2(200);
    assert Rule2(100, 200); // VERIFIES
    assert exists j :: Rule2(100, j); // VERIFIES
    assert Spec2(100); // ERROR ONLY HERE
}

// Case 3 verifies
least predicate Rule3(i: int, j: int) {
    Spec3(j)
}

least predicate Wrapped3(i: int) {
    exists j :: Rule3(i, j)
}

least predicate {:opaque} Spec3(i: int) {
    Wrapped3(i)
}

lemma L3() {
    reveal Spec3();
    assume Spec3(200);
    assert Rule3(100, 200);
    assert Wrapped3(100);
    assert Spec3(100);
}

Command to run and resulting output

dafny verify Code.dfy

What happened?

Hi, I’m having the following issue with a combination of a few Dafny features: least predicate, opaque and exists (if one of these features is absent all cases seem to verify). I tried coming up with a minimal example that doesn’t quite make sense logically, but shows the problem.

For some context, I used to have my specification defined in the style of Case 1. I can then verify that assuming that Spec1(200) holds, that Spec(100) holds too, which follows from the definition directly.

// Case 1 verifies
least predicate {:opaque} Spec1(i: int) {
    exists j :: Spec1(j)
}

lemma L1() {
    reveal Spec1();
    assume Spec1(200);
    assert exists j :: Spec1(j);
    assert Spec1(100);
}

However, once I added many more disjunctions, the predicate became a bit too big, so I tried splitting each case into separate predicates (shown in Case 2). However, I ran into issues where I couldn’t prove direct things about the predicate anymore, like assume that a disjunct holds and therefore showing that the whole predicate holds. In the following, assuming the same things as for Case 1, I can’t seem to prove that Spec2(100) holds anymore.

// Case 2 does not verify
least predicate Rule2(i: int, j: int) {
    Spec2(j)
}

least predicate {:opaque} Spec2(i: int) {
    exists j :: Rule2(i, j)
}

lemma L2() {
    reveal Spec2();
    assume Spec2(200);
    assert Rule2(100, 200);           // VERIFIES
    assert exists j :: Rule2(100, j); // VERIFIES
    assert Spec2(100);                // ERROR ONLY HERE
}

Finally, it seems like adding one more layer of indirection (with a Wrapped3 predicate) in Case 3 makes everything work again which is interesting.

// Case 3 verifies
least predicate Rule3(i: int, j: int) {
    Spec3(j)
}

least predicate Wrapped3(i: int) {
    exists j :: Rule3(i, j)
}

least predicate {:opaque} Spec3(i: int) {
    Wrapped3(i)
}

lemma L3() {
    reveal Spec3();
    assume Spec3(200);
    assert Rule3(100, 200);
    assert Wrapped3(100);
    assert Spec3(100);
}

My current work around is to either use Case 1 and have the predicate Opaque, or use Case 2 with the predicate not opaque, which also works fine but I wanted to make it opaque because I felt like proofs were slowing down a bit. Case 3 is a bit unwieldly.

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

Mac