1. 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 Φ?
  2. 28 Jun, 2021 1 commit
  3. 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
  4. 26 Jun, 2021 1 commit
  5. 22 Jun, 2021 2 commits
  6. 21 Jun, 2021 6 commits
  7. 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
  8. 31 May, 2021 4 commits
  9. 21 May, 2021 2 commits
  10. 15 Apr, 2021 1 commit
  11. 15 Mar, 2021 3 commits
  12. 12 Mar, 2021 3 commits
    • Edoardo Putti's avatar
      add the trivial hoare triple rules · d1ce44c2
      Edoardo Putti authored
    • Edoardo Putti's avatar
      refactor proof rules and use them to prove examples · 27638c50
      Edoardo Putti authored
      the proof rules definitions were ok but to actually use
      them effectively and have the eauto or eapply instance the correct
      parts for us we have to refactor them so that we can specify the
      interesting parts of our goals ourself and have eauto pick up for us
      As an example in the context proof rule reordering from
      Lemma hoare_ctxS E P P' e Q v
      Lemma hoare_ctxS E P' P e Q v
      makes it possible for us to specify both the context we want
      to use and the intermediate heap P' while having eauto fill out
      P e Q v for us
    • Edoardo Putti's avatar
      prove alloc rule · c99f9661
      Edoardo Putti authored
  13. 08 Mar, 2021 4 commits