Commit 1ee95d7b authored by Dan Frumin's avatar Dan Frumin

strong spec (with ▷) for cwp_seq_bind

parent 5e98b3d6
......@@ -407,7 +407,7 @@ Section proofs.
(* Internal spec: breaks the abstraction/notation *)
Lemma cwp_seq_bind' R Φ e (f: val) :
CWP e @ R {{ v, U (CWP f v @ R {{ Φ }}) }} -
CWP e @ R {{ v, U (CWP f v @ R {{ Φ }}) }} -
CWP c_seq_bind e f @ R {{ Φ }}.
Proof.
iIntros "H".
......@@ -418,11 +418,11 @@ Section proofs.
Qed.
Lemma cwp_seq_bind R Φ x e1 e2 :
CWP e1 @ R {{ v, U (CWP subst' x v e2 @ R {{ Φ }}) }} -
CWP e1 @ R {{ v, U (CWP subst' x v e2 @ R {{ Φ }}) }} -
CWP x ←ᶜ e1 ; e2 @ R {{ Φ }}.
Proof.
iIntros "H". cwp_pures. iApply cwp_seq_bind'.
iApply (cwp_wand with "H"); iIntros (v) "H !>". by cwp_lam.
iApply (cwp_wand with "H"); iIntros (v) "H !> !>". by cwp_lam.
Qed.
(* Internal spec: breaks the abstraction/notation *)
......@@ -434,7 +434,7 @@ Section proofs.
Proof.
iIntros "H".
cwp_apply (cwp_wp with "H"); iIntros (ev) "H". cwp_lam. cwp_pures.
iApply cwp_seq_bind'; iApply (cwp_wand with "H"); iIntros (v) "H !>".
iApply cwp_seq_bind'; iApply (cwp_wand with "H"); iIntros (v) "H !> !>".
cwp_pures. iApply cwp_bind.
cwp_apply cwp_atomic_env; iIntros (env) "Henv $". iApply wp_fupd.
iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]". wp_pures.
......@@ -480,7 +480,7 @@ Section proofs.
iIntros "H". rewrite /c_if -lock. cwp_pures.
cwp_apply (cwp_wp with "H"). iIntros (v) "H". cwp_pures.
iApply cwp_seq_bind'. iApply (cwp_wand with "H").
iIntros (v') "[[-> ?] | [-> ?]] !>"; by cwp_pures.
iIntros (v') "[[-> ?] | [-> ?]] !> !>"; by cwp_pures.
Qed.
Lemma cwp_while R Φ c e :
......@@ -498,9 +498,9 @@ Section proofs.
iIntros "H". cwp_lam. cwp_pures. rewrite /c_if -lock. cwp_pures.
cwp_apply (cwp_wp with "H"). iIntros (v) "H". cwp_lam. cwp_pures.
iApply cwp_seq_bind'. iApply (cwp_wand with "H").
iIntros (v') "[[-> H] | [-> H]] !>".
iIntros (v') "[[-> H] | [-> H]] !> !>".
- cwp_pures. iApply cwp_seq_bind'.
iApply (cwp_wand with "H"); iIntros (w) "H !>". by cwp_lam.
iApply (cwp_wand with "H"); iIntros (w) "H !> !>". by cwp_lam.
- cwp_pures. iApply cwp_ret. by iApply wp_value.
Qed.
......@@ -532,7 +532,7 @@ Section proofs.
CWP (λᶜ mx, e)%V v @ R {{ Φ }}.
Proof.
iIntros "H". cwp_lam. iApply cwp_seq_bind; simpl. cwp_lam.
iApply (cwp_wand with "H"); iIntros (w) "H !>".
iApply (cwp_wand with "H"); iIntros (w) "H !> !>".
by iApply cwp_ret; iApply wp_value.
Qed.
......
From stdpp Require Import namespaces.
From iris_c.vcgen Require Import proofmode.
From iris_c.lib Require Import mset list.
From iris.algebra Require Import frac_auth csum excl agree.
Definition storeme : val := λᶜ "l",
c_ret "l" = 10 ; 10.
Definition lol : val := λᶜ "l",
call (c_ret storeme) (c_ret "l") + (c_ret "l" = 11).
Section lol.
Context `{cmonadG Σ, !inG Σ (frac_authR natR)}.
Lemma cwp_store_hard R Φ Ψ1 Ψ2 e1 e2 :
CWP e1 @ R {{ Ψ1 }} -
CWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - R - cl w,
v1 = cloc_to_val cl cl C w (cl C[LLvl] v2 ={}= R Φ v2)) -
CWP e1 = e2 @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
cwp_apply (cwp_wp with "H2"); iIntros (v2) "H2".
cwp_apply (cwp_wp with "H1"); iIntros (v1) "H1".
Transparent c_store. unfold c_store.
cwp_lam. cwp_pures.
iApply cwp_bind. iApply (cwp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>". cwp_pures.
iApply cwp_atomic_env.
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
iDestruct ("HΦ" with "H1 H2 HR") as (cl w ->) "[Hl HΦ]".
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1.
iDestruct (mapsto_offset_non_neg with "Hl") as %?.
assert ((#(cloc_base cl), #(cloc_offset cl))%V X) as HclX.
{ intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
iMod (full_locking_heap_store_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply (mset_add_spec with "[$]"); first done.
iIntros "Hlocks /="; wp_pures.
wp_load; wp_pures.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
wp_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl').
iApply wp_fupd. wp_store.
iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
iMod ("HΦ" with "Hl") as "[$ $]". iIntros "!> !>".
iExists ({[(#(cloc_base cl), #(cloc_offset cl))%V]} X), _.
iFrame "Hσ Hlocks". iPureIntro. rewrite locked_locs_lock. set_solver.
Qed.
Lemma storeme_spec R cl v Φ :
cl C v - (cl C #10 - Φ #10) -
CWP storeme (cloc_to_val cl) @ R {{ Φ }}.
Proof.
iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H".
Qed.
Definition oneshotR := csumR (exclR unitR) (agreeR natC).
Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ oneshotG Σ.
Proof. solve_inG. Qed.
Definition pending γ `{oneshotG Σ} := own γ (Cinl (Excl ())).
Definition shot γ n `{oneshotG Σ} := own γ (Cinr (to_agree n)).
Lemma new_pending `{oneshotG Σ} : (|==> γ, pending γ)%I.
Proof. by apply own_alloc. Qed.
Lemma shoot γ m `{oneshotG Σ} : pending γ == shot γ m.
Proof.
apply own_update.
intros n [f |]; simpl; eauto.
destruct f; simpl; try by inversion 1.
Qed.
Lemma shot_not_pending γ b `{oneshotG Σ} :
shot γ b - pending γ - False.
Proof.
iIntros "Hs Hp".
iPoseProof (own_valid_2 with "Hs Hp") as "H".
iDestruct "H" as %[].
Qed.
Lemma shot_agree γ m n `{oneshotG Σ} :
shot γ m - shot γ n - m = n.
Proof.
iIntros "Hs Hs'".
iPoseProof (own_valid_2 with "Hs Hs'") as "H".
rewrite Cinr_op /=.
by iDestruct "H" as %LOL%agree_op_invL'.
Qed.
Lemma lol_spec R cl `{oneshotG Σ} :
cl C #0%nat -
CWP lol (cloc_to_val cl) @ R {{ v, v = #21
(cl C #10 cl C #11) }}.
Proof.
iIntros "Hl". iApply cwp_fun.
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]"; [done|].
set (lol_inv := ((cl C #0 own γ (! 0%nat))
(cl C #10 own γ (! 10%nat))
(cl C[LLvl] #11 own γ (! 11%nat))
)%I).
iApply (cwp_insert_res _ _ lol_inv with "[Hγ Hl]").
{ iNext. iLeft. eauto with iFrame. }
simpl.
iApply (cwp_bin_op _ _ (λ v, v = #10 own γ (!{1 / 2} 10%nat))%I
(λ v, v = #11 own γ (!{1 / 2} 11%nat))%I
with "[Hγ1] [Hγ2]").
- vcg. unfold lol_inv. iIntros "[H R]".
admit.
- iApply (cwp_store_hard _ _ (λ v, v = cloc_to_val cl)%I
(λ v, v = #11)%I).
1,2: vcg; eauto.
iIntros (? ? -> ->) "[H R]". unfold lol_inv.
iDestruct "H" as "[[Hcl H] | [[Hcl H] | [Hcl H]]]".
+ iExists cl, _. iFrame. iSplit; first done.
iIntros "Hl". iMod (own_update_2 with "H Hγ2") as "[H Hγ2]".
{ apply frac_auth_update.
apply (nat_local_update _ _ 11%nat 11%nat); lia. }
iModIntro. iFrame "Hγ2". iSplit; last done.
iRight. iRight. iFrame.
+ iExists cl, _. iFrame. iSplit; first done.
iIntros "Hl". iMod (own_update_2 with "H Hγ2") as "[H Hγ2]".
{ apply frac_auth_update.
apply (nat_local_update _ _ 11%nat 1%nat). lia. }
iModIntro. Abort.
End lol.
......@@ -212,7 +212,7 @@ Section forward_spec.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
iApply cwp_seq_bind. iApply (cwp_wand with "H1"); iIntros (v1) "[-> Hm]".
iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro.
iDestruct (denv_unlock_interp with "Hm") as "Hm"; do 2 iModIntro.
iDestruct ("H2" with "Hm") as "[Hm2 H]". rewrite -dcexpr_interp_subst'.
iApply (cwp_wand with "H"); iIntros (v2) "[-> Hm]".
iSplit; first done. iApply (denv_merge_interp with "[$]"); eauto 10.
......
......@@ -447,7 +447,7 @@ Section vcg_spec.
iDestruct ("IH" with "[] [] Hm H") as "H"; eauto.
iApply cwp_seq_bind. iApply (cwp_wand with "H").
iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]".
iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro.
iDestruct (denv_unlock_interp with "Hm") as "Hm"; do 2 iModIntro.
rewrite (dcexpr_interp_mono E E') // -dcexpr_interp_subst'.
iDestruct ("IH" with "[] [] Hm H") as "H"; eauto using dcexpr_wf_mono.
iApply (cwp_wand with "H"); iIntros (v) "H".
......
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