Commit 83692823 authored by Robbert Krebbers's avatar Robbert Krebbers

Restore branching.

Also weaken some specs by adding laters.
parent d9b0b2c4
......@@ -6,7 +6,6 @@ theories/utils/list.v
theories/channel/channel.v
theories/channel/proto_model.v
theories/channel/proto_channel.v
theories/channel/branching.v
theories/examples/proofs_enc.v
theories/examples/branching_proofs.v
theories/examples/list_sort.v
From iris.heap_lang Require Import proofmode notation.
From osiris.channel Require Export proto_channel.
Definition TSB {PROP : bi} (a : action)
(prot1 prot2 : proto val PROP) : proto val PROP :=
TSR' a (λ _, True)%I (λ v, if v : bool then prot1 else prot2).
Global Typeclasses Opaque TSB.
Infix "<+>" := (TSB Send) (at level 85) : proto_scope.
Infix "<&>" := (TSB Receive) (at level 85) : proto_scope.
Definition select : val := λ: "c" "s" "b", send "c" "s" "b".
Definition branch : val := λ: "c" "s" "b1" "b2",
if: recv "c" "s" then "b1" else "b2".
(* TODO: This notation should be fixed *)
Notation "'branch:' c @ s 'left' e1 'right' e2" :=
(branch c s (λ: <>, e1)%E (λ: <>, e2)%E #())
(at level 200, c, s, e1, e2 at level 200) : expr_scope.
Global Instance is_dual_tsb {PROP : bi} a1 a2
(proto1 proto1' proto2 proto2' : proto val PROP) :
IsDualAction a1 a2
IsDualProto proto1 proto1' IsDualProto proto2 proto2'
IsDualProto (TSB a1 proto1 proto2) (TSB a2 proto1' proto2').
Proof.
rewrite /IsDualAction.
rewrite /IsDualProto.
intros Ha Hst1 Hst2.
destruct a1.
- simpl.
simpl in Ha. rewrite -Ha.
rewrite -(proto_force_eq (dual_proto _)).
constructor.
f_equiv.
f_equiv.
destruct (val_decode a).
by destruct b. apply is_dual_end.
- simpl.
simpl in Ha. rewrite -Ha.
rewrite -(proto_force_eq (dual_proto _)).
constructor.
f_equiv.
f_equiv.
destruct (val_decode a).
by destruct b.
apply is_dual_end.
Qed.
Section branching_specs.
Context `{!heapG Σ, !logrelG val Σ} (N : namespace).
Lemma select_st_spec proto1 proto2 γ c s (b : side) :
{{{ c @ s : proto1 <+> proto2 {N,γ} }}}
select c #s #b
{{{ RET #(); c @ s : (if b then proto1 else proto2) {N,γ} }}}.
Proof.
iIntros (Φ) "Hproto HΦ".
wp_pures. wp_lam.
wp_pures. rewrite /TSB.
wp_apply (send_st_spec (A:=bool) with "[$Hproto //]"); iIntros "Hstl".
iApply "HΦ". by destruct b.
Qed.
Lemma branch_st_spec proto1 proto2 γ c s (b1 b2 : val) :
{{{ c @ s : proto1 <&> proto2 {N,γ} }}}
branch c #s b1 b2
{{{ v, RET v; (v = b1%V c @ s : proto1 {N,γ})
(v = b2%V c @ s : proto2 {N,γ})}}}.
Proof.
iIntros (Φ').
iIntros "Hproto HΦ'".
wp_pures.
wp_lam. rewrite /TSB. simpl.
wp_apply (recv_st_spec (A:=bool) with "[$Hproto //]").
iIntros ([]) "[Hstl _]".
- wp_pures. iApply ("HΦ'"). eauto with iFrame.
- wp_pures. iApply ("HΦ'"). eauto with iFrame.
Qed.
End branching_specs.
......@@ -53,6 +53,7 @@ Notation "'MSG' v {{ P }}; p" :=
Notation "'MSG' v ; p" :=
(proto_payload v True p) (at level 20, v at level 20, p at level 200) : proto_cont_scope.
(** Dual *)
Definition proto_dual {Σ} (p : iProto Σ) : iProto Σ :=
proto_map action_dual cid cid p.
Arguments proto_dual {_} _%proto.
......@@ -68,6 +69,13 @@ Class IsProtoDual {Σ} (p1 p2 : iProto Σ) :=
Class IsProtoContDual {Σ X} (pc1 pc2 : iProto_cont Σ X) :=
is_dual_proto_cont x : prod_map id proto_dual (tele_app pc1 x) tele_app pc2 x.
(** Branching *)
Definition iProto_branch {Σ} (a : action)(p1 p2 : iProto Σ) : iProto Σ :=
iProto_message a ( b : bool, MSG #b {{ True }}; if b then p1 else p2).
Typeclasses Opaque iProto_branch.
Infix "<+>" := (iProto_branch Send) (at level 85) : proto_scope.
Infix "<&>" := (iProto_branch Receive) (at level 85) : proto_scope.
(** Invariants *)
Fixpoint proto_eval `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
match vs with
......@@ -167,6 +175,14 @@ Section proto.
apply tforall_forall. apply Hpc.
Qed.
Global Instance is_proto_dual_branch a1 a2 (p1 p2 p1' p2' : iProto Σ) :
IsActionDual a1 a2 IsProtoDual p1 p1' IsProtoDual p2 p2'
IsProtoDual (iProto_branch a1 p1 p2) (iProto_branch a2 p1' p2').
Proof.
intros. apply is_proto_dual_message,
is_proto_cont_dual_exist; last (intros []); apply _.
Qed.
Global Instance proto_eval_ne : NonExpansive2 (proto_eval vs).
Proof. induction vs; solve_proper. Qed.
Global Instance proto_eval_proper vs : Proper (() ==> () ==> ()) (proto_eval vs).
......@@ -423,7 +439,7 @@ Section proto.
(.. x : X,
v = (tele_app pc x).1.1
(tele_app pc x).1.2
(c (tele_app pc x).2 @ N - Ψ #())) -
(c (tele_app pc x).2 @ N - Ψ #())) -
WP send c v {{ Ψ }}.
Proof.
iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΨ]".
......@@ -464,12 +480,31 @@ Section proto.
Lemma recv_proto_spec {X} Ψ c (pc : iProto_cont Σ X) :
c <?> pc @ N -
(.. x : X, c (tele_app pc x).2 @ N -
(tele_app pc x).1.2 - Ψ (tele_app pc x).1.1) -
(.. x : X, c (tele_app pc x).2 @ N -
(tele_app pc x).1.2 - Ψ (tele_app pc x).1.1) -
WP recv c {{ Ψ }}.
Proof.
iIntros "Hc H". iApply (recv_proto_spec_packed with "[$]").
iIntros "!>" (x) "[Hc HP]". iDestruct (bi_tforall_forall with "H") as "H".
iApply ("H" with "[$] [$]").
Qed.
Lemma select_spec c b p1 p2 :
{{{ c p1 <+> p2 @ N }}}
send c #b
{{{ RET #(); c (if b : bool then p1 else p2) @ N }}}.
Proof.
rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
Qed.
Lemma branch_spec c p1 p2 :
{{{ c p1 <&> p2 @ N }}}
recv c
{{{ b, RET #b; c if b : bool then p1 else p2 @ N }}}.
Proof.
rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
iApply (recv_proto_spec with "Hc"); simpl.
iIntros "!>" (b) "Hc _". by iApply "HΨ".
Qed.
End proto.
......@@ -123,13 +123,13 @@ Section list_sort.
wp_apply (wp_fork with "[Hcz1]").
{ iNext. wp_apply ("IH" with "Hcz1"); auto. }
wp_apply (send_proto_spec with "Hcy2"); simpl.
iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} Hcy2".
iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcy2".
wp_apply (send_proto_spec with "Hcy2"); simpl.
iExists xs1, l1, vs1. iSplit; first done. iIntros "{$Hl1 $HI1} Hcy2".
iExists xs1, l1, vs1. iSplit; first done. iIntros "{$Hl1 $HI1} !> Hcy2".
wp_apply (send_proto_spec with "Hcz2"); simpl.
iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} Hcz2".
iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcz2".
wp_apply (send_proto_spec with "Hcz2"); simpl.
iExists xs2, l2, vs2. iSplit; first done. iIntros "{$Hl2 $HI2} Hcz2".
iExists xs2, l2, vs2. iSplit; first done. iIntros "{$Hl2 $HI2} !> Hcz2".
wp_apply (recv_proto_spec with "Hcy2"); simpl.
iIntros (ys1 ws1) "_". iDestruct 1 as (??) "[Hl1 HI1]".
wp_apply (recv_proto_spec with "Hcz2"); simpl.
......
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