source: src/ASM/Policy.ma @ 1614

Last change on this file since 1614 was 1614, checked in by boender, 8 years ago
  • split policy from assembly
File size: 74.0 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  ].
Note: See TracBrowser for help on using the repository browser.