From 4acdc7743fc932644c6cf13a9ac381a93f10ee5e Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Thu, 20 Jun 2019 16:13:57 +0200
Subject: [PATCH] Add clairvoyant_coin example

---
 _CoqProject                               |  1 +
 theories/heap_lang/lib/clairvoyant_coin.v | 84 +++++++++++++++++++++++
 2 files changed, 85 insertions(+)
 create mode 100644 theories/heap_lang/lib/clairvoyant_coin.v

diff --git a/_CoqProject b/_CoqProject
index a44cf5215..071cd83b1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -112,6 +112,7 @@ theories/heap_lang/lib/spin_lock.v
 theories/heap_lang/lib/ticket_lock.v
 theories/heap_lang/lib/nondet_bool.v
 theories/heap_lang/lib/lazy_coin.v
+theories/heap_lang/lib/clairvoyant_coin.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
diff --git a/theories/heap_lang/lib/clairvoyant_coin.v b/theories/heap_lang/lib/clairvoyant_coin.v
new file mode 100644
index 000000000..87aa3c437
--- /dev/null
+++ b/theories/heap_lang/lib/clairvoyant_coin.v
@@ -0,0 +1,84 @@
+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.
+
+(** The 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. The [read_coin] operation always returns the head of [bs] and the
+[toss_coin] operation takes the [tail] of [bs]. *)
+
+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 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.
-- 
GitLab