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.
153 alias id "update" = "cic:/Marseille/GC/card/card/update.con".
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
164 (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
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
176 [ true ⇒ 2 + op1 + pc s (* signed!!! *)
186 (acc s) (2 + op1 + pc s) (* signed!!! *)
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!!! *)
203 let rec execute s n on n ≝
206 | S n' ⇒ execute (tick s) n'
209 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
213 lemma goo: execute mult_status (matita_nat_of_coq_nat 4) = mult_status.
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);
229 match match ? % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ?
231 [true\rArr ?|false\rArr ?]))) ?);
237 match % in opcode return ? with
249 match match % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ? with
250 [true\rArr ?|false\rArr ?])) ?);
255 match % in opcode return ? with
264 whd in \vdash (? ? (? match % in bool return ? with [true\rArr ?|false\rArr ?]) ?);
268 match % in opcode return ? with
277 whd in \vdash (? ? match % in bool return ? with [true\rArr ?|false\rArr ?] ?);
280 match % in opcode return ? with