# Library POCS.Helpers.Disk

Require Import Omega.

Require Import RelationClasses.

Require Import List.

Require Import Helpers.

Set Implicit Arguments.

Require Import RelationClasses.

Require Import List.

Require Import Helpers.

Set Implicit Arguments.

# Disk model.

# Model of bytes.

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.

Axiom bytes0 : forall n, bytes n.

Axiom bytes1 : forall n, bytes n.

Axiom bytes_differ : forall n, n > 0 -> bytes0 n <> bytes1 n.

Definition bnull : bytes 0 := bytes0 0.

Axiom bappend : forall n1 n2, bytes n1 -> bytes n2 -> bytes (n1+n2).

Axiom bsplit : forall n1 n2, bytes (n1+n2) -> bytes n1 * bytes n2.

Axiom bsplit_bappend : forall n1 n2 (b1 : bytes n1) (b2 : bytes n2), bsplit (bappend b1 b2) = (b1, b2).

Fixpoint bsplit_list {n} {m} : bytes (n * m) -> list (bytes m) :=

match n with

| O => fun _ => nil

| S n' => fun (bs : bytes ((S n') * m)) =>

let (this, rest) := bsplit bs in

this :: bsplit_list rest

end.

Extraction Language Haskell.

Extract Constant bytes => "Data.ByteString.ByteString".

Extract Constant bytes_dec => "(\n b1 b2 -> b1 Prelude.== b2)".

Extract Constant bytes0 => "(\n -> Data.ByteString.replicate (Prelude.fromIntegral n) 0)".

Extract Constant bappend => "(\_ _ bs1 bs2 -> Data.ByteString.append bs1 bs2)".

Extract Constant bsplit => "(\n1 _ bs -> Data.ByteString.splitAt (Prelude.fromIntegral n1) bs)".

# Model of blocks.

Definition blockbytes := 1024.

Definition block := bytes blockbytes.

Definition block0 : block := bytes0 _.

Definition block1 : block := bytes1 _.

Theorem block0_block1_differ : block0 <> block1.

Hint Resolve block0_block1_differ.

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

# Disk as a list of blocks.

We define three main operations on disks:
We address into disks with addr, which is simply a nat.

- 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.

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

Local Ltac omega_orig := omega.

Ltac omega := unfold addr in *; omega_orig.

Definition diskGet (d : disk) (a : addr) : option block :=

nth_error d a.

Definition diskSize (d : disk) : nat := length d.

Fixpoint diskUpd d (a: addr) b : disk :=

match d with

| nil => nil

| db :: drest =>

match a with

| O => b :: drest

| S a' => db :: diskUpd drest a' b

end

end.

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

Theorem disk_inbounds_exists : forall a d,

a < diskSize d ->

exists b, diskGet d a = Some b.

Theorem disk_inbounds_not_none : forall a d,

a < diskSize d ->

diskGet d a = None ->

False.

Theorem disk_none_oob : forall a d,

diskGet d a = None ->

~a < diskSize d.

Theorem disk_oob_eq : forall d a,

~a < diskSize d ->

diskGet d a = None.

Theorem disk_ext_eq : forall d d',

(forall a, diskGet d a = diskGet d' a) ->

d = d'.

Theorem disk_ext_inbounds_eq : forall d d',

diskSize d = diskSize d' ->

(forall a, a < diskSize d -> diskGet d a = diskGet d' a) ->

d = d'.

Theorem diskUpd_eq_some : forall d a b0 b,

diskGet d a = Some b0 ->

diskGet (diskUpd d a b) a = Some b.

Theorem diskUpd_eq : forall d a b,

a < diskSize d ->

diskGet (diskUpd d a b) a = Some b.

Theorem diskUpd_size : forall d a b,

diskSize (diskUpd d a b) = diskSize d.

Theorem diskUpd_oob_eq : forall d a b,

~a < diskSize d ->

diskGet (diskUpd d a b) a = None.

Theorem diskUpd_neq : forall d a b a',

a <> a' ->

diskGet (diskUpd d a b) a' = diskGet d a'.

Theorem diskUpd_none : forall d a b,

diskGet d a = None ->

diskUpd d a b = d.

Theorem diskUpd_same : forall d a b,

diskGet d a = Some b ->

diskUpd d a b = d.

Theorem diskUpd_twice : forall d a b b',

diskUpd (diskUpd d a b) a b' = diskUpd d a b'.

Theorem diskUpd_oob_noop : forall d a b,

~a < diskSize d ->

diskUpd d a b = d.

Theorem diskShrink_size : forall d,

diskSize d <> 0 ->

diskSize (diskShrink d) = diskSize d - 1.

Theorem diskShrink_preserves : forall d a,

a <> diskSize (diskShrink d) ->

diskGet (diskShrink d) a = diskGet d a.

Theorem diskShrink_diskUpd_last : forall d a b,

a >= diskSize d - 1 ->

diskShrink (diskUpd d a b) = diskShrink d.

Theorem diskShrink_diskUpd_notlast : forall d a b,

a < diskSize d - 1 ->

diskShrink (diskUpd d a b) = diskUpd (diskShrink d) a b.

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.

Hint Rewrite diskUpd_eq using (solve [ auto ]) : upd.

Hint Rewrite disk_oob_eq using (solve [ auto ]) : upd.

Hint Rewrite diskUpd_oob_eq using (solve [ auto ]) : upd.

Hint Rewrite diskUpd_size : upd.

Hint Rewrite diskUpd_neq using (solve [ auto ]) : upd.

Hint Rewrite diskUpd_none using (solve [ auto ]) : upd.

Hint Rewrite diskUpd_same using (solve [ auto ]) : upd.

Hint Rewrite diskUpd_oob_noop using (solve [ auto ]) : upd.

Hint Rewrite diskUpd_twice : upd.

Hint Rewrite diskShrink_size using (solve [ auto || omega ]) : upd.

Hint Rewrite diskShrink_preserves using (solve [ auto || omega ]) : upd.

Hint Rewrite diskShrink_diskUpd_last using (solve [ auto || omega ]) : upd.

Hint Rewrite diskShrink_diskUpd_notlast using (solve [ auto || omega ]) : upd.