source: src/ASM/Assembly.ma @ 1609

Last change on this file since 1609 was 1609, checked in by boender, 8 years ago
  • added alias to ASM/BitVectorTrie
  • removed double include from common/Errors
  • externalised label generation in ASM/Assembly, plus stuff to make it compile
File size: 95.2 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Status.ma".
5include alias "basics/logic.ma".
6include alias "arithmetics/nat.ma".
7include "utilities/extralib.ma".
8
9definition assembly_preinstruction ≝
10  λA: Type[0].
11  λaddr_of: A → Byte. (* relative *)
12  λpre: preinstruction A.
13  match pre with
14  [ ADD addr1 addr2 ⇒
15     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
16      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
17      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
18      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
19      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
20      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
21  | ADDC addr1 addr2 ⇒
22     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
23      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
24      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
25      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
26      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
27      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
28  | ANL addrs ⇒
29     match addrs with
30      [ inl addrs ⇒ match addrs with
31         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
32           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
33            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
34            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
35            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
36            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
37            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
38         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
39            let b1 ≝
40             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
41              [ DIRECT b1 ⇒ λ_.b1
42              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
43            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
44             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
45             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
46             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
47         ]
48      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
49         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
50          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
51          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
52          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
53  | CLR addr ⇒
54     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
55      [ ACC_A ⇒ λ_.
56         [ ([[true; true; true; false; false; true; false; false]]) ]
57      | CARRY ⇒ λ_.
58         [ ([[true; true; false; false; false; false; true; true]]) ]
59      | BIT_ADDR b1 ⇒ λ_.
60         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
61      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
62  | CPL addr ⇒
63     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
64      [ ACC_A ⇒ λ_.
65         [ ([[true; true; true; true; false; true; false; false]]) ]
66      | CARRY ⇒ λ_.
67         [ ([[true; false; true; true; false; false; true; true]]) ]
68      | BIT_ADDR b1 ⇒ λ_.
69         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
70      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
71  | DA addr ⇒
72     [ ([[true; true; false; true; false; true; false; false]]) ]
73  | DEC addr ⇒
74     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
75      [ ACC_A ⇒ λ_.
76         [ ([[false; false; false; true; false; true; false; false]]) ]
77      | REGISTER r ⇒ λ_.
78         [ ([[false; false; false; true; true]]) @@ r ]
79      | DIRECT b1 ⇒ λ_.
80         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
81      | INDIRECT i1 ⇒ λ_.
82         [ ([[false; false; false; true; false; true; true; i1]]) ]
83      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
84      | DJNZ addr1 addr2 ⇒
85         let b2 ≝ addr_of addr2 in
86         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
87          [ REGISTER r ⇒ λ_.
88             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
89          | DIRECT b1 ⇒ λ_.
90             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
91          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
92      | JC addr ⇒
93        let b1 ≝ addr_of addr in
94          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
95      | JNC addr ⇒
96         let b1 ≝ addr_of addr in
97           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
98      | JZ addr ⇒
99         let b1 ≝ addr_of addr in
100           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
101      | JNZ addr ⇒
102         let b1 ≝ addr_of addr in
103           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
104      | JB addr1 addr2 ⇒
105         let b2 ≝ addr_of addr2 in
106         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
107          [ BIT_ADDR b1 ⇒ λ_.
108             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
109          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
110      | JNB addr1 addr2 ⇒
111         let b2 ≝ addr_of addr2 in
112         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
113          [ BIT_ADDR b1 ⇒ λ_.
114             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
115          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
116      | JBC addr1 addr2 ⇒
117         let b2 ≝ addr_of addr2 in
118         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
119          [ BIT_ADDR b1 ⇒ λ_.
120             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
121          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
122      | CJNE addrs addr3 ⇒
123         let b3 ≝ addr_of addr3 in
124         match addrs with
125          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
126             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
127              [ DIRECT b1 ⇒ λ_.
128                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
129              | DATA b1 ⇒ λ_.
130                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
131              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
132          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
133             let b2 ≝
134              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
135               [ DATA b2 ⇒ λ_. b2
136               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
137             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
138              [ REGISTER r ⇒ λ_.
139                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
140              | INDIRECT i1 ⇒ λ_.
141                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
142              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
143         ]
144  | DIV addr1 addr2 ⇒
145     [ ([[true;false;false;false;false;true;false;false]]) ]
146  | INC addr ⇒
147     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
148      [ ACC_A ⇒ λ_.
149         [ ([[false;false;false;false;false;true;false;false]]) ]         
150      | REGISTER r ⇒ λ_.
151         [ ([[false;false;false;false;true]]) @@ r ]
152      | DIRECT b1 ⇒ λ_.
153         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
154      | INDIRECT i1 ⇒ λ_.
155        [ ([[false; false; false; false; false; true; true; i1]]) ]
156      | DPTR ⇒ λ_.
157        [ ([[true;false;true;false;false;false;true;true]]) ]
158      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
159  | MOV 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 ⇒
168                     match addrs with
169                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
170                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
171                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
172                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
173                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
174                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
175                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
176                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
177                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
178                          [ REGISTER r ⇒ λ_.
179                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
180                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
181                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
182                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
183                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
184                          | INDIRECT i1 ⇒ λ_.
185                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
186                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
187                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
188                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
189                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
190                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
191                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
192                     let b1 ≝
193                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
194                       [ DIRECT b1 ⇒ λ_. b1
195                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
196                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
197                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
198                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
199                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
200                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
201                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
202                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
203              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
204                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
205                  [ DATA16 w ⇒ λ_.
206                     let b1_b2 ≝ split ? 8 8 w in
207                     let b1 ≝ \fst b1_b2 in
208                     let b2 ≝ \snd b1_b2 in
209                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
210                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
211          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
212             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
213              [ BIT_ADDR b1 ⇒ λ_.
214                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
215              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
216      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
217         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
218          [ BIT_ADDR b1 ⇒ λ_.
219             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
220          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
221  | MOVX addrs ⇒
222     match addrs with
223      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
224         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
225          [ EXT_INDIRECT i1 ⇒ λ_.
226             [ ([[true;true;true;false;false;false;true;i1]]) ]
227          | EXT_INDIRECT_DPTR ⇒ λ_.
228             [ ([[true;true;true;false;false;false;false;false]]) ]
229          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
230      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
231         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
232          [ EXT_INDIRECT i1 ⇒ λ_.
233             [ ([[true;true;true;true;false;false;true;i1]]) ]
234          | EXT_INDIRECT_DPTR ⇒ λ_.
235             [ ([[true;true;true;true;false;false;false;false]]) ]
236          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
237  | MUL addr1 addr2 ⇒
238     [ ([[true;false;true;false;false;true;false;false]]) ]
239  | NOP ⇒
240     [ ([[false;false;false;false;false;false;false;false]]) ]
241  | ORL addrs ⇒
242     match addrs with
243      [ inl addrs ⇒
244         match addrs with
245          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
246             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
247             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
248             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
249             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
250             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
251             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
252          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
253            let b1 ≝
254              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
255               [ DIRECT b1 ⇒ λ_. b1
256               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
257             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
258              [ ACC_A ⇒ λ_.
259                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
260              | DATA b2 ⇒ λ_.
261                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
262              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
263      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
264         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
265          [ BIT_ADDR b1 ⇒ λ_.
266             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
267          | N_BIT_ADDR b1 ⇒ λ_.
268             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
269          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
270  | POP addr ⇒
271     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
272      [ DIRECT b1 ⇒ λ_.
273         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
274      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
275  | PUSH addr ⇒
276     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
277      [ DIRECT b1 ⇒ λ_.
278         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
279      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
280  | RET ⇒
281     [ ([[false;false;true;false;false;false;true;false]]) ]
282  | RETI ⇒
283     [ ([[false;false;true;true;false;false;true;false]]) ]
284  | RL addr ⇒
285     [ ([[false;false;true;false;false;false;true;true]]) ]
286  | RLC addr ⇒
287     [ ([[false;false;true;true;false;false;true;true]]) ]
288  | RR addr ⇒
289     [ ([[false;false;false;false;false;false;true;true]]) ]
290  | RRC addr ⇒
291     [ ([[false;false;false;true;false;false;true;true]]) ]
292  | SETB addr ⇒     
293     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
294      [ CARRY ⇒ λ_.
295         [ ([[true;true;false;true;false;false;true;true]]) ]
296      | BIT_ADDR b1 ⇒ λ_.
297         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
298      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
299  | SUBB addr1 addr2 ⇒
300     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
301      [ REGISTER r ⇒ λ_.
302         [ ([[true;false;false;true;true]]) @@ r ]
303      | DIRECT b1 ⇒ λ_.
304         [ ([[true;false;false;true;false;true;false;true]]); b1]
305      | INDIRECT i1 ⇒ λ_.
306         [ ([[true;false;false;true;false;true;true;i1]]) ]
307      | DATA b1 ⇒ λ_.
308         [ ([[true;false;false;true;false;true;false;false]]); b1]
309      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
310  | SWAP addr ⇒
311     [ ([[true;true;false;false;false;true;false;false]]) ]
312  | XCH addr1 addr2 ⇒
313     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
314      [ REGISTER r ⇒ λ_.
315         [ ([[true;true;false;false;true]]) @@ r ]
316      | DIRECT b1 ⇒ λ_.
317         [ ([[true;true;false;false;false;true;false;true]]); b1]
318      | INDIRECT i1 ⇒ λ_.
319         [ ([[true;true;false;false;false;true;true;i1]]) ]
320      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
321  | XCHD addr1 addr2 ⇒
322     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
323      [ INDIRECT i1 ⇒ λ_.
324         [ ([[true;true;false;true;false;true;true;i1]]) ]
325      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
326  | XRL addrs ⇒
327     match addrs with
328      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
329         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
330          [ REGISTER r ⇒ λ_.
331             [ ([[false;true;true;false;true]]) @@ r ]
332          | DIRECT b1 ⇒ λ_.
333             [ ([[false;true;true;false;false;true;false;true]]); b1]
334          | INDIRECT i1 ⇒ λ_.
335             [ ([[false;true;true;false;false;true;true;i1]]) ]
336          | DATA b1 ⇒ λ_.
337             [ ([[false;true;true;false;false;true;false;false]]); b1]
338          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
339      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
340         let b1 ≝
341          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
342           [ DIRECT b1 ⇒ λ_. b1
343           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
344         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
345          [ ACC_A ⇒ λ_.
346             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
347          | DATA b2 ⇒ λ_.
348             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
349          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
350       ].
351
352definition assembly1 ≝
353 λi: instruction.
354 match i with
355  [ ACALL addr ⇒
356     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
357      [ ADDR11 w ⇒ λ_.
358         let v1_v2 ≝ split ? 3 8 w in
359         let v1 ≝ \fst v1_v2 in
360         let v2 ≝ \snd v1_v2 in
361          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
362      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
363  | AJMP addr ⇒
364     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
365      [ ADDR11 w ⇒ λ_.
366         let v1_v2 ≝ split ? 3 8 w in
367         let v1 ≝ \fst v1_v2 in
368         let v2 ≝ \snd v1_v2 in
369          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
370      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
371  | JMP adptr ⇒
372     [ ([[false;true;true;true;false;false;true;true]]) ]
373  | LCALL addr ⇒
374     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
375      [ ADDR16 w ⇒ λ_.
376         let b1_b2 ≝ split ? 8 8 w in
377         let b1 ≝ \fst b1_b2 in
378         let b2 ≝ \snd b1_b2 in
379          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
380      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
381  | LJMP addr ⇒
382     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
383      [ ADDR16 w ⇒ λ_.
384         let b1_b2 ≝ split ? 8 8 w in
385         let b1 ≝ \fst b1_b2 in
386         let b2 ≝ \snd b1_b2 in
387          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
388      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
389  | MOVC addr1 addr2 ⇒
390     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
391      [ ACC_DPTR ⇒ λ_.
392         [ ([[true;false;false;true;false;false;true;true]]) ]
393      | ACC_PC ⇒ λ_.
394         [ ([[true;false;false;false;false;false;true;true]]) ]
395      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
396  | SJMP addr ⇒
397     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
398      [ RELATIVE b1 ⇒ λ_.
399         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
400      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
401  | RealInstruction instr ⇒
402    assembly_preinstruction [[ relative ]]
403      (λx.
404        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
405        [ RELATIVE r ⇒ λ_. r
406        | _ ⇒ λabsd. ⊥
407        ] (subaddressing_modein … x)) instr
408  ].
409  cases absd
410qed.
411
412(* definition of & operations on jump length *)
413inductive jump_length: Type[0] ≝
414  | short_jump: jump_length
415  | medium_jump: jump_length
416  | long_jump: jump_length.
417
418definition max_length: jump_length → jump_length → jump_length ≝
419  λj1.λj2.
420  match j1 with
421  [ long_jump   ⇒ long_jump
422  | medium_jump ⇒
423    match j2 with
424    [ long_jump ⇒ long_jump
425    | _         ⇒ medium_jump
426    ]
427  | short_jump  ⇒ j2
428  ].
429
430definition jmple: jump_length → jump_length → Prop ≝
431  λj1.λj2.
432  match j1 with
433  [ short_jump  ⇒
434    match j2 with
435    [ short_jump ⇒ False
436    | _          ⇒ True
437    ]
438  | medium_jump ⇒
439    match j2 with
440    [ long_jump ⇒ True
441    | _         ⇒ False
442    ]
443  | long_jump   ⇒ False
444  ].
445
446definition jmpleq: jump_length → jump_length → Prop ≝
447  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
448 
449lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
450 #x #y cases x cases y /3 by inl, inr, nmk, I/
451qed.
452 
453lemma jmpleq_max_length: ∀ol,nl.
454  jmpleq ol (max_length ol nl).
455 #ol #nl cases ol cases nl
456 /2 by or_introl, or_intror, I/
457qed.
458
459lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
460  #a #b cases a cases b /2/
461  %2 @nmk #H destruct (H)
462qed.
463
464 
465(* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
466definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.
467
468definition expand_relative_jump_internal:
469 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
470 option (list instruction)
471 ≝
472  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
473  match jmp_len with
474  [ short_jump ⇒
475     let lookup_address ≝ lookup_labels jmp in
476     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
477     let 〈upper, lower〉 ≝ split ? 8 8 result in
478     if eq_bv ? upper (zero 8) then
479      let address ≝ RELATIVE lower in
480       Some ? [ RealInstruction (i address) ]
481     else
482       None ?
483  | medium_jump ⇒ None …
484  | long_jump ⇒
485    Some ?
486    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
487      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
488      LJMP (ADDR16 (lookup_labels jmp))
489    ]
490  ].
491  @ I
492qed.
493
494definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
495  λlookup_labels.
496  λjmp_len: jump_length.
497  λpc.
498  λi: preinstruction Identifier.
499  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
500  match i with
501  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
502  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
503  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
504  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
505  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
506  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
507  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
508  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
509  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
510  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
511  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
512  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
513  | INC arg ⇒ Some ? [ INC ? arg ]
514  | DEC arg ⇒ Some ? [ DEC ? arg ]
515  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
516  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
517  | DA arg ⇒ Some ? [ DA ? arg ]
518  | ANL arg ⇒ Some ? [ ANL ? arg ]
519  | ORL arg ⇒ Some ? [ ORL ? arg ]
520  | XRL arg ⇒ Some ? [ XRL ? arg ]
521  | CLR arg ⇒ Some ? [ CLR ? arg ]
522  | CPL arg ⇒ Some ? [ CPL ? arg ]
523  | RL arg ⇒ Some ? [ RL ? arg ]
524  | RR arg ⇒ Some ? [ RR ? arg ]
525  | RLC arg ⇒ Some ? [ RLC ? arg ]
526  | RRC arg ⇒ Some ? [ RRC ? arg ]
527  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
528  | MOV arg ⇒ Some ? [ MOV ? arg ]
529  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
530  | SETB arg ⇒ Some ? [ SETB ? arg ]
531  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
532  | POP arg ⇒ Some ? [ POP ? arg ]
533  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
534  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
535  | RET ⇒ Some ? [ RET ? ]
536  | RETI ⇒ Some ? [ RETI ? ]
537  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
538  ].
539
540definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
541  λlookup_labels.
542  λlookup_datalabels.
543  λpc.
544  λjmp_len.
545  λi.
546  match i with
547  [ Cost cost ⇒ Some ? [ ]
548  | Comment comment ⇒ Some ? [ ]
549  | Call call ⇒
550    match jmp_len with
551    [ short_jump ⇒ None ?
552    | medium_jump ⇒
553      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
554      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
555      if eq_bv ? ignore fst_5 then
556        let address ≝ ADDR11 address in
557          Some ? ([ ACALL address ])
558      else
559        None ?
560    | long_jump ⇒
561      let address ≝ ADDR16 (lookup_labels call) in
562        Some ? [ LCALL address ]
563    ]
564  | Mov d trgt ⇒
565    let address ≝ DATA16 (lookup_datalabels trgt) in
566      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
567  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
568  | Jmp jmp ⇒
569    match jmp_len with
570    [ short_jump ⇒
571      let lookup_address ≝ lookup_labels jmp in
572      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
573      let 〈upper, lower〉 ≝ split ? 8 8 result in
574      if eq_bv ? upper (zero 8) then
575        let address ≝ RELATIVE lower in
576          Some ? [ SJMP address ]
577      else
578        None ?
579    | medium_jump ⇒
580      let address ≝ lookup_labels jmp in
581      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
582      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
583      if eq_bv ? fst_5_addr fst_5_pc then
584        let address ≝ ADDR11 rest_addr in
585          Some ? ([ AJMP address ])
586      else
587        None ?
588    | long_jump ⇒
589      let address ≝ ADDR16 (lookup_labels jmp) in
590        Some ? [ LJMP address ]
591    ]
592  ].
593  @ I
594qed.
595
596(* label_map: identifier ↦ 〈instruction number, address〉 *)
597definition label_map ≝ identifier_map ASMTag (nat × nat).
598
599definition is_label ≝
600  λx:labelled_instruction.λl:Identifier.
601  let 〈lbl,instr〉 ≝ x in
602  match lbl with
603  [ Some l' ⇒ l' = l
604  | _       ⇒ False
605  ].
606
607definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
608  λpc.λjmp_len.λinstr.
609  let bv_pc ≝ bitvector_of_nat 16 pc in
610  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
611  let bv: list (BitVector 8) ≝ match ilist with
612    [ None   ⇒ (* this shouldn't happen *) [ ]
613    | Some l ⇒ flatten … (map … assembly1 l)
614    ] in
615  pc + (|bv|).
616
617lemma label_does_not_occur:
618  ∀i,p,l.
619  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
620 #i #p #l generalize in match i; elim p
621 [ #i >nth_nil #H @⊥ @H
622 | #h #t #IH #i cases i -i
623   [ cases h #hi #hp cases hi
624     [ normalize #H @⊥ @H
625     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
626       whd in Heq; >Heq
627       >eq_identifier_refl //
628     ]
629   | #i #H whd in match (does_not_occur ??);
630     whd in match (instruction_matches_identifier ??);
631     cases h #hi #hp cases hi normalize nodelta
632     [ @(IH i) @H
633     | #l' @eq_identifier_elim
634       [ normalize //
635       | normalize #_ @(IH i) @H
636       ]
637     ]
638   ]
639 ]
640qed. 
641
642lemma coerc_pair_sigma:
643 ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
644#A #B #P * #a #b #p % [@a | /2/]
645qed.
646coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
647≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
648
649definition create_label_map: ∀program:list labelled_instruction.
650  ∀policy:jump_expansion_policy.
651  (Σlabels:label_map.
652    ∀i:ℕ.lt i (|program|) →
653    ∀l.occurs_exactly_once l program →
654    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
655    ∃a.lookup … labels l = Some ? 〈i,a〉
656  ) ≝
657  λprogram.λpolicy.
658  let 〈final_pc, final_labels〉 ≝
659    foldl_strong (option Identifier × pseudo_instruction)
660    (λprefix.ℕ × (Σlabels.
661      ∀i:ℕ.lt i (|prefix|) →
662      ∀l.occurs_exactly_once l prefix →
663      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
664      ∃a.lookup … labels l = Some ? 〈i,a〉)
665    )
666    program
667    (λprefix.λx.λtl.λprf.λacc.
668     let 〈pc,labels〉 ≝ acc in
669     let 〈label,instr〉 ≝ x in
670       let new_labels ≝
671       match label with
672       [ None   ⇒ labels
673       | Some l ⇒ add … labels l 〈|prefix|, pc〉
674       ] in
675     let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in
676       〈add_instruction_size pc jmp_len instr, new_labels〉
677    ) 〈0, empty_map …〉 in
678    final_labels.
679[ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
680  [ #Hi #l normalize nodelta; cases label normalize nodelta
681    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
682      lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
683      % [ @addr | @Haddr ]
684    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
685      @eq_identifier_elim #Heq #Hocc
686      [ normalize in Hocc;
687        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
688        @⊥ @(absurd … Hocc)
689      | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
690        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
691        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
692        ]
693      ]
694      >(label_does_not_occur i … Hl) normalize nodelta @nmk //
695    ]
696  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
697    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
698      [ normalize nodelta #H @⊥ @H
699      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
700      ]
701    | @le_n
702    ]
703  ]
704| #i #Hi #l #Hl @⊥ @Hl
705]
706qed.
707
708definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
709  λlabels.λpc.λlbl.
710  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
711  if leb pc addr (* forward jump *)
712  then if leb (addr - pc) 126
713       then 〈addr, short_jump〉
714       else 〈addr, long_jump〉
715  else if leb (pc - addr) 129
716       then 〈addr, short_jump〉
717       else 〈addr, long_jump〉.
718
719definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
720  λlabels.λpc_nat.λlbl.
721  let pc ≝ bitvector_of_nat 16 pc_nat in
722  let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
723  let addr ≝ bitvector_of_nat 16 addr_nat in
724  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
725  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
726  if eq_bv ? fst_5_addr fst_5_pc
727  then 〈addr_nat, medium_jump〉
728  else 〈addr_nat, long_jump〉.
729 
730definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
731  λlabels.λpc.λlbl.
732  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
733  if leb pc addr
734  then if leb (addr - pc) 126
735       then 〈addr, short_jump〉
736       else select_call_length labels pc lbl
737  else if leb (pc - addr) 129
738       then 〈addr, short_jump〉
739       else select_call_length labels pc lbl.
740 
741definition jump_expansion_step_instruction: label_map → ℕ →
742  preinstruction Identifier → option (ℕ × jump_length) ≝
743  λlabels.λpc.λi.
744  match i with
745  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
746  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
747  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
748  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
749  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
750  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
751  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
752  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
753  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
754  | _        ⇒ None ?
755  ].
756
757definition is_jump' ≝
758  λx:preinstruction Identifier.
759  match x with
760  [ JC _ ⇒ True
761  | JNC _ ⇒ True
762  | JZ _ ⇒ True
763  | JNZ _ ⇒ True
764  | JB _ _ ⇒ True
765  | JNB _ _ ⇒ True
766  | JBC _ _ ⇒ True
767  | CJNE _ _ ⇒ True
768  | DJNZ _ _ ⇒ True
769  | _ ⇒ False
770  ].
771 
772definition is_jump ≝
773  λx:labelled_instruction.
774  let 〈label,instr〉 ≝ x in
775  match instr with
776  [ Instruction i   ⇒ is_jump' i
777  | Call _ ⇒ True
778  | Jmp _ ⇒ True
779  | _ ⇒ False
780  ].
781
782lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
783#x cases x #l #i cases i
784[#id cases id
785 [1,2,3,6,7,33,34:
786  #x #y %2 whd in match (is_jump ?); /2 by nmk/
787 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
788  #x %2 whd in match (is_jump ?); /2 by nmk/
789 |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
790 |9,10,14,15: #x %1 //
791 |11,12,13,16,17: #x #y %1 //
792 ]
793|2,3: #x %2 /2 by nmk/
794|4,5: #x %1 //
795|6: #x #y %2 /2 by nmk/
796]
797qed.
798 
799
800definition jump_in_policy ≝
801  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
802  ∀i:ℕ.i < |prefix| →
803  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
804   ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
805
806(* these should be moved to BitVector at some point *) 
807lemma bitvector_of_nat_ok:
808  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
809 #n elim n -n
810 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
811 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
812 ]
813qed.
814
815lemma bitvector_of_nat_abs:
816  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
817 #n #x #y #Hx #Hy #Heq @notb_elim
818 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
819 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
820 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H //
821 | #H //
822 ]
823qed.
824
825lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
826 ∀policy:(Σp:jump_expansion_policy.
827 (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
828 jump_in_policy prefix p).
829  ∀i:ℕ.i < |prefix| →
830  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
831  (lookup_opt … (bitvector_of_nat 16 i) policy = None ?).
832 #prefix #policy #i #Hi @conj
833 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
834   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
835   [ #H @H
836   | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
837     @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
838   ]
839 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
840   #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs)
841 ] 
842qed.
843
844definition jump_expansion_start:
845  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
846  Σpolicy:jump_expansion_policy.
847    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
848    jump_in_policy program policy ∧
849    ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
850     lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝
851  λprogram.
852  foldl_strong (option Identifier × pseudo_instruction)
853  (λprefix.Σpolicy:jump_expansion_policy.
854    (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
855    jump_in_policy prefix policy ∧
856    ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
857      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉)
858  program
859  (λprefix.λx.λtl.λprf.λpolicy.
860   let 〈label,instr〉 ≝ x in
861   match instr with
862   [ Instruction i ⇒ match i with
863     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
864     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
865     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
866     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
867     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
868     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
869     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
870     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
871     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
872     | _ ⇒ (pi1 … policy)
873     ]
874   | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
875   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
876   | _      ⇒ (pi1 ?? policy)
877   ]
878  ) (Stub ? ?).
879[1,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,35,36,37,38,39,40,41,42:
880 @conj
881 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
882  @conj
883  #i >append_length <commutative_plus #Hi normalize in Hi;
884  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
885   #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i)
886   [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121:
887     @le_S_to_le @le_S_to_le @Hi
888   |2,6,10,14,18,22,26,30,34,38,42,46,50,54,58,62,66,70,74,78,82,86,90,94,98,102,106,110,114,118,122:
889     @Hi2
890   |3,7,11,15,19,23,27,31,35,39,43,47,51,55,59,63,67,71,75,79,83,87,91,95,99,103,107,111,115,119,123:
891     <Hi @le_n_Sn
892   |4,8,12,16,20,24,28,32,36,40,44,48,52,56,60,64,68,72,76,80,84,88,92,96,100,104,108,112,116,120,124:
893     @Hi2
894   ]
895  ]
896  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
897  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
898    >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
899    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
900  ]
901  @conj >(injective_S … Hi)
902   [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
903    >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H
904   ]
905   #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H
906   >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
907   [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
908     #H destruct (H)
909   ]
910   @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
911   @le_plus_n_r
912 ]
913 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
914 -Hi; #Hi
915 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
916  #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
917  >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; //
918 ]
919 >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n
920 #H @⊥ @H
921|2,3,26,27,28,29,30,31,32,33,34: @conj
922 [1,3,5,7,9,11,13,15,17,19,21: @conj
923  [1,3,5,7,9,11,13,15,17,19,21:
924    #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
925   [1,3,5,7,9,11,13,15,17,19,21:
926     @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
927   ]
928   >eq_bv_sym @bitvector_of_nat_abs
929   [1,4,7,10,13,16,19,22,25,28,31:
930     @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
931     @le_plus_n_r
932   |2,5,8,11,14,17,20,23,26,29,32: @Hi2
933   |3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi
934   ]
935  ]
936  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
937  -Hi #Hi
938  [1,3,5,7,9,11,13,15,17,19,21:
939   >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
940   [1,3,5,7,9,11,13,15,17,19,21:
941    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
942   ]
943   @bitvector_of_nat_abs
944   [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
945   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
946   ]
947   @(transitive_lt … (pi2 ?? program))
948   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
949  ]
950  @conj >(injective_S … Hi) #H
951  [2,4,6,8,10,12,14,16,18,20,22:
952   >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n //
953  ]
954  @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
955 ]
956 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
957  -Hi #Hi
958 [1,3,5,7,9,11,13,15,17,19,21:
959  >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss
960  [1,3,5,7,9,11,13,15,17,19,21:
961   @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj)
962  ]
963  @bitvector_of_nat_abs
964  [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
965  |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
966  ]
967  @(transitive_lt … (pi2 ?? program))
968  >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
969 ]
970 #_ >(injective_S … Hi) @lookup_opt_insert_hit
971|@conj
972 [@conj
973  [ #i #Hi //
974  | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
975  ]
976 | #i #Hi >nth_nil #Hj @⊥ @Hj
977]
978qed.
979
980definition policy_increase: list labelled_instruction → jump_expansion_policy →
981  jump_expansion_policy → Prop ≝
982 λprogram.λop.λp.
983  (∀i:ℕ.i < |program| →
984    let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
985    let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in
986    jmpleq oj j).
987
988definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝
989 (*λlabels.*)λpolicy.
990 bvt_forall (ℕ×ℕ×jump_length) 16 policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
991    match jmp_len with
992    [ short_jump  ⇒ if leb pc_nat addr_nat
993       then le (addr_nat - pc_nat) 126
994       else le (pc_nat - addr_nat) 129
995    | medium_jump ⇒
996       let addr ≝ bitvector_of_nat 16 addr_nat in
997       let pc ≝ bitvector_of_nat 16 pc_nat in
998       let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
999       let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
1000       eq_bv 5 fst_5_addr fst_5_pc = true
1001    | long_jump   ⇒ True
1002    ]
1003  ).
1004 
1005definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1006  ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
1007    ∀l.occurs_exactly_once l program →
1008    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
1009    ∃a.lookup … lm l = Some ? 〈i,a〉).
1010  ∀old_policy:(Σpolicy.
1011    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
1012    jump_in_policy program policy).
1013  (Σpolicy.
1014    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
1015    jump_in_policy program policy ∧
1016    policy_increase program old_policy policy)
1017    ≝
1018  λprogram.λlabels.λold_policy.
1019  let 〈final_pc, final_policy〉 ≝
1020    foldl_strong (option Identifier × pseudo_instruction)
1021    (λprefix.ℕ × Σpolicy.
1022      (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
1023      jump_in_policy prefix policy ∧
1024      policy_increase prefix old_policy policy
1025    )
1026    program
1027    (λprefix.λx.λtl.λprf.λacc.
1028      let 〈pc, policy〉 ≝ acc in
1029      let 〈label,instr〉 ≝ x in
1030      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in
1031      let add_instr ≝
1032        match instr with
1033        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
1034        | Call c        ⇒ Some ? (select_call_length labels pc c)
1035        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
1036        | _             ⇒ None ?
1037        ] in
1038      let 〈new_pc, new_policy〉 ≝
1039        let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
1040        match add_instr with
1041        [ None    ⇒ (* i.e. it's not a jump *)
1042          〈add_instruction_size pc long_jump instr, policy〉
1043        | Some z ⇒ let 〈addr,ai〉 ≝ z in
1044          let new_length ≝ max_length old_length ai in
1045          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
1046        ] in
1047      〈new_pc, new_policy〉
1048    ) 〈0, Stub ? ?〉 in
1049    final_policy.
1050[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
1051[ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
1052  [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
1053  | #z cases z -z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss
1054    [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
1055    | >eq_bv_sym @bitvector_of_nat_abs
1056      [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1057        @le_S_S @le_plus_n_r
1058      | @Hi2
1059      | @lt_to_not_eq @Hi
1060      ]
1061    ]
1062  ]
1063| cases (le_to_or_lt_eq … Hi) -Hi;
1064  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
1065    [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
1066      cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
1067      [ @(proj1 ?? Hacc Hj)
1068      | #z cases z -z #z1 #z2 elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
1069        @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
1070        >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
1071        [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
1072        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
1073        ]
1074        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1075        @le_S_S @le_plus_n_r
1076      ]
1077    | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
1078      #H elim H -H; #h #H elim H -H; #n #H elim H -H #j cases add_instr cases (lookup ??? old_policy ?)
1079      normalize nodelta #x #y [2: #z]
1080      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
1081      [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @lookup_opt_insert_miss @bitvector_of_nat_abs
1082        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
1083        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
1084        ]
1085        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1086        @le_S_S @le_plus_n_r
1087      | @Hl
1088      ]
1089    ]
1090  | #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
1091     <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr
1092     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
1093     [3,5,11: #H @⊥ @H (* instr is not a jump *)
1094     |4,6,12: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
1095       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
1096       [1,3,5: #H destruct (H)]
1097       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1098       @le_S_S @le_plus_n_r
1099     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
1100       whd in match (snd ???); @(ex_intro ?? pc)
1101       [ @(ex_intro ?? (\fst (select_jump_length labels pc id)))
1102         @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id))))
1103         cases (select_jump_length labels pc id)
1104       | @(ex_intro ?? (\fst (select_call_length labels pc id)))
1105         @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id))))
1106         cases (select_call_length labels pc id)
1107       ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit
1108     |8,10: #_ //
1109     |1,2: cases pi
1110       [35,36,37: #H @⊥ @H
1111       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
1112       |1,2,3,6,7,33,34: #x #y #H @⊥ @H
1113       |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
1114         whd in match (snd ???); @(ex_intro ?? pc)
1115         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
1116         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
1117         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
1118         @lookup_opt_insert_hit
1119       |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
1120         whd in match (snd ???); @(ex_intro ?? pc)
1121         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
1122         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
1123         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
1124         @lookup_opt_insert_hit
1125       |72,73,74: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
1126        #z cases z -z #x #y #z normalize nodelta
1127        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
1128        [1,3,5: #H destruct (H)]
1129        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1130        @le_S_S @le_plus_n_r     
1131       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
1132        #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
1133        #z cases z -z #x #y #z normalize nodelta
1134        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
1135        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
1136        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1137        @le_S_S @le_plus_n_r
1138       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n #H elim H -H #j
1139        cases (lookup ??? old_policy ?) #z cases z -z #x #y #z normalize nodelta
1140        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
1141        [1,3,5,7,9,11,13: #H destruct (H)]
1142        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1143        @le_S_S @le_plus_n_r             
1144       |46,47,51,52: #id #_ //
1145       |48,49,50,53,54: #x #id #_ //
1146       ]
1147     ]
1148   ]
1149  ]
1150| lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %);
1151  [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
1152    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
1153    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
1154      #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
1155    | normalize nodelta >(injective_S … Hi)
1156      >lookup_opt_lookup_miss
1157      [ >lookup_opt_lookup_miss
1158        [ //
1159        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
1160          #x #y normalize nodelta
1161          >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
1162          [ //
1163          | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1164            @le_S_S @le_plus_n_r
1165          ]
1166        ]
1167      | >(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?))
1168        [ //
1169        | >prf >p1 >nth_append_second [ <minus_n_n
1170        generalize in match Ha; normalize nodelta cases instr normalize nodelta
1171        [1: #pi cases pi
1172         [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/
1173         |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/
1174         |35,36,37: #H normalize /2 by nmk/
1175         |9,10,14,15: #id whd in match (jump_expansion_step_instruction ???);
1176           #H destruct (H)
1177         |11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???);
1178           #H destruct (H)
1179         ]
1180        |2,3: #x #H normalize /2 by nmk/
1181        |6: #x #y #H normalize /2 by nmk/
1182        |4,5: #id #H destruct (H)
1183        ] | @le_n ]
1184        | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
1185        ]
1186      ]
1187    ]
1188  | #x cases x -x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
1189    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
1190    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
1191      #y cases y -y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss
1192      [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
1193      | @bitvector_of_nat_abs
1194        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
1195        |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
1196        ]
1197        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1198        @le_S_S @le_plus_n_r
1199      ]
1200    | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
1201      [ #a #H elim H -H; #b #H elim H -H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H)
1202        normalize nodelta >lookup_insert_hit @jmpleq_max_length
1203      | >prf >p1 >nth_append_second
1204        [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta
1205          [1: #pi cases pi
1206           [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H)
1207           |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize in H; destruct (H)
1208           |35,36,37: #H normalize in H; destruct (H)
1209           |9,10,14,15: #id #H //
1210           |11,12,13,16,17: #x #id #H //
1211           ]
1212          |2,3: #x #H normalize in H; destruct (H)
1213          |6: #x #y #H normalize in H; destruct (H)
1214          |4,5: #id #H //
1215          ]
1216        | @le_n ]
1217      | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
1218      ]
1219    ]
1220  ] ]
1221| @conj [ @conj
1222  [ #i #Hi //
1223  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
1224                   normalize in H3; destruct (H3) ]
1225  ]                 
1226  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
1227]
1228qed.
1229 
1230let rec jump_expansion_internal (program: Σl:list labelled_instruction.|l| < 2^16)
1231  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.
1232    And
1233    (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
1234    (jump_in_policy program policy)) ≝
1235  match n with
1236  [ O   ⇒ jump_expansion_start program
1237  | S m ⇒ let old_policy ≝ jump_expansion_internal program m in
1238    jump_expansion_step program (create_label_map program old_policy) old_policy
1239  ].
1240[ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
1241| @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy)))
1242]
1243qed.
1244
1245definition policy_equal ≝
1246  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
1247  ∀n:ℕ.n < |program| →
1248    let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
1249    let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
1250    j1 = j2.
1251
1252lemma pe_refl:
1253  ∀program.reflexive ? (policy_equal program).
1254 #program whd #x whd #n #Hn cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
1255 #y cases y -y #y #z normalize nodelta @refl
1256qed.
1257
1258lemma pe_sym:
1259  ∀program.symmetric ? (policy_equal program).
1260 #program whd #x #y #Hxy whd #n #Hn
1261 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
1262 #z cases z -z #x1 #x2 #x3 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
1263 #z cases z -z #y1 #y2 #y3 normalize nodelta //
1264qed.
1265
1266lemma pe_trans:
1267  ∀program.transitive ? (policy_equal program).
1268 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
1269 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn
1270 lapply (Hxy n Hn) -Hxy lapply (Hyz n Hn) -Hyz
1271 cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
1272 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
1273 cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z #z1 #z2 #z3
1274 normalize nodelta //
1275qed.
1276
1277lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1278 ∀p1,p2:Σpolicy.
1279 (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
1280 ∧jump_in_policy program policy.
1281  policy_equal program p1 p2 →
1282  policy_equal program (jump_expansion_step program (create_label_map program p1) p1)
1283    (jump_expansion_step program (create_label_map program p2) p2).
1284 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
1285 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
1286 cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?);
1287 [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl)
1288   #Hnotjmp >lookup_opt_lookup_miss
1289   [ >lookup_opt_lookup_miss
1290     [ @refl
1291     | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn))
1292       [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2)))
1293       | @Hnotjmp
1294       ]
1295     ]
1296   | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn))
1297     [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1)))
1298     | @Hnotjmp
1299     ]
1300   ]
1301 | #x #Hl cases daemon (* XXX *)
1302 ]
1303qed.
1304
1305(* this is in the stdlib, but commented out, why? *)
1306theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
1307  #n (elim n) normalize /2 by S_pred/ qed.
1308
1309lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
1310  policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
1311  ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
1312 #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
1313 lapply Heq -Heq; lapply n -n; elim z -z;
1314 [ #n #Heq <plus_n_O @pe_refl 
1315 | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n)))
1316   [ @Heq
1317   | @pe_step @Hind @Heq
1318   ]
1319 ]
1320qed.
1321
1322lemma thingie:
1323  ∀A:Prop.(A + ¬A) → (¬¬A) → A.
1324 #A #Adec #nnA cases Adec
1325 [ //
1326 | #H @⊥ @(absurd (¬A) H nnA)
1327 ]
1328qed.
1329 
1330lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
1331 ∀policy:(Σp:jump_expansion_policy.
1332    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1333    jump_in_policy program p).
1334  ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) →
1335  ∃n:ℕ.n < (|program|) ∧ jmple
1336    (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
1337    (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)).
1338 #program #policy #Hp
1339 cases (dec_bounded_exists (λn.jmple
1340   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
1341   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (|program|))
1342 [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
1343 | #abs @⊥ @(absurd ?? Hp) #n #Hn
1344   lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn)
1345   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
1346   cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %);
1347   #z cases z -z #x1 #x2 #x3 #Hx
1348   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))
1349   cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %);
1350   #z cases z -z #y1 #y2 #y3 #Hy
1351   normalize nodelta #Hj cases Hj
1352   [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | >Hx >Hy @Hj ]
1353   | //
1354   ]
1355 | #n @dec_jmple
1356 ]
1357qed.
1358
1359lemma stupid:
1360  ∀program,n.
1361  pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) =
1362  pi1 … (jump_expansion_internal program (S n)).
1363 //
1364qed.
1365
1366let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
1367 on program: ℕ ≝
1368 match program with
1369 [ nil      ⇒ acc
1370 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) with
1371   [ long_jump   ⇒ measure_int t policy (acc + 2)
1372   | medium_jump ⇒ measure_int t policy (acc + 1)
1373   | _           ⇒ measure_int t policy acc
1374   ]
1375 ].
1376
1377(* definition measure ≝
1378  λprogram.λpolicy.measure_int program policy 0. *)
1379 
1380lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
1381  measure_int program policy (x+d) = measure_int program policy x + d.
1382 #program #policy #x #d generalize in match x; -x elim d
1383 [ //
1384 | -d; #d #Hind elim program
1385   [ //
1386   | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
1387     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
1388     [ normalize nodelta @Hd
1389     |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
1390       @Hd
1391     ]
1392   ]
1393 ]
1394qed.
1395   
1396lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
1397  ∀policy:Σp:jump_expansion_policy.
1398    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1399    jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ.
1400  measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc.
1401#program #policy #l elim l -l;
1402  [ #Hp #acc normalize @le_n
1403  | #h #t #Hind #Hp #acc
1404    lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) Hp)
1405    whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?);
1406    cases (bvt_lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
1407    cases (bvt_lookup … (bitvector_of_nat ? (|t|)) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
1408    normalize nodelta #Hj cases Hj
1409    [ cases x3 cases y3
1410      [1,4,5,7,8,9: #H @⊥ @H
1411      |2,3,6: #_ normalize nodelta
1412        [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) acc))
1413        |3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) (acc+1)))
1414        ]
1415        [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn
1416        |2,4,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus [ @le_n | //]
1417        ]
1418      ]
1419    | #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
1420    ]
1421  ]
1422qed.
1423
1424lemma measure_le: ∀program.∀policy.
1425  measure_int program policy 0 ≤ 2*|program|.
1426 #program #policy elim program
1427 [ normalize @le_n
1428 | #h #t #Hind whd in match (measure_int ???);
1429   cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
1430   [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
1431   |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
1432     @le_plus [1,3: @Hind |2,4: // ]
1433   ]
1434 ]
1435qed.
1436
1437(* these lemmas seem superfluous, but not sure how *)
1438lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
1439 #a elim a
1440 [ normalize #b //
1441 | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
1442   <plus_n_Sm <plus_n_Sm #H
1443   >(Hind b (injective_S ?? (injective_S ?? H))) // ]
1444 ]
1445qed.
1446
1447lemma sth_not_s: ∀x.x ≠ S x.
1448 #x cases x
1449 [ // | #y // ]
1450qed.
1451
1452lemma measure_full: ∀program.∀policy.
1453  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
1454  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
1455 #program #policy elim program
1456 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1457 | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
1458   [ whd in match (measure_int ???) in Hm;
1459     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
1460     normalize nodelta
1461     [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
1462     | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
1463       <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
1464       >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
1465       >plus_n_Sm @le_n
1466     | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
1467     ]
1468   | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
1469   [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
1470   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1471     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
1472     normalize nodelta
1473     [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
1474       >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
1475     | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
1476       #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
1477     | #_ //
1478     ]
1479   ]]
1480 ]
1481qed.
1482
1483lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1484  ∀policy:Σp:jump_expansion_policy.
1485    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1486    jump_in_policy program p.
1487  measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 →
1488  policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy).
1489#program #policy lapply (le_n (|program|)) @(list_ind ?
1490  (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 →
1491      policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy)))
1492   ?? program)
1493 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
1494 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
1495   [ #Hi @Hind
1496     [ @(transitive_le … Hp) //
1497     | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
1498       lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
1499       [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
1500       | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
1501         #x cases x -x #x1 #x2 #x3
1502         cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
1503         #y cases y -y #y1 #y2 #y3
1504         normalize nodelta cases x3 cases y3 normalize nodelta
1505         [1: #H #_ @H
1506         |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1507           @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1508         |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
1509         |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
1510           #H #_ @(injective_plus_r … H)
1511         |6: >measure_plus >measure_plus
1512            change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1513            #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1514            @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1515         |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
1516           #H #_ @(injective_plus_r … H)
1517         ]
1518       ]
1519     | @(le_S_S_to_le … Hi)
1520     ]
1521   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 
1522     whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
1523     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
1524     [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
1525     | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
1526       #x cases x -x #x1 #x2 #x3
1527       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
1528       #y cases y -y #y1 #y2 #y3
1529       normalize nodelta cases x3 cases y3 normalize nodelta
1530       [1,5,9: #_ #_ //
1531       |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
1532       |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1533         @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1534       |6: >measure_plus >measure_plus
1535          change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1536          #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1537          @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1538       ]
1539     ]
1540   ]
1541 ] 
1542qed.
1543
1544lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
1545  |l| ≤ |program| → measure_int l (jump_expansion_internal program 0) 0 = 0.
1546 #l #program elim l
1547 [ //
1548 | #h #t #Hind #Hp whd in match (measure_int ???);
1549   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
1550   [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉)
1551     [ normalize nodelta @Hind @le_S_to_le ]
1552     @Hp
1553   | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,0,short_jump〉)
1554     [ normalize nodelta @Hind @le_S_to_le ]
1555     @Hp
1556   ]
1557 ]
1558qed.
1559 
1560definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1561  Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
1562 #program @(mk_Sig … (jump_expansion_internal program (2*|program|)))
1563 @(ex_intro … (2*|program|)) #k #Hk
1564 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
1565   (jump_expansion_internal program (S k))) ? (2*|program|))
1566 [ #H elim H -H #x #Hx @pe_trans
1567   [ @(jump_expansion_internal program x)
1568   | @pe_sym @equal_remains_equal
1569     [ @(proj2 ?? Hx)
1570     | @(transitive_le ? (2*|program|))
1571       [ @le_S_S_to_le @le_S @(proj1 ?? Hx)
1572       | @le_S_S_to_le @le_S @Hk
1573       ]
1574     ]
1575   | @equal_remains_equal
1576     [ @(proj2 ?? Hx)
1577     | @le_S_S_to_le @le_S @(proj1 ?? Hx)
1578     ]
1579   ]
1580 | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @pe_sym @equal_remains_equal
1581   [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
1582     #Hfull #i #Hi
1583     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program (jump_expansion_internal program (2*|program|))) (jump_expansion_internal program (2*|program|)))) i Hi)
1584     lapply (Hfull ? i Hi)
1585     [ -i @le_to_le_to_eq
1586       [ @measure_le
1587       | lapply (le_n (2*|program|)) elim (2*|program|) in ⊢ (?%? → %);
1588         [ #_ >measure_zero @le_n
1589         | #x #Hind #Hx
1590           cut (measure_int program (jump_expansion_internal program x) 0 <
1591                measure_int program (jump_expansion_internal program (S x)) 0)
1592           [ elim (le_to_or_lt_eq …
1593               (measure_incr_or_equal program (jump_expansion_internal program x) program (le_n (|program|)) 0))
1594             [ //
1595             | #H @⊥ @(absurd ?? (Hfa x Hx)) @measure_special @H
1596             ]
1597           | #H lapply (Hind (le_S_to_le … Hx)) #H2 @(le_to_lt_to_lt … H) @H2
1598           ]
1599         ]
1600       ]
1601     | -Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*|program|)) 〈0,0,short_jump〉)
1602       #x cases x -x #x1 #x2 #x3 normalize nodelta #Hfull
1603       >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉)
1604       #y cases y -y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta 
1605       [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
1606       | #_ //
1607       ]
1608     ]
1609   | @le_S_to_le @Hk
1610   ]
1611 | #n @dec_bounded_forall #m
1612   cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
1613   #x cases x -x #x1 #x2 #x3
1614   cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
1615   #y cases y -y #y1 #y2 #y3 normalize nodelta
1616   @dec_eq_jump_length
1617 ]
1618qed.
1619
1620let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n:
1621  BitVectorTrie jump_length 16 ≝
1622  match n with
1623  [ O    ⇒ acc
1624  | S n' ⇒
1625    match lookup_opt … (bitvector_of_nat 16 n') policy with
1626    [ None   ⇒ transform_policy n' policy acc
1627    | Some x ⇒ let 〈pc,length〉 ≝ x in
1628      transform_policy n' policy (insert … pc length acc)
1629    ]
1630  ].
1631
1632(**************************************** START OF POLICY ABSTRACTION ********************)
1633
1634definition policy_type ≝ Word → jump_length.
1635
1636definition jump_expansion':
1637 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
1638 policy_type ≝
1639 λprogram.λpc.
1640  let policy ≝
1641    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
1642  lookup ? ? pc policy long_jump.
1643/2 by Stub, mk_Sig/
1644qed.
1645
1646definition assembly_1_pseudoinstruction_safe ≝
1647  λprogram: pseudo_assembly_program.
1648  λjump_expansion: policy_type.
1649  λppc: Word.
1650  λpc: Word.
1651  λlookup_labels.
1652  λlookup_datalabels.
1653  λi.
1654  let expansion ≝ jump_expansion ppc in
1655    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
1656    [ None ⇒ None ?
1657    | Some pseudos ⇒
1658      let mapped ≝ map ? ? assembly1 pseudos in
1659      let flattened ≝ flatten ? mapped in
1660      let pc_len ≝ length ? flattened in
1661        Some ? (〈pc_len, flattened〉)
1662    ].
1663 
1664definition construct_costs_safe ≝
1665  λprogram.
1666  λjump_expansion: policy_type.
1667  λpseudo_program_counter: nat.
1668  λprogram_counter: nat.
1669  λcosts: BitVectorTrie costlabel 16.
1670  λi.
1671  match i with
1672  [ Cost cost ⇒
1673    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1674      Some ? 〈program_counter, (insert … program_counter_bv cost costs)〉
1675  | _ ⇒
1676    let pc_bv ≝ bitvector_of_nat ? program_counter in
1677    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
1678    let lookup_labels ≝ λx.pc_bv in
1679    let lookup_datalabels ≝ λx.zero ? in
1680    let pc_delta_assembled ≝
1681      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
1682        lookup_labels lookup_datalabels i
1683    in
1684    match pc_delta_assembled with
1685    [ None ⇒ None ?
1686    | Some pc_delta_assembled ⇒
1687      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
1688        Some ? 〈pc_delta + program_counter, costs〉       
1689    ]
1690  ].
1691
1692(* This establishes the correspondence between pseudo program counters and
1693   program counters. It is at the heart of the proof. *)
1694(*CSC: code taken from build_maps *)
1695definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
1696 λinstr_list.
1697 λjump_expansion: policy_type.
1698 λl:list labelled_instruction.
1699 λacc.
1700  foldl …
1701   (λt,i.
1702       match t with
1703       [ None ⇒ None …
1704       | Some ppc_pc_map ⇒
1705         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1706         let 〈program_counter, sigma_map〉 ≝ pc_map in
1707         let 〈label, i〉 ≝ i in
1708          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
1709           [ None ⇒ None ?
1710           | Some pc_ignore ⇒
1711              let 〈pc,ignore〉 ≝ pc_ignore in
1712                Some … 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ]
1713       ]) acc l.
1714
1715definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) ≝
1716  λprog.
1717  λjump_expansion.
1718    sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, Stub …〉〉).
1719
1720definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
1721 λprogram,jump_expansion,instr_list.
1722  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
1723   [ None ⇒ None …
1724   | Some result ⇒
1725      let 〈ppc,pc_sigma_map〉 ≝ result in
1726      let 〈pc,map〉 ≝ pc_sigma_map in
1727       Some … 〈ppc,pc〉 ].
1728
1729definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
1730 λinstr_list,jump_expansion.
1731  match sigma0 instr_list jump_expansion with
1732  [ None ⇒ None ?
1733  | Some result ⇒
1734    let 〈ppc,pc_sigma_map〉 ≝ result in
1735    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
1736      if gtb pc (2^16) then
1737        None ?
1738      else
1739        Some ? (λx. lookup … x sigma_map (zero …)) ].
1740
1741(* stuff about policy *)
1742
1743definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
1744
1745definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
1746
1747lemma eject_policy: ∀p. policy p → policy_type.
1748 #p #pol @(pi1 … pol)
1749qed.
1750
1751coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
1752
1753definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
1754 λp,policy.
1755  match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
1756   [ None ⇒ λabs. ⊥
1757   | Some r ⇒ λ_.r] (pi2 … policy).
1758 cases abs /2/
1759qed.
1760
1761example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
1762 cases daemon.
1763qed.
1764
1765axiom fetch_pseudo_instruction_split:
1766 ∀instr_list,ppc.
1767  ∃pre,suff,lbl.
1768   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
1769
1770lemma sigma00_append:
1771 ∀instr_list,jump_expansion,l1,l2,acc.
1772  sigma00 instr_list jump_expansion (l1@l2) acc =
1773   sigma00 instr_list jump_expansion
1774    l2 (sigma00 instr_list jump_expansion l1 acc).
1775 whd in match sigma00; normalize nodelta;
1776 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
1777qed.
1778
1779lemma sigma00_strict:
1780 ∀instr_list,jump_expansion,l,acc. acc = None ? →
1781  sigma00 instr_list jump_expansion l acc = None ….
1782 #instr_list #jump_expansion #l elim l
1783  [ #acc #H >H %
1784  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
1785qed.
1786
1787lemma policy_ok_prefix_ok:
1788 ∀program.∀pol:policy program.∀suffix,prefix.
1789  prefix@suffix = \snd program →
1790   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
1791 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
1792 generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol
1793 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
1794 normalize nodelta >sigma00_append
1795 cases (sigma00 ?? prefix ?)
1796  [2: #x #_ % #abs destruct(abs)
1797  | * #abs @⊥ @abs >sigma00_strict % ]
1798qed.
1799
1800lemma policy_ok_prefix_hd_ok:
1801 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
1802  (prefix@[hd])@suffix = \snd program →
1803   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
1804    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1805    let 〈program_counter, sigma_map〉 ≝ pc_map in
1806    let 〈label, i〉 ≝ hd in
1807     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
1808 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
1809 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
1810  (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
1811 @pair_elim #ppc #pc_map #EQ3 normalize nodelta
1812 @pair_elim #pc #map #EQ4 normalize nodelta
1813 @pair_elim #l' #i' #EQ5 normalize nodelta
1814 cases (construct_costs_safe ??????) normalize
1815  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
1816qed.
1817
1818definition expand_pseudo_instruction:
1819 ∀program:pseudo_assembly_program.∀pol: policy program.
1820  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
1821  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1822  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1823  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
1824  pc = sigma program pol ppc →
1825  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
1826≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
1827   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
1828    [ None ⇒ let dummy ≝ [ ] in dummy
1829    | Some res ⇒ res ].
1830 [ @⊥ whd in p:(??%??);
1831   generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);
1832   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
1833   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
1834   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
1835   #res #K
1836   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
1837   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
1838   cases daemon (* CSC: XXXXXXXX Ero qui
1839   
1840    [3: @policy_ok_prefix_ok ]
1841    | sigma00 program pol pre
1842
1843
1844
1845   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
1846   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
1847   per concludere construct_costs_safe ≠ None *)
1848 | >p %]
1849qed.
1850
1851(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1852definition assembly_1_pseudoinstruction':
1853 ∀program:pseudo_assembly_program.∀pol: policy program.
1854  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1855  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1856  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1857  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1858  Σres:(nat × (list Byte)).
1859   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
1860   let 〈len,code〉 ≝ res in
1861    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
1862     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
1863≝ λprogram: pseudo_assembly_program.
1864  λpol: policy program.
1865  λppc: Word.
1866  λlookup_labels.
1867  λlookup_datalabels.
1868  λpi.
1869  λprf1,prf2,prf3.
1870   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
1871    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
1872    | Some res ⇒ res ].
1873 [ @⊥ elim pi in p; [*]
1874   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
1875   generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
1876   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
1877   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
1878   cases daemon
1879 | % [ >p %]
1880   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
1881   (* THIS SHOULD BE TRUE INSTEAD *)
1882   cases daemon]
1883qed.
1884
1885definition assembly_1_pseudoinstruction:
1886 ∀program:pseudo_assembly_program.∀pol: policy program.
1887  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1888  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1889  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1890  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1891   nat × (list Byte)
1892≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
1893   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
1894    prf2 prf3.
1895
1896lemma assembly_1_pseudoinstruction_ok1:
1897 ∀program:pseudo_assembly_program.∀pol: policy program.
1898  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1899  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
1900  ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
1901  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
1902     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
1903   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
1904 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
1905 cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
1906 #H1 #_ @H1
1907qed.
1908
1909(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1910definition construct_costs':
1911 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
1912  Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
1913
1914  λprogram.λpol: policy program.λppc,pc,costs,i.
1915   match construct_costs_safe program pol ppc pc costs i with
1916    [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
1917    | Some res ⇒ res ].
1918 [ cases daemon
1919 | >p %]
1920qed.
1921
1922definition construct_costs ≝
1923 λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i).
1924
1925(*
1926axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
1927axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
1928
1929axiom foldl_strong_step:
1930 ∀A:Type[0].
1931  ∀P: list A → Type[0].
1932   ∀l: list A.
1933    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
1934     ∀acc: P [ ].
1935      ∀Q: ∀prefix. P prefix → Prop.
1936       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
1937        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
1938       Q [ ] acc →
1939        Q l (foldl_strong A P l H acc).
1940(*
1941 #A #P #l #H #acc #Q #HQ #Hacc normalize;
1942 generalize in match
1943  (foldl_strong ?
1944   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
1945   l ? Hacc)
1946 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
1947 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
1948 #K
1949
1950 generalize in match
1951  (foldl_strong ?
1952   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
1953 [2: @H
1954*)
1955
1956axiom foldl_elim:
1957 ∀A:Type[0].
1958  ∀B: Type[0].
1959   ∀H: A → B → A.
1960    ∀acc: A.
1961     ∀l: list B.
1962      ∀Q: A → Prop.
1963       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
1964         Q acc →
1965          Q (foldl A B H acc l).
1966*)
1967
1968lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1969 #A #a #b #EQ destruct //
1970qed.
1971
1972(*
1973lemma tech_pc_sigma00_append_Some:
1974 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1975  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1976   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1977 #program #pol #prefix #costs #label #i #ppc #pc #H
1978  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
1979  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
1980  generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
1981  whd in match sigma0; normalize nodelta;
1982  >foldl_step
1983  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
1984  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
1985  cases (sigma00 program pol prefix) in H ⊢ %
1986   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
1987   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
1988     
1989     normalize nodelta; -H;
1990     
1991 
1992   generalize in match H; -H;
1993  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
1994   [2: whd in ⊢ (??%%)
1995XXX
1996*)
1997
1998axiom construct_costs_sigma:
1999 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
2000  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
2001   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
2002
2003axiom tech_pc_sigma00_append_Some:
2004 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
2005  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
2006   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
2007
2008axiom eq_identifier_eq:
2009  ∀tag: String.
2010  ∀l.
2011  ∀r.
2012    eq_identifier tag l r = true → l = r.
2013
2014axiom neq_identifier_neq:
2015  ∀tag: String.
2016  ∀l, r: identifier tag.
2017    eq_identifier tag l r = false → (l = r → False).
2018
2019definition build_maps:
2020 ∀pseudo_program.∀pol:policy pseudo_program.
2021  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
2022   let 〈labels, costs〉 ≝ res in
2023    ∀id. occurs_exactly_once id (\snd pseudo_program) →
2024     lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
2025  λpseudo_program.
2026  λpol:policy pseudo_program.
2027    let result ≝
2028      foldl_strong
2029        (option Identifier × pseudo_instruction)
2030          (λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))).
2031            let 〈labels,ppc_pc_costs〉 ≝ res in
2032            let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
2033            let 〈pc',costs〉 ≝ pc_costs in
2034              And ( And (
2035              And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
2036                (ppc' = length … pre)) (*∧ *)
2037                (tech_pc_sigma00 pseudo_program (pi1 … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
2038                (∀id. occurs_exactly_once id pre →
2039                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
2040                (\snd pseudo_program)
2041        (λprefix,i,tl,prf,t.
2042          let 〈labels, ppc_pc_costs〉 ≝ t in
2043          let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
2044          let 〈pc,costs〉 ≝ pc_costs in
2045          let 〈label, i'〉 ≝ i in
2046          let labels ≝
2047            match label with
2048            [ None ⇒ labels
2049            | Some label ⇒
2050                let program_counter_bv ≝ bitvector_of_nat ? pc in
2051                  add ? ? labels label program_counter_bv
2052            ]
2053          in
2054            let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
2055              〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
2056    in
2057      let 〈labels, ppc_pc_costs〉 ≝ result in
2058      let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
2059      let 〈pc, costs〉 ≝ pc_costs in
2060        〈labels, costs〉.
2061 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
2062   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
2063   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
2064   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
2065   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
2066   | #id normalize nodelta; -labels1; cases label; normalize nodelta
2067     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
2068     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
2069       generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
2070        [ #EQ #_ <(eq_identifier_eq … EQ) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit
2071          <IH0 [@IHn1 | <(eq_identifier_eq … EQ) in H; #H @H]
2072        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: -IHn1;
2073          (*Andrea:XXXX used to work /2/*)@nmk #IDL lapply (sym_eq ? ? ? IDL)
2074          lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ]
2075          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
2076 |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ]
2077 | generalize in match (pi2 … result) in ⊢ ?;
2078   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
2079   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
2080qed.
2081
2082definition assembly:
2083 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝
2084  λp.let 〈preamble, instr_list〉 ≝ p in
2085   λpol.
2086    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
2087    let datalabels ≝ construct_datalabels preamble in
2088    let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in
2089    let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
2090    let result ≝
2091     foldl_strong
2092      (option Identifier × pseudo_instruction)
2093      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
2094        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
2095        let 〈ppc,code〉 ≝ ppc_code in
2096         ∀ppc'.
2097          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
2098          let 〈len,assembledi〉 ≝
2099           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
2100           True)
2101      instr_list
2102      (λprefix,hd,tl,prf,pc_ppc_code.
2103        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
2104        let 〈ppc, code〉 ≝ ppc_code in
2105        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
2106        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
2107        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
2108         〈new_pc, 〈new_ppc, (code @ program)〉〉)
2109      〈(zero ?), 〈(zero ?), [ ]〉〉
2110    in
2111     〈\snd (\snd result), costs〉.
2112 [2,5: %
2113 |*: cases daemon ]
2114qed.
2115
2116definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
2117 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.