sort_fg.v 11.9 KB
Newer Older
1
From stdpp Require Export 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.
jihgfee's avatar
jihgfee committed
5
From actris.utils Require Import llist 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

Robbert Krebbers's avatar
Robbert Krebbers committed
17
Definition sort_service_fg_forward : 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";;
Robbert Krebbers's avatar
Robbert Krebbers committed
28
      sort_service_fg_forward "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

jihgfee's avatar
jihgfee committed
54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
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".

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

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

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

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

97 98
  Instance sort_fg_head_protocol_aux_contractive :
    Contractive sort_fg_head_protocol_aux.
99
  Proof. solve_proto_contractive. Qed.
100

101 102 103 104 105 106
  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
107

108
  Definition sort_fg_protocol : iProto Σ := sort_fg_head_protocol [].
109

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

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

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

211
  Lemma sort_service_fg_spec cmp c p :
212
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
213
    {{{ c  (iProto_dual sort_fg_protocol <++> p) }}}
214
      sort_service_fg cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
215
    {{{ RET #(); c  p }}}.
jihgfee's avatar
jihgfee committed
216
  Proof.
217
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c p Ψ).
218 219 220
    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
221
        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
222 223
        { iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
        iIntros (cy) "Hcy".
Robbert Krebbers's avatar
Robbert Krebbers committed
224
        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
225 226
        { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
        iIntros (cz) "Hcz". rewrite !right_id.
227 228
        wp_select. wp_send with "[$HIx1]".
        wp_select. wp_send with "[$HIx2]".
229
        wp_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
230
        iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
231
        wp_branch as %_ | %[]%Permutation_nil_cons.
232
        wp_recv (x v) as "[_ HIx]".
233
        wp_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
234
          with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
235
        by rewrite Hxs' Permutation_middle.
236
      + wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
237 238
        wp_select. by iApply "HΨ".
    - wp_select. by iApply "HΨ".
jihgfee's avatar
jihgfee committed
239
  Qed.
jihgfee's avatar
jihgfee committed
240 241 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
  
  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.
  
291
  End sort_fg_inner.
292

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

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