sort_elem.v 9.87 KB
Newer Older
jihgfee's avatar
jihgfee committed
1
From stdpp Require Import sorting.
2
From osiris.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 osiris.utils Require Import list compare.
jihgfee's avatar
jihgfee committed
6

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

Robbert Krebbers's avatar
Robbert Krebbers committed
10
Definition sort_elem_service_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_elem_service_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

Robbert Krebbers's avatar
Robbert Krebbers committed
24
Definition sort_elem_service_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_elem_service_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

Robbert Krebbers's avatar
Robbert Krebbers committed
36
Definition sort_elem_service : 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 44 45
    let: "cc1" := new_chan #() in
    let: "c1" := Fst "cc1" in let: "c1'" := Snd "cc1" in
    let: "cc2" := new_chan #() in
    let: "c2" := Fst "cc2" in let: "c2'" := Snd "cc2" in
46 47
    send "c1" #cont;; send "c1" "x";;
    send "c2" #cont;; send "c2" "y";;
Robbert Krebbers's avatar
Robbert Krebbers committed
48
    sort_elem_service_split "c" "c1" "c2";;
49
    Fork ("go" "cmp" "c1'");; Fork ("go" "cmp" "c2'");;
50
    let: "x" := (if: recv "c1" then recv "c1" else assert #false) in
Robbert Krebbers's avatar
Robbert Krebbers committed
51
    sort_elem_service_merge "cmp" "c" "x" "c1" "c2".
52

Robbert Krebbers's avatar
Robbert Krebbers committed
53
Definition sort_elem_service_top : val := λ: "c",
54
  let: "cmp" := recv "c" in
Robbert Krebbers's avatar
Robbert Krebbers committed
55
  sort_elem_service "cmp" "c".
56

Robbert Krebbers's avatar
Robbert Krebbers committed
57
Section sort_elem.
jihgfee's avatar
jihgfee committed
58
  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
59

Robbert Krebbers's avatar
Robbert Krebbers committed
60
  Section sort_elem_inner.
61
  Context {A} (I : A  val  iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
jihgfee's avatar
jihgfee committed
62

Robbert Krebbers's avatar
Robbert Krebbers committed
63
  Definition sort_elem_tail_protocol_aux (xs : list A)
64 65
      (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]))
66
     <&{ ys  xs }> END)%proto.
jihgfee's avatar
jihgfee committed
67

Robbert Krebbers's avatar
Robbert Krebbers committed
68 69
  Instance sort_elem_tail_protocol_aux_contractive xs :
    Contractive (sort_elem_tail_protocol_aux xs).
70
  Proof. solve_proto_contractive. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71 72 73 74 75 76 77 78
  Definition sort_elem_tail_protocol (xs : list A) : list A  iProto Σ :=
    fixpoint (sort_elem_tail_protocol_aux xs).
  Global Instance sort_elem_tail_protocol_unfold xs ys :
    ProtoUnfold (sort_elem_tail_protocol xs ys)
      (sort_elem_tail_protocol_aux xs (sort_elem_tail_protocol xs) ys).
  Proof. apply proto_unfold_eq, (fixpoint_unfold (sort_elem_tail_protocol_aux _)). Qed.

  Definition sort_elem_head_protocol_aux
79 80
      (rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ xs,
    ((<!> x v, MSG v {{ I x v }}; (rec : _  iProto Σ) (xs ++ [x]))
Robbert Krebbers's avatar
Robbert Krebbers committed
81
     <+> sort_elem_tail_protocol xs [])%proto.
82

Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
  Instance sort_elem_head_protocol_aux_contractive :
    Contractive sort_elem_head_protocol_aux.
85
  Proof. solve_proto_contractive. Qed.
86

Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90 91 92
  Definition sort_elem_head_protocol : list A  iProto Σ :=
    fixpoint sort_elem_head_protocol_aux.
  Global Instance sort_elem_head_protocol_unfold xs :
    ProtoUnfold (sort_elem_head_protocol xs)
      (sort_elem_head_protocol_aux sort_elem_head_protocol xs).
  Proof. apply proto_unfold_eq, (fixpoint_unfold sort_elem_head_protocol_aux). Qed.
jihgfee's avatar
jihgfee committed
93

Robbert Krebbers's avatar
Robbert Krebbers committed
94
  Definition sort_elem_protocol : iProto Σ := sort_elem_head_protocol [].
95

Robbert Krebbers's avatar
Robbert Krebbers committed
96
  Lemma sort_elem_service_split_spec c p c1 c2 xs xs1 xs2 :
jihgfee's avatar
jihgfee committed
97
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99
      c  iProto_dual (sort_elem_head_protocol xs) <++> p @ N 
      c1  sort_elem_head_protocol xs1 @ N  c2  sort_elem_head_protocol xs2 @ N
100
    }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
101
      sort_elem_service_split c c1 c2
jihgfee's avatar
jihgfee committed
102
    {{{ xs' xs1' xs2', RET #();
103
      xs'  xs1' ++ xs2' 
Robbert Krebbers's avatar
Robbert Krebbers committed
104 105 106
      c  iProto_dual (sort_elem_tail_protocol (xs ++ xs') []) <++> p @ N 
      c1  sort_elem_tail_protocol (xs1 ++ xs1') [] @ N 
      c2  sort_elem_tail_protocol (xs2 ++ xs2') [] @ N
107
    }}}.
jihgfee's avatar
jihgfee committed
108 109
  Proof.
    iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
110
    wp_rec. wp_branch.
111
    - wp_recv (x v) as "HI". wp_select. wp_send with "[$HI]".
112 113 114 115
      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.
116
    - wp_select. wp_select.
117
      iApply ("HΨ" $! [] [] []). rewrite !right_id_L. by iFrame.
jihgfee's avatar
jihgfee committed
118
  Qed.
jihgfee's avatar
jihgfee committed
119

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
197
  Lemma sort_elem_service_spec cmp c p :
198
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200
    {{{ c  iProto_dual sort_elem_protocol <++> p @ N }}}
      sort_elem_service cmp c
201
    {{{ RET #(); c  p @ N }}}.
jihgfee's avatar
jihgfee committed
202
  Proof.
203
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c p Ψ).
204 205 206
    wp_rec; wp_pures. wp_branch; wp_pures.
    - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
      + wp_recv (x2 v2) as "HIx2".
207 208
        wp_apply (new_chan_proto_spec N with "[//]"); iIntros (cy1 cy2) "Hcy".
        wp_apply (new_chan_proto_spec N with "[//]"); iIntros (cz1 cz2) "Hcz".
Robbert Krebbers's avatar
Robbert Krebbers committed
209 210
        iMod ("Hcy" $! (sort_elem_protocol <++> END)%proto) as "[Hcy1 Hcy2]".
        iMod ("Hcz" $! (sort_elem_protocol <++> END)%proto) as "[Hcz1 Hcz2]".
211
        iEval (rewrite right_id) in "Hcy1 Hcz1".
212 213
        wp_select. wp_send with "[$HIx1]".
        wp_select. wp_send with "[$HIx2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
214
        wp_apply (sort_elem_service_split_spec with "[$Hc $Hcy1 $Hcz1]").
215
        iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
216 217 218 219
        wp_apply (wp_fork with "[Hcy2]").
        { iNext. wp_apply ("IH" with "Hcy2"); auto. }
        wp_apply (wp_fork with "[Hcz2]").
        { iNext. wp_apply ("IH" with "Hcz2"); auto. }
220
        wp_branch as %_ | %[]%Permutation_nil_cons.
221
        wp_recv (x v) as "[_ HIx]".
Robbert Krebbers's avatar
Robbert Krebbers committed
222
        wp_apply (sort_elem_service_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
223
          with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
224
        by rewrite Hxs' Permutation_middle.
225
      + wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
226 227
        wp_select. by iApply "HΨ".
    - wp_select. by iApply "HΨ".
jihgfee's avatar
jihgfee committed
228
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
  End sort_elem_inner.
230

Robbert Krebbers's avatar
Robbert Krebbers committed
231
  Definition sort_elem_top_protocol : iProto Σ :=
232 233 234
    (<!> A (I : A  val  iProp Σ) (R : A  A  Prop)
         `{!RelDecision R, !Total R} (cmp : val),
       MSG cmp {{ cmp_spec I R cmp }};
Robbert Krebbers's avatar
Robbert Krebbers committed
235
     sort_elem_head_protocol I R [])%proto.
236

Robbert Krebbers's avatar
Robbert Krebbers committed
237 238 239
  Lemma sort_elem_service_top_spec c p :
    {{{ c  iProto_dual sort_elem_top_protocol <++> p @ N }}}
      sort_elem_service_top c
240
    {{{ RET #(); c  p @ N }}}.
241
  Proof.
242
    iIntros (Ψ) "Hc HΨ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
243 244
    wp_recv (A I R ? ? cmp) as "#Hcmp".
    by wp_apply (sort_elem_service_spec with "Hcmp Hc").
245
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
End sort_elem.