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
  16
  17 include "assembly/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 notation "hvbox(# break a)"
  99   non associative with precedence 80
 100 for @{ 'byte_of_opcode $a }.
 101 interpretation "byte_of_opcode" 'byte_of_opcode a =
 102  (cic:/matita/assembly/vm/byte_of_opcode.con a).
 103
 104 record status : Type ≝ {
 105   acc : byte;
 106   pc  : addr;
 107   spc : addr;
 108   zf  : bool;
 109   cf  : bool;
 110   mem : addr → byte;
 111   clk : nat
 112 }.
 113
 114 notation "{hvbox('Acc' ≝ acc ; break 'Pc' ≝ pc ; break 'Spc' ≝ spc ; break 'Fz' ≝ fz ; break 'Fc' ≝ fc ; break  'M' ≝ m ; break 'Clk' ≝ clk)}"
 115 non associative with precedence 80 for
 116  @{ 'mkstatus $acc $pc $spc $fz $fc $m $clk }.
 117
 118 interpretation "mk_status" 'mkstatus acc pc spc fz fc m clk =
 119  (cic:/matita/assembly/vm/status.ind#xpointer(1/1/1) acc pc spc fz fc m clk).
 120
 121 definition update ≝
 122  λf: addr → byte.λa.λv.λx.
 123   match eqb x a with
 124    [ true ⇒ v
 125    | false ⇒ f x ].
 126
 127 notation "hvbox(m break {a ↦ break v})" non associative with precedence 80 for
 128  @{ 'update $m $a $v }.
 129
 130 notation "hvbox(m break {a ↦ break v} \nbsp x)" non associative with precedence 80 for
 131  @{ 'update4 $m $a $v $x }.
 132
 133 interpretation "update" 'update m a v =
 134   (cic:/matita/assembly/vm/update.con m a v).
 135
 136 interpretation "update4" 'update4 m a v x =
 137   (cic:/matita/assembly/vm/update.con m a v x).
 138
 139 lemma update_update_a_a:
 140  ∀s,a,v1,v2,b.
 141   update (update s a v1) a v2 b = update s a v2 b.
 142  intros;
 143  unfold update;
 144  unfold update;
 145  elim (eqb b a);
 146  reflexivity.
 147 qed.
 148
 149 lemma update_update_a_b:
 150  ∀s,a1,v1,a2,v2,b.
 151   a1 ≠ a2 →
 152    update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
 153  intros;
 154  unfold update;
 155  unfold update;
 156  apply (bool_elim ? (eqb b a1)); intros;
 157  apply (bool_elim ? (eqb b a2)); intros;
 158  simplify;
 159  [ elim H;
 160    rewrite < (eqb_true_to_eq ? ? H1);
 161    apply eqb_true_to_eq;
 162    assumption
 163  |*: reflexivity
 164  ].
 165 qed.
 166
 167 lemma eq_update_s_a_sa: ∀s,a,b. update s a (s a) b = s b.
 168  intros;
 169  unfold update;
 170  apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
 171   [ rewrite > (eqb_true_to_eq ? ? H);
 172     reflexivity
 173   | reflexivity
 174   ]
 175 qed.
 176
 177 lemma inj_update:
 178  ∀s,s',a,v,b. (a ≠ b → s b = s' b) → update s a v b = update s' a v b.
 179  intros;
 180  unfold update;
 181  apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
 182   [ reflexivity
 183   | apply H;
 184     intro;
 185     autobatch
 186   ]
 187 qed.
 188
 189 lemma not_eq_a_b_to_eq_update_a_b: ∀s,a,b,v. a ≠ b → update s a v b = s b.
 190  intros;
 191  unfold update;
 192  rewrite > not_eq_to_eqb_false; simplify;
 193   [ reflexivity
 194   | intro;
 195     autobatch
 196   ]
 197 qed.
 198
 199 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
 200
 201 definition tick ≝
 202  λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
 203   let opc ≝ opcode_of_byte (mem pc) in
 204   let op1 ≝ mem (S pc) in
 205   let clk' ≝ cycles_of_opcode opc in
 206   match eqb (S clk) clk' with
 207    [ true ⇒
 208       match opc with
 209        [ ADDd ⇒
 210           let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
 211           let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
 212           let c' ≝ match res with [ couple _ c' ⇒ c'] in
 213            mk_status acc' (2 + pc) spc
 214             (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
 215        | BEQ ⇒
 216           mk_status
 217            acc
 218            (match zf with
 219              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
 220                       (* FIXME: can't work - address truncated to 8 bits *)
 221              | false ⇒ 2 + pc
 222              ])
 223            spc
 224            zf
 225            cf
 226            mem
 227            0
 228        | BRA ⇒
 229           mk_status
 230            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
 231                                       (* FIXME: same as above *)
 232            spc
 233            zf
 234            cf
 235            mem
 236            0
 237        | DECd ⇒
 238           let x ≝ bpred (mem op1) in (* signed!!! *)
 239           let mem' ≝ update mem op1 x in
 240            mk_status acc (2 + pc) spc
 241             (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
 242        | LDAi ⇒
 243           mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
 244        | LDAd ⇒
 245           let x ≝ mem op1 in
 246            mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
 247        | STAd ⇒
 248           mk_status acc (2 + pc) spc zf cf
 249            (update mem op1 acc) 0
 250        ]
 251    | false ⇒
 252        mk_status
 253         acc pc spc zf cf mem (S clk)
 254    ]].
 255
 256 let rec execute s n on n ≝
 257  match n with
 258   [ O ⇒ s
 259   | S n' ⇒ execute (tick s) n'
 260   ].
 261
 262 lemma breakpoint:
 263  ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
 264  intros;
 265  generalize in match s; clear s;
 266  elim n1;
 267   [ reflexivity
 268   | simplify;
 269     apply H;
 270   ]
 271 qed.
 272
 273 axiom status_eq:
 274  ∀s,s'.
 275   acc s = acc s' →
 276   pc s = pc s' →
 277   spc s = spc s' →
 278   zf s = zf s' →
 279   cf s = cf s' →
 280   (∀a. mem s a = mem s' a) →
 281   clk s = clk s' →
 282    s=s'.