source: src/ASM/Assembly.ma @ 1613

Last change on this file since 1613 was 1613, checked in by sacerdot, 8 years ago

Coercion moved to Matita standard lib.

File size: 95.1 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
642definition create_label_map: ∀program:list labelled_instruction.
643  ∀policy:jump_expansion_policy.
644  (Σlabels:label_map.
645    ∀i:ℕ.lt i (|program|) →
646    ∀l.occurs_exactly_once l program →
647    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
648    ∃a.lookup … labels l = Some ? 〈i,a〉
649  ) ≝
650  λprogram.λpolicy.
651  let 〈final_pc, final_labels〉 ≝
652    foldl_strong (option Identifier × pseudo_instruction)
653    (λprefix.ℕ × (Σlabels.
654      ∀i:ℕ.lt i (|prefix|) →
655      ∀l.occurs_exactly_once l prefix →
656      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
657      ∃a.lookup … labels l = Some ? 〈i,a〉)
658    )
659    program
660    (λprefix.λx.λtl.λprf.λacc.
661     let 〈pc,labels〉 ≝ acc in
662     let 〈label,instr〉 ≝ x in
663       let new_labels ≝
664       match label with
665       [ None   ⇒ labels
666       | Some l ⇒ add … labels l 〈|prefix|, pc〉
667       ] in
668     let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in
669       〈add_instruction_size pc jmp_len instr, new_labels〉
670    ) 〈0, empty_map …〉 in
671    final_labels.
672[ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
673  [ #Hi #l normalize nodelta; cases label normalize nodelta
674    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
675      lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
676      % [ @addr | @Haddr ]
677    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
678      @eq_identifier_elim #Heq #Hocc
679      [ normalize in Hocc;
680        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
681        @⊥ @(absurd … Hocc)
682      | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
683        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
684        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
685        ]
686      ]
687      >(label_does_not_occur i … Hl) normalize nodelta @nmk //
688    ]
689  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
690    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
691      [ normalize nodelta #H @⊥ @H
692      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
693      ]
694    | @le_n
695    ]
696  ]
697| #i #Hi #l #Hl @⊥ @Hl
698]
699qed.
700
701definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
702  λlabels.λpc.λlbl.
703  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
704  if leb pc addr (* forward jump *)
705  then if leb (addr - pc) 126
706       then 〈addr, short_jump〉
707       else 〈addr, long_jump〉
708  else if leb (pc - addr) 129
709       then 〈addr, short_jump〉
710       else 〈addr, long_jump〉.
711
712definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
713  λlabels.λpc_nat.λlbl.
714  let pc ≝ bitvector_of_nat 16 pc_nat in
715  let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
716  let addr ≝ bitvector_of_nat 16 addr_nat in
717  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
718  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
719  if eq_bv ? fst_5_addr fst_5_pc
720  then 〈addr_nat, medium_jump〉
721  else 〈addr_nat, long_jump〉.
722 
723definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
724  λlabels.λpc.λlbl.
725  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
726  if leb pc addr
727  then if leb (addr - pc) 126
728       then 〈addr, short_jump〉
729       else select_call_length labels pc lbl
730  else if leb (pc - addr) 129
731       then 〈addr, short_jump〉
732       else select_call_length labels pc lbl.
733 
734definition jump_expansion_step_instruction: label_map → ℕ →
735  preinstruction Identifier → option (ℕ × jump_length) ≝
736  λlabels.λpc.λi.
737  match i with
738  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
739  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
740  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
741  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
742  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
743  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
744  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
745  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
746  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
747  | _        ⇒ None ?
748  ].
749
750definition is_jump' ≝
751  λx:preinstruction Identifier.
752  match x with
753  [ JC _ ⇒ True
754  | JNC _ ⇒ True
755  | JZ _ ⇒ True
756  | JNZ _ ⇒ True
757  | JB _ _ ⇒ True
758  | JNB _ _ ⇒ True
759  | JBC _ _ ⇒ True
760  | CJNE _ _ ⇒ True
761  | DJNZ _ _ ⇒ True
762  | _ ⇒ False
763  ].
764 
765definition is_jump ≝
766  λx:labelled_instruction.
767  let 〈label,instr〉 ≝ x in
768  match instr with
769  [ Instruction i   ⇒ is_jump' i
770  | Call _ ⇒ True
771  | Jmp _ ⇒ True
772  | _ ⇒ False
773  ].
774
775lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
776#x cases x #l #i cases i
777[#id cases id
778 [1,2,3,6,7,33,34:
779  #x #y %2 whd in match (is_jump ?); /2 by nmk/
780 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
781  #x %2 whd in match (is_jump ?); /2 by nmk/
782 |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
783 |9,10,14,15: #x %1 //
784 |11,12,13,16,17: #x #y %1 //
785 ]
786|2,3: #x %2 /2 by nmk/
787|4,5: #x %1 //
788|6: #x #y %2 /2 by nmk/
789]
790qed.
791 
792
793definition jump_in_policy ≝
794  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
795  ∀i:ℕ.i < |prefix| →
796  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
797   ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
798
799(* these should be moved to BitVector at some point *) 
800lemma bitvector_of_nat_ok:
801  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
802 #n elim n -n
803 [ #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
804 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
805 ]
806qed.
807
808lemma bitvector_of_nat_abs:
809  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
810 #n #x #y #Hx #Hy #Heq @notb_elim
811 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
812 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
813 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H //
814 | #H //
815 ]
816qed.
817
818lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
819 ∀policy:(Σp:jump_expansion_policy.
820 (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
821 jump_in_policy prefix p).
822  ∀i:ℕ.i < |prefix| →
823  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
824  (lookup_opt … (bitvector_of_nat 16 i) policy = None ?).
825 #prefix #policy #i #Hi @conj
826 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
827   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
828   [ #H @H
829   | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
830     @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
831   ]
832 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
833   #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs)
834 ] 
835qed.
836
837definition jump_expansion_start:
838  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
839  Σpolicy:jump_expansion_policy.
840    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
841    jump_in_policy program policy ∧
842    ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
843     lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝
844  λprogram.
845  foldl_strong (option Identifier × pseudo_instruction)
846  (λprefix.Σpolicy:jump_expansion_policy.
847    (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
848    jump_in_policy prefix policy ∧
849    ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
850      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉)
851  program
852  (λprefix.λx.λtl.λprf.λpolicy.
853   let 〈label,instr〉 ≝ x in
854   match instr with
855   [ Instruction i ⇒ match i with
856     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
857     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
858     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
859     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
860     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
861     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
862     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
863     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
864     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
865     | _ ⇒ (pi1 … policy)
866     ]
867   | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
868   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
869   | _      ⇒ (pi1 ?? policy)
870   ]
871  ) (Stub ? ?).
872[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:
873 @conj
874 [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:
875  @conj
876  #i >append_length <commutative_plus #Hi normalize in Hi;
877  [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:
878   #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i)
879   [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:
880     @le_S_to_le @le_S_to_le @Hi
881   |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:
882     @Hi2
883   |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:
884     <Hi @le_n_Sn
885   |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:
886     @Hi2
887   ]
888  ]
889  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
890  [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:
891    >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
892    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
893  ]
894  @conj >(injective_S … Hi)
895   [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:
896    >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H
897   ]
898   #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H
899   >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
900   [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:
901     #H destruct (H)
902   ]
903   @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
904   @le_plus_n_r
905 ]
906 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
907 -Hi; #Hi
908 [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:
909  #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
910  >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; //
911 ]
912 >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n
913 #H @⊥ @H
914|2,3,26,27,28,29,30,31,32,33,34: @conj
915 [1,3,5,7,9,11,13,15,17,19,21: @conj
916  [1,3,5,7,9,11,13,15,17,19,21:
917    #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
918   [1,3,5,7,9,11,13,15,17,19,21:
919     @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
920   ]
921   >eq_bv_sym @bitvector_of_nat_abs
922   [1,4,7,10,13,16,19,22,25,28,31:
923     @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
924     @le_plus_n_r
925   |2,5,8,11,14,17,20,23,26,29,32: @Hi2
926   |3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi
927   ]
928  ]
929  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
930  -Hi #Hi
931  [1,3,5,7,9,11,13,15,17,19,21:
932   >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
933   [1,3,5,7,9,11,13,15,17,19,21:
934    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
935   ]
936   @bitvector_of_nat_abs
937   [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
938   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
939   ]
940   @(transitive_lt … (pi2 ?? program))
941   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
942  ]
943  @conj >(injective_S … Hi) #H
944  [2,4,6,8,10,12,14,16,18,20,22:
945   >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n //
946  ]
947  @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
948 ]
949 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
950  -Hi #Hi
951 [1,3,5,7,9,11,13,15,17,19,21:
952  >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss
953  [1,3,5,7,9,11,13,15,17,19,21:
954   @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj)
955  ]
956  @bitvector_of_nat_abs
957  [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
958  |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
959  ]
960  @(transitive_lt … (pi2 ?? program))
961  >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
962 ]
963 #_ >(injective_S … Hi) @lookup_opt_insert_hit
964|@conj
965 [@conj
966  [ #i #Hi //
967  | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
968  ]
969 | #i #Hi >nth_nil #Hj @⊥ @Hj
970]
971qed.
972
973definition policy_increase: list labelled_instruction → jump_expansion_policy →
974  jump_expansion_policy → Prop ≝
975 λprogram.λop.λp.
976  (∀i:ℕ.i < |program| →
977    let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
978    let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in
979    jmpleq oj j).
980
981definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝
982 (*λlabels.*)λpolicy.
983 bvt_forall (ℕ×ℕ×jump_length) 16 policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
984    match jmp_len with
985    [ short_jump  ⇒ if leb pc_nat addr_nat
986       then le (addr_nat - pc_nat) 126
987       else le (pc_nat - addr_nat) 129
988    | medium_jump ⇒
989       let addr ≝ bitvector_of_nat 16 addr_nat in
990       let pc ≝ bitvector_of_nat 16 pc_nat in
991       let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
992       let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
993       eq_bv 5 fst_5_addr fst_5_pc = true
994    | long_jump   ⇒ True
995    ]
996  ).
997 
998definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
999  ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
1000    ∀l.occurs_exactly_once l program →
1001    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
1002    ∃a.lookup … lm l = Some ? 〈i,a〉).
1003  ∀old_policy:(Σpolicy.
1004    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
1005    jump_in_policy program policy).
1006  (Σpolicy.
1007    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
1008    jump_in_policy program policy ∧
1009    policy_increase program old_policy policy)
1010    ≝
1011  λprogram.λlabels.λold_policy.
1012  let 〈final_pc, final_policy〉 ≝
1013    foldl_strong (option Identifier × pseudo_instruction)
1014    (λprefix.ℕ × Σpolicy.
1015      (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
1016      jump_in_policy prefix policy ∧
1017      policy_increase prefix old_policy policy
1018    )
1019    program
1020    (λprefix.λx.λtl.λprf.λacc.
1021      let 〈pc, policy〉 ≝ acc in
1022      let 〈label,instr〉 ≝ x in
1023      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in
1024      let add_instr ≝
1025        match instr with
1026        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
1027        | Call c        ⇒ Some ? (select_call_length labels pc c)
1028        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
1029        | _             ⇒ None ?
1030        ] in
1031      let 〈new_pc, new_policy〉 ≝
1032        let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
1033        match add_instr with
1034        [ None    ⇒ (* i.e. it's not a jump *)
1035          〈add_instruction_size pc long_jump instr, policy〉
1036        | Some z ⇒ let 〈addr,ai〉 ≝ z in
1037          let new_length ≝ max_length old_length ai in
1038          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
1039        ] in
1040      〈new_pc, new_policy〉
1041    ) 〈0, Stub ? ?〉 in
1042    final_policy.
1043[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
1044[ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
1045  [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
1046  | #z cases z -z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss
1047    [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
1048    | >eq_bv_sym @bitvector_of_nat_abs
1049      [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1050        @le_S_S @le_plus_n_r
1051      | @Hi2
1052      | @lt_to_not_eq @Hi
1053      ]
1054    ]
1055  ]
1056| cases (le_to_or_lt_eq … Hi) -Hi;
1057  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
1058    [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
1059      cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
1060      [ @(proj1 ?? Hacc Hj)
1061      | #z cases z -z #z1 #z2 elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
1062        @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
1063        >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
1064        [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
1065        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
1066        ]
1067        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1068        @le_S_S @le_plus_n_r
1069      ]
1070    | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
1071      #H elim H -H; #h #H elim H -H; #n #H elim H -H #j cases add_instr cases (lookup ??? old_policy ?)
1072      normalize nodelta #x #y [2: #z]
1073      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
1074      [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @lookup_opt_insert_miss @bitvector_of_nat_abs
1075        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
1076        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
1077        ]
1078        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1079        @le_S_S @le_plus_n_r
1080      | @Hl
1081      ]
1082    ]
1083  | #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
1084     <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr
1085     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
1086     [3,5,11: #H @⊥ @H (* instr is not a jump *)
1087     |4,6,12: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
1088       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
1089       [1,3,5: #H destruct (H)]
1090       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1091       @le_S_S @le_plus_n_r
1092     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
1093       whd in match (snd ???); @(ex_intro ?? pc)
1094       [ @(ex_intro ?? (\fst (select_jump_length labels pc id)))
1095         @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id))))
1096         cases (select_jump_length labels pc id)
1097       | @(ex_intro ?? (\fst (select_call_length labels pc id)))
1098         @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id))))
1099         cases (select_call_length labels pc id)
1100       ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit
1101     |8,10: #_ //
1102     |1,2: cases pi
1103       [35,36,37: #H @⊥ @H
1104       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
1105       |1,2,3,6,7,33,34: #x #y #H @⊥ @H
1106       |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
1107         whd in match (snd ???); @(ex_intro ?? pc)
1108         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
1109         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
1110         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
1111         @lookup_opt_insert_hit
1112       |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
1113         whd in match (snd ???); @(ex_intro ?? pc)
1114         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
1115         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
1116         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
1117         @lookup_opt_insert_hit
1118       |72,73,74: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
1119        #z cases z -z #x #y #z normalize nodelta
1120        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
1121        [1,3,5: #H destruct (H)]
1122        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1123        @le_S_S @le_plus_n_r     
1124       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
1125        #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,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
1129        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1130        @le_S_S @le_plus_n_r
1131       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n #H elim H -H #j
1132        cases (lookup ??? old_policy ?) #z cases z -z #x #y #z normalize nodelta
1133        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
1134        [1,3,5,7,9,11,13: #H destruct (H)]
1135        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1136        @le_S_S @le_plus_n_r             
1137       |46,47,51,52: #id #_ //
1138       |48,49,50,53,54: #x #id #_ //
1139       ]
1140     ]
1141   ]
1142  ]
1143| lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %);
1144  [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
1145    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
1146    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
1147      #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
1148    | normalize nodelta >(injective_S … Hi)
1149      >lookup_opt_lookup_miss
1150      [ >lookup_opt_lookup_miss
1151        [ //
1152        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
1153          #x #y normalize nodelta
1154          >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
1155          [ //
1156          | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1157            @le_S_S @le_plus_n_r
1158          ]
1159        ]
1160      | >(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?))
1161        [ //
1162        | >prf >p1 >nth_append_second [ <minus_n_n
1163        generalize in match Ha; normalize nodelta cases instr normalize nodelta
1164        [1: #pi cases pi
1165         [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/
1166         |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/
1167         |35,36,37: #H normalize /2 by nmk/
1168         |9,10,14,15: #id whd in match (jump_expansion_step_instruction ???);
1169           #H destruct (H)
1170         |11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???);
1171           #H destruct (H)
1172         ]
1173        |2,3: #x #H normalize /2 by nmk/
1174        |6: #x #y #H normalize /2 by nmk/
1175        |4,5: #id #H destruct (H)
1176        ] | @le_n ]
1177        | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
1178        ]
1179      ]
1180    ]
1181  | #x cases x -x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
1182    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
1183    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
1184      #y cases y -y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss
1185      [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
1186      | @bitvector_of_nat_abs
1187        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
1188        |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
1189        ]
1190        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1191        @le_S_S @le_plus_n_r
1192      ]
1193    | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
1194      [ #a #H elim H -H; #b #H elim H -H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H)
1195        normalize nodelta >lookup_insert_hit @jmpleq_max_length
1196      | >prf >p1 >nth_append_second
1197        [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta
1198          [1: #pi cases pi
1199           [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H)
1200           |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)
1201           |35,36,37: #H normalize in H; destruct (H)
1202           |9,10,14,15: #id #H //
1203           |11,12,13,16,17: #x #id #H //
1204           ]
1205          |2,3: #x #H normalize in H; destruct (H)
1206          |6: #x #y #H normalize in H; destruct (H)
1207          |4,5: #id #H //
1208          ]
1209        | @le_n ]
1210      | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
1211      ]
1212    ]
1213  ] ]
1214| @conj [ @conj
1215  [ #i #Hi //
1216  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
1217                   normalize in H3; destruct (H3) ]
1218  ]                 
1219  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
1220]
1221qed.
1222 
1223let rec jump_expansion_internal (program: Σl:list labelled_instruction.|l| < 2^16)
1224  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.
1225    And
1226    (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
1227    (jump_in_policy program policy)) ≝
1228  match n with
1229  [ O   ⇒ jump_expansion_start program
1230  | S m ⇒ let old_policy ≝ jump_expansion_internal program m in
1231    jump_expansion_step program (create_label_map program old_policy) old_policy
1232  ].
1233[ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
1234| @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy)))
1235]
1236qed.
1237
1238definition policy_equal ≝
1239  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
1240  ∀n:ℕ.n < |program| →
1241    let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
1242    let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
1243    j1 = j2.
1244
1245lemma pe_refl:
1246  ∀program.reflexive ? (policy_equal program).
1247 #program whd #x whd #n #Hn cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
1248 #y cases y -y #y #z normalize nodelta @refl
1249qed.
1250
1251lemma pe_sym:
1252  ∀program.symmetric ? (policy_equal program).
1253 #program whd #x #y #Hxy whd #n #Hn
1254 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
1255 #z cases z -z #x1 #x2 #x3 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
1256 #z cases z -z #y1 #y2 #y3 normalize nodelta //
1257qed.
1258
1259lemma pe_trans:
1260  ∀program.transitive ? (policy_equal program).
1261 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
1262 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn
1263 lapply (Hxy n Hn) -Hxy lapply (Hyz n Hn) -Hyz
1264 cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
1265 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
1266 cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z #z1 #z2 #z3
1267 normalize nodelta //
1268qed.
1269
1270lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1271 ∀p1,p2:Σpolicy.
1272 (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
1273 ∧jump_in_policy program policy.
1274  policy_equal program p1 p2 →
1275  policy_equal program (jump_expansion_step program (create_label_map program p1) p1)
1276    (jump_expansion_step program (create_label_map program p2) p2).
1277 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
1278 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
1279 cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?);
1280 [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl)
1281   #Hnotjmp >lookup_opt_lookup_miss
1282   [ >lookup_opt_lookup_miss
1283     [ @refl
1284     | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn))
1285       [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2)))
1286       | @Hnotjmp
1287       ]
1288     ]
1289   | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn))
1290     [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1)))
1291     | @Hnotjmp
1292     ]
1293   ]
1294 | #x #Hl cases daemon (* XXX *)
1295 ]
1296qed.
1297
1298(* this is in the stdlib, but commented out, why? *)
1299theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
1300  #n (elim n) normalize /2 by S_pred/ qed.
1301
1302lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
1303  policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
1304  ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
1305 #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
1306 lapply Heq -Heq; lapply n -n; elim z -z;
1307 [ #n #Heq <plus_n_O @pe_refl 
1308 | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n)))
1309   [ @Heq
1310   | @pe_step @Hind @Heq
1311   ]
1312 ]
1313qed.
1314
1315lemma thingie:
1316  ∀A:Prop.(A + ¬A) → (¬¬A) → A.
1317 #A #Adec #nnA cases Adec
1318 [ //
1319 | #H @⊥ @(absurd (¬A) H nnA)
1320 ]
1321qed.
1322 
1323lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
1324 ∀policy:(Σp:jump_expansion_policy.
1325    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1326    jump_in_policy program p).
1327  ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) →
1328  ∃n:ℕ.n < (|program|) ∧ jmple
1329    (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
1330    (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)).
1331 #program #policy #Hp
1332 cases (dec_bounded_exists (λn.jmple
1333   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
1334   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (|program|))
1335 [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
1336 | #abs @⊥ @(absurd ?? Hp) #n #Hn
1337   lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn)
1338   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
1339   cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %);
1340   #z cases z -z #x1 #x2 #x3 #Hx
1341   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))
1342   cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %);
1343   #z cases z -z #y1 #y2 #y3 #Hy
1344   normalize nodelta #Hj cases Hj
1345   [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | >Hx >Hy @Hj ]
1346   | //
1347   ]
1348 | #n @dec_jmple
1349 ]
1350qed.
1351
1352lemma stupid:
1353  ∀program,n.
1354  pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) =
1355  pi1 … (jump_expansion_internal program (S n)).
1356 //
1357qed.
1358
1359let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
1360 on program: ℕ ≝
1361 match program with
1362 [ nil      ⇒ acc
1363 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) with
1364   [ long_jump   ⇒ measure_int t policy (acc + 2)
1365   | medium_jump ⇒ measure_int t policy (acc + 1)
1366   | _           ⇒ measure_int t policy acc
1367   ]
1368 ].
1369
1370(* definition measure ≝
1371  λprogram.λpolicy.measure_int program policy 0. *)
1372 
1373lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
1374  measure_int program policy (x+d) = measure_int program policy x + d.
1375 #program #policy #x #d generalize in match x; -x elim d
1376 [ //
1377 | -d; #d #Hind elim program
1378   [ //
1379   | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
1380     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
1381     [ normalize nodelta @Hd
1382     |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
1383       @Hd
1384     ]
1385   ]
1386 ]
1387qed.
1388   
1389lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
1390  ∀policy:Σp:jump_expansion_policy.
1391    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1392    jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ.
1393  measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc.
1394#program #policy #l elim l -l;
1395  [ #Hp #acc normalize @le_n
1396  | #h #t #Hind #Hp #acc
1397    lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) Hp)
1398    whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?);
1399    cases (bvt_lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
1400    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
1401    normalize nodelta #Hj cases Hj
1402    [ cases x3 cases y3
1403      [1,4,5,7,8,9: #H @⊥ @H
1404      |2,3,6: #_ normalize nodelta
1405        [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) acc))
1406        |3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) (acc+1)))
1407        ]
1408        [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn
1409        |2,4,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus [ @le_n | //]
1410        ]
1411      ]
1412    | #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
1413    ]
1414  ]
1415qed.
1416
1417lemma measure_le: ∀program.∀policy.
1418  measure_int program policy 0 ≤ 2*|program|.
1419 #program #policy elim program
1420 [ normalize @le_n
1421 | #h #t #Hind whd in match (measure_int ???);
1422   cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
1423   [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
1424   |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
1425     @le_plus [1,3: @Hind |2,4: // ]
1426   ]
1427 ]
1428qed.
1429
1430(* these lemmas seem superfluous, but not sure how *)
1431lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
1432 #a elim a
1433 [ normalize #b //
1434 | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
1435   <plus_n_Sm <plus_n_Sm #H
1436   >(Hind b (injective_S ?? (injective_S ?? H))) // ]
1437 ]
1438qed.
1439
1440lemma sth_not_s: ∀x.x ≠ S x.
1441 #x cases x
1442 [ // | #y // ]
1443qed.
1444
1445lemma measure_full: ∀program.∀policy.
1446  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
1447  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
1448 #program #policy elim program
1449 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1450 | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
1451   [ whd in match (measure_int ???) in Hm;
1452     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
1453     normalize nodelta
1454     [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
1455     | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
1456       <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
1457       >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
1458       >plus_n_Sm @le_n
1459     | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
1460     ]
1461   | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
1462   [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
1463   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1464     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
1465     normalize nodelta
1466     [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
1467       >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
1468     | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
1469       #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
1470     | #_ //
1471     ]
1472   ]]
1473 ]
1474qed.
1475
1476lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1477  ∀policy:Σp:jump_expansion_policy.
1478    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1479    jump_in_policy program p.
1480  measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 →
1481  policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy).
1482#program #policy lapply (le_n (|program|)) @(list_ind ?
1483  (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 →
1484      policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy)))
1485   ?? program)
1486 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
1487 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
1488   [ #Hi @Hind
1489     [ @(transitive_le … Hp) //
1490     | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
1491       lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
1492       [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
1493       | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
1494         #x cases x -x #x1 #x2 #x3
1495         cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
1496         #y cases y -y #y1 #y2 #y3
1497         normalize nodelta cases x3 cases y3 normalize nodelta
1498         [1: #H #_ @H
1499         |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1500           @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1501         |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
1502         |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
1503           #H #_ @(injective_plus_r … H)
1504         |6: >measure_plus >measure_plus
1505            change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1506            #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1507            @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1508         |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
1509           #H #_ @(injective_plus_r … H)
1510         ]
1511       ]
1512     | @(le_S_S_to_le … Hi)
1513     ]
1514   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 
1515     whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
1516     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
1517     [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
1518     | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
1519       #x cases x -x #x1 #x2 #x3
1520       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
1521       #y cases y -y #y1 #y2 #y3
1522       normalize nodelta cases x3 cases y3 normalize nodelta
1523       [1,5,9: #_ #_ //
1524       |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
1525       |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1526         @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1527       |6: >measure_plus >measure_plus
1528          change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1529          #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1530          @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1531       ]
1532     ]
1533   ]
1534 ] 
1535qed.
1536
1537lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
1538  |l| ≤ |program| → measure_int l (jump_expansion_internal program 0) 0 = 0.
1539 #l #program elim l
1540 [ //
1541 | #h #t #Hind #Hp whd in match (measure_int ???);
1542   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
1543   [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉)
1544     [ normalize nodelta @Hind @le_S_to_le ]
1545     @Hp
1546   | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,0,short_jump〉)
1547     [ normalize nodelta @Hind @le_S_to_le ]
1548     @Hp
1549   ]
1550 ]
1551qed.
1552 
1553definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1554  Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
1555 #program @(mk_Sig … (jump_expansion_internal program (2*|program|)))
1556 @(ex_intro … (2*|program|)) #k #Hk
1557 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
1558   (jump_expansion_internal program (S k))) ? (2*|program|))
1559 [ #H elim H -H #x #Hx @pe_trans
1560   [ @(jump_expansion_internal program x)
1561   | @pe_sym @equal_remains_equal
1562     [ @(proj2 ?? Hx)
1563     | @(transitive_le ? (2*|program|))
1564       [ @le_S_S_to_le @le_S @(proj1 ?? Hx)
1565       | @le_S_S_to_le @le_S @Hk
1566       ]
1567     ]
1568   | @equal_remains_equal
1569     [ @(proj2 ?? Hx)
1570     | @le_S_S_to_le @le_S @(proj1 ?? Hx)
1571     ]
1572   ]
1573 | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @pe_sym @equal_remains_equal
1574   [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
1575     #Hfull #i #Hi
1576     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)
1577     lapply (Hfull ? i Hi)
1578     [ -i @le_to_le_to_eq
1579       [ @measure_le
1580       | lapply (le_n (2*|program|)) elim (2*|program|) in ⊢ (?%? → %);
1581         [ #_ >measure_zero @le_n
1582         | #x #Hind #Hx
1583           cut (measure_int program (jump_expansion_internal program x) 0 <
1584                measure_int program (jump_expansion_internal program (S x)) 0)
1585           [ elim (le_to_or_lt_eq …
1586               (measure_incr_or_equal program (jump_expansion_internal program x) program (le_n (|program|)) 0))
1587             [ //
1588             | #H @⊥ @(absurd ?? (Hfa x Hx)) @measure_special @H
1589             ]
1590           | #H lapply (Hind (le_S_to_le … Hx)) #H2 @(le_to_lt_to_lt … H) @H2
1591           ]
1592         ]
1593       ]
1594     | -Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*|program|)) 〈0,0,short_jump〉)
1595       #x cases x -x #x1 #x2 #x3 normalize nodelta #Hfull
1596       >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉)
1597       #y cases y -y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta 
1598       [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
1599       | #_ //
1600       ]
1601     ]
1602   | @le_S_to_le @Hk
1603   ]
1604 | #n @dec_bounded_forall #m
1605   cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
1606   #x cases x -x #x1 #x2 #x3
1607   cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
1608   #y cases y -y #y1 #y2 #y3 normalize nodelta
1609   @dec_eq_jump_length
1610 ]
1611qed.
1612
1613let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n:
1614  BitVectorTrie jump_length 16 ≝
1615  match n with
1616  [ O    ⇒ acc
1617  | S n' ⇒
1618    match lookup_opt … (bitvector_of_nat 16 n') policy with
1619    [ None   ⇒ transform_policy n' policy acc
1620    | Some x ⇒ let 〈pc,length〉 ≝ x in
1621      transform_policy n' policy (insert … pc length acc)
1622    ]
1623  ].
1624
1625(**************************************** START OF POLICY ABSTRACTION ********************)
1626
1627definition policy_type ≝ Word → jump_length.
1628
1629definition jump_expansion':
1630 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
1631 policy_type ≝
1632 λprogram.λpc.
1633  let policy ≝
1634    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
1635  lookup ? ? pc policy long_jump.
1636/2 by Stub, mk_Sig/
1637qed.
1638
1639definition assembly_1_pseudoinstruction_safe ≝
1640  λprogram: pseudo_assembly_program.
1641  λjump_expansion: policy_type.
1642  λppc: Word.
1643  λpc: Word.
1644  λlookup_labels.
1645  λlookup_datalabels.
1646  λi.
1647  let expansion ≝ jump_expansion ppc in
1648    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
1649    [ None ⇒ None ?
1650    | Some pseudos ⇒
1651      let mapped ≝ map ? ? assembly1 pseudos in
1652      let flattened ≝ flatten ? mapped in
1653      let pc_len ≝ length ? flattened in
1654        Some ? (〈pc_len, flattened〉)
1655    ].
1656 
1657definition construct_costs_safe ≝
1658  λprogram.
1659  λjump_expansion: policy_type.
1660  λpseudo_program_counter: nat.
1661  λprogram_counter: nat.
1662  λcosts: BitVectorTrie costlabel 16.
1663  λi.
1664  match i with
1665  [ Cost cost ⇒
1666    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1667      Some ? 〈program_counter, (insert … program_counter_bv cost costs)〉
1668  | _ ⇒
1669    let pc_bv ≝ bitvector_of_nat ? program_counter in
1670    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
1671    let lookup_labels ≝ λx.pc_bv in
1672    let lookup_datalabels ≝ λx.zero ? in
1673    let pc_delta_assembled ≝
1674      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
1675        lookup_labels lookup_datalabels i
1676    in
1677    match pc_delta_assembled with
1678    [ None ⇒ None ?
1679    | Some pc_delta_assembled ⇒
1680      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
1681        Some ? 〈pc_delta + program_counter, costs〉       
1682    ]
1683  ].
1684
1685(* This establishes the correspondence between pseudo program counters and
1686   program counters. It is at the heart of the proof. *)
1687(*CSC: code taken from build_maps *)
1688definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
1689 λinstr_list.
1690 λjump_expansion: policy_type.
1691 λl:list labelled_instruction.
1692 λacc.
1693  foldl …
1694   (λt,i.
1695       match t with
1696       [ None ⇒ None …
1697       | Some ppc_pc_map ⇒
1698         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1699         let 〈program_counter, sigma_map〉 ≝ pc_map in
1700         let 〈label, i〉 ≝ i in
1701          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
1702           [ None ⇒ None ?
1703           | Some pc_ignore ⇒
1704              let 〈pc,ignore〉 ≝ pc_ignore in
1705                Some … 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ]
1706       ]) acc l.
1707
1708definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) ≝
1709  λprog.
1710  λjump_expansion.
1711    sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, Stub …〉〉).
1712
1713definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
1714 λprogram,jump_expansion,instr_list.
1715  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
1716   [ None ⇒ None …
1717   | Some result ⇒
1718      let 〈ppc,pc_sigma_map〉 ≝ result in
1719      let 〈pc,map〉 ≝ pc_sigma_map in
1720       Some … 〈ppc,pc〉 ].
1721
1722definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
1723 λinstr_list,jump_expansion.
1724  match sigma0 instr_list jump_expansion with
1725  [ None ⇒ None ?
1726  | Some result ⇒
1727    let 〈ppc,pc_sigma_map〉 ≝ result in
1728    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
1729      if gtb pc (2^16) then
1730        None ?
1731      else
1732        Some ? (λx. lookup … x sigma_map (zero …)) ].
1733
1734(* stuff about policy *)
1735
1736definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
1737
1738definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
1739
1740lemma eject_policy: ∀p. policy p → policy_type.
1741 #p #pol @(pi1 … pol)
1742qed.
1743
1744coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
1745
1746definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
1747 λp,policy.
1748  match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
1749   [ None ⇒ λabs. ⊥
1750   | Some r ⇒ λ_.r] (pi2 … policy).
1751 cases abs /2/
1752qed.
1753
1754example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
1755 cases daemon.
1756qed.
1757
1758axiom fetch_pseudo_instruction_split:
1759 ∀instr_list,ppc.
1760  ∃pre,suff,lbl.
1761   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
1762
1763lemma sigma00_append:
1764 ∀instr_list,jump_expansion,l1,l2,acc.
1765  sigma00 instr_list jump_expansion (l1@l2) acc =
1766   sigma00 instr_list jump_expansion
1767    l2 (sigma00 instr_list jump_expansion l1 acc).
1768 whd in match sigma00; normalize nodelta;
1769 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
1770qed.
1771
1772lemma sigma00_strict:
1773 ∀instr_list,jump_expansion,l,acc. acc = None ? →
1774  sigma00 instr_list jump_expansion l acc = None ….
1775 #instr_list #jump_expansion #l elim l
1776  [ #acc #H >H %
1777  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
1778qed.
1779
1780lemma policy_ok_prefix_ok:
1781 ∀program.∀pol:policy program.∀suffix,prefix.
1782  prefix@suffix = \snd program →
1783   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
1784 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
1785 generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol
1786 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
1787 normalize nodelta >sigma00_append
1788 cases (sigma00 ?? prefix ?)
1789  [2: #x #_ % #abs destruct(abs)
1790  | * #abs @⊥ @abs >sigma00_strict % ]
1791qed.
1792
1793lemma policy_ok_prefix_hd_ok:
1794 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
1795  (prefix@[hd])@suffix = \snd program →
1796   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
1797    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1798    let 〈program_counter, sigma_map〉 ≝ pc_map in
1799    let 〈label, i〉 ≝ hd in
1800     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
1801 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
1802 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
1803  (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
1804 @pair_elim #ppc #pc_map #EQ3 normalize nodelta
1805 @pair_elim #pc #map #EQ4 normalize nodelta
1806 @pair_elim #l' #i' #EQ5 normalize nodelta
1807 cases (construct_costs_safe ??????) normalize
1808  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
1809qed.
1810
1811definition expand_pseudo_instruction:
1812 ∀program:pseudo_assembly_program.∀pol: policy program.
1813  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
1814  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1815  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1816  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
1817  pc = sigma program pol ppc →
1818  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
1819≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
1820   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
1821    [ None ⇒ let dummy ≝ [ ] in dummy
1822    | Some res ⇒ res ].
1823 [ @⊥ whd in p:(??%??);
1824   generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);
1825   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
1826   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
1827   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
1828   #res #K
1829   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
1830   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
1831   cases daemon (* CSC: XXXXXXXX Ero qui
1832   
1833    [3: @policy_ok_prefix_ok ]
1834    | sigma00 program pol pre
1835
1836
1837
1838   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
1839   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
1840   per concludere construct_costs_safe ≠ None *)
1841 | >p %]
1842qed.
1843
1844(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1845definition assembly_1_pseudoinstruction':
1846 ∀program:pseudo_assembly_program.∀pol: policy program.
1847  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1848  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1849  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1850  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1851  Σres:(nat × (list Byte)).
1852   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
1853   let 〈len,code〉 ≝ res in
1854    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
1855     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
1856≝ λprogram: pseudo_assembly_program.
1857  λpol: policy program.
1858  λppc: Word.
1859  λlookup_labels.
1860  λlookup_datalabels.
1861  λpi.
1862  λprf1,prf2,prf3.
1863   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
1864    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
1865    | Some res ⇒ res ].
1866 [ @⊥ elim pi in p; [*]
1867   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
1868   generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
1869   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
1870   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
1871   cases daemon
1872 | % [ >p %]
1873   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
1874   (* THIS SHOULD BE TRUE INSTEAD *)
1875   cases daemon]
1876qed.
1877
1878definition assembly_1_pseudoinstruction:
1879 ∀program:pseudo_assembly_program.∀pol: policy program.
1880  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1881  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1882  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1883  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1884   nat × (list Byte)
1885≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
1886   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
1887    prf2 prf3.
1888
1889lemma assembly_1_pseudoinstruction_ok1:
1890 ∀program:pseudo_assembly_program.∀pol: policy program.
1891  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1892  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
1893  ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
1894  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
1895     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
1896   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
1897 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
1898 cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
1899 #H1 #_ @H1
1900qed.
1901
1902(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1903definition construct_costs':
1904 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
1905  Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
1906
1907  λprogram.λpol: policy program.λppc,pc,costs,i.
1908   match construct_costs_safe program pol ppc pc costs i with
1909    [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
1910    | Some res ⇒ res ].
1911 [ cases daemon
1912 | >p %]
1913qed.
1914
1915definition construct_costs ≝
1916 λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i).
1917
1918(*
1919axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
1920axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
1921
1922axiom foldl_strong_step:
1923 ∀A:Type[0].
1924  ∀P: list A → Type[0].
1925   ∀l: list A.
1926    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
1927     ∀acc: P [ ].
1928      ∀Q: ∀prefix. P prefix → Prop.
1929       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
1930        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
1931       Q [ ] acc →
1932        Q l (foldl_strong A P l H acc).
1933(*
1934 #A #P #l #H #acc #Q #HQ #Hacc normalize;
1935 generalize in match
1936  (foldl_strong ?
1937   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
1938   l ? Hacc)
1939 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
1940 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
1941 #K
1942
1943 generalize in match
1944  (foldl_strong ?
1945   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
1946 [2: @H
1947*)
1948
1949axiom foldl_elim:
1950 ∀A:Type[0].
1951  ∀B: Type[0].
1952   ∀H: A → B → A.
1953    ∀acc: A.
1954     ∀l: list B.
1955      ∀Q: A → Prop.
1956       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
1957         Q acc →
1958          Q (foldl A B H acc l).
1959*)
1960
1961lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1962 #A #a #b #EQ destruct //
1963qed.
1964
1965(*
1966lemma tech_pc_sigma00_append_Some:
1967 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1968  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1969   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1970 #program #pol #prefix #costs #label #i #ppc #pc #H
1971  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
1972  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
1973  generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
1974  whd in match sigma0; normalize nodelta;
1975  >foldl_step
1976  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
1977  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
1978  cases (sigma00 program pol prefix) in H ⊢ %
1979   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
1980   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
1981     
1982     normalize nodelta; -H;
1983     
1984 
1985   generalize in match H; -H;
1986  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
1987   [2: whd in ⊢ (??%%)
1988XXX
1989*)
1990
1991axiom construct_costs_sigma:
1992 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
1993  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
1994   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
1995
1996axiom tech_pc_sigma00_append_Some:
1997 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1998  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1999   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
2000
2001axiom eq_identifier_eq:
2002  ∀tag: String.
2003  ∀l.
2004  ∀r.
2005    eq_identifier tag l r = true → l = r.
2006
2007axiom neq_identifier_neq:
2008  ∀tag: String.
2009  ∀l, r: identifier tag.
2010    eq_identifier tag l r = false → (l = r → False).
2011
2012include "basics/russell.ma".
2013
2014lemma weird: ∀A,B,P. (Σx:A × B. P x) → True.
2015 #A #B #P #c
2016 letin H ≝ (let 〈a,b〉 ≝ c in b)
2017 check H
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: check result
2062 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
2063   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
2064   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
2065   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
2066   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
2067   | #id normalize nodelta; -labels1; cases label; normalize nodelta
2068     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
2069     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
2070       generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
2071        [ #EQ #_ <(eq_identifier_eq … EQ) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit
2072          <IH0 [@IHn1 | <(eq_identifier_eq … EQ) in H; #H @H]
2073        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: -IHn1;
2074          (*Andrea:XXXX used to work /2/*)@nmk #IDL lapply (sym_eq ? ? ? IDL)
2075          lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ]
2076          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
2077 |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ]
2078 | generalize in match (pi2 … result) in ⊢ ?;
2079   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
2080   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
2081qed.
2082
2083definition assembly:
2084 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝
2085  λp.let 〈preamble, instr_list〉 ≝ p in
2086   λpol.
2087    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
2088    let datalabels ≝ construct_datalabels preamble in
2089    let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in
2090    let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
2091    let result ≝
2092     foldl_strong
2093      (option Identifier × pseudo_instruction)
2094      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
2095        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
2096        let 〈ppc,code〉 ≝ ppc_code in
2097         ∀ppc'.
2098          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
2099          let 〈len,assembledi〉 ≝
2100           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
2101           True)
2102      instr_list
2103      (λprefix,hd,tl,prf,pc_ppc_code.
2104        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
2105        let 〈ppc, code〉 ≝ ppc_code in
2106        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
2107        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
2108        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
2109         〈new_pc, 〈new_ppc, (code @ program)〉〉)
2110      〈(zero ?), 〈(zero ?), [ ]〉〉
2111    in
2112     〈\snd (\snd result), costs〉.
2113 [2,5: %
2114 |*: cases daemon ]
2115qed.
2116
2117definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
2118 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.