source: src/ASM/Assembly.ma @ 1363

Last change on this file since 1363 was 1363, checked in by boender, 8 years ago
  • done stuff with create_label_trie
File size: 54.9 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                     let b1 ≝ \fst b1_b2 in
206                     let b2 ≝ \snd b1_b2 in
207                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
208                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
209          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
210             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
211              [ BIT_ADDR b1 ⇒ λ_.
212                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
213              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
214      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
215         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
216          [ BIT_ADDR b1 ⇒ λ_.
217             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
218          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
219  | MOVX addrs ⇒
220     match addrs with
221      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
222         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
223          [ EXT_INDIRECT i1 ⇒ λ_.
224             [ ([[true;true;true;false;false;false;true;i1]]) ]
225          | EXT_INDIRECT_DPTR ⇒ λ_.
226             [ ([[true;true;true;false;false;false;false;false]]) ]
227          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
228      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
229         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
230          [ EXT_INDIRECT i1 ⇒ λ_.
231             [ ([[true;true;true;true;false;false;true;i1]]) ]
232          | EXT_INDIRECT_DPTR ⇒ λ_.
233             [ ([[true;true;true;true;false;false;false;false]]) ]
234          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
235  | MUL addr1 addr2 ⇒
236     [ ([[true;false;true;false;false;true;false;false]]) ]
237  | NOP ⇒
238     [ ([[false;false;false;false;false;false;false;false]]) ]
239  | ORL addrs ⇒
240     match addrs with
241      [ inl addrs ⇒
242         match addrs with
243          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
244             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
245             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
246             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
247             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
248             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
249             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
250          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
251            let b1 ≝
252              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
253               [ DIRECT b1 ⇒ λ_. b1
254               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
255             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
256              [ ACC_A ⇒ λ_.
257                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
258              | DATA b2 ⇒ λ_.
259                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
260              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
261      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
262         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
263          [ BIT_ADDR b1 ⇒ λ_.
264             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
265          | N_BIT_ADDR b1 ⇒ λ_.
266             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
267          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
268  | POP addr ⇒
269     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
270      [ DIRECT b1 ⇒ λ_.
271         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
272      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
273  | PUSH addr ⇒
274     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
275      [ DIRECT b1 ⇒ λ_.
276         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
277      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
278  | RET ⇒
279     [ ([[false;false;true;false;false;false;true;false]]) ]
280  | RETI ⇒
281     [ ([[false;false;true;true;false;false;true;false]]) ]
282  | RL addr ⇒
283     [ ([[false;false;true;false;false;false;true;true]]) ]
284  | RLC addr ⇒
285     [ ([[false;false;true;true;false;false;true;true]]) ]
286  | RR addr ⇒
287     [ ([[false;false;false;false;false;false;true;true]]) ]
288  | RRC addr ⇒
289     [ ([[false;false;false;true;false;false;true;true]]) ]
290  | SETB addr ⇒     
291     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
292      [ CARRY ⇒ λ_.
293         [ ([[true;true;false;true;false;false;true;true]]) ]
294      | BIT_ADDR b1 ⇒ λ_.
295         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
296      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
297  | SUBB addr1 addr2 ⇒
298     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
299      [ REGISTER r ⇒ λ_.
300         [ ([[true;false;false;true;true]]) @@ r ]
301      | DIRECT b1 ⇒ λ_.
302         [ ([[true;false;false;true;false;true;false;true]]); b1]
303      | INDIRECT i1 ⇒ λ_.
304         [ ([[true;false;false;true;false;true;true;i1]]) ]
305      | DATA b1 ⇒ λ_.
306         [ ([[true;false;false;true;false;true;false;false]]); b1]
307      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
308  | SWAP addr ⇒
309     [ ([[true;true;false;false;false;true;false;false]]) ]
310  | XCH addr1 addr2 ⇒
311     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
312      [ REGISTER r ⇒ λ_.
313         [ ([[true;true;false;false;true]]) @@ r ]
314      | DIRECT b1 ⇒ λ_.
315         [ ([[true;true;false;false;false;true;false;true]]); b1]
316      | INDIRECT i1 ⇒ λ_.
317         [ ([[true;true;false;false;false;true;true;i1]]) ]
318      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
319  | XCHD addr1 addr2 ⇒
320     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
321      [ INDIRECT i1 ⇒ λ_.
322         [ ([[true;true;false;true;false;true;true;i1]]) ]
323      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
324  | XRL addrs ⇒
325     match addrs with
326      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
327         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
328          [ REGISTER r ⇒ λ_.
329             [ ([[false;true;true;false;true]]) @@ r ]
330          | DIRECT b1 ⇒ λ_.
331             [ ([[false;true;true;false;false;true;false;true]]); b1]
332          | INDIRECT i1 ⇒ λ_.
333             [ ([[false;true;true;false;false;true;true;i1]]) ]
334          | DATA b1 ⇒ λ_.
335             [ ([[false;true;true;false;false;true;false;false]]); b1]
336          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
337      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
338         let b1 ≝
339          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
340           [ DIRECT b1 ⇒ λ_. b1
341           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
342         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
343          [ ACC_A ⇒ λ_.
344             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
345          | DATA b2 ⇒ λ_.
346             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
347          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
348       ].
349
350definition assembly1 ≝
351 λi: instruction.
352 match i with
353  [ ACALL addr ⇒
354     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
355      [ ADDR11 w ⇒ λ_.
356         let v1_v2 ≝ split ? 3 8 w in
357         let v1 ≝ \fst v1_v2 in
358         let v2 ≝ \snd v1_v2 in
359          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
360      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
361  | AJMP addr ⇒
362     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
363      [ ADDR11 w ⇒ λ_.
364         let v1_v2 ≝ split ? 3 8 w in
365         let v1 ≝ \fst v1_v2 in
366         let v2 ≝ \snd v1_v2 in
367          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
368      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
369  | JMP adptr ⇒
370     [ ([[false;true;true;true;false;false;true;true]]) ]
371  | LCALL 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         let b1 ≝ \fst b1_b2 in
376         let b2 ≝ \snd b1_b2 in
377          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
378      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
379  | LJMP addr ⇒
380     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
381      [ ADDR16 w ⇒ λ_.
382         let b1_b2 ≝ split ? 8 8 w in
383         let b1 ≝ \fst b1_b2 in
384         let b2 ≝ \snd b1_b2 in
385          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
386      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
387  | MOVC addr1 addr2 ⇒
388     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
389      [ ACC_DPTR ⇒ λ_.
390         [ ([[true;false;false;true;false;false;true;true]]) ]
391      | ACC_PC ⇒ λ_.
392         [ ([[true;false;false;false;false;false;true;true]]) ]
393      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
394  | SJMP addr ⇒
395     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
396      [ RELATIVE b1 ⇒ λ_.
397         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
398      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
399  | RealInstruction instr ⇒
400    assembly_preinstruction [[ relative ]]
401      (λx.
402        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
403        [ RELATIVE r ⇒ λ_. r
404        | _ ⇒ λabsd. ⊥
405        ] (subaddressing_modein … x)) instr
406  ].
407  cases absd
408qed.
409
410inductive jump_length: Type[0] ≝
411  | short_jump: jump_length
412  | medium_jump: jump_length
413  | long_jump: jump_length.
414
415(* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
416definition jump_expansion_policy ≝ BitVectorTrie (Word × jump_length) 16.
417
418definition expand_relative_jump_internal:
419 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
420 option (list instruction)
421 ≝
422  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
423  match jmp_len with
424  [ short_jump ⇒
425     let lookup_address ≝ lookup_labels jmp in
426     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
427     let 〈upper, lower〉 ≝ split ? 8 8 result in
428     if eq_bv ? upper (zero 8) then
429      let address ≝ RELATIVE lower in
430       Some ? [ RealInstruction (i address) ]
431     else
432       None ?
433  | medium_jump ⇒ None …
434  | long_jump ⇒
435    Some ?
436    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
437      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
438      LJMP (ADDR16 (lookup_labels jmp))
439    ]
440  ].
441  @ I
442qed.
443
444definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
445  λlookup_labels.
446  λjmp_len: jump_length.
447  λpc.
448  λi: preinstruction Identifier.
449  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
450  match i with
451  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
452  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
453  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
454  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
455  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
456  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
457  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
458  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
459  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
460  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
461  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
462  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
463  | INC arg ⇒ Some ? [ INC ? arg ]
464  | DEC arg ⇒ Some ? [ DEC ? arg ]
465  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
466  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
467  | DA arg ⇒ Some ? [ DA ? arg ]
468  | ANL arg ⇒ Some ? [ ANL ? arg ]
469  | ORL arg ⇒ Some ? [ ORL ? arg ]
470  | XRL arg ⇒ Some ? [ XRL ? arg ]
471  | CLR arg ⇒ Some ? [ CLR ? arg ]
472  | CPL arg ⇒ Some ? [ CPL ? arg ]
473  | RL arg ⇒ Some ? [ RL ? arg ]
474  | RR arg ⇒ Some ? [ RR ? arg ]
475  | RLC arg ⇒ Some ? [ RLC ? arg ]
476  | RRC arg ⇒ Some ? [ RRC ? arg ]
477  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
478  | MOV arg ⇒ Some ? [ MOV ? arg ]
479  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
480  | SETB arg ⇒ Some ? [ SETB ? arg ]
481  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
482  | POP arg ⇒ Some ? [ POP ? arg ]
483  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
484  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
485  | RET ⇒ Some ? [ RET ? ]
486  | RETI ⇒ Some ? [ RETI ? ]
487  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
488  ].
489
490definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
491  λlookup_labels.
492  λlookup_datalabels.
493  λpc.
494  λjmp_len.
495  λi.
496  match i with
497  [ Cost cost ⇒ Some ? [ ]
498  | Comment comment ⇒ Some ? [ ]
499  | Call call ⇒
500    match jmp_len with
501    [ short_jump ⇒ None ?
502    | medium_jump ⇒
503      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
504      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
505      if eq_bv ? ignore fst_5 then
506        let address ≝ ADDR11 address in
507          Some ? ([ ACALL address ])
508      else
509        None ?
510    | long_jump ⇒
511      let address ≝ ADDR16 (lookup_labels call) in
512        Some ? [ LCALL address ]
513    ]
514  | Mov d trgt ⇒
515    let address ≝ DATA16 (lookup_datalabels trgt) in
516      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
517  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
518  | Jmp jmp ⇒
519    match jmp_len with
520    [ short_jump ⇒
521      let lookup_address ≝ lookup_labels jmp in
522      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
523      let 〈upper, lower〉 ≝ split ? 8 8 result in
524      if eq_bv ? upper (zero 8) then
525        let address ≝ RELATIVE lower in
526          Some ? [ SJMP address ]
527      else
528        None ?
529    | medium_jump ⇒
530      let address ≝ lookup_labels jmp in
531      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
532      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
533      if eq_bv ? fst_5_addr fst_5_pc then
534        let address ≝ ADDR11 rest_addr in
535          Some ? ([ AJMP address ])
536      else
537        None ?
538    | long_jump ⇒
539      let address ≝ ADDR16 (lookup_labels jmp) in
540        Some ? [ LJMP address ]
541    ]
542  ].
543  @ I
544qed.
545
546(* label_trie: identifier ↦ 〈instruction number, address〉 *)
547definition label_trie ≝ BitVectorTrie (nat × Word) 16.
548
549definition add_instruction_size: Word → jump_length → pseudo_instruction → Word ≝
550  λpc.λjmp_len.λinstr.
551  let ilist ≝ expand_pseudo_instruction_safe (λx.pc) (λx.pc) pc jmp_len instr in
552  let bv: list (BitVector 8) ≝ match ilist with
553    [ None   ⇒ (* hmm, this shouldn't happen *) [ ]
554    | Some l ⇒ flatten … (map … assembly1 l)
555    ] in
556  let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (|bv|)) false in
557  new_pc.
558
559definition is_label ≝
560  λx:labelled_instruction.λl:Identifier.
561  let 〈lbl,instr〉 ≝ x in
562  match lbl with
563  [ Some l' ⇒ l' = l
564  | _       ⇒ False
565  ].
566 
567lemma oeo_Some_Stronger:
568  ∀id,id',i,prefix.
569    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
570    (eq_bv ? id' id ∧ does_not_occur id prefix) ∨
571    (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix).
572 #id #id' #i #prefix elim prefix
573 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?)
574  change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)
575  [ normalize //
576  | normalize #H @⊥ @H 
577  ]
578 | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
579   cases he; normalize nodelta
580   [ #H @ (IH H)
581   | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
582     generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id)
583     cases (eq_bv ???) in ⊢ (???% → %) #Heq
584     [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta
585       [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf
586       | #H >(does_not_occur_Some)
587         [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
588           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
589           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??)
590           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 
591         | @(sym_eq … H)
592         ]
593       ]
594     | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim
595       generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)
596       #Heq2
597       [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor;
598         whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
599         change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
600         cases (does_not_occur id tl) in Hor; normalize nodelta //
601       | normalize nodelta whd in match (occurs_exactly_once ??)
602         whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)
603         >Heq normalize nodelta <Heq2 in Hor; normalize //
604       ]
605     ] 
606   ]
607 ]
608qed.   
609
610lemma bla:
611  ∀i,p,l.
612  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
613 #i #p #l generalize in match i; elim p
614 [ #i >nth_nil #H @⊥ @H
615 | #h #t #IH #i cases i -i
616   [ cases h #hi #hp cases hi normalize
617     [ #H @⊥ @H
618     | #l' #Heq change in match (eq_v ??? l' l) with (eq_bv ? l' l)
619       >(eq_eq_bv … Heq) //
620     ]
621   | #i #H whd in match (does_not_occur ??)
622     whd in match (instruction_matches_identifier ??)
623     cases h #hi #hp cases hi normalize
624     [ @(IH i) @H
625     | #l' cases (eq_v ??? l' l)
626       [ normalize //
627       | normalize @(IH i) @H
628       ]
629     ]
630   ]
631 ]
632qed. 
633     
634definition create_label_trie: list labelled_instruction → jump_expansion_policy →
635  label_trie ≝
636  λprogram.λpolicy.
637  let 〈final_pc, final_labels〉 ≝
638    foldl_strong (option Identifier × pseudo_instruction)
639    (λprefix.Σres.
640      let 〈pc,labels〉 ≝ res in
641      ∀i:ℕ.i < |prefix| →
642      ∀l.occurs_exactly_once l prefix ->
643      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
644      ∃a.lookup_opt … l labels = Some ? 〈i,a〉
645    )
646    program
647    (λprefix.λx.λtl.λprf.λacc.
648     let 〈pc,labels〉 ≝ acc in
649     let 〈label,instr〉 ≝ x in
650     let new_labels ≝
651       match label with
652       [ None   ⇒ labels
653       | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
654       ] in
655     let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉 in
656     let new_pc ≝ add_instruction_size pc jmp_len instr in
657     〈new_pc, new_labels〉
658    ) 〈zero ?, Stub ? ?〉 in
659    final_labels.
660[ lapply (sig2 … acc) >p >p1 normalize nodelta #Hacc #i >append_length
661  <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
662  [ #Hi #l cases label
663    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
664      lapply (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #Ha elim Ha; -Ha; #addr #Haddr
665      % [ @addr | @Haddr ]
666    | #l' #Hocc #Hl lapply (oeo_Some_Stronger … Hocc) -Hocc; #Hocc
667      lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq
668      [ >Heq in Hocc; #Hocc normalize in Hocc;
669        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
670        @⊥ @(absurd … Hocc)
671      | >Heq in Hocc; normalize nodelta #Hocc lapply (Hacc i (le_S_S_to_le … Hi) l ? ?)
672        [ >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
673        | @Hocc
674        | #H elim H #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]   
675        ]
676      ]
677      >(bla i … Hl) normalize nodelta @nmk //
678    ]
679  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
680    [ <minus_n_n #Hl normalize in Hl; cases label in Hl;
681      [ normalize nodelta #H @⊥ @H
682      | #l' normalize nodelta #Heq % [ @pc | <Heq @lookup_opt_insert_hit ]
683      ]
684    | @le_n
685    ]
686  ]
687| #i #Hi #l #Hl @⊥ @Hl
688]
689qed.
690
691definition select_reljump_length: label_trie → Word → Identifier → jump_length ≝
692  λlabels.λpc.λlbl.
693  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
694  if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT pending lookup of right condition *)
695  then short_jump
696  else long_jump.
697
698definition select_call_length: label_trie → Word → Identifier → jump_length ≝
699  λlabels.λpc.λlbl.
700  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
701  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
702  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
703  if eq_bv ? fst_5_addr fst_5_pc
704  then medium_jump
705  else long_jump.
706 
707definition select_jump_length: label_trie → Word → Identifier → jump_length ≝
708  λlabels.λpc.λlbl.
709  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
710  if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT *)
711  then short_jump
712  else
713    let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
714    let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
715    let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
716    if eq_bv ? fst_5_addr fst_5_pc
717    then medium_jump
718    else long_jump.
719 
720definition jump_expansion_step_instruction: label_trie → Word →
721  preinstruction Identifier → option jump_length ≝
722  λlabels.λpc.λi.
723  match i with
724  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
725  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
726  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
727  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
728  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
729  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
730  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
731  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
732  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
733  | _        ⇒ None ?
734  ].
735
736definition max_length: jump_length → jump_length → jump_length ≝
737  λj1.λj2.
738  match j1 with
739  [ long_jump   ⇒ long_jump
740  | medium_jump ⇒
741    match j2 with
742    [ long_jump ⇒ long_jump
743    | _         ⇒ medium_jump
744    ]
745  | short_jump  ⇒ j2
746  ].
747     
748definition jump_expansion_step: list labelled_instruction →
749  jump_expansion_policy → jump_expansion_policy ≝
750  λprogram.λpolicy.
751  let labels ≝ create_label_trie program policy in
752  let 〈final_n, final_pc, final_policy〉 ≝
753    foldl_strong (option Identifier × pseudo_instruction)
754    (λprefix.Σres.True)
755    program
756    (λprefix.λx.λtl.λprf.λacc.
757      let 〈n, pc, policy〉 ≝ acc in
758      let 〈label,instr〉 ≝ x in
759      let old_jump_length ≝ lookup_opt … (bitvector_of_nat 16 n) policy in
760      let add_instr ≝
761        match instr with
762        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
763        | Call c        ⇒ Some ? (select_call_length labels pc c)
764        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
765        | _             ⇒ None ?
766        ] in
767      let 〈new_pc, new_policy〉 ≝
768        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, short_jump〉 in
769        match add_instr with
770        [ None    ⇒ (* i.e. it's not a jump *)
771          〈add_instruction_size pc long_jump instr, policy〉
772        | Some ai ⇒
773          let new_length ≝ max_length old_length ai in
774          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 n) 〈pc, new_length〉 policy〉
775        ] in
776      〈S n, new_pc, new_policy〉
777    ) 〈0, zero ?, Stub ? ?〉 in
778    final_policy.
779 @I
780qed.
781 
782definition jump_expansion_internal: list labelled_instruction → jump_expansion_policy ≝
783  λprogram.
784    Stub ? ?.
785   
786(**************************************** START OF POLICY ABSTRACTION ********************)
787
788definition policy_type ≝ Word → jump_length.
789
790definition jump_expansion': pseudo_assembly_program → policy_type ≝
791 λprogram.λpc.
792  let policy ≝ jump_expansion_internal (\snd program) in
793  let 〈n,j〉 ≝ lookup ? ? pc policy 〈zero ?, long_jump〉 in
794    j.
795 
796definition assembly_1_pseudoinstruction_safe ≝
797  λprogram: pseudo_assembly_program.
798  λjump_expansion: policy_type.
799  λppc: Word.
800  λpc: Word.
801  λlookup_labels.
802  λlookup_datalabels.
803  λi.
804  let expansion ≝ jump_expansion ppc in
805    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
806    [ None ⇒ None ?
807    | Some pseudos ⇒
808      let mapped ≝ map ? ? assembly1 pseudos in
809      let flattened ≝ flatten ? mapped in
810      let pc_len ≝ length ? flattened in
811        Some ? (〈pc_len, flattened〉)
812    ].
813 
814definition construct_costs_safe ≝
815  λprogram.
816  λjump_expansion: policy_type.
817  λpseudo_program_counter: nat.
818  λprogram_counter: nat.
819  λcosts: BitVectorTrie Word 16.
820  λi.
821  match i with
822  [ Cost cost ⇒
823    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
824      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
825  | _ ⇒
826    let pc_bv ≝ bitvector_of_nat ? program_counter in
827    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
828    let lookup_labels ≝ λx.pc_bv in
829    let lookup_datalabels ≝ λx.zero ? in
830    let pc_delta_assembled ≝
831      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
832        lookup_labels lookup_datalabels i
833    in
834    match pc_delta_assembled with
835    [ None ⇒ None ?
836    | Some pc_delta_assembled ⇒
837      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
838        Some ? 〈pc_delta + program_counter, costs〉       
839    ]
840  ].
841
842(* This establishes the correspondence between pseudo program counters and
843   program counters. It is at the heart of the proof. *)
844(*CSC: code taken from build_maps *)
845definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
846 λinstr_list.
847 λjump_expansion: policy_type.
848 λl:list labelled_instruction.
849 λacc.
850  foldl ??
851   (λt,i.
852       match t with
853       [ None ⇒ None ?
854       | Some ppc_pc_map ⇒
855         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
856         let 〈program_counter, sigma_map〉 ≝ pc_map in
857         let 〈label, i〉 ≝ i in
858          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
859           [ None ⇒ None ?
860           | Some pc_ignore ⇒
861              let 〈pc,ignore〉 ≝ pc_ignore in
862              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
863       ]) acc l.
864
865definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
866 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).
867
868definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
869 λprogram,jump_expansion,instr_list.
870  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
871   [ None ⇒ None …
872   | Some result ⇒
873      let 〈ppc,pc_sigma_map〉 ≝ result in
874      let 〈pc,map〉 ≝ pc_sigma_map in
875       Some … 〈ppc,pc〉 ].
876
877definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
878 λinstr_list,jump_expansion.
879  match sigma0 instr_list jump_expansion with
880  [ None ⇒ None ?
881  | Some result ⇒
882    let 〈ppc,pc_sigma_map〉 ≝ result in
883    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
884      if gtb pc (2^16) then
885        None ?
886      else
887        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
888
889(* stuff about policy *)
890
891definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
892
893definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
894
895lemma eject_policy: ∀p. policy p → policy_type.
896 #p #pol @(eject … pol)
897qed.
898
899coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
900
901definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
902 λp,policy.
903  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
904   [ None ⇒ λabs. ⊥
905   | Some r ⇒ λ_.r] (sig2 … policy).
906 cases abs /2/
907qed.
908
909example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
910 cases daemon.
911qed.
912
913definition expand_pseudo_instruction:
914 ∀program:pseudo_assembly_program.∀pol: policy program.
915  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
916  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
917  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
918  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
919  pc = sigma program pol ppc →
920  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
921≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
922   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
923    [ None ⇒ let dummy ≝ [ ] in dummy
924    | Some res ⇒ res ].
925 [ cases daemon
926 | >p %]
927qed.
928
929(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
930definition assembly_1_pseudoinstruction':
931 ∀program:pseudo_assembly_program.∀pol: policy program.
932  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
933  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
934  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
935  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
936  Σres:(nat × (list Byte)).
937   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
938   let 〈len,code〉 ≝ res in
939    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
940     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
941≝ λprogram: pseudo_assembly_program.
942  λpol: policy program.
943  λppc: Word.
944  λlookup_labels.
945  λlookup_datalabels.
946  λpi.
947  λprf1,prf2,prf3.
948   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
949    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
950    | Some res ⇒ res ].
951 [ @⊥ elim pi in p [*]
952   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
953   generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)
954   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
955   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
956   cases daemon
957 | % [ >p %]
958   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
959   (* THIS SHOULD BE TRUE INSTEAD *)
960   cases daemon]
961qed.
962
963definition assembly_1_pseudoinstruction:
964 ∀program:pseudo_assembly_program.∀pol: policy program.
965  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
966  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
967  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
968  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
969   nat × (list Byte)
970≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
971   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
972    prf2 prf3.
973
974lemma assembly_1_pseudoinstruction_ok1:
975 ∀program:pseudo_assembly_program.∀pol: policy program.
976  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
977  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
978  ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
979  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
980     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
981   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
982 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
983 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
984 #H1 #_ @H1
985qed.
986
987(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
988definition construct_costs':
989 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
990  Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
991
992  λprogram.λpol: policy program.λppc,pc,costs,i.
993   match construct_costs_safe program pol ppc pc costs i with
994    [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy
995    | Some res ⇒ res ].
996 [ cases daemon
997 | >p %]
998qed.
999
1000definition construct_costs ≝
1001 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
1002
1003lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1004 #A #a #b #EQ destruct //
1005qed.
1006
1007lemma sigma00_strict:
1008 ∀instr_list,jump_expansion,l,acc. acc = None ? →
1009  sigma00 instr_list jump_expansion l acc = None ….
1010 #instr_list #jump_expansion #l elim l
1011  [ #acc #H >H %
1012  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
1013qed.
1014
1015lemma sigma00_append:
1016 ∀instr_list,jump_expansion,l1,l2,acc.
1017  sigma00 instr_list jump_expansion (l1@l2) acc =
1018   sigma00 instr_list jump_expansion
1019    l2 (sigma00 instr_list jump_expansion l1 acc).
1020 whd in match sigma00; normalize nodelta;
1021 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
1022qed.
1023
1024lemma policy_ok_prefix_ok:
1025 ∀program.∀pol:policy program.∀suffix,prefix.
1026  prefix@suffix = \snd program →
1027   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
1028 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
1029 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
1030 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
1031 normalize nodelta >sigma00_append
1032 cases (sigma00 ?? prefix ?)
1033  [2: #x #_ % #abs destruct(abs)
1034  | * #abs @⊥ @abs >sigma00_strict % ]
1035qed.
1036
1037lemma policy_ok_prefix_hd_ok:
1038 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
1039  (prefix@[hd])@suffix = \snd program →
1040   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
1041    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1042    let 〈program_counter, sigma_map〉 ≝ pc_map in
1043    let 〈label, i〉 ≝ hd in
1044     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
1045 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
1046 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
1047  (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
1048 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
1049 @pair_elim' #pc #map #EQ4 normalize nodelta
1050 @pair_elim' #l' #i' #EQ5 normalize nodelta
1051 cases (construct_costs_safe ??????) normalize
1052  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
1053qed.
1054
1055(*
1056lemma tech_pc_sigma00_append_Some:
1057 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1058  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1059   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1060 #program #pol #prefix #costs #label #i #ppc #pc #H
1061  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
1062  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
1063  generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
1064  whd in match sigma0; normalize nodelta;
1065  >foldl_step
1066  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
1067  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
1068  cases (sigma00 program pol prefix) in H ⊢ %
1069   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
1070   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
1071     
1072     normalize nodelta; -H;
1073     
1074 
1075   generalize in match H; -H;
1076  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
1077   [2: whd in ⊢ (??%%)
1078XXX
1079*)
1080
1081axiom construct_costs_sigma:
1082 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
1083  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
1084   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
1085
1086axiom tech_pc_sigma00_append_Some:
1087 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1088  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1089   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1090
1091definition build_maps:
1092 ∀pseudo_program.∀pol:policy pseudo_program.
1093  Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
1094   let 〈labels,costs〉 ≝ res in
1095    ∀id. occurs_exactly_once id (\snd pseudo_program) →
1096     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
1097
1098  λpseudo_program.λpol:policy pseudo_program.
1099  let result ≝
1100   foldl_strong
1101    (option Identifier × pseudo_instruction)
1102    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
1103      let 〈labels,ppc_pc_costs〉 ≝ res in
1104      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
1105      let 〈pc',costs〉 ≝ pc_costs in
1106       And ( And (
1107       And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
1108       (ppc' = length … pre)) (*∧ *)
1109       (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
1110       (∀id. occurs_exactly_once id pre →
1111        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
1112    (\snd pseudo_program)
1113    (λprefix,i,tl,prf,t.
1114      let 〈labels, ppc_pc_costs〉 ≝ t in
1115      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
1116      let 〈pc,costs〉 ≝ pc_costs in
1117       let 〈label, i'〉 ≝ i in
1118       let labels ≝
1119         match label with
1120         [ None ⇒ labels
1121         | Some label ⇒
1122           let program_counter_bv ≝ bitvector_of_nat ? pc in
1123             insert ? ? label program_counter_bv labels]
1124       in
1125         let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
1126          〈labels, 〈S ppc,construct〉〉
1127    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
1128  in
1129   let 〈labels, ppc_pc_costs〉 ≝ result in
1130   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
1131   let 〈pc, costs〉 ≝ pc_costs in
1132    〈labels, costs〉.
1133 [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
1134   generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
1135   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
1136   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
1137   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
1138   | #id normalize nodelta; -labels1; cases label; normalize nodelta
1139     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
1140     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
1141       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
1142        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
1143          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
1144        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
1145          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
1146 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
1147 | generalize in match (sig2 … result) in ⊢ ?;
1148   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?)
1149   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
1150qed.
1151
1152definition assembly:
1153 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝
1154  λp.let 〈preamble, instr_list〉 ≝ p in
1155   λpol.
1156    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
1157    let datalabels ≝ construct_datalabels preamble in
1158    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
1159    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
1160    let result ≝
1161     foldl_strong
1162      (option Identifier × pseudo_instruction)
1163      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
1164        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
1165        let 〈ppc,code〉 ≝ ppc_code in
1166         ∀ppc'.
1167          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
1168          let 〈len,assembledi〉 ≝
1169           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
1170           True)
1171      instr_list
1172      (λprefix,hd,tl,prf,pc_ppc_code.
1173        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
1174        let 〈ppc, code〉 ≝ ppc_code in
1175        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
1176        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
1177        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
1178         〈new_pc, 〈new_ppc, (code @ program)〉〉)
1179      〈(zero ?), 〈(zero ?), [ ]〉〉
1180    in
1181     〈\snd (\snd result), costs〉.
1182 [2,5: %
1183 |*: cases daemon ]
1184qed.
1185
1186definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
1187 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.