source: src/ASM/Assembly.ma @ 1646

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

Policy now depends on Assembly and not the other way around.

File size: 48.1 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Status.ma".
5include alias "basics/logic.ma".
6include alias "arithmetics/nat.ma".
7include "utilities/extralib.ma".
8
9(**************************************** START OF POLICY ABSTRACTION ********************)
10
11(* definition of & operations on jump length *)
12inductive jump_length: Type[0] ≝
13  | short_jump: jump_length
14  | medium_jump: jump_length
15  | long_jump: jump_length.
16
17definition policy_type ≝ Word → jump_length.
18
19definition assembly_preinstruction ≝
20  λA: Type[0].
21  λaddr_of: A → Byte. (* relative *)
22  λpre: preinstruction A.
23  match pre with
24  [ ADD addr1 addr2 ⇒
25     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
26      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
27      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
28      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
29      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
30      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
31  | ADDC addr1 addr2 ⇒
32     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
33      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
34      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
35      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
36      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
37      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
38  | ANL addrs ⇒
39     match addrs with
40      [ inl addrs ⇒ match addrs with
41         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
42           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
43            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
44            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
45            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
46            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
47            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
48         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
49            let b1 ≝
50             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
51              [ DIRECT b1 ⇒ λ_.b1
52              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
53            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
54             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
55             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
56             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
57         ]
58      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
59         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
60          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
61          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
62          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
63  | CLR addr ⇒
64     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
65      [ ACC_A ⇒ λ_.
66         [ ([[true; true; true; false; false; true; false; false]]) ]
67      | CARRY ⇒ λ_.
68         [ ([[true; true; false; false; false; false; true; true]]) ]
69      | BIT_ADDR b1 ⇒ λ_.
70         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
71      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
72  | CPL addr ⇒
73     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
74      [ ACC_A ⇒ λ_.
75         [ ([[true; true; true; true; false; true; false; false]]) ]
76      | CARRY ⇒ λ_.
77         [ ([[true; false; true; true; false; false; true; true]]) ]
78      | BIT_ADDR b1 ⇒ λ_.
79         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
80      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
81  | DA addr ⇒
82     [ ([[true; true; false; true; false; true; false; false]]) ]
83  | DEC addr ⇒
84     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
85      [ ACC_A ⇒ λ_.
86         [ ([[false; false; false; true; false; true; false; false]]) ]
87      | REGISTER r ⇒ λ_.
88         [ ([[false; false; false; true; true]]) @@ r ]
89      | DIRECT b1 ⇒ λ_.
90         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
91      | INDIRECT i1 ⇒ λ_.
92         [ ([[false; false; false; true; false; true; true; i1]]) ]
93      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
94      | DJNZ addr1 addr2 ⇒
95         let b2 ≝ addr_of addr2 in
96         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
97          [ REGISTER r ⇒ λ_.
98             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
99          | DIRECT b1 ⇒ λ_.
100             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
101          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
102      | JC addr ⇒
103        let b1 ≝ addr_of addr in
104          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
105      | JNC addr ⇒
106         let b1 ≝ addr_of addr in
107           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
108      | JZ addr ⇒
109         let b1 ≝ addr_of addr in
110           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
111      | JNZ addr ⇒
112         let b1 ≝ addr_of addr in
113           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
114      | JB 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; true; false; false; false; false; false]]); b1; b2 ]
119          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
120      | JNB addr1 addr2 ⇒
121         let b2 ≝ addr_of addr2 in
122         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
123          [ BIT_ADDR b1 ⇒ λ_.
124             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
125          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
126      | JBC addr1 addr2 ⇒
127         let b2 ≝ addr_of addr2 in
128         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
129          [ BIT_ADDR b1 ⇒ λ_.
130             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
131          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
132      | CJNE addrs addr3 ⇒
133         let b3 ≝ addr_of addr3 in
134         match addrs with
135          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
136             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
137              [ DIRECT b1 ⇒ λ_.
138                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
139              | DATA b1 ⇒ λ_.
140                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
141              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
142          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
143             let b2 ≝
144              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
145               [ DATA b2 ⇒ λ_. b2
146               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
147             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
148              [ REGISTER r ⇒ λ_.
149                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
150              | INDIRECT i1 ⇒ λ_.
151                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
152              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
153         ]
154  | DIV addr1 addr2 ⇒
155     [ ([[true;false;false;false;false;true;false;false]]) ]
156  | INC addr ⇒
157     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
158      [ ACC_A ⇒ λ_.
159         [ ([[false;false;false;false;false;true;false;false]]) ]         
160      | REGISTER r ⇒ λ_.
161         [ ([[false;false;false;false;true]]) @@ r ]
162      | DIRECT b1 ⇒ λ_.
163         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
164      | INDIRECT i1 ⇒ λ_.
165        [ ([[false; false; false; false; false; true; true; i1]]) ]
166      | DPTR ⇒ λ_.
167        [ ([[true;false;true;false;false;false;true;true]]) ]
168      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
169  | MOV addrs ⇒
170     match addrs with
171      [ inl addrs ⇒
172         match addrs with
173          [ inl addrs ⇒
174             match addrs with
175              [ inl addrs ⇒
176                 match addrs with
177                  [ inl addrs ⇒
178                     match addrs with
179                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
180                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
181                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
182                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
183                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
184                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
185                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
186                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
187                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
188                          [ REGISTER r ⇒ λ_.
189                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
190                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
191                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
192                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
193                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
194                          | INDIRECT i1 ⇒ λ_.
195                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
196                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
197                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
198                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
199                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
200                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
201                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
202                     let b1 ≝
203                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
204                       [ DIRECT b1 ⇒ λ_. b1
205                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
206                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
207                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
208                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
209                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
210                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
211                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
212                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
213              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
214                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
215                  [ DATA16 w ⇒ λ_.
216                     let b1_b2 ≝ split ? 8 8 w in
217                     let b1 ≝ \fst b1_b2 in
218                     let b2 ≝ \snd b1_b2 in
219                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
220                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
221          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
222             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
223              [ BIT_ADDR b1 ⇒ λ_.
224                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
225              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
226      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
227         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
228          [ BIT_ADDR b1 ⇒ λ_.
229             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
230          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
231  | MOVX addrs ⇒
232     match addrs with
233      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
234         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
235          [ EXT_INDIRECT i1 ⇒ λ_.
236             [ ([[true;true;true;false;false;false;true;i1]]) ]
237          | EXT_INDIRECT_DPTR ⇒ λ_.
238             [ ([[true;true;true;false;false;false;false;false]]) ]
239          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
240      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
241         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
242          [ EXT_INDIRECT i1 ⇒ λ_.
243             [ ([[true;true;true;true;false;false;true;i1]]) ]
244          | EXT_INDIRECT_DPTR ⇒ λ_.
245             [ ([[true;true;true;true;false;false;false;false]]) ]
246          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
247  | MUL addr1 addr2 ⇒
248     [ ([[true;false;true;false;false;true;false;false]]) ]
249  | NOP ⇒
250     [ ([[false;false;false;false;false;false;false;false]]) ]
251  | ORL addrs ⇒
252     match addrs with
253      [ inl addrs ⇒
254         match addrs with
255          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
256             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
257             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
258             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
259             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
260             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
261             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
262          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
263            let b1 ≝
264              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
265               [ DIRECT b1 ⇒ λ_. b1
266               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
267             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
268              [ ACC_A ⇒ λ_.
269                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
270              | DATA b2 ⇒ λ_.
271                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
272              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
273      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
274         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
275          [ BIT_ADDR b1 ⇒ λ_.
276             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
277          | N_BIT_ADDR b1 ⇒ λ_.
278             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
279          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
280  | POP addr ⇒
281     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
282      [ DIRECT b1 ⇒ λ_.
283         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
284      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
285  | PUSH addr ⇒
286     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
287      [ DIRECT b1 ⇒ λ_.
288         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
289      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
290  | RET ⇒
291     [ ([[false;false;true;false;false;false;true;false]]) ]
292  | RETI ⇒
293     [ ([[false;false;true;true;false;false;true;false]]) ]
294  | RL addr ⇒
295     [ ([[false;false;true;false;false;false;true;true]]) ]
296  | RLC addr ⇒
297     [ ([[false;false;true;true;false;false;true;true]]) ]
298  | RR addr ⇒
299     [ ([[false;false;false;false;false;false;true;true]]) ]
300  | RRC addr ⇒
301     [ ([[false;false;false;true;false;false;true;true]]) ]
302  | SETB addr ⇒     
303     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
304      [ CARRY ⇒ λ_.
305         [ ([[true;true;false;true;false;false;true;true]]) ]
306      | BIT_ADDR b1 ⇒ λ_.
307         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
308      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
309  | SUBB addr1 addr2 ⇒
310     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
311      [ REGISTER r ⇒ λ_.
312         [ ([[true;false;false;true;true]]) @@ r ]
313      | DIRECT b1 ⇒ λ_.
314         [ ([[true;false;false;true;false;true;false;true]]); b1]
315      | INDIRECT i1 ⇒ λ_.
316         [ ([[true;false;false;true;false;true;true;i1]]) ]
317      | DATA b1 ⇒ λ_.
318         [ ([[true;false;false;true;false;true;false;false]]); b1]
319      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
320  | SWAP addr ⇒
321     [ ([[true;true;false;false;false;true;false;false]]) ]
322  | XCH addr1 addr2 ⇒
323     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
324      [ REGISTER r ⇒ λ_.
325         [ ([[true;true;false;false;true]]) @@ r ]
326      | DIRECT b1 ⇒ λ_.
327         [ ([[true;true;false;false;false;true;false;true]]); b1]
328      | INDIRECT i1 ⇒ λ_.
329         [ ([[true;true;false;false;false;true;true;i1]]) ]
330      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
331  | XCHD addr1 addr2 ⇒
332     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
333      [ INDIRECT i1 ⇒ λ_.
334         [ ([[true;true;false;true;false;true;true;i1]]) ]
335      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
336  | XRL addrs ⇒
337     match addrs with
338      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
339         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
340          [ REGISTER r ⇒ λ_.
341             [ ([[false;true;true;false;true]]) @@ r ]
342          | DIRECT b1 ⇒ λ_.
343             [ ([[false;true;true;false;false;true;false;true]]); b1]
344          | INDIRECT i1 ⇒ λ_.
345             [ ([[false;true;true;false;false;true;true;i1]]) ]
346          | DATA b1 ⇒ λ_.
347             [ ([[false;true;true;false;false;true;false;false]]); b1]
348          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
349      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
350         let b1 ≝
351          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
352           [ DIRECT b1 ⇒ λ_. b1
353           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
354         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
355          [ ACC_A ⇒ λ_.
356             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
357          | DATA b2 ⇒ λ_.
358             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
359          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
360       ].
361
362definition assembly1 ≝
363 λi: instruction.
364 match i with
365  [ ACALL addr ⇒
366     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
367      [ ADDR11 w ⇒ λ_.
368         let v1_v2 ≝ split ? 3 8 w in
369         let v1 ≝ \fst v1_v2 in
370         let v2 ≝ \snd v1_v2 in
371          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
372      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
373  | AJMP addr ⇒
374     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
375      [ ADDR11 w ⇒ λ_.
376         let v1_v2 ≝ split ? 3 8 w in
377         let v1 ≝ \fst v1_v2 in
378         let v2 ≝ \snd v1_v2 in
379          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
380      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
381  | JMP adptr ⇒
382     [ ([[false;true;true;true;false;false;true;true]]) ]
383  | LCALL addr ⇒
384     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
385      [ ADDR16 w ⇒ λ_.
386         let b1_b2 ≝ split ? 8 8 w in
387         let b1 ≝ \fst b1_b2 in
388         let b2 ≝ \snd b1_b2 in
389          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
390      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
391  | LJMP addr ⇒
392     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
393      [ ADDR16 w ⇒ λ_.
394         let b1_b2 ≝ split ? 8 8 w in
395         let b1 ≝ \fst b1_b2 in
396         let b2 ≝ \snd b1_b2 in
397          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
398      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
399  | MOVC addr1 addr2 ⇒
400     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
401      [ ACC_DPTR ⇒ λ_.
402         [ ([[true;false;false;true;false;false;true;true]]) ]
403      | ACC_PC ⇒ λ_.
404         [ ([[true;false;false;false;false;false;true;true]]) ]
405      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
406  | SJMP addr ⇒
407     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
408      [ RELATIVE b1 ⇒ λ_.
409         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
410      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
411  | RealInstruction instr ⇒
412    assembly_preinstruction [[ relative ]]
413      (λx.
414        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
415        [ RELATIVE r ⇒ λ_. r
416        | _ ⇒ λabsd. ⊥
417        ] (subaddressing_modein … x)) instr
418  ].
419  cases absd
420qed.
421
422definition expand_relative_jump_internal:
423 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
424 option (list instruction)
425 ≝
426  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
427  match jmp_len with
428  [ short_jump ⇒
429     let lookup_address ≝ lookup_labels jmp in
430     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
431     let 〈upper, lower〉 ≝ split ? 8 8 result in
432     if eq_bv ? upper (zero 8) then
433      let address ≝ RELATIVE lower in
434       Some ? [ RealInstruction (i address) ]
435     else
436       None ?
437  | medium_jump ⇒ None …
438  | long_jump ⇒
439    Some ?
440    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
441      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
442      LJMP (ADDR16 (lookup_labels jmp))
443    ]
444  ].
445  @ I
446qed.
447
448definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
449  λlookup_labels.
450  λjmp_len: jump_length.
451  λpc.
452  λi: preinstruction Identifier.
453  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
454  match i with
455  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
456  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
457  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
458  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
459  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
460  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
461  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
462  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
463  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
464  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
465  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
466  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
467  | INC arg ⇒ Some ? [ INC ? arg ]
468  | DEC arg ⇒ Some ? [ DEC ? arg ]
469  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
470  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
471  | DA arg ⇒ Some ? [ DA ? arg ]
472  | ANL arg ⇒ Some ? [ ANL ? arg ]
473  | ORL arg ⇒ Some ? [ ORL ? arg ]
474  | XRL arg ⇒ Some ? [ XRL ? arg ]
475  | CLR arg ⇒ Some ? [ CLR ? arg ]
476  | CPL arg ⇒ Some ? [ CPL ? arg ]
477  | RL arg ⇒ Some ? [ RL ? arg ]
478  | RR arg ⇒ Some ? [ RR ? arg ]
479  | RLC arg ⇒ Some ? [ RLC ? arg ]
480  | RRC arg ⇒ Some ? [ RRC ? arg ]
481  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
482  | MOV arg ⇒ Some ? [ MOV ? arg ]
483  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
484  | SETB arg ⇒ Some ? [ SETB ? arg ]
485  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
486  | POP arg ⇒ Some ? [ POP ? arg ]
487  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
488  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
489  | RET ⇒ Some ? [ RET ? ]
490  | RETI ⇒ Some ? [ RETI ? ]
491  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
492  ].
493
494
495definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
496  λlookup_labels.
497  λlookup_datalabels.
498  λpc.
499  λjmp_len.
500  λi.
501  match i with
502  [ Cost cost ⇒ Some ? [ ]
503  | Comment comment ⇒ Some ? [ ]
504  | Call call ⇒
505    match jmp_len with
506    [ short_jump ⇒ None ?
507    | medium_jump ⇒
508      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
509      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
510      if eq_bv ? ignore fst_5 then
511        let address ≝ ADDR11 address in
512          Some ? ([ ACALL address ])
513      else
514        None ?
515    | long_jump ⇒
516      let address ≝ ADDR16 (lookup_labels call) in
517        Some ? [ LCALL address ]
518    ]
519  | Mov d trgt ⇒
520    let address ≝ DATA16 (lookup_datalabels trgt) in
521      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
522  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
523  | Jmp jmp ⇒
524    match jmp_len with
525    [ short_jump ⇒
526      let lookup_address ≝ lookup_labels jmp in
527      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
528      let 〈upper, lower〉 ≝ split ? 8 8 result in
529      if eq_bv ? upper (zero 8) then
530        let address ≝ RELATIVE lower in
531          Some ? [ SJMP address ]
532      else
533        None ?
534    | medium_jump ⇒
535      let address ≝ lookup_labels jmp in
536      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
537      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
538      if eq_bv ? fst_5_addr fst_5_pc then
539        let address ≝ ADDR11 rest_addr in
540          Some ? ([ AJMP address ])
541      else
542        None ?
543    | long_jump ⇒
544      let address ≝ ADDR16 (lookup_labels jmp) in
545        Some ? [ LJMP address ]
546    ]
547  ].
548  @ I
549qed.
550
551
552definition assembly_1_pseudoinstruction_safe ≝
553  λprogram: pseudo_assembly_program.
554  λjump_expansion: policy_type.
555  λppc: Word.
556  λpc: Word.
557  λlookup_labels.
558  λlookup_datalabels.
559  λi.
560  let expansion ≝ jump_expansion ppc in
561    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
562    [ None ⇒ None ?
563    | Some pseudos ⇒
564      let mapped ≝ map ? ? assembly1 pseudos in
565      let flattened ≝ flatten ? mapped in
566      let pc_len ≝ length ? flattened in
567        Some ? (〈pc_len, flattened〉)
568    ].
569 
570definition construct_costs_safe ≝
571  λprogram.
572  λjump_expansion: policy_type.
573  λpseudo_program_counter: nat.
574  λprogram_counter: nat.
575  λcosts: BitVectorTrie costlabel 16.
576  λi.
577  match i with
578  [ Cost cost ⇒
579    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
580      Some ? 〈program_counter, (insert … program_counter_bv cost costs)〉
581  | _ ⇒
582    let pc_bv ≝ bitvector_of_nat ? program_counter in
583    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
584    let lookup_labels ≝ λx.pc_bv in
585    let lookup_datalabels ≝ λx.zero ? in
586    let pc_delta_assembled ≝
587      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
588        lookup_labels lookup_datalabels i
589    in
590    match pc_delta_assembled with
591    [ None ⇒ None ?
592    | Some pc_delta_assembled ⇒
593      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
594        Some ? 〈pc_delta + program_counter, costs〉       
595    ]
596  ].
597
598(* This establishes the correspondence between pseudo program counters and
599   program counters. It is at the heart of the proof. *)
600(*CSC: code taken from build_maps *)
601definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
602 λinstr_list.
603 λjump_expansion: policy_type.
604 λl:list labelled_instruction.
605 λacc.
606  foldl …
607   (λt,i.
608       match t with
609       [ None ⇒ None …
610       | Some ppc_pc_map ⇒
611         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
612         let 〈program_counter, sigma_map〉 ≝ pc_map in
613         let 〈label, i〉 ≝ i in
614          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
615           [ None ⇒ None ?
616           | Some pc_ignore ⇒
617              let 〈pc,ignore〉 ≝ pc_ignore in
618                Some … 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ]
619       ]) acc l.
620
621definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) ≝
622  λprog.
623  λjump_expansion.
624    sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, Stub …〉〉).
625
626definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
627 λprogram,jump_expansion,instr_list.
628  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
629   [ None ⇒ None …
630   | Some result ⇒
631      let 〈ppc,pc_sigma_map〉 ≝ result in
632      let 〈pc,map〉 ≝ pc_sigma_map in
633       Some … 〈ppc,pc〉 ].
634
635definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
636 λinstr_list,jump_expansion.
637  match sigma0 instr_list jump_expansion with
638  [ None ⇒ None ?
639  | Some result ⇒
640    let 〈ppc,pc_sigma_map〉 ≝ result in
641    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
642      if gtb pc (2^16) then
643        None ?
644      else
645        Some ? (λx. lookup … x sigma_map (zero …)) ].
646
647(* stuff about policy *)
648
649definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
650
651definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
652
653lemma eject_policy: ∀p. policy p → policy_type.
654 #p #pol @(pi1 … pol)
655qed.
656
657coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
658
659definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
660 λp,policy.
661  match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
662   [ None ⇒ λabs. ⊥
663   | Some r ⇒ λ_.r] (pi2 … policy).
664 cases abs /2/
665qed.
666
667example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
668 cases daemon.
669qed.
670
671axiom fetch_pseudo_instruction_split:
672 ∀instr_list,ppc.
673  ∃pre,suff,lbl.
674   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
675
676lemma sigma00_append:
677 ∀instr_list,jump_expansion,l1,l2,acc.
678  sigma00 instr_list jump_expansion (l1@l2) acc =
679   sigma00 instr_list jump_expansion
680    l2 (sigma00 instr_list jump_expansion l1 acc).
681 whd in match sigma00; normalize nodelta;
682 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
683qed.
684
685lemma sigma00_strict:
686 ∀instr_list,jump_expansion,l,acc. acc = None ? →
687  sigma00 instr_list jump_expansion l acc = None ….
688 #instr_list #jump_expansion #l elim l
689  [ #acc #H >H %
690  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
691qed.
692
693lemma policy_ok_prefix_ok:
694 ∀program.∀pol:policy program.∀suffix,prefix.
695  prefix@suffix = \snd program →
696   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
697 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
698 generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol
699 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
700 normalize nodelta >sigma00_append
701 cases (sigma00 ?? prefix ?)
702  [2: #x #_ % #abs destruct(abs)
703  | * #abs @⊥ @abs >sigma00_strict % ]
704qed.
705
706lemma policy_ok_prefix_hd_ok:
707 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
708  (prefix@[hd])@suffix = \snd program →
709   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
710    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
711    let 〈program_counter, sigma_map〉 ≝ pc_map in
712    let 〈label, i〉 ≝ hd in
713     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
714 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
715 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
716  (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
717 @pair_elim #ppc #pc_map #EQ3 normalize nodelta
718 @pair_elim #pc #map #EQ4 normalize nodelta
719 @pair_elim #l' #i' #EQ5 normalize nodelta
720 cases (construct_costs_safe ??????) normalize
721  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
722qed.
723
724definition expand_pseudo_instruction:
725 ∀program:pseudo_assembly_program.∀pol: policy program.
726  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
727  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
728  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
729  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
730  pc = sigma program pol ppc →
731  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
732≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
733   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
734    [ None ⇒ let dummy ≝ [ ] in dummy
735    | Some res ⇒ res ].
736 [ @⊥ whd in p:(??%??);
737   generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);
738   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
739   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
740   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
741   #res #K
742   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
743   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
744   cases daemon (* CSC: XXXXXXXX Ero qui
745   
746    [3: @policy_ok_prefix_ok ]
747    | sigma00 program pol pre
748
749
750
751   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
752   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
753   per concludere construct_costs_safe ≠ None *)
754 | >p %]
755qed.
756
757(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
758definition assembly_1_pseudoinstruction':
759 ∀program:pseudo_assembly_program.∀pol: policy program.
760  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
761  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
762  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
763  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
764  Σres:(nat × (list Byte)).
765   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
766   let 〈len,code〉 ≝ res in
767    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
768     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
769≝ λprogram: pseudo_assembly_program.
770  λpol: policy program.
771  λppc: Word.
772  λlookup_labels.
773  λlookup_datalabels.
774  λpi.
775  λprf1,prf2,prf3.
776   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
777    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
778    | Some res ⇒ res ].
779 [ @⊥ elim pi in p; [*]
780   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
781   generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
782   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
783   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
784   cases daemon
785 | % [ >p %]
786   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
787   (* THIS SHOULD BE TRUE INSTEAD *)
788   cases daemon]
789qed.
790
791definition assembly_1_pseudoinstruction:
792 ∀program:pseudo_assembly_program.∀pol: policy program.
793  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
794  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
795  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
796  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
797   nat × (list Byte)
798≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
799   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
800    prf2 prf3.
801
802lemma assembly_1_pseudoinstruction_ok1:
803 ∀program:pseudo_assembly_program.∀pol: policy program.
804  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
805  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
806  ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
807  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
808     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
809   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
810 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
811 cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
812 #H1 #_ @H1
813qed.
814
815(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
816definition construct_costs':
817 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
818  Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
819
820  λprogram.λpol: policy program.λppc,pc,costs,i.
821   match construct_costs_safe program pol ppc pc costs i with
822    [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
823    | Some res ⇒ res ].
824 [ cases daemon
825 | >p %]
826qed.
827
828definition construct_costs ≝
829 λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i).
830
831(*
832axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
833axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
834
835axiom foldl_strong_step:
836 ∀A:Type[0].
837  ∀P: list A → Type[0].
838   ∀l: list A.
839    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
840     ∀acc: P [ ].
841      ∀Q: ∀prefix. P prefix → Prop.
842       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
843        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
844       Q [ ] acc →
845        Q l (foldl_strong A P l H acc).
846(*
847 #A #P #l #H #acc #Q #HQ #Hacc normalize;
848 generalize in match
849  (foldl_strong ?
850   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
851   l ? Hacc)
852 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
853 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
854 #K
855
856 generalize in match
857  (foldl_strong ?
858   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
859 [2: @H
860*)
861
862axiom foldl_elim:
863 ∀A:Type[0].
864  ∀B: Type[0].
865   ∀H: A → B → A.
866    ∀acc: A.
867     ∀l: list B.
868      ∀Q: A → Prop.
869       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
870         Q acc →
871          Q (foldl A B H acc l).
872*)
873
874lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
875 #A #a #b #EQ destruct //
876qed.
877
878(*
879lemma tech_pc_sigma00_append_Some:
880 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
881  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
882   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
883 #program #pol #prefix #costs #label #i #ppc #pc #H
884  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
885  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
886  generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
887  whd in match sigma0; normalize nodelta;
888  >foldl_step
889  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
890  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
891  cases (sigma00 program pol prefix) in H ⊢ %
892   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
893   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
894     
895     normalize nodelta; -H;
896     
897 
898   generalize in match H; -H;
899  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
900   [2: whd in ⊢ (??%%)
901XXX
902*)
903
904axiom construct_costs_sigma:
905 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
906  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
907   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
908
909axiom tech_pc_sigma00_append_Some:
910 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
911  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
912   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
913
914axiom eq_identifier_eq:
915  ∀tag: String.
916  ∀l.
917  ∀r.
918    eq_identifier tag l r = true → l = r.
919
920axiom neq_identifier_neq:
921  ∀tag: String.
922  ∀l, r: identifier tag.
923    eq_identifier tag l r = false → (l = r → False).
924
925definition build_maps:
926 ∀pseudo_program.∀pol:policy pseudo_program.
927  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
928   let 〈labels, costs〉 ≝ res in
929    ∀id. occurs_exactly_once id (\snd pseudo_program) →
930     lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
931  λpseudo_program.
932  λpol:policy pseudo_program.
933    let result ≝
934      foldl_strong
935        (option Identifier × pseudo_instruction)
936          (λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))).
937            let 〈labels,ppc_pc_costs〉 ≝ res in
938            let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
939            let 〈pc',costs〉 ≝ pc_costs in
940              And ( And (
941              And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
942                (ppc' = length … pre)) (*∧ *)
943                (tech_pc_sigma00 pseudo_program (pi1 … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
944                (∀id. occurs_exactly_once id pre →
945                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
946                (\snd pseudo_program)
947        (λprefix,i,tl,prf,t.
948          let 〈labels, ppc_pc_costs〉 ≝ t in
949          let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
950          let 〈pc,costs〉 ≝ pc_costs in
951          let 〈label, i'〉 ≝ i in
952          let labels ≝
953            match label with
954            [ None ⇒ labels
955            | Some label ⇒
956                let program_counter_bv ≝ bitvector_of_nat ? pc in
957                  add ? ? labels label program_counter_bv
958            ]
959          in
960            let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
961              〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
962    in
963      let 〈labels, ppc_pc_costs〉 ≝ result in
964      let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
965      let 〈pc, costs〉 ≝ pc_costs in
966        〈labels, costs〉.
967 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
968   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
969   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
970   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
971   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
972   | #id normalize nodelta; -labels1; cases label; normalize nodelta
973     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
974     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
975       generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
976        [ #EQ #_ <(eq_identifier_eq … EQ) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit
977          <IH0 [@IHn1 | <(eq_identifier_eq … EQ) in H; #H @H]
978        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: -IHn1;
979          (*Andrea:XXXX used to work /2/*)@nmk #IDL lapply (sym_eq ? ? ? IDL)
980          lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ]
981          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
982 |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ]
983 | generalize in match (pi2 … result) in ⊢ ?;
984   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
985   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
986qed.
987
988definition assembly:
989 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝
990  λp.let 〈preamble, instr_list〉 ≝ p in
991   λpol.
992    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
993    let datalabels ≝ construct_datalabels preamble in
994    let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in
995    let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
996    let result ≝
997     foldl_strong
998      (option Identifier × pseudo_instruction)
999      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
1000        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
1001        let 〈ppc,code〉 ≝ ppc_code in
1002         ∀ppc'.
1003          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
1004          let 〈len,assembledi〉 ≝
1005           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
1006           True)
1007      instr_list
1008      (λprefix,hd,tl,prf,pc_ppc_code.
1009        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
1010        let 〈ppc, code〉 ≝ ppc_code in
1011        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
1012        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
1013        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
1014         〈new_pc, 〈new_ppc, (code @ program)〉〉)
1015      〈(zero ?), 〈(zero ?), [ ]〉〉
1016    in
1017     〈\snd (\snd result), costs〉.
1018 [2,5: %
1019 |*: cases daemon ]
1020qed.
1021
1022definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
1023 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.