1. 24 Feb, 2021 6 commits
    • Edoardo Putti's avatar
      add proof rule for free · cbc063a7
      Edoardo Putti authored
      cbc063a7
    • Edoardo Putti's avatar
      finish post_alloc' rule · 2e3ddfd6
      Edoardo Putti authored
      this rule works for when we allocate a previously deallocated cell
      instead of a fresh one
      2e3ddfd6
    • Edoardo Putti's avatar
      finish post_alloc rule · 033023e9
      Edoardo Putti authored
      033023e9
    • Edoardo Putti's avatar
      draft for post_alloc · 81194922
      Edoardo Putti authored
      post_alloc has two variants, this it the one for unallocated cells
      81194922
    • Edoardo Putti's avatar
    • Edoardo Putti's avatar
      update heap definition · 631adb0a
      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.
      631adb0a
  2. 19 Feb, 2021 8 commits
  3. 17 Feb, 2021 2 commits
    • Edoardo Putti's avatar
      unify wp and ewp · 7456cd92
      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.
      7456cd92
    • Edoardo Putti's avatar
      add step rule for EErrror expression · 05d7d103
      Edoardo Putti authored
      05d7d103
  4. 15 Feb, 2021 2 commits
  5. 13 Feb, 2021 1 commit
  6. 12 Feb, 2021 4 commits
  7. 10 Feb, 2021 2 commits
  8. 09 Feb, 2021 1 commit
  9. 08 Feb, 2021 5 commits
  10. 04 Feb, 2021 3 commits
  11. 03 Feb, 2021 1 commit
    • Edoardo Putti's avatar
      update step prerequisites · 43dbcc77
      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
      43dbcc77
  12. 01 Feb, 2021 5 commits