Verdi Aggregation

An implementation of a distributed aggregation protocol, verified in Coq using the Verdi framework.

Requirements

Definitions and proofs:

• Coq 8.6
• Verdi
• math-comp (ssreflect, fingroup, algebra)
• StructTact
• InfSeqExt
• AAC_tactics
• Cheerios
• verdi-cheerios

Executable code:

• OCaml 4.02.3 (or later)
• OCamlbuild
• ocamlfind
• verdi-runtime
• Uuidm
• PortAudio
• ocaml-portaudio

Integration testing of executable code:

• Python 2.7

Unit testing of unverified code:

• OUnit 2.0.0

Building

First, make sure the PortAudio library is installed on the system; on Ubuntu and Debian systems, the package is called portaudio19-dev.

The recommended way to install the OCaml and Coq dependencies of Verdi Aggregation is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
opam install coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-aac-tactics \
 verdi StructTact InfSeqExt cheerios verdi-cheerios verdi-runtime uuidm portaudio

Then, run ./configure in the root directory. This will check for the appropriate version of Coq and ensure all necessary dependencies can be located.

By default, the script assumes that Verdi, StructTact, InfSeqExt, Cheerios, and VerdiCheerios are installed in Coq's user-contrib directory, but this can be overridden by setting the Verdi_PATH, StructTact_PATH, InfSeqExt_PATH, Cheerios_PATH, and VerdiCheerios_PATH environment variables.

Finally, run make in the root directory.