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.