Formally verified biased coin and n-sided die
Project description
Zarpy: formally verified biased coin and n-sided die.
See the paper (to appear in PLDI'23) and Github repository.
Why use Zarpy?
Probabilistic choice
A common operation in randomized algorithms is probabilistic choice:
for some p ∈ [0,1]
, execute action a1
with probability p
or a2
with probability 1-p
(i.e., flip a biased coin to determine the path
of execution). A quick-and-dirty method for performing probabilistic
choice is as follows:
if random() < p:
execute a1
else:
execute a2
where p
is a float in the range [0,1]
and random()
produces a
random float in the range [0,1)
. While good enough for many
applications, this approach is not always correct due to float
roundoff error. We can only expect a1
to be executed with
probability p + ϵ
for some small error term ϵ
, technically
invalidating any correctness guarantees of our overall system that
depend on the correctness of its probabilistic choices.
Zarpy provides an alternative that is guaranteed (by formal proof in
Coq) to execute a1
with probability exactly equal to p
(where n
and d
are integers such that p = n/d
):
from zarpy import build_coin, flip
build_coin((n, d)) # Build and cache coin with bias p = n/d
if flip(): # Generate a Boolean value with Pr(True) = p
execute a1
else:
execute a2
Uniform sampling
Another common operation is randomly drawing from a finite collection
of values with equal (uniform) probabilities. An old trick for drawing
an integer uniformly from the range [0, n)
is to generate a random
integer from [0, RAND_MAX]
and take the modulus wrt. n
:
x = rand() % n # Assign x random value from [0,n)
but this method suffers from modulo bias when n
is not a power of 2,
causing some values to occur with higher probability than others (see,
e.g., this
article
for more information on modulo bias). Zarpy provides a uniform sampler
that is guaranteed for any integer 0 < n
to generate samples from
[0,n)
with probability 1/n
of each:
from zarpy import build_die, roll
build_die(n)
x = roll()
Although the python function random.randint
is ostensibly free from
modulo bias, our implementation provides a formal proof of
correctness.
The samplers provided by Zarpy have been implemented and verified in Coq and extracted to OCaml and bundled into Python package via pythonlib. Validity of the correctness proofs is thus dependent on correctness of Coq's extraction mechanism, a small amount of OCaml shim code (viewable here), and the pythonlib library.
Proofs of correctness
The coin and die samplers are implemented as probabilistic programs and compiled to interaction trees by the Zar probabilistic programming system. See the file zarpy.v for their implementations and proofs of correctness.
Correctness is two-fold. For biased coin with bias p
, we prove:
-
coin_itree_correct: the probability of
true
according to the formal probabilistic semantics of the constructed interaction tree is equal top
, and -
coin_samples_equidistributed: when the source of random bits is uniformly distributed, for any sequence of coin flips the proportion of
true
samples converges top
as the number of samples goes to +∞.
The equidistribution result is dependent on uniform distribution of
the Boolean values generated by OCaml's
Random.bool
function. See
the paper for a more detailed
explanation.
Similarly, the theorem die_itree_correct proves semantic correctness of the n-sided die, and die_samples_equidistributed equidistribution of its samples.
Usage
seed()
initializes the PRNG.
Biased coin
build_coin((num, denom))
builds and caches a coin with Pr(True) = num/denom
for nonnegative integer num
and positive integer denom
.
flip()
produces a single Boolean sample by flipping the cached coin.
flip_n(n)
produces n
Boolean samples by flipping the cached coin.
N-sided die
build_die(n)
builds and caches an n-sided die with Pr(m) = 1/n
for
integer m
where 0 <= m < n
.
roll()
produces a single sample by rolling the cached die.
roll_n(n)
produces n
integer samples by rolling the cached die.
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.