Commit 84f6294f by Dan Frumin

### Merge branch 'ccall'

parents 404b952d 7b4eb36f
 ... @@ -146,8 +146,10 @@ Notation "'λᶜ' x , e" := (c_fun (λ: x, e)%V) ... @@ -146,8 +146,10 @@ Notation "'λᶜ' x , e" := (c_fun (λ: x, e)%V) Definition c_call : val := λ: "f" "arg", Definition c_call : val := λ: "f" "arg", (* sequence point before a function call *) (* sequence point before a function call *) "fa" ←ᶜ ("f" |||ᶜ "arg");ᶜ "fa" ←ᶜ ("f" |||ᶜ "arg") ;;ᶜ c_atomic (λ: <>, (Fst "fa") (Snd "fa")). c_atomic (λ: <>, c_atomic_env mset_clear ;;ᶜ (Fst "fa") (Snd "fa")). Notation "'callᶜ' f a" := Notation "'callᶜ' f a" := (c_call f a)%E (c_call f a)%E (at level 10, f, a at level 9, (at level 10, f, a at level 9, ... @@ -382,23 +384,20 @@ Section proofs. ... @@ -382,23 +384,20 @@ Section proofs. iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame. iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame. Qed. Qed. (* Internal spec: breaks the abstraction/notation *) (** Helper lemma *) Lemma cwp_seq_bind' R Φ e (f: val) : Lemma cwp_mset_clear R Φ : CWP e @ R {{ v, U (CWP f v @ R {{ Φ }}) }} -∗ ▷ U (Φ #()) -∗ CWP c_seq_bind e f @ R {{ Φ }}. CWP c_atomic_env mset_clear @ R {{ Φ }}. Proof. Proof. iIntros "H". iIntros "HΦ". iApply cwp_atomic_env. cwp_apply (cwp_wp with "H"); iIntros (v) "H". cwp_lam. cwp_pures. iIntros (env). iDestruct (1) as (X σ _) "[Hlocks Hσ]". iApply cwp_bind. iApply (cwp_wand with "H"). iIntros (w) "H". iIntros "\$". iApply wp_fupd. cwp_pures. iApply cwp_bind. iApply cwp_atomic_env. iIntros (env) "Henv \$". iApply wp_fupd. iDestruct "Henv" as (X σ _) "[Hlocks Hσ]". wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks". wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks". rewrite U_eq. iDestruct "H" as (us) "[Hus H]". rewrite U_eq. iDestruct "HΦ" as (us) "[Hus H]". iInduction us as [|[ul [uq uv]] us] "IH" using gmultiset_ind forall (σ); simpl. iInduction us as [|[ul [uq uv]] us] "IH" using gmultiset_ind forall (σ); simpl. - iModIntro. iSplitR "H". - iModIntro. iSplitR "H Hus". + iExists ∅, σ. by iFrame. + iExists ∅, σ. by iFrame. + iNext. cwp_lam. by iApply "H". + iNext. by iApply "H". - iDestruct "Hus" as "[Hu Hus]". rewrite !big_sepMS_singleton /=. - iDestruct "Hus" as "[Hu Hus]". rewrite !big_sepMS_singleton /=. iDestruct (full_locking_heap_locked_present with "Hu Hσ") as %[z Hz]. iDestruct (full_locking_heap_locked_present with "Hu Hσ") as %[z Hz]. iMod (full_locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]". iMod (full_locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]". ... @@ -406,6 +405,18 @@ Section proofs. ... @@ -406,6 +405,18 @@ Section proofs. iIntros "Hus". iApply "H". iFrame. by rewrite !big_sepMS_singleton /=. iIntros "Hus". iApply "H". iFrame. by rewrite !big_sepMS_singleton /=. Qed. Qed. (* Internal spec: breaks the abstraction/notation *) Lemma cwp_seq_bind' R Φ e (f: val) : CWP e @ R {{ v, U (CWP f v @ R {{ Φ }}) }} -∗ CWP c_seq_bind e f @ R {{ Φ }}. Proof. iIntros "H". cwp_apply (cwp_wp with "H"); iIntros (v) "H". cwp_lam. cwp_pures. iApply cwp_bind. iApply (cwp_wand with "H"). iIntros (w) "H". cwp_pures. iApply cwp_bind. iApply cwp_mset_clear. iNext. iModIntro. by cwp_lam. Qed. Lemma cwp_seq_bind R Φ x e1 e2 : 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 {{ Φ }}. CWP x ←ᶜ e1 ;ᶜ e2 @ R {{ Φ }}. ... @@ -535,11 +546,12 @@ Section proofs. ... @@ -535,11 +546,12 @@ Section proofs. cwp_apply (cwp_wp with "H2"); iIntros (vf) "H2". cwp_apply (cwp_wp with "H2"); iIntros (vf) "H2". cwp_apply (cwp_wp with "H1"); iIntros (va) "H1". cwp_apply (cwp_wp with "H1"); iIntros (va) "H1". cwp_lam. cwp_pures. cwp_lam. cwp_pures. iApply cwp_seq_bind'. iApply (cwp_par with "H1 H2"). iApply cwp_bind. iApply (cwp_par with "H1 H2"). iIntros "!>" (f a) "H1 H2 !>". iSpecialize ("H" with "H1 H2"); iModIntro. iIntros "!>" (f a) "H1 H2 !>". iSpecialize ("H" with "H1 H2"). cwp_pures. cwp_pures. iApply cwp_atomic. iIntros "HR". iNext. iApply cwp_atomic. iIntros "HR". iSpecialize ("H" with "HR"). iExists True%I. iSplitR; first done. cwp_pures. iExists True%I. iModIntro; iSplit; first done. cwp_pures. iApply cwp_bind. iApply cwp_mset_clear. iNext. iModIntro. iSpecialize ("H" with "HR"). cwp_pures. iApply (cwp_wand with "H"); eauto. iApply (cwp_wand with "H"); eauto. Qed. Qed. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!