source: src/ASM/Assembly.ma @ 1404

Last change on this file since 1404 was 1404, checked in by boender, 8 years ago
  • reworked + added
  • added an axiom to arithmetic, but should be provable
File size: 59.6 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 (ℕ × 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 × nat) 16.
548
549definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
550  λpc.λjmp_len.λinstr.
551  let bv_pc ≝ bitvector_of_nat 16 pc in
552  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
553  let bv: list (BitVector 8) ≝ match ilist with
554    [ None   ⇒ (* hmm, this shouldn't happen *) [ ]
555    | Some l ⇒ flatten … (map … assembly1 l)
556    ] in
557  pc + (|bv|).
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
634lemma coerc_pair_sigma:
635 ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
636#A #B #P * #a #b #p % [@a | /2/]
637qed.
638coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
639≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
640     
641let rec create_label_trie (program: list labelled_instruction)
642  (policy: jump_expansion_policy):
643  (Σlabels:label_trie.
644    ∀i:ℕ.i < |program| →
645    ∀l.occurs_exactly_once l program →
646    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
647    ∃a.lookup_opt … l labels = Some ? 〈i,a〉
648  ) ≝
649  let 〈final_pc, final_labels〉 ≝
650    foldl_strong (option Identifier × pseudo_instruction)
651    (λprefix.ℕ × (Σlabels.
652      ∀i:ℕ.i < |prefix| →
653      ∀l.occurs_exactly_once l prefix →
654      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
655      ∃a.lookup_opt … l labels = Some ? 〈i,a〉)
656    )
657    program
658    (λprefix.λx.λtl.λprf.λacc.
659     let 〈pc,labels〉 ≝ acc in
660     let 〈label,instr〉 ≝ x in
661          let new_labels ≝
662          match label with
663          [ None   ⇒ labels
664          | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
665          ] in
666          let jmp_len ≝ \snd (lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
667          〈add_instruction_size pc jmp_len instr, new_labels〉
668    ) 〈0, Stub ? ?〉 in
669    final_labels.
670[ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
671  [ #Hi #l normalize nodelta; cases label normalize nodelta
672    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
673      lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
674      % [ @addr | @Haddr ]
675    | #l' #Hocc #Hl lapply (oeo_Some_Stronger … Hocc) -Hocc; #Hocc
676      lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq
677      [ >Heq in Hocc; #Hocc normalize in Hocc;
678        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
679        @⊥ @(absurd … Hocc)
680      | >Heq in Hocc; normalize nodelta #Hocc lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
681        [ #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]
682        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
683        ]
684      ]
685      >(bla i … Hl) normalize nodelta @nmk //
686    ]
687  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
688    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
689      [ normalize nodelta #H @⊥ @H
690      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_opt_insert_hit ]
691      ]
692    | @le_n
693    ]
694  ]
695| #i #Hi #l #Hl @⊥ @Hl
696]
697qed.
698
699definition select_reljump_length: label_trie → ℕ → Identifier → jump_length ≝
700  λlabels.λpc.λlbl.
701  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
702  if leb pc addr (* forward jump *)
703  then if leb (addr - pc) 126
704       then short_jump
705       else long_jump
706  else if leb (pc - addr) 129
707       then short_jump
708       else long_jump.
709
710definition select_call_length: label_trie → ℕ → Identifier → jump_length ≝
711  λlabels.λpc_nat.λlbl.
712  let pc ≝ bitvector_of_nat 16 pc_nat in
713  let addr ≝ bitvector_of_nat 16 (\snd (lookup ? ? lbl labels 〈0, pc_nat〉)) 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 select_jump_length: label_trie → ℕ → Identifier → jump_length ≝
721  λlabels.λpc.λlbl.
722  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
723  if leb pc addr
724  then if leb (addr - pc) 126
725       then short_jump
726       else select_call_length labels pc lbl
727  else if leb (pc - addr) 129
728       then short_jump
729       else select_call_length labels pc lbl.
730 
731definition jump_expansion_step_instruction: label_trie → ℕ →
732  preinstruction Identifier → option jump_length ≝
733  λlabels.λpc.λi.
734  match i with
735  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
736  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
737  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
738  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
739  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
740  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
741  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
742  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
743  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
744  | _        ⇒ None ?
745  ].
746
747definition max_length: jump_length → jump_length → jump_length ≝
748  λj1.λj2.
749  match j1 with
750  [ long_jump   ⇒ long_jump
751  | medium_jump ⇒
752    match j2 with
753    [ long_jump ⇒ long_jump
754    | _         ⇒ medium_jump
755    ]
756  | short_jump  ⇒ j2
757  ].
758
759definition jmpleq: jump_length → jump_length → Prop ≝
760  λj1.λj2.
761  match j1 with
762  [ short_jump  ⇒ True
763  | medium_jump ⇒
764    match j2 with
765    [ short_jump ⇒ False
766    | _          ⇒ True
767    ]
768  | long_jump   ⇒
769    match j2 with
770    [ long_jump ⇒ True
771    | _         ⇒ False
772    ]
773  ].
774
775definition is_jump' ≝
776  λx:preinstruction Identifier.
777  match x with
778  [ JC _ ⇒ True
779  | JNC _ ⇒ True
780  | JZ _ ⇒ True
781  | JNZ _ ⇒ True
782  | JB _ _ ⇒ True
783  | JNB _ _ ⇒ True
784  | JBC _ _ ⇒ True
785  | CJNE _ _ ⇒ True
786  | DJNZ _ _ ⇒ True
787  | _ ⇒ False
788  ].
789 
790definition is_jump ≝
791  λx:labelled_instruction.
792  let 〈label,instr〉 ≝ x in
793  match instr with
794  [ Instruction i   ⇒ is_jump' i
795  | Call _ ⇒ True
796  | Jmp _ ⇒ True
797  | _ ⇒ False
798  ].
799
800definition jump_in_policy ≝
801  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
802  ∀i:ℕ.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
803  ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉.
804   
805let rec jump_expansion_step (program: list labelled_instruction)
806  (old_policy: Σpolicy.jump_in_policy program policy):
807  (Σpolicy.
808    jump_in_policy program policy ∧
809    (jump_in_policy program policy → True)) ≝
810  let labels ≝ create_label_trie program old_policy in
811  let 〈final_pc, final_policy〉 ≝
812    foldl_strong (option Identifier × pseudo_instruction)
813    (λprefix.ℕ × Σpolicy.
814      jump_in_policy prefix policy ∧
815      (jump_in_policy prefix policy → True)
816    )
817    program
818    (λprefix.λx.λtl.λprf.λacc.
819      let 〈pc, policy〉 ≝ acc in
820      let 〈label,instr〉 ≝ x in
821      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) policy in
822      let add_instr ≝
823        match instr with
824        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
825        | Call c        ⇒ Some ? (select_call_length labels pc c)
826        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
827        | _             ⇒ None ?
828        ] in
829      let 〈new_pc, new_policy〉 ≝
830        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, short_jump〉 in
831        match add_instr with
832        [ None    ⇒ (* i.e. it's not a jump *)
833          〈add_instruction_size pc long_jump instr, policy〉
834        | Some ai ⇒
835          let new_length ≝ max_length old_length ai in
836          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, new_length〉 policy〉
837        ] in
838      〈new_pc, new_policy〉
839    ) 〈0, Stub ? ?〉 in
840    final_policy.
841[ @conj
842  [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
843    [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
844      lapply (sig2 … policy) #Hacc elim ((proj1 … Hacc) i (le_S_S_to_le … Hi) Hj) #h #n elim n
845      -n #n #Hn
846      % [ @h | % [ @n | normalize nodelta cases instr normalize nodelta
847      [2,3: #x cases (lookup ??? policy ?) #y #z @Hn
848      |6: #x #y cases (lookup ??? policy ?) #w #z @Hn
849      |1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???)
850        [ @Hn
851        | #z normalize nodelta <Hn @lookup_opt_insert_miss
852          @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|)))
853          [ @(bitvector_of_nat_ok … H)
854          | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
855          ] ]
856        ]
857      |4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hn
858        @lookup_opt_insert_miss @notb_elim >eq_bv_false
859        [1,3: //
860        |2,4: @nmk #H @(absurd (i = (|prefix|)))
861          [1,3: @(bitvector_of_nat_ok … H)
862          |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
863          ] ]
864      ] ] ]
865    | #Hi >nth_append_second >(injective_S … Hi)
866      [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
867        [2,3: #x #Hj @⊥ @Hj
868        |6: #x #y #Hj @⊥ @Hj
869        |1: #pi cases pi
870          [35,36,37: #Hj @⊥ @Hj
871          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
872          |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
873          |9,10,14,15: #j normalize nodelta #_
874            % [1,3,5,7: @pc
875              |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
876                cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)         
877                #x #y #Hl normalize nodelta
878            % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
879              |2,4,6,8: @lookup_opt_insert_hit
880              ] ]
881          |11,12,13,16,17: #x #j normalize nodelta #_
882            % [1,3,5,7,9: @pc
883              |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
884                cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)         
885                #x #y #Hl normalize nodelta
886            % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
887              |2,4,6,8,10: @lookup_opt_insert_hit
888              ] ]
889          ]
890        |4,5: #j normalize nodelta #_
891          % [1,3: @pc
892            |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉)
893                #x #y normalize nodelta
894            % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))
895              |3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j))
896              |2,4: @lookup_opt_insert_hit
897              ]
898            ]
899        ]
900      | @le_n
901      ]
902    ]
903  | //
904  ]
905| @conj
906  [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
907  | //
908  ]
909]
910qed.
911 
912definition jump_expansion_internal: list labelled_instruction → jump_expansion_policy ≝
913  λprogram.
914    Stub ? ?.
915   
916(**************************************** START OF POLICY ABSTRACTION ********************)
917
918definition policy_type ≝ Word → jump_length.
919
920definition jump_expansion': pseudo_assembly_program → policy_type ≝
921 λprogram.λpc.
922  let policy ≝ jump_expansion_internal (\snd program) in
923  let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in
924    j.
925 
926definition assembly_1_pseudoinstruction_safe ≝
927  λprogram: pseudo_assembly_program.
928  λjump_expansion: policy_type.
929  λppc: Word.
930  λpc: Word.
931  λlookup_labels.
932  λlookup_datalabels.
933  λi.
934  let expansion ≝ jump_expansion ppc in
935    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
936    [ None ⇒ None ?
937    | Some pseudos ⇒
938      let mapped ≝ map ? ? assembly1 pseudos in
939      let flattened ≝ flatten ? mapped in
940      let pc_len ≝ length ? flattened in
941        Some ? (〈pc_len, flattened〉)
942    ].
943 
944definition construct_costs_safe ≝
945  λprogram.
946  λjump_expansion: policy_type.
947  λpseudo_program_counter: nat.
948  λprogram_counter: nat.
949  λcosts: BitVectorTrie Word 16.
950  λi.
951  match i with
952  [ Cost cost ⇒
953    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
954      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
955  | _ ⇒
956    let pc_bv ≝ bitvector_of_nat ? program_counter in
957    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
958    let lookup_labels ≝ λx.pc_bv in
959    let lookup_datalabels ≝ λx.zero ? in
960    let pc_delta_assembled ≝
961      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
962        lookup_labels lookup_datalabels i
963    in
964    match pc_delta_assembled with
965    [ None ⇒ None ?
966    | Some pc_delta_assembled ⇒
967      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
968        Some ? 〈pc_delta + program_counter, costs〉       
969    ]
970  ].
971
972(* This establishes the correspondence between pseudo program counters and
973   program counters. It is at the heart of the proof. *)
974(*CSC: code taken from build_maps *)
975definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
976 λinstr_list.
977 λjump_expansion: policy_type.
978 λl:list labelled_instruction.
979 λacc.
980  foldl ??
981   (λt,i.
982       match t with
983       [ None ⇒ None ?
984       | Some ppc_pc_map ⇒
985         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
986         let 〈program_counter, sigma_map〉 ≝ pc_map in
987         let 〈label, i〉 ≝ i in
988          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
989           [ None ⇒ None ?
990           | Some pc_ignore ⇒
991              let 〈pc,ignore〉 ≝ pc_ignore in
992              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
993       ]) acc l.
994
995definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
996 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).
997
998definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
999 λprogram,jump_expansion,instr_list.
1000  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
1001   [ None ⇒ None …
1002   | Some result ⇒
1003      let 〈ppc,pc_sigma_map〉 ≝ result in
1004      let 〈pc,map〉 ≝ pc_sigma_map in
1005       Some … 〈ppc,pc〉 ].
1006
1007definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
1008 λinstr_list,jump_expansion.
1009  match sigma0 instr_list jump_expansion with
1010  [ None ⇒ None ?
1011  | Some result ⇒
1012    let 〈ppc,pc_sigma_map〉 ≝ result in
1013    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
1014      if gtb pc (2^16) then
1015        None ?
1016      else
1017        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
1018
1019(* stuff about policy *)
1020
1021definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
1022
1023definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
1024
1025lemma eject_policy: ∀p. policy p → policy_type.
1026 #p #pol @(eject … pol)
1027qed.
1028
1029coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
1030
1031definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
1032 λp,policy.
1033  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
1034   [ None ⇒ λabs. ⊥
1035   | Some r ⇒ λ_.r] (sig2 … policy).
1036 cases abs /2/
1037qed.
1038
1039example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
1040 cases daemon.
1041qed.
1042
1043definition expand_pseudo_instruction:
1044 ∀program:pseudo_assembly_program.∀pol: policy program.
1045  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
1046  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1047  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1048  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
1049  pc = sigma program pol ppc →
1050  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
1051≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
1052   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
1053    [ None ⇒ let dummy ≝ [ ] in dummy
1054    | Some res ⇒ res ].
1055 [ cases daemon
1056 | >p %]
1057qed.
1058
1059(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1060definition assembly_1_pseudoinstruction':
1061 ∀program:pseudo_assembly_program.∀pol: policy program.
1062  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1063  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1064  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1065  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1066  Σres:(nat × (list Byte)).
1067   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
1068   let 〈len,code〉 ≝ res in
1069    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
1070     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
1071≝ λprogram: pseudo_assembly_program.
1072  λpol: policy program.
1073  λppc: Word.
1074  λlookup_labels.
1075  λlookup_datalabels.
1076  λpi.
1077  λprf1,prf2,prf3.
1078   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
1079    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
1080    | Some res ⇒ res ].
1081 [ @⊥ elim pi in p [*]
1082   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
1083   generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)
1084   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
1085   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
1086   cases daemon
1087 | % [ >p %]
1088   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
1089   (* THIS SHOULD BE TRUE INSTEAD *)
1090   cases daemon]
1091qed.
1092
1093definition assembly_1_pseudoinstruction:
1094 ∀program:pseudo_assembly_program.∀pol: policy program.
1095  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1096  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1097  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1098  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1099   nat × (list Byte)
1100≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
1101   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
1102    prf2 prf3.
1103
1104lemma assembly_1_pseudoinstruction_ok1:
1105 ∀program:pseudo_assembly_program.∀pol: policy program.
1106  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1107  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
1108  ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
1109  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
1110     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
1111   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
1112 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
1113 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
1114 #H1 #_ @H1
1115qed.
1116
1117(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1118definition construct_costs':
1119 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
1120  Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
1121
1122  λprogram.λpol: policy program.λppc,pc,costs,i.
1123   match construct_costs_safe program pol ppc pc costs i with
1124    [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy
1125    | Some res ⇒ res ].
1126 [ cases daemon
1127 | >p %]
1128qed.
1129
1130definition construct_costs ≝
1131 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
1132
1133lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1134 #A #a #b #EQ destruct //
1135qed.
1136
1137lemma sigma00_strict:
1138 ∀instr_list,jump_expansion,l,acc. acc = None ? →
1139  sigma00 instr_list jump_expansion l acc = None ….
1140 #instr_list #jump_expansion #l elim l
1141  [ #acc #H >H %
1142  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
1143qed.
1144
1145lemma sigma00_append:
1146 ∀instr_list,jump_expansion,l1,l2,acc.
1147  sigma00 instr_list jump_expansion (l1@l2) acc =
1148   sigma00 instr_list jump_expansion
1149    l2 (sigma00 instr_list jump_expansion l1 acc).
1150 whd in match sigma00; normalize nodelta;
1151 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
1152qed.
1153
1154lemma policy_ok_prefix_ok:
1155 ∀program.∀pol:policy program.∀suffix,prefix.
1156  prefix@suffix = \snd program →
1157   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
1158 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
1159 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
1160 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
1161 normalize nodelta >sigma00_append
1162 cases (sigma00 ?? prefix ?)
1163  [2: #x #_ % #abs destruct(abs)
1164  | * #abs @⊥ @abs >sigma00_strict % ]
1165qed.
1166
1167lemma policy_ok_prefix_hd_ok:
1168 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
1169  (prefix@[hd])@suffix = \snd program →
1170   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
1171    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1172    let 〈program_counter, sigma_map〉 ≝ pc_map in
1173    let 〈label, i〉 ≝ hd in
1174     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
1175 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
1176 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
1177  (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
1178 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
1179 @pair_elim' #pc #map #EQ4 normalize nodelta
1180 @pair_elim' #l' #i' #EQ5 normalize nodelta
1181 cases (construct_costs_safe ??????) normalize
1182  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
1183qed.
1184
1185(*
1186lemma tech_pc_sigma00_append_Some:
1187 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1188  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1189   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1190 #program #pol #prefix #costs #label #i #ppc #pc #H
1191  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
1192  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
1193  generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
1194  whd in match sigma0; normalize nodelta;
1195  >foldl_step
1196  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
1197  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
1198  cases (sigma00 program pol prefix) in H ⊢ %
1199   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
1200   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
1201     
1202     normalize nodelta; -H;
1203     
1204 
1205   generalize in match H; -H;
1206  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
1207   [2: whd in ⊢ (??%%)
1208XXX
1209*)
1210
1211axiom construct_costs_sigma:
1212 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
1213  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
1214   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
1215
1216axiom tech_pc_sigma00_append_Some:
1217 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1218  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1219   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1220
1221definition build_maps:
1222 ∀pseudo_program.∀pol:policy pseudo_program.
1223  Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
1224   let 〈labels,costs〉 ≝ res in
1225    ∀id. occurs_exactly_once id (\snd pseudo_program) →
1226     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
1227
1228  λpseudo_program.λpol:policy pseudo_program.
1229  let result ≝
1230   foldl_strong
1231    (option Identifier × pseudo_instruction)
1232    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
1233      let 〈labels,ppc_pc_costs〉 ≝ res in
1234      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
1235      let 〈pc',costs〉 ≝ pc_costs in
1236       And ( And (
1237       And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
1238       (ppc' = length … pre)) (*∧ *)
1239       (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
1240       (∀id. occurs_exactly_once id pre →
1241        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
1242    (\snd pseudo_program)
1243    (λprefix,i,tl,prf,t.
1244      let 〈labels, ppc_pc_costs〉 ≝ t in
1245      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
1246      let 〈pc,costs〉 ≝ pc_costs in
1247       let 〈label, i'〉 ≝ i in
1248       let labels ≝
1249         match label with
1250         [ None ⇒ labels
1251         | Some label ⇒
1252           let program_counter_bv ≝ bitvector_of_nat ? pc in
1253             insert ? ? label program_counter_bv labels]
1254       in
1255         let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
1256          〈labels, 〈S ppc,construct〉〉
1257    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
1258  in
1259   let 〈labels, ppc_pc_costs〉 ≝ result in
1260   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
1261   let 〈pc, costs〉 ≝ pc_costs in
1262    〈labels, costs〉.
1263 [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
1264   generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
1265   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
1266   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
1267   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
1268   | #id normalize nodelta; -labels1; cases label; normalize nodelta
1269     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
1270     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
1271       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
1272        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
1273          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
1274        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
1275          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
1276 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
1277 | generalize in match (sig2 … result) in ⊢ ?;
1278   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?)
1279   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
1280qed.
1281
1282definition assembly:
1283 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝
1284  λp.let 〈preamble, instr_list〉 ≝ p in
1285   λpol.
1286    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
1287    let datalabels ≝ construct_datalabels preamble in
1288    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
1289    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
1290    let result ≝
1291     foldl_strong
1292      (option Identifier × pseudo_instruction)
1293      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
1294        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
1295        let 〈ppc,code〉 ≝ ppc_code in
1296         ∀ppc'.
1297          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
1298          let 〈len,assembledi〉 ≝
1299           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
1300           True)
1301      instr_list
1302      (λprefix,hd,tl,prf,pc_ppc_code.
1303        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
1304        let 〈ppc, code〉 ≝ ppc_code in
1305        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
1306        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
1307        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
1308         〈new_pc, 〈new_ppc, (code @ program)〉〉)
1309      〈(zero ?), 〈(zero ?), [ ]〉〉
1310    in
1311     〈\snd (\snd result), costs〉.
1312 [2,5: %
1313 |*: cases daemon ]
1314qed.
1315
1316definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
1317 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.