source: src/ASM/Assembly.ma @ 1482

Last change on this file since 1482 was 1482, checked in by sacerdot, 8 years ago
  1. very long standing conflict committed (but don't ask me what the stuff I added is used for...)
  2. ported to new automation (which seems to be slower on one example)
File size: 66.0 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/BitVectorTrie.ma".
3include "ASM/Arithmetic.ma".
4include "ASM/Fetch.ma".
5include "ASM/Status.ma".
6include alias "basics/logic.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
411inductive jump_length: Type[0] ≝
412  | short_jump: jump_length
413  | medium_jump: jump_length
414  | long_jump: jump_length.
415
416(* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
417definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16.
418
419definition expand_relative_jump_internal:
420 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
421 option (list instruction)
422 ≝
423  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
424  match jmp_len with
425  [ short_jump ⇒
426     let lookup_address ≝ lookup_labels jmp in
427     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
428     let 〈upper, lower〉 ≝ split ? 8 8 result in
429     if eq_bv ? upper (zero 8) then
430      let address ≝ RELATIVE lower in
431       Some ? [ RealInstruction (i address) ]
432     else
433       None ?
434  | medium_jump ⇒ None …
435  | long_jump ⇒
436    Some ?
437    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
438      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
439      LJMP (ADDR16 (lookup_labels jmp))
440    ]
441  ].
442  @ I
443qed.
444
445definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
446  λlookup_labels.
447  λjmp_len: jump_length.
448  λpc.
449  λi: preinstruction Identifier.
450  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
451  match i with
452  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
453  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
454  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
455  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
456  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
457  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
458  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
459  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
460  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
461  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
462  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
463  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
464  | INC arg ⇒ Some ? [ INC ? arg ]
465  | DEC arg ⇒ Some ? [ DEC ? arg ]
466  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
467  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
468  | DA arg ⇒ Some ? [ DA ? arg ]
469  | ANL arg ⇒ Some ? [ ANL ? arg ]
470  | ORL arg ⇒ Some ? [ ORL ? arg ]
471  | XRL arg ⇒ Some ? [ XRL ? arg ]
472  | CLR arg ⇒ Some ? [ CLR ? arg ]
473  | CPL arg ⇒ Some ? [ CPL ? arg ]
474  | RL arg ⇒ Some ? [ RL ? arg ]
475  | RR arg ⇒ Some ? [ RR ? arg ]
476  | RLC arg ⇒ Some ? [ RLC ? arg ]
477  | RRC arg ⇒ Some ? [ RRC ? arg ]
478  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
479  | MOV arg ⇒ Some ? [ MOV ? arg ]
480  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
481  | SETB arg ⇒ Some ? [ SETB ? arg ]
482  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
483  | POP arg ⇒ Some ? [ POP ? arg ]
484  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
485  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
486  | RET ⇒ Some ? [ RET ? ]
487  | RETI ⇒ Some ? [ RETI ? ]
488  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
489  ].
490
491definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
492  λlookup_labels.
493  λlookup_datalabels.
494  λpc.
495  λjmp_len.
496  λi.
497  match i with
498  [ Cost cost ⇒ Some ? [ ]
499  | Comment comment ⇒ Some ? [ ]
500  | Call call ⇒
501    match jmp_len with
502    [ short_jump ⇒ None ?
503    | medium_jump ⇒
504      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
505      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
506      if eq_bv ? ignore fst_5 then
507        let address ≝ ADDR11 address in
508          Some ? ([ ACALL address ])
509      else
510        None ?
511    | long_jump ⇒
512      let address ≝ ADDR16 (lookup_labels call) in
513        Some ? [ LCALL address ]
514    ]
515  | Mov d trgt ⇒
516    let address ≝ DATA16 (lookup_datalabels trgt) in
517      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
518  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
519  | Jmp jmp ⇒
520    match jmp_len with
521    [ short_jump ⇒
522      let lookup_address ≝ lookup_labels jmp in
523      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
524      let 〈upper, lower〉 ≝ split ? 8 8 result in
525      if eq_bv ? upper (zero 8) then
526        let address ≝ RELATIVE lower in
527          Some ? [ SJMP address ]
528      else
529        None ?
530    | medium_jump ⇒
531      let address ≝ lookup_labels jmp in
532      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
533      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
534      if eq_bv ? fst_5_addr fst_5_pc then
535        let address ≝ ADDR11 rest_addr in
536          Some ? ([ AJMP address ])
537      else
538        None ?
539    | long_jump ⇒
540      let address ≝ ADDR16 (lookup_labels jmp) in
541        Some ? [ LJMP address ]
542    ]
543  ].
544  @ I
545qed.
546
547(* label_trie: identifier ↦ 〈instruction number, address〉 *)
548definition label_trie ≝ BitVectorTrie (nat × nat) 16.
549
550definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
551  λpc.λjmp_len.λinstr.
552  let bv_pc ≝ bitvector_of_nat 16 pc in
553  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
554  let bv: list (BitVector 8) ≝ match ilist with
555    [ None   ⇒ (* hmm, this shouldn't happen *) [ ]
556    | Some l ⇒ flatten … (map … assembly1 l)
557    ] in
558  pc + (|bv|).
559 
560definition is_label ≝
561  λx:labelled_instruction.λl:Identifier.
562  let 〈lbl,instr〉 ≝ x in
563  match lbl with
564  [ Some l' ⇒ l' = l
565  | _       ⇒ False
566  ].
567 
568lemma label_does_not_occur:
569  ∀i,p,l.
570  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
571 #i #p #l generalize in match i; elim p
572 [ #i >nth_nil #H @⊥ @H
573 | #h #t #IH #i cases i -i
574   [ cases h #hi #hp cases hi normalize
575     [ #H @⊥ @H
576     | #l' #Heq change in match (eq_v ??? l' l) with (eq_bv ? l' l)
577       >(eq_eq_bv … Heq) //
578     ]
579   | #i #H whd in match (does_not_occur ??)
580     whd in match (instruction_matches_identifier ??)
581     cases h #hi #hp cases hi normalize
582     [ @(IH i) @H
583     | #l' cases (eq_v ??? l' l)
584       [ normalize //
585       | normalize @(IH i) @H
586       ]
587     ]
588   ]
589 ]
590qed. 
591
592(* lemma coerc_sigma:
593 ∀A,P.∀p:A.P p → Σx:A.P x.
594#A #P #a #p % [ @a | /2/]
595qed.
596coercion coerc_sigma:∀A,P.∀p:A.P p → Σx:A.P x
597≝ coerc_sigma on p: ? to (Sig ??). *)
598
599lemma coerc_pair_sigma:
600 ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
601#A #B #P * #a #b #p % [@a | /2/]
602qed.
603coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
604≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
605     
606let rec create_label_trie (program: list labelled_instruction)
607  (policy: jump_expansion_policy):
608  (Σlabels:label_trie.
609    ∀i:ℕ.i < |program| →
610    ∀l.occurs_exactly_once l program →
611    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
612    ∃a.lookup_opt … l labels = Some ? 〈i,a〉
613  ) ≝
614  let 〈final_pc, final_labels〉 ≝
615    foldl_strong (option Identifier × pseudo_instruction)
616    (λprefix.ℕ × (Σlabels.
617      ∀i:ℕ.i < |prefix| →
618      ∀l.occurs_exactly_once l prefix →
619      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
620      ∃a.lookup_opt … l labels = Some ? 〈i,a〉)
621    )
622    program
623    (λprefix.λx.λtl.λprf.λacc.
624     let 〈pc,labels〉 ≝ acc in
625     let 〈label,instr〉 ≝ x in
626          let new_labels ≝
627          match label with
628          [ None   ⇒ labels
629          | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
630          ] in
631          let jmp_len ≝ \snd (lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
632          〈add_instruction_size pc jmp_len instr, new_labels〉
633    ) 〈0, Stub ? ?〉 in
634    final_labels.
635[ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
636  [ #Hi #l normalize nodelta; cases label normalize nodelta
637    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
638      lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
639      % [ @addr | @Haddr ]
640    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc; #Hocc
641      lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq
642      [ >Heq in Hocc; #Hocc normalize in Hocc;
643        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
644        @⊥ @(absurd … Hocc)
645      | >Heq in Hocc; normalize nodelta #Hocc lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
646        [ #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]
647        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
648        ]
649      ]
650      >(label_does_not_occur i … Hl) normalize nodelta @nmk //
651    ]
652  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
653    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
654      [ normalize nodelta #H @⊥ @H
655      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_opt_insert_hit ]
656      ]
657    | @le_n
658    ]
659  ]
660| #i #Hi #l #Hl @⊥ @Hl
661]
662qed.
663
664definition select_reljump_length: label_trie → ℕ → Identifier → jump_length ≝
665  λlabels.λpc.λlbl.
666  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
667  if leb pc addr (* forward jump *)
668  then if leb (addr - pc) 126
669       then short_jump
670       else long_jump
671  else if leb (pc - addr) 129
672       then short_jump
673       else long_jump.
674
675definition select_call_length: label_trie → ℕ → Identifier → jump_length ≝
676  λlabels.λpc_nat.λlbl.
677  let pc ≝ bitvector_of_nat 16 pc_nat in
678  let addr ≝ bitvector_of_nat 16 (\snd (lookup ? ? lbl labels 〈0, pc_nat〉)) in
679  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
680  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
681  if eq_bv ? fst_5_addr fst_5_pc
682  then medium_jump
683  else long_jump.
684 
685definition select_jump_length: label_trie → ℕ → Identifier → jump_length ≝
686  λlabels.λpc.λlbl.
687  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
688  if leb pc addr
689  then if leb (addr - pc) 126
690       then short_jump
691       else select_call_length labels pc lbl
692  else if leb (pc - addr) 129
693       then short_jump
694       else select_call_length labels pc lbl.
695 
696definition jump_expansion_step_instruction: label_trie → ℕ →
697  preinstruction Identifier → option jump_length ≝
698  λlabels.λpc.λi.
699  match i with
700  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
701  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
702  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
703  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
704  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
705  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
706  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
707  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
708  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
709  | _        ⇒ None ?
710  ].
711
712definition max_length: jump_length → jump_length → jump_length ≝
713  λj1.λj2.
714  match j1 with
715  [ long_jump   ⇒ long_jump
716  | medium_jump ⇒
717    match j2 with
718    [ long_jump ⇒ long_jump
719    | _         ⇒ medium_jump
720    ]
721  | short_jump  ⇒ j2
722  ].
723
724definition jmpleq: jump_length → jump_length → Prop ≝
725  λj1.λj2.
726  match j1 with
727  [ short_jump  ⇒ True
728  | medium_jump ⇒
729    match j2 with
730    [ short_jump ⇒ False
731    | _          ⇒ True
732    ]
733  | long_jump   ⇒
734    match j2 with
735    [ long_jump ⇒ True
736    | _         ⇒ False
737    ]
738  ].
739
740lemma jmpleq_max_length: ∀x,y.jmpleq y (max_length y x).
741 #x #y
742 cases y
743 [ //
744 | cases x //
745 | //
746 ]
747qed.
748
749definition is_jump' ≝
750  λx:preinstruction Identifier.
751  match x with
752  [ JC _ ⇒ True
753  | JNC _ ⇒ True
754  | JZ _ ⇒ True
755  | JNZ _ ⇒ True
756  | JB _ _ ⇒ True
757  | JNB _ _ ⇒ True
758  | JBC _ _ ⇒ True
759  | CJNE _ _ ⇒ True
760  | DJNZ _ _ ⇒ True
761  | _ ⇒ False
762  ].
763 
764definition is_jump ≝
765  λx:labelled_instruction.
766  let 〈label,instr〉 ≝ x in
767  match instr with
768  [ Instruction i   ⇒ is_jump' i
769  | Call _ ⇒ True
770  | Jmp _ ⇒ True
771  | _ ⇒ False
772  ].
773
774definition jump_in_policy ≝
775  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
776  ∀i:ℕ.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
777  ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉.
778 
779axiom bitvector_of_nat_abs:
780  ∀x,y:ℕ.x ≠ y → ¬eq_bv 16 (bitvector_of_nat 16 x) (bitvector_of_nat 16 y).
781 
782let rec jump_expansion_start (program: list labelled_instruction):
783  (Σpolicy.jump_in_policy program policy) ≝
784  foldl_strong (option Identifier × pseudo_instruction)
785  (λprefix.Σpolicy.jump_in_policy prefix policy)
786  program
787  (λprefix.λx.λtl.λprf.λpolicy.
788   let 〈label,instr〉 ≝ x in
789   match instr with
790   [ Instruction i ⇒ match i with
791     [ JC _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
792     | JNC _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
793     | JZ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
794     | JNZ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
795     | JB _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
796     | JNB _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
797     | JBC _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
798     | CJNE _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
799     | DJNZ _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
800     | _ ⇒ (eject … policy)
801     ]
802   | Call c ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
803   | Jmp j  ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
804   | _      ⇒ (eject … policy)
805   ]
806  ) (Stub ? ?).
807[43: normalize #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ] ]
808whd #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
809#Hi
810[2,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,70,72,74,76,78,80,82,84:
811 >nth_append_second >(injective_S … Hi)
812 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62: @le_n]
813 <minus_n_n #Hj normalize in Hj; @⊥ @Hj
814|4,6,52,54,56,58,60,62,64,66,68: >nth_append_second >(injective_S … Hi)
815 [2,4,6,8,10,12,14,16,18,20,22: @le_n]
816 <minus_n_n #Hj % [1,3,5,7,9,11,13,15,17,19,21: @O ] %
817 [1,3,5,7,9,11,13,15,17,19,21: @short_jump ] @lookup_opt_insert_hit
818]
819 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
820 lapply (sig2 … policy) #Hpolicy elim (Hpolicy i (le_S_S_to_le … Hi) Hj)
821 #p #H elim H #j #Hpj %
822 [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,63,65,67,69,71,73,75,77,79,81,83: @p] %
823 [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,63,65,67,69,71,73,75,77,79,81,83: @j]
824 [2,3,26,27,28,29,30,31,32,33,34: >lookup_opt_insert_miss]
825 [2,4,6,8,10,12,14,16,18,20,22: @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi) ] @Hpj
826qed.
827
828(* not really recursive *)
829let rec jump_expansion_step (program: list labelled_instruction)
830  (old_policy: Σpolicy.jump_in_policy program policy):
831  (Σpolicy.
832    jump_in_policy program policy ∧
833    (jump_in_policy program policy →
834     (∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
835     jmpleq
836       (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
837       (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
838    )
839   ) ≝
840  let labels ≝ create_label_trie program old_policy in
841  let 〈final_pc, final_policy〉 ≝
842    foldl_strong (option Identifier × pseudo_instruction)
843    (λprefix.ℕ × Σpolicy.
844      jump_in_policy prefix policy ∧
845      (jump_in_policy prefix policy →
846       (∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
847       jmpleq
848         (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
849         (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
850      )
851    )
852    program
853    (λprefix.λx.λtl.λprf.λacc.
854      let 〈pc, policy〉 ≝ acc in
855      let 〈label,instr〉 ≝ x in
856      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in
857      let add_instr ≝
858        match instr with
859        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
860        | Call c        ⇒ Some ? (select_call_length labels pc c)
861        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
862        | _             ⇒ None ?
863        ] in
864      let 〈new_pc, new_policy〉 ≝
865        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, short_jump〉 in
866        match add_instr with
867        [ None    ⇒ (* i.e. it's not a jump *)
868          〈add_instruction_size pc long_jump instr, policy〉
869        | Some ai ⇒
870          let new_length ≝ max_length old_length ai in
871          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, new_length〉 policy〉
872        ] in
873      〈new_pc, new_policy〉
874    ) 〈0, Stub ? ?〉 in
875    final_policy.
876[ @conj
877  [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
878    [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
879      lapply (sig2 … policy) #Hacc elim ((proj1 … Hacc) i (le_S_S_to_le … Hi) Hj) #h #n elim n
880      -n #n #Hn
881      % [ @h | % [ @n | normalize nodelta cases instr normalize nodelta
882      [2,3: #x cases (lookup ??? old_policy ?) #y #z @Hn
883      |6: #x #y cases (lookup ??? old_policy ?) #w #z @Hn
884      |1: #pi cases (lookup ??? old_policy ?) #x #y cases (jump_expansion_step_instruction ???)
885        [ @Hn
886        | #z normalize nodelta <Hn @lookup_opt_insert_miss
887          @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
888        ]
889      |4,5: #id cases (lookup ??? old_policy ?) #x #y normalize nodelta <Hn
890        @lookup_opt_insert_miss @bitvector_of_nat_abs
891        @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
892      ] ] ]
893    | #Hi >nth_append_second >(injective_S … Hi)
894      [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
895        [2,3: #x #Hj @⊥ @Hj
896        |6: #x #y #Hj @⊥ @Hj
897        |1: #pi cases pi
898          [35,36,37: #Hj @⊥ @Hj
899          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
900          |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
901          |9,10,14,15: #j normalize nodelta #_
902            % [1,3,5,7: @pc
903              |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
904                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %)
905                #x #y #Hl normalize nodelta
906            % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
907              |2,4,6,8: @lookup_opt_insert_hit
908              ] ]
909          |11,12,13,16,17: #x #j normalize nodelta #_
910            % [1,3,5,7,9: @pc
911              |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
912                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %)         
913                #x #y #Hl normalize nodelta
914            % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
915              |2,4,6,8,10: @lookup_opt_insert_hit
916              ] ]
917          ]
918        |4,5: #j normalize nodelta #_
919          % [1,3: @pc
920            |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
921                #x #y normalize nodelta
922            % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))
923              |3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j))
924              |2,4: @lookup_opt_insert_hit
925              ]
926            ]
927        ]
928      | @le_n
929      ]
930    ]
931  | #Hjip #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
932    [ #Hi >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
933      lapply (sig2 … policy) #Hpolicy normalize nodelta cases instr normalize nodelta
934      [2,3: #x cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #y #z
935        normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
936      |6: #x #y cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #w #z
937        normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
938      |1: #pi cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
939        cases (jump_expansion_step_instruction ???)
940        [ @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
941        | #z normalize nodelta
942          whd in match (snd ℕ jump_expansion_policy ?) >lookup_insert_miss
943          [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
944          | @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
945          ]
946        ]
947      |4,5: #id cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
948        normalize nodelta >lookup_insert_miss
949        [1,3: @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
950        |2,4: @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
951        ]
952      ]
953    | #Hi >nth_append_second >(injective_S … Hi)
954      [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
955        [2,3: #x #Hj @⊥ @Hj
956        |6: #x #y #Hj @⊥ @Hj
957        |1: #pi cases pi
958          [35,36,37: #Hj @⊥ @Hj
959          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
960          |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
961          |9,10,14,15: #j normalize nodelta #_
962            cases (lookup ???? 〈0,short_jump〉) #x #y
963            whd in match (snd ℕ jump_expansion_policy ?)
964            >lookup_insert_hit normalize @jmpleq_max_length
965          |11,12,13,16,17: #z #j normalize nodelta #_
966            cases (lookup ???? 〈0,short_jump〉) #x #y           
967            whd in match (snd ℕ jump_expansion_policy ?)
968            >lookup_insert_hit normalize @jmpleq_max_length
969          ]
970        |4,5: #id #_ cases (lookup ???? 〈0,short_jump〉) #x #y
971              whd in match (snd ℕ jump_expansion_policy ?)
972              >lookup_insert_hit normalize @jmpleq_max_length
973        ]
974      | @le_n
975      ]
976    ]
977  ]
978| @conj
979  [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
980  | #H #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
981  ]
982]
983qed.
984 
985let rec jump_expansion_internal (program: list labelled_instruction)
986  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.jump_in_policy program policy) ≝
987  match n with
988  [ O   ⇒ jump_expansion_start program
989  | S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
990  ].
991[ @(sig2 … (jump_expansion_start program))
992| @(proj1 … (sig2 … (jump_expansion_step program (jump_expansion_internal program m))))
993]
994qed.
995
996(**************************************** START OF POLICY ABSTRACTION ********************)
997
998definition policy_type ≝ Word → jump_length.
999
1000definition jump_expansion': pseudo_assembly_program → policy_type ≝
1001 λprogram.λpc.
1002  let policy ≝ jump_expansion_internal (\snd program) (|\snd program|) in
1003  let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in
1004    j.
1005 
1006definition assembly_1_pseudoinstruction_safe ≝
1007  λprogram: pseudo_assembly_program.
1008  λjump_expansion: policy_type.
1009  λppc: Word.
1010  λpc: Word.
1011  λlookup_labels.
1012  λlookup_datalabels.
1013  λi.
1014  let expansion ≝ jump_expansion ppc in
1015    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
1016    [ None ⇒ None ?
1017    | Some pseudos ⇒
1018      let mapped ≝ map ? ? assembly1 pseudos in
1019      let flattened ≝ flatten ? mapped in
1020      let pc_len ≝ length ? flattened in
1021        Some ? (〈pc_len, flattened〉)
1022    ].
1023 
1024definition construct_costs_safe ≝
1025  λprogram.
1026  λjump_expansion: policy_type.
1027  λpseudo_program_counter: nat.
1028  λprogram_counter: nat.
1029  λcosts: BitVectorTrie Word 16.
1030  λi.
1031  match i with
1032  [ Cost cost ⇒
1033    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1034      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
1035  | _ ⇒
1036    let pc_bv ≝ bitvector_of_nat ? program_counter in
1037    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
1038    let lookup_labels ≝ λx.pc_bv in
1039    let lookup_datalabels ≝ λx.zero ? in
1040    let pc_delta_assembled ≝
1041      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
1042        lookup_labels lookup_datalabels i
1043    in
1044    match pc_delta_assembled with
1045    [ None ⇒ None ?
1046    | Some pc_delta_assembled ⇒
1047      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
1048        Some ? 〈pc_delta + program_counter, costs〉       
1049    ]
1050  ].
1051
1052(* This establishes the correspondence between pseudo program counters and
1053   program counters. It is at the heart of the proof. *)
1054(*CSC: code taken from build_maps *)
1055definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
1056 λinstr_list.
1057 λjump_expansion: policy_type.
1058 λl:list labelled_instruction.
1059 λacc.
1060  foldl ??
1061   (λt,i.
1062       match t with
1063       [ None ⇒ None ?
1064       | Some ppc_pc_map ⇒
1065         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1066         let 〈program_counter, sigma_map〉 ≝ pc_map in
1067         let 〈label, i〉 ≝ i in
1068          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
1069           [ None ⇒ None ?
1070           | Some pc_ignore ⇒
1071              let 〈pc,ignore〉 ≝ pc_ignore in
1072              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
1073       ]) acc l.
1074
1075definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
1076 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).
1077
1078definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
1079 λprogram,jump_expansion,instr_list.
1080  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
1081   [ None ⇒ None …
1082   | Some result ⇒
1083      let 〈ppc,pc_sigma_map〉 ≝ result in
1084      let 〈pc,map〉 ≝ pc_sigma_map in
1085       Some … 〈ppc,pc〉 ].
1086
1087definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
1088 λinstr_list,jump_expansion.
1089  match sigma0 instr_list jump_expansion with
1090  [ None ⇒ None ?
1091  | Some result ⇒
1092    let 〈ppc,pc_sigma_map〉 ≝ result in
1093    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
1094      if gtb pc (2^16) then
1095        None ?
1096      else
1097        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
1098
1099(* stuff about policy *)
1100
1101definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
1102
1103definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
1104
1105lemma eject_policy: ∀p. policy p → policy_type.
1106 #p #pol @(eject … pol)
1107qed.
1108
1109coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
1110
1111definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
1112 λp,policy.
1113  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
1114   [ None ⇒ λabs. ⊥
1115   | Some r ⇒ λ_.r] (sig2 … policy).
1116 cases abs /2/
1117qed.
1118
1119example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
1120 cases daemon.
1121qed.
1122
1123axiom fetch_pseudo_instruction_split:
1124 ∀instr_list,ppc.
1125  ∃pre,suff,lbl.
1126   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
1127
1128lemma sigma00_append:
1129 ∀instr_list,jump_expansion,l1,l2,acc.
1130  sigma00 instr_list jump_expansion (l1@l2) acc =
1131   sigma00 instr_list jump_expansion
1132    l2 (sigma00 instr_list jump_expansion l1 acc).
1133 whd in match sigma00; normalize nodelta;
1134 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
1135qed.
1136
1137lemma sigma00_strict:
1138 ∀instr_list,jump_expansion,l,acc. acc = None ? →
1139  sigma00 instr_list jump_expansion l acc = None ….
1140 #instr_list #jump_expansion #l elim l
1141  [ #acc #H >H %
1142  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
1143qed.
1144
1145lemma policy_ok_prefix_ok:
1146 ∀program.∀pol:policy program.∀suffix,prefix.
1147  prefix@suffix = \snd program →
1148   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
1149 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
1150 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
1151 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
1152 normalize nodelta >sigma00_append
1153 cases (sigma00 ?? prefix ?)
1154  [2: #x #_ % #abs destruct(abs)
1155  | * #abs @⊥ @abs >sigma00_strict % ]
1156qed.
1157
1158lemma policy_ok_prefix_hd_ok:
1159 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
1160  (prefix@[hd])@suffix = \snd program →
1161   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
1162    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1163    let 〈program_counter, sigma_map〉 ≝ pc_map in
1164    let 〈label, i〉 ≝ hd in
1165     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
1166 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
1167 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
1168  (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
1169 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
1170 @pair_elim' #pc #map #EQ4 normalize nodelta
1171 @pair_elim' #l' #i' #EQ5 normalize nodelta
1172 cases (construct_costs_safe ??????) normalize
1173  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
1174qed.
1175
1176definition expand_pseudo_instruction:
1177 ∀program:pseudo_assembly_program.∀pol: policy program.
1178  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
1179  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1180  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1181  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
1182  pc = sigma program pol ppc →
1183  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
1184≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
1185   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
1186    [ None ⇒ let dummy ≝ [ ] in dummy
1187    | Some res ⇒ res ].
1188 [ @⊥ whd in p:(??%??);
1189   generalize in match (sig2 ?? pol) whd in ⊢ (% → ?)
1190   whd in ⊢ (?(??%?) → ?) change in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?) with (sigma00 ????)
1191   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)))
1192   cases (sigma00 ????) in ⊢ (??%? → %) normalize nodelta [#_ * #abs @abs %]
1193   #res #K
1194   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
1195   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?
1196   cases daemon (* CSC: XXXXXXXX Ero qui
1197   
1198    [3: @policy_ok_prefix_ok ]
1199    | sigma00 program pol pre
1200
1201
1202
1203   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
1204   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
1205   per concludere construct_costs_safe ≠ None *)
1206 | >p %]
1207qed.
1208
1209(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1210definition assembly_1_pseudoinstruction':
1211 ∀program:pseudo_assembly_program.∀pol: policy program.
1212  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1213  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1214  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1215  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1216  Σres:(nat × (list Byte)).
1217   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
1218   let 〈len,code〉 ≝ res in
1219    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
1220     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
1221≝ λprogram: pseudo_assembly_program.
1222  λpol: policy program.
1223  λppc: Word.
1224  λlookup_labels.
1225  λlookup_datalabels.
1226  λpi.
1227  λprf1,prf2,prf3.
1228   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
1229    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
1230    | Some res ⇒ res ].
1231 [ @⊥ elim pi in p [*]
1232   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
1233   generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)
1234   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
1235   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
1236   cases daemon
1237 | % [ >p %]
1238   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
1239   (* THIS SHOULD BE TRUE INSTEAD *)
1240   cases daemon]
1241qed.
1242
1243definition assembly_1_pseudoinstruction:
1244 ∀program:pseudo_assembly_program.∀pol: policy program.
1245  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1246  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1247  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1248  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1249   nat × (list Byte)
1250≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
1251   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
1252    prf2 prf3.
1253
1254lemma assembly_1_pseudoinstruction_ok1:
1255 ∀program:pseudo_assembly_program.∀pol: policy program.
1256  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1257  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
1258  ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
1259  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
1260     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
1261   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
1262 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
1263 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
1264 #H1 #_ @H1
1265qed.
1266
1267(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1268definition construct_costs':
1269 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
1270  Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
1271
1272  λprogram.λpol: policy program.λppc,pc,costs,i.
1273   match construct_costs_safe program pol ppc pc costs i with
1274    [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy
1275    | Some res ⇒ res ].
1276 [ cases daemon
1277 | >p %]
1278qed.
1279
1280definition construct_costs ≝
1281 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
1282
1283(*
1284axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
1285axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
1286
1287axiom foldl_strong_step:
1288 ∀A:Type[0].
1289  ∀P: list A → Type[0].
1290   ∀l: list A.
1291    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
1292     ∀acc: P [ ].
1293      ∀Q: ∀prefix. P prefix → Prop.
1294       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
1295        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
1296       Q [ ] acc →
1297        Q l (foldl_strong A P l H acc).
1298(*
1299 #A #P #l #H #acc #Q #HQ #Hacc normalize;
1300 generalize in match
1301  (foldl_strong ?
1302   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
1303   l ? Hacc)
1304 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
1305 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
1306 #K
1307
1308 generalize in match
1309  (foldl_strong ?
1310   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
1311 [2: @H
1312*)
1313
1314axiom foldl_elim:
1315 ∀A:Type[0].
1316  ∀B: Type[0].
1317   ∀H: A → B → A.
1318    ∀acc: A.
1319     ∀l: list B.
1320      ∀Q: A → Prop.
1321       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
1322         Q acc →
1323          Q (foldl A B H acc l).
1324*)
1325
1326lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1327 #A #a #b #EQ destruct //
1328qed.
1329
1330(*
1331lemma tech_pc_sigma00_append_Some:
1332 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1333  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1334   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1335 #program #pol #prefix #costs #label #i #ppc #pc #H
1336  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
1337  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
1338  generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
1339  whd in match sigma0; normalize nodelta;
1340  >foldl_step
1341  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
1342  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
1343  cases (sigma00 program pol prefix) in H ⊢ %
1344   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
1345   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
1346     
1347     normalize nodelta; -H;
1348     
1349 
1350   generalize in match H; -H;
1351  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
1352   [2: whd in ⊢ (??%%)
1353XXX
1354*)
1355
1356axiom construct_costs_sigma:
1357 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
1358  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
1359   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
1360
1361axiom tech_pc_sigma00_append_Some:
1362 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1363  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1364   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1365
1366definition build_maps:
1367 ∀pseudo_program.∀pol:policy pseudo_program.
1368  Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
1369   let 〈labels,costs〉 ≝ res in
1370    ∀id. occurs_exactly_once id (\snd pseudo_program) →
1371     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
1372
1373  λpseudo_program.λpol:policy pseudo_program.
1374  let result ≝
1375   foldl_strong
1376    (option Identifier × pseudo_instruction)
1377    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
1378      let 〈labels,ppc_pc_costs〉 ≝ res in
1379      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
1380      let 〈pc',costs〉 ≝ pc_costs in
1381       And ( And (
1382       And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
1383       (ppc' = length … pre)) (*∧ *)
1384       (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
1385       (∀id. occurs_exactly_once id pre →
1386        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
1387    (\snd pseudo_program)
1388    (λprefix,i,tl,prf,t.
1389      let 〈labels, ppc_pc_costs〉 ≝ t in
1390      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
1391      let 〈pc,costs〉 ≝ pc_costs in
1392       let 〈label, i'〉 ≝ i in
1393       let labels ≝
1394         match label with
1395         [ None ⇒ labels
1396         | Some label ⇒
1397           let program_counter_bv ≝ bitvector_of_nat ? pc in
1398             insert ? ? label program_counter_bv labels]
1399       in
1400         let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
1401          〈labels, 〈S ppc,construct〉〉
1402    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
1403  in
1404   let 〈labels, ppc_pc_costs〉 ≝ result in
1405   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
1406   let 〈pc, costs〉 ≝ pc_costs in
1407    〈labels, costs〉.
1408 [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
1409   generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
1410   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
1411   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
1412   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
1413   | #id normalize nodelta; -labels1; cases label; normalize nodelta
1414     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
1415     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
1416       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
1417        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
1418          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
1419        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
1420          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
1421 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
1422 | generalize in match (sig2 … result) in ⊢ ?;
1423   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?)
1424   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
1425qed.
1426
1427definition assembly:
1428 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝
1429  λp.let 〈preamble, instr_list〉 ≝ p in
1430   λpol.
1431    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
1432    let datalabels ≝ construct_datalabels preamble in
1433    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
1434    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
1435    let result ≝
1436     foldl_strong
1437      (option Identifier × pseudo_instruction)
1438      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
1439        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
1440        let 〈ppc,code〉 ≝ ppc_code in
1441         ∀ppc'.
1442          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
1443          let 〈len,assembledi〉 ≝
1444           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
1445           True)
1446      instr_list
1447      (λprefix,hd,tl,prf,pc_ppc_code.
1448        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
1449        let 〈ppc, code〉 ≝ ppc_code in
1450        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
1451        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
1452        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
1453         〈new_pc, 〈new_ppc, (code @ program)〉〉)
1454      〈(zero ?), 〈(zero ?), [ ]〉〉
1455    in
1456     〈\snd (\snd result), costs〉.
1457 [2,5: %
1458 |*: cases daemon ]
1459qed.
1460
1461definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
1462 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.