Verification condition generated for an ensures is too different from an equivalent assertion before return

[keyboardDrummer]

predicate P(x: int) { x > 1 }
predicate Q(x: int) requires P(x) { x < 10 }

method Foo() returns (x: int)
  ensures P(x) ==> Q(x) { // <-- first VC to keep in mind
  x := 2;
  return;
}

method Bar() returns (x: int)
  ensures P(x) ==> Q(x) {
  x := 20;
  assert P(x) ==> Q(x); // <-- second VC to keep in mind, should be extremely similar to the first
  return;
}

Boogie for the first VC:

implementation Impl$$_module.__default.Foo-0/assert@5() returns (defass#x#0: bool, x#0: int, $_reverifyPost: bool)
{
  anon0:
    assume $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);
    assume 2 == $FunctionContextHeight;
    assume $_ModifiesFrame#AT#0 == lambda#0(null, $Heap, alloc, false);
    assume {:captureState "temp2.dfy(5,24): initial state"} true;
    assume true;
    assume true;
    assume {:id "id13"} x#0#AT#0 == LitInt(2);
    assume {:captureState "temp2.dfy(6,8)"} true;
    assume true;
    assume _module.__default.P#canCall(x#0#AT#0)
       && (_module.__default.P(x#0#AT#0) ==> _module.__default.Q#canCall(x#0#AT#0));
    assert {:id "id12"} _module.__default.P(x#0#AT#0)
       ==> 
      _module.__default.Q#canCall(x#0#AT#0)
       ==> _module.__default.Q(x#0#AT#0) || x#0#AT#0 < 10;
    return;
}

Boogie for the second VC:

implementation {:smt_option "smt.arith.solver", "2"} {:verboseName "Bar (correctness)"} Impl$$_module.__default.Bar-0/assert@13() returns (defass#x#0: bool, x#0: int, $_reverifyPost: bool)
{

  anon0:
    assume $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);
    assume 2 == $FunctionContextHeight;
    assume $_ModifiesFrame#AT#0 == lambda#0(null, $Heap, alloc, false);
    assume {:captureState "temp2.dfy(11,24): initial state"} true;
    assume true;
    assume true;
    assume {:id "id22"} x#0#AT#0 == LitInt(20);
    assume {:captureState "temp2.dfy(12,9)"} true;
    assume true;
    assume $IsAlloc(x#0#AT#0, TInt, $Heap);
    assume _module.__default.P#canCall(x#0#AT#0);
    goto anon4_Then, anon4_Else;

  anon4_Then:
    assume {:partition} _module.__default.P(x#0#AT#0);
    assume true;
    assume $IsAlloc(x#0#AT#0, TInt, $Heap);
    assume _module.__default.P#canCall(x#0#AT#0);
    assume true;
    assume _module.__default.Q#canCall(x#0#AT#0);
    goto anon2;

  anon4_Else:
    assume {:partition} !_module.__default.P(x#0#AT#0);
    goto anon2;

  anon2:
    assume _module.__default.P#canCall(x#0#AT#0)
       && (_module.__default.P(x#0#AT#0) ==> _module.__default.Q#canCall(x#0#AT#0));
    assert {:id "id26"} {:subsumption 0} _module.__default.P(x#0#AT#0)
       ==> 
      _module.__default.Q#canCall(x#0#AT#0)
       ==> _module.__default.Q(x#0#AT#0) || x#0#AT#0 < 10;
    return;
}

[keyboardDrummer]

The assertion in the body gets translated differently because assertion the precondition and the expression itself is done in the same implementation, while for the ensures clause this is separated between the WF check Boogie implementation and the correctness check Boogie implementation.

The WF check produces a Boogie if cmd, and the control flow from that command remains when isolating the assertion.

A fix would be to check for the precondition in a check and forget block, and then we could assume the precondition after that block.

Or even better would be not to generate control flow blocks when translating expressions, since then the Boogie code looks more like the Dafny code. It's not clear to me why we're doing that now.

[keyboardDrummer]

My preference would be for the Boogie to look like this in both cases:

implementation Impl$$_module.__default.Foo-0/assert@5() returns (defass#x#0: bool, x#0: int, $_reverifyPost: bool)
{
  anon0:
    assume $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);
    assume 2 == $FunctionContextHeight;
    assume $_ModifiesFrame#AT#0 == lambda#0(null, $Heap, alloc, false);
    assume {:id "id13"} x#0#AT#0 == LitInt(2);
    assume _module.__default.P#canCall(x#0#AT#0)
       && (_module.__default.P(x#0#AT#0) ==> _module.__default.Q#canCall(x#0#AT#0));
    assert {:id "id12"} _module.__default.P(x#0#AT#0)
       ==> 
      _module.__default.Q#canCall(x#0#AT#0)
       ==> _module.__default.Q(x#0#AT#0) || x#0#AT#0 < 10;
    return;
}