Disk model.

This file defines our model of a disk. We represent a disk as a list of 1KB blocks and provide functions to read and update disks, as well as theorems about these operations. In order to describe disks, we first provide a model of byte sequences.

Model of bytes.

In our lab assignments, we will model disks as consisting of blocks, which are in turn composed of bytes. Here, we define a notion of a byte array: the type of an array of n bytes will be bytes n. There's one unusual aspect of how we model bytes: instead of defining the bytes type in Coq, we simply add it as an Axiom. This means we are not providing a Coq (Gallina) implementation of bytes, and instead we are telling Coq to assume that there exists something called bytes, and there exist other functions that manipulate bytes that we define here as well (like bytes_dec to decide if two byte arrays are equal). When we generate executable code by extracting our Coq (Gallina) code into Haskell, we will be required to provide a Haskell implementation of any such Axiom. This correspondence is made below, using Extract Constant, and we (as developers) are responsible for making sure any axioms we state (like bsplit_bappend) are true of our Haskell implementations.

Two "initial" byte values: an all-zero array, bytes0, and an all-ones array, bytes1. We also promise that all-zero and all-ones arrays are different, as long as there's at least one element.

Model of blocks.

We represent blocks as a byte array of a fixed size. We define the block size as a separate constant, blockbytes, to avoid the literal constant 1024 reducing performance of proofs.

Mark blockbytes as opaque so that Coq doesn't expand it too eagerly.

Disk as a list of blocks.

Now we can define our model of a disk: a list of blocks. A disk with zero blocks is an empty list, nil.

We define three main operations on disks:

• diskGet d a gets the contents of an address a in disk d. It returns an option block, which is either a block value b (represented by Some b), or None if a is past the end of the disk.
• diskSize returns the size of the disk, which is just the length of the list representing the disk.
• diskUpd writes to a disk. Since Gallina is a functional language, we cannot update a disk "in-place", so instead diskUpd returns a new disk reflecting the write. Specifically, diskUpd d a b returns a new disk with address a updated to block value b, if a is in-bounds, or the original disk unchanged if a is out-of-bounds.

We address into disks with addr, which is simply a nat.

Coq v8.6 has a minor bug in the omega tactic, which is helpful in solving simple arithmetic goals. In particular, when we have arithmetic expressions that involve the addr type, omega gets confused because it doesn't see that addr is simply a wrapper for nat. This works around the bug, which should eventually be fixed by https://github.com/coq/coq/pull/876

We also define another helper operation, diskShrink, which takes a disk and drops the last block. This will be helpful in the bad-block-remapping lab assignment.

Finally, we prove a variety of theorems about the behavior of these disk operations.

Theorems about diskGet

Theorems about diskUpd

Theorems about diskShrink

We combine all of the above theorems into a hint database called "upd". This means that, when you type autorewrite with upd in some Coq proof, Coq will try to rewrite using all of the hints in that database. The using part of the hint tells Coq that all of the side conditions associated with the rewrite must be solved using the tactic specified in the using clause. This prevents Coq from applying a rewrite rule if some side condition (like an address being out-of-bounds) cannot be immediately proven.