Register-File Model

The MIPS-3k architecture features 32, 32-bit (word-sized) registers. We use the inductive type reg_t to enumerate the identifiers (constructors of reg_t).
  type reg_t =
    Zero | At | V0 | V1 | A0 | A1 | A2 | A3 
    | T0 | T1 | T2 | T3 | T4 | T5 | T6 | T7
    | S0 | S1 | S2 | S3 | S4 | S5 | S6 | S7
    | T8 | T9 | K0 | K1 | Gp | Sp | Fp | Ra


For simplicity, at this point, we model the data content by the int type which is unbound (infinite) in the whyML language. We store the the content in a map reg_t int, i.e., relating (mapping) each register to an integer value.

In order to allow the register content to be mutated (updated), we define the global variable r.

  (* maps reg_t -> v : int *)
  type reg_file_t = map reg_t int 

  (* mutable map *)
  val r : ref reg_file_t          


We define a set of predicates capturing the semantics of the register file. Predicates are here context free, so they take a register file r as an argument.

In a real MIPS you may write to register Zero, however without any effect. In our model we chose to disallow writes to Zero instead, just for simplicity.
  (* register Zero = 0 *)
  predicate reg_zero (r : reg_file_t) =
    r[Zero] = 0


reg_content r rn v asserts that the content or register rn is v.
  (* content of register rn = v *)
  predicate reg_content (r : reg_file_t) (rn : reg_t) (v : int) =
    r[rn] = v


reg_eg_preservation r r_old rn v, checks both content reg_content r rn v and that all other registers remain their old values.
  (* content & preservation besides rn *)
  predicate reg_preservation (r r_old : reg_file_t) (rn : reg_t) (v : int) =
    reg_content r rn v /\
    forall rn':reg_t. rn' <> rn ->
      r[rn'] = r_old[rn']  


We can now formulate the read with both contract and implementation.
  (* read register rn *)
  let read (rn : reg_t) : int
    ensures { reg_content !r rn result }
  =
    !r[rn] 


The write is guarded not to write to register Zero (requires { rn <> Zero }). In the contract !r refers to the state of r after the execution of write, while !(old r) refers to the state before the execution. Hence we can assert the preservation criterion (which will be needed later for verification).
  (* write register rn with value v *)
  let write (rn : reg_t) (v : int) 
    requires { rn <> Zero }
    ensures  { reg_preservation !r !(old r) rn v }
  =
    r := !r[rn <- v] 

end


We can now test (assert) the behaviour of the register file model.
module RegTest
  use import RegFile

  (* test raw access *)
  let test_raw () 
  = 
    r :=  !r[T0 <- 7];       (* raw write          *)
    assert { !r[T0] =  7 }   (* raw read           *)

  (* test contract, write and read *)
  let test_write ()
    requires { reg_zero !r } (* !r[Zero] = 0       *)
    requires { !r[T0] = 1 }
    requires { !r[T1] = 2 }
  = 
    assert { !r[T0] = 1 };   (* by contract        *)
    assert { !r[T1] = 2 };   (* by contract        *)
    write T1 3;
    assert { !r[T0] = 1 };   (* preservation       *)
    assert { !r[T1] = 3 };   (* 1) new content     *)
    let r = read T1 in
    assert { r = 3 };        (* 2) same as 1)      *)
    write Zero 3;            (* precondition fails *)

end


Assignment 1)
Give an implementation that adds the content fulfils the contract, i.e., computes A0 + A1 + A2 + A3 and stores the result in V0. (At this point you may of course cheat, by just assigning V0, right.)

  let sum1_A0_A1_A2_A3 () 
    requires { reg_zero !r } (* !r[Zero] = 0       *)
    requires { !r[A0] = 1 }
    requires { !r[A1] = 2 }
    requires { !r[A2] = 3 }
    requires { !r[A3] = 4 }

    ensures { !r[V0] = 10 }
 
  =  
    (* your code here *)

Assignment 2) Here the contract is stronger (i.e., the precondition is weaker) and the cheating is over!

Give an implementation that fulfils the the contract. (If you did not cheat in Assignment 1), the implementation will be the same.
let sum2_A0_A1_A2_A3 () 
    requires { reg_zero !r } (* !r[Zero] = 0       *)

    ensures { 
      let v = !(old r)[A0] + !(old r)[A1] + !(old r)[A2] + !(old r)[A3] in
      reg_preservation !r !(old r) V0 v
    }
  =  
    (* your code here *)

Assignment 3) Optional (well everything is optional, but this is extra optional).
Formulate a lemma (and prove) that
sum A0 A1 0 0 + sum 0 0 A2 A3 = sum A0 A1 A2 A3

To this end, you may formulate the lemma on the (logic) function:
function sum_a0_a1_a2_a3 (a0 a1 a2 a3 : int) : int =
    a0 + a1 + a2 + a3

Assignment 4) Extra super optional.

Show for the same thing for sum_A0_A1_A2_A3.

Seemingly simple a lemma approach turn out difficult (since we are dealing with stateful representations, i.e., the register file), but there is a way around it... When why3 checks a function, (e.g. let x (i j : int) = ....) it quantifies over all i, j. You may use this approach to quantify over the unknown register content, and then just prove that a program that computes sum A0 A1 0 0 + sum 0 0 A2 A3 renders sum A0 A1 A2 A3.

(It is essentially more difficult to prove properties of imperative programs, this is just one example...)
/Per Lindgren, September 2015