From fdc7a867b1fd2649ef3a8930e0926c4ffb443cfe Mon Sep 17 00:00:00 2001
From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com>
Date: Wed, 6 Mar 2024 17:01:36 +0000
Subject: [PATCH] Remove Coin (#162)

Depends on https://github.com/dafny-lang/Dafny-VMC/pull/161

By submitting this pull request, I confirm that my contribution is made
under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).

---------

Co-authored-by: John Tristan <trjohnb@amazon.com>
---
 audit.log                                 |  1 -
 src/Distributions/Coin/Implementation.dfy | 26 -----------------------
 src/Distributions/Coin/Interface.dfy      | 20 -----------------
 src/Distributions/Coin/Model.dfy          | 13 ------------
 src/Distributions/Uniform/Correctness.dfy |  3 ---
 5 files changed, 63 deletions(-)
 delete mode 100644 src/Distributions/Coin/Implementation.dfy
 delete mode 100644 src/Distributions/Coin/Interface.dfy
 delete mode 100644 src/Distributions/Coin/Model.dfy

diff --git a/audit.log b/audit.log
index 2e9aa2fd..6777b8da 100644
--- a/audit.log
+++ b/audit.log
@@ -1,5 +1,4 @@
 src/Distributions/Uniform/Correctness.dfy(31,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Uniform/Correctness.dfy(36,17): SampleCoin: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/Uniform/Model.dfy(19,33): Sample: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/Uniform/Model.dfy(46,17): IntervalSampleIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Independence.dfy(30,27): IsIndep: Declaration has explicit `{:axiom}` attribute. 
diff --git a/src/Distributions/Coin/Implementation.dfy b/src/Distributions/Coin/Implementation.dfy
deleted file mode 100644
index 6f38a9d8..00000000
--- a/src/Distributions/Coin/Implementation.dfy
+++ /dev/null
@@ -1,26 +0,0 @@
-/*******************************************************************************
- *  Copyright by the contributors to the Dafny Project
- *  SPDX-License-Identifier: MIT
- *******************************************************************************/
-
-module Coin.Implementation {
-  import Model
-  import Monad
-  import Interface
-  import Uniform
-
-  trait {:termination false} Trait extends Interface.Trait {
-
-    method CoinSample() returns (b: bool)
-      modifies `s
-      decreases *
-      ensures Model.Sample(old(s)) == Monad.Result(b, s)
-    {
-      var x := UniformSample(2);
-      b := if x == 1 then true else false;
-      Uniform.Correctness.SampleCoin(old(s));
-    }
-
-  }
-
-}
\ No newline at end of file
diff --git a/src/Distributions/Coin/Interface.dfy b/src/Distributions/Coin/Interface.dfy
deleted file mode 100644
index a28e5363..00000000
--- a/src/Distributions/Coin/Interface.dfy
+++ /dev/null
@@ -1,20 +0,0 @@
-/*******************************************************************************
- *  Copyright by the contributors to the Dafny Project
- *  SPDX-License-Identifier: MIT
- *******************************************************************************/
-
-module Coin.Interface {
-  import Monad
-  import Rand
-  import Model
-  import Uniform
-
-  trait {:termination false} Trait extends Uniform.Interface.Trait {
-
-    method CoinSample() returns (b: bool)
-      modifies `s
-      decreases *
-      ensures Model.Sample(old(s)) == Monad.Result(b, s)
-
-  }
-}
diff --git a/src/Distributions/Coin/Model.dfy b/src/Distributions/Coin/Model.dfy
deleted file mode 100644
index a6aef4ed..00000000
--- a/src/Distributions/Coin/Model.dfy
+++ /dev/null
@@ -1,13 +0,0 @@
-/*******************************************************************************
- *  Copyright by the contributors to the Dafny Project
- *  SPDX-License-Identifier: MIT
- *******************************************************************************/
-
-module Coin.Model {
-  import Rand
-  import Monad
-
-  function Sample(s: Rand.Bitstream): Monad.Result<bool> {
-    Monad.Coin(s)
-  }
-}
diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy
index e8ce22b0..ca2dc0c7 100644
--- a/src/Distributions/Uniform/Correctness.dfy
+++ b/src/Distributions/Uniform/Correctness.dfy
@@ -33,9 +33,6 @@ module Uniform.Correctness {
     ensures SampleEquals(n, i) in Rand.eventSpace
     ensures Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real)
 
-  lemma {:axiom} SampleCoin(s: Rand.Bitstream)
-    ensures Model.Sample(2)(s)== Monad.Coin(s).Map(b => if b then 1 else 0)
-
   // Correctness theorem for Model.IntervalSample
   lemma UniformFullIntervalCorrectness(a: int, b: int, i: int)
     requires a <= i < b