]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/assembly/assembly.ma
More opcodes (badly) implemented.
[helm.git] / 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 *)