Skip to content

Commit

Permalink
Merge branch 'main' into limit
Browse files Browse the repository at this point in the history
  • Loading branch information
@fzaiser
fzaiser committed Oct 10, 2023
2 parents 0ee82db + 411cb87 commit 6c0e539
Show file tree
Hide file tree
Showing 54 changed files with 1,220 additions and 1,562 deletions.
47 changes: 25 additions & 22 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,35 +2,38 @@

The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to C# and Java. For the future, we plan to extend both the functionality and the range of supported languages.

To use `DafnyVMC` in your code, you must:
There are two ways to use the library:
- The trait `DRandomFoundational` only needs fair coin flips as a primitive.
- The trait `DRandomExternUniform` also uses an external implementation of uniformly random numbers.

1. `include` and `import` the `DafnyVMC` module as you would any other library module
2. incorporate the corresponding language-specific implementation file when building or running your program

For example, to run the examples in the `docs` directory, run one of the following.
To run the examples in the `docs` directory, use one of the following commands:

```bash
# C#
$ dafny run docs/ExamplesFoundational.dfy --target:cs --input interop/cs/DRandomCoin.cs --input interop/cs/DRandomUniform.cs
$ dafny run docs/ExamplesExternUniform.dfy --target:cs --input interop/cs/DRandomCoin.cs --input interop/cs/DRandomUniform.cs
# Java
$ dafny run docs/ExamplesFoundational.dfy --target:java --input interop/java/DRandomCoin.java --input interop/java/DRandomUniform.java
$ dafny run docs/ExamplesExternUniform.dfy --target:java --input interop/java/DRandomCoin.java --input interop/java/DRandomUniform.java
# C# ExamplesFoundational
$ dafny build docs/dafny/ExamplesFoundational.dfy --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs dfyconfig.toml --no-verify
$ dotnet docs/dafny/ExamplesFoundational.dll
# C# ExamplesExternUniform
$ dafny build docs/dafny/ExamplesExternUniform.dfy --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs dfyconfig.toml --no-verify
$ dotnet docs/dafny/ExamplesExternUniform.dll
# Java ExamplesFoundational
$ dafny build docs/dafny/ExamplesFoundational.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java dfyconfig.toml --no-verify
$ java -jar docs/dafny/ExamplesFoundational.jar
# Java ExamplesExternUniform
$ dafny build docs/dafny/ExamplesExternUniform.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java dfyconfig.toml --no-verify
$ java -jar docs/dafny/ExamplesExternUniform.jar
```

(If you aren't using `dafny run` to run your program,
then you should instead integrate the appropriate language-specific implementation file in your build system.)

# Testing

To run the statistical tests, run one of the following:
To run the statistical tests in the `tests` diretory, use one of the following commands:

```bash
# C#
$ dafny test --target:cs interop/cs/DRandomCoin.cs interop/cs/DRandomUniform.cs tests/TestsFoundational.dfy
$ dafny test --target:cs interop/cs/DRandomCoin.cs interop/cs/DRandomUniform.cs tests/TestsExternUniform.dfy
# Java#
$ dafny test --target:java interop/cs/DRandomCoin.java interop/cs/DRandomUniform.java tests/TestsFoundational.dfy
$ dafny test --target:java interop/cs/DRandomCoin.java interop/cs/DRandomUniform.java tests/TestsExternUniform.dfy

# C# TestsFoundational
$ dafny test --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
# C# TestsExternUniform
$ dafny test --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml --no-verify
# Java TestsFoundational
$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
# Java TestsExternUniform
$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml --no-verify
```
122 changes: 34 additions & 88 deletions audit.log
View file
Original file line number Diff line number Diff line change
@@ -1,88 +1,34 @@

Auditing ./src/Dafny-VMC.dfy

Auditing ./src/Distributions/Base/Interface.dfy
Coin: Definition has `assume {:axiom}` statement in body.

Auditing ./src/Distributions/Base/Model.dfy

Auditing ./src/Distributions/Bernoulli/Correctness.dfy

Auditing ./src/Distributions/Bernoulli/Implementation.dfy

Auditing ./src/Distributions/Bernoulli/Interface.dfy

Auditing ./src/Distributions/Bernoulli/Model.dfy

Auditing ./src/Distributions/BernoulliExpNeg/Implementation.dfy

Auditing ./src/Distributions/BernoulliExpNeg/Interface.dfy

Auditing ./src/Distributions/DiscreteGaussian/Implementation.dfy

Auditing ./src/Distributions/DiscreteGaussian/Interface.dfy

Auditing ./src/Distributions/DiscreteLaplace/Implementation.dfy

Auditing ./src/Distributions/DiscreteLaplace/Interface.dfy

Auditing ./src/Distributions/Uniform/Correctness.dfy
ProbUniformIsIndepFn: Declaration has explicit `{:axiom}` attribute.

Auditing ./src/Distributions/Uniform/Implementation.dfy
Uniform: Definition has `assume {:axiom}` statement in body.
Uniform: Definition has `assume {:axiom}` statement in body.

Auditing ./src/Distributions/Uniform/Interface.dfy

Auditing ./src/Distributions/Uniform/Model.dfy

Auditing ./src/Distributions/UniformPowerOfTwo/Correctness.dfy
ProbUniformAlternative: Definition has `assume {:axiom}` statement in body.
UnifCorrectness2: Definition has `assume {:axiom}` statement in body.
UnifCorrectness2: Definition has `assume {:axiom}` statement in body.
ProbUnifIsIndepFn: Declaration has explicit `{:axiom}` attribute.

Auditing ./src/Distributions/UniformPowerOfTwo/Implementation.dfy

Auditing ./src/Distributions/UniformPowerOfTwo/Interface.dfy

Auditing ./src/Distributions/UniformPowerOfTwo/Model.dfy
ProbUnifTerminates: Declaration has explicit `{:axiom}` attribute.
ProbUnifCorrespondence: Definition has `assume {:axiom}` statement in body.

Auditing ./src/Math/Helper.dfy

Auditing ./src/Math/Limits.dfy

Auditing ./src/Math/MeasureTheory.dfy
CountableSum: Definition has `assume {:axiom}` statement in body.
CountableSumOfZeroesIsZero: Declaration has explicit `{:axiom}` attribute.

Auditing ./src/Math/Rationals.dfy

Auditing ./src/ProbabilisticProgramming/Independence.dfy
IsIndepFn: Declaration has explicit `{:axiom}` attribute.
DeconstructIsIndepFn: Declaration has explicit `{:axiom}` attribute.
ReturnIsIndepFn: Declaration has explicit `{:axiom}` attribute.
IndepFnIsCompositional: Declaration has explicit `{:axiom}` attribute.

Auditing ./src/ProbabilisticProgramming/Monad.dfy
TailIsRNG: Declaration has explicit `{:axiom}` attribute.
HeadIsMeasurable: Declaration has explicit `{:axiom}` attribute.
MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute.
TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute.

Auditing ./src/ProbabilisticProgramming/Quantifier.dfy

Auditing ./src/ProbabilisticProgramming/RandomNumberGenerator.dfy
IsRNG: Declaration has explicit `{:axiom}` attribute.
RNGHasMeasure: Declaration has explicit `{:axiom}` attribute.

Auditing ./src/ProbabilisticProgramming/WhileAndUntil.dfy
ProbWhile: Definition has `assume {:axiom}` statement in body.
EnsureProbWhileTerminates: Declaration has explicit `{:axiom}` attribute.
ProbUntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute.
ProbUntilAsBind: Declaration has explicit `{:axiom}` attribute.
EnsureProbUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body.

src/Distributions/BernoulliExpNeg/Correctness.dfy(13,17): Correctness: Declaration has explicit `{:axiom}` attribute.
src/Distributions/BernoulliExpNeg/Correctness.dfy(17,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute.
src/Distributions/BernoulliExpNeg/Implementation.dfy(34,6): BernoulliExpNegSample: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Implementation.dfy(52,6): BernoulliExpNegSampleCaseLe1: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(30,4): GammaReductionLoop: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(60,4): GammaLe1Loop: Definition has `assume {:axiom}` statement in body.
src/Distributions/Coin/Interface.dfy(20,6): CoinSample: Definition has `assume {:axiom}` statement in body.
src/Distributions/Uniform/Implementation.dfy(43,6): UniformSample: Definition has `assume {:axiom}` statement in body.
src/Math/Exponential.dfy(11,17): EvalOne: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(2,26): Exp: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(4,17): FunctionalEquation: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(7,17): Increasing: 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(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(207,8): ProbWhileIsIndepFn: Definition has `assume {:axiom}` statement in body.
src/ProbabilisticProgramming/WhileAndUntil.dfy(39,4): ProbWhile: Definition has `assume {:axiom}` statement in body.
5 changes: 5 additions & 0 deletions dfyconfig.toml
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
includes = ["src/**/*.dfy"]
excludes = []

[options]
enforce-determinism = true
42 changes: 19 additions & 23 deletions docs/dafny/ExamplesExternUniform.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -19,18 +15,18 @@ module RandomExamples {

var t := 0;
for i := 0 to n {
var b := r.Coin();
var b := r.CoinSample();
if b {
t := t + 1;
}
}
print "Estimated parameter for Coin(): ", (t as real) / (n as real), " (should be around 0.5)\n";
print "Estimated parameter for CoinSample(): ", (t as real) / (n as real), " (should be around 0.5)\n";

var a := 0;
var b := 0;
var c := 0;
for i := 0 to n {
var k := r.Uniform(10);
var k := r.UniformSample(10);
if k == 0 {
a := a + 1;
} else if k == 5 {
Expand All @@ -39,13 +35,13 @@ module RandomExamples {
c := c + 1;
}
}
print "Estimated probabilities for Uniform(10): ", (a as real) / (n as real), "; " , (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.1)\n";
print "Estimated probabilities for UniformSample(10): ", (a as real) / (n as real), "; " , (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.1)\n";

a := 0;
b := 0;
c := 0;
for i := 0 to n {
var k := r.UniformInterval(7,10);
var k := r.UniformIntervalSample(7,10);
if k == 7 {
a := a + 1;
} else if k == 8 {
Expand All @@ -54,52 +50,52 @@ module RandomExamples {
c := c + 1;
}
}
print "Estimated probabilities for UniformInterval(7,10): ", (a as real) / (n as real), "; ", (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.33)\n";
print "Estimated probabilities for UniformIntervalSample(7,10): ", (a as real) / (n as real), "; ", (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.33)\n";

t := 0;
for i := 0 to n {
var b := r.Bernoulli(Rationals.Rational(1, 5));
var b := r.BernoulliSample(Rationals.Rational(1, 5));
if b {
t := t + 1;
}
}

print "Estimated parameter for Bernoulli(1, 5): ", (t as real) / (n as real), " (should be around 0.2)\n";
print "Estimated parameter for BernoulliSample(1, 5): ", (t as real) / (n as real), " (should be around 0.2)\n";

t := 0;
for i := 0 to n {
var b := r.Bernoulli(Rationals.Rational(0, 5));
var b := r.BernoulliSample(Rationals.Rational(0, 5));
if b {
t := t + 1;
}
}

print "Estimated parameter for Bernoulli(0, 5): ", (t as real) / (n as real), " (should be around 0.0)\n";
print "Estimated parameter for BernoulliSample(0, 5): ", (t as real) / (n as real), " (should be around 0.0)\n";

t := 0;
for i := 0 to n {
var b := r.Bernoulli(Rationals.Rational(5, 5));
var b := r.BernoulliSample(Rationals.Rational(5, 5));
if b {
t := t + 1;
}
}

print "Estimated parameter for Bernoulli(5, 5): ", (t as real) / (n as real), " (should be around 1.0\n";
print "Estimated parameter for BernoulliSample(5, 5): ", (t as real) / (n as real), " (should be around 1.0\n";

t := 0;
for i := 0 to n {
var u := r.BernoulliExpNeg(Rationals.Rational(12381, 5377)); // about -ln(0.1)
var u := r.BernoulliExpNegSample(Rationals.Rational(12381, 5377)); // about -ln(0.1)
if u {
t := t + 1;
}
}
print "Estimated parameter for BernoulliExpNeg(-ln(0.1)): ", (t as real) / (n as real), " (should be around 0.1)\n";
print "Estimated parameter for BernoulliExpNegSample(-ln(0.1)): ", (t as real) / (n as real), " (should be around 0.1)\n";

var count0 := 0;
var count1 := 0;
var countneg1 := 0;
for i := 0 to n {
var u := r.DiscreteLaplace(Rationals.Rational(7, 5));
var u := r.DiscreteLaplaceSample(Rationals.Rational(7, 5));
match u {
case -1 => countneg1 := countneg1 + 1;
case 0 => count0 := count0 + 1;
Expand All @@ -110,13 +106,13 @@ module RandomExamples {
// Reference values computed with Wolfram Alpha:
// https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+0%7D%5D
// https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+1%7D%5D
print "Estimated probabilities for DiscreteLaplace(7/5): ", count0 as real / n as real, " (should be around 0.3426949) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.1677634)\n";
print "Estimated probabilities for DiscreteLaplaceSample(7/5): ", count0 as real / n as real, " (should be around 0.3426949) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.1677634)\n";

count0 := 0;
count1 := 0;
countneg1 := 0;
for i := 0 to n {
var u := r.DiscreteGaussian(Rationals.Rational(7, 5));
var u := r.DiscreteGaussianSample(Rationals.Rational(7, 5));
match u {
case -1 => countneg1 := countneg1 + 1;
case 0 => count0 := count0 + 1;
Expand All @@ -127,6 +123,6 @@ module RandomExamples {
// Reference values computed with Wolfram Alpha:
// https://www.wolframalpha.com/input?i=ReplaceAll%5BE%5E%28-x%5E2+%2F+%282+*%CF%83%5E2%29%29+%2F+Sum%5BE%5E%28-y%5E2%2F%282+%CF%83%5E2%29%29%2C+%7By%2C+-Infinity%2C+Infinity%7D%5D%2C+%7Bx+-%3E+0%2C+%CF%83+-%3E+1.4%7D%5D
// https://www.wolframalpha.com/input?i=ReplaceAll%5BE%5E%28-x%5E2+%2F+%282+*%CF%83%5E2%29%29+%2F+Sum%5BE%5E%28-y%5E2%2F%282+%CF%83%5E2%29%29%2C+%7By%2C+-Infinity%2C+Infinity%7D%5D%2C+%7Bx+-%3E+1%2C+%CF%83+-%3E+1.4%7D%5D
print "Estimated probabilities for DiscreteGaussian(1.4): ", count0 as real / n as real, " (should be around 0.284959) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.220797)\n";
print "Estimated probabilities for DiscreteGaussianSample(1.4): ", count0 as real / n as real, " (should be around 0.284959) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.220797)\n";
}
}
Loading

0 comments on commit 6c0e539

Please sign in to comment.