Commit f5481a10 authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify protocol interpretation to use equality with tail.

parent 585379fb
Pipeline #20569 failed with stage
in 0 seconds
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [ depends: [
"coq-iris" { (= "dev.2019-10-14.0.1f83451a") | (= "dev") } "coq-iris" { (= "dev.2019-10-25.0.bbd38120") | (= "dev") }
] ]
...@@ -193,12 +193,15 @@ Instance: Params (@iProto_app) 1 := {}. ...@@ -193,12 +193,15 @@ Instance: Params (@iProto_app) 1 := {}.
Infix "<++>" := iProto_app (at level 60) : proto_scope. Infix "<++>" := iProto_app (at level 60) : proto_scope.
(** * Auxiliary definitions and invariants *) (** * Auxiliary definitions and invariants *)
Definition proto_eq_next {Σ} (p : iProto Σ) : laterO (iProto Σ) -n> iPropO Σ :=
OfeMor (sbi_internal_eq (Next p)).
Fixpoint proto_interp `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ := Fixpoint proto_interp `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
match vs with match vs with
| [] => p1 iProto_dual p2 | [] => iProto_dual p1 p2
| v :: vs => pc p2', | v :: vs => pc p2',
p2 (proto_message Receive pc)%proto p2 proto_message Receive pc
( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p2') - pc v f) pc v (proto_eq_next p2')
proto_interp vs p1 p2' proto_interp vs p1 p2'
end%I. end%I.
Arguments proto_interp {_ _} _ _%proto _%proto : simpl nomatch. Arguments proto_interp {_ _} _ _%proto _%proto : simpl nomatch.
...@@ -416,32 +419,40 @@ Section proto. ...@@ -416,32 +419,40 @@ Section proto.
by rewrite own_op. by rewrite own_op.
Qed. Qed.
Lemma proto_eq_next_dual p :
ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid (proto_eq_next (iProto_dual p))
proto_eq_next p.
Proof.
intros lp. iSplit; iIntros "Hlp /="; last by iRewrite -"Hlp".
destruct (Next_uninj lp) as [p' ->].
rewrite /later_map /= !bi.later_equivI. iNext.
rewrite -{2}(involutive iProto_dual p) -{2}(involutive iProto_dual p').
by iRewrite "Hlp".
Qed.
Lemma proto_interp_send v vs pc p1 p2 : Lemma proto_interp_send v vs pc p1 p2 :
proto_interp vs (proto_message Send pc) p2 - proto_interp vs (proto_message Send pc) p2 -
( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p1) - pc v f) - pc v (proto_eq_next p1) -
proto_interp (vs ++ [v]) p1 p2. proto_interp (vs ++ [v]) p1 p2.
Proof. Proof.
iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl. iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
- iDestruct "Heval" as "#Heval". - iDestruct "Heval" as "#Heval".
iExists _, (iProto_dual p1). iSplit. iExists _, (iProto_dual p1). iSplit.
{ rewrite -{2}(involutive iProto_dual p2). iRewrite -"Heval". { iRewrite -"Heval". by rewrite /iProto_dual proto_map_message. }
rewrite /iProto_dual. by rewrite proto_map_message. } rewrite /= proto_eq_next_dual; auto.
iSplit.
{ iIntros (f) "Hf /=". by iApply "Hc". }
by rewrite involutive.
- iDestruct "Heval" as (pc' p2') "(Heq & Hc' & Heval)". - iDestruct "Heval" as (pc' p2') "(Heq & Hc' & Heval)".
iExists pc', p2'. iFrame "Heq Hc'". iNext. iApply ("IH" with "Heval Hc"). iExists pc', p2'. iFrame "Heq Hc'". iNext. iApply ("IH" with "Heval Hc").
Qed. Qed.
Lemma proto_interp_recv v vs p1 pc : Lemma proto_interp_recv v vs p1 pc :
proto_interp (v :: vs) p1 (proto_message Receive pc) - p2, proto_interp (v :: vs) p1 (proto_message Receive pc) - p2,
( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p2) - pc v f) pc v (proto_eq_next p2)
proto_interp vs p1 p2. proto_interp vs p1 p2.
Proof. Proof.
simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2". simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2".
iDestruct (@proto_message_equivI with "Heq") as "[_ Heq]". iDestruct (@proto_message_equivI with "Heq") as "[_ Heq]".
iSpecialize ("Heq" $! v). rewrite bi.ofe_morO_equivI. iSpecialize ("Heq" $! v). rewrite bi.ofe_morO_equivI.
iIntros (f) "Hfp2". iRewrite ("Heq" $! f). by iApply "Hc". by iRewrite ("Heq" $! (proto_eq_next p2)).
Qed. Qed.
Lemma proto_interp_False p pc v vs : Lemma proto_interp_False p pc v vs :
...@@ -452,7 +463,7 @@ Section proto. ...@@ -452,7 +463,7 @@ Section proto.
Qed. Qed.
Lemma proto_interp_nil p1 p2 : proto_interp [] p1 p2 - p1 iProto_dual p2. Lemma proto_interp_nil p1 p2 : proto_interp [] p1 p2 - p1 iProto_dual p2.
Proof. done. Qed. Proof. iIntros "#H /=". iRewrite -"H". by rewrite involutive. Qed.
Arguments proto_interp : simpl never. Arguments proto_interp : simpl never.
...@@ -505,14 +516,13 @@ Section proto. ...@@ -505,14 +516,13 @@ Section proto.
{ iNext. iExists _,_,_,_. iFrame "Hcrf Hstra Hstla Hclf". iLeft. { iNext. iExists _,_,_,_. iFrame "Hcrf Hstra Hstla Hclf". iLeft.
iRewrite "Heq" in "Hinv'". iRewrite "Heq" in "Hinv'".
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]". iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
{ iSplit=> //. iApply (proto_interp_send with "Heval [HP]"). { iSplit=> //. iApply (proto_interp_send with "Heval [HP]"); simpl.
iIntros (f) "Hf /=". iExists x. by iFrame. } iExists x. by iFrame. }
destruct r as [|vr r]; last first. destruct r as [|vr r]; last first.
{ iDestruct (proto_interp_False with "Heval") as %[]. } { iDestruct (proto_interp_False with "Heval") as %[]. }
iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval"). iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval").
iApply (proto_interp_send _ [] with "[] [HP]"). iApply (proto_interp_send _ [] with "[//] [HP]").
{ by rewrite /proto_interp involutive. } iExists x. by iFrame. }
iIntros (f) "Hf /=". iExists x. by iFrame. }
iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ. iFrame; auto. iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ. iFrame; auto.
- iExists _. - iExists _.
iIntros "{$Hcrf} !>" (x) "HP Hcrf". iIntros "{$Hcrf} !>" (x) "HP Hcrf".
...@@ -524,14 +534,13 @@ Section proto. ...@@ -524,14 +534,13 @@ Section proto.
{ iNext. iExists _, _, _, _. iFrame "Hcrf Hstra Hstla Hclf". iRight. { iNext. iExists _, _, _, _. iFrame "Hcrf Hstra Hstla Hclf". iRight.
iRewrite "Heq" in "Hinv'". iRewrite "Heq" in "Hinv'".
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last first. iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last first.
{ iSplit=> //. iApply (proto_interp_send with "Heval [HP]"). { iSplit=> //. iApply (proto_interp_send with "Heval [HP]"); simpl.
iIntros (f) "Hf /=". iExists x. by iFrame. } iExists x. by iFrame. }
destruct l as [|vl l]; last first. destruct l as [|vl l]; last first.
{ iDestruct (proto_interp_False with "Heval") as %[]. } { iDestruct (proto_interp_False with "Heval") as %[]. }
iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval"). iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval").
iApply (proto_interp_send _ [] with "[] [HP]"). iApply (proto_interp_send _ [] with "[//] [HP]").
{ by rewrite /proto_interp involutive. } iExists x. by iFrame. }
iIntros (f) "Hf /=". iExists x. by iFrame. }
iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ. iFrame; auto. iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ. iFrame; auto.
Qed. Qed.
...@@ -574,14 +583,10 @@ Section proto. ...@@ -574,14 +583,10 @@ Section proto.
iMod (proto_own_auth_update _ _ _ _ q with "Hstla Hstlf") as "[Hstla Hstlf]". iMod (proto_own_auth_update _ _ _ _ q with "Hstla Hstlf") as "[Hstla Hstlf]".
iMod ("Hclose" with "[-Hstlf Hf]") as %_. iMod ("Hclose" with "[-Hstlf Hf]") as %_.
{ iExists _, _,_ ,_. eauto 10 with iFrame. } { iExists _, _,_ ,_. eauto 10 with iFrame. }
iIntros "!> !>". iIntros "!> !> /=".
set (f lp := ( q, lp Next q c1 q)%I). iDestruct "Hf" as (x) "(Hv & HP & #Hf) /=".
assert (NonExpansive f) by solve_proper. iNext. iExists x. iFrame "Hv HP". iRewrite -"Hf".
iDestruct ("Hf" $! (OfeMor f) with "[Hstlf]") as (x) "(Hv & HP & Hf) /=". rewrite mapsto_proto_eq. iExists Left, c1, c2, γ. iFrame; auto.
{ iExists q. iSplit; first done. rewrite mapsto_proto_eq.
iExists Left, c1, c2, γ. iFrame; auto. }
iDestruct "Hf" as (q') "[#Hq Hc]". iModIntro.
iExists x. iFrame "Hv HP". by iRewrite "Hq".
- iIntros "{$Hclf} !>". - iIntros "{$Hclf} !>".
iRename "Hstf" into "Hstrf". iRename "Hstf" into "Hstrf".
iDestruct (proto_own_auth_agree with "Hstra Hstrf") as "#Heq". iDestruct (proto_own_auth_agree with "Hstra Hstrf") as "#Heq".
...@@ -601,13 +606,9 @@ Section proto. ...@@ -601,13 +606,9 @@ Section proto.
iMod ("Hclose" with "[-Hstrf Hf]") as %_. iMod ("Hclose" with "[-Hstrf Hf]") as %_.
{ iExists _, _, _, _. eauto 10 with iFrame. } { iExists _, _, _, _. eauto 10 with iFrame. }
iIntros "!> !>". iIntros "!> !>".
set (f lp := ( q, lp Next q c2 q)%I). iDestruct "Hf" as (x) "(Hv & HP & Hf) /=".
assert (NonExpansive f) by solve_proper. iNext. iExists x. iFrame "Hv HP". iRewrite -"Hf".
iDestruct ("Hf" $! (OfeMor f) with "[Hstrf]") as (x) "(Hv & HP & Hf) /=". rewrite mapsto_proto_eq. iExists Right, c1, c2, γ. iFrame; auto.
{ iExists q. iSplit; first done. rewrite mapsto_proto_eq.
iExists Right, c1, c2, γ. iFrame; auto. }
iDestruct "Hf" as (q') "[#Hq Hc]". iModIntro.
iExists x. iFrame "Hv HP". by iRewrite "Hq".
Qed. Qed.
(** ** Specifications of [send] and [receive] *) (** ** Specifications of [send] and [receive] *)
......
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