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 op2 ≝ mem s (S (S (pc s))) in
 158   let clk' ≝ cycles_of_opcode opc in
 159   match eqb (S (clk s)) clk' with
 160    [ false ⇒
 161        mk_status
 162         (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
 163    | true ⇒
 164       match opc with
 165        [ ADDd ⇒
 166           let x ≝ mem s op1 in
 167           let acc' ≝ x + acc s in (* signed!!! *)
 168            mk_status acc' (2 + pc s) (spc s)
 169             (eqb O acc') (cf s) (mem s) 0
 170        | BEQ ⇒
 171           mk_status
 172            (acc s)
 173            (match zf s with
 174              [ true ⇒ 2 + op1 + pc s   (* signed!!! *)
 175              | false ⇒ 2 + pc s
 176              ])
 177            (spc s)
 178            (zf s)
 179            (cf s)
 180            (mem s)
 181            0
 182        | BRA ⇒
 183           mk_status
 184            (acc s) (2 + op1 + pc s) (* signed!!! *)
 185            (spc s)
 186            (zf s)
 187            (cf s)
 188            (mem s)
 189            0
 190        | DECd ⇒
 191           let x ≝ pred (mem s op1) in (* signed!!! *)
 192           let mem' ≝ update (mem s) op1 x in
 193            mk_status (acc s) (2 + pc s) (spc s)
 194             (eqb O x) (cf s) mem' 0 (* check zb!!! *)
 195        | LDAi ⇒
 196           mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
 197        | LDAd ⇒
 198           let x ≝ pred (mem s op1) in
 199            mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
 200        | STAd ⇒
 201           mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
 202            (update (mem s) op1 (acc s)) 0
 203        ]
 204    ].
 205
 206 let rec execute s n on n ≝
 207  match n with
 208   [ O ⇒ s
 209   | S n' ⇒ execute (tick s) n'
 210   ].
 211
 212 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
 213  intros; reflexivity.
 214 qed.
 215 (*
 216 lemma goo: pc (execute mult_status 4) = O.
 217  reduce;
 218  CSC.
 219
 220
 221  simplify;
 222  whd in ⊢ (? ? (? (? (? %))) ?);
 223  do 2 (simplify in match (matita_nat_of_coq_nat ?));
 224  simplify in match (matita_nat_of_coq_nat ?);
 225  whd in ⊢ (? ? (? (? (? (? ? ? ? ? ? ? %)))) ?);
 226  whd in ⊢ (? ? (? (? (? %))) ?);
 227
 228
 229
 230
 231
 232
 233
 234
 235
 236
 237
 238
 239  change with (tick (tick (tick mult_status)) = mult_status);
 240  change with (tick (tick mult_status) = mult_status);
 241  change with (tick mult_status = mult_status);
 242  change with (mult_status = mult_status);
 243  reflexivity.
 244 qed.
 245
 246 (*
 247  unfold mult_status;
 248  simplify;
 249  whd in ⊢ (? ?
 250 (?
 251  (?
 252   (?
 253    match match ? % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ?
 254     with
 255    [true\rArr ?|false\rArr ?]))) ?);
 256  simplify;
 257  whd in ⊢ (? ?
 258 (?
 259  (?
 260   (?
 261    match % in opcode return ? with
 262    [ADDd\rArr ?
 263    |BEQ\rArr ?
 264    |BRA\rArr ?
 265    |DECd\rArr ?
 266    |LDAi\rArr ?
 267    |LDAd\rArr ?
 268    |STAd\rArr ?]))) ?);
 269  simplify;
 270  whd in \vdash (? ?
 271 (?
 272  (?
 273   match match % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ? with
 274   [true\rArr ?|false\rArr ?])) ?);
 275  simplify;
 276  whd in \vdash (? ?
 277 (?
 278  (?
 279   match % in opcode return ? with
 280   [ADDd\rArr ?
 281   |BEQ\rArr ?
 282   |BRA\rArr ?
 283   |DECd\rArr ?
 284   |LDAi\rArr ?
 285   |LDAd\rArr ?
 286   |STAd\rArr ?])) ?);
 287  simplify;
 288  whd in \vdash (? ? (? match % in bool return ? with [true\rArr ?|false\rArr ?]) ?);
 289  simplify;
 290  whd in \vdash (? ?
 291 (?
 292  match % in opcode return ? with
 293  [ADDd\rArr ?
 294  |BEQ\rArr ?
 295  |BRA\rArr ?
 296  |DECd\rArr ?
 297  |LDAi\rArr ?
 298  |LDAd\rArr ?
 299  |STAd\rArr ?]) ?);
 300  simplify;
 301  whd in \vdash (? ? match % in bool return ? with [true\rArr ?|false\rArr ?] ?);
 302  simplify;
 303  whd in \vdash (? ?
 304 match % in opcode return ? with
 305 [ADDd\rArr ?
 306 |BEQ\rArr ?
 307 |BRA\rArr ?
 308 |DECd\rArr ?
 309 |LDAi\rArr ?
 310 |LDAd\rArr ?
 311 |STAd\rArr ?] ?);
 312  simplify;
 313  reflexivity.
 314 *)
 315 *)