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
      355ceff7
    • Edoardo Putti's avatar
      add a section for the double free examples · ebdaed1e
      Edoardo Putti authored
      ebdaed1e
    • Edoardo Putti's avatar
      73c97d50
    • 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
      8f39a784
    • 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.
      6810c92c
    • 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 Φ?
      18a31ecb
  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
      7105730f
    • Edoardo Putti's avatar
      add post_bind · 80e7da05
      Edoardo Putti authored
      80e7da05
    • 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
      assertion.
      
      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.
      6fc357be
    • 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
      6c400a19
  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.
      9735757c
    • 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.
      2b457482
    • Edoardo Putti's avatar
      draft for CoqProject file · 4ee79380
      Edoardo Putti authored
      4ee79380
  9. 31 May, 2021 4 commits
  10. 21 May, 2021 2 commits
  11. 15 Apr, 2021 1 commit
  12. 15 Mar, 2021 3 commits