Skip to content

Commit

Permalink
Merge branch 'main' into different-api-example
Browse files Browse the repository at this point in the history
  • Loading branch information
@stefan-aws
stefan-aws authored Feb 14, 2024
2 parents b537d4d + e819db8 commit b7b7449
Show file tree
Hide file tree
Showing 31 changed files with 340 additions and 2,331 deletions.
34 changes: 4 additions & 30 deletions audit.log
View file
Original file line number Diff line number Diff line change
@@ -1,30 +1,6 @@
src/DafnyVMC.dfy(23,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body.
src/Distributions/Bernoulli/Correctness.dfy(59,17): BernoulliCorrectnessCaseFalse: Declaration has explicit `{:axiom}` attribute.
src/Distributions/BernoulliExpNeg/Correctness.dfy(229,6): CorrectnessLe1: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Correctness.dfy(346,17): Le1SeriesConvergesToExpNeg: Declaration has explicit `{:axiom}` attribute.
src/Distributions/BernoulliExpNeg/Correctness.dfy(411,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Correctness.dfy(412,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Correctness.dfy(419,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Correctness.dfy(420,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Correctness.dfy(424,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Correctness.dfy(425,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Correctness.dfy(615,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Correctness.dfy(616,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(112,10): Le1LoopTerminatesAlmostSurely: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(148,4): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(161,8): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(162,8): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(185,10): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(71,17): Le1LoopIterCorrectness: Declaration has explicit `{:axiom}` attribute.
src/Distributions/DiscreteLaplace/Correctness.dfy(37,17): Correctness: Declaration has explicit `{:axiom}` attribute.
src/Distributions/DiscreteLaplace/Model.dfy(89,17): SampleInnerLoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute.
src/Distributions/DiscreteLaplace/Model.dfy(93,17): SampleLoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute.
src/Math/Analysis/Limits.dfy(126,17): Sandwich: Declaration has explicit `{:axiom}` attribute.
src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(55,17): ExpSeriesConverges: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(58,17): FunctionalEquation: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(61,17): Increasing: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(65,17): EvalOne: Declaration has explicit `{:axiom}` attribute.
src/Math/Measures.dfy(125,17): ProbabilityLe1: Declaration has explicit `{:axiom}` attribute.
src/Math/Measures.dfy(130,17): IsMonotonic: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Independence.dfy(105,17): BindIsIndep: Declaration has explicit `{:axiom}` attribute.
Expand All @@ -35,12 +11,10 @@ src/ProbabilisticProgramming/Independence.dfy(77,17): IsIndepImpliesMeasurableNa
src/ProbabilisticProgramming/Independence.dfy(82,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Independence.dfy(87,17): CoinIsIndep: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Independence.dfy(91,17): ReturnIsIndep: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Loops.dfy(362,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Loops.dfy(367,17): EnsureWhileTerminatesAlmostSurelyViaLimit: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Loops.dfy(385,17): WhileProbabilityViaLimit: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Loops.dfy(402,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Loops.dfy(435,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body.
src/ProbabilisticProgramming/Loops.dfy(458,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body.
src/ProbabilisticProgramming/Loops.dfy(361,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Loops.dfy(371,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/Loops.dfy(404,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body.
src/ProbabilisticProgramming/Loops.dfy(427,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body.
src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/RandomSource.dfy(54,17): CoinHasProbOneHalf: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/RandomSource.dfy(61,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute.
Expand Down
20 changes: 6 additions & 14 deletions docs/dafny/ExamplesRandom.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
*******************************************************************************/

module Examples {
import Rationals
import DafnyVMC
import Helper

Expand All @@ -15,13 +14,6 @@ module Examples {
var r: DafnyVMC.Random := new DafnyVMC.Random();

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

var a := 0;
var b := 0;
Expand Down Expand Up @@ -55,7 +47,7 @@ module Examples {

t := 0;
for i := 0 to n {
var b := r.BernoulliSample(Rationals.Rational(1, 5));
var b := r.BernoulliSample(1, 5);
if b {
t := t + 1;
}
Expand All @@ -65,7 +57,7 @@ module Examples {

t := 0;
for i := 0 to n {
var b := r.BernoulliSample(Rationals.Rational(0, 5));
var b := r.BernoulliSample(0, 5);
if b {
t := t + 1;
}
Expand All @@ -75,7 +67,7 @@ module Examples {

t := 0;
for i := 0 to n {
var b := r.BernoulliSample(Rationals.Rational(5, 5));
var b := r.BernoulliSample(5, 5);
if b {
t := t + 1;
}
Expand All @@ -85,7 +77,7 @@ module Examples {

t := 0;
for i := 0 to n {
var u := r.BernoulliExpNegSample(Rationals.Rational(12381, 5377)); // about -ln(0.1)
var u := r.BernoulliExpNegSample(12381, 5377); // about -ln(0.1)
if u {
t := t + 1;
}
Expand All @@ -96,7 +88,7 @@ module Examples {
var count1 := 0;
var countneg1 := 0;
for i := 0 to n {
var u := r.DiscreteLaplaceSample(Rationals.Rational(7, 5));
var u := r.DiscreteLaplaceSample(7, 5);
match u {
case -1 => countneg1 := countneg1 + 1;
case 0 => count0 := count0 + 1;
Expand All @@ -113,7 +105,7 @@ module Examples {
count1 := 0;
countneg1 := 0;
for i := 0 to n {
var u := r.DiscreteGaussianSample(Rationals.Rational(7, 5));
var u := r.DiscreteGaussianSample(7, 5);
match u {
case -1 => countneg1 := countneg1 + 1;
case 0 => count0 := count0 + 1;
Expand Down
27 changes: 11 additions & 16 deletions docs/java/BuildTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,30 +22,28 @@ public static void main(String[] args) {
boolean[] arr5 = {true, false, false, true};
long[] arr6 = {111111L, 333333L, 999999L};
short[] arr7 = {-3, 0, 3};
Rationals.Rational gamma = new Rationals.Rational(BigInteger.valueOf(3), BigInteger.valueOf(5));

BigInteger num = BigInteger.valueOf(3);
BigInteger den = BigInteger.valueOf(5);

/* STANDARD RNG */
System.out.println("\nSTANDARD RNG TESTS\n");

DafnyVMC.Random r = new DafnyVMC.Random();

System.out.println("Example of Coin sampling");
System.out.println(r.CoinSample());

System.out.println("Example of Uniform sampling");
System.out.println(r.UniformSample(BigInteger.valueOf(4)));

System.out.println("Example of Bernoulli sampling");
System.out.println(r.BernoulliSample(gamma));
System.out.println(r.BernoulliSample(num,den));

System.out.println("Example of BernoulliExpNeg sampling");
System.out.println(r.BernoulliExpNegSample(gamma));
System.out.println(r.BernoulliExpNegSample(num,den));

System.out.println("Example of DiscreteGaussian sampling");
System.out.println(r.DiscreteGaussianSample(gamma));
System.out.println(r.DiscreteGaussianSample(num,den));

System.out.println("Example of DiscreteLaplace sampling");
System.out.println(r.DiscreteLaplaceSample(gamma));
System.out.println(r.DiscreteLaplaceSample(num,den));

System.out.println("Example of Fisher-Yates: BigInteger");
r.Shuffle(arr1);
Expand Down Expand Up @@ -82,23 +80,20 @@ public static void main(String[] args) {
ThreadLocal<SecureRandom> rng = ThreadLocal.withInitial(() -> secRand);
DafnyVMC.Random t = new DafnyVMC.Random(n -> UniformPowerOfTwoSample(n, rng));

System.out.println("Example of Coin sampling");
System.out.println(t.CoinSample());

System.out.println("Example of Uniform sampling");
System.out.println(t.UniformSample(BigInteger.valueOf(4)));

System.out.println("Example of Bernoulli sampling");
System.out.println(t.BernoulliSample(gamma));
System.out.println(t.BernoulliSample(num,den));

System.out.println("Example of BernoulliExpNeg sampling");
System.out.println(t.BernoulliExpNegSample(gamma));
System.out.println(r.BernoulliExpNegSample(num,den));

System.out.println("Example of DiscreteGaussian sampling");
System.out.println(t.DiscreteGaussianSample(gamma));
System.out.println(t.DiscreteGaussianSample(num,den));

System.out.println("Example of DiscreteLaplace sampling");
System.out.println(t.DiscreteLaplaceSample(gamma));
System.out.println(t.DiscreteLaplaceSample(num,den));

System.out.println("Example of Fisher-Yates: BigInteger");
t.Shuffle(arr1);
Expand Down
2 changes: 1 addition & 1 deletion scripts/audit.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,4 +8,4 @@ then
exit 1
fi

$DAFNY audit dfyconfig.toml | grep -v '{:termination false}\|{:extern}\|decreases *\|Dafny auditor completed\|Dafny program verifier\|No terms found to trigger on\|Compiled declaration has no body' | sed 's/Warning: //' | sed 's/Possible mitigation: .*//' | sed '/^$/d' | sort > audit.log
$DAFNY audit dfyconfig.toml | grep -v '{:termination false}\|{:extern}\|decreases *\|DafnyVMCTrait\|Dafny auditor completed\|Dafny program verifier\|No terms found to trigger on\|Compiled declaration has no body' | sed 's/Warning: //' | sed 's/Possible mitigation: .*//' | sed '/^$/d' | sort > audit.log
1 change: 1 addition & 0 deletions scripts/checkformat.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,4 +10,5 @@ fi

echo "Checking the formatting of all Dafny files..."
echo "Run \`DAFNY=dafny scripts/format.sh\` to fix any errors."
$DAFNY format src/DafnyVMCTrait.dfy
$DAFNY format --check dfyconfig.toml
Loading

0 comments on commit b7b7449

Please sign in to comment.