Use CanCall everywhere

[RustanLeino]

Description

This PR changes the axiomatization of functions to uniformly rely on "CanCall certificates". Not only does this simplify the logical encoding, but it also enables further improvements to the encoding of functions, which will appear in separate PRs.

The essence of CanCall

Consider a function

function F(x: nat): int
  requires x < 100
{
  2 * x
}

The fact that this function yields a value that's twice its argument is captured by the function's definition axiom. To a first order of approximation, the definition axiom is

axiom (forall x: int ::
  0 <= x && x < 100
  ==>
  F(x) == 2 * x);

Prior to each use of the function, the verifier generates a proof obligation that checks the arguments to have the appropriate types and the preconditions to be met. For example, an assignment z := F(y); is (to a first order of approximation) translated into Boogie as

assert 0 <= y && y < 100;
z := F(y);

To reason about the value assigned to z, the verifier uses the definition axiom. To obtain the fact z == 2 * y, the verifier first needs to discharge the axiom's antecedent. This may seem redundant, since the assertion before the use of F makes sure that the antecedent holds, but it required for soundness (as demonstrated by replacing the body of F by if x == 157 then 1 + F(x) else 2 * x). The cost of this redundancy is often neglible, but if the function's precondition uses disjunctions and quantifiers, then there is extra effort involved in discharging the antecedent, even after proving the assertion.

To remove the cost of the redundancy and to clean up what is generated, this PR makes use of a so-called CanCall function, which acts as a "certificate" that says "the function's precondition has been validated for the arguments ...". This changes the definition axiom to

axiom (forall x: int ::
  F#CanCall(x)
  ==>
  F(x) == 2 * x);

and changes the translation of the assignment above to

assert 0 <= y && y < 100;
assume F#CanCall(y);
z := F(y);

(CanCall antecedents are used not only in definition axioms, but also in other axioms generated from a function: consequence axioms, override axioms.)

CanCall's before this PR

Dafny introduced CanCalls a long time ago (perhaps 10 years ago?). However, previously, CanCalls were only a possible shortcut to discharging the antecedent. Specifically, the definition axiom had (to a first order of approximation) the form

axiom (forall x: int ::
  F#CanCall(x) || (0 <= x && x < 100)
  ==>
  F(x) == 2 * x);

While this gives the verifier the opportunity to use the CanCall, it still pollutes the axiom with the function's type constraints and precondition.

In fact, the axiom was even slightly more complicated, namely

axiom
  K <= $FunctionContextHeight
  ==>
  (forall x: int ::
    F#CanCall(x) || (K < $FunctionContextHeight && 0 <= x && x < 100)
    ==>
    F(x) == 2 * x);

for some numeric constant K determined from the given program. The antecedent K <= $FunctionContextHeight remains even after this PR, but it will soon be removed in a separate PR.

To rely solely on CanCall, the verifier needed to be changed to emit the CanCall assumptions everywhere. The work to emit these CanCall assumptions everywhere was started by @typerSniper in 2021. We picked this up again in the last year and have now completed the task.

Other changes

The PR also contains some other improvements and bug fixes:

• Fix bug where an enumeration of disjuncts had erroneously enumerated nested conjuncts.
• Pass in a neutral heap argument ($OneHeap) in places where the heap argument is not used (for example, in a seq constructor that's given a total function).
• Show as tooltips any let-bindings created by trigger generation.
• Improve proofs in the standard libraries.
• Improve some tests (better formatting, less nondeterminism, etc.).

Co-authored-by: Jatin Arora [email protected]

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[typerSniper]

looks good to go! there were a couple of minor things that I fixed and committed.