[Civl] Combine linear heaps and maps into a single abstraction

[shazqadeer]

This PR unifies Lmap and Lheap into a single abstraction with the latter being defined in terms of the former.

type Lheap T = Lmap (Ref T) T

The type Ref T is explained below.

The implementation of Lmap primitives is done by modeling them directly as pure procedures in Boogie syntax. Thus a lot of rewriting code in LinearRewriter.cs is eliminated. However, inlining of atomic actions had to be adjusted to allow for calling and inlining pure procedures from atomic actions. It is possible that these changes can be reverted by modeling these primitives as pure actions (which are already callable from both yield procedures and actions).

An important innovation is separating the Lmap primitives from the dynamic allocation of keys for which two separate types are provided.

type Loc _;
datatype Ref<V> {
  Ref(loc: Loc V),
  Nil()
}

The type Loc models a dynamically-allocated location. The allocation itself is performed by the Loc_New primitive:

pure procedure {:inline 1} Loc_New<V>() returns (k: Lval (Loc V)) { }

The caller gets a fresh location (notice the Lval wrapper) every time Loc_New is called. An instance of Loc T may be wrapped into an instance of Ref T via the Ref constructor.

Two separate types Loc and Ref are needed because we want the domains of different Lheap T values to be disjoint. At the same time, we want to provide the capability to have unique references to locations. If we unified Loc and Ref, then we cannot have both capabilities.

This PR appears to be a step in the right direction due to the unification of Lmap and Lheap. However, there is still room for improvement. To avoid the need to write collector functions, we introduced types Lval, Lset, and Lheap that have built-in collector functions. But we have introduced drawbacks.

1. We lost the ability to have both ordinary and linear variables of these types, a flexibility that was always present in Civl. The rules for passing and copying linear values are draconian and sometimes it is convenient to be able to treat a linear value as an ordinary value for the purpose of specification and verification, e.g., using them in a pure procedure written as a lemma.
2. We introduced wrappers Lmap around an ordinary Map and a wrapper Lset around an ordinary Set. These wrappers cause an extra level of indirection when writing code to read/modify these values.

My current assessment is that the wrapper Lval for wrapping a value to convert it into a possibly linear value is fundamental because it influences the definition of the collector function for the value. But the wrappers Lmap and Lset can be eliminated by going back to the original Civl approach.

[shazqadeer]

@bkragl : I added you as a reviewer just so you get a notification. You could read through the PR summary and look at the changes in base.bpl if you are curious. But there is no need to review the C# code changes at the moment.