source: src/ASM/Assembly.ma @ 1298

Last change on this file since 1298 was 1103, checked in by boender, 9 years ago
  • reverted to old policy
File size: 55.5 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/BitVectorTrie.ma".
3include "ASM/Arithmetic.ma".
4include "ASM/Fetch.ma".
5include "ASM/Status.ma".
6
7definition assembly_preinstruction ≝
8  λA: Type[0].
9  λaddr_of: A → Byte. (* relative *)
10  λpre: preinstruction A.
11  match pre with
12  [ ADD addr1 addr2 ⇒
13     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
14      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
15      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
16      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
17      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
18      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
19  | ADDC addr1 addr2 ⇒
20     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
21      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
22      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
23      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
24      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
25      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
26  | ANL addrs ⇒
27     match addrs with
28      [ inl addrs ⇒ match addrs with
29         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
30           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
31            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
32            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
33            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
34            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
35            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
36         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
37            let b1 ≝
38             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
39              [ DIRECT b1 ⇒ λ_.b1
40              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
41            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
42             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
43             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
44             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
45         ]
46      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
47         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
48          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
49          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
50          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
51  | CLR addr ⇒
52     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
53      [ ACC_A ⇒ λ_.
54         [ ([[true; true; true; false; false; true; false; false]]) ]
55      | CARRY ⇒ λ_.
56         [ ([[true; true; false; false; false; false; true; true]]) ]
57      | BIT_ADDR b1 ⇒ λ_.
58         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
59      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
60  | CPL addr ⇒
61     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
62      [ ACC_A ⇒ λ_.
63         [ ([[true; true; true; true; false; true; false; false]]) ]
64      | CARRY ⇒ λ_.
65         [ ([[true; false; true; true; false; false; true; true]]) ]
66      | BIT_ADDR b1 ⇒ λ_.
67         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
68      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
69  | DA addr ⇒
70     [ ([[true; true; false; true; false; true; false; false]]) ]
71  | DEC addr ⇒
72     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
73      [ ACC_A ⇒ λ_.
74         [ ([[false; false; false; true; false; true; false; false]]) ]
75      | REGISTER r ⇒ λ_.
76         [ ([[false; false; false; true; true]]) @@ r ]
77      | DIRECT b1 ⇒ λ_.
78         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
79      | INDIRECT i1 ⇒ λ_.
80         [ ([[false; false; false; true; false; true; true; i1]]) ]
81      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
82      | DJNZ addr1 addr2 ⇒
83         let b2 ≝ addr_of addr2 in
84         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
85          [ REGISTER r ⇒ λ_.
86             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
87          | DIRECT b1 ⇒ λ_.
88             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
89          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
90      | JC addr ⇒
91        let b1 ≝ addr_of addr in
92          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
93      | JNC addr ⇒
94         let b1 ≝ addr_of addr in
95           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
96      | JZ addr ⇒
97         let b1 ≝ addr_of addr in
98           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
99      | JNZ addr ⇒
100         let b1 ≝ addr_of addr in
101           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
102      | JB addr1 addr2 ⇒
103         let b2 ≝ addr_of addr2 in
104         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
105          [ BIT_ADDR b1 ⇒ λ_.
106             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
107          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
108      | JNB addr1 addr2 ⇒
109         let b2 ≝ addr_of addr2 in
110         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
111          [ BIT_ADDR b1 ⇒ λ_.
112             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
113          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
114      | JBC addr1 addr2 ⇒
115         let b2 ≝ addr_of addr2 in
116         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
117          [ BIT_ADDR b1 ⇒ λ_.
118             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
119          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
120      | CJNE addrs addr3 ⇒
121         let b3 ≝ addr_of addr3 in
122         match addrs with
123          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
124             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
125              [ DIRECT b1 ⇒ λ_.
126                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
127              | DATA b1 ⇒ λ_.
128                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
129              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
130          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
131             let b2 ≝
132              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
133               [ DATA b2 ⇒ λ_. b2
134               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
135             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
136              [ REGISTER r ⇒ λ_.
137                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
138              | INDIRECT i1 ⇒ λ_.
139                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
140              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
141         ]
142  | DIV addr1 addr2 ⇒
143     [ ([[true;false;false;false;false;true;false;false]]) ]
144  | INC addr ⇒
145     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
146      [ ACC_A ⇒ λ_.
147         [ ([[false;false;false;false;false;true;false;false]]) ]         
148      | REGISTER r ⇒ λ_.
149         [ ([[false;false;false;false;true]]) @@ r ]
150      | DIRECT b1 ⇒ λ_.
151         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
152      | INDIRECT i1 ⇒ λ_.
153        [ ([[false; false; false; false; false; true; true; i1]]) ]
154      | DPTR ⇒ λ_.
155        [ ([[true;false;true;false;false;false;true;true]]) ]
156      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
157  | MOV addrs ⇒
158     match addrs with
159      [ inl 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 ⇒ let 〈addr1,addr2〉 ≝ addrs in
168                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
169                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
170                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
171                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
172                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
173                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
174                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
175                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
176                          [ REGISTER r ⇒ λ_.
177                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
178                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
179                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
180                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
181                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
182                          | INDIRECT i1 ⇒ λ_.
183                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
184                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
185                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
186                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
187                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
188                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
189                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
190                     let b1 ≝
191                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
192                       [ DIRECT b1 ⇒ λ_. b1
193                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
194                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
195                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
196                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
197                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
198                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
199                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
200                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
201              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
202                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
203                  [ DATA16 w ⇒ λ_.
204                     let b1_b2 ≝ split ? 8 8 w in
205                     let b1 ≝ \fst b1_b2 in
206                     let b2 ≝ \snd b1_b2 in
207                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
208                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
209          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
210             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
211              [ BIT_ADDR b1 ⇒ λ_.
212                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
213              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
214      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
215         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
216          [ BIT_ADDR b1 ⇒ λ_.
217             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
218          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
219  | MOVX addrs ⇒
220     match addrs with
221      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
222         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
223          [ EXT_INDIRECT i1 ⇒ λ_.
224             [ ([[true;true;true;false;false;false;true;i1]]) ]
225          | EXT_INDIRECT_DPTR ⇒ λ_.
226             [ ([[true;true;true;false;false;false;false;false]]) ]
227          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
228      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
229         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
230          [ EXT_INDIRECT i1 ⇒ λ_.
231             [ ([[true;true;true;true;false;false;true;i1]]) ]
232          | EXT_INDIRECT_DPTR ⇒ λ_.
233             [ ([[true;true;true;true;false;false;false;false]]) ]
234          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
235  | MUL addr1 addr2 ⇒
236     [ ([[true;false;true;false;false;true;false;false]]) ]
237  | NOP ⇒
238     [ ([[false;false;false;false;false;false;false;false]]) ]
239  | ORL addrs ⇒
240     match addrs with
241      [ inl addrs ⇒
242         match addrs with
243          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
244             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
245             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
246             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
247             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
248             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
249             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
250          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
251            let b1 ≝
252              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
253               [ DIRECT b1 ⇒ λ_. b1
254               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
255             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
256              [ ACC_A ⇒ λ_.
257                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
258              | DATA b2 ⇒ λ_.
259                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
260              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
261      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
262         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
263          [ BIT_ADDR b1 ⇒ λ_.
264             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
265          | N_BIT_ADDR b1 ⇒ λ_.
266             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
267          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
268  | POP addr ⇒
269     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
270      [ DIRECT b1 ⇒ λ_.
271         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
272      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
273  | PUSH addr ⇒
274     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
275      [ DIRECT b1 ⇒ λ_.
276         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
277      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
278  | RET ⇒
279     [ ([[false;false;true;false;false;false;true;false]]) ]
280  | RETI ⇒
281     [ ([[false;false;true;true;false;false;true;false]]) ]
282  | RL addr ⇒
283     [ ([[false;false;true;false;false;false;true;true]]) ]
284  | RLC addr ⇒
285     [ ([[false;false;true;true;false;false;true;true]]) ]
286  | RR addr ⇒
287     [ ([[false;false;false;false;false;false;true;true]]) ]
288  | RRC addr ⇒
289     [ ([[false;false;false;true;false;false;true;true]]) ]
290  | SETB addr ⇒     
291     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
292      [ CARRY ⇒ λ_.
293         [ ([[true;true;false;true;false;false;true;true]]) ]
294      | BIT_ADDR b1 ⇒ λ_.
295         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
296      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
297  | SUBB addr1 addr2 ⇒
298     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
299      [ REGISTER r ⇒ λ_.
300         [ ([[true;false;false;true;true]]) @@ r ]
301      | DIRECT b1 ⇒ λ_.
302         [ ([[true;false;false;true;false;true;false;true]]); b1]
303      | INDIRECT i1 ⇒ λ_.
304         [ ([[true;false;false;true;false;true;true;i1]]) ]
305      | DATA b1 ⇒ λ_.
306         [ ([[true;false;false;true;false;true;false;false]]); b1]
307      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
308  | SWAP addr ⇒
309     [ ([[true;true;false;false;false;true;false;false]]) ]
310  | XCH addr1 addr2 ⇒
311     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
312      [ REGISTER r ⇒ λ_.
313         [ ([[true;true;false;false;true]]) @@ r ]
314      | DIRECT b1 ⇒ λ_.
315         [ ([[true;true;false;false;false;true;false;true]]); b1]
316      | INDIRECT i1 ⇒ λ_.
317         [ ([[true;true;false;false;false;true;true;i1]]) ]
318      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
319  | XCHD addr1 addr2 ⇒
320     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
321      [ INDIRECT i1 ⇒ λ_.
322         [ ([[true;true;false;true;false;true;true;i1]]) ]
323      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
324  | XRL addrs ⇒
325     match addrs with
326      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
327         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
328          [ REGISTER r ⇒ λ_.
329             [ ([[false;true;true;false;true]]) @@ r ]
330          | DIRECT b1 ⇒ λ_.
331             [ ([[false;true;true;false;false;true;false;true]]); b1]
332          | INDIRECT i1 ⇒ λ_.
333             [ ([[false;true;true;false;false;true;true;i1]]) ]
334          | DATA b1 ⇒ λ_.
335             [ ([[false;true;true;false;false;true;false;false]]); b1]
336          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
337      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
338         let b1 ≝
339          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
340           [ DIRECT b1 ⇒ λ_. b1
341           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
342         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
343          [ ACC_A ⇒ λ_.
344             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
345          | DATA b2 ⇒ λ_.
346             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
347          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
348       ].
349
350definition assembly1 ≝
351 λi: instruction.
352 match i with
353  [ ACALL addr ⇒
354     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
355      [ ADDR11 w ⇒ λ_.
356         let v1_v2 ≝ split ? 3 8 w in
357         let v1 ≝ \fst v1_v2 in
358         let v2 ≝ \snd v1_v2 in
359          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
360      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
361  | AJMP addr ⇒
362     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
363      [ ADDR11 w ⇒ λ_.
364         let v1_v2 ≝ split ? 3 8 w in
365         let v1 ≝ \fst v1_v2 in
366         let v2 ≝ \snd v1_v2 in
367          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
368      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
369  | JMP adptr ⇒
370     [ ([[false;true;true;true;false;false;true;true]]) ]
371  | LCALL addr ⇒
372     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
373      [ ADDR16 w ⇒ λ_.
374         let b1_b2 ≝ split ? 8 8 w in
375         let b1 ≝ \fst b1_b2 in
376         let b2 ≝ \snd b1_b2 in
377          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
378      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
379  | LJMP addr ⇒
380     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
381      [ ADDR16 w ⇒ λ_.
382         let b1_b2 ≝ split ? 8 8 w in
383         let b1 ≝ \fst b1_b2 in
384         let b2 ≝ \snd b1_b2 in
385          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
386      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
387  | MOVC addr1 addr2 ⇒
388     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
389      [ ACC_DPTR ⇒ λ_.
390         [ ([[true;false;false;true;false;false;true;true]]) ]
391      | ACC_PC ⇒ λ_.
392         [ ([[true;false;false;false;false;false;true;true]]) ]
393      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
394  | SJMP addr ⇒
395     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
396      [ RELATIVE b1 ⇒ λ_.
397         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
398      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
399  | RealInstruction instr ⇒
400    assembly_preinstruction [[ relative ]]
401      (λx.
402        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
403        [ RELATIVE r ⇒ λ_. r
404        | _ ⇒ λabsd. ⊥
405        ] (subaddressing_modein … x)) instr
406  ].
407  cases absd
408qed.
409
410definition is_relative_jump ≝
411  λi: preinstruction Identifier.
412  match i with
413  [ JC _ ⇒ True
414  | JNC _ ⇒ True
415  | JB _ _ ⇒ True
416  | JNB _ _ ⇒ True
417  | JBC _ _ ⇒ True
418  | JZ _ ⇒ True
419  | JNZ _ ⇒ True
420  | CJNE _ _ ⇒ True
421  | DJNZ _ _ ⇒ True
422  | _ ⇒ False
423  ].
424
425definition pseudo_instruction_is_relative_jump: pseudo_instruction → Prop ≝
426 λi.
427  match i with
428   [ Instruction j ⇒ is_relative_jump j
429   | _ ⇒ False ].
430
431inductive jump_length: Type[0] ≝
432  | short_jump: jump_length
433  | medium_jump: jump_length
434  | long_jump: jump_length.
435
436definition find_right_call: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝
437 (* medium call: 11 bits, only in "current segment" *)
438 (* can this be done more efficiently with bit vector arithmetic? *)
439 λpc.λaddress.
440  let 〈a1, a2〉 ≝ split ? 5 11 address in
441  let 〈p1, p2〉 ≝ split ? 5 11 pc in
442   if eq_bv ? a1 p1 then (* we're in the same segment *)
443    〈2, 2, address, Some ? medium_jump〉
444   else
445    〈2, 3, address, Some ? long_jump〉.
446   
447(* lemma frc_ok:
448  ∀pc.∀j_addr.
449  let 〈i1,i2,addr,jl〉 ≝ find_right_call pc j_addr in
450  addr = j_addr ∧
451  match jl with
452  [ None ⇒ False (* doesn't happen *)
453  | Some j ⇒ match j with
454    [ short_jump ⇒ False (* doesn't happen either *)
455    | medium_jump ⇒ \fst (split ? 5 11 j_addr) = \fst (split ? 5 11 pc)
456    | long_jump ⇒ True
457    ]
458  ].
459 #pc #j_addr whd in match (find_right_call pc j_addr) cases (split ????) cases (split ????)
460 #p1 #p2 #a1 #a2 normalize nodelta
461 lapply (refl ? (eq_bv 5 a1 p1)) cases (eq_bv 5 a1 p1) in ⊢ (???% → %) #H normalize
462 [ %1 [ @refl | @(eq_bv_eq … H) ]
463 | %1 [ @refl | // ] ]
464qed. *)
465       
466definition distance ≝
467 λx.λy.if gtb x y then x - y else y - x.
468 
469definition find_right_jump: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝
470 (* short jump: 8 bits signed *)
471 (* medium jump: 11 bits, forward only *)
472 λpc.λaddress.
473  let pn ≝ nat_of_bitvector ? pc in
474  let pa ≝ nat_of_bitvector ? address in
475   if ltb (distance pn pa) 127 then
476    〈2, 2, address, Some ? short_jump〉
477   else
478    find_right_call pc address.
479
480(* lemma frj_ok:
481  ∀pc.∀j_addr.
482  let 〈i1,i2,addr,jl〉 ≝ find_right_jump pc j_addr in
483  addr = j_addr ∧
484  match jl with
485  [ None ⇒ False (* doesn't happen *)
486  | Some j ⇒ match j with
487    [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? j_addr) < 127
488    | medium_jump ⇒ \fst (split ? 5 11 j_addr) = \fst (split ? 5 11 pc)
489    | long_jump ⇒ True
490    ]
491  ].
492 #pc #j_addr whd in match (find_right_jump pc j_addr)
493 lapply (refl ? (ltb (distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 j_addr)) 127))
494 cases (ltb (distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 j_addr)) 127) in ⊢ (???% → %) #H
495 normalize nodelta
496 [ %1 [ @refl | whd @(leb_true_to_le … H) ]
497 | lapply (frc_ok pc j_addr) cases (find_right_call ??) normalize nodelta #x #y cases x
498 #i1 #i2 cases y #addr #jl normalize nodelta cases jl normalize
499   [ //
500   | #jl cases jl normalize
501     [1: #f @⊥ @(proj2 ? ? f) |2,3: // ]
502   ]
503  ]
504qed. *)
505   
506definition find_right_relative_jump: Word → (BitVectorTrie (Word × Identifier) 16) →
507 Identifier → (nat × nat) × (Word × (option jump_length)) ≝
508 λpc.λlabels.λjmp.
509 match lookup_opt ? ? jmp labels with
510 [ None ⇒ 〈2, 2, pc, Some ? short_jump〉
511 | Some x ⇒ let 〈ignore, a〉 ≝ x in find_right_jump pc a ].
512 
513(* lemma frrj_ok:
514  ∀pc.∀labels.∀j_id.
515  let 〈i1,i2,addr,jl〉 ≝ find_right_relative_jump pc labels j_id in
516  match lookup_opt ? ? j_id labels with
517  [ None ⇒ True (* long jump *)
518  | Some x ⇒ let 〈ignore,j_addr〉 ≝ x in addr = j_addr ∧ match jl with
519    [ None ⇒ False (* doesn't happen *)
520    | Some j ⇒ match j with
521      [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? j_addr) < 127
522      | medium_jump ⇒ \fst (split ? 5 11 j_addr) = \fst (split ? 5 11 pc)
523      | long_jump ⇒ True
524      ]
525    ]
526  ].
527 #pc #labels #j_id whd in match (find_right_relative_jump pc labels j_id)
528 cases (lookup_opt ? ? j_id labels) normalize nodelta
529 [ //
530 | #x cases x #y #j_addr -x; normalize nodelta lapply (frj_ok pc j_addr)
531   cases (find_right_jump ??) #x cases x #i1 #i2 -x #x cases x #i3 #z -x; cases z
532   normalize nodelta
533   [ //
534   | #jl cases jl normalize nodelta
535     [1,3: // |2: #H @H ]
536   ]
537 ]
538qed. *)
539     
540definition jep_relative: Word → (BitVectorTrie (Word × Identifier) 16) → preinstruction Identifier → ? ≝
541 λpc.λlabels.λi.
542  match i with
543  [ JC jmp ⇒ find_right_relative_jump pc labels jmp
544  | JNC jmp ⇒ find_right_relative_jump pc labels jmp
545  | JB baddr jmp ⇒ find_right_relative_jump pc labels jmp
546  | JZ jmp ⇒ find_right_relative_jump pc labels jmp
547  | JNZ jmp ⇒ find_right_relative_jump pc labels jmp
548  | JBC baddr jmp ⇒ find_right_relative_jump pc labels jmp
549  | JNB baddr jmp ⇒ find_right_relative_jump pc labels jmp
550  | CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp
551  | DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp
552  | _ ⇒ let l ≝ length ? (assembly_preinstruction ? (λx.zero ?) i) in
553         〈l, l, pc, None …〉 ].
554
555definition is_long_jump ≝
556 λj.match j with
557 [ long_jump ⇒ true
558 | _         ⇒ false
559 ].
560
561definition policy_safe ≝
562 (λ_:Word.λx:Word×Word×jump_length.let 〈pc,addr,j〉 ≝ x in
563   match j with
564   [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? addr) < 127
565   | medium_jump ⇒ \fst (split ? 5 11 addr) = \fst (split ? 5 11 pc)
566   | long_jump ⇒ True
567   ]
568  ).
569
570definition jump_expansion_policy ≝
571  Σpolicy:BitVectorTrie (Word × Word × jump_length) 16.
572    forall ? ? policy policy_safe.
573 
574definition inject_jump_expansion_policy:
575 ∀p:BitVectorTrie (Word × Word × jump_length) 16.
576  forall ? ? p policy_safe → jump_expansion_policy ≝ inject ….
577 
578coercion inject_jump_expansion_policy:
579 ∀p:BitVectorTrie (Word × Word × jump_length) 16.
580  forall ? ? p policy_safe → jump_expansion_policy ≝ inject_jump_expansion_policy
581 on p:(BitVectorTrie (Word × Word × jump_length) 16) to jump_expansion_policy.
582 
583(* the jump length in a is greater than or equal to the jump length in b *)
584definition jump_length_decrease ≝
585 λa:jump_length.λb:jump_length.
586 match a with
587 [ short_jump ⇒ b = short_jump
588 | medium_jump ⇒ b = short_jump ∨ b = medium_jump
589 | long_jump ⇒ True
590 ].
591
592definition jump_expansion_policy_internal: pseudo_assembly_program →
593 (BitVectorTrie (Word × Identifier) 16) → jump_expansion_policy →
594 Σres:(BitVectorTrie (Word × Identifier) 16) × (BitVectorTrie (Word × Word × jump_length) 16).
595  let 〈x,p〉 ≝ res in
596  True ≝
597 λprogram.λold_labels.λold_policy.
598   let res ≝
599   foldl_strong (option Identifier × pseudo_instruction)
600    (λprefix.Σres.True)
601    (\snd program)
602    (λprefix.λi.λtl.λprf.λacc.   
603     let 〈label, instr〉 ≝ i in
604     let 〈pc,orig_pc,labels,policy〉 ≝ acc in
605     let new_labels ≝ match label return λ_.(BitVectorTrie (Word × Identifier) 16) with
606      [ None ⇒ labels
607      | Some l ⇒ insert ? ? orig_pc 〈pc,l〉 labels
608      ] in
609     let add_instr ≝ match instr with
610      [ Call c ⇒
611        match lookup_opt ? ? c new_labels with
612         [ None   ⇒ 〈2, 2, pc, Some ? short_jump〉
613         | Some x ⇒ let 〈ignore,c_addr〉 ≝ x in find_right_call pc c_addr ]
614      | Jmp j ⇒
615        match lookup_opt ? ? j new_labels with
616         [ None   ⇒ 〈2, 2, pc, Some ? short_jump〉
617         | Some x ⇒ let 〈ignore,j_addr〉 ≝ x in find_right_jump pc j_addr ]
618      | Instruction i ⇒ jep_relative pc new_labels i
619      | Mov _ _ ⇒ 〈3, 3, pc, None …〉
620      | Cost _ ⇒ 〈0, 0, pc, None …〉
621      | Comment _ ⇒ 〈0, 0, pc, None …〉 ] in
622     let 〈pc_delta, orig_pc_delta, addr, jmp_len〉 ≝ add_instr in
623     let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
624     let 〈new_orig_pc,ignore〉 ≝ add_16_with_carry orig_pc (bitvector_of_nat ? orig_pc_delta) false in
625     match jmp_len with
626      [ None   ⇒ 〈new_pc, orig_pc, new_labels, policy〉
627      | Some j ⇒ 〈new_pc, new_orig_pc, new_labels, insert ? ? orig_pc 〈pc, addr, j〉 policy〉
628      ]
629    ) 〈zero ?, zero ?, old_labels, eject … old_policy〉 in
630   let 〈npc, norig_pc, nlabels, npolicy〉 ≝ res in
631   〈nlabels, npolicy〉.
632   //.
633(* [ cases res in p -res; #res >p1 >p2 normalize nodelta #Ha #Hb normalize in Hb;
634     >Hb in Ha; normalize nodelta #H @H
635   | generalize in match (sig2 … acc) >p1 >p2 >p3 #H
636     @(forall_insert … H)  normalize nodelta normalize nodelta in p4; cases instr in p4; >p5 >p6 normalize nodelta
637     [5: #str >p9 #Heq cases (lookup_opt ? ? str ?) in Heq; normalize nodelta
638         [ #Heq2 lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2))))
639           #Heq3 destruct (Heq3) //
640         | #x cases x -x #i0 #c_addr normalize nodelta lapply (frc_ok pc c_addr)
641           cases (find_right_call pc c_addr) #x #y cases x #i0 #i1 -x; cases y #ad #jmp -y;
642           normalize nodelta #Heq #Heq2
643           >(proj1 ? ? Heq) in Heq2; #Heq2
644           <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2))))
645           >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq;
646           cases j normalize nodelta #Heq [ @⊥ ] @(proj2 ? ? Heq)
647         ]
648    |2,3,6: [3: #x] #z >p9 #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
649       #ctd destruct (ctd)
650    |1,4:
651      #pi
652       [1: cases label normalize nodelta [ #Hjep | #id #Hjep ] whd in Hjep: (??%??); cases pi in Hjep;
653       |2: cases (lookup_opt ? ? pi ?) normalize nodelta >p9
654           [ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
655             #ctd destruct (ctd) //
656           | #x cases x -x #i0 #j_addr normalize nodelta lapply (frj_ok pc j_addr)
657             cases (find_right_jump pc j_addr) #x #y cases x #i0 #i1 -x; cases y #ad #jump -y;
658             normalize nodelta #Heq #Heq2
659             >(proj1 ? ? Heq) in Heq2; #Heq2
660             <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2))))
661             >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq;
662             cases j normalize nodelta #Heq @(proj2 ? ? Heq)
663           ]
664       ]
665       [1,2,3,6,7,33,34,38,39,40,43,44,70,71: #acc #x normalize nodelta #Heq
666         <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9;
667         #ctd destruct (ctd)
668       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69:
669         #acc normalize nodelta #Heq
670         <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9;
671         #ctd destruct (ctd)
672       |35,36,37,72,73,74: normalize nodelta #Heq
673         <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9;
674         #ctd destruct (ctd)
675       |9,10,14,15: #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id)
676           whd in match (find_right_relative_jump pc labels j_id)
677          normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta
678          [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
679             #Heq2 destruct (Heq2) //
680          |2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
681            normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
682          ]
683       |46,47,51,52: #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id)
684          whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id)
685          normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta
686          [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
687             #Heq2 destruct (Heq2) //
688          |2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
689            normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
690          ]
691       |11,12,13,16,17: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id)
692          whd in match (find_right_relative_jump pc labels j_id)
693          normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta
694          [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
695             #Heq2 destruct (Heq2) //
696          |2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
697            normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
698          ]
699       |48,49,50,53,54: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id)
700          whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id)
701          normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta
702          [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
703             #Heq2 destruct (Heq2) //
704          |2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
705            normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
706          ]
707       ]
708     ]
709   | generalize in match (sig2 … acc) >p1 >p2 >p3 #H
710     @H
711   | generalize in match (sig2 … old_policy) #H @H
712   ] *)
713qed.
714
715(* lemma short_jumps_ok:
716  ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy.
717  forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p))
718    (λk.λx.let 〈pc,addr,j〉 ≝ x in
719      j = short_jump →
720      distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127).
721 #program #l #p @lookup_forall
722  #x #b cases x -x #x cases x #pc #addr #j #Hl normalize nodelta
723  cases j in Hl; #Hl #Hj
724  [2,3: destruct (Hj)
725  |-Hj; cases (jump_expansion_policy_internal program l p) in Hl;
726    #res cases res -res #r #res normalize nodelta #Hf #Hl
727    normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl)
728    normalize #H @H
729  ]   
730qed. *)
731
732(* lemma medium_jumps_ok:
733  ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy.
734  forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p))
735    (λk.λx.let 〈pc,addr,j〉 ≝ x in
736      j = medium_jump →
737      distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127).
738 #program #l #p @lookup_forall
739  #x #b cases x -x #x cases x #pc #addr #j #Hl normalize nodelta
740  cases j in Hl; #Hl #Hj
741  [2,3: destruct (Hj)
742  |-Hj; cases (jump_expansion_policy_internal program l p) in Hl;
743    #res cases res -res #r #res normalize nodelta #Hf #Hl
744    normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl)
745    normalize #H @H
746  ]   
747qed. *)
748     
749definition expand_relative_jump_internal:
750 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
751 option (list instruction)
752 ≝
753  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
754  match jmp_len with
755  [ short_jump ⇒
756     let lookup_address ≝ lookup_labels jmp in
757     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
758     let 〈upper, lower〉 ≝ split ? 8 8 result in
759     if eq_bv ? upper (zero 8) then
760      let address ≝ RELATIVE lower in
761       Some ? [ RealInstruction (i address) ]
762     else
763       None ?
764  | medium_jump ⇒ None …
765  | long_jump ⇒
766    Some ?
767    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
768      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
769      LJMP (ADDR16 (lookup_labels jmp))
770    ]
771  ].
772  @ I
773qed.
774
775definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
776  λlookup_labels.
777  λjmp_len: jump_length.
778  λpc.
779  λi: preinstruction Identifier.
780  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
781  match i with
782  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
783  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
784  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
785  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
786  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
787  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
788  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
789  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
790  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
791  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
792  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
793  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
794  | INC arg ⇒ Some ? [ INC ? arg ]
795  | DEC arg ⇒ Some ? [ DEC ? arg ]
796  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
797  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
798  | DA arg ⇒ Some ? [ DA ? arg ]
799  | ANL arg ⇒ Some ? [ ANL ? arg ]
800  | ORL arg ⇒ Some ? [ ORL ? arg ]
801  | XRL arg ⇒ Some ? [ XRL ? arg ]
802  | CLR arg ⇒ Some ? [ CLR ? arg ]
803  | CPL arg ⇒ Some ? [ CPL ? arg ]
804  | RL arg ⇒ Some ? [ RL ? arg ]
805  | RR arg ⇒ Some ? [ RR ? arg ]
806  | RLC arg ⇒ Some ? [ RLC ? arg ]
807  | RRC arg ⇒ Some ? [ RRC ? arg ]
808  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
809  | MOV arg ⇒ Some ? [ MOV ? arg ]
810  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
811  | SETB arg ⇒ Some ? [ SETB ? arg ]
812  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
813  | POP arg ⇒ Some ? [ POP ? arg ]
814  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
815  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
816  | RET ⇒ Some ? [ RET ? ]
817  | RETI ⇒ Some ? [ RETI ? ]
818  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
819  ].
820
821definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
822  λlookup_labels.
823  λlookup_datalabels.
824  λpc.
825  λjmp_len.
826  λi.
827  match i with
828  [ Cost cost ⇒ Some ? [ ]
829  | Comment comment ⇒ Some ? [ ]
830  | Call call ⇒
831    match jmp_len with
832    [ short_jump ⇒ None ?
833    | medium_jump ⇒
834      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
835      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
836      if eq_bv ? ignore fst_5 then
837        let address ≝ ADDR11 address in
838          Some ? ([ ACALL address ])
839      else
840        None ?
841    | long_jump ⇒
842      let address ≝ ADDR16 (lookup_labels call) in
843        Some ? [ LCALL address ]
844    ]
845  | Mov d trgt ⇒
846    let address ≝ DATA16 (lookup_datalabels trgt) in
847      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
848  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
849  | Jmp jmp ⇒
850    match jmp_len with
851    [ short_jump ⇒
852      let lookup_address ≝ lookup_labels jmp in
853      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
854      let 〈upper, lower〉 ≝ split ? 8 8 result in
855      if eq_bv ? upper (zero 8) then
856        let address ≝ RELATIVE lower in
857          Some ? [ SJMP address ]
858      else
859        None ?
860    | medium_jump ⇒
861      let address ≝ lookup_labels jmp in
862      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
863      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
864      if eq_bv ? fst_5_addr fst_5_pc then
865        let address ≝ ADDR11 rest_addr in
866          Some ? ([ AJMP address ])
867      else
868        None ?
869    | long_jump ⇒
870      let address ≝ ADDR16 (lookup_labels jmp) in
871        Some ? [ LJMP address ]
872    ]
873  ].
874  @ I
875qed.
876
877let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program)
878 (old_labels: BitVectorTrie (Word × Identifier) 16)
879 (old_policy: Σbla:BitVectorTrie (Word × Word × jump_length) 16.
880   forall ? ? bla policy_safe)
881 on n: BitVectorTrie jump_length 16 ≝
882 match n with
883 [ O ⇒ fold …
884   (λ_.λx.λacc.let 〈pc,i2,jmp_len〉 ≝ x in insert … pc jmp_len acc)
885   old_policy (Stub ? ?)
886 | S n' ⇒
887    jump_expansion_internal n' program
888    (\fst (jump_expansion_policy_internal program old_labels old_policy))
889    (\snd (jump_expansion_policy_internal program old_labels old_policy))
890 ].
891 generalize in match (sig2 … (jump_expansion_policy_internal program old_labels old_policy))
892 cases (jump_expansion_policy_internal program old_labels old_policy)
893 #a cases a #xx #pp normalize nodelta
894 #H #H2 normalize nodelta @H2
895qed.
896
897
898
899 
900(**************************************** START OF POLICY ABSTRACTION ********************)
901
902definition policy_type ≝ Word → jump_length.
903
904definition jump_expansion': pseudo_assembly_program → policy_type ≝
905 λprogram.λpc.
906  let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
907  lookup ? ? pc policy long_jump.
908 normalize //
909qed.
910 
911definition assembly_1_pseudoinstruction_safe ≝
912  λprogram: pseudo_assembly_program.
913  λjump_expansion: policy_type.
914  λppc: Word.
915  λpc: Word.
916  λlookup_labels.
917  λlookup_datalabels.
918  λi.
919  let expansion ≝ jump_expansion ppc in
920    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
921    [ None ⇒ None ?
922    | Some pseudos ⇒
923      let mapped ≝ map ? ? assembly1 pseudos in
924      let flattened ≝ flatten ? mapped in
925      let pc_len ≝ length ? flattened in
926        Some ? (〈pc_len, flattened〉)
927    ].
928 
929definition construct_costs_safe ≝
930  λprogram.
931  λjump_expansion: policy_type.
932  λpseudo_program_counter: nat.
933  λprogram_counter: nat.
934  λcosts: BitVectorTrie Word 16.
935  λi.
936  match i with
937  [ Cost cost ⇒
938    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
939      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
940  | _ ⇒
941    let pc_bv ≝ bitvector_of_nat ? program_counter in
942    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
943    let lookup_labels ≝ λx.pc_bv in
944    let lookup_datalabels ≝ λx.zero ? in
945    let pc_delta_assembled ≝
946      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
947        lookup_labels lookup_datalabels i
948    in
949    match pc_delta_assembled with
950    [ None ⇒ None ?
951    | Some pc_delta_assembled ⇒
952      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
953        Some ? 〈pc_delta + program_counter, costs〉       
954    ]
955  ].
956
957(* This establishes the correspondence between pseudo program counters and
958   program counters. It is at the heart of the proof. *)
959(*CSC: code taken from build_maps *)
960definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
961 λinstr_list.
962 λjump_expansion: policy_type.
963 λl:list labelled_instruction.
964  foldl ??
965   (λt,i.
966       match t with
967       [ None ⇒ None ?
968       | Some ppc_pc_map ⇒
969         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
970         let 〈program_counter, sigma_map〉 ≝ pc_map in
971         let 〈label, i〉 ≝ i in
972          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
973           [ None ⇒ None ?
974           | Some pc_ignore ⇒
975              let 〈pc,ignore〉 ≝ pc_ignore in
976              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
977       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
978
979definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
980 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog).
981
982definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
983 λprogram,jump_expansion,instr_list.
984  match sigma00 program jump_expansion instr_list with
985   [ None ⇒ None …
986   | Some result ⇒
987      let 〈ppc,pc_sigma_map〉 ≝ result in
988      let 〈pc,map〉 ≝ pc_sigma_map in
989       Some … 〈ppc,pc〉 ].
990
991definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
992 λinstr_list,jump_expansion.
993  match sigma0 instr_list jump_expansion with
994  [ None ⇒ None ?
995  | Some result ⇒
996    let 〈ppc,pc_sigma_map〉 ≝ result in
997    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
998      if gtb pc (2^16) then
999        None ?
1000      else
1001        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
1002
1003(* stuff about policy *)
1004
1005definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
1006
1007definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
1008
1009lemma eject_policy: ∀p. policy p → policy_type.
1010 #p #pol @(eject … pol)
1011qed.
1012
1013coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
1014
1015definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
1016 λp,policy.
1017  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
1018   [ None ⇒ λabs. ⊥
1019   | Some r ⇒ λ_.r] (sig2 … policy).
1020 cases abs /2/
1021qed.
1022
1023example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
1024 cases daemon.
1025qed.
1026
1027definition expand_pseudo_instruction:
1028 ∀program:pseudo_assembly_program.∀pol: policy program.
1029  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
1030  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1031  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1032  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
1033  pc = sigma program pol ppc →
1034  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
1035≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
1036   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
1037    [ None ⇒ let dummy ≝ [ ] in dummy
1038    | Some res ⇒ res ].
1039 [ cases daemon
1040 | >p %]
1041qed.
1042
1043(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1044definition assembly_1_pseudoinstruction:
1045 ∀program:pseudo_assembly_program.∀pol: policy program.
1046  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1047  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1048  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
1049  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1050  Σres:(nat × (list Byte)).
1051   let 〈len,code〉 ≝ res in
1052    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
1053     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
1054≝ λprogram: pseudo_assembly_program.
1055  λpol: policy program.
1056  λppc: Word.
1057  λlookup_labels.
1058  λlookup_datalabels.
1059  λpi.
1060  λprf1,prf2,prf3.
1061   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
1062    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
1063    | Some res ⇒ res ].
1064 [ @⊥ elim pi in p [*]
1065   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
1066   generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)
1067   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
1068   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
1069   cases daemon
1070 | cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
1071   (* THIS SHOULD BE TRUE INSTEAD *)
1072   cases daemon]
1073qed.
1074
1075(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1076definition construct_costs':
1077 ∀program. policy program → nat → nat → ? → ? →
1078  Σres:(nat × (BitVectorTrie Word 16)). True
1079≝
1080  λprogram.λpol: policy program.λppc,pc,costs,i.
1081   match construct_costs_safe program pol ppc pc costs i with
1082    [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy
1083    | Some res ⇒ res ].
1084 [ cases daemon
1085 | %]
1086qed.
1087
1088definition construct_costs ≝
1089 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
1090
1091axiom construct_costs_sigma:
1092 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
1093  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
1094   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
1095
1096axiom tech_pc_sigma00_append_Some:
1097 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1098  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1099   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1100
1101definition build_maps:
1102 ∀pseudo_program.∀pol:policy pseudo_program.
1103  Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
1104   let 〈labels,costs〉 ≝ res in
1105    ∀id. occurs_exactly_once id (\snd pseudo_program) →
1106     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
1107≝
1108  λpseudo_program.λpol:policy pseudo_program.
1109  let result ≝
1110   foldl_strong
1111    (option Identifier × pseudo_instruction)
1112    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
1113      let 〈labels,ppc_pc_costs〉 ≝ res in
1114      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
1115      let 〈pc',costs〉 ≝ pc_costs in
1116       And ( And (
1117       And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
1118       (ppc' = length … pre)) (*∧ *)
1119       (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
1120       (∀id. occurs_exactly_once id pre →
1121        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
1122    (\snd pseudo_program)
1123    (λprefix,i,tl,prf,t.
1124      let 〈labels, ppc_pc_costs〉 ≝ t in
1125      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
1126      let 〈pc,costs〉 ≝ pc_costs in
1127       let 〈label, i'〉 ≝ i in
1128       let labels ≝
1129         match label with
1130         [ None ⇒ labels
1131         | Some label ⇒
1132           let program_counter_bv ≝ bitvector_of_nat ? pc in
1133             insert ? ? label program_counter_bv labels]
1134       in
1135         let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
1136          〈labels, 〈S ppc,construct〉〉
1137    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
1138  in
1139   let 〈labels, ppc_pc_costs〉 ≝ result in
1140   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
1141   let 〈pc, costs〉 ≝ pc_costs in
1142    〈labels, costs〉.
1143 [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
1144   generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
1145   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
1146   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
1147   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
1148   | #id normalize nodelta; -labels1; cases label; normalize nodelta
1149     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
1150     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
1151       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
1152        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
1153          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
1154        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
1155          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
1156 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
1157 | generalize in match (sig2 … result) in ⊢ ?;
1158   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?)
1159   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
1160qed.
1161
1162definition assembly:
1163 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝
1164  λp.let 〈preamble, instr_list〉 ≝ p in
1165   λpol.
1166    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
1167    let datalabels ≝ construct_datalabels preamble in
1168    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
1169    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
1170    let result ≝
1171     foldl_strong
1172      (option Identifier × pseudo_instruction)
1173      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
1174        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
1175        let 〈ppc,code〉 ≝ ppc_code in
1176         ∀ppc'.
1177          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
1178          let 〈len,assembledi〉 ≝
1179           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
1180           True)
1181      instr_list
1182      (λprefix,hd,tl,prf,pc_ppc_code.
1183        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
1184        let 〈ppc, code〉 ≝ ppc_code in
1185        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
1186        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
1187        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
1188         〈new_pc, 〈new_ppc, (code @ program)〉〉)
1189      〈(zero ?), 〈(zero ?), [ ]〉〉
1190    in
1191     〈\snd (\snd result), costs〉.
1192 [2,5: %
1193 |*: cases daemon ]
1194qed.
1195
1196definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
1197 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.