Commit 58fb2b1a authored by Robbert Krebbers's avatar Robbert Krebbers

Move compare stuff to its own file.

parent 82cfbaf1
......@@ -3,6 +3,7 @@
theories/utils/auth_excl.v
theories/utils/encodable.v
theories/utils/list.v
theories/utils/compare.v
theories/channel/channel.v
theories/channel/proto_model.v
theories/channel/proto_channel.v
......
From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel.
From iris.heap_lang Require Import proofmode notation.
From osiris.utils Require Import list.
From osiris.utils Require Import list compare.
Definition lmerge : val :=
rec: "go" "cmp" "ys" "zs" :=
......@@ -38,13 +38,6 @@ Definition list_sort_client : val := λ: "cmp" "xs",
Section list_sort.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
Definition cmp_spec {A} (I : A val iProp Σ)
(R : A A Prop) `{!RelDecision R} (cmp : val) : iProp Σ :=
( x x' v v',
{{{ I x v I x' v' }}}
cmp v v'
{{{ RET #(bool_decide (R x x')); I x v I x' v' }}})%I.
Definition sort_protocol : iProto Σ :=
(<!> A (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} (cmp : val),
......@@ -163,5 +156,4 @@ Section list_sort.
iIntros (ys ws) "Hc (Hsorted & Hperm & Hl & HI)".
wp_pures. iApply "HΦ". iFrame.
Qed.
End list_sort.
......@@ -2,7 +2,7 @@ From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
From osiris.utils Require Import list.
From osiris.utils Require Import list compare.
Definition cont := true.
Definition stop := false.
......@@ -47,14 +47,6 @@ Definition list_sort_elem_service : val :=
let: "x" := (if: recv "c1" then recv "c1" else assert #false) in
list_sort_elem_service_merge "cmp" "c" "x" "c1" "c2".
(** This definition is also in list_sort, move elsewhere *)
Definition cmp_spec `{!heapG Σ} {A} (I : A val iProp Σ)
(R : relation A) `{!RelDecision R} (cmp : val) : iProp Σ :=
( x x' v v',
{{{ I x v I x' v' }}}
cmp v v'
{{{ RET #(bool_decide (R x x')); I x v I x' v' }}})%I.
Section list_sort_elem.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
Context {A} (I : A val iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
......
From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel.
From iris.heap_lang Require Import proofmode notation.
From osiris.utils Require Import list.
From osiris.utils Require Import list compare.
From osiris.examples Require Import list_sort.
Definition cmpZ : val :=
λ: "x" "y", "x" "y".
Section list_sort_instances.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
(* Example: Sort of integers *)
Definition IZ (x : Z) (v : val) : iProp Σ := v = #x%I.
Lemma cmpZ_spec : cmp_spec IZ () cmpZ.
Proof.
rewrite /IZ. iIntros (x x' v v' Φ [-> ->]) "!> HΦ".
wp_lam. wp_pures. by iApply "HΦ".
Qed.
Local Arguments val_encode _ _ !_ /.
Lemma list_sort_client_le_spec l (xs : list Z) :
{{{ l val_encode xs }}}
list_sort_client cmpZ #l
{{{ ys, RET #(); Sorted () ys ys xs l val_encode ys }}}.
{{{ ys, RET #(); Sorted () ys ys xs l val_encode ys }}}.
Proof.
assert ( zs : list Z, val_encode zs = val_encode (LitV LitInt <$> zs)) as Henc.
{ intros zs. induction zs; f_equal/=; auto with f_equal. }
......
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Definition cmp_spec `{!heapG Σ} {A} (I : A val iProp Σ)
(R : relation A) `{!RelDecision R} (cmp : val) : iProp Σ :=
( x x' v v',
{{{ I x v I x' v' }}}
cmp v v'
{{{ RET #(bool_decide (R x x')); I x v I x' v' }}})%I.
Definition IZ `{!heapG Σ} (x : Z) (v : val) : iProp Σ := v = #x%I.
Definition cmpZ : val := λ: "x" "y", "x" "y".
Lemma cmpZ_spec `{!heapG Σ} : cmp_spec IZ () cmpZ.
Proof.
rewrite /IZ. iIntros (x x' v v' Φ [-> ->]) "!> HΦ".
wp_lam. wp_pures. by iApply "HΦ".
Qed.
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment