1. 26 May, 2019 1 commit
  2. 20 May, 2019 1 commit
  3. 03 Feb, 2019 1 commit
  4. 29 Nov, 2018 1 commit
  5. 26 Nov, 2018 1 commit
  6. 16 Nov, 2018 1 commit
  7. 15 Nov, 2018 1 commit
  8. 14 Nov, 2018 1 commit
  9. 11 Nov, 2018 2 commits
  10. 01 Nov, 2018 1 commit
  11. 17 Oct, 2018 2 commits
  12. 12 Oct, 2018 1 commit
  13. 09 Oct, 2018 1 commit
  14. 02 Jul, 2018 1 commit
  15. 01 Jul, 2018 1 commit
  16. 28 Jun, 2018 2 commits
  17. 26 Jun, 2018 3 commits
  18. 25 Jun, 2018 1 commit
  19. 20 Jun, 2018 1 commit
  20. 18 Jun, 2018 2 commits
    • Robbert Krebbers's avatar
      Bump Iris and many random changes. · 15062624
      Robbert Krebbers authored
      - Consistent notation for ↦ of the C language: `x ↦C[lv]{q] v`, which is
        not redefined in every file.
      - Many useless stylistic changes.
      15062624
    • Léon Gondelman's avatar
      This commit fixes the case of computation of `vcg_wp` for the sequence. · d304a819
      Léon Gondelman authored
      Now all the small tests work, and the `swap` example passes as well.
      
      The main idea for fixing `vcg_wp` for sequence,
      is to change the continuation `(Φ : dval → wp_expr)` of `vcg_wp`
      so that it takes `denv` as additional parameter.
      
      Then, in `vcg_wp` all cases, except for the **sequence** and **store** are simply passing the continuation.
      
      The `vcg_wp` for the sequence becomes :
      
      ```Coq
      | dCSeq de1 de2 => vcg_wp E m de1 R (λ m' _, UMod (vcg_wp E (denv_unlock m') de2 R Φ))
      ```
      
      The case for  **store** is more subtle.  The critical part is the case
      where `vcg_sp E m de1 = Some (mIn, mOut, dv1)` and `dv1 = dLitV (dLitLoc (dLoc i))`,
      where the continuation will make use of the function  `denv_replace_full i dv2 m'` whose specification is
      
      ```Coq
       Some m' = (denv_replace_full i dv m) →
             ∃ x q dv0 m0,
              (denv_interp E m0 ∗ dloc_interp E (dLoc i) ↦(x   ,  q  ) dval_interp E dv0 ⊣⊢ denv_interp E m) ∧
              (denv_interp E m0 ∗ dloc_interp E (dLoc i) ↦(LLvl, 1%Qp) dval_interp E dv  ⊣⊢ denv_interp E m').
      ```
      
      In that case, we do not need to generate `IsLoc dv1 ...`, inlining instead the precise form of
      `dv1` in the resulting formula, using `denv_replace_full` in the end:
      
      ```Coq
      | dCStore de1 de2 =>
            match vcg_sp E m de1 with
            | Some (mIn, mOut, dv1) =>
              match dv1 with
              | dLitV (dLitLoc (dLoc i)) =>
                mapsto_star_list m
                  (mapsto_wand_list mIn
                     (vcg_wp E mIn de2 R (λ m' dv2,
                        mapsto_wand_list mOut
                          (MapstoStarFull (dLoc i) (λ _, (MapstoWand (dLoc i) dv2 LLvl 1%Qp
                               (match (denv_replace_full i dv2 m') with
                                | Some mf => (Φ mf dv2)
                                | None => Base False (*TODO: maybe this is too strong, return just (Φ m' dv2) *)
                                end)))))))
      ```
      
      Note the comment for the case where `denv_replace_full i dv2 =  None`.
      Note also, that for the other cases, including `match vcg_sp E m de2 = Some (mIn, mOut, dv1)`,
      the continuation is passed as such, without replacing its content.
      For the latter case ( `match vcg_sp E m de2 = Some (mIn, mOut, dv1)`) we probably also need to
      update the continuation as described above.
      
      Finally, the correctness statement for the `vcg_wp` becomes :
      
      ```Coq
      Lemma vcg_wp_correct R E m de Φ :
          wp_interp E (vcg_wp E m de R Φ) ⊢
              awp (dcexpr_interp E de) R
            (λ v, ∃ dv m', ⌜dval_interp E dv = v⌝ ∧ wp_interp E (Φ m' dv)).
       ```
      
      This statement is proven for all cases. Somehow surprisingly, the specification
      for `denv_replace_full` was not needed. The reason for that is probably that the correctness
      statement only affirms the bare existence of 'm'.
      d304a819
  21. 14 Jun, 2018 1 commit
  22. 13 Jun, 2018 1 commit
  23. 12 Jun, 2018 1 commit
  24. 08 Jun, 2018 1 commit
  25. 07 Jun, 2018 2 commits
  26. 06 Jun, 2018 1 commit
  27. 04 Jun, 2018 1 commit
  28. 31 May, 2018 1 commit
  29. 18 May, 2018 1 commit
  30. 15 May, 2018 1 commit
    • Léon Gondelman's avatar
      Just a sketch of a very naive vcgen for heap-lang, · c36dda2a
      Léon Gondelman authored
      without any optimisation.
      
      Next steps:
       modify definition of wp_expr, with a deep embedding of
        - functions : to allow optimisation go recursively through lambdas,
          in particular, to allow exhale-inhale optimisation;
        - conjunction and equations : to allow optimisation
          of redundant and trivial equations
      c36dda2a
  31. 14 May, 2018 1 commit
  32. 07 May, 2018 1 commit
  33. 04 May, 2018 1 commit