Skip to content

Commit 035d48e

Browse files
stefan-awsstefan-aws
committed
skeleton
1 parent f616573 commit 035d48e

File tree

10 files changed

+273
-8
lines changed

10 files changed

+273
-8
lines changed

‎build/cs/cs.csproj

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
<Project Sdk="Microsoft.NET.Sdk">
2+
3+
<PropertyGroup>
4+
<OutputType>Exe</OutputType>
5+
<TargetFramework>net6.0</TargetFramework>
6+
<ImplicitUsings>enable</ImplicitUsings>
7+
<Nullable>enable</Nullable>
8+
</PropertyGroup>
9+
10+
<ItemGroup>
11+
<Reference Include="DafnyVMC.dll" />
12+
</ItemGroup>
13+
14+
</Project>

‎build/cs/run.sh

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
#!/bin/bash
2+
3+
rm -f build/cs/DafnyVMC.cs
4+
cp docs/cs/BuildTest.cs build/cs/
5+
dotnet run --project build/cs/cs.csproj

‎docs/cs/BuildTest.cs

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
using System;
2+
using System.Threading;
3+
using System.Numerics;
4+
using DafnyVMC;
5+
6+
class Check {
7+
public static void Main(string[] args) {
8+
BigInteger[] arr1 = {new BigInteger(0), new BigInteger(1), new BigInteger(2)};
9+
int[] arr2 = {0, 1, 2};
10+
string[] arr3 = {"aa", "bb", "cc"};
11+
char[] arr4 = {'a', 'b', 'c'};
12+
bool[] arr5 = {true, false, false, true};
13+
long[] arr6 = {111111L, 333333L, 999999L};
14+
short[] arr7 = {-3, 0, 3};
15+
//var gamma = new Rationals._IRational(BigInteger(3), BigInteger(5));
16+
17+
/* STANDARD RNG */
18+
Console.WriteLine("\nSTANDARD RNG TESTS\n");
19+
20+
var r = new DafnyVMC.Random();
21+
22+
Console.WriteLine("Example of Coin sampling");
23+
Console.WriteLine(r.CoinSample());
24+
25+
Console.WriteLine("Example of Uniform sampling");
26+
Console.WriteLine(r.UniformSample(new BigInteger(4)));
27+
28+
/* Console.WriteLine("Example of Bernoulli sampling");
29+
Console.WriteLine(r.BernoulliSample(gamma));
30+
31+
Console.WriteLine("Example of BernoulliExpNeg sampling");
32+
Console.WriteLine(r.BernoulliExpNegSample(gamma));
33+
34+
Console.WriteLine("Example of DiscreteGaussian sampling");
35+
Console.WriteLine(r.DiscreteGaussianSample(gamma));
36+
37+
Console.WriteLine("Example of DiscreteLaplace sampling");
38+
Console.WriteLine(r.DiscreteLaplaceSample(gamma)); */
39+
40+
/* Console.WriteLine("Example of Fisher-Yates: BigInteger");
41+
r.Shuffle(arr1);
42+
Console.WriteLine(Arrays.toString(arr1));
43+
44+
Console.WriteLine("Example of Fisher-Yates: int");
45+
r.Shuffle(arr2);
46+
Console.WriteLine(Arrays.toString(arr2));
47+
48+
Console.WriteLine("Example of Fisher-Yates: String");
49+
r.Shuffle(arr3);
50+
Console.WriteLine(Arrays.toString(arr3));
51+
52+
Console.WriteLine("Example of Fisher-Yates: char");
53+
r.Shuffle(arr4);
54+
Console.WriteLine(Arrays.toString(arr4));
55+
56+
Console.WriteLine("Example of Fisher-Yates: boolean");
57+
r.Shuffle(arr5);
58+
Console.WriteLine(Arrays.toString(arr5));
59+
60+
Console.WriteLine("Example of Fisher-Yates: long");
61+
r.Shuffle(arr6);
62+
Console.WriteLine(Arrays.toString(arr6));
63+
64+
Console.WriteLine("Example of Fisher-Yates: short");
65+
r.Shuffle(arr7);
66+
Console.WriteLine(Arrays.toString(arr7)); */
67+
68+
/* CUSTOM RNG */
69+
Console.WriteLine("\nCUSTOM RNG TESTS\n");
70+
71+
var rng = new System.Random();
72+
var t = new DafnyVMC.Random(rng);
73+
74+
Console.WriteLine("Example of Coin sampling");
75+
Console.WriteLine(t.CoinSample());
76+
77+
Console.WriteLine("Example of Uniform sampling");
78+
Console.WriteLine(t.UniformSample(new BigInteger(4)));
79+
80+
/* Console.WriteLine("Example of Bernoulli sampling");
81+
Console.WriteLine(t.BernoulliSample(gamma));
82+
83+
Console.WriteLine("Example of BernoulliExpNeg sampling");
84+
Console.WriteLine(t.BernoulliExpNegSample(gamma));
85+
86+
Console.WriteLine("Example of DiscreteGaussian sampling");
87+
Console.WriteLine(t.DiscreteGaussianSample(gamma));
88+
89+
Console.WriteLine("Example of DiscreteLaplace sampling");
90+
Console.WriteLine(t.DiscreteLaplaceSample(gamma)); */
91+
92+
/* Console.WriteLine("Example of Fisher-Yates: BigInteger");
93+
t.Shuffle(arr1);
94+
Console.WriteLine(Arrays.toString(arr1));
95+
96+
Console.WriteLine("Example of Fisher-Yates: int");
97+
t.Shuffle(arr2);
98+
Console.WriteLine(Arrays.toString(arr2));
99+
100+
Console.WriteLine("Example of Fisher-Yates: String");
101+
t.Shuffle(arr3);
102+
Console.WriteLine(Arrays.toString(arr3));
103+
104+
Console.WriteLine("Example of Fisher-Yates: char");
105+
t.Shuffle(arr4);
106+
Console.WriteLine(Arrays.toString(arr4));
107+
108+
Console.WriteLine("Example of Fisher-Yates: boolean");
109+
t.Shuffle(arr5);
110+
Console.WriteLine(Arrays.toString(arr5));
111+
112+
Console.WriteLine("Example of Fisher-Yates: long");
113+
t.Shuffle(arr6);
114+
Console.WriteLine(Arrays.toString(arr6));
115+
116+
Console.WriteLine("Example of Fisher-Yates: short");
117+
t.Shuffle(arr7);
118+
Console.WriteLine(Arrays.toString(arr7)); */
119+
}
120+
}

‎docs/java/BuildTest.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ public static void main(String[] args) {
8282
System.out.println(t.BernoulliSample(gamma));
8383

8484
System.out.println("Example of BernoulliExpNeg sampling");
85-
System.out.println(r.BernoulliExpNegSample(gamma));
85+
System.out.println(t.BernoulliExpNegSample(gamma));
8686

8787
System.out.println("Example of DiscreteGaussian sampling");
8888
System.out.println(t.DiscreteGaussianSample(gamma));

‎scripts/build.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,4 +14,4 @@ then
1414
exit 1
1515
fi
1616

17-
$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify
17+
$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o docs/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify

‎scripts/test.sh

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,14 +16,16 @@ fi
1616

1717
echo Running $TARGET_LANG tests...
1818
echo "Running tests/TestsRandom.dfy:"
19-
time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
19+
time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
2020

2121
echo Running $TARGET_LANG documentation...
2222

2323
echo "Building docs/dafny/ExamplesRandom.dfy..."
24-
$DAFNY build docs/dafny/ExamplesRandom.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG dfyconfig.toml --no-verify
24+
$DAFNY build docs/dafny/ExamplesRandom.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG dfyconfig.toml --no-verify
2525
echo "Executing compiled docs/dafny/ExamplesRandom.dfy:"
2626
if [ "$TARGET_LANG" = "java" ]
2727
then
2828
java -jar docs/dafny/ExamplesRandom.jar
29+
else
30+
dotnet docs/dafny/ExamplesRandom.dll
2931
fi

‎src/interop/cs/Full/Random.cs

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
using System;
2+
using System.Threading;
3+
using System.Numerics;
4+
5+
namespace DafnyVMC {
6+
7+
public class Random: DafnyVMCTrait.RandomTrait {
8+
static ThreadLocal<System.Random> RNG;
9+
10+
public Random() {
11+
RNG = new ThreadLocal<System.Random>(createRandom);
12+
}
13+
14+
public Random(System.Random rng) {
15+
RNG = new ThreadLocal<System.Random>(() => rng);
16+
}
17+
18+
private static System.Random createRandom() {
19+
var rng = new System.Random();
20+
// Required for proper initialization
21+
rng.Next(2);
22+
return rng;
23+
}
24+
25+
public BigInteger UniformPowerOfTwoSample(BigInteger n) {
26+
if (n.Sign < 1) {
27+
throw new ArgumentException("n must be positive");
28+
}
29+
30+
// Constructs a uniform random BigInteger in {0, ..., 2^k - 1)}, where k == n.GetBitLength() - 1.
31+
// E.g. for n = 8, we have k=3, since 2^{3} <= n < 2^{3+1}, and k == 3 == 4 - 1 = n.GetBitLength() - 1, as desired.
32+
// Next(m) returns a uniform random value in {0, ..., m - 1}.
33+
var m = (long) Math.Pow(2, n.GetBitLength() - 1); // converting double to long
34+
var o = RNG.Value.NextInt64(m);
35+
return new BigInteger(o);
36+
}
37+
38+
public BigInteger UniformIntervalSample(BigInteger a, BigInteger b) {
39+
return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b);
40+
}
41+
42+
public BigInteger UniformSample(BigInteger n) {
43+
return Uniform.Implementation._Companion_Trait.UniformSample(this, n);
44+
}
45+
46+
public bool CoinSample() {
47+
return Coin.Implementation._Companion_Trait.CoinSample(this);
48+
}
49+
50+
public bool BernoulliSample(Rationals._IRational p) {
51+
return Bernoulli.Implementation._Companion_Trait.BernoulliSample(this, p);
52+
}
53+
54+
public bool BernoulliExpNegSampleCaseLe1(Rationals._IRational gamma) {
55+
return BernoulliExpNeg.Implementation._Companion_Trait.BernoulliExpNegSampleCaseLe1(this, gamma);
56+
}
57+
58+
public bool BernoulliExpNegSample(Rationals._IRational gamma) {
59+
return BernoulliExpNeg.Implementation._Companion_Trait.BernoulliExpNegSample(this, gamma);
60+
}
61+
62+
public BigInteger DiscreteGaussianSample(Rationals._IRational sigma) {
63+
return DiscreteGaussian.Implementation._Companion_Trait.DiscreteGaussianSample(this, sigma);
64+
}
65+
66+
public _System._ITuple2<bool, BigInteger> DiscreteLaplaceSampleLoop(Rationals._IRational scale) {
67+
return DiscreteLaplace.Implementation._Companion_Trait.DiscreteLaplaceSampleLoop(this, scale);
68+
}
69+
70+
public BigInteger DisceteLaplaceSampleInnerLoop() {
71+
return DiscreteLaplace.Implementation._Companion_Trait.DisceteLaplaceSampleInnerLoop(this);
72+
}
73+
74+
public BigInteger DiscreteLaplaceSample(Rationals._IRational scale) {
75+
return DiscreteLaplace.Implementation._Companion_Trait.DiscreteLaplaceSample(this, scale);
76+
}
77+
78+
public void Shuffle<__T>(__T[] a) {
79+
FisherYates.Implementation._Companion_Trait.Shuffle(this, a);
80+
}
81+
}
82+
83+
}

‎src/interop/cs/Part/Random.cs

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
using System;
2+
using System.Threading;
3+
using System.Numerics;
4+
5+
namespace DafnyVMCPartMaterial {
6+
7+
public sealed class Random {
8+
9+
private static readonly ThreadLocal<System.Random> RNG = new ThreadLocal<System.Random>(createRandom);
10+
11+
private Random() {} // Prevent instantiation
12+
13+
private static System.Random createRandom() {
14+
var rng = new System.Random();
15+
// Required for proper initialization
16+
rng.Next(2);
17+
return rng;
18+
}
19+
20+
// Let k be such that 2^k <= n < 2^(k+1). Then the model UniformPowerOfTwo(n) returns a uniform random value in {0, ..., 2^k - 1}.
21+
// E.g. for n = 8, the model returns a uniform random value in {0, ..., 7 = 2^3 - 1}.
22+
public static BigInteger UniformPowerOfTwoSample(BigInteger n) {
23+
if (n.Sign < 1) {
24+
throw new ArgumentException("n must be positive");
25+
}
26+
27+
// Constructs a uniform random BigInteger in {0, ..., 2^k - 1)}, where k == n.GetBitLength() - 1.
28+
// E.g. for n = 8, we have k=3, since 2^{3} <= n < 2^{3+1}, and k == 3 == 4 - 1 = n.GetBitLength() - 1, as desired.
29+
// Next(m) returns a uniform random value in {0, ..., m - 1}.
30+
var m = (long) Math.Pow(2, n.GetBitLength() - 1); // converting double to long
31+
var o = RNG.Value.NextInt64(m);
32+
return new BigInteger(o);
33+
}
34+
}
35+
36+
}

‎src/interop/java/Full/Random.java

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,14 @@
55
import java.security.SecureRandom;
66

77
public class Random implements DafnyVMCTrait.RandomTrait {
8-
static ThreadLocal<SecureRandom> rng;
8+
static ThreadLocal<SecureRandom> RNG;
99

1010
public Random() {
11-
this.rng = ThreadLocal.withInitial(Random::createSecureRandom);
11+
RNG = ThreadLocal.withInitial(Random::createSecureRandom);
1212
}
1313

1414
public Random(SecureRandom rng) {
15-
this.rng = ThreadLocal.withInitial(() -> rng);
15+
RNG = ThreadLocal.withInitial(() -> rng);
1616
}
1717

1818
private static final SecureRandom createSecureRandom() {
@@ -27,7 +27,7 @@ public BigInteger UniformPowerOfTwoSample(BigInteger n) {
2727
throw new IllegalArgumentException("n must be positive");
2828
}
2929

30-
return new BigInteger(n.bitLength()-1, rng.get());
30+
return new BigInteger(n.bitLength()-1, RNG.get());
3131
}
3232

3333
public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) {

‎src/interop/java/Part/Random.java

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,16 @@ private static final SecureRandom createSecureRandom() {
1717
return rng;
1818
}
1919

20+
// Let k be such that 2^k <= n < 2^(k+1). Then the model UniformPowerOfTwo(n) returns a uniform random value in {0, ..., 2^k - 1}.
21+
// E.g. for n = 8, the model returns a uniform random value in {0, ..., 7 = 2^3 - 1}.
2022
public static BigInteger UniformPowerOfTwoSample(BigInteger n) {
2123
if (n.compareTo(BigInteger.ONE) < 0) {
2224
throw new IllegalArgumentException("n must be positive");
2325
}
2426

27+
// BigInteger(int numBits, Random rnd) constructs a randomly generated BigInteger, uniformly distributed over the range 0 to (2^numBits - 1), inclusive.
28+
// For n = 8, we have 2^3 <= 8 < 2^{3+1}, i.e. k == 3 = 4 - 1 == n.bitLength() - 1
29+
// We thus return a uniform random value in {0, ..., 2^{n.bitLength()-1} - 1 == 2^k - 1}, as desired.
2530
return new BigInteger(n.bitLength()-1, RNG.get());
2631
}
2732
}

0 commit comments

Comments
 (0)