1. 19 Sep, 2019 1 commit
  2. 13 Sep, 2019 1 commit
    • Jacques-Henri Jourdan's avatar
      Reorder Requires so that we do not depend of Export bugs. · 43a1a90f
      Jacques-Henri Jourdan authored
      The general idea is to first import/export modules which are further
      than the current one, and then import/export modules which are close
      dependencies.
      
      This commit tries to use the same order of imports for every file, and
      describes the convention in ProofGuide.md. There is one exception,
      where we do not follow said convention: in program_logic/weakestpre.v,
      using that order would break printing of texan triples (??).
      43a1a90f
  3. 06 Sep, 2019 1 commit
  4. 16 Jun, 2019 1 commit
    • Robbert Krebbers's avatar
      Replace `C`s with `O`s since we use OFEs instead of COFEs. · 2855d1f5
      Robbert Krebbers authored
      Used the following script:
      
      sed '
      s/\bCofeMor/OfeMor/g;
      s/\-c>/\-d>/g;
      s/\bcFunctor/oFunctor/g;
      s/\bCFunctor/OFunctor/g;
      s/\b\%CF/\%OF/g;
      s/\bconstCF/constOF/g;
      s/\bidCF/idOF/g
      s/\bdiscreteC/discreteO/g;
      s/\bleibnizC/leibnizO/g;
      s/\bunitC/unitO/g;
      s/\bprodC/prodO/g;
      s/\bsumC/sumO/g;
      s/\bboolC/boolO/g;
      s/\bnatC/natO/g;
      s/\bpositiveC/positiveO/g;
      s/\bNC/NO/g;
      s/\bZC/ZO/g;
      s/\boptionC/optionO/g;
      s/\blaterC/laterO/g;
      s/\bofe\_fun/discrete\_fun/g;
      s/\bdiscrete\_funC/discrete\_funO/g;
      s/\bofe\_morC/ofe\_morO/g;
      s/\bsigC/sigO/g;
      s/\buPredC/uPredO/g;
      s/\bcsumC/csumO/g;
      s/\bagreeC/agreeO/g;
      s/\bauthC/authO/g;
      s/\bnamespace_mapC/namespace\_mapO/g;
      s/\bcmra\_ofeC/cmra\_ofeO/g;
      s/\bucmra\_ofeC/ucmra\_ofeO/g;
      s/\bexclC/exclO/g;
      s/\bgmapC/gmapO/g;
      s/\blistC/listO/g;
      s/\bvecC/vecO/g;
      s/\bgsetC/gsetO/g;
      s/\bgset\_disjC/gset\_disjO/g;
      s/\bcoPsetC/coPsetO/g;
      s/\bgmultisetC/gmultisetO/g;
      s/\bufracC/ufracO/g
      s/\bfracC/fracO/g;
      s/\bvalidityC/validityO/g;
      s/\bbi\_ofeC/bi\_ofeO/g;
      s/\bsbi\_ofeC/sbi\_ofeO/g;
      s/\bmonPredC/monPredO/g;
      s/\bstateC/stateO/g;
      s/\bvalC/valO/g;
      s/\bexprC/exprO/g;
      s/\blocC/locO/g;
      ' -i $(find theories -name "*.v")
      2855d1f5
  5. 06 Mar, 2019 1 commit
  6. 05 Mar, 2019 1 commit
  7. 24 Jan, 2019 3 commits
  8. 11 Jan, 2019 1 commit
  9. 31 Oct, 2018 5 commits
    • Robbert Krebbers's avatar
    • Robbert Krebbers's avatar
      Get rid of `irisG'`. · d0f42b2a
      Robbert Krebbers authored
      d0f42b2a
    • Robbert Krebbers's avatar
      98ddbead
    • Robbert Krebbers's avatar
      f7af5b3f
    • Robbert Krebbers's avatar
      Fine-grained post-conditions for forked-off threads. · ebf06f91
      Robbert Krebbers authored
      This commit extends the state interpretation with an additional parameter to
      talk about the number of forked-off threads, and a fixed postcondition for each
      forked-off thread:
      
          state_interp : Λstate → list Λobservation → nat → iProp Σ;
          fork_post : iProp Σ;
      
      This way, instead of having `True` as the post-condition of `Fork`, one can
      have any post-condition, which is then recorded in the state interpretation.
      The point of keeping track of the postconditions of forked-off threads, is that
      we get an (additional) stronger adequacy theorem:
      
          Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
             (∀ `{Hinv : invG Σ} κs,
               (|={⊤}=> ∃
                   (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
                   (fork_post : iProp Σ),
                 let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
                 stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v,
                   let m := length vs in
                   stateI σ2 [] m -∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) →
            rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) →
            φ v.
      
      The difference with the ordinary adequacy theorem is that this one only applies
      once all threads terminated. In this case, one gets back the post-conditions
      `[∗] replicate m fork_post` of all forked-off threads.
      
      In Iron we showed that we can use this mechanism to make sure that all
      resources are disposed of properly in the presence of fork-based concurrency.
      ebf06f91
  10. 18 Oct, 2018 1 commit
  11. 05 Oct, 2018 4 commits
  12. 02 Jul, 2018 1 commit
  13. 20 Jun, 2018 1 commit
  14. 18 Jun, 2018 1 commit
  15. 15 Jun, 2018 2 commits
  16. 14 Jun, 2018 5 commits
  17. 11 Jun, 2018 1 commit
  18. 06 Jun, 2018 2 commits
  19. 18 May, 2018 1 commit
  20. 03 May, 2018 1 commit
  21. 02 May, 2018 2 commits
  22. 26 Apr, 2018 1 commit
  23. 25 Apr, 2018 2 commits