<commit_before>Verdi Raft
==========

[![Build Status](https://api.travis-ci.org/uwplse/verdi-raft.svg?branch=master)](https://travis-ci.org/uwplse/verdi-raft)

An implementation of the [Raft](https://raft.github.io) distributed consensus protocol, verified in Coq using the Verdi framework.

Requirements
------------

Definitions and proofs:

- [`Coq 8.6`](https://coq.inria.fr/coq-86)
- [`Verdi`](https://github.com/uwplse/verdi)
- [`StructTact`](https://github.com/uwplse/StructTact)
- [`Cheerios`](https://github.com/uwplse/cheerios)

Executable `vard` key-value store:

- [`OCaml 4.02.3`](https://ocaml.org/docs/install.html) (or later)
- [`OCamlbuild`](https://github.com/ocaml/ocamlbuild)
- [`verdi-runtime`](https://github.com/DistributedComponents/verdi-runtime)
- [`cheerios-runtime`](https://github.com/uwplse/cheerios)

Client for `vard`:

- [`Python 2.7`](https://www.python.org/download/releases/2.7/)

Integration testing of `vard`:

- [`Python 2.7`](https://www.python.org/download/releases/2.7/)

Unit testing of unverified `vard` code:

- [`OUnit 2.0.0`](http://ounit.forge.ocamlcore.org)

Building
--------

We recommend installing the dependencies of Verdi Raft via
[OPAM](http://opam.ocaml.org/doc/Install.html):

```
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
opam install verdi StructTact verdi-runtime ocamlbuild cheerios verdi-cheerios cheerios-runtime
```

Then, run `./configure` in the Verdi Raft root directory.  This will check
for the appropriate version of Coq and ensure all necessary
Coq dependencies can be located. By default, `Verdi`, `StructTact`,
and `Cheerios` are assumed to be installed in Coq's
`user-contrib` directory, but this can be overridden by setting the
`Verdi_PATH`, `StructTact_PATH`, and `Cheerios_PATH` environment variables.

Finally, run `make` in the root directory. This will compile the Raft
implementation and proof interfaces, and check all the proofs.

To build the `vard` key-value store program in `extraction/vard`,
run `make vard` in the root directory. If the implementation has<commit_msg>fix install instructions in README.md<commit_after>Verdi Raft
==========

[![Build Status](https://api.travis-ci.org/uwplse/verdi-raft.svg?branch=master)](https://travis-ci.org/uwplse/verdi-raft)

An implementation of the [Raft](https://raft.github.io) distributed consensus protocol, verified in Coq using the Verdi framework.

Requirements
------------

Definitions and proofs:

- [`Coq 8.6`](https://coq.inria.fr/coq-86)
- [`Verdi`](https://github.com/uwplse/verdi)
- [`StructTact`](https://github.com/uwplse/StructTact)
- [`Cheerios`](https://github.com/uwplse/cheerios)

Executable `vard` key-value store:

- [`OCaml 4.02.3`](https://ocaml.org/docs/install.html) (or later)
- [`OCamlbuild`](https://github.com/ocaml/ocamlbuild)
- [`verdi-runtime`](https://github.com/DistributedComponents/verdi-runtime)
- [`cheerios-runtime`](https://github.com/uwplse/cheerios)

Client for `vard`:

- [`Python 2.7`](https://www.python.org/download/releases/2.7/)

Integration testing of `vard`:

- [`Python 2.7`](https://www.python.org/download/releases/2.7/)

Unit testing of unverified `vard` code:

- [`OUnit 2.0.0`](http://ounit.forge.ocamlcore.org)

Building
--------

We recommend installing the dependencies of Verdi Raft via
[OPAM](http://opam.ocaml.org/doc/Install.html):

```
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
opam install verdi StructTact verdi-runtime ocamlbuild cheerios cheerios-runtime
```

Then, run `./configure` in the Verdi Raft root directory.  This will check
for the appropriate version of Coq and ensure all necessary
Coq dependencies can be located. By default, `Verdi`, `StructTact`,
and `Cheerios` are assumed to be installed in Coq's
`user-contrib` directory, but this can be overridden by setting the
`Verdi_PATH`, `StructTact_PATH`, and `Cheerios_PATH` environment variables.

Finally, run `make` in the root directory. This will compile the Raft
implementation and proof interfaces, and check all the proofs.

To build the `vard` key-value store program in `extraction/vard`,
run `make vard` in the root directory. If the implementation has
{'fraction_non_alphanumeric': 0.154698683906719, 'fraction_numerical': 0.008773955206649734, 'mean_word_length': 4.640625, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 28, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2382802', 'n_tokens_mistral': 1504, 'n_tokens_neox': 1429, 'n_words': 372}