[Civl] Fix Lheap and add Lmap

[shazqadeer]

This PR has two goals.

First, fix the soundness of nested Lheap accesses. Specifically, Lheap occurrences must be erasable so the only operations allowed are the primitives, reads, and writes. Additionally, all reads and writes must be guarded by the boundary checks. This PR addresses all this systematically disallowing reads anywhere else except assignments (so that instrumenting the boundary checks become relatively easy).

Second, a parallel type to Lheap called Lmap is added. Type checking for Lmap builds on top of the type checking for Lheap.