Lab 2: Remapped disk

In this lab assignment, you will implement a remapped disk that takes a disk with a bad sector and exports an API with no bad sector (but a disk that is one sector smaller).

To get started, commit your work in the class repo locally and run git pull to merge in the new lab. Run make to compile the starter code for the lab.

We recommend you first briefly read src/Lab2/BadBlockAPI.v, which is the specification for the disk with a bad sector that you will build upon, and also src/Common/OneDiskAPI.v, which is the specification for a regular disk that your implementation will meet.

Your implementation will all be in src/Lab2/RemappedDiskImpl.v. We provide init and read, and leave you to implement write. Your most important task is to come up with a good abstraction relation for this problem. You will likely find that you discover new conditions needed in the abstraction relation as you work on the proofs.

Submission for this lab is split into two parts:

When you are done with the lab assignment, run make prepare-submit to generate a lab2-handin.tar.gz file, and submit it via the submission web site. Please follow the same submission process for both parts of the lab.

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at

Creative Commons License