1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/assembly/".
17 include "nat/times.ma".
18 include "nat/compare.ma".
19 include "list/list.ma".
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)".
24 let rec matita_nat_of_coq_nat n ≝
27 | SS y ⇒ S (matita_nat_of_coq_nat y)
29 coercion cic:/matita/assembly/matita_nat_of_coq_nat.con.
30 alias num (instance 0) = "natural number".
32 definition byte ≝ nat.
33 definition addr ≝ nat.
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 *)
44 let rec cycles_of_opcode op ≝
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
55 inductive cartesian_product (A,B: Type) : Type ≝
56 couple: ∀a:A.∀b:B. cartesian_product A B.
58 definition opcodemap ≝
59 [ couple ? ? ADDd 171;
65 couple ? ? STAd 183 ].
67 definition opcode_of_byte ≝
75 match eqb (matita_nat_of_coq_nat n) b with
82 definition magic_of_opcode ≝
93 definition opcodeeqb ≝
94 λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
96 definition byte_of_opcode : opcode → byte ≝
100 [ nil ⇒ matita_nat_of_coq_nat 0
104 match opcodeeqb op op' with
105 [ true ⇒ matita_nat_of_coq_nat n
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).
117 definition byte_of_coq_nat : nat → byte ≝ matita_nat_of_coq_nat.
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).
125 definition mult_source : list byte ≝
127 #STAd; @18; (* 18 = locazione $12 *)
128 #LDAd; @17; (* 17 = locazione $11 *)
132 #ADDd; @16; (* 16 = locazione $10 *)
135 #BRA; @246; (* 246 = -10 *)
138 definition mult_source' : list byte.
140 record status : Type ≝ {
150 definition mult_status : status ≝
151 mk_status @0 @0 @0 false false (λa:addr. nth ? mult_source @0 a) 0.
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
163 (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
171 [ true ⇒ op1 + pc s (* signed!!! *)
187 let rec execute s n on n ≝
190 | S n' ⇒ execute (tick s) n'
193 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
197 lemma goo: execute mult_status (matita_nat_of_coq_nat 4) = mult_status.
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);
213 match match ? % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ?
215 [true\rArr ?|false\rArr ?]))) ?);
221 match % in opcode return ? with
233 match match % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ? with
234 [true\rArr ?|false\rArr ?])) ?);
239 match % in opcode return ? with
248 whd in \vdash (? ? (? match % in bool return ? with [true\rArr ?|false\rArr ?]) ?);
252 match % in opcode return ? with
261 whd in \vdash (? ? match % in bool return ? with [true\rArr ?|false\rArr ?] ?);
264 match % in opcode return ? with