 24 Feb, 2021 6 commits


Edoardo Putti authored

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

Edoardo Putti authored

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

Edoardo Putti authored

Edoardo Putti authored
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.

 19 Feb, 2021 8 commits


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

Edoardo Putti authored

Edoardo Putti authored

Edoardo Putti authored

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

Edoardo Putti authored

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

Edoardo Putti authored

 17 Feb, 2021 2 commits


Edoardo Putti authored
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.

Edoardo Putti authored

 15 Feb, 2021 2 commits


julesjacobs authored

julesjacobs authored

 13 Feb, 2021 1 commit


Edoardo Putti authored

 12 Feb, 2021 4 commits


Edoardo Putti authored

Edoardo Putti authored

Edoardo Putti authored

Edoardo Putti authored

 10 Feb, 2021 2 commits


Edoardo Putti authored

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

 09 Feb, 2021 1 commit


Edoardo Putti authored

 08 Feb, 2021 5 commits


julesjacobs authored

julesjacobs authored

julesjacobs authored

Edoardo Putti authored
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.

Edoardo Putti authored
rename wp_alloc

 04 Feb, 2021 3 commits


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

Edoardo Putti authored

Edoardo Putti authored
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

 03 Feb, 2021 1 commit


Edoardo Putti authored
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

 01 Feb, 2021 5 commits


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

Edoardo Putti authored

julesjacobs authored

julesjacobs authored

julesjacobs authored
