Built with Alectryon, running Coq+SerAPI v8.12.0+0.12.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
6.826 lab assignments infrastructure
We include some libraries from the Coq standard library:
- List provides linked lists
- Arith provides lemmas for dealing with arithmetic
- Lia provides a tactic, lia, for proving simple arithmetic facts
Require Export List. Require Export Arith. Require Export Lia.
Helpers.Helpers has some definitions to augment the standard library, as well as a variety of proof automation (Ltac) used to simplify writing proofs with the POCS infrastructure.
Require Export Helpers.Helpers.
Helpers.Disk defines our disk model. Disks are defined as lists of blocks, with many helper functions and theorems.
Require Export Helpers.Disk.
Spec.Proc defines proc, the type of the procedures you'll write in 6.826. We also describe how these procedures run, including how procedures can crash and how the system can run a recovery procedure afterward.
Require Export Spec.Proc.
Spec.Abstraction defines how we write specifications in terms of abstraction relations.
Require Export Spec.Abstraction.
Spec.Recovery proves a number of theorems for reasoning about recovery across abstraction layers.
Require Export Spec.Recovery.
Spec.Loop provides loop combinators, along with a way of proving that the loop meets a specification by writing a loop invariant.
Require Export Spec.Loop.