1. 26 Jul, 2021 7 commits
  2. 21 Jul, 2021 6 commits
    • Edoardo Putti's avatar
      update hoare_let · 355ceff7
      Edoardo Putti authored
      as done before for the context rule here I need to move the
      intermediate value v to the start of the arguments because it
      is not automatically picked up by eapply
    • Edoardo Putti's avatar
      add a section for the double free examples · ebdaed1e
      Edoardo Putti authored
    • Edoardo Putti's avatar
    • Edoardo Putti's avatar
      allow for specifying the intermediate value · 8f39a784
      Edoardo Putti authored
      kind of silly for me to find it now but the intermediate value
      is something I might want to specify without giving out all
      the other values
    • Edoardo Putti's avatar
      prove context rule for error triples in Iris style · 6810c92c
      Edoardo Putti authored
      The new rules are a generalisation of the normal hoare
      context rule and to prove it we show how to recover
      the first context rule from the general.
      Both rules admit the existence of values v in the lemma
      premises but they describe it differently.
      If in the first triple the value was explicit when using
      ⌜ r = v ⌝ or ⌜ Φ v ⌝ in the triple result for the general
      rule we don't need to be explicity immediately.
      There is a problem though as now the result assertion for
      is Q : val → val → iProp instead of being Q :  val → iProp
      and this might confuse people. Where do we get the new v
      in the current triple if it does not have it?
      You can always introduce a dummy ⌜ Φ v ⌝ in the result assertion
      or just ignore v by wrapping in another lamba the original term
      λ _ : Q.
    • Edoardo Putti's avatar
      rename hoare_pure to hoare_intro · 18a31ecb
      Edoardo Putti authored
      this rule mimicks the iIntro rule from Iris. Pure assertions in the
      precondition of a correctness triple can be pulled in the proof
      context and used when unfolding a program execution but in our logic
      it's not the pure assertions in the presumption but the pure assertion
      in the result that can be pulled.
      This also is a path I've been thinking on recently; an incorrectness
      triple {{ ⌜ Φ ⌝ ∗ P }} e {{ Q }} cannot give you the Φ?
  3. 28 Jun, 2021 1 commit
  4. 27 Jun, 2021 4 commits
    • Edoardo Putti's avatar
      add bind section to examples · 7105730f
      Edoardo Putti authored
    • Edoardo Putti's avatar
      add post_bind · 80e7da05
      Edoardo Putti authored
    • Edoardo Putti's avatar
      add a hoare context triple that mimics the SL one · 6fc357be
      Edoardo Putti authored
      In separation logic the hoare triple for the context is as follows
      {{ P }} e {{ x, R x }}  forall v, {{ R v }} K[v] {{ x, Q x}}
      	{{ P }} e {{ x, Q x}}
      But this rule makes use of the fact that {{ False }} e {{x, Q x}}
      is always valid.
      In IL this is not true, the trivial triple is  [ P ] e [x, False ]
      which gave me the idea of moving the value v to the result assertion.
      This is actually in line with the previous IL triples that I saw where
      the distinction on the good/bad values are put in the result
      Say K ≝ let x =  in if x ≥ 1 then x else error. Then the traditional
      incorrectness triples are written as.
      [v ∈ N] K[v] [r, v ≥ 1]
      [v ∈ N] K[v] [ERR: v = 0]
      So the current hoare_ctxS_iris_forall' rule encodes this pattern
      as we can always split the bad values from the good value in the
      result assertion.
    • Edoardo Putti's avatar
      update last incorrectness triples signatures · 6c400a19
      Edoardo Putti authored
      again these signatures are easier to use when
      it comes to eapply
  5. 26 Jun, 2021 1 commit
  6. 22 Jun, 2021 2 commits
  7. 21 Jun, 2021 6 commits
  8. 08 Jun, 2021 3 commits
    • Edoardo Putti's avatar
      update seq rule with a more general statement · 9735757c
      Edoardo Putti authored
      the original statement included a part about the intermediate
      result of our computation even though we only throw it away.
      This lemma is stronger because we can prove the previous one and
      works better syntactically.
    • Edoardo Putti's avatar
      add a primitive rule for the wand · 2b457482
      Edoardo Putti authored
      the interesting part of this is that in the theory behind Iris
      the frame rule is recovered through the wand rule and monotonicity.
      As I followed the same path this is quite nice to have, at least
      to confirm that everything is working as I am expecting.
    • Edoardo Putti's avatar
      draft for CoqProject file · 4ee79380
      Edoardo Putti authored
  9. 31 May, 2021 4 commits
  10. 21 May, 2021 2 commits
  11. 15 Apr, 2021 1 commit
  12. 15 Mar, 2021 3 commits