Add support for Python (#150)

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).

.github/workflows/build_py.yml

@@ -0,0 +1,15 @@
+name: 'Build Python'
+on:
+  workflow_dispatch:
+  pull_request:
+  push:
+    branches:
+      - 'main'
+jobs:
+  build-python:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - run: bash scripts/prep.sh
+      - run: DAFNY=dafny/dafny TARGET_LANG=py bash scripts/build.sh
+      - run: build/py/run.sh

.github/workflows/test_py.yml

@@ -0,0 +1,14 @@
+name: 'Run Python tests'
+on:
+  workflow_dispatch:
+  pull_request:
+  push:
+    branches:
+      - 'main'
+jobs:
+  test-python:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - run: bash scripts/prep.sh
+      - run: DAFNY=dafny/dafny TARGET_LANG=py bash scripts/test.sh

audit.log

@@ -1,4 +1,4 @@
-src/DafnyVMC.dfy(23,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
+src/DafnyVMC.dfy(28,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
 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/Measures.dfy(125,17): ProbabilityLe1: Declaration has explicit `{:axiom}` attribute. 

build/py/run.sh

@@ -0,0 +1,3 @@
+#1/bin/bash
+
+PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/BuildTest.py

docs/py/BuildTest.py

@@ -0,0 +1,53 @@
+import DafnyVMC
+
+def main():
+    arr1 = [0, 1, 2]
+    arr2 = [float(0), float(1), float(2)]
+    arr3 = ["aa", "bb", "cc"]
+    arr4 = ['a', 'b', 'c']
+    arr5 = [True, False, False, True]
+    num = 3
+    den = 5
+
+    # STANDARD RNG
+    print("\nSTANDARD RNG TESTS\n")
+
+    r = DafnyVMC.Random()
+
+    print("Example of Uniform sampling")
+    print(r.UniformSample(4))
+
+    print("Example of Bernoulli sampling")
+    print(r.BernoulliSample(num,den))
+
+    print("Example of BernoulliExpNeg sampling")
+    print(r.BernoulliExpNegSample(num,den))
+
+    print("Example of DiscreteGaussian sampling")
+    print(r.DiscreteGaussianSample(num,den))
+
+    print("Example of DiscreteLaplace sampling")
+    print(r.DiscreteLaplaceSample(num,den))
+
+    print("Example of Fisher-Yates: int")
+    arr1 = r.Shuffle(arr1)
+    print(arr1)
+
+    print("Example of Fisher-Yates: float")
+    arr2 = r.Shuffle(arr2)
+    print(arr2)
+
+    print("Example of Fisher-Yates: str")
+    arr3 = r.Shuffle(arr3)
+    print(arr3)
+
+    print("Example of Fisher-Yates: char/str")
+    arr4 = r.Shuffle(arr4)
+    print(arr4)
+
+    print("Example of Fisher-Yates: boolean")
+    arr5 = r.Shuffle(arr5)
+    print(arr5)
+
+if __name__ == "__main__":
+    main()

scripts/test.sh

@@ -15,15 +15,19 @@ then
 fi
 
 echo Running $TARGET_LANG tests...
+
 echo "Running tests/TestsRandom.dfy:"
 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
 
 echo Running $TARGET_LANG documentation...
 
 echo "Building docs/dafny/ExamplesRandom.dfy..." 
-$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
+time $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
+
 echo "Executing compiled docs/dafny/ExamplesRandom.dfy:" 
 if [ "$TARGET_LANG" = "java" ]
 then
   java -jar docs/dafny/ExamplesRandom.jar
-fi
+else
+  python3 docs/dafny/ExamplesRandom-py/__main__.py
+fi

src/DafnyVMC.dfy

@@ -3,14 +3,19 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
+module {:extern} DafnyVMCPartMaterial {
+  class {:extern} Random {
+    // For running Dafny native testing with standard SecureRandom rng
+    static method {:extern "UniformPowerOfTwoSample"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat)
+  }
+}
+
 module {:extern "DafnyVMCPart"} DafnyVMC {
   import DafnyVMCTrait
+  import DafnyVMCPartMaterial
   import Monad
   import UniformPowerOfTwo
 
-  // For running Dafny native testing with standard SecureRandom rng
-  method {:extern "DafnyVMCPartMaterial.Random", "UniformPowerOfTwoSample"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat)
-
   class Random extends DafnyVMCTrait.RandomTrait {
     constructor {:extern} ()
 
@@ -19,7 +24,7 @@ module {:extern "DafnyVMCPart"} DafnyVMC {
       modifies this
       ensures UniformPowerOfTwo.Model.Sample(n)(old(s)) == Monad.Result(u, s)
     {
-      u := ExternUniformPowerOfTwoSample(n);
+      u := DafnyVMCPartMaterial.Random.ExternUniformPowerOfTwoSample(n);
       assume {:axiom} false; // assume correctness of extern implementation
     }
   }

src/interop/py/Full/Random.py

@@ -0,0 +1,17 @@
+# Module: DafnyVMC
+
+import secrets
+import _dafny
+import DafnyVMCPart
+
+def ArrayFromList(l):
+  arr = _dafny.Array(None, len(l))
+  for i, e in enumerate(l):
+      arr[i] = e
+  return arr
+
+class Random(DafnyVMCPart.Random):
+  def Shuffle(self, xs):
+    a = ArrayFromList(xs)
+    DafnyVMCPart.Random.Shuffle(self, a)
+    return list(a)

src/interop/py/Part/Random.py

@@ -0,0 +1,7 @@
+# Module: DafnyVMCPartMaterial
+
+import secrets
+
+class Random:
+    def UniformPowerOfTwoSample(n):
+        return secrets.randbits(n.bit_length()-1)