Lab 1: StatDB

In this lab assignment, you will implement a database that supports adding numbers and getting the mean of the numbers added so far. The specification will keep track of all numbers added; your proof will connect your implementation to this specification.

To get started, clone the class repo at https://github.com/mit-pdos/6.826-2017-labs. Run make to build the starter code for the lab. We've provided a CLI to test your implementation, although we will only be checking your proof. You can try running it before starting the lab by running bin/statdb-cli, which should successfully build if your Coq and Haskell setup is working.

We recommend you begin by understanding the basics of the POCS infrastructure. The coqdoc documentation for the POCS module gives an overview, which is a good place to start. For the purposes of this lab, you can ignore the disk model.

Next, read the documentation for StatDB. We recommend reading the coqdoc in the following order:

1. Start with the StatDB API.
2. Next, read the API for the Variables module. You'll be implementing the StatDB using this API for storing the StatDB state.
3. Finally, read through the StatDB Implementation documentation. Some of this implementation is provided, as well as some starter code for the proofs. The assignment is to complete the exercises in this file.

When you are done with the lab assignment, run make prepare-submit to generate a lab1-handin.tar.gz file, and submit it via the submission web site.

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.