Null pointer comparison of out-of-bounds pointers is unsound

Problem: Currently, Caesium allows arbitrary out of bounds pointer construction and pointers always compare in-equal to NULL. This is unsound since one can create an out of bounds pointer with address 0 and it would still compare in-equal to NULL.

Proposed solution:

• For each block, keep track of the bounds of the allocation. I.e. make st_used_blocks a gmap from Z to (Z, Z).
• Add heap_loc_in_bounds : loc -> nat -> state -> Prop which means that the range l...l+n is included in the range of the allocation
• Add a heap_loc_in_bounds l 0 st precondition to comparison with NULL
• (Optional) Make heap_loc_in_bounds a precondition of offset operations
• Add a loc_in_bounds : loc -> nat -> iProp ghost state that corresponds to heap_loc_in_bounds, should be persistent
• From l |->{q} v you should get loc_in_bounds l (length v)
• Add a axiom to type that ty_own implies loc_in_bounds l 0

Open problems:

• What about an allocation that ends at the maximal address and where the 1-past-the-end pointer overflows to NULL? Can we just not support this?

Handled in a later step, not here:

• Making allocations return pointers in a finite address range
• Making allocation able to fail