source: src/ASM/Assembly.ma @ 828

Last change on this file since 828 was 825, checked in by mulligan, 10 years ago

lots of refactoring, finally got something to prove
File size: 26.4 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/BitVectorTrie.ma".
3include "ASM/Arithmetic.ma".
4include "ASM/Fetch.ma".
5include "ASM/Status.ma".
6
7definition assembly_preinstruction ≝
8  λA: Type[0].
9  λaddr_of: A → Byte. (* relative *)
10  λpre: preinstruction A.
11  match pre with
12  [ ADD addr1 addr2 ⇒
13     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
14      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
15      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
16      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
17      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
18      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
19  | ADDC addr1 addr2 ⇒
20     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
21      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
22      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
23      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
24      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
25      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
26  | ANL addrs ⇒
27     match addrs with
28      [ inl addrs ⇒ match addrs with
29         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
30           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
31            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
32            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
33            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
34            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
35            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
36         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
37            let b1 ≝
38             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
39              [ DIRECT b1 ⇒ λ_.b1
40              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
41            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
42             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
43             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
44             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
45         ]
46      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
47         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
48          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
49          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
50          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
51  | CLR addr ⇒
52     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
53      [ ACC_A ⇒ λ_.
54         [ ([[true; true; true; false; false; true; false; false]]) ]
55      | CARRY ⇒ λ_.
56         [ ([[true; true; false; false; false; false; true; true]]) ]
57      | BIT_ADDR b1 ⇒ λ_.
58         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
59      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
60  | CPL addr ⇒
61     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
62      [ ACC_A ⇒ λ_.
63         [ ([[true; true; true; true; false; true; false; false]]) ]
64      | CARRY ⇒ λ_.
65         [ ([[true; false; true; true; false; false; true; true]]) ]
66      | BIT_ADDR b1 ⇒ λ_.
67         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
68      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
69  | DA addr ⇒
70     [ ([[true; true; false; true; false; true; false; false]]) ]
71  | DEC addr ⇒
72     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
73      [ ACC_A ⇒ λ_.
74         [ ([[false; false; false; true; false; true; false; false]]) ]
75      | REGISTER r ⇒ λ_.
76         [ ([[false; false; false; true; true]]) @@ r ]
77      | DIRECT b1 ⇒ λ_.
78         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
79      | INDIRECT i1 ⇒ λ_.
80         [ ([[false; false; false; true; false; true; true; i1]]) ]
81      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
82      | DJNZ addr1 addr2 ⇒
83         let b2 ≝ addr_of addr2 in
84         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
85          [ REGISTER r ⇒ λ_.
86             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
87          | DIRECT b1 ⇒ λ_.
88             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
89          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
90      | JC addr ⇒
91        let b1 ≝ addr_of addr in
92          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
93      | JNC addr ⇒
94         let b1 ≝ addr_of addr in
95           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
96      | JZ addr ⇒
97         let b1 ≝ addr_of addr in
98           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
99      | JNZ addr ⇒
100         let b1 ≝ addr_of addr in
101           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
102      | JB addr1 addr2 ⇒
103         let b2 ≝ addr_of addr2 in
104         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
105          [ BIT_ADDR b1 ⇒ λ_.
106             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
107          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
108      | JNB addr1 addr2 ⇒
109         let b2 ≝ addr_of addr2 in
110         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
111          [ BIT_ADDR b1 ⇒ λ_.
112             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
113          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
114      | JBC addr1 addr2 ⇒
115         let b2 ≝ addr_of addr2 in
116         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
117          [ BIT_ADDR b1 ⇒ λ_.
118             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
119          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
120      | CJNE addrs addr3 ⇒
121         let b3 ≝ addr_of addr3 in
122         match addrs with
123          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
124             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
125              [ DIRECT b1 ⇒ λ_.
126                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
127              | DATA b1 ⇒ λ_.
128                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
129              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
130          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
131             let b2 ≝
132              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
133               [ DATA b2 ⇒ λ_. b2
134               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
135             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
136              [ REGISTER r ⇒ λ_.
137                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
138              | INDIRECT i1 ⇒ λ_.
139                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
140              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
141         ]
142  | DIV addr1 addr2 ⇒
143     [ ([[true;false;false;false;false;true;false;false]]) ]
144  | INC addr ⇒
145     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
146      [ ACC_A ⇒ λ_.
147         [ ([[false;false;false;false;false;true;false;false]]) ]         
148      | REGISTER r ⇒ λ_.
149         [ ([[false;false;false;false;true]]) @@ r ]
150      | DIRECT b1 ⇒ λ_.
151         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
152      | INDIRECT i1 ⇒ λ_.
153        [ ([[false; false; false; false; false; true; true; i1]]) ]
154      | DPTR ⇒ λ_.
155        [ ([[true;false;true;false;false;false;true;true]]) ]
156      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
157  | MOV addrs ⇒
158     match addrs with
159      [ inl addrs ⇒
160         match addrs with
161          [ inl addrs ⇒
162             match addrs with
163              [ inl addrs ⇒
164                 match addrs with
165                  [ inl addrs ⇒
166                     match addrs with
167                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
168                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
169                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
170                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
171                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
172                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
173                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
174                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
175                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
176                          [ REGISTER r ⇒ λ_.
177                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
178                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
179                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
180                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
181                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
182                          | INDIRECT i1 ⇒ λ_.
183                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
184                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
185                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
186                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
187                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
188                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
189                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
190                     let b1 ≝
191                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
192                       [ DIRECT b1 ⇒ λ_. b1
193                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
194                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
195                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
196                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
197                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
198                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
199                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
200                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
201              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
202                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
203                  [ DATA16 w ⇒ λ_.
204                     let 〈b1,b2〉 ≝ split ? 8 8 w in
205                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
206                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
207          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
208             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
209              [ BIT_ADDR b1 ⇒ λ_.
210                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
211              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
212      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
213         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
214          [ BIT_ADDR b1 ⇒ λ_.
215             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
216          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
217  | MOVX addrs ⇒
218     match addrs with
219      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
220         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
221          [ EXT_INDIRECT i1 ⇒ λ_.
222             [ ([[true;true;true;false;false;false;true;i1]]) ]
223          | EXT_INDIRECT_DPTR ⇒ λ_.
224             [ ([[true;true;true;false;false;false;false;false]]) ]
225          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
226      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
227         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
228          [ EXT_INDIRECT i1 ⇒ λ_.
229             [ ([[true;true;true;true;false;false;true;i1]]) ]
230          | EXT_INDIRECT_DPTR ⇒ λ_.
231             [ ([[true;true;true;true;false;false;false;false]]) ]
232          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
233  | MUL addr1 addr2 ⇒
234     [ ([[true;false;true;false;false;true;false;false]]) ]
235  | NOP ⇒
236     [ ([[false;false;false;false;false;false;false;false]]) ]
237  | ORL addrs ⇒
238     match addrs with
239      [ inl addrs ⇒
240         match addrs with
241          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
242             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
243             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
244             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
245             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
246             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
247             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
248          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
249            let b1 ≝
250              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
251               [ DIRECT b1 ⇒ λ_. b1
252               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
253             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
254              [ ACC_A ⇒ λ_.
255                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
256              | DATA b2 ⇒ λ_.
257                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
258              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
259      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
260         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
261          [ BIT_ADDR b1 ⇒ λ_.
262             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
263          | N_BIT_ADDR b1 ⇒ λ_.
264             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
265          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
266  | POP addr ⇒
267     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
268      [ DIRECT b1 ⇒ λ_.
269         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
270      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
271  | PUSH addr ⇒
272     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
273      [ DIRECT b1 ⇒ λ_.
274         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
275      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
276  | RET ⇒
277     [ ([[false;false;true;false;false;false;true;false]]) ]
278  | RETI ⇒
279     [ ([[false;false;true;true;false;false;true;false]]) ]
280  | RL addr ⇒
281     [ ([[false;false;true;false;false;false;true;true]]) ]
282  | RLC addr ⇒
283     [ ([[false;false;true;true;false;false;true;true]]) ]
284  | RR addr ⇒
285     [ ([[false;false;false;false;false;false;true;true]]) ]
286  | RRC addr ⇒
287     [ ([[false;false;false;true;false;false;true;true]]) ]
288  | SETB addr ⇒     
289     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
290      [ CARRY ⇒ λ_.
291         [ ([[true;true;false;true;false;false;true;true]]) ]
292      | BIT_ADDR b1 ⇒ λ_.
293         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
294      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
295  | SUBB addr1 addr2 ⇒
296     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
297      [ REGISTER r ⇒ λ_.
298         [ ([[true;false;false;true;true]]) @@ r ]
299      | DIRECT b1 ⇒ λ_.
300         [ ([[true;false;false;true;false;true;false;true]]); b1]
301      | INDIRECT i1 ⇒ λ_.
302         [ ([[true;false;false;true;false;true;true;i1]]) ]
303      | DATA b1 ⇒ λ_.
304         [ ([[true;false;false;true;false;true;false;false]]); b1]
305      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
306  | SWAP addr ⇒
307     [ ([[true;true;false;false;false;true;false;false]]) ]
308  | XCH addr1 addr2 ⇒
309     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
310      [ REGISTER r ⇒ λ_.
311         [ ([[true;true;false;false;true]]) @@ r ]
312      | DIRECT b1 ⇒ λ_.
313         [ ([[true;true;false;false;false;true;false;true]]); b1]
314      | INDIRECT i1 ⇒ λ_.
315         [ ([[true;true;false;false;false;true;true;i1]]) ]
316      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
317  | XCHD addr1 addr2 ⇒
318     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
319      [ INDIRECT i1 ⇒ λ_.
320         [ ([[true;true;false;true;false;true;true;i1]]) ]
321      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
322  | XRL addrs ⇒
323     match addrs with
324      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
325         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
326          [ REGISTER r ⇒ λ_.
327             [ ([[false;true;true;false;true]]) @@ r ]
328          | DIRECT b1 ⇒ λ_.
329             [ ([[false;true;true;false;false;true;false;true]]); b1]
330          | INDIRECT i1 ⇒ λ_.
331             [ ([[false;true;true;false;false;true;true;i1]]) ]
332          | DATA b1 ⇒ λ_.
333             [ ([[false;true;true;false;false;true;false;false]]); b1]
334          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
335      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
336         let b1 ≝
337          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
338           [ DIRECT b1 ⇒ λ_. b1
339           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
340         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
341          [ ACC_A ⇒ λ_.
342             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
343          | DATA b2 ⇒ λ_.
344             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
345          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
346       ].
347
348definition assembly1 ≝
349 λi: instruction.
350 match i with
351  [ ACALL addr ⇒
352     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
353      [ ADDR11 w ⇒ λ_.
354         let 〈v1,v2〉 ≝ split ? 3 8 w in
355          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
356      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
357  | AJMP addr ⇒
358     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
359      [ ADDR11 w ⇒ λ_.
360         let 〈v1,v2〉 ≝ split ?  3 8 w in
361          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
362      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
363  | JMP adptr ⇒
364     [ ([[false;true;true;true;false;false;true;true]]) ]
365  | LCALL addr ⇒
366     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
367      [ ADDR16 w ⇒ λ_.
368         let 〈b1,b2〉 ≝ split ? 8 8 w in
369          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
370      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
371  | LJMP addr ⇒
372     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
373      [ ADDR16 w ⇒ λ_.
374         let 〈b1,b2〉 ≝ split ? 8 8 w in
375          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
376      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
377  | MOVC addr1 addr2 ⇒
378     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
379      [ ACC_DPTR ⇒ λ_.
380         [ ([[true;false;false;true;false;false;true;true]]) ]
381      | ACC_PC ⇒ λ_.
382         [ ([[true;false;false;false;false;false;true;true]]) ]
383      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
384  | SJMP addr ⇒
385     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
386      [ RELATIVE b1 ⇒ λ_.
387         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
388      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
389  | RealInstruction instr ⇒
390    assembly_preinstruction [[ relative ]]
391      (λx.
392        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
393        [ RELATIVE r ⇒ λ_. r
394        | _ ⇒ λabsd. ⊥
395        ] (subaddressing_modein … x)) instr
396  ].
397  cases absd
398qed.
399
400definition address_of: BitVectorTrie Word 16 → Identifier → Byte ≝
401    λmap.
402    λid: Identifier.
403      let address ≝ lookup … id map (zero ?) in
404      let 〈high, low〉 ≝ split ? 8 8 address in
405      if eq_bv ? high (zero ?) then
406        low
407      else
408        ?.
409      elim not_implemented.
410qed.
411
412definition assembly_expansion ≝
413  λi.
414  λcosts: BitVectorTrie Identifier 16.
415  λprogram_counter: nat.
416            match i with
417              [ Instruction instr ⇒
418                let code_memory ≝ load_code_memory (assembly_preinstruction Identifier (λx. zero 8) instr) in
419                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
420                let 〈instr', program_counter'〉 ≝ instr_pc' in
421                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
422                  〈program_counter + program_counter_n', costs〉
423              | Comment comment ⇒ 〈program_counter, costs〉
424              | Cost cost ⇒
425                let program_counter_bv ≝ bitvector_of_nat ? program_counter in
426                  〈program_counter, (insert ? ? program_counter_bv cost costs)〉
427              | Jmp jmp ⇒
428                  〈program_counter + 3, costs〉
429              | Call call ⇒
430                  〈program_counter + 3, costs〉
431              | Mov dptr trgt ⇒ 〈program_counter, costs〉
432              ].
433
434definition assembly_1_pseudoinstruction ≝
435  λlookup_labels.
436  λlookup_datalabels.
437  λaddress_of.
438  λi: labelled_instruction.
439                match \snd i with
440                  [ Cost cost ⇒ [ ]
441                  | Comment comment ⇒ [ ]
442                  | Call call ⇒
443                    let address ≝ ADDR16 (lookup_labels call) in
444                      assembly1 (LCALL address)
445                  | Mov d trgt ⇒
446                    let address ≝ DATA16 (lookup_datalabels trgt) in
447                      assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
448                  | Instruction instr ⇒ assembly_preinstruction ? address_of instr
449                  | Jmp jmp ⇒
450                    let address ≝ ADDR16 (lookup_labels jmp) in
451                      assembly1 (LJMP address)
452(*                  | WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels))
453*)
454                  ].
455  @ I
456qed.
457
458definition construct_datalabels ≝
459  λpreamble.
460    \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
461    λt. λpreamble.
462      let 〈datalabels, addr〉 ≝ t in
463      let 〈name, size〉 ≝ preamble in
464      let addr_16 ≝ bitvector_of_nat 16 addr in
465        〈insert ? ? name addr_16 datalabels, addr + size〉)
466          〈(Stub ? ?), 0〉 preamble).
467
468definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
469  λp.
470    let 〈preamble, instr_list〉 ≝ p in
471    let datalabels ≝ construct_datalabels preamble in
472    let 〈labels,pc_costs〉 ≝
473      foldl ((BitVectorTrie ? ?) × (nat  × (BitVectorTrie ? ?))) ? (
474        λt. λi.
475          let 〈label, i〉 ≝ i in
476          let 〈labels, pc_costs〉 ≝ t in
477          let 〈program_counter, costs〉 ≝ pc_costs in
478          let labels ≝ match label with
479          [ None ⇒ labels
480          | Some label ⇒
481            let program_counter_bv ≝ bitvector_of_nat ? program_counter in
482              insert ? ? label program_counter_bv labels
483          ] in
484          〈labels, assembly_expansion i costs program_counter〉
485          ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in
486    let 〈program_counter, costs〉 ≝ pc_costs in
487      if gtb program_counter (2^16) then (* 65536 *)
488        None ?
489      else
490        let flat_list ≝ flatten ? (
491          map ? ? (
492            assembly_1_pseudoinstruction (
493              λx. lookup ? ? x labels (zero ?))
494                (λx. lookup ? ? x datalabels (zero ?))
495                (address_of labels)) instr_list) in
496        Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
497(*
498  [2,3,4,5,6:
499    normalize; %;
500  | whd in ⊢ (? (? ? ? %));
501      cases (split bool 8 8 (lookup Word 16 trgt labels (zero 16)))
502      # high
503      # low
504      whd in ⊢ (? (? ? ? %))
505      cases (eq_bv 8 high (zero 8))
506      [ normalize
507        %
508      | elim not_implemented;
509      ]
510  ]
511qed. *)
512
513definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
514 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
515
Note: See TracBrowser for help on using the repository browser.