GitLab

this rule works for when we allocate a previously deallocated cell
instead of a fresh one

post_alloc has two variants, this it the one for unallocated cells

our current heap definition is a partial map that does not preserve
freed cells. This is gonna be problematic later on when we want to
prove the heap manipulation proof rules.

This changes the underlying value in the map from a value to a
disjoint union of a value or a Reserved cell.

Reserved is a value that only the EFree expression can put in the
heap and it is used to distinguish cells that were previously allocated
and freed from cells that were never allocated.

The head_step rule for EAlloc then changes to allow not only
allocating unused cells but the Reserved too. The head_step rule
for EFree, EStore, ELoad instead change the lookup value to be
Some (Value w) because we have to restric us from loading previously
deallocated cells.

The Alloc_head_step rule could be split into two, one for each result of
lookup that we allow, None and Some (Reserved) but this can be
unified using another predicate.

m !! l = Some e -> e = Reserved gives us both the allowed cases;
if location l has value e then it is a Reserve, meaning that it
was previously freed.

obviously we are missing the NULL rule for all the
heap primiitives but it should not be a problem

all the language forms needed an update now that we want to use
post instead of wp/ewp

the key lemmas that we need to prove the ISL paper rules
are about monotonicity, disjunctions and the frame rule

Robbert suggested unifying wp and ewp by having a match on the final
value. This helps with the amount of lemmas that I had to prove as
now there is only one predicate and also evaluating in context holes
has been taken care of.

This predicate also relies on frame baking as the previous two and we
might rework this when we hit some more problems.

both our weakest precondition definitions are about reachability
from a set of initial heaps, therefore there is monotonicity in
the initial heaps as set

this part is important because we have changed the rules of inference to
a weakest precondition style and we have to show that they are as
powerful as the original one; the straightforward way to do this is
to prove the originals using ours.

rename wp_alloc

also fixes the examples to make sure we can still prove them
with this new definition

When working with is_error we will have to prove something
cannot step and when this is because of a resource usage
this lemmas should prove sufficient to move the proof to the
resources

Because we want to use step instead of head_step in our error
predicate we need some lemmas to shift the proof from the expression
to the resources

how does malloc work in the original ISL paper?
are all pointers _fresh_ or are they allowed to alias another location?