Universal elimination not working for opaque functions

[RustanLeino]

Dafny version

4.0.0

Code to produce this issue

opaque predicate S(x: int) {
  true
}

lemma UniversalElimination(y: int)
  requires forall x :: S(x)
  ensures S(y)
{
}

Command to run and resulting output

> dafny test.dfy

test.dfy(8,0): Error: A postcondition might not hold on this return path.
test.dfy(7,10): Related location: This is the postcondition that might not hold.

Dafny program verifier finished with 0 verified, 1 error

What happened?

The postcondition of lemma UniversalElimination should follow directly from the precondition, independently of S's definition or opacity. But the verifier fails to prove the lemma if S is opaque and not revealed.

The lemma verifies if S is not declared to be opaque.

A workaround for the lack of an automatic proof is to add reveal S(); in the body of the lemma, which proves the lemma.

The problem stems from a lack of connection between the StartFuelAssert and StartFuel constants. I think it maybe possible to get the desired behavior even in the missing case by establishing a connection between S being invoked (in Boogie) with StartFuelAssert and S being invoked with StartFuel. More precisely, the connection between the two constants would be: S(StartFuelAssert, ...) is a synonym for S(StartFuel, ...). Indeed, the following axiom makes the program above verify:

// opaque fuel synonym axiom
axiom (forall x#0: int :: 
  { _module.__default.S(StartFuelAssert__module._default.S, x#0) } 
  _module.__default.S(StartFuelAssert__module._default.S, x#0) == _module.__default.S(StartFuel__module._default.S, x#0));

I don't know if this axiom has any negative impact on performance or provability of other examples.

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

Mac

[MikaelMayer]

I think these axioms would solve countless issues regarding things we can't prove because the fuel for assumption is not the same as the fuel for assertions. I would be all in to do this one.