matita/library/assembly/assembly.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/".
  16
  17 include "nat/div_and_mod.ma".
  18 (*include "nat/compare.ma".*)
  19 include "list/list.ma".
  20
  21 inductive exadecimal : Type ≝
  22    x0: exadecimal
  23  | x1: exadecimal
  24  | x2: exadecimal
  25  | x3: exadecimal
  26  | x4: exadecimal
  27  | x5: exadecimal
  28  | x6: exadecimal
  29  | x7: exadecimal
  30  | x8: exadecimal
  31  | x9: exadecimal
  32  | xA: exadecimal
  33  | xB: exadecimal
  34  | xC: exadecimal
  35  | xD: exadecimal
  36  | xE: exadecimal
  37  | xF: exadecimal.
  38
  39 record byte : Type ≝ {
  40  bh: exadecimal;
  41  bl: exadecimal
  42 }.
  43
  44 definition eqex ≝
  45  λb1,b2.
  46   match b1 with
  47    [ x0 ⇒
  48        match b2 with
  49         [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  50         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  51         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  52         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  53    | x1 ⇒
  54        match b2 with
  55         [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
  56         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  57         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  58         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  59    | x2 ⇒
  60        match b2 with
  61         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
  62         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  63         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  64         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  65    | x3 ⇒
  66        match b2 with
  67         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
  68         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  69         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  70         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  71    | x4 ⇒
  72        match b2 with
  73         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  74         | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  75         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  76         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  77    | x5 ⇒
  78        match b2 with
  79         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  80         | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
  81         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  82         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  83    | x6 ⇒
  84        match b2 with
  85         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  86         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
  87         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  88         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  89    | x7 ⇒
  90        match b2 with
  91         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  92         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
  93         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  94         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  95    | x8 ⇒
  96        match b2 with
  97         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  98         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  99         | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 100         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 101    | x9 ⇒
 102        match b2 with
 103         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 104         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 105         | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 106         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 107    | xA ⇒
 108        match b2 with
 109         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 110         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 111         | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
 112         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 113    | xB ⇒
 114        match b2 with
 115         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 116         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 117         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 118         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 119    | xC ⇒
 120        match b2 with
 121         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 122         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 123         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 124         | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 125    | xD ⇒
 126        match b2 with
 127         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 128         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 129         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 130         | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 131    | xE ⇒
 132        match b2 with
 133         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 134         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 135         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 136         | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ]
 137    | xF ⇒
 138        match b2 with
 139         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 140         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 141         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 142         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]].
 143
 144
 145 definition eqbyte ≝
 146  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
 147
 148 alias num (instance 0) = "natural number".
 149 definition nat_of_exadecimal ≝
 150  λb.
 151   match b with
 152    [ x0 ⇒ 0
 153    | x1 ⇒ 1
 154    | x2 ⇒ 2
 155    | x3 ⇒ 3
 156    | x4 ⇒ 4
 157    | x5 ⇒ 5
 158    | x6 ⇒ 6
 159    | x7 ⇒ 7
 160    | x8 ⇒ 8
 161    | x9 ⇒ 9
 162    | x10 ⇒ 10
 163    | x11 ⇒ 11
 164    | x12 ⇒ 12
 165    | x13 ⇒ 13
 166    | x14 ⇒ 14
 167    | x15 ⇒ 15
 168    ].
 169
 170 coercion cic:/matita/assembly/nat_of_exadecimal.con.
 171
 172 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
 173
 174 coercion cic:/matita/assembly/nat_of_byte.con.
 175
 176 definition exadecimal_of_nat ≝
 177  λb.
 178   match b with [ O ⇒ x0 | S b ⇒
 179   match b with [ O ⇒ x1 | S b ⇒
 180   match b with [ O ⇒ x2 | S b ⇒
 181   match b with [ O ⇒ x3 | S b ⇒
 182   match b with [ O ⇒ x4 | S b ⇒
 183   match b with [ O ⇒ x5 | S b ⇒
 184   match b with [ O ⇒ x6 | S b ⇒
 185   match b with [ O ⇒ x7 | S b ⇒
 186   match b with [ O ⇒ x8 | S b ⇒
 187   match b with [ O ⇒ x9 | S b ⇒
 188   match b with [ O ⇒ xA | S b ⇒
 189   match b with [ O ⇒ xB | S b ⇒
 190   match b with [ O ⇒ xC | S b ⇒
 191   match b with [ O ⇒ xD | S b ⇒
 192   match b with [ O ⇒ xE | S b ⇒
 193   match b with [ O ⇒ xF | S b ⇒ x0]]]]]]]]]]]]]]]].
 194
 195 definition byte_of_nat ≝
 196  λn. mk_byte (exadecimal_of_nat ((n / 16) \mod 16)) (exadecimal_of_nat (n \mod 16)).
 197
 198 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
 199  intros;
 200  elim b;
 201  elim e;
 202  elim e1;
 203  reflexivity.
 204 qed.
 205
 206 lemma sign_ok: byte_of_nat 257 = mk_byte x0 x1.
 207  reflexivity.
 208 qed.
 209
 210 definition addr ≝ nat.
 211
 212 definition xpred ≝
 213  λb.
 214   match b with
 215    [ x0 ⇒ xF
 216    | x1 ⇒ x0
 217    | x2 ⇒ x1
 218    | x3 ⇒ x2
 219    | x4 ⇒ x3
 220    | x5 ⇒ x4
 221    | x6 ⇒ x5
 222    | x7 ⇒ x6
 223    | x8 ⇒ x7
 224    | x9 ⇒ x8
 225    | xA ⇒ x9
 226    | xB ⇒ xA
 227    | xC ⇒ xB
 228    | xD ⇒ xC
 229    | xE ⇒ xD
 230    | xF ⇒ xE ].
 231
 232 definition bpred ≝
 233  λb.
 234   match eqex (bl b) x0 with
 235    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
 236    | false ⇒ mk_byte (bh b) (xpred (bl b))
 237    ].
 238
 239 (* way too slow!
 240 lemma bpred_pred:
 241  ∀b.
 242   match eqbyte b (mk_byte x0 x0) with
 243    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
 244    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
 245  intros;
 246  elim b;
 247  elim e;
 248  elim e1;
 249  whd;
 250  reflexivity.
 251 qed.
 252 *)
 253
 254 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
 255
 256 coercion cic:/matita/assembly/addr_of_byte.con.
 257
 258 inductive opcode: Type ≝
 259    ADDd: opcode  (* 3 clock, 171 *)
 260  | BEQ: opcode   (* 3, 55 *)
 261  | BRA: opcode   (* 3, 48 *)
 262  | DECd: opcode  (* 5, 58 *)
 263  | LDAi: opcode  (* 2, 166 *)
 264  | LDAd: opcode  (* 3, 182 *)
 265  | STAd: opcode. (* 3, 183 *)
 266
 267 let rec cycles_of_opcode op : nat ≝
 268  match op with
 269   [ ADDd ⇒ 3
 270   | BEQ ⇒ 3
 271   | BRA ⇒ 3
 272   | DECd ⇒ 5
 273   | LDAi ⇒ 2
 274   | LDAd ⇒ 3
 275   | STAd ⇒ 3
 276   ].
 277
 278 inductive cartesian_product (A,B: Type) : Type ≝
 279  couple: ∀a:A.∀b:B. cartesian_product A B.
 280
 281 definition opcodemap ≝
 282  [ couple ? ? ADDd (mk_byte xA xB);
 283    couple ? ? BEQ (mk_byte x3 x7);
 284    couple ? ? BRA (mk_byte x3 x0);
 285    couple ? ? DECd (mk_byte x3 xA);
 286    couple ? ? LDAi (mk_byte xA x6);
 287    couple ? ? LDAd (mk_byte xB x6);
 288    couple ? ? STAd (mk_byte xB x7) ].
 289
 290 definition opcode_of_byte ≝
 291  λb.
 292   let rec aux l ≝
 293    match l with
 294     [ nil ⇒ ADDd
 295     | cons c tl ⇒
 296        match c with
 297         [ couple op n ⇒
 298            match eqbyte n b with
 299             [ true ⇒ op
 300             | false ⇒ aux tl
 301             ]]]
 302   in
 303    aux opcodemap.
 304
 305 definition magic_of_opcode ≝
 306  λop1.
 307   match op1 with
 308    [ ADDd ⇒ 0
 309    | BEQ ⇒  1
 310    | BRA ⇒  2
 311    | DECd ⇒ 3
 312    | LDAi ⇒ 4
 313    | LDAd ⇒ 5
 314    | STAd ⇒ 6 ].
 315
 316 definition opcodeeqb ≝
 317  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
 318
 319 definition byte_of_opcode : opcode → byte ≝
 320  λop.
 321   let rec aux l ≝
 322    match l with
 323     [ nil ⇒ mk_byte x0 x0
 324     | cons c tl ⇒
 325        match c with
 326         [ couple op' n ⇒
 327            match opcodeeqb op op' with
 328             [ true ⇒ n
 329             | false ⇒ aux tl
 330             ]]]
 331   in
 332    aux opcodemap.
 333
 334 notation "hvbox(# break a)"
 335   non associative with precedence 80
 336 for @{ 'byte_of_opcode $a }.
 337 interpretation "byte_of_opcode" 'byte_of_opcode a =
 338  (cic:/matita/assembly/byte_of_opcode.con a).
 339
 340 definition mult_source : list byte ≝
 341   [#LDAi; mk_byte x0 x0;
 342    #STAd; mk_byte x2 x0; (* 18 = locazione $12 *)
 343    #LDAd; mk_byte x1 xF; (* 17 = locazione $11 *)
 344    #BEQ;  mk_byte x0 xC;
 345    #LDAd; mk_byte x1 x2;
 346    #DECd; mk_byte x1 xF;
 347    #ADDd; mk_byte x1 xE; (* 16 = locazione $10 *)
 348    #STAd; mk_byte x2 x0;
 349    #LDAd; mk_byte x1 xF;
 350    #BRA;  mk_byte xF x2; (* 242 = -14 *)
 351    #LDAd; mk_byte x2 x0].
 352
 353 record status : Type ≝ {
 354   acc : byte;
 355   pc  : addr;
 356   spc : addr;
 357   zf  : bool;
 358   cf  : bool;
 359   mem : addr → byte;
 360   clk : nat
 361 }.
 362
 363 definition mult_status : status ≝
 364  mk_status (mk_byte x0 x0) 0 0 false false
 365   (λa:addr. nth ? mult_source (mk_byte x0 x0) a) 0.
 366
 367 definition update ≝
 368  λf: addr → byte.λa.λv.λx.
 369   match eqb x a with
 370    [ true ⇒ v
 371    | false ⇒ f x ].
 372
 373 definition tick ≝
 374  λs:status.
 375   (* fetch *)
 376   let opc ≝ opcode_of_byte (mem s (pc s)) in
 377   let op1 ≝ mem s (S (pc s)) in
 378   let clk' ≝ cycles_of_opcode opc in
 379   match eqb (S (clk s)) clk' with
 380    [ true ⇒
 381       match opc with
 382        [ ADDd ⇒
 383           let x ≝ nat_of_byte (mem s op1) in
 384           let acc' ≝ x + acc s in (* signed!!! *)
 385            mk_status (byte_of_nat acc') (2 + pc s) (spc s)
 386             (eqb O acc') (cf s) (mem s) 0
 387        | BEQ ⇒
 388           mk_status
 389            (acc s)
 390            (match zf s with
 391              [ true ⇒ 2 + op1 + pc s   (* signed!!! *)
 392              | false ⇒ 2 + pc s
 393              ])
 394            (spc s)
 395            (zf s)
 396            (cf s)
 397            (mem s)
 398            0
 399        | BRA ⇒
 400           mk_status
 401            (acc s) (2 + op1 + pc s) (* signed!!! *)
 402            (spc s)
 403            (zf s)
 404            (cf s)
 405            (mem s)
 406            0
 407        | DECd ⇒
 408           let x ≝ bpred (mem s op1) in (* signed!!! *)
 409           let mem' ≝ update (mem s) op1 x in
 410            mk_status (acc s) (2 + pc s) (spc s)
 411             (eqb O x) (cf s) mem' 0 (* check zb!!! *)
 412        | LDAi ⇒
 413           mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
 414        | LDAd ⇒
 415           let x ≝ bpred (mem s op1) in
 416            mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
 417        | STAd ⇒
 418           mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
 419            (update (mem s) op1 (acc s)) 0
 420        ]
 421    | false ⇒
 422        mk_status
 423         (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
 424    ].
 425
 426 let rec execute s n on n ≝
 427  match n with
 428   [ O ⇒ s
 429   | S n' ⇒ execute (tick s) n'
 430   ].
 431
 432 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
 433  intros; reflexivity.
 434 qed.
 435
 436 lemma goo: True.
 437  letin s0 ≝ mult_status;
 438  letin pc0 ≝ (pc s0);
 439
 440  reduce in pc0;
 441  letin i0 ≝ (opcode_of_byte (mem s0 pc0));
 442  reduce in i0;
 443
 444  letin s1 ≝ (execute s0 (cycles_of_opcode i0));
 445  letin pc1 ≝ (pc s1);
 446  reduce in pc1;
 447  letin i1 ≝ (opcode_of_byte (mem s1 pc1));
 448  reduce in i1;
 449
 450  letin s2 ≝ (execute s1 (cycles_of_opcode i1));
 451  letin pc2 ≝ (pc s2);
 452  reduce in pc2;
 453  letin i2 ≝ (opcode_of_byte (mem s2 pc2));
 454  reduce in i2;
 455
 456  letin s3 ≝ (execute s2 (cycles_of_opcode i2));
 457  letin pc3 ≝ (pc s3);
 458  reduce in pc3;
 459  letin i3 ≝ (opcode_of_byte (mem s3 pc3));
 460  reduce in i3;
 461
 462  letin s4 ≝ (execute s3 (cycles_of_opcode i3));
 463  letin pc4 ≝ (pc s4);
 464  reduce in pc4;
 465  letin i4 ≝ (opcode_of_byte (mem s4 pc4));
 466  reduce in i4;
 467
 468  exact I.
 469 qed.