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

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 :

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 least-upper bound). We define the type O₁→^m O₂ of monotonic functions and define the fixpoint-construction 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 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 constants: (n∈ ℕ) ↦  1 1+n [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: (x,y) ↦  1 2  x +  1 2  y 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

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 :

µ(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.

SProbas

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

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](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.

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 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) = C_kⁿ 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₁ and p₂ 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₁,p₂) evaluates Q not less than k₁(1−k₂)+k₂ (which is greater than both k₁ and k₂ when k₁ and k₂ 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 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.

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

[5]

The Coq Development Team. The Coq Proof Assistant Reference Manual – Version V8.3, 2010. .

This document was translated from L^AT_EX by H^EV^EA.