Alea: a library for reasoning on randomized algorithms in Coq
Version 8Christine PaulinMohring
with contributions by David Baelde and Pierre Courtieu
PROVAL Team
LRI, UMR 8623 Univ. ParisSud 11, CNRS & INRIA Saclay  ÎledeFranceMay 2013 
1 Introduction
This library forms a basis for reasoning on randomised algorithms in
the proof assistant Coq [5]. The source files are
available from the
(author homepage). They
can be compiled using Coq version V8.3.
The theoretical basis of this work is a joint work with Philippe
Audebaud and is described in [1]. It
is developed in the framework of the SCALP
project (ANR07SESU010) on
Security of Cryptographic ALgorithms with Probabilities.
As proposed by Kozen [2, 3], we interpret
probabilistic programs as measures; the originality of our approach is
to view this interpretation as a monadic transformation on functional
programs. Using this semantics, we derive general rules for
estimating the probability for a randomised algorithm to satisfy a
given property. We apply this approach to the formal proof in Coq
of properties of randomised algorithms. The repository contains
simple examples: a program implementing a Bernoulli distribution using
a coin flip as a primitive, the construction of the binomial
distribution. We prove the probabilistic termination of a linear
random walk. We also prove a general scheme for combining 2
different randomized expressions in order to get a better result. We
also study an example of partial termination. The library ALEA has
been used in larger developments, mainly the
CertiCrypt
environment for formal proofs for computational cryptography based on
a game representation.
With respect to previous versions of this library, we use the
mechanism of type classes introduced by N. Oury and
M. Sozeau [4] in order to represent the order
structure and the cpo structure on a given type. In this version,
P. Courtieu started to design simple automatic tactics for reasoning
on measures, making an essential use of the possibility to rewrite
under abstraction.
Starting from version 7, this library also provides a livrary for positive real numbers represented with both integral part (in nat) and fractional part in [0,1].
Version 8 is compatible with Coq V8.4pl2. Also the development for positive real numbers has been slightly adapted.
2 Contents of the library
The library is composed of the following files :

Misc
 A few preliminary definitions, in
particular primitives for reasoning classically in Coq are defined.
 Cpo
 The definition of structures for ordered
sets and ωcomplete partial orders (a monotonic sequence has
a leastupper bound). We define the type O_{1}→^{m} O_{2} of monotonic
functions and define the fixpointconstruction for monotonic
functionals. Continuity is also defined.
 Utheory
 An axiomatisation of the interval
[0,1]. The type [0,1] is given a cpo structure: we have
the predicates ≤ and ==, a least element 0
and a leastupper bound on all monotonic
sequences of elements of [0,1].
The primitive operations are:
Operation  Meaning  Coq Notation 

bounded addition :  (x,y)↦ min(x+y,1)  x+y 
multiplication :  (x,y)↦ x × y  x*y 
division:  (x,y)↦ min(x / y,1)  x/y 
inverse function:  x ↦ 1−x  [1−]x 
constants:   [1/1+]n 

 Uprop
 Derived operations and properties of
operators on [0,1]. The main defined operations are:
Operation  Meaning  Coq Notation  Alea definition 

bounded subtraction:  (x,y)↦ max(x−y,0)  x−y  [1−]([1−]x + y) 
maximum:  (x,y) ↦ max(x,y)  max x y  (x−y)+y 
minimum:  (x,y) ↦ min(x,y)  min x y  [1−]((y−x)+[1−]y) 
addition dual:  (x,y) ↦ max(x+y−1,0)  x & y  [1−]([1−]x+[1−]y) 
difference:  (x,y) ↦ x−y  diff x y  (x−y) + (y−x) 
mean:   mean x y  [1/2]x+[1/2] y 
multiple:  (n∈ℕ,x) ↦ nx  n */ x  induction on n 
power:  (n∈ℕ,x) ↦ x^{n}  x ^ n  induction on n 
generalized sum:  (f ∈ ℕ → [0,1],n∈ℕ) ↦
Σ_{i=0}^{i=n−1} f(i)  sigma f n  induction on n 

This file defines a tactic Usimpl designed to help simplify expressions using operations on [0,1].
 Monads
 Definition of the basic monad for
randomized constructions,
the type α is mapped to the type (α →
[0,1])→^{m} [0,1] of measure functions.
We define the unit and star constructions and prove that
they satisfy the basic monadic properties.
A measure will be a function of type (α →
[0,1])→^{m} [0,1] which enjoys extra properties such as
stability with respect to basic operations, continuity.
We prove that functions produced by unit and star
satisfy these extra properties under apropriate assumptions.
 Probas
 Definition of a dependent type for
distributions on a type α. A distribution on a type α
is a record containing a function µ of type (α →
[0,1])→^{m} [0,1] and proofs that this function enjoys the stability
properties of measures. These properties are :
µ(f_{1}+f_{2})  = µ(f_{1}) + µ(f_{2}) when f_{1} ≤ 1 − f_{2} 
µ(k × f)  = k × µ (f) 
µ(1− f)  ≤ 1 − µ(f) 
µ(lub_{n} (f n))  ≤ lub_{n} (µ(f n)) when f is
a monotonic sequence of functions 

We define the interpretation of specific random primitives : the
distribution corresponding to a coin flip and the distribution
corresponding to the random function
which applied to n gives a number between 0 and n with
probability 1/n+1.  SProbas
 a relaxed notion of distributions called subdistributions suitable to model programs using both nondeterministic and random choice.
A subdistribution is not additive but instead satisfies the following weaker properties:
µ(f_{1}) + µ(f_{2})  ≤ µ(f_{1}+f_{2}) when f_{1} ≤ 1 − f_{2} 
µ(f) & µ (g)  ≤ µ (f & g) 
µ(f+c)  ≤ µ(f) + c 

 Prog
 Definition of randomized programs
constructions. We define the probabilistic choice and
conditional constructions and a fixpoint operator
obtained by iterating a monotonic functional.
We introduce an axiomatic semantics for these randomized
programs :
let e be a randomized expression of type τ, p be an element
of [0,1] and q be a function of type τ → [0,1], we define
p ≤ [e](q) to be the property : the measure of q by the
distribution associated to the expression e is not less than p.
In the case q is the characteristic function of a predicate Q,
p ≤ [e](q) can be interpreted as “the probability for the result of
the evaluation of e to satisfy Q is not less than p”.
In the particular case where q is the constant function equal to
1, the relation p ≤ [e](q) can be interpreted as “the probability for the
evaluation of e to terminate is not less than p”.
We derive inference rules for this relation.
 Cover
 A definition of what it means for a
function f to be the characteristic function of a predicate
P. Defines also characteristic functions for decidable
predicates. This file contains a proof of the principle :
1 ≤ [a](I_{P}) ∀ x, (P x) ⇒
k ≤ [b](f) 

k ≤ [let x=a in b](f) 

This file uses the library Sets.v which defines sets as predicates
and finite sets with an inductive definition.  BinCoeff
 Definition of binomial coefficients.
 Bernoulli
 Construction of a bernoulli
distribution from the flip distribution.
We consider the program
let rec bernoulli p = if flip () then
if x < 1/2 then false else bernoulli (2 p1)
else if x < 1/2 then bernoulli (2 p) else true
We prove that the probability of bernouilli(p) to answer
true is exactly p. We use this distribution in order to
simulate a binomial distribution such that Pr((binomial p n)=k) =
C_{k}^{n} p^{k}(1−p)^{n−k}.
 IsDiscrete

Proof that a distribution on a discrete domain is discrete.
This result is adapted from the Certicrypt development.
 DistrTactic
 This file introduces a tactic
rsimplmu which attempts to simplify expressions involving randomized programs.
3 Examples

IterFlip

A proof of probabilistic termination for a random walk.
We consider the program
let rec iter x = if flip() then iter (x+1) else x
We prove that the probability that this program terminates is 1.
 Choice
 A proof of composition of two runs of a probabilistic
program, when a choice can improve the quality of the result.
Given two randomized expressions p_{1} and p_{2} of type τ and a
function Q to be estimated,
we consider a choice function such that the value of Q for
choice(x,y) is not less than Q(x)+Q(y).
We prove that if p_{i} evaluates Q not less than k_{i} and
terminates with probability 1 then the
expression choice(p_{1},p_{2}) evaluates Q not less than
k_{1}(1−k_{2})+k_{2} (which is greater than both k_{1} and k_{2} when
k_{1} and k_{2} are not equal to 0).
 RandomList
 Construction of a distribution to pick uniformely an element in a list.
 ProbTuring

A simple formalisation of probabilistic Turing machines in ALEA.
 Ycart
 Evaluation of probability of termination for a
program adapted from an example
due to B. Ycart, parameterized by a function K of type
nat→ nat and a natural number N.
let rec ycart n = if random N < K n then n else ycart (n+1)
Probability of termination of (ycart n) is shown to be equal to
∏_{k=n}^{∞} (1−F k), with F n=K n/(1+N).
 AbstractWalk
 proof of termination
of a special walk where with a bounded positive probability we strictly decrease the size of the object in the call (otherwise we call the procedure on the same object).
4 Modeling positive real numbers
This experimental library represents positive real numbers with an integral part and a fractional part in [0,1]. It requires an extra axiom for decidability
of testing x≤ y in [0,1].

Markov
 A general library to implement a minimimalization algorithm for a decidable predicat P on natural numbers, assuming a proof of ∃ n, P n.
 Rplus
 An experimental representation
of positive real numbers with integral and fractional part. The real (n,1) is equal to (n+1,0). The four arithmetic operations are implemented and their main properties proved. The exponential (with respect to a natural number) is defined as well as bounded sum.
A tactic Rpsimpl is defined to perform basic simplifications on expressions.
 RpRing
 Implementation of tactics Ring and Field on the set Rplus.
References

[1]

Philippe Audebaud and Christine PaulinMohring.
Proofs of randomized algorithms in Coq.
Science of Computer Programming, 74(8):568–589, 2009.
A preliminary version appeared in the proc. of MPC 06.
 [2]

Dexter Kozen.
Semantics of probabilistic programs.
J. of Computer and System Science, 1981.
 [3]

Dexter Kozen.
A probabilistic PDL.
In 15th ACM Symposium on Theory of Computing, 1983.
 [4]

Matthieu Sozeau and Nicolas Oury.
FirstClass Type Classes.
In Sofiène Tahar, Otmame AitMohamed, and César Muñoz,
editors, 21th International Conference on Theorem Proving in Higher
Order Logics, LNCS. SpringerVerlag, August 2008.
 [5]

The Coq Development Team.
The Coq Proof Assistant Reference Manual – Version V8.3,
2010.
.
This document was translated from L^{A}T_{E}X by
H^{E}V^{E}A.