sort_br_del.v 4.1 KB
Newer Older
jihgfee's avatar
jihgfee committed
1
From stdpp Require Import sorting.
2
From actris.channel Require Import proto_channel proofmode.
jihgfee's avatar
jihgfee committed
3
From iris.heap_lang Require Import proofmode notation.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From actris.examples Require Import sort.
jihgfee's avatar
jihgfee committed
5

6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
Definition sort_service_br : val :=
  rec: "go" "cmp" "c" :=
    if: ~recv "c" then #() else
    sort_service "cmp" "c";;
    "go" "cmp" "c".

Definition sort_service_del : val :=
  rec: "go" "cmp" "c" :=
    if: ~recv "c" then #() else
    send "c" (start_chan (λ: "c", sort_service "cmp" "c"));;
    "go" "cmp" "c".

Definition sort_service_br_del : val :=
  rec: "go" "cmp" "c" :=
    if: recv "c" then
      sort_service "cmp" "c";;
      "go" "cmp" "c"
jihgfee's avatar
jihgfee committed
23
    else if: recv "c" then
24 25
      send "c" (start_chan (λ: "c", "go" "cmp" "c"));;
      "go" "cmp" "c"
jihgfee's avatar
jihgfee committed
26 27
    else #().

28
Section sort_service_br_del.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  Context `{!heapG Σ, !proto_chanG Σ}.
30 31 32 33 34 35 36 37 38 39 40 41 42
  Context {A} (I : A  val  iProp Σ) (R : A  A  Prop) `{!RelDecision R, !Total R}.

  Definition sort_protocol_br_aux (rec : iProto Σ) : iProto Σ :=
    ((sort_protocol I R <++> rec) <+> END)%proto.
  Instance sort_protocol_br_aux_contractive : Contractive sort_protocol_br_aux.
  Proof. solve_proto_contractive. Qed.
  Definition sort_protocol_br : iProto Σ := fixpoint sort_protocol_br_aux.
  Global Instance sort_protocol_br_unfold :
    ProtoUnfold sort_protocol_br (sort_protocol_br_aux sort_protocol_br).
  Proof. apply proto_unfold_eq, (fixpoint_unfold sort_protocol_br_aux). Qed.

  Lemma sort_service_br_spec cmp c :
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
43
    {{{ c  iProto_dual sort_protocol_br }}}
44
      sort_service_br cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
45
    {{{ RET #(); c  END }}}.
46 47 48 49 50 51 52 53 54
  Proof.
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
    wp_rec. wp_branch; wp_pures.
    { wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
      by wp_apply ("IH" with "Hc"). }
    by iApply "HΨ".
  Qed.

  Definition sort_protocol_del_aux (rec : iProto Σ) : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
55
    ((<?> c, MSG c {{ c  sort_protocol I R }}; rec) <+> END)%proto.
56 57 58 59 60 61
  Instance sort_protocol_del_aux_contractive : Contractive sort_protocol_del_aux.
  Proof. solve_proto_contractive. Qed.
  Definition sort_protocol_del : iProto Σ := fixpoint sort_protocol_del_aux.
  Global Instance sort_protocol_del_unfold :
    ProtoUnfold sort_protocol_del (sort_protocol_del_aux sort_protocol_del).
  Proof. apply proto_unfold_eq, (fixpoint_unfold sort_protocol_del_aux). Qed.
jihgfee's avatar
jihgfee committed
62

63 64
  Lemma sort_protocol_del_spec cmp c :
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
65
    {{{ c  iProto_dual sort_protocol_del }}}
66
      sort_service_del cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
67
    {{{ RET #(); c  END }}}.
68 69 70
  Proof.
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
    wp_rec. wp_branch; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
    { wp_apply (start_chan_proto_spec (sort_protocol I R <++> END)%proto);
72 73 74 75 76
        iIntros (c') "Hc'".
      { wp_pures. wp_apply (sort_service_spec with "Hcmp Hc'"); auto. }
      wp_send with "[$Hc']". by wp_apply ("IH" with "Hc"). }
    by iApply "HΨ".
  Qed.
jihgfee's avatar
jihgfee committed
77

78
  Definition sort_protocol_br_del_aux (rec : iProto Σ) : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
79
    ((sort_protocol I R <++> rec) <+> ((<?> c, MSG c {{ c  rec }}; rec) <+> END))%proto.
80
  Instance sort_protocol_br_del_aux_contractive : Contractive sort_protocol_br_del_aux.
81
  Proof. solve_proto_contractive. Qed.
82 83 84 85 86 87 88
  Definition sort_protocol_br_del : iProto Σ := fixpoint sort_protocol_br_del_aux.
  Global Instance sort_protocol_br_del_unfold :
    ProtoUnfold sort_protocol_br_del (sort_protocol_br_del_aux sort_protocol_br_del).
  Proof. apply proto_unfold_eq, (fixpoint_unfold sort_protocol_br_del_aux). Qed.

  Lemma sort_service_br_del_spec cmp c :
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
89
    {{{ c  iProto_dual sort_protocol_br_del }}}
90
      sort_service_br_del cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    {{{ RET #(); c  END }}}.
jihgfee's avatar
jihgfee committed
92
  Proof.
93 94 95 96 97
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
    wp_rec. wp_branch; wp_pures.
    { wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
      by wp_apply ("IH" with "Hc"). }
    wp_branch; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
    { wp_apply (start_chan_proto_spec sort_protocol_br_del); iIntros (c') "Hc'".
99 100
      { wp_apply ("IH" with "Hc'"); auto. }
      wp_send with "[$Hc']".
jihgfee's avatar
jihgfee committed
101
      by wp_apply ("IH" with "Hc"). }
102
    by iApply "HΨ".
jihgfee's avatar
jihgfee committed
103
  Qed.
104
End sort_service_br_del.