Alea: a library for reasoning on randomized algorithms in Coq
Version 8

Christine Paulin-Mohring
with contributions by David Baelde and Pierre Courtieu
LRI, UMR 8623 Univ. Paris-Sud 11, CNRS & INRIA Saclay - Île-de-France

May 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 (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 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 :

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 O1m 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:
OperationMeaningCoq Notation 
bounded addition :(x,y)↦ min(x+y,1)x+y
multiplication :(x,y)↦ x ×   yx*y 
division:(x,y)↦ min(x / y,1)x/y 
inverse function:x ↦ 1−x[1−]x
(n∈ ℕ) ↦ 
Derived operations and properties of operators on [0,1]. The main defined operations are:
OperationMeaningCoq NotationAlea definition
bounded subtraction:(x,y)↦ max(xy,0)xy[1−]([1−]x + y)
maximum:(x,y) ↦ max(x,y)max x y(xy)+y 
minimum:(x,y) ↦ min(x,y)min x y[1−]((yx)+[1−]y
addition dual:(x,y) ↦ max(x+y−1,0)x & y[1−]([1−]x+[1−]y
difference:(x,y) ↦ |xy|diff  x  y(xy) + (yx
(x,y) ↦ 
 x + 
mean x y[1/2]x+[1/2] y 
multiple:(n∈ℕ,x) ↦ nxn */ xinduction on n 
power:(n∈ℕ,x) ↦ xnx  ^  ninduction on n 
generalized sum:(f ∈ ℕ → [0,1],n∈ℕ) ↦ Σi=0i=n−1 f(i)sigma f ninduction on n 
This file defines a tactic Usimpl designed to help simplify expressions using operations on [0,1].
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.
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 :
µ(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
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.
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 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.

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](IP)     ∀ 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.
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) = Ckn pk(1−p)nk.
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.

3  Examples

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 natnat 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 xy 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.
Dexter Kozen. Semantics of probabilistic programs. J. of Computer and System Science, 1981.
Dexter Kozen. 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, 2010. .

This document was translated from LATEX by HEVEA.