diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v index fcb7012e344970269d79cbfc7b85a7dd88a5c36c..d4663bc009e5b360f7e5ba6fcb09ec5ce2d99ea3 100644 --- a/theories/c_translation/translation.v +++ b/theories/c_translation/translation.v @@ -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. diff --git a/theories/tests/store_strong.v b/theories/tests/store_strong.v new file mode 100644 index 0000000000000000000000000000000000000000..6a9ad9168aaefe8a99f61b0e8230a5dadbc551f0 --- /dev/null +++ b/theories/tests/store_strong.v @@ -0,0 +1,126 @@ +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. + diff --git a/theories/vcgen/forward.v b/theories/vcgen/forward.v index a9afc224e5bd500c03bf93cba74e04759a2be2db..7a92b2c1ea1e5a55062268877dadf2ea5e9e50e6 100644 --- a/theories/vcgen/forward.v +++ b/theories/vcgen/forward.v @@ -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. diff --git a/theories/vcgen/vcg.v b/theories/vcgen/vcg.v index 414108f8fab84ff4dd316ffc6166dca30e53ef56..e3ca7fe5abdcd439cbc98044496a7f1e0d316e60 100644 --- a/theories/vcgen/vcg.v +++ b/theories/vcgen/vcg.v @@ -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".