Cannot prove tautology with map, opaque function and transparent function.

[MikaelMayer]

Consider the following code:

function {:opaque} f(t: int): int { t }
function summarize(input: map<int, int>): int { |input| }

lemma lemme(input: map<int, int>, i: int, m: map<int, int>) {
    reveal f();
    assert  i == summarize(map k <- input :: f(k));
    assert  i == summarize(map k <- input :: f(k));
}

The last two asserts are failing, although they are identical. Changing the fuel of any function above does not help.
Note that the problem goes away either:

• If you remove the call to summarize
• If you replace the call f(k) by k
• If you remove {:opaque} from f and the reveal f(); (just removing the reveal f(); does not solve the problem)
• If you replacei == summarizeChildren( by m ==

Looking at Boogie
The reveal statement generates no code in Boogie. That's weird.

As in #1631, the fuel is the only difference. However, contrary to #1631; all opaque functions are revealed and the problem is still there.

    assert {:subsumption 0} i#0
       == _module.__default.summarize(StartFuelAssert__module._default.summarize, 
        Map#Glue((lambda $w#4: Box :: $IsBox($w#4, TInt) && Map#Domain(input#0)[$w#4]), 
          (lambda $w#4: Box :: 
            $Box(_module.__default.f(StartFuelAssert__module._default.f, $Unbox($w#4): int))), 
          TMap(TInt, TInt)));
    assume i#0
       == _module.__default.summarize(StartFuel__module._default.summarize, 
        Map#Glue((lambda $w#5: Box :: $IsBox($w#5, TInt) && Map#Domain(input#0)[$w#5]), 
          (lambda $w#5: Box :: 
            $Box(_module.__default.f(StartFuel__module._default.f, $Unbox($w#5): int))), 
          TMap(TInt, TInt)));

Why it matters

• Normally the second assert is in a postcondition, and I want to prove it.
• Normally, the first assert should have a variation of the second one that guides the verifier to prove the second one. But, if the tautology cannot be proven, any other variation does not help either.

[MikaelMayer]

Essentially, the problem reduces to having to prove the following, where MoreFuel__module._default.f0 is uninterpreted when f is opaque and then revealed, and $LZ when f is not opaque (that's why opaqueness does not matter):

assert    (lambda $w#5: Box :: 
            $Box(_module.__default.f($LS(MoreFuel__module._default.f0), $Unbox($w#5): int)))
       == (lambda $w#5: Box :: 
            $Box(_module.__default.f($LS($LS(MoreFuel__module._default.f0)), $Unbox($w#5): int)));

which fails.

However, I can assert and then assume the following without problem, although it does not help.

assert (forall $w#5: Box ::
           _module.__default.f($LS(MoreFuel__module._default.f0), $Unbox($w#5): int)
       == _module.__default.f($LS($LS(MoreFuel__module._default.f0)), $Unbox($w#5): int));

Ideally thus, I would like to instantiate a higher-level axiom that says that two lambdas are the same iff their body can be proven to be equal, for all their inputs. The problem is, I did not find how to abstract their bodies easily like this:

assume (forall f, g ::
            (forall x :: f(x) == g(x)) ==>
            (lambda x: Box :: f(x))
         == (lambda x: Box :: g(x)));

the only way I found to be able to quantify over functions so far is to use the Dafny encoding, and thus the axiom becomes too different from what we want to prove:

   assume (forall f: HandleType, g: HandleType ::
            (forall x: Box :: Apply1(TInt, TInt, $Heap, f, x) == Apply1(TInt, TInt, $Heap, g, x)) ==>
            (lambda x: Box :: Apply1(TInt, TInt, $Heap, f, x))
         == (lambda x: Box :: Apply1(TInt, TInt, $Heap, g, x)));

This axiom will never match the expression above.

So for now, In Boogie, we could simply assume an instantation of this axiom, and I verified that it is sufficient to prove the rest

    assume  (forall $lt: LayerType, $lt2: LayerType ::
              (forall $w#5: Box ::
                 $Box(_module.__default.f($lt, $Unbox($w#5): int))
              == $Box(_module.__default.f($lt2, $Unbox($w#5): int))
            ) ==>
           (lambda $w#5: Box :: $Box(_module.__default.f($lt, $Unbox($w#5): int)))
       ==  (lambda $w#5: Box :: $Box(_module.__default.f($lt2, $Unbox($w#5): int))));

But that does not scale very well. I'm not sure how we would detect when to actually write such an axiom. The above would not cover the case when f is further wrapped by another function.

I suggest, for the sake of completeness, that we add a Dafny construct:

lambda_equal((x: int) => f(x))

that will explicit the axiom for which two lambdas can be equal. And we could automatically inline it for some trivial cases like mine.

Another way would be to not use Boogie's lambdas, and encode variable names with wrappers, such as Lambda(Var("$w#5"), $Box, $Box(_module.__default.f($lt, $Unbox(Var("$w#5")): int))
We would need more axioms to evaluate a lambda call and I'm not sure if it works.

Feedback wanted.

[cpitclaudel]

We do not have functional extensionality in Dafny's theory. I asked @RustanLeino about it recently, and he thought it would be non-trivial to add. Part of the issue is that lambdas can read the heap, so pointwise equality without considering the heap is not enough.

That said, I'm surprised that you would need extensionality here. I think the equations that you listed may be too strong: do we really need equalities on functions, or couldn't we get away with equalities on Map#Glue? Specifically, we want to say that Map#Glue is a morphism for pointwise equality, i.e. Map#Glue(f0, f1) == Map#Glue(f0', f1') <== (forall x :: f0(x) == f0'(x) && forall x :: f1(x) == f1'(x)).

But in fact I'm not sure we don't even really need this; instead we want to fix the thing that makes the fuel differ between these two expressions. Beyond that, it's expected that in Dafny sometimes you need to explicitly assert equalities between sequences or maps, because these get translated to Seq#Equal and Map#Equal instead of plain equality. What makes this example striking is that the expressions are literally the same, and we should fix it by making sure that they are translated the same.

Here is a simplified example to illustrate the point I'm making:

function f(t: int): int
function summarize(input: map<int, int>): int { |input| }

lemma lemme(input: map<int, int>, i: int, m: map<int, int>) {
  var m := map k <- input :: f(k) + 1 - 1;
  var m' := map k <- input :: f(k);
  // assert m == m';
  assume  i == summarize(m);
  assert  i == summarize(m');
}

This example fails without the assert, but it succeeds with it. That's because the assert doesn't get translated to a plain equality, but instead to Map#Equal, which triggers the map extensionality axiom, which is essentially the morphism that I posted above.

So, in a sense, we already have the required extensionality, but just for maps:

axiom (forall<U,V> m: Map U V, m': Map U V :: 
  { Map#Equal(m, m') } 
  Map#Equal(m, m')
     <==> (forall u: U :: Map#Domain(m)[u] == Map#Domain(m')[u])
       && (forall u: U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u]));

axiom (forall<U,V> m: Map U V, m': Map U V :: 
  { Map#Equal(m, m') } 
  Map#Equal(m, m') ==> m == m');

It's just that you need an explicit == between maps to trigger them… and the original example is surprising because the expressions are literally the same. IMO, this means that we need to worry about the translation of syntactically equivalent expressions, but not about function equalities.

[MikaelMayer]

Following your idea, I added the following axiom to the boogie prelude manually:

axiom (forall a: [Box]bool, b: [Box]Box, t0: Ty, t1: Ty :: 
  { Map#Glue(a, b, TMap(t0, t1)) } 
    (forall a2: [Box]bool, b2: [Box]Box, t2: Ty, t3: Ty ::
    Map#Glue(a, b, TMap(t0, t1)) == Map#Glue(a2, b2, TMap(t2, t3))
     <==> (forall u: Box :: a[u] == a2[u])
       && (forall u: Box :: b[u] == b2[u])
       && t0 == t2
       && t1 == t3));

and it worked ! I did not complain anymore about the second assert. Let me create a PR for that.

[cpitclaudel]

I'm not sure this is the right fix: we don't have a similar axiom for sequences, do we?

I think the existing axiom on Map#Equal may be sufficient, if we accept that sometimes you have to write equalities explicitly.

In fact, I worry that this will "hide" an issue: the fact that we're not translating these two syntactically-equal expressions in the same way.

[MikaelMayer]

I have understood from @RustanLeino that It's really by design that assumed expressions have one less layer than assertions, so that the verifier can make more efforts to prove the expression. That's why it's probably not the real issue here. There are axioms that say that having less fuel compute still the same result, so the verifier should be able to pick it up.

Seq actually do have the same problem, thanks for pointing out:

function {:opaque} f(t: int): int { t }
function {:opaque} summarize(input: seq<int>): int { |input| }

lemma lemme(input: seq<int>, i: int, m: map<int, int>) {
    reveal f();
    assert  i == summarize(seq(|input|, k => f(k)));
    assert  i == summarize(seq(|input|, k => f(k)));
}

fails twice. Note that I needed to make summarize opaque, otherwise it would have picked the axiom

axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType ::
  { Seq#Length(Seq#Create(ty, heap, len, init): Seq Box) }
  $IsGoodHeap(heap) && 0 <= len ==>
  Seq#Length(Seq#Create(ty, heap, len, init): Seq Box) == len);

. I'll work on the axiom to add so that the case above works also for sequences

[cpitclaudel]

It's not obvious to me that the difference in fuel is legitimate in the body of lambdas, and it is the source of the discrepancy, here.

I would be careful with adding new extensionality axioms like this. The reason is that such axioms can be costly, and they can fire in unexpected circumstances. We already accept that sequence equality does not come "for free" in Dafny (again, because we only introduce seq#equal when we see an explicit equality between sequences. Here is a concrete example:

const s0: seq<int>
const s1: seq<int>
lemma {:axiom} eq()
  ensures |s0| == |s1|
  ensures forall i | 0 <= i < |s0| :: s0[i] == s1[i]

type T
function f(s: seq<int>): T

method M() {
  eq();
  // assert s0 == s1; // Proof fails without this
  assert f(s0) == f(s1);
}

I'm not saying that we definitely should not add the axiom that I mentioned in the issue (the one you have in this PR), but since there is a workaround we should tread very carefully.

[MikaelMayer]

I get your point about extensionality. We want to be careful to not instantiate too many conjuncts, because it could be a source of instability. Moreover, since my axiom can apply to a single Map#Glue, it will actually instantiate it for every glue.

Yours is an interesting axiom, but one problem is that you cannot pack it in a library, since you are only ensuring equality. Equality should not be defined by axioms.

Another way we could solve this problem is maybe to consider a replacement for the fuel = 2 to assert and fuel = 1 to assume, and axiom like f(fuel := 2, x) == f(fuel := 1, y) which are causing problem when wrapped in non-extensional types like map#glue,
If the goal is to be able to assert with a fuel of 2 just to unroll the function at least twice, but only assume with a fuel of 1 to prevent the verifier from unrolling too much, then we could have the following alternatives:

• Have a way to only provide a fuel of 1 and assert, and if this assertion fail, then we provide a fuel of 2. That might be problematic because it's a disjunction of cases and it might exhaust the resources of the verifier trying to prove the first case.
• In an assert, replace the fuel with an "assertToken" fuel variable which is the same as for the assume.
• If revealed, there is an axiom assertToken == $LS(assertToken2)
• If in the context of an assert, there is one more axiom available assertToken2 == $LS(bottomFuel)
• Otherwise, this axiom is not available.

What do you think of that? That way, an assume followed by an assert of the same thing should make the assert automatically hold since it's the same expression syntactically.
It would not however make it possible to catch f(x) + 1 - 1 like you suggested, we would still need extensionality axioms.
Is there a way we could expose extensionality as a library?

[cpitclaudel]

Yours is an interesting axiom, but one problem is that you cannot pack it in a library, since you are only ensuring equality. Equality should not be defined by axioms.

Which axiom do you mean? I was just assuming a lemma for the convenience of the example.

Is there a way we could expose extensionality as a library?

I don't understand this part. We already have extensionality: if you assert m1 == m2, then we try to prove the equality extensionally.

then we could have the following alternatives:

Before we get into deep discussions about changing the prelude, I'd like to understand why we even bump the fuel to 2 inside lambdas. Is that a good thing?

[RustanLeino]

As I commented on the pull request (#2317), the proposed axiom is unsound. In exploring this, I also detected that Dafny has another existing unsoundness in this area, which I reported as #2375.

I'd like to propose the following tenet:

Twice asserting (or first assuming and then asserting) the syntactically same expression should make the final assertion pass--with one exception, namely when the expression syntactically contains a :| (as described in this paper).

As @MikaelMayer pointed out above, we do change the fuel setting in assert and assume contexts (+1 versus +2). Usually, this still lives up to the tenet. The places where it might not involve some kind of binder. Thus, it could affect matters inside a quantifier (but I don't currently know of any such examples) or inside a translation that uses a Boogie lambda.

One possible solution is thus to change how we assign fuel. Such a change is likely to have a large destabilizing effect on current programs. Moreover, the current +1/+2 assignment of fuel came about because it was needed in important cases. Therefore, I favor exploring a smaller change. In particular, I like what @cpitclaudel suggested above to try to not bump the fuel inside lambdas. I don't know how complicated that is, but I think it would be nice if it could work out.

(It might also be that the problem has less to do with +1/+2 in particular, and more to do with the ...FuelAssertStart... complications. If those features weren't used, I would love to rip them out, because we've had a number of difficult problems with that encoding. But I believe they are used, so we may be stuck with them until we find something better to replace them with.)

[cpitclaudel]

The places where it might not involve some kind of binder. Thus, it could affect matters inside a quantifier (but I don't currently know of any such examples)

predicate P(x: int) {
  if x <= 0 then true else P(x - 1)
}

method M() {
  var y;
  assume y == forall x :: P(x);
  assert y == forall x :: P(x); // assertion might not hold
}

This becomes:

    assume y#0
       == (forall x#1: int :: 
        { _module.__default.P($LS($LZ), x#1) } 
        true ==> _module.__default.P($LS($LZ), x#1));
    assert {:subsumption 0} y#0
       == (forall x#3: int :: 
        { _module.__default.P($LS($LS($LZ)), x#3) } 
        true ==> _module.__default.P($LS($LS($LZ)), x#3));

[MikaelMayer]

Expanding a bit on your example:

predicate P(x: int) {
  if x <= 0 then true else P(x - 1)
}

method M(y: bool)
{
  assume y == forall x :: P(x);
  assert y ==> (forall x :: P(x));  // ok
  assert (forall x :: P(x)) ==> y;  // ok
  assert (forall x :: P(x)) <==> y; // assertion might not hold
  assert y == forall x :: P(x); // assertion might not hold
}

if I move the assumption into a precondition, then everything proves.

I'm surprised by the last one that cannot be proven anyway from the equivalence above.