Cage

Cage is a library and set of tools in Ssreflect-Coq for implementing and verifying convergence and quality bounds on game-based distributed systems such as distributed routers and load balancers. Cage includes, as a subcomponent, a verified implementation of the multiplicative weights update (MWU) algorithm:

• High-level implementation of MWU weights.v
• MWU DSL weightslang.v
• MWU DSL interpreter, along with correctness results weightsextract.v

An introduction to the research ideas underlying Cage (in the form of a technical paper) is forthcoming.

Prerequisites

• Coq 8.6
• Ssreflect 1.6.1
• OCaml (>= 4.02.1)
• Zarith OCaml library (>= 1.5)
• Ohio University Verification Toolsuite (OUVerT)
• Ohio University Verified Multiplicative Weights Update (MWU)

OPAM is the best way to install prereqs:

Using aptitude in debian/Ubuntu linux:

Install and set up OPAM:

apt-get install opam
opam init
opam switch 4.02.3
eval `opam config env`

Once OPAM is set-up with OCaml (>= 4.02.1):

opam install coq.8.6
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect.1.6.1
apt-get install libgmp-dev
opam install zarith
opam install coq-mathcomp-algebra

Build Instructions

• Type make in the toplevel directory.