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/times.ma".
  18 include "nat/compare.ma".
  19 include "list/list.ma".
  20
  21 (*alias id "OO" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
  22 alias id "SS" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
  23
  24 let rec matita_nat_of_coq_nat n ≝
  25  match n with
  26   [ OO ⇒ O
  27   | SS y ⇒ S (matita_nat_of_coq_nat y)
  28   ].
  29 coercion cic:/matita/assembly/matita_nat_of_coq_nat.con.
  30 alias num (instance 0) = "natural number".
  31 *)
  32 definition byte ≝ nat.
  33 definition addr ≝ nat.
  34
  35 inductive opcode: Type ≝
  36    ADDd: opcode  (* 3 clock, 171 *)
  37  | BEQ: opcode   (* 3, 55 *)
  38  | BRA: opcode   (* 3, 48 *)
  39  | DECd: opcode  (* 5, 58 *)
  40  | LDAi: opcode  (* 2, 166 *)
  41  | LDAd: opcode  (* 3, 182 *)
  42  | STAd: opcode. (* 3, 183 *)
  43
  44 alias num (instance 0) = "natural number".
  45 let rec cycles_of_opcode op : nat ≝
  46  match op with
  47   [ ADDd ⇒ 3
  48   | BEQ ⇒ 3
  49   | BRA ⇒ 3
  50   | DECd ⇒ 5
  51   | LDAi ⇒ 2
  52   | LDAd ⇒ 3
  53   | STAd ⇒ 3
  54   ].
  55
  56 inductive cartesian_product (A,B: Type) : Type ≝
  57  couple: ∀a:A.∀b:B. cartesian_product A B.
  58
  59 definition opcodemap ≝
  60  [ couple ? ? ADDd 171;
  61    couple ? ? BEQ 55;
  62    couple ? ? BRA 48;
  63    couple ? ? DECd 58;
  64    couple ? ? LDAi 166;
  65    couple ? ? LDAd 182;
  66    couple ? ? STAd 183 ].
  67
  68 definition opcode_of_byte ≝
  69  λb.
  70   let rec aux l ≝
  71    match l with
  72     [ nil ⇒ ADDd
  73     | cons c tl ⇒
  74        match c with
  75         [ couple op n ⇒
  76            match eqb n b with
  77             [ true ⇒ op
  78             | false ⇒ aux tl
  79             ]]]
  80   in
  81    aux opcodemap.
  82
  83 definition magic_of_opcode ≝
  84  λop1.
  85   match op1 with
  86    [ ADDd ⇒ 0
  87    | BEQ ⇒  1
  88    | BRA ⇒  2
  89    | DECd ⇒ 3
  90    | LDAi ⇒ 4
  91    | LDAd ⇒ 5
  92    | STAd ⇒ 6 ].
  93
  94 definition opcodeeqb ≝
  95  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
  96
  97 definition byte_of_opcode : opcode → byte ≝
  98  λop.
  99   let rec aux l ≝
 100    match l with
 101     [ nil ⇒ 0
 102     | cons c tl ⇒
 103        match c with
 104         [ couple op' n ⇒
 105            match opcodeeqb op op' with
 106             [ true ⇒ n
 107             | false ⇒ aux tl
 108             ]]]
 109   in
 110    aux opcodemap.
 111
 112 notation "hvbox(# break a)"
 113   non associative with precedence 80
 114 for @{ 'byte_of_opcode $a }.
 115 interpretation "byte_of_opcode" 'byte_of_opcode a =
 116  (cic:/matita/assembly/byte_of_opcode.con a).
 117
 118 definition mult_source : list byte ≝
 119   [#LDAi; 0;
 120    #STAd; 32; (* 18 = locazione $12 *)
 121    #LDAd; 31; (* 17 = locazione $11 *)
 122    #BEQ;  12;
 123    #LDAd; 18;
 124    #DECd; 31;
 125    #ADDd; 30; (* 16 = locazione $10 *)
 126    #STAd; 32;
 127    #LDAd; 31;
 128    #BRA;  246; (* 242 = -14 *)
 129    #LDAd; 32].
 130
 131 definition mult_source' : list byte.
 132
 133 record status : Type ≝ {
 134   acc : byte;
 135   pc  : addr;
 136   spc : addr;
 137   zf  : bool;
 138   cf  : bool;
 139   mem : addr → byte;
 140   clk : nat
 141 }.
 142
 143 definition mult_status : status ≝
 144  mk_status 0 0 0 false false (λa:addr. nth ? mult_source 0 a) 0.
 145
 146 definition update ≝
 147  λf: addr → byte.λa.λv.λx.
 148   match eqb x a with
 149    [ true ⇒ v
 150    | false ⇒ f x ].
 151
 152 definition tick ≝
 153  λs:status.
 154   (* fetch *)
 155   let opc ≝ opcode_of_byte (mem s (pc s)) in
 156   let op1 ≝ mem s (S (pc s)) in
 157   let clk' ≝ cycles_of_opcode opc in
 158   match eqb (S (clk s)) clk' with
 159    [ true ⇒
 160       match opc with
 161        [ ADDd ⇒
 162           let x ≝ mem s op1 in
 163           let acc' ≝ x + acc s in (* signed!!! *)
 164            mk_status acc' (2 + pc s) (spc s)
 165             (eqb O acc') (cf s) (mem s) 0
 166        | BEQ ⇒
 167           mk_status
 168            (acc s)
 169            (match zf s with
 170              [ true ⇒ 2 + op1 + pc s   (* signed!!! *)
 171              | false ⇒ 2 + pc s
 172              ])
 173            (spc s)
 174            (zf s)
 175            (cf s)
 176            (mem s)
 177            0
 178        | BRA ⇒
 179           mk_status
 180            (acc s) (2 + op1 + pc s) (* signed!!! *)
 181            (spc s)
 182            (zf s)
 183            (cf s)
 184            (mem s)
 185            0
 186        | DECd ⇒
 187           let x ≝ pred (mem s op1) in (* signed!!! *)
 188           let mem' ≝ update (mem s) op1 x in
 189            mk_status (acc s) (2 + pc s) (spc s)
 190             (eqb O x) (cf s) mem' 0 (* check zb!!! *)
 191        | LDAi ⇒
 192           mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
 193        | LDAd ⇒
 194           let x ≝ pred (mem s op1) in
 195            mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
 196        | STAd ⇒
 197           mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
 198            (update (mem s) op1 (acc s)) 0
 199        ]
 200    | false ⇒
 201        mk_status
 202         (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
 203    ].
 204
 205 let rec execute s n on n ≝
 206  match n with
 207   [ O ⇒ s
 208   | S n' ⇒ execute (tick s) n'
 209   ].
 210
 211 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
 212  intros; reflexivity.
 213 qed.
 214
 215 lemma goo: True.
 216  letin s0 ≝ mult_status;
 217  letin pc0 ≝ (pc s0);
 218
 219  reduce in pc0;
 220  letin i0 ≝ (opcode_of_byte (mem s0 pc0));
 221  reduce in i0;
 222
 223  letin s1 ≝ (execute s0 (cycles_of_opcode i0));
 224  letin pc1 ≝ (pc s1);
 225  reduce in pc1;
 226  letin i1 ≝ (opcode_of_byte (mem s1 pc1));
 227  reduce in i1;
 228
 229  letin s2 ≝ (execute s1 (cycles_of_opcode i1));
 230  letin pc2 ≝ (pc s2);
 231  reduce in pc2;
 232  letin i2 ≝ (opcode_of_byte (mem s2 pc2));
 233  reduce in i2;
 234
 235  letin s3 ≝ (execute s2 (cycles_of_opcode i2));
 236  letin pc3 ≝ (pc s3);
 237  reduce in pc3;
 238  letin i3 ≝ (opcode_of_byte (mem s3 pc3));
 239  reduce in i3;
 240
 241  letin s4 ≝ (execute s3 (cycles_of_opcode i3));
 242  letin pc4 ≝ (pc s4);
 243  reduce in pc4;
 244  letin i4 ≝ (opcode_of_byte (mem s4 pc4));
 245  reduce in i4;
 246
 247  exact I.
 248 qed.