Use local variables for the old state

[gauravpartha]

Before this PR, Carbon used Boogie's old state to model Viper's old state. As a result, Carbon deals with the old state differently compared to other states such as labelled old states. In particular, state components (i.e., the heap and permission modules) must explicitly wrap the currently tracked Boogie variable corresponding to the component with old, which is reflected as a special case in the code.

Moreover, the previous encoding is indirect because Boogie's old state conceptually does not capture Viper's state. The following encoding snippet previously used at the beginning of a method encoding illustrates this:

procedure p(...) {
  Mask := ZeroMask;
  assume state(Heap, Mask);
  [encoding of `inhale precondition` in `(Heap, Mask)`]
  
  assume Heap == old(Heap);
  assume Mask == old(Mask);
  
  [encoding of method body]
  ...
}

Viper's old state is the state after inhaling the precondition, while Boogie's old state is the state of the global variables right at the beginning of the Boogie procedure. The two assume statements after inhaling the precondition make sure that the two states are in-sync. The encoding is sound because the Boogie code before the assume statements does not use Boogie's old state at all. Thus, for any relevant Boogie trace, there is a corresponding one where old(Heap) and old(Mask) match the values of Heap and Mask right after inhaling the precondition.

This pull request addresses both of these problems by introducing local Boogie variables that model the old state. The new encoding corresponding to the one shown above is:

var oldHeap: HeapType;
var oldMask: MaskType;
Mask := ZeroMask;
assume state(Heap, Mask);
[encoding of `inhale precondition` in `(Heap, Mask)`]

oldHeap := Heap;
oldMask := Mask;

[encoding of method body]

This encoding is more direct. Moreover, this way of modeling the old state is the same as the approach that Carbon takes for other states (e.g., labelled old expressions). As a result, Carbon's state components (i.e., the heap and permission module) do not need to wrap their tracked variables with old.

Another positive consequence is that the Boogie old state does not show up in unexpected places. For example, when inhaling the postcondition acc(x.f) && x.f == old(x.f)+1 as part of a method call, the second conjunct was previously translated to:

assume Heap[x,f] == old(PreCallHeap)[x,f]+1

Here, PreCallHeap has the value of the heap right before the call, which thus symbolizes the old heap during the method call. The usage of the Boogie old wrapper is redundant here since PreCallHeap is a local variable. The reason Carbon uses the old wrapper here is because whenever the body of an old expression is evaluated, the state is marked as being an old state, which then leads to the Carbon state components using using the old wrapper. In the new encoding, the state components do not use the old wrapper anymore (but the state is still marked as an old state in the Carbon implementation itself).