Add a Random module to the dafny library.

The Dafny.Random module supports nextBool, nextInt, and nextReal
returning arbitrary boolean, integer, and real values using the
underlying random number generator of the target language (currently
C#, Java, and JavaScript).

Author: Mark R. Tuttle

examples/Random/.gitignore

@@ -0,0 +1,8 @@
+random.cs
+random.dll
+random.jar
+random.js
+random.runtimeconfig.json
+node_modules
+package-lock.json
+package.json

examples/Random/random.dfy

@@ -0,0 +1,37 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+// RUN: %verify "%s"
+
+// #RUN: %run --no-verify --target:cs "%s" --input "%S/../../src/Random/Random.cs"
+// #RUN: %run --no-verify --target:java "%s" --input "%S/../../src/Random/Random.java"
+// #RUN: %run --no-verify --target:js "%s" --input "%S/../../src/Random/Random.js"
+
+include "../../src/Random/Random.dfy"
+
+module RandomExample {
+  import Dafny.Random
+
+  method Main(args: seq<string>) {
+    var verbose := false;
+    if |args| > 1 { verbose := args[1] == "--verbose"; }
+
+    var bvalue := Random.nextBool();
+    if verbose { print "Random boolean: ", bvalue, "\n"; }
+
+    var bound := 10;
+    var ivalue := Random.nextInt(bound);
+    if verbose { print "Random integer from [0,", bound, "): ", ivalue, "\n"; }
+    expect 0 <= ivalue < bound, "Random integer not within bounds [0,bound)";
+
+    var lvalue := Random.nextInt();
+    if verbose { print "Random integer from [0,MAXINT): ", lvalue, "\n"; }
+    expect 0 <= ivalue, "Random unbounded integer not within bounds [0,MAXINT)";
+
+    var rvalue: real := Random.nextReal();
+    if verbose { print "Random real from [0,1): ", rvalue, "\n"; }
+    expect 0.0 <= rvalue < 1.0, "Random real not within [0,1)";
+  }
+}

src/Random/README.md

@@ -0,0 +1,62 @@
+# Dafny.Random
+
+## Overview
+
+The `Dafny.Random` module provides a uniform interface to random values across target languages.
+
+```
+    // Return an arbitrary boolean value
+    predicate nextBool()
+
+    // Return an arbitrary integer value in the range [0, bound)
+    function nextInt(bound: int := 0): (value: int)
+        ensures 0 <= value
+        ensures bound > 0 ==> value < bound
+
+    // Return an arbitrary real value in the range [0,1)
+     function nextReal(): (value: real)
+        ensures 0.0 <= value < 1.0
+```
+To see the need for a uniform interface to probability,
+C# provides random integer values and Java and JavaScript provide random real values,
+and Dafny actually models real numbers as rationals with integral numerators and denominators
+of arbitrary size.
+This module gives one interface to these various sources of randomness.
+This is a simple interface to probability.
+For a more sophisticated treatment of probability, see
+the [Verified Monte Carlo (VMC)](https://github.com/dafny-lang/Dafny-VMC) library.
+
+The `Dafny.Random` module also provides a uniform interface to nondeterminism and probability.
+For example, `nextInt(10)` returns an arbitrary integer from [0,10), but
+
+* in a proof context, the integer is chosen nondeterministcally, and
+* in a compiled code context, the integer is chose probabilistically according to the uniform probability distribution.
+
+Compare this with the Dafny construct `var value: int := *;` where value is arbitrary in a proof context and
+constant (typically 0) in compiled code.
+
+## Usage
+
+The `Random` module, like `FileIO` will not compile or run correctly without a language-specific
+implementation file.  Implementations are currently provided for C#, Java, and JavaScript.
+To use `Random` in your code, you must:
+* `include` and `import` the `Random` module as you would any other library module
+* incorporate the corresponding language-specific implementation file (e.g. `Random.cs`) when building or running your program
+
+The example [random.dfy](../../examples/Random/random.dfy) in the `examples` directory
+shows how to use the module.
+From the [examples](../../examples/Random) directory, compile and run the file `random.dfy` with
+
+```bash
+# C#
+$ dafny run random.dfy --target cs --input ../../src/Random/Random.cs -- --verbose
+
+# Java
+$ dafny run random.dfy --target java --input ../../src/Random/Random.java -- --verbose
+
+# JavaScript
+$ dafny run random.dfy --target js --input ../../src/Random/Random.js -- --verbose
+```
+
+If you aren't using `dafny run` to run your program, you will have to integrate the
+appropriate language-specific implementation file into your build system.

src/Random/Random.cs

@@ -0,0 +1,31 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+namespace DafnyLibraries
+{
+    using Dafny;
+    using System;
+    using System.Numerics;
+    public class Random
+    {
+        private static System.Random rnd = new System.Random();
+        public static bool nextBool()
+        {
+            return rnd.Next(2) == 0;
+        }
+        public static BigInteger nextInt(BigInteger Bound)
+        {
+            Int64 bound = (Int64) Bound;
+            Int64 bnd = bound > 0 ? bound : Int64.MaxValue;
+            return new BigInteger(rnd.NextInt64(bound));
+        }
+        public static BigRational nextReal()
+        {
+            Int64 num = rnd.NextInt64();
+            Int64 den = Int64.MaxValue;
+            return new BigRational(new BigInteger(num), new BigInteger(den));
+        }
+    }
+}

src/Random/Random.dfy

@@ -0,0 +1,22 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+module Dafny.Random {
+
+    // Return an arbitrary boolean value.
+    predicate {:extern "DafnyLibraries.Random", "nextBool"} nextBool()
+
+    // Return an arbitrary integer value in the range [0, bound).  If the optional
+    // bound is omitted, return an arbitrary nonnegative integer (generally limited
+    // to a 64-bit integer value when compiled).
+    function {:extern "DafnyLibraries.Random", "nextInt"} nextInt(bound: int := 0): (value: int)
+        ensures 0 <= value
+        ensures bound > 0 ==> value < bound
+
+    // Return an arbitrary real value in the range [0,1).
+     function {:extern "DafnyLibraries.Random", "nextReal"} nextReal(): (value: real)
+        ensures 0.0 <= value < 1.0
+
+}

src/Random/Random.java

@@ -0,0 +1,28 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+package DafnyLibraries;
+
+import dafny.*;
+import java.math.*;
+
+public class Random {
+    public static boolean nextBool()
+    {
+        return Math.random() < 0.5;
+    }
+    public static BigInteger nextInt(BigInteger Bound)
+    {
+        long bound = Bound.longValue();
+        long bnd = bound > 0 ? bound : Long.MAX_VALUE;
+        return BigInteger.valueOf((long) Math.floor(Math.random() * bnd));
+    }
+    public static BigRational nextReal()
+    {
+        long num = (long) Math.floor(Math.random() * Long.MAX_VALUE);
+        long den = Long.MAX_VALUE;
+        return new BigRational(BigInteger.valueOf(num), BigInteger.valueOf(den));
+    }
+}

src/Random/Random.js

@@ -0,0 +1,30 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+var DafnyLibraries = DafnyLibraries || {};
+DafnyLibraries.Random = (function () {
+    let $module = {};
+
+    $module.nextBool = function () {
+        try {
+        return Math.random() < 0.5;
+        } catch (e) {
+            throw "nextBool failed";
+        }
+    }
+
+    $module.nextInt = function (bound) {
+        bound = bound > 0 ? bound : Number.MAX_SAFE_INTEGER;
+        return new BigNumber(Math.floor(Math.random() * bound));
+    }
+
+    $module.nextReal = function () {
+        num = Math.floor(Math.random() * Number.MAX_SAFE_INTEGER);
+        den = Number.MAX_SAFE_INTEGER;
+        return new _dafny.BigRational(new BigNumber(num), new BigNumber(den));
+    }
+
+    return $module;
+})();