sort_fg.v 9.43 KB
Newer Older
jihgfee's avatar
jihgfee committed
1
From stdpp Require Import sorting.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From actris.channel Require Import proto_channel proofmode.
jihgfee's avatar
jihgfee committed
3 4
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
5
From actris.utils Require Import compare.
jihgfee's avatar
jihgfee committed
6

jihgfee's avatar
jihgfee committed
7 8 9
Definition cont := true.
Definition stop := false.

10
Definition sort_service_fg_split : val :=
jihgfee's avatar
jihgfee committed
11
  rec: "go" "c" "c1" "c2" :=
12 13 14 15
    if: ~(recv "c") then send "c1" #stop;; send "c2" #stop else
    let: "x" := recv "c" in
    send "c1" #cont;; send "c1" "x";;
    "go" "c" "c2" "c1".
jihgfee's avatar
jihgfee committed
16

17
Definition sort_service_fg_move : val :=
jihgfee's avatar
jihgfee committed
18
  rec: "go" "c" "cin" :=
19 20 21 22
    if: ~(recv "cin") then send "c" #stop else
    let: "x" := recv "cin" in
    send "c" #cont;; send "c" "x";;
    "go" "c" "cin".
jihgfee's avatar
jihgfee committed
23

24
Definition sort_service_fg_merge : val :=
25 26 27
  rec: "go" "cmp" "c" "x1" "c1" "c2" :=
    if: ~recv "c2" then
      send "c" #cont;; send "c" "x1";;
28
      sort_service_fg_move "c" "c1"
29 30 31 32 33 34
    else
      let: "x2" := recv "c2" in
      if: "cmp" "x1" "x2" then
        send "c" #cont;; send "c" "x1";; "go" "cmp" "c" "x2" "c2" "c1"
      else
        send "c" #cont;; send "c" "x2";; "go" "cmp" "c" "x1" "c1" "c2".
jihgfee's avatar
jihgfee committed
35

36
Definition sort_service_fg : val :=
37 38 39 40 41
  rec: "go" "cmp" "c" :=
    if: ~(recv "c") then send "c" #stop else
    let: "x" := recv "c" in
    if: ~(recv "c") then send "c" #cont;; send "c" "x";; send "c" #stop else
    let: "y" := recv "c" in
42 43
    let: "c1" := start_chan (λ: "c", "go" "cmp" "c") in
    let: "c2" := start_chan (λ: "c", "go" "cmp" "c") in
44 45
    send "c1" #cont;; send "c1" "x";;
    send "c2" #cont;; send "c2" "y";;
46
    sort_service_fg_split "c" "c1" "c2";;
47
    let: "x" := (if: recv "c1" then recv "c1" else assert #false) in
48
    sort_service_fg_merge "cmp" "c" "x" "c1" "c2".
49

50
Definition sort_service_fg_func : val := λ: "c",
51
  let: "cmp" := recv "c" in
52
  sort_service_fg "cmp" "c".
53

54
Section sort_fg.
jihgfee's avatar
jihgfee committed
55
  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
56

57
  Section sort_fg_inner.
58
  Context {A} (I : A  val  iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
jihgfee's avatar
jihgfee committed
59

60
  Definition sort_fg_tail_protocol_aux (xs : list A)
61 62
      (rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ ys,
    ((<?> y v, MSG v {{  TlRel R y ys   I y v }}; (rec : _  iProto Σ) (ys ++ [y]))
63
     <&{ ys  xs }> END)%proto.
jihgfee's avatar
jihgfee committed
64

65 66
  Instance sort_fg_tail_protocol_aux_contractive xs :
    Contractive (sort_fg_tail_protocol_aux xs).
67
  Proof. solve_proto_contractive. Qed.
68 69 70 71 72 73 74 75
  Definition sort_fg_tail_protocol (xs : list A) : list A  iProto Σ :=
    fixpoint (sort_fg_tail_protocol_aux xs).
  Global Instance sort_fg_tail_protocol_unfold xs ys :
    ProtoUnfold (sort_fg_tail_protocol xs ys)
      (sort_fg_tail_protocol_aux xs (sort_fg_tail_protocol xs) ys).
  Proof. apply proto_unfold_eq, (fixpoint_unfold (sort_fg_tail_protocol_aux _)). Qed.

  Definition sort_fg_head_protocol_aux
76 77
      (rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ xs,
    ((<!> x v, MSG v {{ I x v }}; (rec : _  iProto Σ) (xs ++ [x]))
78
     <+> sort_fg_tail_protocol xs [])%proto.
79

80 81
  Instance sort_fg_head_protocol_aux_contractive :
    Contractive sort_fg_head_protocol_aux.
82
  Proof. solve_proto_contractive. Qed.
83

84 85 86 87 88 89
  Definition sort_fg_head_protocol : list A  iProto Σ :=
    fixpoint sort_fg_head_protocol_aux.
  Global Instance sort_fg_head_protocol_unfold xs :
    ProtoUnfold (sort_fg_head_protocol xs)
      (sort_fg_head_protocol_aux sort_fg_head_protocol xs).
  Proof. apply proto_unfold_eq, (fixpoint_unfold sort_fg_head_protocol_aux). Qed.
jihgfee's avatar
jihgfee committed
90

91
  Definition sort_fg_protocol : iProto Σ := sort_fg_head_protocol [].
92

93
  Lemma sort_service_fg_split_spec c p c1 c2 xs xs1 xs2 :
jihgfee's avatar
jihgfee committed
94
    {{{
95 96
      c  iProto_dual (sort_fg_head_protocol xs) <++> p @ N 
      c1  sort_fg_head_protocol xs1 @ N  c2  sort_fg_head_protocol xs2 @ N
97
    }}}
98
      sort_service_fg_split c c1 c2
jihgfee's avatar
jihgfee committed
99
    {{{ xs' xs1' xs2', RET #();
100
      xs'  xs1' ++ xs2' 
101 102 103
      c  iProto_dual (sort_fg_tail_protocol (xs ++ xs') []) <++> p @ N 
      c1  sort_fg_tail_protocol (xs1 ++ xs1') [] @ N 
      c2  sort_fg_tail_protocol (xs2 ++ xs2') [] @ N
104
    }}}.
jihgfee's avatar
jihgfee committed
105 106
  Proof.
    iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
107
    wp_rec. wp_branch.
108
    - wp_recv (x v) as "HI". wp_select. wp_send with "[$HI]".
109 110 111 112
      wp_apply ("IH" with "Hc Hc2 Hc1").
      iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hc2 & Hc1)".
      rewrite -!(assoc_L (++)).
      iApply "HΨ". iFrame "Hc Hc1 Hc2". by rewrite Hxs' (comm (++) xs1') assoc_L.
113
    - wp_select. wp_select.
114
      iApply ("HΨ" $! [] [] []). rewrite !right_id_L. by iFrame.
jihgfee's avatar
jihgfee committed
115
  Qed.
jihgfee's avatar
jihgfee committed
116

117
  Lemma sort_service_fg_move_spec c p cin xs ys zs xs' ys' :
118 119
    xs  xs' ++ zs 
    ys  ys' ++ zs 
120 121
    Sorted R ys 
    ( x, TlRel R x ys'  TlRel R x ys) 
jihgfee's avatar
jihgfee committed
122
    {{{
123 124
      c  iProto_dual (sort_fg_tail_protocol xs ys) <++> p @ N 
      cin  sort_fg_tail_protocol xs' ys' @ N
jihgfee's avatar
jihgfee committed
125
    }}}
126
      sort_service_fg_move c cin
127
    {{{ RET #(); c  p @ N  cin  END @ N }}}.
jihgfee's avatar
jihgfee committed
128
  Proof.
129 130
    iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
    iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
131
    wp_rec. wp_branch as %_ | %Hys'.
132 133
    - wp_recv (x v) as (Htl) "HI".
      wp_select. wp_send with "[$HI]"; first by auto.
134
      wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
135 136
      * done.
      * by rewrite Hys -!assoc_L (comm _ zs).
137 138
      * auto using Sorted_snoc.
      * intros x'.
139
        inversion 1; discriminate_list || simplify_list_eq. by constructor.
140
    - wp_select with "[]".
141 142
      { by rewrite /= Hys Hxs Hys'. }
      iApply "HΨ". iFrame.
jihgfee's avatar
jihgfee committed
143
  Qed.
144

145
  Lemma sort_service_fg_merge_spec cmp c p c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147
    xs  xs1 ++ xs2 
    ys  ys1 ++ ys2 
148 149 150
    Sorted R ys 
    TlRel R y1 ys 
    ( x, TlRel R x ys2  R x y1  TlRel R x ys) 
151
    cmp_spec I R cmp -
jihgfee's avatar
jihgfee committed
152
    {{{
153 154 155
      c  iProto_dual (sort_fg_tail_protocol xs ys) <++> p @ N 
      c1  sort_fg_tail_protocol xs1 (ys1 ++ [y1]) @ N 
      c2  sort_fg_tail_protocol xs2 ys2 @ N 
156
      I y1 w1
Robbert Krebbers's avatar
Robbert Krebbers committed
157
    }}}
158
      sort_service_fg_merge cmp c w1 c1 c2
159
    {{{ RET #(); c  p @ N }}}.
jihgfee's avatar
jihgfee committed
160
  Proof.
161 162 163
    iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
    iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
    iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
164
    wp_rec. wp_branch as %_ | %Hys2.
165
    - wp_recv (x v) as (Htl2) "HIx".
166
      wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
jihgfee's avatar
jihgfee committed
167
      case_bool_decide.
168
      + wp_select. wp_send with "[$HIy1 //]".
169 170 171
        wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx HΨ").
        * by rewrite comm.
        * by rewrite assoc (comm _ ys2) Hys.
172 173 174
        * by apply Sorted_snoc.
        * by constructor.
        * intros x'.
175
          inversion 1; discriminate_list || simplify_list_eq. by constructor.
176
      + wp_select. wp_send with "[$HIx]".
177 178
        { iPureIntro. by apply Htl_le, total_not. }
        wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
179
        * by rewrite Hys assoc.
180 181 182
        * by apply Sorted_snoc, Htl_le, total_not.
        * constructor. by apply total_not.
        * intros x'.
183
          inversion 1; discriminate_list || simplify_list_eq. by constructor.
184
    - wp_select. wp_send with "[$HIy1 //]".
185
      wp_apply (sort_service_fg_move_spec with "[$Hc $Hc1]").
186 187
      * done.
      * by rewrite Hys Hys2 -!assoc_L (comm _ xs2).
188 189
      * by apply Sorted_snoc.
      * intros x'.
190 191
        inversion 1; discriminate_list || simplify_list_eq. by constructor.
      * iIntros "[Hc Hc1]". iApply "HΨ". iFrame.
jihgfee's avatar
jihgfee committed
192
  Qed.
jihgfee's avatar
jihgfee committed
193

194
  Lemma sort_service_fg_spec cmp c p :
195
    cmp_spec I R cmp -
196 197
    {{{ c  iProto_dual sort_fg_protocol <++> p @ N }}}
      sort_service_fg cmp c
198
    {{{ RET #(); c  p @ N }}}.
jihgfee's avatar
jihgfee committed
199
  Proof.
200
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c p Ψ).
201 202 203
    wp_rec; wp_pures. wp_branch; wp_pures.
    - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
      + wp_recv (x2 v2) as "HIx2".
204
        wp_apply (start_chan_proto_spec N (sort_fg_protocol <++> END)%proto).
205 206
        { iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
        iIntros (cy) "Hcy".
207
        wp_apply (start_chan_proto_spec N (sort_fg_protocol <++> END)%proto).
208 209
        { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
        iIntros (cz) "Hcz". rewrite !right_id.
210 211
        wp_select. wp_send with "[$HIx1]".
        wp_select. wp_send with "[$HIx2]".
212
        wp_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
213
        iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
214
        wp_branch as %_ | %[]%Permutation_nil_cons.
215
        wp_recv (x v) as "[_ HIx]".
216
        wp_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
217
          with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
218
        by rewrite Hxs' Permutation_middle.
219
      + wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
220 221
        wp_select. by iApply "HΨ".
    - wp_select. by iApply "HΨ".
jihgfee's avatar
jihgfee committed
222
  Qed.
223
  End sort_fg_inner.
224

225
  Definition sort_fg_func_protocol : iProto Σ :=
226 227 228
    (<!> A (I : A  val  iProp Σ) (R : A  A  Prop)
         `{!RelDecision R, !Total R} (cmp : val),
       MSG cmp {{ cmp_spec I R cmp }};
229
     sort_fg_head_protocol I R [])%proto.
230

231 232 233
  Lemma sort_service_fg_func_spec c p :
    {{{ c  iProto_dual sort_fg_func_protocol <++> p @ N }}}
      sort_service_fg_func c
234
    {{{ RET #(); c  p @ N }}}.
235
  Proof.
236
    iIntros (Ψ) "Hc HΨ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
    wp_recv (A I R ? ? cmp) as "#Hcmp".
238
    by wp_apply (sort_service_fg_spec with "Hcmp Hc").
239
  Qed.
240
End sort_fg.