Commit 8de152b1 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'typed_proph' into 'master'

Typed prophecy variables + cleanup

See merge request iris/examples!28
parents f2637250 0c551f14
......@@ -25,3 +25,6 @@ hocap: $(filter theories/hocap/%,$(VOFILES))
logatom: $(filter theories/logatom/%,$(VOFILES))
.PHONY: logatom
proph: $(filter theories/proph/%,$(VOFILES))
.PHONY: proph
......@@ -98,8 +98,6 @@ theories/hocap/parfib.v
theories/logatom/treiber.v
theories/logatom/treiber2.v
theories/logatom/lib/gc.v
theories/logatom/lib/one_shot_proph.v
theories/logatom/lib/typed_proph.v
theories/logatom/elimination_stack/hocap_spec.v
theories/logatom/elimination_stack/stack.v
theories/logatom/elimination_stack/spec.v
......@@ -115,6 +113,17 @@ theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss/rdcss.v
theories/logatom/rdcss/spec.v
theories/logatom/proph_erasure.v
theories/logatom/herlihy_wing_queue/spec.v
theories/logatom/herlihy_wing_queue/hwq.v
theories/proph/proph_erasure.v
theories/proph/lib/one_shot_proph.v
theories/proph/lib/typed_proph.v
theories/proph/eager_coin_spec.v
theories/proph/eager_coin.v
theories/proph/lazy_coin.v
theories/proph/lazy_coin_one_shot.v
theories/proph/lazy_coin_one_shot_typed.v
theories/proph/clairvoyant_coin_spec.v
theories/proph/clairvoyant_coin.v
theories/proph/clairvoyant_coin_typed.v
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
From iris_examples.proph Require Import clairvoyant_coin_spec.
(* Clairvoyant coin using (untyped) sequence prophecies. *)
Definition new_coin: val :=
λ: <>, (ref (nondet_bool #()), NewProph).
Definition read_coin : val := λ: "cp", !(Fst "cp").
Definition toss_coin : val :=
λ: "cp",
let: "c" := Fst "cp" in
let: "p" := Snd "cp" in
let: "r" := nondet_bool #() in
"c" <- "r";; resolve_proph: "p" to: "r";; #().
Section proof.
Context `{!heapG Σ}.
Definition prophecy_to_list_bool (vs : list (val * val)) : list bool :=
(λ v, bool_decide (v = #true)) snd <$> vs.
Definition coin (cp : val) (bs : list bool) : iProp Σ :=
( (c : loc) (p : proph_id) (vs : list (val * val)),
cp = (#c, #p)%V
bs [] tail bs = prophecy_to_list_bool vs
proph p vs
from_option (λ b : bool, c #b) ( b : bool, c #b) (head bs))%I.
Lemma coin_exclusive (cp : val) (bs1 bs2 : list bool) :
coin cp bs1 - coin cp bs2 - False.
Proof.
iIntros "H1 H2".
iDestruct "H1" as (c1 p1 vs1) "(-> & _ & _ & Hp1 & _)".
iDestruct "H2" as (c2 p2 vs2) "(% & _ & _ & Hp2 & _)".
simplify_eq. iApply (proph_exclusive with "Hp1 Hp2").
Qed.
Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c bs, RET c; coin c bs }}}.
Proof.
iIntros (Φ) "_ HΦ".
wp_lam.
wp_apply wp_new_proph; first done.
iIntros (vs p) "Hp".
wp_apply nondet_bool_spec; first done.
iIntros (b) "_".
wp_alloc c as "Hc".
wp_pair.
iApply ("HΦ" $! (#c, #p)%V (b :: prophecy_to_list_bool vs)).
rewrite /coin; eauto with iFrame.
Qed.
Lemma read_coin_spec cp bs :
{{{ coin cp bs }}}
read_coin cp
{{{ b bs', RET #b; bs = b :: bs' coin cp bs }}}.
Proof.
iIntros (Φ) "Hc HΦ".
iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
destruct bs as [|b bs]; simplify_eq/=.
wp_lam. wp_load.
iApply "HΦ"; iSplit; first done.
rewrite /coin; eauto 10 with iFrame.
Qed.
Lemma toss_coin_spec cp bs :
{{{ coin cp bs }}}
toss_coin cp
{{{ b bs', RET #(); bs = b :: bs' coin cp bs' }}}.
Proof.
iIntros (Φ) "Hc HΦ".
iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
destruct bs as [|b bs]; simplify_eq/=.
wp_lam. do 2 (wp_proj; wp_let).
wp_apply nondet_bool_spec; first done.
iIntros (r) "_".
wp_store.
wp_apply (wp_resolve_proph with "[Hp]"); first done.
iIntros (ws) "[-> Hp]".
wp_seq.
iApply "HΦ"; iSplit; first done.
destruct r; rewrite /coin; eauto 10 with iFrame.
Qed.
End proof.
Definition clairvoyant_coin_spec_instance `{!heapG Σ} :
clairvoyant_coin_spec.clairvoyant_coin_spec Σ :=
{| clairvoyant_coin_spec.new_coin_spec := new_coin_spec;
clairvoyant_coin_spec.read_coin_spec := read_coin_spec;
clairvoyant_coin_spec.toss_coin_spec := toss_coin_spec;
clairvoyant_coin_spec.coin_exclusive := coin_exclusive |}.
Typeclasses Opaque coin.
From iris.heap_lang Require Export lifting notation.
Set Default Proof Using "Type".
(** Specification for a clairvoyant coin. A clairvoyant coin predicts all the
values that it will *non-deterministically* choose throughout the execution of
the program. This can be seen in the spec. The predicate [coin c bs] expresses
that [bs] is the list of all the values of the coin in the future. Note that
the [read_coin] operation returns the head of [bs] and that the [toss_coin]
operation takes the [tail] of [bs]. *)
Record clairvoyant_coin_spec `{!heapG Σ} := ClairvoyantCoinSpec {
(* -- operations -- *)
new_coin: val;
read_coin: val;
toss_coin: val;
(* -- predicates -- *)
coin (c : val) (bs : list bool) : iProp Σ;
(* -- predicate properties -- *)
coin_exclusive c b1 b2 : coin c b1 - coin c b2 - False;
(* -- operation specs -- *)
new_coin_spec :
{{{ True }}}
new_coin #()
{{{ c bs, RET c ; coin c bs }}};
read_coin_spec c bs:
{{{ coin c bs }}}
read_coin c
{{{ b bs', RET #b ; bs = b :: bs' coin c bs }}};
toss_coin_spec c bs:
{{{ coin c bs }}}
toss_coin c
{{{ b bs', RET #(); bs = b :: bs' coin c bs' }}};
}.
Arguments clairvoyant_coin_spec _ {_}.
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
From iris_examples.proph.lib Require Import typed_proph.
From iris_examples.proph Require Import clairvoyant_coin_spec.
(* Clairvoyant coin with *typed* prophecies. *)
Definition new_coin: val :=
λ: <>, (ref (nondet_bool #()), NewProph).
Definition read_coin : val := λ: "cp", !(Fst "cp").
Definition toss_coin : val :=
λ: "cp",
let: "c" := Fst "cp" in
let: "p" := Snd "cp" in
let: "r" := nondet_bool #() in
"c" <- "r";; resolve_proph: "p" to: "r";; #().
Section proof.
Context `{!heapG Σ}.
Definition coin (cp : val) (bs : list bool) : iProp Σ :=
( (c : loc) (p : proph_id) (b : bool) (bs' : list bool),
cp = (#c, #p)%V bs = b :: bs' c #b
(typed_proph_prop BoolTypedProph) p bs')%I.
Lemma coin_exclusive (cp : val) (bs1 bs2 : list bool) :
coin cp bs1 - coin cp bs2 - False.
Proof.
iIntros "H1 H2".
iDestruct "H1" as (c1 p1 b1 bs'1) "(-> & -> & _ & Hp1)".
iDestruct "H2" as (c2 p2 b2 bs'2) "(% & -> & _ & Hp2)".
simplify_eq.
iApply (typed_proph_prop_excl BoolTypedProph). iFrame.
Qed.
Lemma new_coin_spec :
{{{ True }}}
new_coin #()
{{{ c bs, RET c; coin c bs }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (typed_proph_wp_new_proph BoolTypedProph); first done.
iIntros (bs p) "Hp".
wp_apply nondet_bool_spec; first done.
iIntros (b) "_". wp_alloc c as "Hc". wp_pair.
iApply ("HΦ" $! _ (b :: bs)).
iExists c, p, b, bs. by iFrame.
Qed.
Lemma read_coin_spec cp bs :
{{{ coin cp bs }}}
read_coin cp
{{{ b bs', RET #b; bs = b :: bs' coin cp bs }}}.
Proof.
iIntros (Φ) "Hc HΦ".
iDestruct "Hc" as (c p b bs') "[-> [-> [Hc Hp]]]".
wp_lam. wp_load. iApply "HΦ". iSplit; first done.
iExists c, p, b, bs'. by iFrame.
Qed.
Lemma toss_coin_spec cp bs :
{{{ coin cp bs }}}
toss_coin cp
{{{ b bs', RET #(); bs = b :: bs' coin cp bs' }}}.
Proof.
iIntros (Φ) "Hc HΦ".
iDestruct "Hc" as (c p b bs') "[-> [-> [Hc Hp]]]".
wp_lam. wp_pures. wp_apply nondet_bool_spec; first done.
iIntros (r) "_". wp_store.
wp_apply (typed_proph_wp_resolve BoolTypedProph with "[Hp]"); try done.
wp_pures. iIntros (bs) "-> Hp". wp_seq.
iApply "HΦ"; iSplit; first done.
iExists c, p, r, bs. by iFrame.
Qed.
End proof.
Definition clairvoyant_coin_spec_instance `{!heapG Σ} :
clairvoyant_coin_spec.clairvoyant_coin_spec Σ :=
{| clairvoyant_coin_spec.new_coin_spec := new_coin_spec;
clairvoyant_coin_spec.read_coin_spec := read_coin_spec;
clairvoyant_coin_spec.toss_coin_spec := toss_coin_spec;
clairvoyant_coin_spec.coin_exclusive := coin_exclusive |}.
Typeclasses Opaque coin.
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
From iris_examples.proph Require Import eager_coin_spec.
(* Simple implementation of the eager specification. *)
Definition new_eager_coin : val :=
λ: <>, ref (nondet_bool #()).
Definition read_eager_coin : val :=
λ: "c", !"c".
Section proof.
Context `{!heapG Σ}.
Definition eager_coin (c : val) (b : bool) : iProp Σ :=
( (l : loc), c = #l l #b).
Lemma eager_coin_exclusive (c : val) (b1 b2 : bool) :
eager_coin c b1 - eager_coin c b2 - False.
Proof.
iIntros "H1 H2".
iDestruct "H1" as (l1) "[% Hl1]".
iDestruct "H2" as (l2) "[% Hl2]".
simplify_eq.
by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %?.
Qed.
Lemma new_eager_coin_spec :
{{{ True }}}
new_eager_coin #()
{{{ c b, RET c; eager_coin c b }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam. wp_apply nondet_bool_spec; first done.
iIntros (r) "_". wp_alloc l as "Hl". iApply "HΦ". iExists l. by iFrame.
Qed.
Lemma read_eager_coin_spec c b :
{{{ eager_coin c b }}}
read_eager_coin c
{{{ RET #b; eager_coin c b }}}.
Proof.
iIntros (Φ) "Hc HΦ". iDestruct "Hc" as (l) "[-> Hl]".
wp_lam. wp_load. iApply "HΦ". iExists l. by iFrame.
Qed.
End proof.
Definition eager_coin_spec_instance `{!heapG Σ} :
eager_coin_spec.eager_coin_spec Σ :=
{| eager_coin_spec.new_coin_spec := new_eager_coin_spec;
eager_coin_spec.read_coin_spec := read_eager_coin_spec;
eager_coin_spec.coin_exclusive := eager_coin_exclusive |}.
Typeclasses Opaque eager_coin.
From iris.heap_lang Require Export lifting notation.
Set Default Proof Using "Type".
(** Specification for an eager coin. The coin is only ever tossed once, at the
time of its creation with [new_coin]. All subsequent calls to [read_coin] give
the same value. *)
Record eager_coin_spec `{!heapG Σ} := EagerCoinSpec {
(* -- operations -- *)
new_coin: val;
read_coin: val;
(* -- predicates -- *)
coin (c : val) (b : bool) : iProp Σ;
(* -- predicate properties -- *)
coin_exclusive c b1 b2 : coin c b1 - coin c b2 - False;
(* -- operation specs -- *)
new_coin_spec :
{{{ True }}}
new_coin #()
{{{ c b, RET c ; coin c b }}};
read_coin_spec c b :
{{{ coin c b }}}
read_coin c
{{{ RET #b ; coin c b }}};
}.
Arguments eager_coin_spec _ {_}.
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
From iris_examples.proph Require Import eager_coin_spec.
(* Lazy implementation of the eager specification. The value of the coin is
unknown at the time of the creation of the coin. As a consequence, we rely on
a prophecy variable. *)
Definition new_lazy_coin : val :=
λ: <>, (ref NONE, NewProph).
Definition read_lazy_coin : val :=
λ: "cp",
let: "c" := Fst "cp" in
let: "p" := Snd "cp" in
match: !"c" with
NONE => let: "r" := nondet_bool #() in
"c" <- SOME "r";; resolve_proph: "p" to: "r";; "r"
| SOME "b" => "b"
end.
Section proof.
Context `{!heapG Σ}.
Definition val_to_bool (v : val) : bool := bool_decide (v = #true).
Definition prophecy_to_bool (vs : list (val * val)) : bool :=
default false (val_to_bool snd <$> head vs).
Lemma prophecy_to_bool_of_bool (b : bool) v vs :
prophecy_to_bool ((v, #b) :: vs) = b.
Proof. by destruct b. Qed.
Definition lazy_coin (cp : val) (b : bool) : iProp Σ :=
( (c : loc) (p : proph_id) (vs : list (val * val)),
cp = (#c, #p)%V proph p vs
(c SOMEV #b (c NONEV b = prophecy_to_bool vs)))%I.
Lemma lazy_coin_exclusive (cp : val) (b1 b2 : bool) :
lazy_coin cp b1 - lazy_coin cp b2 - False.
Proof.
iIntros "H1 H2".
iDestruct "H1" as (c1 p1 vs1) "(-> & Hp1 & _)".
iDestruct "H2" as (c2 p2 vs2) "(% & Hp2 & _)".
simplify_eq. iApply (proph_exclusive with "Hp1 Hp2").
Qed.
Lemma new_lazy_coin_spec :
{{{ True }}}
new_lazy_coin #()
{{{ c b, RET c; lazy_coin c b }}}.
Proof.
iIntros (Φ) "_ HΦ".
wp_lam.
wp_apply wp_new_proph; first done.
iIntros (vs p) "Hp".
wp_alloc c as "Hc".
wp_pair.
iApply ("HΦ" $! (#c, #p)%V ).
rewrite /lazy_coin; eauto 10 with iFrame.
Qed.
Lemma read_lazy_coin_spec cp b :
{{{ lazy_coin cp b }}}
read_lazy_coin cp
{{{ RET #b; lazy_coin cp b }}}.
Proof.
iIntros (Φ) "Hc HΦ".
iDestruct "Hc" as (c p vs ->) "[Hp [Hc | [Hc ->]]]".
- wp_lam. wp_load. wp_match.
iApply "HΦ".
rewrite /lazy_coin; eauto 10 with iFrame.
- wp_lam. wp_load. wp_match.
wp_apply nondet_bool_spec; first done.
iIntros (r) "_".
wp_let.
wp_store.
wp_apply (wp_resolve_proph with "[Hp]"); first done.
iIntros (ws) "[-> Hws]".
rewrite !prophecy_to_bool_of_bool.
wp_seq.
iApply "HΦ".
rewrite /lazy_coin; eauto with iFrame.
Qed.
End proof.
Definition lazy_coin_spec_instance `{!heapG Σ} :
eager_coin_spec.eager_coin_spec Σ :=
{| eager_coin_spec.new_coin_spec := new_lazy_coin_spec;
eager_coin_spec.read_coin_spec := read_lazy_coin_spec;
eager_coin_spec.coin_exclusive := lazy_coin_exclusive |}.
Typeclasses Opaque lazy_coin.
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
From iris_examples.proph Require Import eager_coin_spec.
From iris_examples.proph.lib Require Import one_shot_proph.
(* Lazy implementation of the eager specification. The value of the coin is
unknown at the time of the creation of the coin. As a consequence, we rely on
a *one-shot* prophecy variable. *)
Definition new_lazy_coin : val :=
λ: <>, (ref NONE, NewProph).
Definition read_lazy_coin : val :=
λ: "cp",
let: "c" := Fst "cp" in
let: "p" := Snd "cp" in
match: !"c" with
NONE => let: "r" := nondet_bool #() in
"c" <- SOME "r";; resolve_proph: "p" to: "r";; "r"
| SOME "b" => "b"
end.
Section proof.
Context `{!heapG Σ}.
Definition val_to_bool (v : val) : bool := bool_decide (v = #true).
Lemma val_to_bool_of_bool (b : bool) :
val_to_bool #b = b.
Proof.
by destruct b.
Qed.
Definition lazy_coin (cp : val) (b : bool) : iProp Σ :=
( (c : loc) (p : proph_id) (v : val),
cp = (#c, #p)%V
(c SOMEV #b (c NONEV proph1 p v b = val_to_bool v)))%I.
Lemma lazy_coin_exclusive (cp : val) (b1 b2 : bool) :
lazy_coin cp b1 - lazy_coin cp b2 - False.
Proof.
iIntros "H1 H2".
iDestruct "H1" as (c1 p1 v1) "[-> H1]".
iDestruct "H2" as (c2 p2 v2) "[% H2]".
simplify_eq.
iDestruct "H1" as "[Hc1 | [Hc1 _]]";
iDestruct "H2" as "[Hc2 | [Hc2 _]]";
by iDestruct (mapsto_valid_2 with "Hc1 Hc2") as %?.
Qed.
Lemma new_lazy_coin_spec :
{{{ True }}}
new_lazy_coin #()
{{{ c b, RET c; lazy_coin c b }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply wp_new_proph1; first done. iIntros (p v) "Hp".
wp_alloc c as "Hc". wp_pair.
iApply ("HΦ" $! (#c, #p)%V).
iExists c, p, v. iSplit; first done. iRight. by iFrame.
Qed.
Lemma read_lazy_coin_spec cp b :
{{{ lazy_coin cp b }}}
read_lazy_coin cp
{{{ RET #b; lazy_coin cp b }}}.
Proof.
iIntros (Φ) "Hc HΦ".
iDestruct "Hc" as (c p v ->) "[Hc | [Hc [Hp ->]]]".
- wp_lam. wp_load. wp_match. iApply "HΦ".
iExists c, p, #(). iSplit; first done. by iLeft.
- wp_lam. wp_load. wp_match.
wp_apply nondet_bool_spec; first done. iIntros (r) "_".
wp_let. wp_store.
wp_apply (wp_resolve1 with "Hp"); first done.
wp_pures. iIntros "->". wp_pures.
rewrite !val_to_bool_of_bool. iApply "HΦ".
iExists c, p, #(). iSplit; first done. by iLeft.
Qed.
End proof.
Definition lazy_coin_spec_instance `{!heapG Σ} :
eager_coin_spec.eager_coin_spec Σ :=
{| eager_coin_spec.new_coin_spec := new_lazy_coin_spec;
eager_coin_spec.read_coin_spec := read_lazy_coin_spec;
eager_coin_spec.coin_exclusive := lazy_coin_exclusive |}.
Typeclasses Opaque lazy_coin.
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
From iris_examples.proph Require Import eager_coin_spec.
From iris_examples.proph.lib Require Import typed_proph.
(* Lazy implementation of the eager specification. The value of the coin is
unknown at the time of the creation of the coin. As a consequence, we rely on
a *typed*, *one-shot* prophecy variable. *)
Definition new_lazy_coin : val :=
λ: <>, (ref NONE, NewProph).
Definition read_lazy_coin : val :=
λ: "cp",
let: "c" := Fst "cp" in
let: "p" := Snd "cp" in
match: !"c" with
NONE => let: "r" := nondet_bool #() in
"c" <- SOME "r";; resolve_proph: "p" to: "r";; "r"
| SOME "b" => "b"
end.
Section proof.
Context `{!heapG Σ}.
Definition lazy_coin (cp : val) (b : bool) : iProp Σ :=
( (c : loc) (p : proph_id),
cp = (#c, #p)%V
(c SOMEV #b (c NONEV (typed_proph1_prop BoolTypedProph) p b)))%I.
Lemma lazy_coin_exclusive (cp : val) (b1 b2 : bool) :
lazy_coin cp b1 - lazy_coin cp b2 - False.
Proof.
iIntros "H1 H2".
iDestruct "H1" as (c1 p1) "[-> H1]".
iDestruct "H2" as (c2 p2) "[% H2]".
simplify_eq.
iDestruct "H1" as "[Hc1 | [Hc1 _]]";
iDestruct "H2" as "[Hc2 | [Hc2 _]]";
by iDestruct (mapsto_valid_2 with "Hc1 Hc2") as %?.
Qed.
Lemma new_lazy_coin_spec :
{{{ True }}}
new_lazy_coin #()
{{{ c b, RET c; lazy_coin c b }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (typed_proph_wp_new_proph1 BoolTypedProph); first done.
iIntros (o p) "Hp". wp_alloc c as "Hc". wp_pair.
iApply ("HΦ" $! (#c, #p)%V).
iExists c, p. iSplit; first done. iRight. by iFrame.