Commit d304a819 authored by Léon Gondelman's avatar Léon Gondelman

This commit fixes the case of computation of `vcg_wp` for the sequence.

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'.
parent d5f93711
......@@ -15,7 +15,7 @@ theories/vcgen/denv.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
theories/vcgen/test.v
# theories/vcgen/test.v
theories/vcgen/tests/swap.v
# theories/heap_lang_vcgen/dval.v
# theories/heap_lang_vcgen/vcgen.v
# theories/heap_lang_vcgen/test.v
......
......@@ -64,6 +64,17 @@ Section denv.
end
end.
Fixpoint denv_replace_full (i : nat) (dv: dval) (m: denv) : option denv :=
match m with
| [] => None
| dio :: m' =>
match i with
| O => '' _ dio; Some (Some (DenvItem LLvl 1%Qp dv) :: m')
| S i => m' denv_replace_full i dv m'; Some (dio :: m')
end
end.
Fixpoint denv_delete_frac (i : nat) (m : denv) : option (denv * frac * dval) :=
match m with
......@@ -140,6 +151,15 @@ Section denv_spec.
((denv_interp E m1 denv_interp E m2))%I (denv_interp E (denv_merge m1 m2))%I.
Proof. Admitted.
Lemma denv_replace_interp E m i dv m':
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').
Proof. Admitted.
Lemma denv_delete_frac_interp E i m m' q dv :
Some (m', q, dv) = denv_delete_frac i m
denv_interp E m' dloc_interp E (dLoc i) (ULvl, q) dval_interp E dv denv_interp E m.
......
......@@ -31,10 +31,10 @@ Section Tests_vcg.
awp (a_store (a_ret #s) (a_load (a_ret #l))) R (λ _, s L #1 l U #1).
Proof.
iIntros "Hs Hl".
vcg_solver. eauto with iFrame.
vcg_solver. rewrite Qp_half_half. eauto with iFrame.
Qed.
(*
Lemma store_load_load (s1 s2 l : loc) R :
s1 U #0 - l U #1 - s2 U #0 -
awp ((a_store (a_ret #s1) (a_load (a_ret #l))) ;;;;
......@@ -43,49 +43,10 @@ Section Tests_vcg.
Proof.
iIntros "Hs1 Hl Hs2".
iApply (a_sequence_spec). vcg_solver.
iIntros "Hs2 Hl Hs1". iModIntro. awp_lam. vcg_solver.
vcg_solver. eauto with iFrame.
(* vcg_solver. *)
eapply tac_vcg_sound;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| compute; reflexivity (* E = penv_to_known_locs Γls *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *) |].
compute[vcg_wp vcg_sp].
rewrite -wp_interp_sane_sound. simpl.
compute[denv_interp]. simpl.
iIntros "(? & ? & ? & ?)".
iExists _; iSplit; eauto.
iFrame.
iIntros "Hs2 Hl Hs1".
iExists _; iSplit; eauto.
iExists _; iFrame "Hl". iIntros "Hl".
iExists _; iFrame "Hs1". iIntros "Hs1".
iModIntro. iFrame "Hs2 Hl".
vcg_solver. eauto with iFrame.
iIntros "Hs2 Hl Hs1". iModIntro. awp_lam. vcg_solver. rewrite Qp_half_half.
eauto with iFrame.
Qed.
*)
(*
Lemma swap_spec (l1 l2 r : loc) (v1 v2: nat) R :
r ↦U #32 -∗ l1 ↦U #41 ∗ l2 ↦U #42 -∗
awp (swap #l1 #l2 #r) R (λ _, l2 ↦U #41 ∗ l1 ↦U #42).
Proof.
iIntros "Hr [Hl1 Hl2]". do 3 awp_lam.
vcg_solver.
eapply tac_vcg_sound;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| compute; reflexivity (* E = penv_to_known_locs Γls *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *) |]. compute[vcg_wp vcg_sp].
compute[denv_interp big_opL]. simpl. iExists #41.
iDestruct "H" as "[Hm Hde1]"
*)
Lemma test3 (l : loc) :
l U #1 -
awp (a_bin_op PlusOp (a_store (a_ret #l) (a_ret #2))
......@@ -100,5 +61,4 @@ iDestruct "H" as "[Hm Hde1]"
Proof. iIntros "Hl". vcg_solver. Abort.
End Tests_vcg.
\ No newline at end of file
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Ltac vcg_solver :=
eapply tac_vcg_sound;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| compute; reflexivity (* E = penv_to_known_locs Γls *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
| rewrite -wp_interp_sane_sound ].
Ltac vcg_opt_solver :=
eapply tac_vcg_opt_sound;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| compute; reflexivity (* E = penv_to_known_locs Γls *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
| ].
Section Tests_vcg.
Context `{amonadG Σ}.
Notation "l ↦( x , q ) v" :=
(mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l ↦( x , q ) v").
Definition swap : val := λ: "l1" "l2" "r",
(a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
(a_store (a_ret "l1") (a_load (a_ret "l2"))) ;;;;
((a_store (a_ret "l2") (a_load (a_ret "r"))));;;;
(a_ret #0).
Lemma swap_spec_by_vcg_opt (l1 l2 r : loc) (v1 v2: nat) R :
r U #0 - l1 U #1 l2 U #2 -
awp (swap #l1 #l2 #r) R (λ _, l2 U #1 l1 U #2).
Proof.
iIntros "Hr [Hl1 Hl2]". do 3 awp_lam.
vcg_opt_solver. simpl. eauto with iFrame.
Qed.
Lemma swap_spec_by_vcg (l1 l2 r : loc) (v1 v2: nat) R :
r U #0 - l1 U #1 l2 U #2 -
awp (swap #l1 #l2 #r) R (λ _, l2 U #1 l1 U #2).
Proof.
iIntros "Hr [Hl1 Hl2]". do 3 awp_lam.
vcg_solver. compute[denv_interp]. simpl.
iIntros "(Hl2 & Hl1 & Hr & _)". iFrame.
iIntros "Hl2 Hl1 Hr".
iExists l1; iSplit; first done. iExists 1%Qp, #1. iFrame "Hl1". iIntros "Hl1".
iExists #0. iFrame "Hr". iIntros "Hr". iModIntro. iFrame.
iIntros "Hl2 Hl1 Hr". iExists (dLoc 0); iSplit; first done. simpl. iExists 1%Qp, (dLitV (dLitInt 2)).
iFrame "Hl2". simpl. iIntros "Hl2". iExists (dLitV (dLitInt 1)). iFrame "Hl1". iIntros "Hl1".
iModIntro. iFrame.
iIntros "Hl2 Hl1 Hr". iExists (dLoc 2); iSplit; first done. simpl. iExists 1%Qp, (dLitV (dLitInt 1)).
iFrame "Hr". iIntros "Hr". iExists (dLitV (dLitInt 2)). simpl. iFrame "Hl2". iIntros "Hl2".
iModIntro. iFrame.
Qed.
End Tests_vcg.
\ No newline at end of file
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment