### Bumped try_recv and recv to ofe st's

parent 4aa2399d
 ... ... @@ -4,3 +4,4 @@ theories/list.v theories/auth_excl.v theories/typing.v theories/channel.v theories/logrel.v
 ... ... @@ -72,36 +72,50 @@ Section logrel. match vs with | [] => st1 ≡ dual_stype st2 | v::vs => match st2 with | TSR Receive P st2 => ▷ P v ∗ st_eval vs st1 (st2 v) | TSR Receive P st2 => P v ∗ st_eval vs st1 (st2 v) | _ => False end end%I. Arguments st_eval : simpl nomatch. Lemma st_later_eq a P2 (st : stype (iProp Σ)) st2 : (▷ (st ≡ TSR a P2 st2) -∗ ◇ (∃ P1 st1, st ≡ TSR a P1 st1 ∗ ▷ ((∀ v, P1 v ≡ P2 v)) ∗ ▷ ((∀ v, st1 v ≡ st2 v))) : iProp Σ). Proof. destruct st. - iIntros "Heq". iDestruct (stype_equivI with "Heq") as ">Heq". done. - iIntros "Heq". iDestruct (stype_equivI with "Heq") as "Heq". iDestruct ("Heq") as "[>Haeq [HPeq Hsteq]]". iDestruct "Haeq" as %Haeq. subst. iExists P, st. iSplit=> //. by iSplitL "HPeq". Qed. Global Instance st_eval_ne : NonExpansive2 (st_eval vs). Proof. intros vs n. induction vs as [|v vs IH]; [solve_proper|]. destruct 2 as [|[] ????? Hst]=> //=. f_equiv. solve_proper. by apply IH, Hst. destruct 2 as [|[] ????? Hst]=> //=. f_equiv. solve_proper. by apply IH, Hst. Qed. Lemma st_eval_send (P : val -> iProp Σ) st l str v : ▷ P v -∗ st_eval l (TSR Send P st) str -∗ st_eval (l ++ [v]) (st v) str. P v -∗ st_eval l (TSR Send P st) str -∗ st_eval (l ++ [v]) (st v) str. Proof. iIntros "HP". iRevert (str). iInduction l as [|l] "IH"; iIntros (str) "Heval". - simpl. destruct str. + iDestruct (stype_equivI with "Heval") as "Heval". eauto. + destruct a. * iDestruct (stype_equivI with "Heval") as (Haction) "Heval". inversion Haction. * iDestruct (stype_equivI with "Heval") as (Haction) "Heval". iDestruct ("Heval") as "[HPeq Hsteq]". iSpecialize ("HPeq" \$!v). iSpecialize ("Hsteq" \$!v). iRewrite "HPeq" in "HP". iFrame. iDestruct (dual_stype_flip with "Heval") as "Heval". iRewrite -"Heval". simpl. rewrite dual_stype_involutive. by iFrame. - simpl. destruct str; auto. destruct a; auto. ... ... @@ -111,7 +125,7 @@ Section logrel. Qed. Lemma st_eval_recv (P : val → iProp Σ) st1 l st2 v : st_eval (v :: l) st1 (TSR Receive P st2) -∗ st_eval l st1 (st2 v) ∗ ▷ P v. st_eval (v :: l) st1 (TSR Receive P st2) -∗ st_eval l st1 (st2 v) ∗ P v. Proof. iDestruct 1 as "[HP Heval]". iFrame. Qed. Definition inv_st (γ : st_name) (c : val) : iProp Σ := ... ... @@ -234,7 +248,7 @@ Section logrel. Qed. Lemma send_st_spec st γ c s (P : val → iProp Σ) v : {{{ ▷ P v ∗ ⟦ c @ s : TSR Send P st ⟧{γ} }}} {{{ P v ∗ ⟦ c @ s : TSR Send P st ⟧{γ} }}} send c #s v {{{ RET #(); ⟦ c @ s : st v ⟧{γ} }}}. Proof. ... ... @@ -247,29 +261,27 @@ Section logrel. iApply ("H" \$! v with "HP"). by destruct s. Qed. Lemma try_recv_vs c γ s (P : val → Prop) st E : Lemma try_recv_vs c γ s (P : val → iProp Σ) st E : ↑N ⊆ E → ⟦ c @ s : TRecv P st ⟧{γ} ⟦ c @ s : TSR Receive P st ⟧{γ} ={E,E∖↑N}=∗ ∃ vs, chan_own (st_c_name γ) (dual_side s) vs ∗ (▷ ((⌜vs = []⌝ -∗ chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗ ⟦ c @ s : TRecv P st ⟧{γ}) ∧ (∀ v vs', ⌜vs = v :: vs'⌝ -∗ chan_own (st_c_name γ) (dual_side s) vs' ={E∖↑N,E}=∗ ⟦ c @ s : (st v) ⟧{γ} ∗ ⌜P v⌝))). ⟦ c @ s : TSR Receive P st ⟧{γ}) ∧ (∀ v vs', ⌜vs = v :: vs'⌝ -∗ chan_own (st_c_name γ) (dual_side s) vs' -∗ |={E∖↑N,E}=> ⟦ c @ s : (st v) ⟧{γ} ∗ ▷ P v))). Proof. iIntros (Hin) "[Hstf #[Hcctx Hinv]]". iMod (inv_open with "Hinv") as "Hinv'"=> //. iDestruct "Hinv'" as "[Hinv' Hinvstep]". iDestruct "Hinv'" as (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')". iExists (side_elim s l r). iModIntro. iExists (side_elim s r l). iModIntro. destruct s. - iExists _. iIntros "{\$Hcrf} !>". - simpl. iIntros "{\$Hcrf} !>". iRename "Hstf" into "Hstlf". rewrite /st_own /st_ctx. simpl. iDestruct (excl_eq with "Hstla Hstlf") as %<-. iDestruct (st_excl_eq with "Hstla Hstlf") as "#Heq". iSplit=> //. + iIntros "Hvs Hown". iMod ("Hinvstep" with "[-Hstlf]") as "_". ... ... @@ -277,38 +289,56 @@ Section logrel. iModIntro. iFrame "Hcctx ∗ Hinv". + iIntros (v vs Hvs) "Hown". iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; first inversion Hvs. iMod (excl_update _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]". iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]". subst. iDestruct "Heval" as %Heval. apply st_eval_recv in Heval as [Heval HP]. iMod ("Hinvstep" with "[-Hstlf]") as "_". { iExists _,_,_,_. iFrame. iRight=> //. } by iFrame (HP) "Hcctx Hinv". - iExists _. iIntros "{\$Hclf} !>". iDestruct (st_later_eq with "Heq") as ">Hleq". iDestruct "Hleq" as (P1 st1) "[Hsteq [HPeq Hsteq']]". iSpecialize ("HPeq" \$!v). iSpecialize ("Hsteq'" \$!v). iRewrite "Hsteq" in "Heval". subst. iDestruct (st_eval_recv with "Heval") as "[Heval HP]". iMod ("Hinvstep" with "[-Hstlf HP]") as "H". { iExists _,_,_,_. iFrame. iRight=> //. iNext. iSplit=> //. by iRewrite -"Hsteq'". } iModIntro. iSplitR "HP". * iFrame "Hstlf Hcctx Hinv". * iNext. by iRewrite -"HPeq". - simpl. iIntros "{\$Hclf} !>". iRename "Hstf" into "Hstrf". iDestruct (excl_eq with "Hstra Hstrf") as %<-. iDestruct (st_excl_eq with "Hstra Hstrf") as "#Heq". iSplit=> //. + iIntros "Hvs Hown". iMod ("Hinvstep" with "[-Hstrf]") as "_". { iNext. iExists l,r,_,_. iFrame. } iModIntro. iFrame "Hcctx ∗ Hinv". + simpl. iIntros (v vs' Hvs) "Hown". + iIntros (v vs' Hvs) "Hown". iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last inversion Hvs. iMod (excl_update _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]". iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]". subst. iDestruct "Heval" as %Heval. apply st_eval_recv in Heval as [Heval HP]. iMod ("Hinvstep" with "[-Hstrf]") as "_". { iExists _,_,_,_. iFrame. iLeft=> //. } by iFrame (HP) "Hcctx Hinv". iDestruct (st_later_eq with "Heq") as ">Hleq". iDestruct "Hleq" as (P1 st1) "[Hsteq [HPeq Hsteq']]". iSpecialize ("HPeq" \$!v). iSpecialize ("Hsteq'" \$!v). iRewrite "Hsteq" in "Heval". iDestruct (st_eval_recv with "Heval") as "[Heval HP]". iMod ("Hinvstep" with "[-Hstrf HP]") as "_". { iExists _,_,_,_. iFrame. iLeft=> //. iNext. iSplit=> //. by iRewrite -"Hsteq'". } iModIntro. iSplitR "HP". * iFrame "Hstrf Hcctx Hinv". * iNext. by iRewrite -"HPeq". Qed. Lemma try_recv_st_spec st γ c s (P : val → Prop) : {{{ ⟦ c @ s : TRecv P st ⟧{γ} }}} Lemma try_recv_st_spec st γ c s (P : val → iProp Σ) : {{{ ⟦ c @ s : TSR Receive P st ⟧{γ} }}} try_recv c #s {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : TRecv P st ⟧{γ}) ∨ (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : st w ⟧{γ} ∗ ⌜P w⌝)}}}. {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : TSR Receive P st ⟧{γ}) ∨ (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : st w ⟧{γ} ∗ ▷ P w)}}}. Proof. iIntros (Φ) "Hrecv HΦ". iApply (try_recv_spec with "[#]"). ... ... @@ -333,10 +363,10 @@ Section logrel. eauto with iFrame. Qed. Lemma recv_st_spec st γ c s (P : val → Prop) : {{{ ⟦ c @ s : TRecv P st ⟧{γ} }}} Lemma recv_st_spec st γ c s (P : val → iProp Σ) : {{{ ⟦ c @ s : TSR Receive P st ⟧{γ} }}} recv c #s {{{ v, RET v; ⟦ c @ s : st v ⟧{γ} ∗ ⌜P v⌝}}}. {{{ v, RET v; ⟦ c @ s : st v ⟧{γ} ∗ P v}}}. Proof. iIntros (Φ) "Hrecv HΦ". iLöb as "IH". wp_rec. ... ... @@ -347,11 +377,11 @@ Section logrel. iDestruct "Hv" as %->. wp_pures. iApply ("IH" with "[H]")=> //. - iDestruct "H" as (w) "[Hv H]". - iDestruct "H" as (w) "[Hv [H HP]]". iDestruct "Hv" as %->. wp_pures. iApply "HΦ". iFrame. Qed. End logrel. End logrel. \ No newline at end of file
 ... ... @@ -6,7 +6,6 @@ From iris.algebra Require Import updates local_updates. From iris.heap_lang Require Import proofmode notation. Set Default Proof Using "Type". Class Involutive {A} (R : relation A) (f : A → A) := involutive x : R (f (f x)) x. ... ... @@ -136,6 +135,15 @@ Section stype_ofe. destruct st1, st2=> //=; [constructor|]. by intros [[= ->] [??]]; constructor. Qed. Lemma dual_stype_flip {M} st1 st2 : dual_stype st1 ≡ st2 ⊣⊢@{uPredI M} st1 ≡ dual_stype st2. Proof. iSplit. - iIntros "Heq". iRewrite -"Heq". by rewrite dual_stype_involutive. - iIntros "Heq". iRewrite "Heq". by rewrite dual_stype_involutive. Qed. End stype_ofe. Arguments stypeC : clear implicits. ... ...
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