remove uniform extern

dafny-lang · Nov 6, 2023 · c342f38 · c342f38
1 parent a8ad7d5
commit c342f38
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 19 deletions.
diff --git a/src/Dafny-VMC.dfy b/src/Dafny-VMC.dfy
@@ -16,10 +16,6 @@ module DafnyVMC {
     constructor {:extern} ()
   }
 
-/*   class DRandomExternUniform extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.Trait, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitExtern, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
-    constructor {:extern} ()
-  } */
-
   class DRandomExternUniform extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.TraitExtern, Bernoulli.Implementation.Trait, Uniform.Implementation.Trait, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
     constructor {:extern} ()
   }

diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy
@@ -32,19 +32,4 @@ module Uniform.Implementation {
       reveal Model.Sample();
     }
   }
-
-  method {:extern "DRandomUniform", "Uniform"} ExternUniformSample(n: nat) returns (u: nat)
-
-  trait {:termination false} TraitExtern extends Interface.Trait {
-    method UniformSample(n: nat) returns (u: nat)
-      modifies this
-      decreases *
-      requires n > 0
-      ensures u < n
-      ensures Model.Sample(n)(old(s)) == Monad.Result(u, s)
-    {
-      u := ExternUniformSample(n);
-      assume {:axiom} false; // assume correctness of extern implementation
-    }
-  }
 }