diff --git a/_CoqProject b/_CoqProject
index ec2059ef884237ce41412b494509c2b13056efd4..9453981ae9cc52d2b081226d5fe733886990f2d0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,4 +4,4 @@ theories/list.v
theories/auth_excl.v
theories/typing.v
theories/channel.v
-theories/logrel.v
\ No newline at end of file
+theories/logrel.v
diff --git a/theories/auth_excl.v b/theories/auth_excl.v
index 0382c0f902940822d019a4ea0488c740ebbaf7ee..69c8b3e6b5f6fff29b9dff549dc1f7e73a939868 100644
--- a/theories/auth_excl.v
+++ b/theories/auth_excl.v
@@ -4,52 +4,64 @@ From iris.algebra Require Import excl auth.
From iris.base_logic.lib Require Import auth.
Set Default Proof Using "Type".
-Definition exclUR (A : Type) : ucmraT :=
- optionUR (exclR (leibnizC A)).
+Class auth_exclG (A : ofeT) (Σ : gFunctors) := AuthExclG {
+ exclG_authG :> inG Σ (authR (optionUR (exclR A)));
+}.
-Class auth_exclG (A : Type) (Σ :gFunctors) :=
- AuthExclG {
- exclG_authG :> authG Σ (exclUR A);
- }.
+Definition auth_exclΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
+ #[GFunctor (authRF (optionURF (exclRF F)))].
-Definition auth_exclΣ (A : Type) : gFunctors :=
- #[GFunctor (authR (exclUR A))].
-
-Instance subG_auth_exclG (A : Type) {Σ} :
- subG (auth_exclΣ A) Σ → (auth_exclG A) Σ.
+Instance subG_auth_exclG (F : cFunctor) `{!cFunctorContractive F} {Σ} :
+ subG (auth_exclΣ F) Σ → auth_exclG (F (iPreProp Σ)) Σ.
Proof. solve_inG. Qed.
-Definition to_auth_excl {A : Type} (a : A) : exclUR A :=
- Excl' (a: leibnizC A).
+Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
+ Excl' a.
+Instance: Params (@to_auth_excl) 1.
+
+Section auth_excl_ofe.
+ Context {A : ofeT}.
+
+ Global Instance to_auth_excl_ne : NonExpansive (@to_auth_excl A).
+ Proof. solve_proper. Qed.
+
+ Global Instance to_auth_excl_proper :
+ Proper ((≡) ==> (≡)) (@to_auth_excl A).
+ Proof. solve_proper. Qed.
+End auth_excl_ofe.
Section auth_excl.
Context `{!auth_exclG A Σ}.
+ Implicit Types x y : A.
+
+ Lemma to_auth_excl_valid x y :
+ ✓ (◠to_auth_excl x ⋅ ◯ to_auth_excl y) -∗ (x ≡ y : iProp Σ).
+ Proof.
+ iIntros "Hvalid".
+ iDestruct (auth_validI with "Hvalid") as "[Hy Hvalid]"; simpl.
+ iDestruct "Hy" as ([z|]) "Hy"; last first.
+ - by rewrite left_id right_id_L bi.option_equivI /= excl_equivI.
+ - iRewrite "Hy" in "Hvalid".
+ by rewrite left_id uPred.option_validI /= excl_validI /=.
+ Qed.
Lemma excl_eq γ x y :
- own γ (â— to_auth_excl y) -∗ own γ (â—¯ to_auth_excl x) -∗ ⌜x = yâŒ%I.
+ own γ (◠to_auth_excl x) -∗ own γ (◯ to_auth_excl y) -∗ x ≡ y.
Proof.
iIntros "Hauth Hfrag".
- iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
- apply auth_valid_discrete_2 in Hvalid.
- destruct Hvalid as [Hincl _].
- apply Excl_included in Hincl.
- unfold to_auth_excl.
- rewrite Hincl.
- iFrame.
- eauto.
+ iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
+ iDestruct (to_auth_excl_valid with "Hvalid") as "$".
Qed.
Lemma excl_update γ x y z :
- own γ (◠to_auth_excl y) -∗ own γ (◯ to_auth_excl x) ==∗
- own γ (◠to_auth_excl z) ∗ own γ (◯ to_auth_excl z).
+ own γ (◠to_auth_excl y) -∗ own γ (◯ to_auth_excl x) ==∗
+ own γ (◠to_auth_excl z) ∗ own γ (◯ to_auth_excl z).
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_update_2 with "Hauth Hfrag") as "H".
{ eapply (auth_update _ _ (to_auth_excl z) (to_auth_excl z)).
eapply option_local_update.
eapply exclusive_local_update. done. }
- rewrite own_op.
- done.
+ by rewrite own_op.
Qed.
-
End auth_excl.
diff --git a/theories/channel.v b/theories/channel.v
index a43b413067fe68db15d312e1aca35a0e5bba2df8..33f0f48d8ed1e74cb096040136411d85b0d22040 100644
--- a/theories/channel.v
+++ b/theories/channel.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl auth.
+From iris.algebra Require Import excl auth list.
From iris.base_logic.lib Require Import auth.
From iris.heap_lang.lib Require Import spin_lock.
From osiris Require Import list.
@@ -57,8 +57,17 @@ Definition recv : val :=
| NONE => "go" "c" "s"
end.
+Class chanG Σ := {
+ chanG_lockG :> lockG Σ;
+ chanG_authG :> auth_exclG (listC valC) Σ;
+}.
+Definition chanΣ : gFunctors :=
+ #[ lockΣ; auth_exclΣ (constCF (listC valC)) ].
+Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
+Proof. solve_inG. Qed.
+
Section channel.
- Context `{!heapG Σ, !lockG Σ, !auth_exclG (list val) Σ} (N : namespace).
+ Context `{!heapG Σ, !chanG Σ} (N : namespace).
Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
(∃ l':loc, ∃ hd : val, ⌜l = #l'⌠∧ l' ↦ hd ∗ ⌜is_list hd xsâŒ)%I.
@@ -159,7 +168,7 @@ Section channel.
wp_load. wp_apply (lsnoc_spec with "Hlvs"). iIntros (lhd' Hlvs).
wp_bind (_ <- _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
- iDestruct (excl_eq with "Hvs Hchan") as %->.
+ iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
wp_store. iMod ("HΦ" with "Hchan") as "HΦ".
iModIntro.
@@ -188,7 +197,7 @@ Section channel.
wp_bind (! _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
wp_load.
- iDestruct (excl_eq with "Hvs Hchan") as %->.
+ iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
destruct vs as [|v vs]; simpl.
- iDestruct "Hlvs" as %->.
iDestruct "HΦ" as "[HΦ _]".
diff --git a/theories/list.v b/theories/list.v
index df0935e04e536b83e98bbf14af68ae24bbd379f1..0563e905a8d00b6302eda666f13102d61fd7e28b 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -154,15 +154,13 @@ Lemma lsnoc_spec hd vs v :
Proof.
iIntros (Φ Hvs) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hvs Φ).
- - inversion Hvs.
- subst.
+ - simplify_eq/=.
wp_rec.
wp_pures.
wp_lam.
wp_pures.
iApply "HΦ". simpl. eauto.
- - inversion Hvs as [vs' [Hhd Hvs']]; subst.
- eauto.
+ - destruct Hvs as [vs' [-> Hvs']].
wp_rec.
wp_pures.
wp_bind (lsnoc vs' v).
@@ -175,5 +173,4 @@ Proof.
eauto.
iApply "HΦ".
Qed.
-
End lists.
\ No newline at end of file
diff --git a/theories/logrel.v b/theories/logrel.v
index 0fbb9e968df033be39d810ec820e254f02d9e372..c2b55f5d580f3d5b042fe667e23c18777c3e045a 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -7,10 +7,21 @@ From osiris Require Import typing auth_excl channel.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
+Class logrelG Σ := {
+ logrelG_channelG :> chanG Σ;
+ logrelG_authG :> auth_exclG (laterC (stypeC (iPreProp Σ))) Σ;
+}.
+
+Definition logrelΣ :=
+ #[ chanΣ ; GFunctor (authRF (optionURF (exclRF (laterCF (stypeCF idCF))))) ].
+Instance subG_chanΣ {Σ} : subG logrelΣ Σ → logrelG Σ.
+Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
+
Section logrel.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
- Context `{!auth_exclG (list val) Σ}.
- Context `{!auth_exclG stype Σ}.
+ Context `{!logrelG Σ}.
+
+ Notation stype_iprop := (@stypeC (laterC (iProp Σ))).
Record st_name := SessionType_name {
st_c_name : chan_name;
@@ -18,59 +29,118 @@ Section logrel.
st_r_name : gname
}.
- Definition st_own (γ : st_name) (s : side) (st : stype) : iProp Σ :=
- own (side_elim s st_l_name st_r_name γ) (◯ to_auth_excl st)%I.
+ Definition to_stype_auth_excl (st : stype (iProp Σ)) :=
+ to_auth_excl (Next (stype_map iProp_unfold st)).
+
+ Definition st_own (γ : st_name) (s : side) (st : stype (iProp Σ)) : iProp Σ :=
+ own (side_elim s st_l_name st_r_name γ)
+ (â—¯ to_stype_auth_excl st)%I.
+
+ Definition st_ctx (γ : st_name) (s : side) (st : stype (iProp Σ)) : iProp Σ :=
+ own (side_elim s st_l_name st_r_name γ)
+ (â— to_stype_auth_excl st)%I.
+
+ Lemma st_excl_eq γ s st st' :
+ st_ctx γ s st -∗ st_own γ s st' -∗ ▷ (st ≡ st').
+ Proof.
+ iIntros "Hauth Hfrag".
+ iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
+ iDestruct (to_auth_excl_valid with "Hvalid") as "Hvalid".
+ iDestruct (bi.later_eq_1 with "Hvalid") as "Hvalid"; iNext.
+ assert (∀ st : stype (iProp Σ),
+ stype_map iProp_fold (stype_map iProp_unfold st) ≡ st) as help.
+ { intros st''. rewrite -stype_fmap_compose -{2}(stype_fmap_id st'').
+ apply stype_map_ext=> P. by rewrite /= iProp_fold_unfold. }
+ rewrite -{2}(help st). iRewrite "Hvalid". by rewrite help.
+ Qed.
- Definition st_ctx (γ : st_name) (s : side) (st : stype) : iProp Σ :=
- own (side_elim s st_l_name st_r_name γ) (◠to_auth_excl st)%I.
+ Lemma st_excl_update γ s st st' st'' :
+ st_ctx γ s st -∗ st_own γ s st' ==∗
+ st_ctx γ s st'' ∗ st_own γ s st''.
+ Proof.
+ iIntros "Hauth Hfrag".
+ iDestruct (own_update_2 with "Hauth Hfrag") as "H".
+ { eapply (auth_update _ _ (to_stype_auth_excl st'')
+ (to_stype_auth_excl st'')).
+ eapply option_local_update.
+ eapply exclusive_local_update. done. }
+ rewrite own_op.
+ done.
+ Qed.
- Fixpoint st_eval (vs : list val) (st1 st2 : stype) : Prop :=
+ Fixpoint st_eval (vs : list val) (st1 st2 : stype (iProp Σ)) : iProp Σ :=
match vs with
- | [] => st1 = dual_stype st2
+ | [] => st1 ≡ dual_stype st2
| v::vs => match st2 with
- | TRecv 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.
+ end%I.
+ Arguments st_eval : simpl nomatch.
- Lemma st_eval_send (P : val -> Prop) st l str v :
- P v → st_eval l (TSend P st) str → st_eval (l ++ [v]) (st v) str.
+ 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.
- intro HP.
- revert str.
- induction l; intros str.
- - inversion 1. simpl.
- destruct str; inversion H1; subst. eauto.
- - intros. simpl.
- destruct str; inversion H.
- split=> //.
- apply IHl=> //.
+ 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.
- Lemma st_eval_recv (P : val → Prop) st1 l st2 v :
- st_eval (v :: l) st1 (TRecv P st2) → st_eval l st1 (st2 v) ∧ P v.
+ Global Instance st_eval_ne : NonExpansive2 (st_eval vs).
Proof.
- intros Heval.
- generalize dependent st1.
- induction l; intros.
- - inversion Heval; subst. split=> //.
- - inversion Heval; subst. simpl.
- constructor=> //.
+ intros vs n. induction vs as [|v vs IH]; [solve_proper|].
+ destruct 2 as [|[] ????? Hst]=> //=. f_equiv. solve_proper.
+ by apply IH, Hst.
Qed.
- Definition inv_st (γ :st_name) (c : val) : iProp Σ :=
+ 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.
+ Proof.
+ iIntros "HP".
+ iRevert (str).
+ iInduction l as [|l] "IH"; iIntros (str) "Heval".
+ - simpl.
+ iDestruct (dual_stype_flip with "Heval") as "Heval".
+ iRewrite -"Heval". simpl.
+ rewrite dual_stype_involutive.
+ by iFrame.
+ - simpl.
+ destruct str; auto.
+ destruct a; auto.
+ iDestruct "Heval" as "[HP0 Heval]".
+ iFrame.
+ by iApply ("IH" with "HP").
+ 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.
+ Proof. iDestruct 1 as "[HP Heval]". iFrame. Qed.
+
+ Definition inv_st (γ : st_name) (c : val) : iProp Σ :=
(∃ l r stl str,
chan_own (st_c_name γ) Left l ∗
chan_own (st_c_name γ) Right r ∗
st_ctx γ Left stl ∗
st_ctx γ Right str ∗
- ((⌜r = []⌠∗ ⌜st_eval l stl strâŒ) ∨
- (⌜l = []⌠∗ ⌜st_eval r str stlâŒ)))%I.
+ ((⌜r = []⌠∗ st_eval l stl str) ∨
+ (⌜l = []⌠∗ st_eval r str stl)))%I.
- Definition is_st (γ : st_name) (st : stype) (c : val) : iProp Σ :=
+ Definition is_st (γ : st_name) (st : stype (iProp Σ)) (c : val) : iProp Σ :=
(is_chan N (st_c_name γ) c ∗ inv N (inv_st γ c))%I.
- Definition interp_st (γ : st_name) (st : stype)
+ Definition interp_st (γ : st_name) (st : stype (iProp Σ))
(c : val) (s : side) : iProp Σ :=
(st_own γ s st ∗ is_st γ st c)%I.
@@ -88,11 +158,11 @@ Section logrel.
⟦ c @ Left : st ⟧{γ} ∗ ⟦ c @ Right : dual_stype st ⟧{γ}.
Proof.
iIntros "[#Hcctx [Hcol Hcor]]".
- iMod (own_alloc (â— (to_auth_excl st) â‹…
- â—¯ (to_auth_excl st)))
+ iMod (own_alloc (â— (to_stype_auth_excl st) â‹…
+ â—¯ (to_stype_auth_excl st)))
as (lγ) "[Hlsta Hlstf]"; first done.
- iMod (own_alloc (â— (to_auth_excl (dual_stype st)) â‹…
- â—¯ (to_auth_excl (dual_stype st))))
+ iMod (own_alloc (â— (to_stype_auth_excl (dual_stype st)) â‹…
+ â—¯ (to_stype_auth_excl (dual_stype st))))
as (rγ) "[Hrsta Hrstf]"; first done.
pose (SessionType_name cγ lγ rγ) as stγ.
iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
@@ -120,13 +190,13 @@ Section logrel.
by iFrame.
Qed.
- Lemma send_vs c γ s (P : val → Prop) st E :
+ Lemma send_vs c γ s (P : val → iProp Σ) st E :
↑N ⊆ E →
- ⟦ c @ s : TSend P st ⟧{γ} ={E,E∖↑N}=∗
+ ⟦ c @ s : TSR Send P st ⟧{γ} ={E,E∖↑N}=∗
∃ vs, chan_own (st_c_name γ) s vs ∗
- ▷ (∀ v, ⌜P v⌠-∗
- chan_own (st_c_name γ) s (vs ++ [v])
- ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{γ}).
+ ▷ (∀ v, P v -∗
+ chan_own (st_c_name γ) s (vs ++ [v])
+ ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{γ}).
Proof.
iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
iMod (inv_open with "Hinv") as "Hinv'"=> //.
@@ -136,93 +206,82 @@ Section logrel.
iModIntro.
destruct s.
- iExists _.
- iIntros "{$Hclf} !>" (v HP) "Hclf".
+ iIntros "{$Hclf} !>" (v) "HP Hclf".
iRename "Hstf" into "Hstlf".
- iDestruct (excl_eq with "Hstla Hstlf") as %<-.
- iMod (excl_update _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
+ iDestruct (st_excl_eq with "Hstla Hstlf") as "#Heq".
+ iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf")
+ as "[Hstla Hstlf]".
iMod ("Hinvstep" with "[-Hstlf]") as "_".
{
iNext.
iExists _,_,_,_. iFrame.
iLeft.
- iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
- iDestruct "Heval" as %Heval.
+ iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iSplit=> //.
- iPureIntro.
- by eapply st_eval_send.
- - destruct r; inversion Heval; subst.
- iSplit=> //.
- iPureIntro.
- simpl.
- rewrite (involutive (st v)).
- rewrite -(involutive (dual_stype (st v))).
- split=> //.
+ iApply (st_eval_send with "HP").
+ by iRewrite -"Heq".
+ - iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //.
+ iSplit; first done. simpl.
+ iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
}
- iModIntro. iFrame "Hcctx ∗ Hinv".
+ iModIntro. iFrame. rewrite /is_st. auto.
- iExists _.
- iIntros "{$Hcrf} !>" (v HP) "Hcrf".
+ iIntros "{$Hcrf} !>" (v) "HP Hcrf".
iRename "Hstf" into "Hstrf".
- iDestruct (excl_eq with "Hstra Hstrf") as %<-.
- iMod (excl_update _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
+ iDestruct (st_excl_eq with "Hstra Hstrf") as "#Heq".
+ iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf")
+ as "[Hstra Hstrf]".
iMod ("Hinvstep" with "[-Hstrf]") as "_".
{
iNext.
- iExists _,_, _, _. iFrame.
+ iExists _,_,_,_. iFrame.
iRight.
- iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
- iDestruct "Heval" as %Heval.
- - destruct l; inversion Heval; subst.
- iSplit=> //.
- iPureIntro.
- simpl.
- rewrite (involutive (st v)).
- rewrite -(involutive (dual_stype (st v))).
- split=> //.
+ iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
+ - iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
+ iSplit; first done. simpl.
+ iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
- iSplit=> //.
- iPureIntro.
- by eapply st_eval_send.
+ iApply (st_eval_send with "HP").
+ by iRewrite -"Heq".
}
- iModIntro. iFrame "Hcctx ∗ Hinv".
+ iModIntro. iFrame. rewrite /is_st. auto.
Qed.
- Lemma send_st_spec st γ c s (P : val → Prop) v :
- P v →
- {{{ ⟦ c @ s : TSend P st ⟧{γ} }}}
+ Lemma send_st_spec st γ c s (P : val → iProp Σ) v :
+ {{{ P v ∗ ⟦ c @ s : TSR Send P st ⟧{γ} }}}
send c #s v
{{{ RET #(); ⟦ c @ s : st v ⟧{γ} }}}.
Proof.
- iIntros (HP Φ) "Hsend HΦ".
+ iIntros (Φ) "[HP Hsend] HΦ".
iApply (send_spec with "[#]").
{ iDestruct "Hsend" as "[? [$ ?]]". }
iMod (send_vs with "Hsend") as (vs) "[Hch H]"; first done.
iModIntro. iExists vs. iFrame "Hch".
iIntros "!> Hupd". iApply "HΦ".
- iApply ("H" $! v HP with "[Hupd]"). by destruct s.
+ 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')".
- 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 "_".
@@ -230,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 "[#]").
@@ -286,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.
@@ -300,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
diff --git a/theories/typing.v b/theories/typing.v
index b742bd8a288b275fef677ebc73ace11e6e84b196..773117634fa7bd884a9bd626c7343bac53489662 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -1,41 +1,217 @@
From iris.heap_lang Require Export lang.
-Require Import FunctionalExtensionality.
+From iris.algebra Require Export cmra.
+From stdpp Require Export list.
+From iris.base_logic Require Import base_logic.
+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.
-Class Involutive {T} (f : T → T) :=
- involutive : ∀ t : T, t = f (f t).
-
-Inductive side : Set :=
-| Left
-| Right.
-
+Inductive side := Left | Right.
Instance side_inhabited : Inhabited side := populate Left.
-
Definition dual_side (s : side) : side :=
match s with Left => Right | Right => Left end.
+Instance dual_side_involutive : Involutive (=) dual_side.
+Proof. by intros []. Qed.
+
+Inductive action := Send | Receive.
+Instance action_inhabited : Inhabited action := populate Send.
+Definition dual_action (a : action) : action :=
+ match a with Send => Receive | Receive => Send end.
+Instance dual_action_involutive : Involutive (=) dual_action.
+Proof. by intros []. Qed.
+
+Inductive stype (A : Type) :=
+ | TEnd
+ | TSR (a : action) (P : val → A) (st : val → stype A).
+Arguments TEnd {_}.
+Arguments TSR {_} _ _ _.
+Instance: Params (@TSR) 2.
+
+Instance stype_inhabited A : Inhabited (stype A) := populate TEnd.
+
+Fixpoint dual_stype {A} (st : stype A) :=
+ match st with
+ | TEnd => TEnd
+ | TSR a P st => TSR (dual_action a) P (λ v, dual_stype (st v))
+ end.
+Instance: Params (@dual_stype) 1.
+
+Section stype_ofe.
+ Context {A : ofeT}.
+
+ Inductive stype_equiv : Equiv (stype A) :=
+ | TEnd_equiv : TEnd ≡ TEnd
+ | TSR_equiv a P1 P2 st1 st2 :
+ pointwise_relation val (≡) P1 P2 →
+ pointwise_relation val (≡) st1 st2 →
+ TSR a P1 st1 ≡ TSR a P2 st2.
+ Existing Instance stype_equiv.
+
+ Inductive stype_dist' (n : nat) : relation (stype A) :=
+ | TEnd_dist : stype_dist' n TEnd TEnd
+ | TSR_dist a P1 P2 st1 st2 :
+ pointwise_relation val (dist n) P1 P2 →
+ pointwise_relation val (stype_dist' n) st1 st2 →
+ stype_dist' n (TSR a P1 st1) (TSR a P2 st2).
+ Instance stype_dist : Dist (stype A) := stype_dist'.
+
+ Definition stype_ofe_mixin : OfeMixin (stype A).
+ Proof.
+ split.
+ - intros st1 st2. rewrite /dist /stype_dist. split.
+ + intros Hst n. induction Hst as [|a P1 P2 st1 st2 HP Hst IH]; constructor.
+ * intros v. apply equiv_dist, HP.
+ * intros v. apply IH.
+ + revert st2. induction st1 as [|a P1 st1 IH]; intros [|a' P2 st2] Hst.
+ * constructor.
+ * feed inversion (Hst O).
+ * feed inversion (Hst O).
+ * feed inversion (Hst O); subst.
+ constructor.
+ ** intros v. apply equiv_dist=> n. feed inversion (Hst n); subst; auto.
+ ** intros v. apply IH=> n. feed inversion (Hst n); subst; auto.
+ - rewrite /dist /stype_dist. split.
+ + intros st. induction st; constructor; repeat intro; auto.
+ + intros st1 st2. induction 1; constructor; repeat intro; auto.
+ symmetry; auto.
+ + intros st1 st2 st3 H1 H2.
+ revert H2. revert st3.
+ induction H1 as [| a P1 P2 st1 st2 HP Hst12 IH]=> //.
+ inversion 1. subst. constructor.
+ ** by transitivity P2.
+ ** intros v. by apply IH.
+ - intros n st1 st2. induction 1; constructor.
+ + intros v. apply dist_S. apply H.
+ + intros v. apply H1.
+ Qed.
+ Canonical Structure stypeC : ofeT := OfeT (stype A) stype_ofe_mixin.
+
+ Global Instance TSR_stype_ne a n :
+ Proper (pointwise_relation _ (dist n) ==> pointwise_relation _ (dist n) ==> dist n) (TSR a).
+ Proof.
+ intros P1 P2 HP st1 st2 Hst.
+ constructor.
+ - apply HP.
+ - intros v. apply Hst.
+ Qed.
+ Global Instance TSR_stype_proper a :
+ Proper (pointwise_relation _ (≡) ==> pointwise_relation _ (≡) ==> (≡)) (TSR a).
+ Proof.
+ intros P1 P2 HP st1 st2 Hst. apply equiv_dist=> n.
+ by f_equiv; intros v; apply equiv_dist.
+ Qed.
+
+ Global Instance dual_stype_ne : NonExpansive dual_stype.
+ Proof.
+ intros n. induction 1 as [| a P1 P2 st1 st2 HP Hst IH].
+ - constructor.
+ - constructor. apply HP. intros v. apply IH.
+ Qed.
+ Global Instance dual_stype_proper : Proper ((≡) ==> (≡)) dual_stype.
+ Proof. apply (ne_proper _). Qed.
-Instance dual_side_involutive : Involutive dual_side.
-Proof. intros s; destruct s; eauto. Qed.
+ Global Instance dual_stype_involutive : Involutive (≡) dual_stype.
+ Proof.
+ intros st.
+ induction st.
+ - constructor.
+ - rewrite /= (involutive (f:=dual_action)).
+ constructor. reflexivity. intros v. apply H.
+ Qed.
+
+ Lemma stype_equivI {M} st1 st2 :
+ st1 ≡ st2 ⊣⊢@{uPredI M}
+ match st1, st2 with
+ | TEnd, TEnd => True
+ | TSR a1 P1 st1, TSR a2 P2 st2 =>
+ ⌜ a1 = a2 ⌠∧ (∀ v, P1 v ≡ P2 v) ∧ (∀ v, st1 v ≡ st2 v)
+ | _, _ => False
+ end.
+ Proof.
+ uPred.unseal; constructor=> n x ?. split; first by destruct 1.
+ destruct st1, st2=> //=; [constructor|].
+ by intros [[= ->] [??]]; constructor.
+ Qed.
-Inductive stype :=
-| TEnd
-| TSend (P : val → Prop) (st : val → stype)
-| TRecv (P : val → Prop) (st : val → stype).
+ 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.
-Instance stype_inhabited : Inhabited stype := populate TEnd.
+End stype_ofe.
+Arguments stypeC : clear implicits.
-Fixpoint dual_stype (st :stype) :=
+Fixpoint stype_map {A B} (f : A → B) (st : stype A) : stype B :=
match st with
| TEnd => TEnd
- | TSend P st => TRecv P (λ v, dual_stype (st v))
- | TRecv P st => TSend P (λ v, dual_stype (st v))
+ | TSR a P st => TSR a (λ v, f (P v)) (λ v, stype_map f (st v))
end.
+Lemma stype_map_ext_ne {A} {B : ofeT} (f g : A → B) (st : stype A) n :
+ (∀ x, f x ≡{n}≡ g x) → stype_map f st ≡{n}≡ stype_map g st.
+Proof.
+ intros Hf. induction st as [| a P st IH]; constructor.
+ - intros v. apply Hf.
+ - intros v. apply IH.
+Qed.
+Lemma stype_map_ext {A} {B : ofeT} (f g : A → B) (st : stype A) :
+ (∀ x, f x ≡ g x) → stype_map f st ≡ stype_map g st.
+Proof.
+ intros Hf. apply equiv_dist.
+ intros n. apply stype_map_ext_ne.
+ intros x. apply equiv_dist.
+ apply Hf.
+Qed.
+Instance stype_map_ne {A B : ofeT} (f : A → B) n:
+ Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (stype_map f).
+Proof.
+ intros Hf st1 st2. induction 1 as [| a P1 P2 st1 st2 HP Hst IH]; constructor.
+ - intros v. f_equiv. apply HP.
+ - intros v. apply IH.
+Qed.
+Lemma stype_fmap_id {A : ofeT} (st : stype A) : stype_map id st ≡ st.
+Proof.
+ induction st as [| a P st IH]; constructor.
+ - intros v. reflexivity.
+ - intros v. apply IH.
+Qed.
+Lemma stype_fmap_compose {A B C : ofeT} (f : A → B) (g : B → C) st :
+ stype_map (g ∘ f) st ≡ stype_map g (stype_map f st).
+Proof.
+ induction st as [| a P st IH]; constructor.
+ - intros v. reflexivity.
+ - intros v. apply IH.
+Qed.
+
+Definition stypeC_map {A B} (f : A -n> B) : stypeC A -n> stypeC B :=
+ CofeMor (stype_map f : stypeC A → stypeC B).
+Instance stypeC_map_ne A B : NonExpansive (@stypeC_map A B).
+Proof. intros n f g ? st. by apply stype_map_ext_ne. Qed.
+
+Program Definition stypeCF (F : cFunctor) : cFunctor := {|
+ cFunctor_car A B := stypeC (cFunctor_car F A B);
+ cFunctor_map A1 A2 B1 B2 fg := stypeC_map (cFunctor_map F fg)
+|}.
+Next Obligation.
+ by intros F A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_ne.
+Qed.
+Next Obligation.
+ intros F A B x. rewrite /= -{2}(stype_fmap_id x).
+ apply stype_map_ext=>y. apply cFunctor_id.
+Qed.
+Next Obligation.
+ intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -stype_fmap_compose.
+ apply stype_map_ext=>y; apply cFunctor_compose.
+Qed.
-Instance dual_stype_involutive : Involutive dual_stype.
+Instance stypeCF_contractive F :
+ cFunctorContractive F → cFunctorContractive (stypeCF F).
Proof.
- intros st.
- induction st => //; simpl;
- assert (st = (λ v : val, dual_stype (dual_stype (st v)))) as Heq
- by apply functional_extensionality => //;
- rewrite -Heq => //.
+ by intros ? A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_contractive.
Qed.
+