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