]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/assembly/assembly.ma
6cdf4091569624430db6be1bac1ca849c622892d
[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 definition tick ≝
154  λs:status.
155   (* fetch *)
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
161    [ false ⇒
162        mk_status
163         (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
164    | true ⇒
165       match opc with
166        [ ADDd ⇒ s
167        | BEQ ⇒
168           mk_status
169            (acc s)
170            (match zf s with
171              [ true ⇒ op1 + pc s   (* signed!!! *)
172              | false ⇒ 2 + pc s
173              ])
174            (spc s)
175            (zf s)
176            (cf s)
177            (mem s)
178            0
179        | BRA ⇒ s
180        | DECd ⇒ s
181        | LDAi ⇒ s
182        | LDAd ⇒ s
183        | STAd ⇒ s
184        ]
185    ].
186
187 let rec execute s n on n ≝
188  match n with
189   [ O ⇒ s
190   | S n' ⇒ execute (tick s) n'
191   ].
192   
193 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
194  intros; reflexivity.
195 qed.
196
197 lemma goo: execute mult_status (matita_nat_of_coq_nat 4) = mult_status.
198  simplify;
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);
203  reflexivity.
204 qed.
205
206 (*
207  unfold mult_status; 
208  simplify;
209  whd in ⊢ (? ?
210 (?
211  (?
212   (?
213    match match ? % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ?
214     with 
215    [true\rArr ?|false\rArr ?]))) ?);
216  simplify;
217  whd in ⊢ (? ?
218 (?
219  (?
220   (?
221    match % in opcode return ? with 
222    [ADDd\rArr ?
223    |BEQ\rArr ?
224    |BRA\rArr ?
225    |DECd\rArr ?
226    |LDAi\rArr ?
227    |LDAd\rArr ?
228    |STAd\rArr ?]))) ?);
229  simplify;
230  whd in \vdash (? ?
231 (?
232  (?
233   match match % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ? with 
234   [true\rArr ?|false\rArr ?])) ?);
235  simplify;
236  whd in \vdash (? ?
237 (?
238  (?
239   match % in opcode return ? with 
240   [ADDd\rArr ?
241   |BEQ\rArr ?
242   |BRA\rArr ?
243   |DECd\rArr ?
244   |LDAi\rArr ?
245   |LDAd\rArr ?
246   |STAd\rArr ?])) ?);
247  simplify;
248  whd in \vdash (? ? (? match % in bool return ? with [true\rArr ?|false\rArr ?]) ?);
249  simplify;
250  whd in \vdash (? ?
251 (?
252  match % in opcode return ? with 
253  [ADDd\rArr ?
254  |BEQ\rArr ?
255  |BRA\rArr ?
256  |DECd\rArr ?
257  |LDAi\rArr ?
258  |LDAd\rArr ?
259  |STAd\rArr ?]) ?);
260  simplify;
261  whd in \vdash (? ? match % in bool return ? with [true\rArr ?|false\rArr ?] ?);
262  simplify;
263  whd in \vdash (? ?
264 match % in opcode return ? with 
265 [ADDd\rArr ?
266 |BEQ\rArr ?
267 |BRA\rArr ?
268 |DECd\rArr ?
269 |LDAi\rArr ?
270 |LDAd\rArr ?
271 |STAd\rArr ?] ?);
272  simplify;
273  reflexivity.
274 *)