sort_fg.v 12 KB
Newer Older
1 2
(** This file implements a fine-grained Merge Sort,
a specification thereof and its proofs. *)
3
From stdpp Require Export sorting.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From actris.channel Require Import proto_channel proofmode.
jihgfee's avatar
jihgfee committed
5 6
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
jihgfee's avatar
jihgfee committed
7
From actris.utils Require Import llist compare.
jihgfee's avatar
jihgfee committed
8

jihgfee's avatar
jihgfee committed
9 10 11
Definition cont := true.
Definition stop := false.

12
Definition sort_service_fg_split : val :=
jihgfee's avatar
jihgfee committed
13
  rec: "go" "c" "c1" "c2" :=
14 15 16 17
    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
18

Robbert Krebbers's avatar
Robbert Krebbers committed
19
Definition sort_service_fg_forward : val :=
jihgfee's avatar
jihgfee committed
20
  rec: "go" "c" "cin" :=
21 22 23 24
    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
25

26
Definition sort_service_fg_merge : val :=
27 28 29
  rec: "go" "cmp" "c" "x1" "c1" "c2" :=
    if: ~recv "c2" then
      send "c" #cont;; send "c" "x1";;
Robbert Krebbers's avatar
Robbert Krebbers committed
30
      sort_service_fg_forward "c" "c1"
31 32 33 34 35 36
    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
37

38
Definition sort_service_fg : val :=
39 40 41 42 43
  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
44 45
    let: "c1" := start_chan (λ: "c", "go" "cmp" "c") in
    let: "c2" := start_chan (λ: "c", "go" "cmp" "c") in
46 47
    send "c1" #cont;; send "c1" "x";;
    send "c2" #cont;; send "c2" "y";;
48
    sort_service_fg_split "c" "c1" "c2";;
49
    let: "x" := (if: recv "c1" then recv "c1" else assert #false) in
50
    sort_service_fg_merge "cmp" "c" "x" "c1" "c2".
51

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

jihgfee's avatar
jihgfee committed
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
Definition send_all : val :=
  rec: "go" "c" "xs" :=
    if: lisnil "xs" then #() else
    send "c" #cont;; send "c" (lpop "xs");; "go" "c" "xs".

Definition recv_all : val :=
  rec: "go" "c" "ys" :=
    if: ~recv "c" then #() else
    let: "x" := recv "c" in
    "go" "c" "ys";; lcons "x" "ys".

Definition sort_client_fg : val := λ: "cmp" "xs",
  let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
  send_all "c" "xs";;
  send "c" #stop;;
  recv_all "c" "xs".

73
Section sort_fg.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  Context `{!heapG Σ, !proto_chanG Σ}.
75

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

79
  Definition sort_fg_tail_protocol_aux (xs : list A)
80 81
      (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]))
82
     <&{ ys  xs }> END)%proto.
jihgfee's avatar
jihgfee committed
83

84 85
  Instance sort_fg_tail_protocol_aux_contractive xs :
    Contractive (sort_fg_tail_protocol_aux xs).
86
  Proof. solve_proto_contractive. Qed.
87 88 89 90 91 92 93 94
  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
95 96
      (rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ xs,
    ((<!> x v, MSG v {{ I x v }}; (rec : _  iProto Σ) (xs ++ [x]))
97
     <+> sort_fg_tail_protocol xs [])%proto.
98

99 100
  Instance sort_fg_head_protocol_aux_contractive :
    Contractive sort_fg_head_protocol_aux.
101
  Proof. solve_proto_contractive. Qed.
102

103 104 105 106 107 108
  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
109

110
  Definition sort_fg_protocol : iProto Σ := sort_fg_head_protocol [].
111

112
  Lemma sort_service_fg_split_spec c p c1 c2 xs xs1 xs2 :
jihgfee's avatar
jihgfee committed
113
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115
      c  (iProto_dual (sort_fg_head_protocol xs) <++> p) 
      c1  sort_fg_head_protocol xs1  c2  sort_fg_head_protocol xs2
116
    }}}
117
      sort_service_fg_split c c1 c2
jihgfee's avatar
jihgfee committed
118
    {{{ xs' xs1' xs2', RET #();
119
      xs'  xs1' ++ xs2' 
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122
      c  (iProto_dual (sort_fg_tail_protocol (xs ++ xs') []) <++> p) 
      c1  sort_fg_tail_protocol (xs1 ++ xs1') [] 
      c2  sort_fg_tail_protocol (xs2 ++ xs2') []
123
    }}}.
jihgfee's avatar
jihgfee committed
124 125
  Proof.
    iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
126
    wp_rec. wp_branch.
127
    - wp_recv (x v) as "HI". wp_select. wp_send with "[$HI]".
128 129 130 131
      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.
132
    - wp_select. wp_select.
133
      iApply ("HΨ" $! [] [] []). rewrite !right_id_L. by iFrame.
jihgfee's avatar
jihgfee committed
134
  Qed.
jihgfee's avatar
jihgfee committed
135

Robbert Krebbers's avatar
Robbert Krebbers committed
136
  Lemma sort_service_fg_forward_spec c p cin xs ys zs xs' ys' :
137 138
    xs  xs' ++ zs 
    ys  ys' ++ zs 
139 140
    Sorted R ys 
    ( x, TlRel R x ys'  TlRel R x ys) 
jihgfee's avatar
jihgfee committed
141
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143
      c  (iProto_dual (sort_fg_tail_protocol xs ys) <++> p) 
      cin  sort_fg_tail_protocol xs' ys'
jihgfee's avatar
jihgfee committed
144
    }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
145
      sort_service_fg_forward c cin
Robbert Krebbers's avatar
Robbert Krebbers committed
146
    {{{ RET #(); c  p  cin  END }}}.
jihgfee's avatar
jihgfee committed
147
  Proof.
148 149
    iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
    iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
150
    wp_rec. wp_branch as %_ | %Hys'.
151 152
    - wp_recv (x v) as (Htl) "HI".
      wp_select. wp_send with "[$HI]"; first by auto.
153
      wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
154 155
      * done.
      * by rewrite Hys -!assoc_L (comm _ zs).
156 157
      * auto using Sorted_snoc.
      * intros x'.
158
        inversion 1; discriminate_list || simplify_list_eq. by constructor.
159
    - wp_select with "[]".
160 161
      { by rewrite /= Hys Hxs Hys'. }
      iApply "HΨ". iFrame.
jihgfee's avatar
jihgfee committed
162
  Qed.
163

164
  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
165 166
    xs  xs1 ++ xs2 
    ys  ys1 ++ ys2 
167 168 169
    Sorted R ys 
    TlRel R y1 ys 
    ( x, TlRel R x ys2  R x y1  TlRel R x ys) 
170
    cmp_spec I R cmp -
jihgfee's avatar
jihgfee committed
171
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173 174
      c  (iProto_dual (sort_fg_tail_protocol xs ys) <++> p) 
      c1  sort_fg_tail_protocol xs1 (ys1 ++ [y1]) 
      c2  sort_fg_tail_protocol xs2 ys2 
175
      I y1 w1
Robbert Krebbers's avatar
Robbert Krebbers committed
176
    }}}
177
      sort_service_fg_merge cmp c w1 c1 c2
Robbert Krebbers's avatar
Robbert Krebbers committed
178
    {{{ RET #(); c  p }}}.
jihgfee's avatar
jihgfee committed
179
  Proof.
180 181 182
    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).
183
    wp_rec. wp_branch as %_ | %Hys2.
184
    - wp_recv (x v) as (Htl2) "HIx".
185
      wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
jihgfee's avatar
jihgfee committed
186
      case_bool_decide.
187
      + wp_select. wp_send with "[$HIy1 //]".
188 189 190
        wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx HΨ").
        * by rewrite comm.
        * by rewrite assoc (comm _ ys2) Hys.
191 192 193
        * by apply Sorted_snoc.
        * by constructor.
        * intros x'.
194
          inversion 1; discriminate_list || simplify_list_eq. by constructor.
195
      + wp_select. wp_send with "[$HIx]".
196 197
        { iPureIntro. by apply Htl_le, total_not. }
        wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
198
        * by rewrite Hys assoc.
199 200 201
        * by apply Sorted_snoc, Htl_le, total_not.
        * constructor. by apply total_not.
        * intros x'.
202
          inversion 1; discriminate_list || simplify_list_eq. by constructor.
203
    - wp_select. wp_send with "[$HIy1 //]".
Robbert Krebbers's avatar
Robbert Krebbers committed
204
      wp_apply (sort_service_fg_forward_spec with "[$Hc $Hc1]").
205 206
      * done.
      * by rewrite Hys Hys2 -!assoc_L (comm _ xs2).
207 208
      * by apply Sorted_snoc.
      * intros x'.
209 210
        inversion 1; discriminate_list || simplify_list_eq. by constructor.
      * iIntros "[Hc Hc1]". iApply "HΨ". iFrame.
jihgfee's avatar
jihgfee committed
211
  Qed.
jihgfee's avatar
jihgfee committed
212

213
  Lemma sort_service_fg_spec cmp c p :
214
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
215
    {{{ c  (iProto_dual sort_fg_protocol <++> p) }}}
216
      sort_service_fg cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
217
    {{{ RET #(); c  p }}}.
jihgfee's avatar
jihgfee committed
218
  Proof.
219
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c p Ψ).
220 221 222
    wp_rec; wp_pures. wp_branch; wp_pures.
    - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
      + wp_recv (x2 v2) as "HIx2".
Robbert Krebbers's avatar
Robbert Krebbers committed
223
        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
224 225
        { iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
        iIntros (cy) "Hcy".
Robbert Krebbers's avatar
Robbert Krebbers committed
226
        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
227 228
        { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
        iIntros (cz) "Hcz". rewrite !right_id.
229 230
        wp_select. wp_send with "[$HIx1]".
        wp_select. wp_send with "[$HIx2]".
231
        wp_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
232
        iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
233
        wp_branch as %_ | %[]%Permutation_nil_cons.
234
        wp_recv (x v) as "[_ HIx]".
235
        wp_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
236
          with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
237
        by rewrite Hxs' Permutation_middle.
238
      + wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
239 240
        wp_select. by iApply "HΨ".
    - wp_select. by iApply "HΨ".
jihgfee's avatar
jihgfee committed
241
  Qed.
jihgfee's avatar
jihgfee committed
242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
  
  Lemma send_all_spec c p xs' l xs :
    {{{ llist I l xs  c  (sort_fg_head_protocol xs' <++> p) }}}
      send_all c #l
    {{{ RET #(); llist I l []  c  (sort_fg_head_protocol (xs' ++ xs) <++> p) }}}.
  Proof.
    iIntros (Φ) "[Hl Hc] HΦ".
    iInduction xs as [|x xs] "IH" forall (xs').
    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
      iApply "HΦ". rewrite right_id_L. iFrame. }
    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
    wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
  Qed.

  Lemma recv_all_spec c p l xs ys' :
    Sorted R ys' 
    {{{ llist I l []  c  (sort_fg_tail_protocol xs ys' <++> p) }}}
      recv_all c #l
    {{{ ys, RET #();
        Sorted R (ys' ++ ys)  ys' ++ ys  xs  llist I l ys  c  p
    }}}.
  Proof.
    iIntros (Hsort Φ) "[Hl Hc] HΦ".
    iLöb as "IH" forall (xs ys' Φ Hsort).
    wp_lam. wp_branch as %_ | %Hperm; wp_pures.
    - wp_recv (y v) as (Htl) "HIx".
      wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
      iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
      wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl"; wp_pures.
      iApply ("HΦ" with "[$Hl $Hc]"); simpl; eauto.
    - iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
  Qed.

  Lemma sort_client_fg_spec cmp l xs :
    cmp_spec I R cmp -
    {{{ llist I l xs }}}
      sort_client_fg cmp #l
    {{{ ys, RET #(); Sorted R ys  ys  xs  llist I l ys }}}.
  Proof.
    iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
    wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto);
      iIntros (c) "Hc".
    { wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
    wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
    wp_select.
    wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.
    iIntros (ys) "/=". iDestruct 1 as (??) "[Hk _]".
    iApply "HΦ"; auto with iFrame.
  Qed.
  
293
  End sort_fg_inner.
294

295
  Definition sort_fg_func_protocol : iProto Σ :=
296 297 298
    (<!> A (I : A  val  iProp Σ) (R : A  A  Prop)
         `{!RelDecision R, !Total R} (cmp : val),
       MSG cmp {{ cmp_spec I R cmp }};
299
     sort_fg_head_protocol I R [])%proto.
300

301
  Lemma sort_service_fg_func_spec c p :
Robbert Krebbers's avatar
Robbert Krebbers committed
302
    {{{ c  (iProto_dual sort_fg_func_protocol <++> p) }}}
303
      sort_service_fg_func c
Robbert Krebbers's avatar
Robbert Krebbers committed
304
    {{{ RET #(); c  p }}}.
305
  Proof.
306
    iIntros (Ψ) "Hc HΨ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
    wp_recv (A I R ? ? cmp) as "#Hcmp".
308
    by wp_apply (sort_service_fg_spec with "Hcmp Hc").
309
  Qed.
jihgfee's avatar
jihgfee committed
310
End sort_fg.