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/div_and_mod_new.ma".
18 (*include "nat/compare.ma".*)
19 include "list/list.ma".
21 inductive exadecimal : Type ≝
39 record byte : Type ≝ {
49 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
50 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
51 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
52 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
55 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
56 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
57 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
58 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
61 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ false
62 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
63 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
64 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
67 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
68 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
69 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
70 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
73 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
74 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
75 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
76 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
79 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
80 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
81 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
82 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
85 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
86 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ false
87 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
88 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
91 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
92 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
93 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
94 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
97 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
98 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
99 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
100 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
103 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
104 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
105 | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ false
106 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
109 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
110 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
111 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ false
112 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
115 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
116 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
117 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
118 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
121 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
122 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
123 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
124 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
127 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
128 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
129 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
130 | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
133 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
134 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
135 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
136 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ false ]
139 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
140 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
141 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
142 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]].
146 λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
148 alias num (instance 0) = "natural number".
149 definition nat_of_exadecimal ≝
170 coercion cic:/matita/assembly/nat_of_exadecimal.con.
172 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
174 coercion cic:/matita/assembly/nat_of_byte.con.
176 definition exadecimal_of_nat ≝
178 match b with [ O ⇒ x0 | S b ⇒
179 match b with [ O ⇒ x1 | S b ⇒
180 match b with [ O ⇒ x2 | S b ⇒
181 match b with [ O ⇒ x3 | S b ⇒
182 match b with [ O ⇒ x4 | S b ⇒
183 match b with [ O ⇒ x5 | S b ⇒
184 match b with [ O ⇒ x6 | S b ⇒
185 match b with [ O ⇒ x7 | S b ⇒
186 match b with [ O ⇒ x8 | S b ⇒
187 match b with [ O ⇒ x9 | S b ⇒
188 match b with [ O ⇒ xA | S b ⇒
189 match b with [ O ⇒ xB | S b ⇒
190 match b with [ O ⇒ xC | S b ⇒
191 match b with [ O ⇒ xD | S b ⇒
192 match b with [ O ⇒ xE | S b ⇒
193 match b with [ O ⇒ xF | S b ⇒ x0]]]]]]]]]]]]]]]].
195 definition byte_of_nat ≝
196 λn. mk_byte (exadecimal_of_nat ((n / 16) \mod 16)) (exadecimal_of_nat (n \mod 16)).
198 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
206 lemma sign_ok: byte_of_nat 257 = mk_byte x0 x1.
210 definition addr ≝ nat.
234 match eqex (bl b) x0 with
235 [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
236 | false ⇒ mk_byte (bh b) (xpred (bl b))
242 match eqbyte b (mk_byte x0 x0) with
243 [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
244 | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
254 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
256 coercion cic:/matita/assembly/addr_of_byte.con.
258 inductive opcode: Type ≝
259 ADDd: opcode (* 3 clock, 171 *)
260 | BEQ: opcode (* 3, 55 *)
261 | BRA: opcode (* 3, 48 *)
262 | DECd: opcode (* 5, 58 *)
263 | LDAi: opcode (* 2, 166 *)
264 | LDAd: opcode (* 3, 182 *)
265 | STAd: opcode. (* 3, 183 *)
267 let rec cycles_of_opcode op : nat ≝
278 inductive cartesian_product (A,B: Type) : Type ≝
279 couple: ∀a:A.∀b:B. cartesian_product A B.
281 definition opcodemap ≝
282 [ couple ? ? ADDd (mk_byte xA xB);
283 couple ? ? BEQ (mk_byte x3 x7);
284 couple ? ? BRA (mk_byte x3 x0);
285 couple ? ? DECd (mk_byte x3 xA);
286 couple ? ? LDAi (mk_byte xA x6);
287 couple ? ? LDAd (mk_byte xB x6);
288 couple ? ? STAd (mk_byte xB x7) ].
290 definition opcode_of_byte ≝
298 match eqbyte n b with
305 definition magic_of_opcode ≝
316 definition opcodeeqb ≝
317 λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
319 definition byte_of_opcode : opcode → byte ≝
323 [ nil ⇒ mk_byte x0 x0
327 match opcodeeqb op op' with
334 notation "hvbox(# break a)"
335 non associative with precedence 80
336 for @{ 'byte_of_opcode $a }.
337 interpretation "byte_of_opcode" 'byte_of_opcode a =
338 (cic:/matita/assembly/byte_of_opcode.con a).
340 definition mult_source : list byte ≝
341 [#LDAi; mk_byte x0 x0;
342 #STAd; mk_byte x2 x0; (* 18 = locazione $12 *)
343 #LDAd; mk_byte x1 xF; (* 17 = locazione $11 *)
345 #LDAd; mk_byte x1 x2;
346 #DECd; mk_byte x1 xF;
347 #ADDd; mk_byte x1 xE; (* 16 = locazione $10 *)
348 #STAd; mk_byte x2 x0;
349 #LDAd; mk_byte x1 xF;
350 #BRA; mk_byte xF x2; (* 242 = -14 *)
351 #LDAd; mk_byte x2 x0].
353 record status : Type ≝ {
363 definition mult_status : status ≝
364 mk_status (mk_byte x0 x0) 0 0 false false
365 (λa:addr. nth ? mult_source (mk_byte x0 x0) a) 0.
368 λf: addr → byte.λa.λv.λx.
376 let opc ≝ opcode_of_byte (mem s (pc s)) in
377 let op1 ≝ mem s (S (pc s)) in
378 let clk' ≝ cycles_of_opcode opc in
379 match eqb (S (clk s)) clk' with
383 let x ≝ nat_of_byte (mem s op1) in
384 let acc' ≝ x + acc s in (* signed!!! *)
385 mk_status (byte_of_nat acc') (2 + pc s) (spc s)
386 (eqb O acc') (cf s) (mem s) 0
391 [ true ⇒ 2 + op1 + pc s (* signed!!! *)
401 (acc s) (2 + op1 + pc s) (* signed!!! *)
408 let x ≝ bpred (mem s op1) in (* signed!!! *)
409 let mem' ≝ update (mem s) op1 x in
410 mk_status (acc s) (2 + pc s) (spc s)
411 (eqb O x) (cf s) mem' 0 (* check zb!!! *)
413 mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
415 let x ≝ bpred (mem s op1) in
416 mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
418 mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
419 (update (mem s) op1 (acc s)) 0
423 (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
426 let rec execute s n on n ≝
429 | S n' ⇒ execute (tick s) n'
432 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
437 letin s0 ≝ mult_status;
441 letin i0 ≝ (opcode_of_byte (mem s0 pc0));
444 letin s1 ≝ (execute s0 (cycles_of_opcode i0));
447 letin i1 ≝ (opcode_of_byte (mem s1 pc1));
450 letin s2 ≝ (execute s1 (cycles_of_opcode i1));
453 letin i2 ≝ (opcode_of_byte (mem s2 pc2));
456 letin s3 ≝ (execute s2 (cycles_of_opcode i2));
459 letin i3 ≝ (opcode_of_byte (mem s3 pc3));
462 letin s4 ≝ (execute s3 (cycles_of_opcode i3));
465 letin i4 ≝ (opcode_of_byte (mem s4 pc4));