Lab 1: Hoare logic and StatDB

This lab assignment will introduce you to the basics of formal reasoning about the correctness of code, using Hoare logic and state abstraction.

To get started, clone the class repo at https://github.com/mit-pdos/6.826-2020-labs. Run make to build the starter code for the lab.

We recommend you begin by understanding the basics of the POCS infrastructure. The coqdoc documentation for the Proc, Loop, and (for part B especially) Abstraction modules, as well as the top-level POCS module, are a good place to start. For the purposes of this lab, you can ignore the disk model.

Part A: Hoare logic

Read the documentation for the lab. We recommend reading the coqdoc in the following order:

1. Start with the variables API.
2. Next, look at the the Exercises.v file. You'll be writing various procedures, specifications, and proofs in this file. This file is part A of this lab.

Once you have familiarized yourself with the reading, open up src/Lab1/Exercises.v and start working on the exercises for part A of this lab. When you are done with part A, run make lab1a-handin.tar.gz to generate a lab1a-handin.tar.gz file, and submit it via the submission web site.

Part B: StatDB

In part B, 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, but the implementation will just keep track of two variables (the sum and the count of numbers seen so far). Your proof will connect your implementation to the specification.

You may want to commit your work for part A, using git commit, before you proceed with part B.

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 make bin/statdb-cli followed by ./bin/statdb-cli, which should successfully build if your Coq and Haskell setup is working.

We recommend that you begin by reading the documentation for StatDB. We recommend reading the coqdoc in the following order:

1. Start with the StatDB API.
2. You have already seen 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 lab1b-handin.tar.gz to generate a lab1b-handin.tar.gz file, and submit it via the submission web site.