sort_br_del.v 4.2 KB
Newer Older
1
2
(** This file implements a looping distributed Merge Sort,
a specification thereof and its proofs. *)
jihgfee's avatar
jihgfee committed
3
From stdpp Require Import sorting.
4
From actris.channel Require Import proto_channel proofmode.
jihgfee's avatar
jihgfee committed
5
From iris.heap_lang Require Import proofmode notation.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
From actris.examples Require Import sort.
jihgfee's avatar
jihgfee committed
7

8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
25
    else if: recv "c" then
26
27
      send "c" (start_chan (λ: "c", "go" "cmp" "c"));;
      "go" "cmp" "c"
jihgfee's avatar
jihgfee committed
28
29
    else #().

30
Section sort_service_br_del.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  Context `{!heapG Σ, !proto_chanG Σ}.
32
33
34
35
36
37
38
39
40
41
42
43
44
  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
45
    {{{ c  iProto_dual sort_protocol_br }}}
46
      sort_service_br cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
47
    {{{ RET #(); c  END }}}.
48
49
50
51
52
53
54
55
56
  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
57
    ((<?> c, MSG c {{ c  sort_protocol I R }}; rec) <+> END)%proto.
58
59
60
61
62
63
  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
64

65
66
  Lemma sort_protocol_del_spec cmp c :
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
67
    {{{ c  iProto_dual sort_protocol_del }}}
68
      sort_service_del cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
69
    {{{ RET #(); c  END }}}.
70
71
72
  Proof.
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
    wp_rec. wp_branch; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
    { wp_apply (start_chan_proto_spec (sort_protocol I R <++> END)%proto);
74
75
76
77
78
        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
79

80
  Definition sort_protocol_br_del_aux (rec : iProto Σ) : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
81
    ((sort_protocol I R <++> rec) <+> ((<?> c, MSG c {{ c  rec }}; rec) <+> END))%proto.
82
  Instance sort_protocol_br_del_aux_contractive : Contractive sort_protocol_br_del_aux.
83
  Proof. solve_proto_contractive. Qed.
84
85
86
87
88
89
90
  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
91
    {{{ c  iProto_dual sort_protocol_br_del }}}
92
      sort_service_br_del cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    {{{ RET #(); c  END }}}.
jihgfee's avatar
jihgfee committed
94
  Proof.
95
96
97
98
99
    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
100
    { wp_apply (start_chan_proto_spec sort_protocol_br_del); iIntros (c') "Hc'".
101
102
      { wp_apply ("IH" with "Hc'"); auto. }
      wp_send with "[$Hc']".
jihgfee's avatar
jihgfee committed
103
      by wp_apply ("IH" with "Hc"). }
104
    by iApply "HΨ".
jihgfee's avatar
jihgfee committed
105
  Qed.
106
End sort_service_br_del.