Lab 2: Remapped disk

This lab will introduce you to working with more sophisticated code and spec states, and to our model of a disk storage system.

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.

To implement your bad-block remapper, you will need to interact with our representation of a disk. You should look through Helpers/Disk.v, which defines our disk model and provides a number of theorems for reasoning about disks. You may need to come back to this file as you are implementing and proving the correctness of your remapper to find the appropriate operations on disks and theorems about them.

You may find the following diagram helpful in thinking through your abstraction relation.

Submission for this lab is split into two parts:

• Lab 2A: Complete the write implementation and abstraction relation. You should also prove the example abstraction relation theorems, which will catch a variety of bugs. We recommend you try to also prove init_ok and start on read_ok (which may inform your abstraction relation), but you don't have to submit working proofs (that is, you can end those proofs with Admitted.).
• Lab 2B: Complete the rest of the lab. Specifically, you should prove init_ok, read_ok, write_ok, and size_ok.

When you are done with the lab assignment, run make lab2a-handin.tar.gz to generate a lab2a-handin.tar.gz file for part A (and, similarly, lab2b-handin.tar.gz for part B), and submit it via the submission web site. Please follow the same submission process for both parts of the lab.