EECS 755

Software Requirements Modeling and Analysis

Index
Blog

Dependent Register File

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.