Alea: a library for reasoning on randomized algorithms in Coq
with contributions by David Baelde and Pierre Courtieu
LRI, UMR 8623 Univ. Paris-Sud 11, CNRS & INRIA Saclay - Île-de-France
This library forms a basis for reasoning on randomised algorithms in
the proof assistant Coq . 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 . It
is developed in the framework of the SCALP
project (ANR-07-SESU-010) 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
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  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
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 :
- A few preliminary definitions, in
particular primitives for reasoning classically in Coq are defined.
- The definition of structures for ordered
sets and ω-complete partial orders (a monotonic sequence has
a least-upper bound). We define the type O1→m O2 of monotonic
functions and define the fixpoint-construction for monotonic
functionals. Continuity is also defined.
- 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 least-upper 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|
- Derived operations and properties of
operators on [0,1]. The main defined operations are:
This file defines a tactic Usimpl designed to help simplify expressions using operations on [0,1].
|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) ↦ xn||x ^ n||induction on n |
|generalized sum:||(f ∈ ℕ → [0,1],n∈ℕ) ↦
Σi=0i=n−1 f(i)||sigma f n||induction on n |
- Definition of the basic monad for
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.
- 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 :
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
|µ(f1+f2)||= µ(f1) + µ(f2) when f1 ≤ 1 − f2 |
|µ(k × f)||= k × µ (f) |
|µ(1− f)||≤ 1 − µ(f) |
|µ(lubn (f n))||≤ lubn (µ(f n)) when f is
a monotonic sequence of functions|
- a relaxed notion of distributions called sub-distributions suitable to model programs using both non-deterministic and random choice.
A sub-distribution is not additive but instead satisfies the following weaker properties:
|µ(f1) + µ(f2)||≤ µ(f1+f2) when f1 ≤ 1 − f2 |
|µ(f) & µ (g)||≤ µ (f & g)|
|µ(f+c)||≤ µ(f) + c |
- 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
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.
- 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 :
This file uses the library Sets.v which defines sets as predicates
and finite sets with an inductive definition.
|1 ≤ [a](IP) ∀ x, (P x) ⇒
k ≤ [b](f)|
|k ≤ [let x=a in b](f)|
- Definition of binomial coefficients.
- 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 p-1)
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) =
Proof that a distribution on a discrete domain is discrete.
This result is adapted from the Certicrypt development.
- This file introduces a tactic
rsimplmu which attempts to simplify expressions involving randomized programs.
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.
- 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 p1 and p2 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 pi evaluates Q not less than ki and
terminates with probability 1 then the
expression choice(p1,p2) evaluates Q not less than
k1(1−k2)+k2 (which is greater than both k1 and k2 when
k1 and k2 are not equal to 0).
- Construction of a distribution to pick uniformely an element in a list.
A simple formalisation of probabilistic Turing machines in ALEA.
- 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).
- 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].
- A general library to implement a minimimalization algorithm for a decidable predicat P on natural numbers, assuming a proof of ∃ n, P n.
- 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.
- Implementation of tactics Ring and Field on the set Rplus.
Philippe Audebaud and Christine Paulin-Mohring.
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.
Semantics of probabilistic programs.
J. of Computer and System Science, 1981.
A probabilistic PDL.
In 15th ACM Symposium on Theory of Computing, 1983.
Matthieu Sozeau and Nicolas Oury.
First-Class Type Classes.
In Sofiène Tahar, Otmame Ait-Mohamed, and César Muñoz,
editors, 21th International Conference on Theorem Proving in Higher
Order Logics, LNCS. Springer-Verlag, August 2008.
The Coq Development Team.
The Coq Proof Assistant Reference Manual – Version V8.3,
This document was translated from LATEX by