Add a Random module to the dafny library #151

markrtuttle · 2023-11-04T02:06:49Z

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) 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 in the examples directory shows how to use the module. From the examples directory, compile and run the file random.dfy with

# 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

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

robin-aws

Thanks for the contribution! I agree this would be a useful little library for a lot of use cases.

FYI we are in the process of moving lots of this code into the Dafny distribution itself, and Dafny 4.4 will bundle many standard libraries so that all you have to do to depend on them is pass the --standard-libraries flag. See https://github.com/dafny-lang/dafny/tree/master/Source/DafnyStandardLibraries for details.

I'm in the process of adding support for libraries that need target language specific code, so I think it makes sense to move this code over into Dafny itself once that's in.

I did have a quick look and dropped a few quick comments on there. Do also have a look at the Dafny Style Guide (https://github.com/dafny-lang/dafny/blob/master/docs/StyleGuide/Style-Guide.md) - the idiom is usually to PascalCase method names. :)

robin-aws · 2023-11-04T18:29:09Z

src/Random/README.md

+    predicate nextBool()
+
+    // Return an arbitrary integer value in the range [0, bound)
+    function nextInt(bound: int := 0): (value: int)


Why not make bound a required argument? I can see only by looking at the implementation that the implicit default bound is target language dependent, and that doesn't seem terribly useful.

robin-aws · 2023-11-04T18:31:01Z

src/Random/Random.js

+        } catch (e) {
+            throw "nextBool failed";
+        }


Why is this more likely to fail than the others?

robin-aws · 2023-11-04T18:33:03Z

src/Random/Random.java

+public class Random {
+    public static boolean nextBool()
+    {
+        return Math.random() < 0.5;


Why not Math.nextBoolean()?

robin-aws · 2023-11-04T18:35:04Z

src/Random/README.md

+        ensures bound > 0 ==> value < bound
+
+    // Return an arbitrary real value in the range [0,1)
+     function nextReal(): (value: real)


This does seem useful, but I'd call it something more specific, since the implicit bounds will be less obvious on the caller side.

robin-aws · 2023-11-04T21:56:08Z

src/Random/Random.dfy

+module {:options "-functionSyntax:4"} Dafny.Random {
+
+    // Return an arbitrary boolean value.
+    predicate {:extern "DafnyLibraries.Random", "nextBool"} nextBool()


Soundness issue: none of these can be predicates/functions since they are nondeterminisitic. Otherwise Dafny can prove false:

if nextReal() != nextReal() { print 1/0; // Verifies but crashes at runtime almost 100% of the time }

Credit to @seebees for spotting this while I was distracted by other things. :P

Team effort, came in this AM to make sure this was on the PR, thanks!

One can make them functions as long as they take a seed input (ideally an opaque type that can only be created with a method), which is how all of this is handled in e.g. Haskell.

fzaiser · 2023-11-06T15:53:04Z

src/Random/Random.dfy

+
+    // Return an arbitrary real value in the range [0,1).
+     function {:extern "DafnyLibraries.Random", "nextReal"} nextReal(): (value: real)
+        ensures 0.0 <= value < 1.0


I don't think such a function makes sense because a random real number is irrational with probability 1, but real numbers in Dafny are translated to rational numbers in the target language. It is not even clear what a "uniform distribution" on the rational numbers would be.

So my suggestion: What we could have instead is a uniform distribution on {0, 1/(2^k), 2/(2^k), ..., 2^k/(2^k)} for a given k as an argument. This is probably reasonably close to what other languages do when they give a you a uniform floating-point value between 0 and 1.

I think it's fine to have such a method, if a distribution is not specified. The spec is correct.

You're right in that it satisfies the post-condition. But I would argue that the name Random.nextReal creates an expectation that is not captured by the post-condition. Returning 0.5 deterministically would also satisfy the post-condition, but would probably be unexpected for users.

fzaiser · 2023-11-06T18:37:40Z

General comment on using floating point random numbers: One has to be very careful if using random floating point numbers because FP numbers have a higher resolution closer to zero, which could potentially skew the distribution. Ideally one would use library functions that directly return a random integer without going through floating point. There's a lot of subtleties that are easy to get wrong here, see the last paragraph of https://en.wikipedia.org/wiki/Fisher%E2%80%93Yates_shuffle#Modulo_bias as an example. The whole article contains a nice list of things that can go wrong if one is not very careful around randomness.

codyroux · 2023-11-13T22:21:56Z

I'd feel remiss not to add: https://xkcd.com/221/

Add a Random module to the dafny library.

15a048a

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

markrtuttle force-pushed the random branch from 146749c to 15a048a Compare November 4, 2023 02:12

markrtuttle marked this pull request as ready for review November 4, 2023 02:35

robin-aws requested changes Nov 4, 2023

View reviewed changes

robin-aws reviewed Nov 4, 2023

View reviewed changes

fzaiser reviewed Nov 6, 2023

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add a Random module to the dafny library #151

Add a Random module to the dafny library #151

markrtuttle commented Nov 4, 2023

robin-aws left a comment

robin-aws Nov 4, 2023

robin-aws Nov 4, 2023

robin-aws Nov 4, 2023

robin-aws Nov 4, 2023

robin-aws Nov 4, 2023

robin-aws Nov 4, 2023

seebees Nov 6, 2023

codyroux Nov 6, 2023

fzaiser Nov 6, 2023

codyroux Nov 6, 2023

fzaiser Nov 6, 2023

fzaiser commented Nov 6, 2023

codyroux commented Nov 13, 2023

Add a Random module to the dafny library #151

Are you sure you want to change the base?

Add a Random module to the dafny library #151

Conversation

markrtuttle commented Nov 4, 2023

Overview

Usage

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fzaiser commented Nov 6, 2023

codyroux commented Nov 13, 2023