helm/software/matita/library/assembly/vm.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/assembly/vm/".
  16
  17 include "byte.ma".
  18
  19 definition addr ≝ nat.
  20
  21 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
  22
  23 coercion cic:/matita/assembly/vm/addr_of_byte.con.
  24
  25 inductive opcode: Type ≝
  26    ADDd: opcode  (* 3 clock, 171 *)
  27  | BEQ: opcode   (* 3, 55 *)
  28  | BRA: opcode   (* 3, 48 *)
  29  | DECd: opcode  (* 5, 58 *)
  30  | LDAi: opcode  (* 2, 166 *)
  31  | LDAd: opcode  (* 3, 182 *)
  32  | STAd: opcode. (* 3, 183 *)
  33
  34 let rec cycles_of_opcode op : nat ≝
  35  match op with
  36   [ ADDd ⇒ 3
  37   | BEQ ⇒ 3
  38   | BRA ⇒ 3
  39   | DECd ⇒ 5
  40   | LDAi ⇒ 2
  41   | LDAd ⇒ 3
  42   | STAd ⇒ 3
  43   ].
  44
  45 definition opcodemap ≝
  46  [ couple ? ? ADDd (mk_byte xA xB);
  47    couple ? ? BEQ (mk_byte x3 x7);
  48    couple ? ? BRA (mk_byte x3 x0);
  49    couple ? ? DECd (mk_byte x3 xA);
  50    couple ? ? LDAi (mk_byte xA x6);
  51    couple ? ? LDAd (mk_byte xB x6);
  52    couple ? ? STAd (mk_byte xB x7) ].
  53
  54 definition opcode_of_byte ≝
  55  λb.
  56   let rec aux l ≝
  57    match l with
  58     [ nil ⇒ ADDd
  59     | cons c tl ⇒
  60        match c with
  61         [ couple op n ⇒
  62            match eqbyte n b with
  63             [ true ⇒ op
  64             | false ⇒ aux tl
  65             ]]]
  66   in
  67    aux opcodemap.
  68
  69 definition magic_of_opcode ≝
  70  λop1.
  71   match op1 with
  72    [ ADDd ⇒ 0
  73    | BEQ ⇒  1
  74    | BRA ⇒  2
  75    | DECd ⇒ 3
  76    | LDAi ⇒ 4
  77    | LDAd ⇒ 5
  78    | STAd ⇒ 6 ].
  79
  80 definition opcodeeqb ≝
  81  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
  82
  83 definition byte_of_opcode : opcode → byte ≝
  84  λop.
  85   let rec aux l ≝
  86    match l with
  87     [ nil ⇒ mk_byte x0 x0
  88     | cons c tl ⇒
  89        match c with
  90         [ couple op' n ⇒
  91            match opcodeeqb op op' with
  92             [ true ⇒ n
  93             | false ⇒ aux tl
  94             ]]]
  95   in
  96    aux opcodemap.
  97
  98 record status : Type ≝ {
  99   acc : byte;
 100   pc  : addr;
 101   spc : addr;
 102   zf  : bool;
 103   cf  : bool;
 104   mem : addr → byte;
 105   clk : nat
 106 }.
 107
 108 definition update ≝
 109  λf: addr → byte.λa.λv.λx.
 110   match eqb x a with
 111    [ true ⇒ v
 112    | false ⇒ f x ].
 113
 114 lemma update_update_a_a:
 115  ∀s,a,v1,v2,b.
 116   update (update s a v1) a v2 b = update s a v2 b.
 117  intros;
 118  unfold update;
 119  unfold update;
 120  elim (eqb b a);
 121  reflexivity.
 122 qed.
 123
 124 lemma update_update_a_b:
 125  ∀s,a1,v1,a2,v2,b.
 126   a1 ≠ a2 →
 127    update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
 128  intros;
 129  unfold update;
 130  unfold update;
 131  apply (bool_elim ? (eqb b a1)); intros;
 132  apply (bool_elim ? (eqb b a2)); intros;
 133  simplify;
 134  [ elim H;
 135    rewrite < (eqb_true_to_eq ? ? H1);
 136    apply eqb_true_to_eq;
 137    assumption
 138  |*: reflexivity
 139  ].
 140 qed.
 141
 142 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
 143
 144 definition tick ≝
 145  λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
 146   let opc ≝ opcode_of_byte (mem pc) in
 147   let op1 ≝ mem (S pc) in
 148   let clk' ≝ cycles_of_opcode opc in
 149   match eqb (S clk) clk' with
 150    [ true ⇒
 151       match opc with
 152        [ ADDd ⇒
 153           let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
 154           let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
 155           let c' ≝ match res with [ couple _ c' ⇒ c'] in
 156            mk_status acc' (2 + pc) spc
 157             (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
 158        | BEQ ⇒
 159           mk_status
 160            acc
 161            (match zf with
 162              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
 163                       (* FIXME: can't work - address truncated to 8 bits *)
 164              | false ⇒ 2 + pc
 165              ])
 166            spc
 167            zf
 168            cf
 169            mem
 170            0
 171        | BRA ⇒
 172           mk_status
 173            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
 174                                       (* FIXME: same as above *)
 175            spc
 176            zf
 177            cf
 178            mem
 179            0
 180        | DECd ⇒
 181           let x ≝ bpred (mem op1) in (* signed!!! *)
 182           let mem' ≝ update mem op1 x in
 183            mk_status acc (2 + pc) spc
 184             (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
 185        | LDAi ⇒
 186           mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
 187        | LDAd ⇒
 188           let x ≝ mem op1 in
 189            mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
 190        | STAd ⇒
 191           mk_status acc (2 + pc) spc zf cf
 192            (update mem op1 acc) 0
 193        ]
 194    | false ⇒
 195        mk_status
 196         acc pc spc zf cf mem (S clk)
 197    ]].
 198
 199 let rec execute s n on n ≝
 200  match n with
 201   [ O ⇒ s
 202   | S n' ⇒ execute (tick s) n'
 203   ].
 204
 205 lemma breakpoint:
 206  ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
 207  intros;
 208  generalize in match s; clear s;
 209  elim n1;
 210   [ reflexivity
 211   | simplify;
 212     apply H;
 213   ]
 214 qed.
 215
 216 axiom status_eq:
 217  ∀s,s'.
 218   acc s = acc s' →
 219   pc s = pc s' →
 220   spc s = spc s' →
 221   zf s = zf s' →
 222   cf s = cf s' →
 223   (∀a. mem s a = mem s' a) →
 224   clk s = clk s' →
 225    s=s'.