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.
Read the documentation for the lab. We recommend reading the coqdoc in the following order:
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.
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:
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.