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 alias num (instance 0) = "natural number".
45 let rec cycles_of_opcode op : nat ≝
56 inductive cartesian_product (A,B: Type) : Type ≝
57 couple: ∀a:A.∀b:B. cartesian_product A B.
59 definition opcodemap ≝
60 [ couple ? ? ADDd 171;
66 couple ? ? STAd 183 ].
68 definition opcode_of_byte ≝
83 definition magic_of_opcode ≝
94 definition opcodeeqb ≝
95 λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
97 definition byte_of_opcode : opcode → byte ≝
105 match opcodeeqb op op' with
112 notation "hvbox(# break a)"
113 non associative with precedence 80
114 for @{ 'byte_of_opcode $a }.
115 interpretation "byte_of_opcode" 'byte_of_opcode a =
116 (cic:/matita/assembly/byte_of_opcode.con a).
118 definition mult_source : list byte ≝
120 #STAd; 32; (* 18 = locazione $12 *)
121 #LDAd; 31; (* 17 = locazione $11 *)
125 #ADDd; 30; (* 16 = locazione $10 *)
128 #BRA; 246; (* 242 = -14 *)
131 definition mult_source' : list byte.
133 record status : Type ≝ {
143 definition mult_status : status ≝
144 mk_status 0 0 0 false false (λa:addr. nth ? mult_source 0 a) 0.
147 λf: addr → byte.λa.λv.λx.
155 let opc ≝ opcode_of_byte (mem s (pc s)) in
156 let op1 ≝ mem s (S (pc s)) in
157 let clk' ≝ cycles_of_opcode opc in
158 match eqb (S (clk s)) clk' with
163 let acc' ≝ x + acc s in (* signed!!! *)
164 mk_status acc' (2 + pc s) (spc s)
165 (eqb O acc') (cf s) (mem s) 0
170 [ true ⇒ 2 + op1 + pc s (* signed!!! *)
180 (acc s) (2 + op1 + pc s) (* signed!!! *)
187 let x ≝ pred (mem s op1) in (* signed!!! *)
188 let mem' ≝ update (mem s) op1 x in
189 mk_status (acc s) (2 + pc s) (spc s)
190 (eqb O x) (cf s) mem' 0 (* check zb!!! *)
192 mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
194 let x ≝ pred (mem s op1) in
195 mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
197 mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
198 (update (mem s) op1 (acc s)) 0
202 (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
205 let rec execute s n on n ≝
208 | S n' ⇒ execute (tick s) n'
211 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
216 letin s0 ≝ mult_status;
220 letin i0 ≝ (opcode_of_byte (mem s0 pc0));
223 letin s1 ≝ (execute s0 (cycles_of_opcode i0));
226 letin i1 ≝ (opcode_of_byte (mem s1 pc1));
229 letin s2 ≝ (execute s1 (cycles_of_opcode i1));
232 letin i2 ≝ (opcode_of_byte (mem s2 pc2));
235 letin s3 ≝ (execute s2 (cycles_of_opcode i2));
238 letin i3 ≝ (opcode_of_byte (mem s3 pc3));
241 letin s4 ≝ (execute s3 (cycles_of_opcode i3));
244 letin i4 ≝ (opcode_of_byte (mem s4 pc4));