Library POCS.POCS
6.826 lab assignments infrastructure
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.
Helpers.Disk defines our disk model. Disks are defined as lists of blocks,
with many helper functions and theorems.
Spec.Proc defines proc, the type of the programs you'll write in 6.826.
We also describe how these programs run, including how programs can crash and
how the system can run a recovery procedure afterward.
Spec.Abstraction defines how we write specifications in terms of
abstraction relations.
Spec.Recovery proves a number of theorems for reasoning about recovery
across abstraction layers.