- Project 3 Extension
- Mystery tactics
- Crypto theory
- Project 3 is posted
- Runtime Checks to Type Checks
- Dependent Register File
- Bounded register file
- Array model from class
- distr_rev
- Eval on theorems

Blog

This model moves the assurance that an index use to access a register file is in range from runtime to type check time using a simple dependent type. This is based on Chlipala’s first dependent typing example.

```
Require Import Omega.
Require Import Maybe.
Module RegFileDep.
```

First we’ll define a simple function that calculates less than or equals over naturals and returns a `bool`

rather than a `Prop`

. This will be useful later.

```
Fixpoint leb (m:nat) : nat -> bool :=
match m with
| O => fun _:nat => true
| S m' =>
fun n:nat => match n with
| O => false
| S n' => leb m' n'
end
end.
```

Not much changes in the basic definitions of register contents or the register file itself.

```
Inductive RC : Type :=
| val : nat -> RC
| unknown : RC.
Notation "??" := unknown.
Definition RFC : Type := nat -> RC.
Inductive RF : Type :=
| file : nat -> RFC -> RF.
Definition empty_rf(s:nat):RF := file s (fun n:nat => ??).
Definition bound_check(i:nat)(r:RF):Prop :=
match r with
| file s _ => i <= s
end.
```

`get`

and `put`

are the first places where definitions change significantly. In both cases, the return type is a function from a `Prop`

to their traditional value. The result is a function that takes a proof that `bound_check`

holds for the given index and returns a register contents value.

Note the new values returned by the `match`

expression. They are now functions and not stack or contents values.

```
Definition get(i:nat)(f:RF):bound_check i f -> RC :=
match f with
| file s c => (fun p:bound_check i f => (c i))
end.
Definition put(i:nat)(f:RF)(v:RC):bound_check i f -> RF :=
match f with
| file s c => (fun p:bound_check i f =>
file s (fun n:nat => if (beq_nat i n) then v else c n))
end.
```

Following are my working examples to get from these new functions to proofs of their properties. They represent what I would put in a research notebook and scratch work.

```
Theorem bound_check_3_10: bound_check 3 (empty_rf 10).
Proof.
simpl. omega.
Qed.
Theorem bound_check_2_10: bound_check 2 (empty_rf 10).
Proof.
simpl. omega.
Qed.
Theorem bound_check_4_10: bound_check 4 (empty_rf 10).
Proof.
simpl. omega.
Qed.
Example test1: (get 3 ((put 3 (empty_rf 10) (val 3)) bound_check_3_10)) bound_check_3_10 = (val 3).
Proof.
reflexivity.
Qed.
Example test2: (get 2 ((put 3 (empty_rf 10) (val 3)) bound_check_3_10)) bound_check_2_10 = ??.
Proof. reflexivity. Qed.
Example test3: (get 4 ((put 3 (empty_rf 10) (val 3)) bound_check_3_10)) bound_check_4_10 = ??.
Proof. reflexivity. Qed.
Theorem update_position_3: forall m, (get 3 ((put 3 (empty_rf 10) (val m)) bound_check_3_10)) bound_check_3_10 = (val m).
Proof.
intros.
trivial.
Qed.
Theorem update_position_size: forall v s rfc, forall p:bound_check 3 (file s rfc),
leb 3 s = true -> (get 3 ((put 3 (file s rfc) (val v)) p)) = (fun p => val v).
Proof.
intros. unfold put. unfold bound_check.
simpl.
reflexivity.
Qed.
Lemma beq_refl: forall i, beq_nat i i = true.
Proof.
intros.
induction i.
reflexivity.
auto.
Qed.
Theorem empty_empty: forall i s,
(leb i s) = true -> (get i (empty_rf s)) = (fun p:bound_check i (empty_rf s) => ??).
Proof.
intros. simpl. reflexivity.
Qed.
```

Earlier versions had a proof, `unknown_oob`

, that showed any out-of-bounds access resulted in `??`

. This is gone because such accesses are now prevented by type checking.

Following are the two major correctness theorems for the register file `put`

and `get`

functions. First a check that updates occur following `put`

and then a check that values not accessed by a `put`

are not modified.

```
Theorem update_immediate: forall v i s rfc, forall p:bound_check i (file s rfc),
((get i ((put i (file s rfc) (val v)) p)) p) = val v.
Proof.
intros.
simpl.
rewrite beq_refl.
trivial.
Qed.
Theorem update_invariant: forall v i j s rfc,
forall p:bound_check i (file s rfc),
forall p':bound_check j (file s rfc),
(beq_nat j i) = false ->
((get i ((put j (file s rfc) (val v)) p')) p) = rfc i.
Proof.
intros.
simpl.
rewrite H.
trivial.
Qed.
End RegFileDep.
```