helm/software/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 record status : Type ≝ {
 335   acc : byte;
 336   pc  : addr;
 337   spc : addr;
 338   zf  : bool;
 339   cf  : bool;
 340   mem : addr → byte;
 341   clk : nat
 342 }.
 343
 344 definition update ≝
 345  λf: addr → byte.λa.λv.λx.
 346   match eqb x a with
 347    [ true ⇒ v
 348    | false ⇒ f x ].
 349
 350 definition tick ≝
 351  λs:status.
 352   (* fetch *)
 353   let opc ≝ opcode_of_byte (mem s (pc s)) in
 354   let op1 ≝ mem s (S (pc s)) in
 355   let clk' ≝ cycles_of_opcode opc in
 356   match eqb (S (clk s)) clk' with
 357    [ true ⇒
 358       match opc with
 359        [ ADDd ⇒
 360           let x ≝ nat_of_byte (mem s op1) in
 361           let acc' ≝ x + acc s in (* signed!!! *)
 362            mk_status (byte_of_nat acc') (2 + pc s) (spc s)
 363             (eqb O acc') (cf s) (mem s) 0
 364        | BEQ ⇒
 365           mk_status
 366            (acc s)
 367            (match zf s with
 368              [ true ⇒ 2 + op1 + pc s   (* signed!!! *)
 369              | false ⇒ 2 + pc s
 370              ])
 371            (spc s)
 372            (zf s)
 373            (cf s)
 374            (mem s)
 375            0
 376        | BRA ⇒
 377           mk_status
 378            (acc s) (2 + op1 + pc s) (* signed!!! *)
 379            (spc s)
 380            (zf s)
 381            (cf s)
 382            (mem s)
 383            0
 384        | DECd ⇒
 385           let x ≝ bpred (mem s op1) in (* signed!!! *)
 386           let mem' ≝ update (mem s) op1 x in
 387            mk_status (acc s) (2 + pc s) (spc s)
 388             (eqb O x) (cf s) mem' 0 (* check zb!!! *)
 389        | LDAi ⇒
 390           mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
 391        | LDAd ⇒
 392           let x ≝ bpred (mem s op1) in
 393            mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
 394        | STAd ⇒
 395           mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
 396            (update (mem s) op1 (acc s)) 0
 397        ]
 398    | false ⇒
 399        mk_status
 400         (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
 401    ].
 402
 403 let rec execute s n on n ≝
 404  match n with
 405   [ O ⇒ s
 406   | S n' ⇒ execute (tick s) n'
 407   ].
 408
 409 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
 410  intros; reflexivity.
 411 qed.
 412
 413 notation "hvbox(# break a)"
 414   non associative with precedence 80
 415 for @{ 'byte_of_opcode $a }.
 416 interpretation "byte_of_opcode" 'byte_of_opcode a =
 417  (cic:/matita/assembly/byte_of_opcode.con a).
 418
 419 definition mult_source : list byte ≝
 420   [#LDAi; mk_byte x0 x0;
 421    #STAd; mk_byte x2 x0; (* 18 = locazione $12 *)
 422    #LDAd; mk_byte x1 xF; (* 17 = locazione $11 *)
 423    #BEQ;  mk_byte x0 xC;
 424    #LDAd; mk_byte x1 x2;
 425    #DECd; mk_byte x1 xF;
 426    #ADDd; mk_byte x1 xE; (* 16 = locazione $10 *)
 427    #STAd; mk_byte x2 x0;
 428    #LDAd; mk_byte x1 xF;
 429    #BRA;  mk_byte xF x2; (* 242 = -14 *)
 430    #LDAd; mk_byte x2 x0].
 431
 432 definition mult_status ≝
 433  λx,y.
 434   mk_status (mk_byte x0 x0) 0 0 false false
 435    (λa:addr.
 436      match leb a 29 with
 437       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
 438       | false ⇒
 439          match eqb a 30 with
 440           [ true ⇒ x
 441           | false ⇒ y
 442           ]
 443       ]) 0.
 444
 445 lemma goo1:
 446  ∀x.
 447   (λi.
 448     let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
 449      pc s = 22 ∧ mem s 32 = byte_of_nat 0) 14.
 450  intros;
 451  whd;
 452  split;
 453   [ reduce;
 454     reflexivity
 455   | reduce;
 456     reflexivity
 457   ].
 458
 459
 460 lemma goo1:
 461  ∀x.
 462   let i ≝ 14 in
 463   let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
 464    pc s = 22 ∧ mem s 32 = byte_of_nat 0.
 465  intros;
 466  split;
 467   [ reduce;
 468
 469   |
 470   ].
 471 qed.
 472
 473 lemma goo1:
 474  ∀x,y.
 475   let i ≝ 14 + 23 * nat_of_byte y in
 476   let s ≝ execute (mult_status x y) i in
 477    pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
 478  intros;
 479 qed.
 480
 481 lemma goo: True.
 482  letin s0 ≝ mult_status;
 483  letin pc0 ≝ (pc s0);
 484  reduce in pc0;
 485  letin i0 ≝ (opcode_of_byte (mem s0 pc0));
 486  reduce in i0;
 487
 488  letin s1 ≝ (execute s0 (cycles_of_opcode i0));
 489  letin pc1 ≝ (pc s1);
 490  reduce in pc1;
 491  letin i1 ≝ (opcode_of_byte (mem s1 pc1));
 492  reduce in i1;
 493
 494  letin s2 ≝ (execute s1 (cycles_of_opcode i1));
 495  letin pc2 ≝ (pc s2);
 496  reduce in pc2;
 497  letin i2 ≝ (opcode_of_byte (mem s2 pc2));
 498  reduce in i2;
 499
 500  letin s3 ≝ (execute s2 (cycles_of_opcode i2));
 501  letin pc3 ≝ (pc s3);
 502  reduce in pc3;
 503  letin i3 ≝ (opcode_of_byte (mem s3 pc3));
 504  reduce in i3;
 505  letin zf3 ≝ (zf s3);
 506  reduce in zf3;
 507
 508  letin s4 ≝ (execute s3 (cycles_of_opcode i3));
 509  letin pc4 ≝ (pc s4);
 510  reduce in pc4;
 511  letin i4 ≝ (opcode_of_byte (mem s4 pc4));
 512  reduce in i4;
 513
 514  letin s5 ≝ (execute s4 (cycles_of_opcode i4));
 515  letin pc5 ≝ (pc s5);
 516  reduce in pc5;
 517  letin i5 ≝ (opcode_of_byte (mem s5 pc5));
 518  reduce in i5;
 519
 520  letin s6 ≝ (execute s5 (cycles_of_opcode i5));
 521  letin pc6 ≝ (pc s6);
 522  reduce in pc6;
 523  letin i6 ≝ (opcode_of_byte (mem s6 pc6));
 524  reduce in i6;
 525
 526  letin s7 ≝ (execute s6 (cycles_of_opcode i6));
 527  letin pc7 ≝ (pc s7);
 528  reduce in pc7;
 529  letin i7 ≝ (opcode_of_byte (mem s7 pc7));
 530  reduce in i7;
 531
 532  letin s8 ≝ (execute s7 (cycles_of_opcode i7));
 533  letin pc8 ≝ (pc s8);
 534  reduce in pc8;
 535  letin i8 ≝ (opcode_of_byte (mem s8 pc8));
 536  reduce in i8;
 537
 538  letin s9 ≝ (execute s8 (cycles_of_opcode i8));
 539  letin pc9 ≝ (pc s9);
 540  reduce in pc9;
 541  letin i9 ≝ (opcode_of_byte (mem s9 pc9));
 542  reduce in i9;
 543
 544  exact I.
 545 qed.