source: src/ASM/Assembly.ma @ 987

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

Real parameterization over the policy.

File size: 41.7 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 ≝ \fst 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 jump_expansion_policy ≝ BitVectorTrie jump_length 16.
437
438definition find_right_call: Word → Word → nat × (option jump_length) ≝
439 (* medium call: 11 bits, only in "current segment" *)
440 (* can this be done more efficiently with bit vector arithmetic? *)
441 λpc.λaddress.
442  let 〈p1, p2〉 ≝ split ? 5 11 address in
443  let 〈a1, a2〉 ≝ split ? 5 11 pc in
444   if eq_bv ? p1 a1 then (* we're in the same segment *)
445    〈2, Some ? medium_jump〉
446   else
447    〈3, Some ? long_jump〉.
448
449definition distance ≝
450 λx.λy.if gtb x y then x - y else y - x.
451 
452definition find_right_jump: Word → Word → nat × (option jump_length) ≝
453 (* short jump: 8 bits signed *)
454 (* medium jump: 11 bits, forward only *)
455 λpc.λaddress.
456  let pn ≝ nat_of_bitvector ? pc in
457  let pa ≝ nat_of_bitvector ? address in
458   if ltb (distance pn pa) 127 then
459    〈2, Some ? short_jump〉
460   else
461    find_right_call pc address.
462
463definition find_right_relative_jump: Word → (BitVectorTrie Word 16) →
464 Identifier → nat × (option jump_length) ≝
465 λpc.λlabels.λjmp.
466 match lookup_opt ? ? jmp labels with
467 [ None ⇒ 〈2, Some ? short_jump〉
468 | Some a ⇒ find_right_jump pc a ].
469 
470definition jep_relative: Word → (BitVectorTrie Word 16) → preinstruction Identifier → ? ≝
471 λpc.λlabels.λi.
472  match i with
473  [ JC jmp ⇒ find_right_relative_jump pc labels jmp
474  | JNC jmp ⇒ find_right_relative_jump pc labels jmp
475  | JB baddr jmp ⇒ find_right_relative_jump pc labels jmp
476  | JZ jmp ⇒ find_right_relative_jump pc labels jmp
477  | JNZ jmp ⇒ find_right_relative_jump pc labels jmp
478  | JBC baddr jmp ⇒ find_right_relative_jump pc labels jmp
479  | JNB baddr jmp ⇒ find_right_relative_jump pc labels jmp
480  | CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp
481  | DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp
482  | _ ⇒ 〈length ? (assembly_preinstruction ? (λx.zero ?) i), None …〉 ].
483 
484definition jump_expansion_policy_internal: pseudo_assembly_program →
485 (BitVectorTrie Word 16) → jump_expansion_policy →
486 ((BitVectorTrie Word 16) × jump_expansion_policy × bool)≝
487 λprogram.λlabels.λpolicy.
488   let 〈pc, new_labels, new_policy, changed〉 ≝
489   foldl ? ? (λacc.λi:labelled_instruction.
490    let 〈label, instr〉 ≝ i in
491    let 〈pc,labels,policy,c0〉 ≝ acc in
492    let 〈c1,new_labels〉 ≝ match label with
493     [ None ⇒ 〈c0,labels〉
494     | Some l ⇒
495       match update ? ? pc l labels with
496       [ None ⇒ 〈c0,labels〉
497       | Some x ⇒ 〈true, x〉 ] ] in
498    let 〈pc_delta, jmp_len〉 ≝ match instr with
499     [ Call c ⇒
500       match lookup_opt ? ? c new_labels with
501        [ None        ⇒ 〈2, Some ? medium_jump〉
502        | Some c_addr ⇒ find_right_call pc c_addr ]
503     | Jmp j ⇒
504       match lookup_opt ? ? j new_labels with
505        [ None        ⇒ 〈2, Some ? short_jump〉
506        | Some j_addr ⇒ find_right_jump pc j_addr ]
507     | Instruction i ⇒ jep_relative pc new_labels i
508     | Mov _ _ ⇒ 〈3, None …〉
509     | Cost _ ⇒ 〈0, None …〉
510     | Comment _ ⇒ 〈0, None …〉 ] in
511    let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
512    match jmp_len with
513    [ None   ⇒ 〈new_pc, new_labels, policy, c1〉
514    | Some j ⇒
515      match update ? ? pc j policy with
516      [ None ⇒ 〈new_pc, new_labels, policy, c1〉
517      | Some x ⇒ 〈new_pc, new_labels, x, true〉 ] ]
518   ) 〈zero ?, labels, policy, false〉 (\snd program) in
519   〈labels, policy, changed〉.
520
521definition expand_relative_jump_internal:
522 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
523 option (list instruction)
524 ≝
525  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
526  match jmp_len with
527  [ short_jump ⇒
528     let lookup_address ≝ lookup_labels jmp in
529     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
530     let 〈upper, lower〉 ≝ split ? 8 8 result in
531     if eq_bv ? upper (zero 8) then
532      let address ≝ RELATIVE lower in
533       Some ? [ RealInstruction (i address) ]
534     else
535       None ?
536  | medium_jump ⇒ None …
537  | long_jump ⇒
538    Some ?
539    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
540      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
541      LJMP (ADDR16 (lookup_labels jmp))
542    ]
543  ].
544  @ I
545qed.
546
547definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
548  λlookup_labels.
549  λjmp_len: jump_length.
550  λpc.
551  λi: preinstruction Identifier.
552  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
553  match i with
554  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
555  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
556  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
557  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
558  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
559  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
560  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
561  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
562  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
563  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
564  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
565  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
566  | INC arg ⇒ Some ? [ INC ? arg ]
567  | DEC arg ⇒ Some ? [ DEC ? arg ]
568  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
569  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
570  | DA arg ⇒ Some ? [ DA ? arg ]
571  | ANL arg ⇒ Some ? [ ANL ? arg ]
572  | ORL arg ⇒ Some ? [ ORL ? arg ]
573  | XRL arg ⇒ Some ? [ XRL ? arg ]
574  | CLR arg ⇒ Some ? [ CLR ? arg ]
575  | CPL arg ⇒ Some ? [ CPL ? arg ]
576  | RL arg ⇒ Some ? [ RL ? arg ]
577  | RR arg ⇒ Some ? [ RR ? arg ]
578  | RLC arg ⇒ Some ? [ RLC ? arg ]
579  | RRC arg ⇒ Some ? [ RRC ? arg ]
580  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
581  | MOV arg ⇒ Some ? [ MOV ? arg ]
582  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
583  | SETB arg ⇒ Some ? [ SETB ? arg ]
584  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
585  | POP arg ⇒ Some ? [ POP ? arg ]
586  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
587  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
588  | RET ⇒ Some ? [ RET ? ]
589  | RETI ⇒ Some ? [ RETI ? ]
590  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
591  ].
592
593definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
594  λlookup_labels.
595  λlookup_datalabels.
596  λpc.
597  λjmp_len.
598  λi.
599  match i with
600  [ Cost cost ⇒ Some ? [ ]
601  | Comment comment ⇒ Some ? [ ]
602  | Call call ⇒
603    match jmp_len with
604    [ short_jump ⇒ None ?
605    | medium_jump ⇒
606      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
607      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
608      if eq_bv ? ignore fst_5 then
609        let address ≝ ADDR11 address in
610          Some ? ([ ACALL address ])
611      else
612        None ?
613    | long_jump ⇒
614      let address ≝ ADDR16 (lookup_labels call) in
615        Some ? [ LCALL address ]
616    ]
617  | Mov d trgt ⇒
618    let address ≝ DATA16 (lookup_datalabels trgt) in
619      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
620  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
621  | Jmp jmp ⇒
622    match jmp_len with
623    [ short_jump ⇒
624      let lookup_address ≝ lookup_labels jmp in
625      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
626      let 〈upper, lower〉 ≝ split ? 8 8 result in
627      if eq_bv ? upper (zero 8) then
628        let address ≝ RELATIVE lower in
629          Some ? [ SJMP address ]
630      else
631        None ?
632    | medium_jump ⇒
633      let address ≝ lookup_labels jmp in
634      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
635      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
636      if eq_bv ? fst_5_addr fst_5_pc then
637        let address ≝ ADDR11 rest_addr in
638          Some ? ([ AJMP address ])
639      else
640        None ?
641    | long_jump ⇒
642      let address ≝ ADDR16 (lookup_labels jmp) in
643        Some ? [ LJMP address ]
644    ]
645  ].
646  @ I
647qed.
648
649let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program)
650 (old_labels: BitVectorTrie Word 16) (old_policy: BitVectorTrie jump_length 16)
651 on n: jump_expansion_policy ≝
652 match n with
653 [ O ⇒ old_policy
654 | S n' ⇒
655   let 〈new_labels, new_policy, ch〉 ≝
656    jump_expansion_policy_internal program old_labels old_policy in
657    jump_expansion_internal n' program new_labels new_policy ].
658
659definition policy_type ≝ Word → jump_length.
660
661definition jump_expansion': pseudo_assembly_program → policy_type ≝
662 λprogram.λpc.
663  let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
664  lookup ? ? pc policy long_jump.
665 
666definition assembly_1_pseudoinstruction ≝
667  λprogram: pseudo_assembly_program.
668  λjump_expansion: policy_type.
669  λppc: Word.
670  λpc: Word.
671  λlookup_labels.
672  λlookup_datalabels.
673  λi.
674  let expansion ≝ jump_expansion ppc in
675    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
676    [ None ⇒ None ?
677    | Some pseudos ⇒
678      let mapped ≝ map ? ? assembly1 pseudos in
679      let flattened ≝ flatten ? mapped in
680      let pc_len ≝ length ? flattened in
681        Some ? (〈pc_len, flattened〉)
682    ].
683 
684definition construct_costs ≝
685  λprogram.
686  λjump_expansion: policy_type.
687  λpseudo_program_counter: nat.
688  λprogram_counter: nat.
689  λlookup_labels.
690  λlookup_datalabels.
691  λcosts: BitVectorTrie Word 16.
692  λi.
693  match i with
694  [ Cost cost ⇒
695    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
696      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
697  | _ ⇒
698    let pc_bv ≝ bitvector_of_nat ? program_counter in
699    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
700    let pc_delta_assembled ≝
701      assembly_1_pseudoinstruction program jump_expansion ppc_bv pc_bv
702        lookup_labels lookup_datalabels i
703    in
704    match pc_delta_assembled with
705    [ None ⇒ None ?
706    | Some pc_delta_assembled ⇒
707      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
708        Some ? 〈pc_delta + program_counter, costs〉       
709    ]
710  ].
711
712(* This establishes the correspondence between pseudo program counters and
713   program counters. It is at the heart of the proof. *)
714(*CSC: code taken from build_maps *)
715definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
716 λinstr_list.
717 λjump_expansion: policy_type.
718 λl:list labelled_instruction.
719  foldl ??
720   (λt,i.
721       match t with
722       [ None ⇒ None ?
723       | Some ppc_pc_map ⇒
724         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
725         let 〈program_counter, sigma_map〉 ≝ pc_map in
726         let 〈label, i〉 ≝ i in
727          match construct_costs instr_list jump_expansion ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
728           [ None ⇒ None ?
729           | Some pc_ignore ⇒
730              let 〈pc,ignore〉 ≝ pc_ignore in
731              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
732       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
733
734definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
735 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog).
736
737definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
738 λprogram,jump_expansion,instr_list.
739  match sigma00 program jump_expansion instr_list with
740   [ None ⇒ None …
741   | Some result ⇒
742      let 〈ppc,pc_sigma_map〉 ≝ result in
743      let 〈pc,map〉 ≝ pc_sigma_map in
744       Some … 〈ppc,pc〉 ].
745
746definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
747 λinstr_list,jump_expansion.
748  match sigma0 instr_list jump_expansion with
749  [ None ⇒ None ?
750  | Some result ⇒
751    let 〈ppc,pc_sigma_map〉 ≝ result in
752    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
753      if gtb pc (2^16) then
754        None ?
755      else
756        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
757
758(* stuff about policy *)
759
760definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
761
762definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
763
764lemma eject_policy: ∀p. policy p → policy_type.
765 #p #pol @(eject … pol)
766qed.
767
768coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
769
770definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
771 λp,policy.
772  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
773   [ None ⇒ λabs. ⊥
774   | Some r ⇒ λ_.r] (sig2 … policy).
775 cases abs //
776qed.
777
778example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
779 cases daemon.
780qed.
781
782axiom construct_costs_sigma:
783 ∀p.∀pol:policy p.∀ppc,pc,pc',costs,costs',i.
784  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
785   Some … 〈pc',costs'〉 = construct_costs p pol ppc pc (λx.zero 16) (λx.zero 16) costs i →
786    bitvector_of_nat ? pc' = sigma p pol (bitvector_of_nat 16 (S ppc)).
787
788axiom tech_pc_sigma00_append_Some:
789 ∀program.∀pol:policy program.∀prefix,costs,label,i,pc',code,ppc,pc.
790  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
791   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
792    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
793
794axiom tech_pc_sigma00_append_None:
795 ∀program.∀pol:policy program.∀prefix,i,ppc,pc,costs.
796  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
797   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
798    → False.
799
800definition build_maps ≝
801  λpseudo_program.λpol:policy pseudo_program.
802  let result ≝
803   foldl_strong
804    (option Identifier × pseudo_instruction)
805    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
806      let 〈labels,ppc_pc_costs〉 ≝ res in
807      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
808      let 〈pc',costs〉 ≝ pc_costs in
809       bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc') ∧
810       ppc' = length … pre ∧
811       tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉 ∧
812       ∀id. occurs_exactly_once id pre →
813        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))
814    (\snd pseudo_program)
815    (λprefix,i,tl,prf,t.
816      let 〈labels, ppc_pc_costs〉 ≝ t in
817      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
818      let 〈pc,costs〉 ≝ pc_costs in
819       let 〈label, i'〉 ≝ i in
820       let labels ≝
821         match label with
822         [ None ⇒ labels
823         | Some label ⇒
824           let program_counter_bv ≝ bitvector_of_nat ? pc in
825             insert ? ? label program_counter_bv labels
826         ]
827       in
828         match construct_costs pseudo_program pol ppc pc (λx. zero ?) (λx. zero ?) costs i' with
829         [ None ⇒
830            let dummy ≝ 〈labels,ppc_pc_costs〉 in
831             dummy
832         | Some construct ⇒ 〈labels, 〈S ppc,construct〉〉
833         ]
834    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
835  in
836   let 〈labels, ppc_pc_costs〉 ≝ result in
837   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
838   let 〈pc, costs〉 ≝ pc_costs in
839    〈labels, costs〉.
840 [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
841 | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
842   cases construct in p4 #PC #CODE #JMEQ % [% [%]]
843   [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
844   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
845   | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
846   | #id normalize nodelta; -labels1; cases label; normalize nodelta
847     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
848     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
849       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
850        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
851          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
852        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
853          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
854 | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
855   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
856qed.
857
858(*
859lemma build_maps_ok:
860 ∀p:pseudo_assembly_program.
861  let 〈labels,costs〉 ≝ build_maps' p in
862   ∀pc.
863    (nat_of_bitvector … pc) < length … (\snd p) →
864     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
865 #p cases p #preamble #instr_list
866  elim instr_list
867   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
868   | #hd #tl #IH
869    whd in ⊢ (match % with [ _ ⇒ ?])
870   ]
871qed.
872*)
873
874definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝
875  λp,pol.
876    let 〈preamble, instr_list〉 ≝ p in
877    let 〈labels,costs〉 ≝ build_maps p pol in
878    let datalabels ≝ construct_datalabels preamble in
879    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
880    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
881    let result ≝ foldr ? ? (λx. λy.
882        match y with
883        [ None ⇒ None ?
884        | Some lst ⇒
885          let 〈pc, ppc_y〉 ≝ lst in
886          let 〈ppc, y〉 ≝ ppc_y in
887          let x ≝ assembly_1_pseudoinstruction p pol ppc pc lookup_labels lookup_datalabels (\snd x) in
888          match x with
889          [ None ⇒ None ?
890          | Some x ⇒
891            let 〈pc_delta, program〉 ≝ x in
892            let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
893            let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
894              Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉
895          ]
896        ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list
897    in
898      match result with
899      [ None ⇒ None ?
900      | Some result ⇒ Some ? (〈\snd (\snd result), costs〉)].
901
902definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
903 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.