sort.v 5.72 KB
Newer Older
1
From stdpp Require Import sorting.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From actris.channel Require Import proto_channel proofmode.
3
From iris.heap_lang Require Import proofmode notation.
4
From actris.utils Require Export llist compare.
Robbert Krebbers's avatar
Robbert Krebbers committed
5

Robbert Krebbers's avatar
Robbert Krebbers committed
6
Definition lmerge : val :=
7
  rec: "go" "cmp" "ys" "zs" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9
    if: lisnil "ys" then lapp "ys" "zs" else
    if: lisnil "zs" then #() else
10 11 12
    let: "y" := lhead "ys" in
    let: "z" := lhead "zs" in
    if: "cmp" "y" "z"
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14
    then lpop "ys";; "go" "cmp" "ys" "zs";; lcons "y" "ys"
    else lpop "zs";; "go" "cmp" "ys" "zs";; lcons "z" "ys".
Robbert Krebbers's avatar
Robbert Krebbers committed
15

Robbert Krebbers's avatar
Robbert Krebbers committed
16
Definition sort_service : val :=
17
  rec: "go" "cmp" "c" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
18
    let: "xs" := recv "c" in
19 20
    if: llength "xs"  #1 then send "c" #() else
    let: "zs" := lsplit "xs" in
21 22 23 24
    let: "cy" := start_chan (λ: "c", "go" "cmp" "c") in
    let: "cz" := start_chan (λ: "c", "go" "cmp" "c") in
    send "cy" "xs";;
    send "cz" "zs";;
Robbert Krebbers's avatar
Robbert Krebbers committed
25
    recv "cy";; recv "cz";;
26
    lmerge "cmp" "xs" "zs";;
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28
    send "c" #().

29 30 31 32 33 34 35 36 37
Definition sort_service_func : val := λ: "c",
  let: "cmp" := recv "c" in
  sort_service "cmp" "c".

Definition sort_client_func : val := λ: "cmp" "xs",
  let: "c" := start_chan sort_service_func in
  send "c" "cmp";; send "c" "xs";;
  recv "c".

Robbert Krebbers's avatar
Robbert Krebbers committed
38
Section sort.
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40
  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).

41 42 43 44 45 46 47
  Definition sort_protocol {A} (I : A  val  iProp Σ) (R : A  A  Prop)
      `{!RelDecision R, !Total R} : iProto Σ :=
    (<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
     <?> (xs' : list A), MSG #() {{  Sorted R xs'    xs'  xs   llist I l xs' }};
     END)%proto.

  Definition sort_protocol_func : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
48
    (<!> A (I : A  val  iProp Σ) (R : A  A  Prop)
49
         `{!RelDecision R, !Total R} (cmp : val),
Robbert Krebbers's avatar
Robbert Krebbers committed
50
       MSG cmp {{ cmp_spec I R cmp }};
51
     sort_protocol I R)%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53

  Lemma lmerge_spec {A} (I : A  val  iProp Σ) (R : A  A  Prop)
Robbert Krebbers's avatar
Robbert Krebbers committed
54
      `{!RelDecision R, !Total R} (cmp : val) l1 l2 xs1 xs2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
55
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
56
    {{{ llist I l1 xs1  llist I l2 xs2 }}}
57
      lmerge cmp #l1 #l2
Robbert Krebbers's avatar
Robbert Krebbers committed
58
    {{{ RET #(); llist I l1 (list_merge R xs1 xs2) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61
    iIntros "#Hcmp" (Ψ) "!> [Hl1 Hl2] HΨ".
    iLöb as "IH" forall (l2 xs1 xs2 Ψ).
Robbert Krebbers's avatar
Robbert Krebbers committed
62
    wp_lam. wp_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
Robbert Krebbers's avatar
Robbert Krebbers committed
63
    destruct xs1 as [|x1 xs1]; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66
    { wp_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
      iApply "HΨ". iFrame. by rewrite list_merge_nil_l. }
    wp_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
Robbert Krebbers's avatar
Robbert Krebbers committed
67
    destruct xs2 as [|x2 xs2]; wp_pures.
68
    { iApply "HΨ". iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71
    wp_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
    wp_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
    wp_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73
    case_bool_decide; wp_pures.
    - rewrite decide_True //.
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75 76 77 78
      wp_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
      wp_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
      { iExists _, _. iFrame. }
      iIntros "Hl1".
      wp_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
    - rewrite decide_False //.
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81 82 83 84
      wp_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
      wp_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
      { iExists _, _. iFrame. }
      iIntros "Hl1".
      wp_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  Qed.
86

87 88 89 90 91
  Lemma sort_service_spec {A} (I : A  val  iProp Σ) (R : A  A  Prop)
      `{!RelDecision R, !Total R} (cmp : val) p c :
    cmp_spec I R cmp -
    {{{ c  iProto_dual (sort_protocol I R) <++> p @ N }}}
      sort_service cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
92
    {{{ RET #(); c  p @ N }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  Proof.
94
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
    wp_recv (xs l) as "Hl".
96
    wp_apply (llength_spec with "Hl"); iIntros "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98 99
    wp_op; case_bool_decide as Hlen; wp_if.
    { assert (Sorted R xs).
      { destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
Robbert Krebbers's avatar
Robbert Krebbers committed
100
      wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
101 102
    wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
      iDestruct 1 as (->) "[Hl1 Hl2]".
103
    wp_apply (start_chan_proto_spec N (sort_protocol I R)); iIntros (cy) "Hcy".
Robbert Krebbers's avatar
Robbert Krebbers committed
104 105
    { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
      wp_apply ("IH" with "Hcy"); auto. }
106
    wp_apply (start_chan_proto_spec N (sort_protocol I R)); iIntros (cz) "Hcz".
Robbert Krebbers's avatar
Robbert Krebbers committed
107 108
    { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
      wp_apply ("IH" with "Hcz"); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
109 110 111 112 113 114
    wp_send with "[$Hl1]".
    wp_send with "[$Hl2]".
    wp_recv (ys1) as (??) "Hl1".
    wp_recv (ys2) as (??) "Hl2".
    wp_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
    wp_send ((list_merge R ys1 ys2)) with "[$Hl]".
115 116 117 118
    - iSplit; iPureIntro.
      + by apply (Sorted_list_merge _).
      + rewrite (merge_Permutation R). by f_equiv.
    - by iApply "HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  Qed.
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146

  Lemma sort_service_func_spec p c :
    {{{ c  iProto_dual sort_protocol_func <++> p @ N }}}
      sort_service_func c
    {{{ RET #(); c  p @ N }}}.
  Proof.
    iIntros (Ψ) "Hc HΨ". wp_lam.
    wp_recv (A I R ?? cmp) as "#Hcmp".
    by wp_apply (sort_service_spec with "Hcmp Hc").
  Qed.

  Lemma sort_client_func_spec {A} (I : A  val  iProp Σ) R
       `{!RelDecision R, !Total R} cmp l (xs : list A) :
    cmp_spec I R cmp -
    {{{ llist I l xs }}}
      sort_client_func 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 N sort_protocol_func); iIntros (c) "Hc".
    { rewrite -(right_id END%proto _ (iProto_dual _)).
      wp_apply (sort_service_func_spec with "Hc"); auto. }
    wp_send with "[$Hcmp]".
    wp_send with "[$Hl]".
    wp_recv (ys) as "(Hsorted & Hperm & Hl)".
    wp_pures. iApply "HΦ"; iFrame.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
End sort.