Remove all include statements (#83)

Remove includes <small>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).</small>
dafny-lang · Oct 6, 2023 · 77237ef · 77237ef
1 parent 513ab2e
commit 77237ef
Show file tree

Hide file tree

Showing 43 changed files with 50 additions and 189 deletions.
diff --git a/audit.log b/audit.log
@@ -1,25 +1,25 @@
-src/Distributions/Coin/Interface.dfy(23,6): CoinSample: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/Uniform/Correctness.dfy(167,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Uniform/Implementation.dfy(47,6): UniformSample: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/Uniform/Model.dfy(41,17): SampleTerminates: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Coin/Interface.dfy(20,6): CoinSample: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/Uniform/Correctness.dfy(157,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Implementation.dfy(43,6): UniformSample: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/Uniform/Model.dfy(34,17): SampleTerminates: Declaration has explicit `{:axiom}` attribute. 
 src/Math/MeasureTheory.dfy(150,17): CountableSumOfZeroesIsZero: Declaration has explicit `{:axiom}` attribute. 
 src/Math/MeasureTheory.dfy(25,4): CountableSum: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/Independence.dfy(32,27): IsIndepFn: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(38,17): IsIndepFnImpliesFstMeasurableBool: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(42,17): IsIndepFnImpliesFstMeasurableNat: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(46,17): IsIndepFnImpliesSndMeasurable: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(50,17): IsIndepFnImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(55,17): DeconstructIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(59,17): ReturnIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(63,17): IndepFnIsCompositional: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Monad.dfy(139,17): TailIsRNG: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Monad.dfy(143,17): HeadIsMeasurable: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Monad.dfy(150,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Monad.dfy(156,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomNumberGenerator.dfy(15,21): IsRNG: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomNumberGenerator.dfy(29,17): RNGHasMeasure: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(170,17): EnsureProbWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(176,17): ProbUntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(188,17): ProbUntilAsBind: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(202,4): EnsureProbUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(44,4): ProbWhile: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Independence.dfy(28,27): IsIndepFn: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(34,17): IsIndepFnImpliesFstMeasurableBool: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(38,17): IsIndepFnImpliesFstMeasurableNat: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(42,17): IsIndepFnImpliesSndMeasurable: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(46,17): IsIndepFnImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(51,17): DeconstructIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(55,17): ReturnIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(59,17): IndepFnIsCompositional: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(136,17): TailIsRNG: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(140,17): HeadIsMeasurable: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(147,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(153,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/RandomNumberGenerator.dfy(13,21): IsRNG: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/RandomNumberGenerator.dfy(27,17): RNGHasMeasure: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/WhileAndUntil.dfy(165,17): EnsureProbWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/WhileAndUntil.dfy(171,17): ProbUntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/WhileAndUntil.dfy(183,17): ProbUntilAsBind: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/WhileAndUntil.dfy(197,4): EnsureProbUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/WhileAndUntil.dfy(39,4): ProbWhile: Definition has `assume {:axiom}` statement in body. 
diff --git a/docs/dafny/ExamplesExternUniform.dfy b/docs/dafny/ExamplesExternUniform.dfy
@@ -3,11 +3,7 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-// RUN: %verify "%s"
-
-include "../../src/Dafny-VMC.dfy"
-
-module RandomExamples {
+module RandomExamples.ExternUniform {
   import Rationals
   import DafnyVMC
 

diff --git a/docs/dafny/ExamplesFoundational.dfy b/docs/dafny/ExamplesFoundational.dfy
@@ -3,11 +3,7 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-// RUN: %verify "%s"
-
-include "../../src/Dafny-VMC.dfy"
-
-module RandomExamples {
+module RandomExamples.Foundational {
   import Rationals
   import DafnyVMC
 

diff --git a/scripts/build.sh b/scripts/build.sh
@@ -14,4 +14,4 @@ then
   exit 1
 fi
 
-$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG src/Dafny-VMC.dfy -o build/$TARGET_LANG/Dafny-VMC
+$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG src/Dafny-VMC.dfy -o build/$TARGET_LANG/Dafny-VMC dfyconfig.toml --no-verify
diff --git a/scripts/gendoc.sh b/scripts/gendoc.sh
@@ -18,6 +18,6 @@ echo Generating Dafny documentation...
 $DAFNY doc dfyconfig.toml --output docs/dafny/dafny-doc/
 
 echo Generating Java documentation...
-$DAFNY translate java src/Dafny-VMC.dfy
+$DAFNY translate java src/Dafny-VMC.dfy --no-verify
 cp $DAFNYSOURCE/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/*.java src/Dafny-VMC-java/dafny/
 javadoc -d docs/java/java-doc/ -sourcepath src/Dafny-VMC-java -package DafnyVMC
diff --git a/scripts/test.sh b/scripts/test.sh
@@ -16,12 +16,28 @@ fi
 
 echo Running $TARGET_LANG tests...
 echo "Running tests/TestsFoundational.dfy:"
-time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG tests/TestsFoundational.dfy
+time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 echo "Running tests/TestsExternUniform.dfy:"
-time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG tests/TestsExternUniform.dfy
+time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml  --no-verify
 
 echo Running $TARGET_LANG documentation...
-echo "Running docs/ExamplesFoundational.dfy"
-$DAFNY run docs/dafny/ExamplesFoundational.dfy --target:$TARGET_LANG --input src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG --input src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG
-echo "docs/ExamplesExternUniform.dfy"
-$DAFNY run docs/dafny/ExamplesExternUniform.dfy --target:$TARGET_LANG --input src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG --input src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG
+
+echo "Building docs/dafny/ExamplesFoundational.dfy..." 
+$DAFNY build docs/dafny/ExamplesFoundational.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG dfyconfig.toml --no-verify
+echo "Executing compiled docs/dafny/ExamplesFoundational.dfy:" 
+if [ "$TARGET_LANG" = "cs" ]
+then
+  dotnet docs/dafny/ExamplesFoundational.dll
+else
+  java -jar docs/dafny/ExamplesFoundational.jar
+fi
+
+echo "Building docs/dafny/ExamplesExternUniform.dfy..." 
+$DAFNY build docs/dafny/ExamplesExternUniform.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG dfyconfig.toml --no-verify
+echo "Executing compiled docs/dafny/ExamplesExternUniform.dfy:" 
+if [ "$TARGET_LANG" = "cs" ]
+then
+  dotnet docs/dafny/ExamplesExternUniform.dll
+else
+  java -jar docs/dafny/ExamplesExternUniform.jar
+fi
diff --git a/scripts/verify.sh b/scripts/verify.sh
@@ -9,4 +9,4 @@ then
 fi
 
 echo Verifying the proofs...
-time $DAFNY verify dfyconfig.toml
+time $DAFNY verify dfyconfig.toml docs/dafny/ExamplesExternUniform.dfy docs/dafny/ExamplesFoundational.dfy tests/Tests.dfy tests/TestsExternUniform.dfy tests/TestsFoundational.dfy
diff --git a/src/Dafny-VMC.dfy b/src/Dafny-VMC.dfy
@@ -3,16 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-// RUN: %verify "%s"
-
-include "Distributions/Coin/Coin.dfy"
-include "Distributions/Bernoulli/Bernoulli.dfy"
-include "Distributions/BernoulliExpNeg/BernoulliExpNeg.dfy"
-include "Distributions/DiscreteGaussian/DiscreteGaussian.dfy"
-include "Distributions/DiscreteLaplace/DiscreteLaplace.dfy"
-include "Distributions/UniformPowerOfTwo/UniformPowerOfTwo.dfy"
-include "Distributions/Uniform/Uniform.dfy"
-
 module DafnyVMC {
   import Coin
   import Bernoulli

diff --git a/src/Distributions/Bernoulli/Bernoulli.dfy b/src/Distributions/Bernoulli/Bernoulli.dfy
diff --git a/src/Distributions/Bernoulli/Correctness.dfy b/src/Distributions/Bernoulli/Correctness.dfy
@@ -3,14 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/MeasureTheory.dfy"
-include "../../Math/Helper.dfy"
-include "../Uniform/Uniform.dfy"
-include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
-include "../../ProbabilisticProgramming/Independence.dfy"
-include "../../ProbabilisticProgramming/Monad.dfy"
-include "Model.dfy"
-
 module Bernoulli.Correctness {
   import MeasureTheory
   import Helper

diff --git a/src/Distributions/Bernoulli/Implementation.dfy b/src/Distributions/Bernoulli/Implementation.dfy
@@ -3,10 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Rationals.dfy"
-include "Interface.dfy"
-include "Model.dfy"
-
 module Bernoulli.Implementation {
   import Rationals
   import Model

diff --git a/src/Distributions/Bernoulli/Interface.dfy b/src/Distributions/Bernoulli/Interface.dfy
@@ -3,10 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Rationals.dfy"
-include "../Uniform/Uniform.dfy"
-include "Model.dfy"
-
 module Bernoulli.Interface {
   import Rationals
   import Uniform

diff --git a/src/Distributions/Bernoulli/Model.dfy b/src/Distributions/Bernoulli/Model.dfy
@@ -3,9 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../Uniform/Uniform.dfy"
-include "../../ProbabilisticProgramming/Monad.dfy"
-
 module Bernoulli.Model {
   import Uniform
   import Monad

diff --git a/src/Distributions/BernoulliExpNeg/BernoulliExpNeg.dfy b/src/Distributions/BernoulliExpNeg/BernoulliExpNeg.dfy
diff --git a/src/Distributions/BernoulliExpNeg/Implementation.dfy b/src/Distributions/BernoulliExpNeg/Implementation.dfy
@@ -3,9 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Rationals.dfy"
-include "Interface.dfy"
-
 module BernoulliExpNeg.Implementation {
   import Rationals
   import Interface

diff --git a/src/Distributions/BernoulliExpNeg/Interface.dfy b/src/Distributions/BernoulliExpNeg/Interface.dfy
@@ -3,9 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Rationals.dfy"
-include "../Bernoulli/Bernoulli.dfy"
-
 module BernoulliExpNeg.Interface {
   import Rationals
   import Bernoulli

diff --git a/src/Distributions/Coin/Coin.dfy b/src/Distributions/Coin/Coin.dfy
diff --git a/src/Distributions/Coin/Interface.dfy b/src/Distributions/Coin/Interface.dfy
@@ -3,9 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
-include "Model.dfy"
-
 module Coin.Interface {
   import RandomNumberGenerator
   import Model

diff --git a/src/Distributions/Coin/Model.dfy b/src/Distributions/Coin/Model.dfy
@@ -3,9 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
-include "../../ProbabilisticProgramming/Monad.dfy"
-
 module Coin.Model {
   import RandomNumberGenerator
   import Monad

diff --git a/src/Distributions/DiscreteGaussian/DiscreteGaussian.dfy b/src/Distributions/DiscreteGaussian/DiscreteGaussian.dfy
diff --git a/src/Distributions/DiscreteGaussian/Implementation.dfy b/src/Distributions/DiscreteGaussian/Implementation.dfy
@@ -3,9 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Rationals.dfy"
-include "Interface.dfy"
-
 module DiscreteGaussian.Implementation {
   import Rationals
   import Interface

diff --git a/src/Distributions/DiscreteGaussian/Interface.dfy b/src/Distributions/DiscreteGaussian/Interface.dfy
@@ -3,10 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Rationals.dfy"
-include "../BernoulliExpNeg/BernoulliExpNeg.dfy"
-include "../DiscreteLaplace/DiscreteLaplace.dfy"
-
 module DiscreteGaussian.Interface {
   import Rationals
   import BernoulliExpNeg

diff --git a/src/Distributions/DiscreteLaplace/DiscreteLaplace.dfy b/src/Distributions/DiscreteLaplace/DiscreteLaplace.dfy
diff --git a/src/Distributions/DiscreteLaplace/Implementation.dfy b/src/Distributions/DiscreteLaplace/Implementation.dfy
@@ -3,9 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Rationals.dfy"
-include "Interface.dfy"
-
 module DiscreteLaplace.Implementation {
   import Rationals
   import Interface

diff --git a/src/Distributions/DiscreteLaplace/Interface.dfy b/src/Distributions/DiscreteLaplace/Interface.dfy
@@ -3,11 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Rationals.dfy"
-include "../Bernoulli/Bernoulli.dfy"
-include "../Uniform/Uniform.dfy"
-include "../BernoulliExpNeg/BernoulliExpNeg.dfy"
-
 module DiscreteLaplace.Interface {
   import Rationals
   import Bernoulli

diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy
@@ -3,16 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Helper.dfy"
-include "../../Math/MeasureTheory.dfy"
-include "../../ProbabilisticProgramming/Monad.dfy"
-include "../../ProbabilisticProgramming/Independence.dfy"
-include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
-include "../../ProbabilisticProgramming/Quantifier.dfy"
-include "../../ProbabilisticProgramming/WhileAndUntil.dfy"
-include "../UniformPowerOfTwo/UniformPowerOfTwo.dfy"
-include "Model.dfy"
-
 module Uniform.Correctness {
   import Helper
   import Monad

diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy
@@ -3,10 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../UniformPowerOfTwo/UniformPowerOfTwo.dfy"
-include "Interface.dfy"
-include "Model.dfy"
-
 module Uniform.Implementation {
   import UniformPowerOfTwo
   import Model

diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy
@@ -3,10 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../Coin/Coin.dfy"
-include "../UniformPowerOfTwo/UniformPowerOfTwo.dfy"
-include "Model.dfy"
-
 module Uniform.Interface {
   import Coin
   import Model

diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy
@@ -3,13 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
-include "../../ProbabilisticProgramming/Monad.dfy"
-include "../../ProbabilisticProgramming/Independence.dfy"
-include "../../ProbabilisticProgramming/Quantifier.dfy"
-include "../../ProbabilisticProgramming/WhileAndUntil.dfy"
-include "../UniformPowerOfTwo/UniformPowerOfTwo.dfy"
-
 module Uniform.Model {
   import RandomNumberGenerator
   import Quantifier

diff --git a/src/Distributions/Uniform/Uniform.dfy b/src/Distributions/Uniform/Uniform.dfy
diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy
@@ -3,15 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../../Math/Helper.dfy"
-include "../../Math/MeasureTheory.dfy"
-include "../../ProbabilisticProgramming/Monad.dfy"
-include "../../ProbabilisticProgramming/Independence.dfy"
-include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
-include "../../ProbabilisticProgramming/Quantifier.dfy"
-include "../../ProbabilisticProgramming/WhileAndUntil.dfy"
-include "Model.dfy"
-
 module UniformPowerOfTwo.Correctness {
   import Helper
   import Monad

diff --git a/src/Distributions/UniformPowerOfTwo/Implementation.dfy b/src/Distributions/UniformPowerOfTwo/Implementation.dfy
@@ -3,9 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "Interface.dfy"
-include "Model.dfy"
-
 module UniformPowerOfTwo.Implementation {
   import Model
   import Interface

diff --git a/src/Distributions/UniformPowerOfTwo/Interface.dfy b/src/Distributions/UniformPowerOfTwo/Interface.dfy
@@ -3,9 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-include "../Coin/Coin.dfy"
-include "Model.dfy"
-
 module UniformPowerOfTwo.Interface {
   import Coin
   import Model
-Original file line number
+Diff line change
@@ Expand Up / @@ -14,4 +14,4 @@ then @@
       exit 1
     fi
-    $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG src/Dafny-VMC.dfy -o build/$TARGET_LANG/Dafny-VMC
+    $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG src/Dafny-VMC.dfy -o build/$TARGET_LANG/Dafny-VMC dfyconfig.toml --no-verify