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