source: src/ASM/Assembly.ma @ 1528

Last change on this file since 1528 was 1528, checked in by campbell, 10 years ago

Update most of Assembly.ma with new syntax and identifier maps.
Change positive.ma a little to reduce name clashes.
File size: 66.1 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".
7include alias "arithmetics/nat.ma".
8
9definition assembly_preinstruction ≝
10  λA: Type[0].
11  λaddr_of: A → Byte. (* relative *)
12  λpre: preinstruction A.
13  match pre with
14  [ ADD addr1 addr2 ⇒
15     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
16      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
17      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
18      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
19      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
20      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
21  | ADDC addr1 addr2 ⇒
22     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
23      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
24      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
25      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
26      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
27      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
28  | ANL addrs ⇒
29     match addrs with
30      [ inl addrs ⇒ match addrs with
31         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
32           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
33            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
34            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
35            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
36            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
37            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
38         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
39            let b1 ≝
40             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
41              [ DIRECT b1 ⇒ λ_.b1
42              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
43            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
44             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
45             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
46             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
47         ]
48      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
49         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
50          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
51          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
52          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
53  | CLR addr ⇒
54     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
55      [ ACC_A ⇒ λ_.
56         [ ([[true; true; true; false; false; true; false; false]]) ]
57      | CARRY ⇒ λ_.
58         [ ([[true; true; false; false; false; false; true; true]]) ]
59      | BIT_ADDR b1 ⇒ λ_.
60         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
61      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
62  | CPL addr ⇒
63     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
64      [ ACC_A ⇒ λ_.
65         [ ([[true; true; true; true; false; true; false; false]]) ]
66      | CARRY ⇒ λ_.
67         [ ([[true; false; true; true; false; false; true; true]]) ]
68      | BIT_ADDR b1 ⇒ λ_.
69         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
70      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
71  | DA addr ⇒
72     [ ([[true; true; false; true; false; true; false; false]]) ]
73  | DEC addr ⇒
74     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
75      [ ACC_A ⇒ λ_.
76         [ ([[false; false; false; true; false; true; false; false]]) ]
77      | REGISTER r ⇒ λ_.
78         [ ([[false; false; false; true; true]]) @@ r ]
79      | DIRECT b1 ⇒ λ_.
80         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
81      | INDIRECT i1 ⇒ λ_.
82         [ ([[false; false; false; true; false; true; true; i1]]) ]
83      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
84      | DJNZ addr1 addr2 ⇒
85         let b2 ≝ addr_of addr2 in
86         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
87          [ REGISTER r ⇒ λ_.
88             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
89          | DIRECT b1 ⇒ λ_.
90             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
91          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
92      | JC addr ⇒
93        let b1 ≝ addr_of addr in
94          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
95      | JNC addr ⇒
96         let b1 ≝ addr_of addr in
97           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
98      | JZ addr ⇒
99         let b1 ≝ addr_of addr in
100           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
101      | JNZ addr ⇒
102         let b1 ≝ addr_of addr in
103           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
104      | JB addr1 addr2 ⇒
105         let b2 ≝ addr_of addr2 in
106         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
107          [ BIT_ADDR b1 ⇒ λ_.
108             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
109          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
110      | JNB addr1 addr2 ⇒
111         let b2 ≝ addr_of addr2 in
112         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
113          [ BIT_ADDR b1 ⇒ λ_.
114             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
115          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
116      | JBC addr1 addr2 ⇒
117         let b2 ≝ addr_of addr2 in
118         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
119          [ BIT_ADDR b1 ⇒ λ_.
120             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
121          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
122      | CJNE addrs addr3 ⇒
123         let b3 ≝ addr_of addr3 in
124         match addrs with
125          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
126             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
127              [ DIRECT b1 ⇒ λ_.
128                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
129              | DATA b1 ⇒ λ_.
130                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
131              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
132          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
133             let b2 ≝
134              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
135               [ DATA b2 ⇒ λ_. b2
136               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
137             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
138              [ REGISTER r ⇒ λ_.
139                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
140              | INDIRECT i1 ⇒ λ_.
141                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
142              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
143         ]
144  | DIV addr1 addr2 ⇒
145     [ ([[true;false;false;false;false;true;false;false]]) ]
146  | INC addr ⇒
147     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
148      [ ACC_A ⇒ λ_.
149         [ ([[false;false;false;false;false;true;false;false]]) ]         
150      | REGISTER r ⇒ λ_.
151         [ ([[false;false;false;false;true]]) @@ r ]
152      | DIRECT b1 ⇒ λ_.
153         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
154      | INDIRECT i1 ⇒ λ_.
155        [ ([[false; false; false; false; false; true; true; i1]]) ]
156      | DPTR ⇒ λ_.
157        [ ([[true;false;true;false;false;false;true;true]]) ]
158      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
159  | MOV addrs ⇒
160     match addrs with
161      [ inl addrs ⇒
162         match addrs with
163          [ inl addrs ⇒
164             match addrs with
165              [ inl addrs ⇒
166                 match addrs with
167                  [ inl addrs ⇒
168                     match addrs with
169                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
170                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
171                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
172                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
173                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
174                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
175                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
176                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
177                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
178                          [ REGISTER r ⇒ λ_.
179                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
180                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
181                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
182                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
183                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
184                          | INDIRECT i1 ⇒ λ_.
185                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
186                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
187                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
188                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
189                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
190                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
191                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
192                     let b1 ≝
193                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
194                       [ DIRECT b1 ⇒ λ_. b1
195                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
196                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
197                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
198                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
199                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
200                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
201                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
202                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
203              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
204                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
205                  [ DATA16 w ⇒ λ_.
206                     let b1_b2 ≝ split ? 8 8 w in
207                     let b1 ≝ \fst b1_b2 in
208                     let b2 ≝ \snd b1_b2 in
209                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
210                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
211          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
212             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
213              [ BIT_ADDR b1 ⇒ λ_.
214                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
215              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
216      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
217         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
218          [ BIT_ADDR b1 ⇒ λ_.
219             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
220          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
221  | MOVX addrs ⇒
222     match addrs with
223      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
224         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
225          [ EXT_INDIRECT i1 ⇒ λ_.
226             [ ([[true;true;true;false;false;false;true;i1]]) ]
227          | EXT_INDIRECT_DPTR ⇒ λ_.
228             [ ([[true;true;true;false;false;false;false;false]]) ]
229          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
230      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
231         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
232          [ EXT_INDIRECT i1 ⇒ λ_.
233             [ ([[true;true;true;true;false;false;true;i1]]) ]
234          | EXT_INDIRECT_DPTR ⇒ λ_.
235             [ ([[true;true;true;true;false;false;false;false]]) ]
236          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
237  | MUL addr1 addr2 ⇒
238     [ ([[true;false;true;false;false;true;false;false]]) ]
239  | NOP ⇒
240     [ ([[false;false;false;false;false;false;false;false]]) ]
241  | ORL addrs ⇒
242     match addrs with
243      [ inl addrs ⇒
244         match addrs with
245          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
246             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
247             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
248             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
249             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
250             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
251             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
252          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
253            let b1 ≝
254              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
255               [ DIRECT b1 ⇒ λ_. b1
256               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
257             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
258              [ ACC_A ⇒ λ_.
259                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
260              | DATA b2 ⇒ λ_.
261                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
262              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
263      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
264         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
265          [ BIT_ADDR b1 ⇒ λ_.
266             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
267          | N_BIT_ADDR b1 ⇒ λ_.
268             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
269          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
270  | POP addr ⇒
271     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
272      [ DIRECT b1 ⇒ λ_.
273         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
274      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
275  | PUSH addr ⇒
276     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
277      [ DIRECT b1 ⇒ λ_.
278         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
279      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
280  | RET ⇒
281     [ ([[false;false;true;false;false;false;true;false]]) ]
282  | RETI ⇒
283     [ ([[false;false;true;true;false;false;true;false]]) ]
284  | RL addr ⇒
285     [ ([[false;false;true;false;false;false;true;true]]) ]
286  | RLC addr ⇒
287     [ ([[false;false;true;true;false;false;true;true]]) ]
288  | RR addr ⇒
289     [ ([[false;false;false;false;false;false;true;true]]) ]
290  | RRC addr ⇒
291     [ ([[false;false;false;true;false;false;true;true]]) ]
292  | SETB addr ⇒     
293     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
294      [ CARRY ⇒ λ_.
295         [ ([[true;true;false;true;false;false;true;true]]) ]
296      | BIT_ADDR b1 ⇒ λ_.
297         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
298      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
299  | SUBB addr1 addr2 ⇒
300     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
301      [ REGISTER r ⇒ λ_.
302         [ ([[true;false;false;true;true]]) @@ r ]
303      | DIRECT b1 ⇒ λ_.
304         [ ([[true;false;false;true;false;true;false;true]]); b1]
305      | INDIRECT i1 ⇒ λ_.
306         [ ([[true;false;false;true;false;true;true;i1]]) ]
307      | DATA b1 ⇒ λ_.
308         [ ([[true;false;false;true;false;true;false;false]]); b1]
309      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
310  | SWAP addr ⇒
311     [ ([[true;true;false;false;false;true;false;false]]) ]
312  | XCH addr1 addr2 ⇒
313     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
314      [ REGISTER r ⇒ λ_.
315         [ ([[true;true;false;false;true]]) @@ r ]
316      | DIRECT b1 ⇒ λ_.
317         [ ([[true;true;false;false;false;true;false;true]]); b1]
318      | INDIRECT i1 ⇒ λ_.
319         [ ([[true;true;false;false;false;true;true;i1]]) ]
320      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
321  | XCHD addr1 addr2 ⇒
322     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
323      [ INDIRECT i1 ⇒ λ_.
324         [ ([[true;true;false;true;false;true;true;i1]]) ]
325      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
326  | XRL addrs ⇒
327     match addrs with
328      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
329         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
330          [ REGISTER r ⇒ λ_.
331             [ ([[false;true;true;false;true]]) @@ r ]
332          | DIRECT b1 ⇒ λ_.
333             [ ([[false;true;true;false;false;true;false;true]]); b1]
334          | INDIRECT i1 ⇒ λ_.
335             [ ([[false;true;true;false;false;true;true;i1]]) ]
336          | DATA b1 ⇒ λ_.
337             [ ([[false;true;true;false;false;true;false;false]]); b1]
338          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
339      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
340         let b1 ≝
341          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
342           [ DIRECT b1 ⇒ λ_. b1
343           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
344         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
345          [ ACC_A ⇒ λ_.
346             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
347          | DATA b2 ⇒ λ_.
348             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
349          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
350       ].
351
352definition assembly1 ≝
353 λi: instruction.
354 match i with
355  [ ACALL addr ⇒
356     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
357      [ ADDR11 w ⇒ λ_.
358         let v1_v2 ≝ split ? 3 8 w in
359         let v1 ≝ \fst v1_v2 in
360         let v2 ≝ \snd v1_v2 in
361          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
362      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
363  | AJMP addr ⇒
364     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
365      [ ADDR11 w ⇒ λ_.
366         let v1_v2 ≝ split ? 3 8 w in
367         let v1 ≝ \fst v1_v2 in
368         let v2 ≝ \snd v1_v2 in
369          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
370      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
371  | JMP adptr ⇒
372     [ ([[false;true;true;true;false;false;true;true]]) ]
373  | LCALL addr ⇒
374     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
375      [ ADDR16 w ⇒ λ_.
376         let b1_b2 ≝ split ? 8 8 w in
377         let b1 ≝ \fst b1_b2 in
378         let b2 ≝ \snd b1_b2 in
379          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
380      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
381  | LJMP addr ⇒
382     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
383      [ ADDR16 w ⇒ λ_.
384         let b1_b2 ≝ split ? 8 8 w in
385         let b1 ≝ \fst b1_b2 in
386         let b2 ≝ \snd b1_b2 in
387          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
388      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
389  | MOVC addr1 addr2 ⇒
390     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
391      [ ACC_DPTR ⇒ λ_.
392         [ ([[true;false;false;true;false;false;true;true]]) ]
393      | ACC_PC ⇒ λ_.
394         [ ([[true;false;false;false;false;false;true;true]]) ]
395      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
396  | SJMP addr ⇒
397     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
398      [ RELATIVE b1 ⇒ λ_.
399         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
400      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
401  | RealInstruction instr ⇒
402    assembly_preinstruction [[ relative ]]
403      (λx.
404        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
405        [ RELATIVE r ⇒ λ_. r
406        | _ ⇒ λabsd. ⊥
407        ] (subaddressing_modein … x)) instr
408  ].
409  cases absd
410qed.
411
412inductive jump_length: Type[0] ≝
413  | short_jump: jump_length
414  | medium_jump: jump_length
415  | long_jump: jump_length.
416
417(* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
418definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16.
419
420definition expand_relative_jump_internal:
421 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
422 option (list instruction)
423 ≝
424  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
425  match jmp_len with
426  [ short_jump ⇒
427     let lookup_address ≝ lookup_labels jmp in
428     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
429     let 〈upper, lower〉 ≝ split ? 8 8 result in
430     if eq_bv ? upper (zero 8) then
431      let address ≝ RELATIVE lower in
432       Some ? [ RealInstruction (i address) ]
433     else
434       None ?
435  | medium_jump ⇒ None …
436  | long_jump ⇒
437    Some ?
438    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
439      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
440      LJMP (ADDR16 (lookup_labels jmp))
441    ]
442  ].
443  @ I
444qed.
445
446definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
447  λlookup_labels.
448  λjmp_len: jump_length.
449  λpc.
450  λi: preinstruction Identifier.
451  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
452  match i with
453  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
454  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
455  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
456  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
457  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
458  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
459  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
460  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
461  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
462  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
463  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
464  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
465  | INC arg ⇒ Some ? [ INC ? arg ]
466  | DEC arg ⇒ Some ? [ DEC ? arg ]
467  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
468  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
469  | DA arg ⇒ Some ? [ DA ? arg ]
470  | ANL arg ⇒ Some ? [ ANL ? arg ]
471  | ORL arg ⇒ Some ? [ ORL ? arg ]
472  | XRL arg ⇒ Some ? [ XRL ? arg ]
473  | CLR arg ⇒ Some ? [ CLR ? arg ]
474  | CPL arg ⇒ Some ? [ CPL ? arg ]
475  | RL arg ⇒ Some ? [ RL ? arg ]
476  | RR arg ⇒ Some ? [ RR ? arg ]
477  | RLC arg ⇒ Some ? [ RLC ? arg ]
478  | RRC arg ⇒ Some ? [ RRC ? arg ]
479  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
480  | MOV arg ⇒ Some ? [ MOV ? arg ]
481  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
482  | SETB arg ⇒ Some ? [ SETB ? arg ]
483  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
484  | POP arg ⇒ Some ? [ POP ? arg ]
485  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
486  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
487  | RET ⇒ Some ? [ RET ? ]
488  | RETI ⇒ Some ? [ RETI ? ]
489  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
490  ].
491
492definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
493  λlookup_labels.
494  λlookup_datalabels.
495  λpc.
496  λjmp_len.
497  λi.
498  match i with
499  [ Cost cost ⇒ Some ? [ ]
500  | Comment comment ⇒ Some ? [ ]
501  | Call call ⇒
502    match jmp_len with
503    [ short_jump ⇒ None ?
504    | medium_jump ⇒
505      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
506      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
507      if eq_bv ? ignore fst_5 then
508        let address ≝ ADDR11 address in
509          Some ? ([ ACALL address ])
510      else
511        None ?
512    | long_jump ⇒
513      let address ≝ ADDR16 (lookup_labels call) in
514        Some ? [ LCALL address ]
515    ]
516  | Mov d trgt ⇒
517    let address ≝ DATA16 (lookup_datalabels trgt) in
518      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
519  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
520  | Jmp jmp ⇒
521    match jmp_len with
522    [ short_jump ⇒
523      let lookup_address ≝ lookup_labels jmp in
524      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
525      let 〈upper, lower〉 ≝ split ? 8 8 result in
526      if eq_bv ? upper (zero 8) then
527        let address ≝ RELATIVE lower in
528          Some ? [ SJMP address ]
529      else
530        None ?
531    | medium_jump ⇒
532      let address ≝ lookup_labels jmp in
533      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
534      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
535      if eq_bv ? fst_5_addr fst_5_pc then
536        let address ≝ ADDR11 rest_addr in
537          Some ? ([ AJMP address ])
538      else
539        None ?
540    | long_jump ⇒
541      let address ≝ ADDR16 (lookup_labels jmp) in
542        Some ? [ LJMP address ]
543    ]
544  ].
545  @ I
546qed.
547
548(* label_map: identifier ↦ 〈instruction number, address〉 *)
549definition label_map ≝ identifier_map ASMTag (nat × nat).
550
551definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
552  λpc.λjmp_len.λinstr.
553  let bv_pc ≝ bitvector_of_nat 16 pc in
554  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
555  let bv: list (BitVector 8) ≝ match ilist with
556    [ None   ⇒ (* hmm, this shouldn't happen *) [ ]
557    | Some l ⇒ flatten … (map … assembly1 l)
558    ] in
559  pc + (|bv|).
560 
561definition is_label ≝
562  λx:labelled_instruction.λl:Identifier.
563  let 〈lbl,instr〉 ≝ x in
564  match lbl with
565  [ Some l' ⇒ l' = l
566  | _       ⇒ False
567  ].
568 
569lemma label_does_not_occur:
570  ∀i,p,l.
571  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
572 #i #p #l generalize in match i; elim p
573 [ #i >nth_nil #H @⊥ @H
574 | #h #t #IH #i cases i -i
575   [ cases h #hi #hp cases hi
576     [ normalize #H @⊥ @H
577     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
578       whd in Heq; >Heq
579       >eq_identifier_refl //
580     ]
581   | #i #H whd in match (does_not_occur ??);
582     whd in match (instruction_matches_identifier ??);
583     cases h #hi #hp cases hi normalize nodelta
584     [ @(IH i) @H
585     | #l' @eq_identifier_elim
586       [ normalize //
587       | normalize #_ @(IH i) @H
588       ]
589     ]
590   ]
591 ]
592qed. 
593
594(* lemma coerc_sigma:
595 ∀A,P.∀p:A.P p → Σx:A.P x.
596#A #P #a #p % [ @a | /2/]
597qed.
598coercion coerc_sigma:∀A,P.∀p:A.P p → Σx:A.P x
599≝ coerc_sigma on p: ? to (Sig ??). *)
600
601lemma coerc_pair_sigma:
602 ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
603#A #B #P * #a #b #p % [@a | /2/]
604qed.
605coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
606≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
607
608let rec create_label_map (program: list labelled_instruction)
609  (policy: jump_expansion_policy):
610  (Σlabels:label_map.
611    ∀i:ℕ.lt i (|program|) (* XXX using < causes (false?) ambiguity *) →
612    ∀l.occurs_exactly_once l program →
613    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
614    ∃a.lookup … labels l = Some ? 〈i,a〉
615  ) ≝
616  let 〈final_pc, final_labels〉 ≝
617    foldl_strong (option Identifier × pseudo_instruction)
618    (λprefix.ℕ × (Σlabels.
619      ∀i:ℕ.i < |prefix| →
620      ∀l.occurs_exactly_once l prefix →
621      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
622      ∃a.lookup … labels l = Some ? 〈i,a〉)
623    )
624    program
625    (λprefix.λx.λtl.λprf.λacc.
626     let 〈pc,labels〉 ≝ acc in
627     let 〈label,instr〉 ≝ x in
628          let new_labels ≝
629          match label with
630          [ None   ⇒ labels
631          | Some l ⇒ add … labels l 〈|prefix|, pc〉
632          ] in
633          let jmp_len ≝ \snd (bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
634          〈add_instruction_size pc jmp_len instr, new_labels〉
635    ) 〈0, empty_map …〉 in
636    final_labels.
637[ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
638  [ #Hi #l normalize nodelta; cases label normalize nodelta
639    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
640      lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
641      % [ @addr | @Haddr ]
642    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
643      @eq_identifier_elim #Heq #Hocc
644      [ normalize in Hocc;
645        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
646        @⊥ @(absurd … Hocc)
647      | normalize nodelta lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
648        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
649        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
650        ]
651      ]
652      >(label_does_not_occur i … Hl) normalize nodelta @nmk //
653    ]
654  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
655    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
656      [ normalize nodelta #H @⊥ @H
657      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
658      ]
659    | @le_n
660    ]
661  ]
662| #i #Hi #l #Hl @⊥ @Hl
663]
664qed.
665
666definition select_reljump_length: label_map → ℕ → Identifier → jump_length ≝
667  λlabels.λpc.λlbl.
668  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
669  if leb pc addr (* forward jump *)
670  then if leb (addr - pc) 126
671       then short_jump
672       else long_jump
673  else if leb (pc - addr) 129
674       then short_jump
675       else long_jump.
676
677definition select_call_length: label_map → ℕ → Identifier → jump_length ≝
678  λlabels.λpc_nat.λlbl.
679  let pc ≝ bitvector_of_nat 16 pc_nat in
680  let addr ≝ bitvector_of_nat 16 (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
681  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
682  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
683  if eq_bv ? fst_5_addr fst_5_pc
684  then medium_jump
685  else long_jump.
686 
687definition select_jump_length: label_map → ℕ → Identifier → jump_length ≝
688  λlabels.λpc.λlbl.
689  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
690  if leb pc addr
691  then if leb (addr - pc) 126
692       then short_jump
693       else select_call_length labels pc lbl
694  else if leb (pc - addr) 129
695       then short_jump
696       else select_call_length labels pc lbl.
697 
698definition jump_expansion_step_instruction: label_map → ℕ →
699  preinstruction Identifier → option jump_length ≝
700  λlabels.λpc.λi.
701  match i with
702  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
703  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
704  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
705  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
706  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
707  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
708  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
709  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
710  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
711  | _        ⇒ None ?
712  ].
713
714definition max_length: jump_length → jump_length → jump_length ≝
715  λj1.λj2.
716  match j1 with
717  [ long_jump   ⇒ long_jump
718  | medium_jump ⇒
719    match j2 with
720    [ long_jump ⇒ long_jump
721    | _         ⇒ medium_jump
722    ]
723  | short_jump  ⇒ j2
724  ].
725
726definition jmpleq: jump_length → jump_length → Prop ≝
727  λj1.λj2.
728  match j1 with
729  [ short_jump  ⇒ True
730  | medium_jump ⇒
731    match j2 with
732    [ short_jump ⇒ False
733    | _          ⇒ True
734    ]
735  | long_jump   ⇒
736    match j2 with
737    [ long_jump ⇒ True
738    | _         ⇒ False
739    ]
740  ].
741
742lemma jmpleq_max_length: ∀x,y.jmpleq y (max_length y x).
743 #x #y
744 cases y
745 [ //
746 | cases x //
747 | //
748 ]
749qed.
750
751definition is_jump' ≝
752  λx:preinstruction Identifier.
753  match x with
754  [ JC _ ⇒ True
755  | JNC _ ⇒ True
756  | JZ _ ⇒ True
757  | JNZ _ ⇒ True
758  | JB _ _ ⇒ True
759  | JNB _ _ ⇒ True
760  | JBC _ _ ⇒ True
761  | CJNE _ _ ⇒ True
762  | DJNZ _ _ ⇒ True
763  | _ ⇒ False
764  ].
765 
766definition is_jump ≝
767  λx:labelled_instruction.
768  let 〈label,instr〉 ≝ x in
769  match instr with
770  [ Instruction i   ⇒ is_jump' i
771  | Call _ ⇒ True
772  | Jmp _ ⇒ True
773  | _ ⇒ False
774  ].
775
776definition jump_in_policy ≝
777  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
778  ∀i:ℕ.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
779  ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉.
780 
781axiom bitvector_of_nat_abs:
782  ∀x,y:ℕ.x ≠ y → ¬eq_bv 16 (bitvector_of_nat 16 x) (bitvector_of_nat 16 y).
783 
784let rec jump_expansion_start (program: list labelled_instruction):
785  (Σpolicy.jump_in_policy program policy) ≝
786  foldl_strong (option Identifier × pseudo_instruction)
787  (λprefix.Σpolicy.jump_in_policy prefix policy)
788  program
789  (λprefix.λx.λtl.λprf.λpolicy.
790   let 〈label,instr〉 ≝ x in
791   match instr with
792   [ Instruction i ⇒ match i with
793     [ JC _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
794     | JNC _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
795     | JZ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
796     | JNZ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
797     | JB _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
798     | JNB _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
799     | JBC _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
800     | CJNE _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
801     | DJNZ _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
802     | _ ⇒ (eject … policy)
803     ]
804   | Call c ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
805   | Jmp j  ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
806   | _      ⇒ (eject … policy)
807   ]
808  ) (Stub ? ?).
809[43: normalize #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ] ]
810whd #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
811#Hi
812[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:
813 >nth_append_second >(injective_S … Hi)
814 [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]
815 <minus_n_n #Hj normalize in Hj; @⊥ @Hj
816|4,6,52,54,56,58,60,62,64,66,68: >nth_append_second >(injective_S … Hi)
817 [2,4,6,8,10,12,14,16,18,20,22: @le_n]
818 <minus_n_n #Hj % [1,3,5,7,9,11,13,15,17,19,21: @O ] %
819 [1,3,5,7,9,11,13,15,17,19,21: @short_jump ] @lookup_opt_insert_hit
820]
821 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
822 lapply (sig2 … policy) #Hpolicy elim (Hpolicy i (le_S_S_to_le … Hi) Hj)
823 #p #H elim H #j #Hpj %
824 [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] %
825 [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]
826 [2,3,26,27,28,29,30,31,32,33,34: >lookup_opt_insert_miss]
827 [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
828qed.
829
830(* not really recursive *)
831let rec jump_expansion_step (program: list labelled_instruction)
832  (old_policy: Σpolicy.jump_in_policy program policy):
833  (Σpolicy.
834    And (jump_in_policy program policy) (* XXX ∧ causes ambiguity *)
835    (jump_in_policy program policy →
836     (∀i.lt i (|program|) (* XXX < causes ambiguity *) → is_jump (nth i ? program 〈None ?, Comment []〉) →
837     jmpleq
838       (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
839       (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
840    )
841   ) ≝
842  let labels ≝ create_label_map program old_policy in
843  let 〈final_pc, final_policy〉 ≝
844    foldl_strong (option Identifier × pseudo_instruction)
845    (λprefix.ℕ × Σpolicy.
846      jump_in_policy prefix policy ∧
847      (jump_in_policy prefix policy →
848       (∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
849       jmpleq
850         (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
851         (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
852      )
853    )
854    program
855    (λprefix.λx.λtl.λprf.λacc.
856      let 〈pc, policy〉 ≝ acc in
857      let 〈label,instr〉 ≝ x in
858      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in
859      let add_instr ≝
860        match instr with
861        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
862        | Call c        ⇒ Some ? (select_call_length labels pc c)
863        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
864        | _             ⇒ None ?
865        ] in
866      let 〈new_pc, new_policy〉 ≝
867        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, short_jump〉 in
868        match add_instr with
869        [ None    ⇒ (* i.e. it's not a jump *)
870          〈add_instruction_size pc long_jump instr, policy〉
871        | Some ai ⇒
872          let new_length ≝ max_length old_length ai in
873          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, new_length〉 policy〉
874        ] in
875      〈new_pc, new_policy〉
876    ) 〈0, Stub ? ?〉 in
877    final_policy.
878[ @conj
879  [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
880    [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
881      lapply (sig2 … policy) #Hacc elim ((proj1 … Hacc) i (le_S_S_to_le … Hi) Hj) #h #n elim n
882      -n #n #Hn
883      % [ @h | % [ @n | normalize nodelta cases instr normalize nodelta
884      [2,3: #x cases (lookup ??? old_policy ?) #y #z @Hn
885      |6: #x #y cases (lookup ??? old_policy ?) #w #z @Hn
886      |1: #pi cases (lookup ??? old_policy ?) #x #y cases (jump_expansion_step_instruction ???)
887        [ @Hn
888        | #z normalize nodelta <Hn @lookup_opt_insert_miss
889          @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
890        ]
891      |4,5: #id cases (lookup ??? old_policy ?) #x #y normalize nodelta <Hn
892        @lookup_opt_insert_miss @bitvector_of_nat_abs
893        @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
894      ] ] ]
895    | #Hi >nth_append_second >(injective_S … Hi)
896      [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
897        [2,3: #x #Hj @⊥ @Hj
898        |6: #x #y #Hj @⊥ @Hj
899        |1: #pi cases pi
900          [35,36,37: #Hj @⊥ @Hj
901          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
902          |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
903          |9,10,14,15: #j normalize nodelta #_
904            % [1,3,5,7: @pc
905              |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
906                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %);
907                #x #y #Hl normalize nodelta
908            % [1,3,5,7: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j))
909              |2,4,6,8: @lookup_opt_insert_hit
910              ] ]
911          |11,12,13,16,17: #x #j normalize nodelta #_
912            % [1,3,5,7,9: @pc
913              |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
914                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %);
915                #x #y #Hl normalize nodelta
916            % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j))
917              |2,4,6,8,10: @lookup_opt_insert_hit
918              ] ]
919          ]
920        |4,5: #j normalize nodelta #_
921          % [1,3: @pc
922            |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
923                #x #y normalize nodelta
924            % [1: @(max_length y (select_jump_length (create_label_map program old_policy) pc j))
925              |3: @(max_length y (select_call_length (create_label_map program old_policy) pc j))
926              |2,4: @lookup_opt_insert_hit
927              ]
928            ]
929        ]
930      | @le_n
931      ]
932    ]
933  | #Hjip #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
934    [ #Hi >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
935      lapply (sig2 … policy) #Hpolicy normalize nodelta cases instr normalize nodelta
936      [2,3: #x cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #y #z
937        normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
938      |6: #x #y cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #w #z
939        normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
940      |1: #pi cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
941        cases (jump_expansion_step_instruction ???)
942        [ @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
943        | #z normalize nodelta
944          whd in match (snd ℕ jump_expansion_policy ?); >lookup_insert_miss
945          [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
946          | @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
947          ]
948        ]
949      |4,5: #id cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
950        normalize nodelta >lookup_insert_miss
951        [1,3: @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
952        |2,4: @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
953        ]
954      ]
955    | #Hi >nth_append_second >(injective_S … Hi)
956      [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
957        [2,3: #x #Hj @⊥ @Hj
958        |6: #x #y #Hj @⊥ @Hj
959        |1: #pi cases pi
960          [35,36,37: #Hj @⊥ @Hj
961          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
962          |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
963          |9,10,14,15: #j normalize nodelta #_
964            cases (lookup ???? 〈0,short_jump〉) #x #y
965            whd in match (snd ℕ jump_expansion_policy ?);
966            >lookup_insert_hit normalize @jmpleq_max_length
967          |11,12,13,16,17: #z #j normalize nodelta #_
968            cases (lookup ???? 〈0,short_jump〉) #x #y           
969            whd in match (snd ℕ jump_expansion_policy ?);
970            >lookup_insert_hit normalize @jmpleq_max_length
971          ]
972        |4,5: #id #_ cases (lookup ???? 〈0,short_jump〉) #x #y
973              whd in match (snd ℕ jump_expansion_policy ?);
974              >lookup_insert_hit normalize @jmpleq_max_length
975        ]
976      | @le_n
977      ]
978    ]
979  ]
980| @conj
981  [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
982  | #H #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
983  ]
984]
985qed.
986 
987let rec jump_expansion_internal (program: list labelled_instruction)
988  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.jump_in_policy program policy) ≝
989  match n with
990  [ O   ⇒ jump_expansion_start program
991  | S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
992  ].
993[ @(sig2 … (jump_expansion_start program))
994| @(proj1 … (sig2 … (jump_expansion_step program (jump_expansion_internal program m))))
995]
996qed.
997
998(**************************************** START OF POLICY ABSTRACTION ********************)
999
1000definition policy_type ≝ Word → jump_length.
1001
1002definition jump_expansion': pseudo_assembly_program → policy_type ≝
1003 λprogram.λpc.
1004  let policy ≝ jump_expansion_internal (\snd program) (|\snd program|) in
1005  let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in
1006    j.
1007 
1008definition assembly_1_pseudoinstruction_safe ≝
1009  λprogram: pseudo_assembly_program.
1010  λjump_expansion: policy_type.
1011  λppc: Word.
1012  λpc: Word.
1013  λlookup_labels.
1014  λlookup_datalabels.
1015  λi.
1016  let expansion ≝ jump_expansion ppc in
1017    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
1018    [ None ⇒ None ?
1019    | Some pseudos ⇒
1020      let mapped ≝ map ? ? assembly1 pseudos in
1021      let flattened ≝ flatten ? mapped in
1022      let pc_len ≝ length ? flattened in
1023        Some ? (〈pc_len, flattened〉)
1024    ].
1025 
1026definition construct_costs_safe ≝
1027  λprogram.
1028  λjump_expansion: policy_type.
1029  λpseudo_program_counter: nat.
1030  λprogram_counter: nat.
1031  λcosts: BitVectorTrie costlabel 16.
1032  λi.
1033  match i with
1034  [ Cost cost ⇒
1035    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1036      Some ? 〈program_counter, (insert … program_counter_bv cost costs)〉
1037  | _ ⇒
1038    let pc_bv ≝ bitvector_of_nat ? program_counter in
1039    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
1040    let lookup_labels ≝ λx.pc_bv in
1041    let lookup_datalabels ≝ λx.zero ? in
1042    let pc_delta_assembled ≝
1043      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
1044        lookup_labels lookup_datalabels i
1045    in
1046    match pc_delta_assembled with
1047    [ None ⇒ None ?
1048    | Some pc_delta_assembled ⇒
1049      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
1050        Some ? 〈pc_delta + program_counter, costs〉       
1051    ]
1052  ].
1053
1054(* This establishes the correspondence between pseudo program counters and
1055   program counters. It is at the heart of the proof. *)
1056(*CSC: code taken from build_maps *)
1057definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
1058 λinstr_list.
1059 λjump_expansion: policy_type.
1060 λl:list labelled_instruction.
1061 λacc.
1062  foldl ??
1063   (λt,i.
1064       match t with
1065       [ None ⇒ None ?
1066       | Some ppc_pc_map ⇒
1067         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1068         let 〈program_counter, sigma_map〉 ≝ pc_map in
1069         let 〈label, i〉 ≝ i in
1070          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
1071           [ None ⇒ None ?
1072           | Some pc_ignore ⇒
1073              let 〈pc,ignore〉 ≝ pc_ignore in
1074              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
1075       ]) acc l.
1076
1077definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
1078 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).
1079
1080definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
1081 λprogram,jump_expansion,instr_list.
1082  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
1083   [ None ⇒ None …
1084   | Some result ⇒
1085      let 〈ppc,pc_sigma_map〉 ≝ result in
1086      let 〈pc,map〉 ≝ pc_sigma_map in
1087       Some … 〈ppc,pc〉 ].
1088
1089definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
1090 λinstr_list,jump_expansion.
1091  match sigma0 instr_list jump_expansion with
1092  [ None ⇒ None ?
1093  | Some result ⇒
1094    let 〈ppc,pc_sigma_map〉 ≝ result in
1095    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
1096      if gtb pc (2^16) then
1097        None ?
1098      else
1099        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
1100
1101(* stuff about policy *)
1102
1103definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
1104
1105definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
1106
1107lemma eject_policy: ∀p. policy p → policy_type.
1108 #p #pol @(eject … pol)
1109qed.
1110
1111coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
1112
1113definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
1114 λp,policy.
1115  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
1116   [ None ⇒ λabs. ⊥
1117   | Some r ⇒ λ_.r] (sig2 … policy).
1118 cases abs /2/
1119qed.
1120
1121example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
1122 cases daemon.
1123qed.
1124
1125axiom fetch_pseudo_instruction_split:
1126 ∀instr_list,ppc.
1127  ∃pre,suff,lbl.
1128   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
1129
1130lemma sigma00_append:
1131 ∀instr_list,jump_expansion,l1,l2,acc.
1132  sigma00 instr_list jump_expansion (l1@l2) acc =
1133   sigma00 instr_list jump_expansion
1134    l2 (sigma00 instr_list jump_expansion l1 acc).
1135 whd in match sigma00; normalize nodelta;
1136 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
1137qed.
1138
1139lemma sigma00_strict:
1140 ∀instr_list,jump_expansion,l,acc. acc = None ? →
1141  sigma00 instr_list jump_expansion l acc = None ….
1142 #instr_list #jump_expansion #l elim l
1143  [ #acc #H >H %
1144  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
1145qed.
1146
1147lemma policy_ok_prefix_ok:
1148 ∀program.∀pol:policy program.∀suffix,prefix.
1149  prefix@suffix = \snd program →
1150   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
1151 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
1152 generalize in match (sig2 ?? pol); whd in prf:(???%); <prf in pol; #pol
1153 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
1154 normalize nodelta >sigma00_append
1155 cases (sigma00 ?? prefix ?)
1156  [2: #x #_ % #abs destruct(abs)
1157  | * #abs @⊥ @abs >sigma00_strict % ]
1158qed.
1159
1160lemma policy_ok_prefix_hd_ok:
1161 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
1162  (prefix@[hd])@suffix = \snd program →
1163   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
1164    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1165    let 〈program_counter, sigma_map〉 ≝ pc_map in
1166    let 〈label, i〉 ≝ hd in
1167     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
1168 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
1169 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
1170  (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
1171 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
1172 @pair_elim' #pc #map #EQ4 normalize nodelta
1173 @pair_elim' #l' #i' #EQ5 normalize nodelta
1174 cases (construct_costs_safe ??????) normalize
1175  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
1176qed.
1177
1178definition expand_pseudo_instruction:
1179 ∀program:pseudo_assembly_program.∀pol: policy program.
1180  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
1181  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1182  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1183  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
1184  pc = sigma program pol ppc →
1185  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
1186≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
1187   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
1188    [ None ⇒ let dummy ≝ [ ] in dummy
1189    | Some res ⇒ res ].
1190 [ @⊥ whd in p:(??%??);
1191   generalize in match (sig2 ?? pol) whd in ⊢ (% → ?)
1192   whd in ⊢ (?(??%?) → ?) change in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?) with (sigma00 ????)
1193   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)))
1194   cases (sigma00 ????) in ⊢ (??%? → %) normalize nodelta [#_ * #abs @abs %]
1195   #res #K
1196   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
1197   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?
1198   cases daemon (* CSC: XXXXXXXX Ero qui
1199   
1200    [3: @policy_ok_prefix_ok ]
1201    | sigma00 program pol pre
1202
1203
1204
1205   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
1206   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
1207   per concludere construct_costs_safe ≠ None *)
1208 | >p %]
1209qed.
1210
1211(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1212definition assembly_1_pseudoinstruction':
1213 ∀program:pseudo_assembly_program.∀pol: policy program.
1214  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1215  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1216  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1217  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1218  Σres:(nat × (list Byte)).
1219   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
1220   let 〈len,code〉 ≝ res in
1221    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
1222     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
1223≝ λprogram: pseudo_assembly_program.
1224  λpol: policy program.
1225  λppc: Word.
1226  λlookup_labels.
1227  λlookup_datalabels.
1228  λpi.
1229  λprf1,prf2,prf3.
1230   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
1231    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
1232    | Some res ⇒ res ].
1233 [ @⊥ elim pi in p [*]
1234   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
1235   generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)
1236   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
1237   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
1238   cases daemon
1239 | % [ >p %]
1240   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
1241   (* THIS SHOULD BE TRUE INSTEAD *)
1242   cases daemon]
1243qed.
1244
1245definition assembly_1_pseudoinstruction:
1246 ∀program:pseudo_assembly_program.∀pol: policy program.
1247  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1248  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1249  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1250  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1251   nat × (list Byte)
1252≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
1253   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
1254    prf2 prf3.
1255
1256lemma assembly_1_pseudoinstruction_ok1:
1257 ∀program:pseudo_assembly_program.∀pol: policy program.
1258  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1259  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
1260  ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
1261  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
1262     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
1263   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
1264 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
1265 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
1266 #H1 #_ @H1
1267qed.
1268
1269(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1270definition construct_costs':
1271 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
1272  Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
1273≝
1274  λprogram.λpol: policy program.λppc,pc,costs,i.
1275   match construct_costs_safe program pol ppc pc costs i with
1276    [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy
1277    | Some res ⇒ res ].
1278 [ cases daemon
1279 | >p %]
1280qed.
1281
1282definition construct_costs ≝
1283 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
1284
1285(*
1286axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
1287axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
1288
1289axiom foldl_strong_step:
1290 ∀A:Type[0].
1291  ∀P: list A → Type[0].
1292   ∀l: list A.
1293    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
1294     ∀acc: P [ ].
1295      ∀Q: ∀prefix. P prefix → Prop.
1296       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
1297        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
1298       Q [ ] acc →
1299        Q l (foldl_strong A P l H acc).
1300(*
1301 #A #P #l #H #acc #Q #HQ #Hacc normalize;
1302 generalize in match
1303  (foldl_strong ?
1304   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
1305   l ? Hacc)
1306 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
1307 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
1308 #K
1309
1310 generalize in match
1311  (foldl_strong ?
1312   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
1313 [2: @H
1314*)
1315
1316axiom foldl_elim:
1317 ∀A:Type[0].
1318  ∀B: Type[0].
1319   ∀H: A → B → A.
1320    ∀acc: A.
1321     ∀l: list B.
1322      ∀Q: A → Prop.
1323       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
1324         Q acc →
1325          Q (foldl A B H acc l).
1326*)
1327
1328lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1329 #A #a #b #EQ destruct //
1330qed.
1331
1332(*
1333lemma tech_pc_sigma00_append_Some:
1334 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1335  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1336   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1337 #program #pol #prefix #costs #label #i #ppc #pc #H
1338  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
1339  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
1340  generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
1341  whd in match sigma0; normalize nodelta;
1342  >foldl_step
1343  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
1344  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
1345  cases (sigma00 program pol prefix) in H ⊢ %
1346   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
1347   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
1348     
1349     normalize nodelta; -H;
1350     
1351 
1352   generalize in match H; -H;
1353  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
1354   [2: whd in ⊢ (??%%)
1355XXX
1356*)
1357
1358axiom construct_costs_sigma:
1359 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
1360  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
1361   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
1362
1363axiom tech_pc_sigma00_append_Some:
1364 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1365  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1366   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1367
1368definition build_maps:
1369 ∀pseudo_program.∀pol:policy pseudo_program.
1370  Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
1371   let 〈labels,costs〉 ≝ res in
1372    ∀id. occurs_exactly_once id (\snd pseudo_program) →
1373     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
1374≝
1375  λpseudo_program.λpol:policy pseudo_program.
1376  let result ≝
1377   foldl_strong
1378    (option Identifier × pseudo_instruction)
1379    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
1380      let 〈labels,ppc_pc_costs〉 ≝ res in
1381      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
1382      let 〈pc',costs〉 ≝ pc_costs in
1383       And ( And (
1384       And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
1385       (ppc' = length … pre)) (*∧ *)
1386       (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
1387       (∀id. occurs_exactly_once id pre →
1388        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
1389    (\snd pseudo_program)
1390    (λprefix,i,tl,prf,t.
1391      let 〈labels, ppc_pc_costs〉 ≝ t in
1392      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
1393      let 〈pc,costs〉 ≝ pc_costs in
1394       let 〈label, i'〉 ≝ i in
1395       let labels ≝
1396         match label with
1397         [ None ⇒ labels
1398         | Some label ⇒
1399           let program_counter_bv ≝ bitvector_of_nat ? pc in
1400             insert ? ? label program_counter_bv labels]
1401       in
1402         let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
1403          〈labels, 〈S ppc,construct〉〉
1404    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
1405  in
1406   let 〈labels, ppc_pc_costs〉 ≝ result in
1407   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
1408   let 〈pc, costs〉 ≝ pc_costs in
1409    〈labels, costs〉.
1410 [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
1411   generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
1412   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
1413   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
1414   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
1415   | #id normalize nodelta; -labels1; cases label; normalize nodelta
1416     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
1417     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
1418       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
1419        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
1420          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
1421        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
1422          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
1423 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
1424 | generalize in match (sig2 … result) in ⊢ ?;
1425   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?)
1426   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
1427qed.
1428
1429definition assembly:
1430 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝
1431  λp.let 〈preamble, instr_list〉 ≝ p in
1432   λpol.
1433    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
1434    let datalabels ≝ construct_datalabels preamble in
1435    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
1436    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
1437    let result ≝
1438     foldl_strong
1439      (option Identifier × pseudo_instruction)
1440      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
1441        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
1442        let 〈ppc,code〉 ≝ ppc_code in
1443         ∀ppc'.
1444          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
1445          let 〈len,assembledi〉 ≝
1446           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
1447           True)
1448      instr_list
1449      (λprefix,hd,tl,prf,pc_ppc_code.
1450        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
1451        let 〈ppc, code〉 ≝ ppc_code in
1452        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
1453        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
1454        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
1455         〈new_pc, 〈new_ppc, (code @ program)〉〉)
1456      〈(zero ?), 〈(zero ?), [ ]〉〉
1457    in
1458     〈\snd (\snd result), costs〉.
1459 [2,5: %
1460 |*: cases daemon ]
1461qed.
1462
1463definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
1464 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.