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 lemma eq_update_s_a_sa: ∀s,a,b. update s a (s a) b = s b.
 143  intros;
 144  unfold update;
 145  apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
 146   [ rewrite > (eqb_true_to_eq ? ? H);
 147     reflexivity
 148   | reflexivity
 149   ]
 150 qed.
 151
 152 lemma inj_update:
 153  ∀s,s',a,v,b. (a ≠ b → s b = s' b) → update s a v b = update s' a v b.
 154  intros;
 155  unfold update;
 156  apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
 157   [ reflexivity
 158   | apply H;
 159     intro;
 160     autobatch
 161   ]
 162 qed.
 163
 164 lemma not_eq_a_b_to_eq_update_a_b: ∀s,a,b,v. a ≠ b → update s a v b = s b.
 165  intros;
 166  unfold update;
 167  rewrite > not_eq_to_eqb_false; simplify;
 168   [ reflexivity
 169   | intro;
 170     autobatch
 171   ]
 172 qed.
 173
 174 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
 175
 176 definition tick ≝
 177  λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
 178   let opc ≝ opcode_of_byte (mem pc) in
 179   let op1 ≝ mem (S pc) in
 180   let clk' ≝ cycles_of_opcode opc in
 181   match eqb (S clk) clk' with
 182    [ true ⇒
 183       match opc with
 184        [ ADDd ⇒
 185           let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
 186           let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
 187           let c' ≝ match res with [ couple _ c' ⇒ c'] in
 188            mk_status acc' (2 + pc) spc
 189             (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
 190        | BEQ ⇒
 191           mk_status
 192            acc
 193            (match zf with
 194              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
 195                       (* FIXME: can't work - address truncated to 8 bits *)
 196              | false ⇒ 2 + pc
 197              ])
 198            spc
 199            zf
 200            cf
 201            mem
 202            0
 203        | BRA ⇒
 204           mk_status
 205            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
 206                                       (* FIXME: same as above *)
 207            spc
 208            zf
 209            cf
 210            mem
 211            0
 212        | DECd ⇒
 213           let x ≝ bpred (mem op1) in (* signed!!! *)
 214           let mem' ≝ update mem op1 x in
 215            mk_status acc (2 + pc) spc
 216             (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
 217        | LDAi ⇒
 218           mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
 219        | LDAd ⇒
 220           let x ≝ mem op1 in
 221            mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
 222        | STAd ⇒
 223           mk_status acc (2 + pc) spc zf cf
 224            (update mem op1 acc) 0
 225        ]
 226    | false ⇒
 227        mk_status
 228         acc pc spc zf cf mem (S clk)
 229    ]].
 230
 231 let rec execute s n on n ≝
 232  match n with
 233   [ O ⇒ s
 234   | S n' ⇒ execute (tick s) n'
 235   ].
 236
 237 lemma breakpoint:
 238  ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
 239  intros;
 240  generalize in match s; clear s;
 241  elim n1;
 242   [ reflexivity
 243   | simplify;
 244     apply H;
 245   ]
 246 qed.
 247
 248 axiom status_eq:
 249  ∀s,s'.
 250   acc s = acc s' →
 251   pc s = pc s' →
 252   spc s = spc s' →
 253   zf s = zf s' →
 254   cf s = cf s' →
 255   (∀a. mem s a = mem s' a) →
 256   clk s = clk s' →
 257    s=s'.