From 1b6cfe1a73230c393a097eafd0d4226f1a173db3 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Thu, 13 Jun 2019 16:57:34 +0200
Subject: [PATCH] Add the lazy_coin example
---
_CoqProject | 3 +-
theories/heap_lang/lib/coin_flip.v | 91 ----------------------------
theories/heap_lang/lib/lazy_coin.v | 68 +++++++++++++++++++++
theories/heap_lang/lib/nondet_bool.v | 25 ++++++++
4 files changed, 95 insertions(+), 92 deletions(-)
delete mode 100644 theories/heap_lang/lib/coin_flip.v
create mode 100644 theories/heap_lang/lib/lazy_coin.v
create mode 100644 theories/heap_lang/lib/nondet_bool.v
diff --git a/_CoqProject b/_CoqProject
index c03ec564b..a44cf5215 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -110,7 +110,8 @@ theories/heap_lang/lib/assert.v
theories/heap_lang/lib/lock.v
theories/heap_lang/lib/spin_lock.v
theories/heap_lang/lib/ticket_lock.v
-theories/heap_lang/lib/coin_flip.v
+theories/heap_lang/lib/nondet_bool.v
+theories/heap_lang/lib/lazy_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/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
deleted file mode 100644
index 08545fa3b..000000000
--- a/theories/heap_lang/lib/coin_flip.v
+++ /dev/null
@@ -1,91 +0,0 @@
-From iris.base_logic.lib Require Export invariants.
-From iris.program_logic Require Export atomic.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
-
-(** Nondeterminism and Speculation:
- Implementing "Late choice versus early choice" example from
- Logical Relations for Fine-Grained Concurrency by Turon et al. (POPL'13) *)
-
-Definition rand: val :=
- λ: "_",
- let: "y" := ref #false in
- Fork ("y" <- #true) ;;
- !"y".
-
-Definition earlyChoice: val :=
- λ: "x",
- let: "r" := rand #() in
- "x" <- #0 ;;
- "r".
-
-Definition lateChoice: val :=
- λ: "x",
- let: "p" := NewProph in
- "x" <- #0 ;;
- let: "r" := rand #() in
- resolve_proph: "p" to: "r" ;;
- "r".
-
-Section coinflip.
- Context `{!heapG Σ}.
-
- Local Definition N := nroot .@ "coin".
-
- Lemma rand_spec :
- {{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
- Proof.
- iIntros (Φ) "_ HP". wp_lam. wp_alloc l as "Hl".
- iMod (inv_alloc N _ (∃ (b: bool), l ↦ #b)%I with "[Hl]") as "#Hinv"; first by eauto.
- wp_apply wp_fork.
- - iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
- - wp_pures. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
- iApply "HP". done.
- Qed.
-
- Lemma earlyChoice_spec (x: loc) :
- <<< x ↦ - >>>
- earlyChoice #x
- @ ⊤
- <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
- Proof.
- iIntros (Φ) "AU". wp_lam.
- wp_apply rand_spec; first done.
- iIntros (b) "_". wp_let.
- wp_bind (_ <- _)%E.
- iMod "AU" as "[Hl [_ Hclose]]".
- iDestruct "Hl" as (v) "Hl".
- wp_store.
- iMod ("Hclose" with "[Hl]") as "HΦ"; first by eauto.
- iModIntro. wp_seq. done.
- Qed.
-
- Definition extract_bool (l : list (val * val)) : bool :=
- match l with
- | (_, LitV (LitBool b)) :: _ => b
- | _ => true
- end.
-
- Lemma lateChoice_spec (x: loc) :
- <<< x ↦ - >>>
- lateChoice #x
- @ ⊤
- <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
- Proof.
- iIntros (Φ) "AU". wp_lam.
- wp_apply wp_new_proph; first done.
- iIntros (v p) "Hp".
- wp_let.
- wp_bind (_ <- _)%E.
- iMod "AU" as "[Hl [_ Hclose]]".
- iDestruct "Hl" as (v') "Hl".
- wp_store.
- iMod ("Hclose" $! (extract_bool v) with "[Hl]") as "HΦ"; first by eauto.
- iModIntro. wp_apply rand_spec; try done.
- iIntros (b') "_".
- wp_apply (wp_resolve_proph with "Hp").
- iIntros (vs) "[HEq _]". iDestruct "HEq" as "->". wp_seq. done.
- Qed.
-
-End coinflip.
diff --git a/theories/heap_lang/lib/lazy_coin.v b/theories/heap_lang/lib/lazy_coin.v
new file mode 100644
index 000000000..c1acf7ed5
--- /dev/null
+++ b/theories/heap_lang/lib/lazy_coin.v
@@ -0,0 +1,68 @@
+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.
+
+Definition new_coin: val := λ: <>, (ref NONE, NewProph).
+
+Definition read_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 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 new_coin_spec : {{{ True }}} new_coin #() {{{ c b, RET c; 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 /coin; eauto 10 with iFrame.
+ Qed.
+
+ Lemma read_coin_spec cp b :
+ {{{ coin cp b }}} read_coin cp {{{ RET #b; 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 /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 /coin; eauto with iFrame.
+ Qed.
+
+End proof.
diff --git a/theories/heap_lang/lib/nondet_bool.v b/theories/heap_lang/lib/nondet_bool.v
new file mode 100644
index 000000000..fcf7f6a03
--- /dev/null
+++ b/theories/heap_lang/lib/nondet_bool.v
@@ -0,0 +1,25 @@
+From iris.base_logic Require Export invariants.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang proofmode notation.
+
+Definition nondet_bool : val :=
+ λ: <>, let: "l" := ref #true in Fork ("l" <- #false);; !"l".
+
+Section proof.
+ Context `{!heapG Σ}.
+
+ Lemma nondet_bool_spec : {{{ True }}} nondet_bool #() {{{ (b : bool), RET #b; True }}}.
+ Proof.
+ iIntros (Φ) "_ HΦ".
+ wp_lam. wp_alloc l as "Hl". wp_let.
+ pose proof (nroot .@ "rnd") as rndN.
+ iMod (inv_alloc rndN _ (∃ (b : bool), l ↦ #b)%I with "[Hl]") as "#Hinv";
+ first by eauto.
+ wp_apply wp_fork.
+ - iInv rndN as (?) "?". wp_store; eauto.
+ - wp_seq. iInv rndN as (?) "?". wp_load.
+ iSplitR "HΦ"; first by eauto.
+ by iApply "HΦ".
+ Qed.
+
+End proof.
--
GitLab