Commit 0fedd453 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Bumped Robbert feedback, WIP send st triple

parent f5672f9a
......@@ -27,27 +27,18 @@ Section auth_excl_ofe.
Context {A : ofeT}.
Global Instance to_auth_excl_ne : NonExpansive (@to_auth_excl A).
Proof.
intros n.
intros x y Heq.
rewrite /to_auth_excl.
by repeat f_equiv.
Qed.
Proof. solve_proper. Qed.
Global Instance to_auth_excl_proper :
Proper (() ==> ()) (@to_auth_excl A).
Proof.
intros x y Heq.
rewrite /to_auth_excl.
by repeat f_equiv.
Qed.
Proof. solve_proper. Qed.
End auth_excl_ofe.
Section auth_excl.
Context `{!auth_exclG A Σ}.
Lemma excl_eq γ x y :
own γ ( to_auth_excl y) - own γ ( to_auth_excl x) - x y.
own γ ( to_auth_excl y) - own γ ( to_auth_excl x) - x y.
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
......@@ -57,8 +48,8 @@ Section auth_excl.
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".
......
......@@ -7,10 +7,9 @@ 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 (@stypeC (laterC (iProp Σ))) Σ; (* Annotation? *)
logrelG_authG :> auth_exclG (stypeC (laterC (iProp Σ))) Σ;
}.
Section logrel.
......@@ -25,13 +24,49 @@ Section logrel.
st_r_name : gname
}.
Definition st_own (γ : st_name) (s : side) (st : stype_iprop) : iProp Σ :=
own (side_elim s st_l_name st_r_name γ) ( to_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_auth_excl st)%I.
Definition to_stype_auth_excl (st : stype (iProp Σ)) :=
to_auth_excl (stype_map Next 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.
apply auth_valid_discrete_2 in Hvalid.
destruct Hvalid as [Hincl _].
apply Excl_included in Hincl.
destruct st, st'; simpl in Hincl.
- eauto.
- inversion Hincl.
- inversion Hincl.
- inversion Hincl; subst.
admit.
Admitted.
Fixpoint st_eval (vs : list val) (st1 st2 : stype_iprop) : iProp Σ :=
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 (iProp Σ)) : iProp Σ :=
match vs with
| [] => st1 dual_stype st2
| v::vs => match st2 with
......@@ -40,30 +75,35 @@ Section logrel.
end
end%I.
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_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.
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=> //.
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.
- 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 Prop) st1 l st2 v :
st_eval (v :: l) st1 (TRecv P st2) st_eval l st1 (st2 v) P v.
Proof.
intros Heval.
generalize dependent st1.
induction l; intros.
- inversion Heval; subst. split=> //.
- inversion Heval; subst. simpl.
constructor=> //.
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,
......@@ -71,13 +111,13 @@ Section logrel.
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.
......@@ -95,11 +135,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".
......@@ -127,13 +167,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'"=> //.
......@@ -143,68 +183,68 @@ 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.
iDestruct (stype_equivI with "Heq") as "Heq'".
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=> //.
}
iModIntro. iFrame "Hcctx ∗ Hinv".
- iExists _.
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]".
iMod ("Hinvstep" with "[-Hstrf]") as "_".
{
iNext.
iExists _,_, _, _. iFrame.
iRight.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
iDestruct "Heval" as %Heval.
- destruct l; inversion Heval; subst.
iApply (st_eval_send with "HP").
destruct stl.
+ iDestruct "Heq'" as %Heq'. inversion Heq'.
+ iDestruct "Heq'" as "[Ha [HP Hst]]".
iDestruct "Ha" as %->.
admit. (* Rewrite! *)
- destruct r.
iSplit=> //.
iPureIntro.
simpl.
rewrite (involutive (st v)).
rewrite -(involutive (dual_stype (st v))).
split=> //.
- iSplit=> //.
iPureIntro.
by eapply st_eval_send.
iDestruct (stype_equivI with "Heval") as "Heval".
destruct stl.
+ iDestruct "Heq'" as %Heq'. inversion Heq'.
+ destruct str.
* simpl. iApply "Heval".
* simpl.
iDestruct "Heq'" as (Ha) "[HPeq Hsteq]".
iDestruct "Heval" as (Ha') "[HPeq' Hsteq']".
subst. simpl.
iSpecialize ("HPeq" $!v).
iSpecialize ("HPeq'" $!v).
iSplitL "HPeq' HP".
iRewrite "HPeq'". iRewrite "HPeq". iApply "HP".
iSpecialize ("Hsteq" $!v).
iSpecialize ("Hsteq'" $!v).
iRewrite "Hsteq'". iRewrite "Hsteq".
rewrite (involutive (st v)).
done.
+ simpl. destruct stl.
* iDestruct "Heq'" as %Heq'. inversion Heq'.
* iDestruct "Heq'" as (Ha) "Heq'".
rewrite Ha.
iDestruct "Heval" as %Heval. inversion Heval.
}
iModIntro. iFrame "Hcctx ∗ Hinv".
Qed.
- admit. (* Converse case *)
Admitted.
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 :
......
From iris.heap_lang Require Export lang.
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.
......@@ -102,9 +109,7 @@ Section stype_ofe.
Proof.
intros n. induction 1 as [| a P1 P2 st1 st2 HP Hst IH].
- constructor.
- destruct a.
+ constructor. apply HP. intros v. apply IH.
+ constructor. apply HP. intros v. apply IH.
- constructor. apply HP. intros v. apply IH.
Qed.
Global Instance dual_stype_proper : Proper (() ==> ()) dual_stype.
Proof. apply (ne_proper _). Qed.
......@@ -114,11 +119,40 @@ Section stype_ofe.
intros st.
induction st.
- constructor.
- simpl. destruct a.
+ constructor. reflexivity. intros v. apply H.
+ constructor. reflexivity. intros v. apply H.
- 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.
- intros Heq.
destruct st1, st2.
+ constructor.
+ inversion Heq.
+ inversion Heq.
+ inversion Heq; subst.
repeat split; eauto.
- intros Heq.
destruct st1, st2.
+ constructor.
+ inversion Heq.
+ inversion Heq.
+ inversion Heq; subst.
rewrite H.
constructor.
apply H0. apply Heq.
Qed.
End stype_ofe.
Arguments stypeC : clear implicits.
Fixpoint stype_map {A B} (f : A B) (st : stype A) : stype B :=
match st with
......@@ -187,3 +221,4 @@ Instance stypeCF_contractive F :
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_contractive.
Qed.
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