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 let rec cycles_of_opcode op ≝
  45  match op with
  46   [ ADDd ⇒ matita_nat_of_coq_nat 3
  47   | BEQ ⇒ matita_nat_of_coq_nat 3
  48   | BRA ⇒ matita_nat_of_coq_nat 3
  49   | DECd ⇒ matita_nat_of_coq_nat 5
  50   | LDAi ⇒ matita_nat_of_coq_nat 2
  51   | LDAd ⇒ matita_nat_of_coq_nat 3
  52   | STAd ⇒ matita_nat_of_coq_nat 3
  53   ].
  54
  55 inductive cartesian_product (A,B: Type) : Type ≝
  56  couple: ∀a:A.∀b:B. cartesian_product A B.
  57
  58 definition opcodemap ≝
  59  [ couple ? ? ADDd 171;
  60    couple ? ? BEQ 55;
  61    couple ? ? BRA 48;
  62    couple ? ? DECd 58;
  63    couple ? ? LDAi 166;
  64    couple ? ? LDAd 182;
  65    couple ? ? STAd 183 ].
  66
  67 definition opcode_of_byte ≝
  68  λb.
  69   let rec aux l ≝
  70    match l with
  71     [ nil ⇒ ADDd
  72     | cons c tl ⇒
  73        match c with
  74         [ couple op n ⇒
  75            match eqb (matita_nat_of_coq_nat n) b with
  76             [ true ⇒ op
  77             | false ⇒ aux tl
  78             ]]]
  79   in
  80    aux opcodemap.
  81
  82 definition magic_of_opcode ≝
  83  λop1.
  84   match op1 with
  85    [ ADDd ⇒ 0
  86    | BEQ ⇒  1
  87    | BRA ⇒  2
  88    | DECd ⇒ 3
  89    | LDAi ⇒ 4
  90    | LDAd ⇒ 5
  91    | STAd ⇒ 6 ].
  92
  93 definition opcodeeqb ≝
  94  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
  95
  96 definition byte_of_opcode : opcode → byte ≝
  97  λop.
  98   let rec aux l ≝
  99    match l with
 100     [ nil ⇒ matita_nat_of_coq_nat 0
 101     | cons c tl ⇒
 102        match c with
 103         [ couple op' n ⇒
 104            match opcodeeqb op op' with
 105             [ true ⇒ matita_nat_of_coq_nat n
 106             | false ⇒ aux tl
 107             ]]]
 108   in
 109    aux opcodemap.
 110
 111 notation "hvbox(# break a)"
 112   non associative with precedence 80
 113 for @{ 'byte_of_opcode $a }.
 114 interpretation "byte_of_opcode" 'byte_of_opcode a =
 115  (cic:/matita/assembly/byte_of_opcode.con a).
 116
 117 definition byte_of_coq_nat : nat → byte ≝ matita_nat_of_coq_nat.
 118
 119 notation "hvbox(@ break a)"
 120   non associative with precedence 80
 121 for @{ 'matita_nat_of_coq_nat $a }.
 122 interpretation "matita_nat_of_coq_nat" 'matita_nat_of_coq_nat a =
 123  (cic:/matita/assembly/byte_of_coq_nat.con a).
 124
 125 definition mult_source : list byte ≝
 126   [#LDAi; @0;
 127    #STAd; @18; (* 18 = locazione $12 *)
 128    #LDAd; @17; (* 17 = locazione $11 *)
 129    #BEQ;  @14;
 130    #LDAd; @18;
 131    #DECd; @17;
 132    #ADDd; @16; (* 16 = locazione $10 *)
 133    #STAd; @18;
 134    #LDAd; @17;
 135    #BRA;  @246; (* 246 = -10 *)
 136    #LDAd; @18].
 137
 138 definition mult_source' : list byte.
 139
 140 record status : Type ≝ {
 141   acc : byte;
 142   pc  : addr;
 143   spc : addr;
 144   zf  : bool;
 145   cf  : bool;
 146   mem : addr → byte;
 147   clk : nat
 148 }.
 149
 150 definition mult_status : status ≝
 151  mk_status @0 @0 @0 false false (λa:addr. nth ? mult_source @0 a) 0.
 152
 153 definition tick ≝
 154  λs:status.
 155   (* fetch *)
 156   let opc ≝ opcode_of_byte (mem s (pc s)) in
 157   let op1 ≝ mem s (S (pc s)) in
 158   let op2 ≝ mem s (S (S (pc s))) in
 159   let clk' ≝ cycles_of_opcode opc in
 160   match eqb (S (clk s)) clk' with
 161    [ false ⇒
 162        mk_status
 163         (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
 164    | true ⇒
 165       match opc with
 166        [ ADDd ⇒ s
 167        | BEQ ⇒
 168           mk_status
 169            (acc s)
 170            (match zf s with
 171              [ true ⇒ op1 + pc s   (* signed!!! *)
 172              | false ⇒ 2 + pc s
 173              ])
 174            (spc s)
 175            (zf s)
 176            (cf s)
 177            (mem s)
 178            0
 179        | BRA ⇒ s
 180        | DECd ⇒ s
 181        | LDAi ⇒ s
 182        | LDAd ⇒ s
 183        | STAd ⇒ s
 184        ]
 185    ].
 186
 187 let rec execute s n on n ≝
 188  match n with
 189   [ O ⇒ s
 190   | S n' ⇒ execute (tick s) n'
 191   ].
 192
 193 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
 194  intros; reflexivity.
 195 qed.
 196
 197 lemma goo: execute mult_status (matita_nat_of_coq_nat 4) = mult_status.
 198  simplify;
 199  change with (tick (tick (tick mult_status)) = mult_status);
 200  change with (tick (tick mult_status) = mult_status);
 201  change with (tick mult_status = mult_status);
 202  change with (mult_status = mult_status);
 203  reflexivity.
 204 qed.
 205
 206 (*
 207  unfold mult_status;
 208  simplify;
 209  whd in ⊢ (? ?
 210 (?
 211  (?
 212   (?
 213    match match ? % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ?
 214     with
 215    [true\rArr ?|false\rArr ?]))) ?);
 216  simplify;
 217  whd in ⊢ (? ?
 218 (?
 219  (?
 220   (?
 221    match % in opcode return ? with
 222    [ADDd\rArr ?
 223    |BEQ\rArr ?
 224    |BRA\rArr ?
 225    |DECd\rArr ?
 226    |LDAi\rArr ?
 227    |LDAd\rArr ?
 228    |STAd\rArr ?]))) ?);
 229  simplify;
 230  whd in \vdash (? ?
 231 (?
 232  (?
 233   match match % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ? with
 234   [true\rArr ?|false\rArr ?])) ?);
 235  simplify;
 236  whd in \vdash (? ?
 237 (?
 238  (?
 239   match % in opcode return ? with
 240   [ADDd\rArr ?
 241   |BEQ\rArr ?
 242   |BRA\rArr ?
 243   |DECd\rArr ?
 244   |LDAi\rArr ?
 245   |LDAd\rArr ?
 246   |STAd\rArr ?])) ?);
 247  simplify;
 248  whd in \vdash (? ? (? match % in bool return ? with [true\rArr ?|false\rArr ?]) ?);
 249  simplify;
 250  whd in \vdash (? ?
 251 (?
 252  match % in opcode return ? with
 253  [ADDd\rArr ?
 254  |BEQ\rArr ?
 255  |BRA\rArr ?
 256  |DECd\rArr ?
 257  |LDAi\rArr ?
 258  |LDAd\rArr ?
 259  |STAd\rArr ?]) ?);
 260  simplify;
 261  whd in \vdash (? ? match % in bool return ? with [true\rArr ?|false\rArr ?] ?);
 262  simplify;
 263  whd in \vdash (? ?
 264 match % in opcode return ? with
 265 [ADDd\rArr ?
 266 |BEQ\rArr ?
 267 |BRA\rArr ?
 268 |DECd\rArr ?
 269 |LDAi\rArr ?
 270 |LDAd\rArr ?
 271 |STAd\rArr ?] ?);
 272  simplify;
 273  reflexivity.
 274 *)