sort_client.v 1.06 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From actris.examples Require Import sort.
5

6 7 8 9 10
Definition sort_client : val := λ: "cmp" "xs",
  let: "c" := start_chan sort_service in
  send "c" "cmp";; send "c" "xs";;
  recv "c".

Robbert Krebbers's avatar
Robbert Krebbers committed
11
Section sort_client.
12 13
  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).

14
  Lemma sort_client_spec {A} (I : A  val  iProp Σ) R
Robbert Krebbers's avatar
Robbert Krebbers committed
15
       `{!RelDecision R, !Total R} cmp l (xs : list A) :
16
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
17
    {{{ llist I l xs }}}
18
      sort_client cmp #l
Robbert Krebbers's avatar
Robbert Krebbers committed
19
    {{{ ys, RET #(); Sorted R ys  ys  xs  llist I l ys }}}.
20 21 22 23 24 25 26
  Proof.
    iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
    wp_apply (start_chan_proto_spec N sort_protocol); iIntros (c) "Hc".
    { rewrite -(right_id END%proto _ (iProto_dual _)).
      wp_apply (sort_service_spec with "Hc"); auto. }
    wp_send with "[$Hcmp]".
    wp_send with "[$Hl]".
Robbert Krebbers's avatar
Robbert Krebbers committed
27
    wp_recv (ys) as "(Hsorted & Hperm & Hl)".
28 29
    wp_pures. iApply "HΦ"; iFrame.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
End sort_client.