add flip

theories/clutch/examples/awkward_lazy_eager_coin.v

@@ -6,7 +6,7 @@
     the only difference being the use of sequential composition with `f()` in the
     body of the closures. *)
 
-From clutch Require Export clutch lib.flip. 
+From clutch Require Export clutch clutch.lib.flip. 
 Set Default Proof Using "Type*".
 
 (** The lazy/eager coins, without tapes *)

theories/clutch/examples/awkward_probabilistic.v

@@ -13,7 +13,7 @@ NB: e1 and e2 are equivalent only if executed only once. We prove the
 equivalence by adding a guard that returns `NONE` after the first invocation.
 *)
 
-From clutch Require Export clutch lib.flip. 
+From clutch Require Export clutch clutch.lib.flip. 
 From clutch.clutch.examples Require Export one_time_pad.
 
 Set Default Proof Using "Type*".

theories/clutch/examples/counterexample.v

@@ -1,4 +1,4 @@
-From clutch Require Export clutch lib.flip.
+From clutch Require Export clutch clutch.lib.flip.
 Set Default Proof Using "Type*".
 
 (** If we assume that we can freely pick presampling tapes to read from when

theories/clutch/examples/env_bisim.v

@@ -4,7 +4,7 @@
    NB: This example was mentioned as open problem in Aleš Bizjak's thesis.
  *)
 
-From clutch Require Export clutch lib.flip.
+From clutch Require Export clutch clutch.lib.flip.
 Set Default Proof Using "Type*".
 
 (* A diverging term. *)

theories/clutch/examples/flip_once_many_synchronised_coin.v

@@ -18,7 +18,7 @@
    "lazy_alt") and "β" (from eager) synchronised.
  *)
 
-From clutch Require Export clutch lib.flip.
+From clutch Require Export clutch clutch.lib.flip.
 Set Default Proof Using "Type*".
 
 Section proofs.

theories/clutch/examples/geometric.v

@@ -1,6 +1,6 @@
 (* Small demo that Clutch can prove equivalence of recursively defined procedures. *)
 
-From clutch Require Export clutch lib.flip.
+From clutch Require Export clutch clutch.lib.flip.
 Set Default Proof Using "Type*".
 
 Definition geo_true : val := rec: "f" "n" := if: flip then "n" else "f" ("n" + #1).

theories/clutch/examples/id_rec.v

@@ -1,4 +1,4 @@
-From clutch Require Export clutch lib.flip.
+From clutch Require Export clutch clutch.lib.flip.
 Set Default Proof Using "Type*".
 
 Section proofs.

theories/clutch/examples/lazy_eager_coin.v

@@ -1,4 +1,4 @@
-From clutch Require Export clutch lib.flip. 
+From clutch Require Export clutch clutch.lib.flip. 
 Set Default Proof Using "Type*".
 
 (** The lazy/eager coins, without tapes *)

theories/clutch/examples/lazy_int.v

@@ -1,4 +1,4 @@
-From clutch Require Export clutch lib.flip.
+From clutch Require Export clutch clutch.lib.flip.
 From clutch.clutch.examples Require Export sample_int.
 
 Section lazy_int.

theories/clutch/examples/one_time_pad.v

@@ -1,4 +1,4 @@
-From clutch Require Export clutch lib.flip.
+From clutch Require Export clutch clutch.lib.flip.
 Set Default Proof Using "Type*".
 
 Definition xor b1 b2 : expr :=

theories/clutch/examples/sample_int.v

@@ -1,4 +1,4 @@
-From clutch Require Export clutch lib.flip lib.conversion.
+From clutch Require Export clutch clutch.lib.flip clutch.lib.conversion.
 
 (* This is a library for sampling integers in the set {0, ..., 2^n-1}
    for some natural number n > 0.

theories/clutch/examples/von_neumann_coin.v

@@ -1,5 +1,5 @@
 (* A zoo of variants of Von Neumann's construction of a fair coin from a biased coin. *)
-From clutch Require Export clutch lib.flip.
+From clutch Require Export clutch clutch.lib.flip.
 Set Default Proof Using "Type*".
 
 Section proofs.

theories/clutch/lib/flip.v

@@ -2,7 +2,7 @@
 From stdpp Require Import namespaces.
 From iris.proofmode Require Import
   coq_tactics ltac_tactics sel_patterns environments reduction proofmode.
-From clutch Require Import clutch lib.conversion.
+From clutch Require Import clutch clutch.lib.conversion.
 
 Definition flipL : val := λ: "e", int_to_bool (rand("e") #1%nat).
 Definition flip : expr := (flipL #()).

theories/coneris/examples/parallel_add.v

@@ -0,0 +1,27 @@
+From clutch.coneris Require Import coneris par lib.flip.
+
+Local Open Scope Z.
+
+Section simple_parallel_add.
+Definition simple_parallel_add : expr :=
+  let: "r" := ref #0 in
+  ( if: #0 < rand #2 then FAA "r" #1 else #())
+  |||
+  (if: #0 < rand #2 then FAA "r" #1 else #())
+  ;;
+  !"r".
+
+End simple_parallel_add.
+
+Section parallel_add.
+
+Definition parallel_add : expr :=
+  let: "r" := ref #0 in
+  ( if: flip then FAA "r" #1 else #())
+  |||
+  (if: #0 < rand #2 then FAA "r" #1 else #())
+  ;;
+  !"r".
+
+End parallel_add.
+

theories/coneris/lib/conversion.v

@@ -0,0 +1,41 @@
+From clutch.coneris Require Import coneris.
+
+Definition bool_to_int : val :=
+  λ: "b",
+    if: "b" = #false then
+      #0
+    else #1.
+
+Definition int_to_bool : val :=
+  λ: "z",
+    if: "z" = #0 then #false      
+    else #true.
+
+Section specs.
+  Context `{!conerisGS Σ}.
+
+  Lemma wp_bool_to_int (b: bool) E :
+    {{{ True }}}
+      bool_to_int #b @ E
+    {{{ RET #(Z.b2z b); True%I}}}.
+  Proof.
+    iIntros (Φ) "_ HΦ".
+    rewrite /bool_to_int.
+    wp_pures. destruct b; case_bool_decide as Heq; try congruence; wp_pures; by iApply "HΦ".
+  Qed.
+
+  Lemma wp_int_to_bool (z : Z) E :    
+    {{{ True }}}
+      int_to_bool #z @ E
+    {{{ RET #(Z_to_bool z); True%I}}}.
+  Proof. 
+    iIntros (Φ) "_ HΦ".
+    rewrite /int_to_bool.
+    wp_pures.
+    case_bool_decide as Heq; simplify_eq; wp_pures. 
+    - by iApply "HΦ".
+    - rewrite Z_to_bool_neq_0; [|by intros ->].
+      by iApply "HΦ".
+  Qed.
+
+End specs.       

theories/coneris/lib/flip.v

@@ -0,0 +1,124 @@
+(** * Derived laws for a fair coin flip *)
+From stdpp Require Import namespaces.
+From iris.proofmode Require Import
+  coq_tactics ltac_tactics sel_patterns environments reduction proofmode.
+From clutch.coneris Require Import coneris lib.conversion.
+
+Definition flipL : val := λ: "e", int_to_bool (rand("e") #1%nat).
+Definition flip : expr := (flipL #()).
+Definition allocB := alloc #1%nat.
+
+Definition tapeB (bs : list bool) : tape := (1; bool_to_fin <$> bs).
+Definition bool_tape `{conerisGS Σ} l bs : iProp Σ := l ↪ tapeB bs.
+
+Notation "l ↪B bs" := (bool_tape l bs)
+  (at level 20, format "l  ↪B  bs") : bi_scope.
+
+Section specs.
+  Context `{conerisGS Σ}.
+
+  Lemma tape_conversion_bool_nat α bs:
+    α ↪B (bs) ⊣⊢ α ↪N (1; (λ b:bool, if b then 1 else 0) <$> bs).
+  Proof.
+    rewrite /bool_tape/tapeB.
+    iSplit.
+    - iIntros. iExists (bool_to_fin <$> bs).
+      iFrame.
+      iPureIntro.
+      rewrite -list_fmap_compose.
+      f_equal.
+      apply functional_extensionality_dep; intros []; done.
+    - iIntros "[%[%?]]".
+      replace fs with (bool_to_fin <$> bs); first done.
+      generalize dependent fs.
+      induction bs as [|a].
+      + simpl. intros.
+        by erewrite fmap_nil_inv.
+      + intros fs H0. destruct fs; first done.
+        * rewrite !fmap_cons in H0.
+          simplify_eq.
+          apply IHbs in H1.
+          rewrite fmap_cons.
+          f_equal; last done.
+          destruct a; subst.
+          -- inv_fin t; first done; intros t.
+             by inv_fin t.
+          -- inv_fin t; first done; intros t; by inv_fin t.
+  Qed.
+
+  Lemma tape_conversion_nat_bool α ns:
+    α ↪N (1;ns) ⊢ α ↪B ((λ n, n=?1) <$> ns).
+  Proof.
+    iIntros "[%fs [%?]]".
+    rewrite tape_conversion_bool_nat.
+    iExists fs.
+    iFrame.
+    subst.
+    iPureIntro.
+    rewrite -!list_fmap_compose.
+    induction fs as [|x]; first done.
+    rewrite !fmap_cons. f_equal; last done.
+    inv_fin x; first done; intros x.
+    inv_fin x; first done; intros x.
+    inv_fin x.
+  Qed. 
+
+  Lemma wp_allocB_tape E :
+    {{{ True }}} allocB @ E {{{ α, RET #lbl:α; α ↪B [] }}}.
+  Proof. iIntros (Φ) "_ HΦ". iApply wp_alloc_tape; first done.
+         iModIntro. iIntros. erewrite tape_conversion_nat_bool. simpl.
+         by iApply "HΦ".
+  Qed.
+
+  Lemma wp_flip E :
+    {{{ True }}} flip @ E {{{ (b : bool), RET #(LitBool b); True }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ". rewrite /flip/flipL.
+    wp_pures.
+    wp_bind (rand(_) _)%E.
+    wp_apply (wp_rand 1 with "[//]").
+    iIntros (?) "_ /=".
+    wp_apply (wp_int_to_bool with "[//]").
+    iIntros "_".
+    by iApply "HΦ".
+  Qed.
+
+  Lemma wp_flipL E α b bs :
+    {{{ ▷ α ↪B (b :: bs) }}} flipL #lbl:α @ E {{{ RET #(LitBool b); α ↪B bs }}}.
+  Proof.
+    iIntros (Φ) ">Hl HΦ". rewrite /flip/flipL.
+    wp_pures.
+    wp_bind (rand(_) _)%E.
+    rewrite tape_conversion_bool_nat; simpl.
+    wp_apply (wp_rand_tape 1 with "Hl").
+    iIntros "[Hl _] /=".
+    wp_apply (wp_int_to_bool with "[//]").
+    iIntros "_".
+    destruct b; rewrite Z_to_bool_of_nat.
+    - rewrite nat_to_bool_neq_0; last lia.
+      iApply "HΦ".
+      rewrite tape_conversion_bool_nat. iFrame.
+    - rewrite nat_to_bool_eq_0.
+      iApply "HΦ".
+      rewrite tape_conversion_bool_nat. iFrame.
+  Qed.
+
+
+  Lemma wp_flipL_empty E α :
+    {{{ ▷ α ↪B [] }}} flipL #lbl:α @ E {{{ b, RET #(LitBool b); α ↪B [] }}}.
+  Proof.
+    iIntros (Φ) ">Hl HΦ". rewrite /flip/flipL.
+    wp_pures.
+    wp_bind (rand(_) _)%E.
+    erewrite tape_conversion_bool_nat.
+    wp_apply (wp_rand_tape_empty with "Hl").
+    iIntros (n) "[Hl _] /=".
+    wp_apply (wp_int_to_bool with "[//]").
+    iIntros "_".
+    iApply "HΦ".
+    by rewrite tape_conversion_nat_bool. 
+  Qed.
+
+
+Global Opaque tapeB.
+End specs.