source: src/ASM/Assembly.ma @ 1606

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

Porting to last library of Matita.

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