source: src/ASM/Assembly.ma @ 2015

Last change on this file since 2015 was 2015, checked in by mulligan, 8 years ago

Changes following a conversation with Jaap: as it stands computation of the length of machine code jump required to expand a pseudo relative jump was mismatched in his code and the assembler. The assembler assumed all lengths were computed from the start of the instruction, whereas Jaap's policies assumed that lengths were computed from the end. This has now been changed in the assembler, where the previous computation was incorrect. From the old point of view, it now appears that we can jump 129 forward and only 125 backward.

File size: 56.6 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 assembly_preinstruction ≝
18  λA: Type[0].
19  λaddr_of: A → Byte. (* relative *)
20  λpre: preinstruction A.
21  match pre with
22  [ ADD addr1 addr2 ⇒
23     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
24      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
25      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
26      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
27      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
28      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
29  | ADDC addr1 addr2 ⇒
30     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
31      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
32      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
33      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
34      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
35      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
36  | ANL addrs ⇒
37     match addrs with
38      [ inl addrs ⇒ match addrs with
39         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
40           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
41            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
42            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
43            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
44            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
45            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
46         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
47            let b1 ≝
48             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
49              [ DIRECT b1 ⇒ λ_.b1
50              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
51            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
52             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
53             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
54             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
55         ]
56      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
57         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
58          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
59          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
60          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
61  | CLR addr ⇒
62     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
63      [ ACC_A ⇒ λ_.
64         [ ([[true; true; true; false; false; true; false; false]]) ]
65      | CARRY ⇒ λ_.
66         [ ([[true; true; false; false; false; false; true; true]]) ]
67      | BIT_ADDR b1 ⇒ λ_.
68         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
69      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
70  | CPL addr ⇒
71     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
72      [ ACC_A ⇒ λ_.
73         [ ([[true; true; true; true; false; true; false; false]]) ]
74      | CARRY ⇒ λ_.
75         [ ([[true; false; true; true; false; false; true; true]]) ]
76      | BIT_ADDR b1 ⇒ λ_.
77         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
78      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
79  | DA addr ⇒
80     [ ([[true; true; false; true; false; true; false; false]]) ]
81  | DEC addr ⇒
82     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
83      [ ACC_A ⇒ λ_.
84         [ ([[false; false; false; true; false; true; false; false]]) ]
85      | REGISTER r ⇒ λ_.
86         [ ([[false; false; false; true; true]]) @@ r ]
87      | DIRECT b1 ⇒ λ_.
88         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
89      | INDIRECT i1 ⇒ λ_.
90         [ ([[false; false; false; true; false; true; true; i1]]) ]
91      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
92      | DJNZ addr1 addr2 ⇒
93         let b2 ≝ addr_of addr2 in
94         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
95          [ REGISTER r ⇒ λ_.
96             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
97          | DIRECT b1 ⇒ λ_.
98             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
99          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
100      | JC addr ⇒
101        let b1 ≝ addr_of addr in
102          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
103      | JNC addr ⇒
104         let b1 ≝ addr_of addr in
105           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
106      | JZ addr ⇒
107         let b1 ≝ addr_of addr in
108           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
109      | JNZ addr ⇒
110         let b1 ≝ addr_of addr in
111           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
112      | JB addr1 addr2 ⇒
113         let b2 ≝ addr_of addr2 in
114         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
115          [ BIT_ADDR b1 ⇒ λ_.
116             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
117          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
118      | JNB addr1 addr2 ⇒
119         let b2 ≝ addr_of addr2 in
120         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
121          [ BIT_ADDR b1 ⇒ λ_.
122             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
123          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
124      | JBC addr1 addr2 ⇒
125         let b2 ≝ addr_of addr2 in
126         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
127          [ BIT_ADDR b1 ⇒ λ_.
128             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
129          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
130      | CJNE addrs addr3 ⇒
131         let b3 ≝ addr_of addr3 in
132         match addrs with
133          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
134             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
135              [ DIRECT b1 ⇒ λ_.
136                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
137              | DATA b1 ⇒ λ_.
138                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
139              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
140          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
141             let b2 ≝
142              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
143               [ DATA b2 ⇒ λ_. b2
144               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
145             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
146              [ REGISTER r ⇒ λ_.
147                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
148              | INDIRECT i1 ⇒ λ_.
149                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
150              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
151         ]
152  | DIV addr1 addr2 ⇒
153     [ ([[true;false;false;false;false;true;false;false]]) ]
154  | INC addr ⇒
155     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
156      [ ACC_A ⇒ λ_.
157         [ ([[false;false;false;false;false;true;false;false]]) ]         
158      | REGISTER r ⇒ λ_.
159         [ ([[false;false;false;false;true]]) @@ r ]
160      | DIRECT b1 ⇒ λ_.
161         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
162      | INDIRECT i1 ⇒ λ_.
163        [ ([[false; false; false; false; false; true; true; i1]]) ]
164      | DPTR ⇒ λ_.
165        [ ([[true;false;true;false;false;false;true;true]]) ]
166      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
167  | MOV addrs ⇒
168     match addrs with
169      [ inl 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 ⇒ let 〈addr1,addr2〉 ≝ addrs in
178                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
179                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
180                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
181                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
182                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
183                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
184                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
185                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
186                          [ REGISTER r ⇒ λ_.
187                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
188                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
189                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
190                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
191                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
192                          | INDIRECT i1 ⇒ λ_.
193                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
194                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
195                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
196                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
197                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
198                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
199                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
200                     let b1 ≝
201                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
202                       [ DIRECT b1 ⇒ λ_. b1
203                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
204                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
205                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
206                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
207                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
208                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
209                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
210                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
211              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
212                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
213                  [ DATA16 w ⇒ λ_.
214                     let b1_b2 ≝ split ? 8 8 w in
215                     let b1 ≝ \fst b1_b2 in
216                     let b2 ≝ \snd b1_b2 in
217                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
218                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
219          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
220             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
221              [ BIT_ADDR b1 ⇒ λ_.
222                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
223              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
224      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
225         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
226          [ BIT_ADDR b1 ⇒ λ_.
227             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
228          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
229  | MOVX addrs ⇒
230     match addrs with
231      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
232         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
233          [ EXT_INDIRECT i1 ⇒ λ_.
234             [ ([[true;true;true;false;false;false;true;i1]]) ]
235          | EXT_INDIRECT_DPTR ⇒ λ_.
236             [ ([[true;true;true;false;false;false;false;false]]) ]
237          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
238      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
239         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
240          [ EXT_INDIRECT i1 ⇒ λ_.
241             [ ([[true;true;true;true;false;false;true;i1]]) ]
242          | EXT_INDIRECT_DPTR ⇒ λ_.
243             [ ([[true;true;true;true;false;false;false;false]]) ]
244          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
245  | MUL addr1 addr2 ⇒
246     [ ([[true;false;true;false;false;true;false;false]]) ]
247  | NOP ⇒
248     [ ([[false;false;false;false;false;false;false;false]]) ]
249  | ORL addrs ⇒
250     match addrs with
251      [ inl addrs ⇒
252         match addrs with
253          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
254             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
255             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
256             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
257             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
258             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
259             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
260          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
261            let b1 ≝
262              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
263               [ DIRECT b1 ⇒ λ_. b1
264               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
265             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
266              [ ACC_A ⇒ λ_.
267                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
268              | DATA b2 ⇒ λ_.
269                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
270              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
271      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
272         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
273          [ BIT_ADDR b1 ⇒ λ_.
274             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
275          | N_BIT_ADDR b1 ⇒ λ_.
276             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
277          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
278  | POP addr ⇒
279     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
280      [ DIRECT b1 ⇒ λ_.
281         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
282      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
283  | PUSH addr ⇒
284     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
285      [ DIRECT b1 ⇒ λ_.
286         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
287      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
288  | RET ⇒
289     [ ([[false;false;true;false;false;false;true;false]]) ]
290  | RETI ⇒
291     [ ([[false;false;true;true;false;false;true;false]]) ]
292  | RL addr ⇒
293     [ ([[false;false;true;false;false;false;true;true]]) ]
294  | RLC addr ⇒
295     [ ([[false;false;true;true;false;false;true;true]]) ]
296  | RR addr ⇒
297     [ ([[false;false;false;false;false;false;true;true]]) ]
298  | RRC addr ⇒
299     [ ([[false;false;false;true;false;false;true;true]]) ]
300  | SETB addr ⇒     
301     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
302      [ CARRY ⇒ λ_.
303         [ ([[true;true;false;true;false;false;true;true]]) ]
304      | BIT_ADDR b1 ⇒ λ_.
305         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
306      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
307  | SUBB addr1 addr2 ⇒
308     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
309      [ REGISTER r ⇒ λ_.
310         [ ([[true;false;false;true;true]]) @@ r ]
311      | DIRECT b1 ⇒ λ_.
312         [ ([[true;false;false;true;false;true;false;true]]); b1]
313      | INDIRECT i1 ⇒ λ_.
314         [ ([[true;false;false;true;false;true;true;i1]]) ]
315      | DATA b1 ⇒ λ_.
316         [ ([[true;false;false;true;false;true;false;false]]); b1]
317      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
318  | SWAP addr ⇒
319     [ ([[true;true;false;false;false;true;false;false]]) ]
320  | XCH addr1 addr2 ⇒
321     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
322      [ REGISTER r ⇒ λ_.
323         [ ([[true;true;false;false;true]]) @@ r ]
324      | DIRECT b1 ⇒ λ_.
325         [ ([[true;true;false;false;false;true;false;true]]); b1]
326      | INDIRECT i1 ⇒ λ_.
327         [ ([[true;true;false;false;false;true;true;i1]]) ]
328      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
329  | XCHD addr1 addr2 ⇒
330     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
331      [ INDIRECT i1 ⇒ λ_.
332         [ ([[true;true;false;true;false;true;true;i1]]) ]
333      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
334  | XRL addrs ⇒
335     match addrs with
336      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
337         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
338          [ REGISTER r ⇒ λ_.
339             [ ([[false;true;true;false;true]]) @@ r ]
340          | DIRECT b1 ⇒ λ_.
341             [ ([[false;true;true;false;false;true;false;true]]); b1]
342          | INDIRECT i1 ⇒ λ_.
343             [ ([[false;true;true;false;false;true;true;i1]]) ]
344          | DATA b1 ⇒ λ_.
345             [ ([[false;true;true;false;false;true;false;false]]); b1]
346          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
347      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
348         let b1 ≝
349          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
350           [ DIRECT b1 ⇒ λ_. b1
351           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
352         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
353          [ ACC_A ⇒ λ_.
354             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
355          | DATA b2 ⇒ λ_.
356             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
357          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
358       ].
359
360definition assembly1 ≝
361 λi: instruction.
362 match i with
363  [ ACALL addr ⇒
364     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
365      [ ADDR11 w ⇒ λ_.
366         let v1_v2 ≝ split ? 3 8 w in
367         let v1 ≝ \fst v1_v2 in
368         let v2 ≝ \snd v1_v2 in
369          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
370      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
371  | AJMP addr ⇒
372     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
373      [ ADDR11 w ⇒ λ_.
374         let v1_v2 ≝ split ? 3 8 w in
375         let v1 ≝ \fst v1_v2 in
376         let v2 ≝ \snd v1_v2 in
377          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
378      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
379  | JMP adptr ⇒
380     [ ([[false;true;true;true;false;false;true;true]]) ]
381  | LCALL addr ⇒
382     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
383      [ ADDR16 w ⇒ λ_.
384         let b1_b2 ≝ split ? 8 8 w in
385         let b1 ≝ \fst b1_b2 in
386         let b2 ≝ \snd b1_b2 in
387          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
388      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
389  | LJMP addr ⇒
390     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
391      [ ADDR16 w ⇒ λ_.
392         let b1_b2 ≝ split ? 8 8 w in
393         let b1 ≝ \fst b1_b2 in
394         let b2 ≝ \snd b1_b2 in
395          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
396      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
397  | MOVC addr1 addr2 ⇒
398     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
399      [ ACC_DPTR ⇒ λ_.
400         [ ([[true;false;false;true;false;false;true;true]]) ]
401      | ACC_PC ⇒ λ_.
402         [ ([[true;false;false;false;false;false;true;true]]) ]
403      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
404  | SJMP addr ⇒
405     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
406      [ RELATIVE b1 ⇒ λ_.
407         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
408      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
409  | RealInstruction instr ⇒
410    assembly_preinstruction [[ relative ]]
411      (λx.
412        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
413        [ RELATIVE r ⇒ λ_. r
414        | _ ⇒ λabsd. ⊥
415        ] (subaddressing_modein … x)) instr
416  ].
417  cases absd
418qed.
419
420(* XXX: pc_plus_sjmp_length used to be just sigma of ppc.  This is incorrect
421        as relative lengths are computed from the *end* of the SJMP, not from
422        the beginning.  This caused a mismatch with Jaap's code which was
423        computing the lengths correctly, and has not been fixed.
424*)
425definition expand_relative_jump_internal:
426 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
427 Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
428 list instruction
429 ≝
430  λlookup_labels.λsigma.λlbl.λppc,i.
431   let lookup_address ≝ sigma (lookup_labels lbl) in
432   let pc_plus_sjmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
433   let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_sjmp_length lookup_address false in
434   let 〈upper, lower〉 ≝ split ? 8 8 result in
435   if eq_bv ? upper (zero 8) then
436     let address ≝ RELATIVE lower in
437       [ RealInstruction (i address) ]
438   else
439    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
440      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
441      LJMP (ADDR16 lookup_address)
442    ].
443  %
444qed.
445
446(*definition rel_jump_length_ok ≝
447 λlookup_address:Word.
448 λpc:Word.
449 Σjump_len:jump_length.
450  (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)
451  ∀(*x,*)y. expand_relative_jump_internal_safe lookup_address jump_len (*x*) pc y ≠ None ?.
452
453lemma eject_rel_jump_length: ∀x,y. rel_jump_length_ok x y → jump_length.
454 #x #y #p @(pi1 … p)
455qed.
456
457coercion eject_rel_jump_length nocomposites:
458 ∀x,y.∀pol:rel_jump_length_ok x y. jump_length ≝
459 eject_rel_jump_length on _pol:(rel_jump_length_ok ??) to jump_length.*)
460
461(*definition expand_relative_jump_internal:
462 ∀lookup_address:Word. ∀pc:Word. ([[relative]] → preinstruction [[relative]]) →
463 list instruction
464≝ λlookup_address,pc,i.
465   match expand_relative_jump_internal_safe lookup_address pc i
466   return λres. res ≠ None ? → ?
467   with
468   [ None ⇒ λabs.⊥
469   | Some res ⇒ λ_.res ] (pi2 … jump_len i).
470 cases abs /2/
471qed.*)
472
473definition expand_relative_jump:
474  ∀lookup_labels.∀sigma.
475  Word → (*jump_length →*)
476  preinstruction Identifier → list instruction ≝
477  λlookup_labels: Identifier → Word.
478  λsigma:Word → Word.
479  λppc: Word.
480  (*λjmp_len: jump_length.*)
481  λi: preinstruction Identifier.
482  (*let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in*)
483  match i with
484  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JC ?)
485  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNC ?)
486  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JB ? baddr)
487  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JZ ?)
488  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNZ ?)
489  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JBC ? baddr)
490  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNB ? baddr)
491  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (CJNE ? addr)
492  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (DJNZ ? addr)
493  | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
494  | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
495  | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ]
496  | INC arg ⇒ [ INC ? arg ]
497  | DEC arg ⇒ [ DEC ? arg ]
498  | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ]
499  | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ]
500  | DA arg ⇒ [ DA ? arg ]
501  | ANL arg ⇒ [ ANL ? arg ]
502  | ORL arg ⇒ [ ORL ? arg ]
503  | XRL arg ⇒ [ XRL ? arg ]
504  | CLR arg ⇒ [ CLR ? arg ]
505  | CPL arg ⇒ [ CPL ? arg ]
506  | RL arg ⇒ [ RL ? arg ]
507  | RR arg ⇒ [ RR ? arg ]
508  | RLC arg ⇒ [ RLC ? arg ]
509  | RRC arg ⇒ [ RRC ? arg ]
510  | SWAP arg ⇒ [ SWAP ? arg ]
511  | MOV arg ⇒ [ MOV ? arg ]
512  | MOVX arg ⇒ [ MOVX ? arg ]
513  | SETB arg ⇒ [ SETB ? arg ]
514  | PUSH arg ⇒ [ PUSH ? arg ]
515  | POP arg ⇒ [ POP ? arg ]
516  | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ]
517  | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ]
518  | RET ⇒ [ RET ? ]
519  | RETI ⇒ [ RETI ? ]
520  | NOP ⇒ [ RealInstruction (NOP ?) ]
521  ].
522
523definition expand_pseudo_instruction:
524    ∀lookup_labels.
525    ∀sigma: Word → Word.
526    ∀policy: Word → bool.
527      Word → ? → pseudo_instruction → list instruction ≝
528  λlookup_labels: Identifier → Word.
529  λsigma: Word → Word.
530  λpolicy: Word → bool.
531  λppc.
532  λlookup_datalabels:Identifier → Word.
533  λi.
534  match i with
535  [ Cost cost ⇒ [ ]
536  | Comment comment ⇒ [ ]
537  | Call call ⇒
538    let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in
539    let pc ≝ sigma ppc in
540    let do_a_long ≝ policy ppc in
541    let 〈pc_5, restp〉 ≝ split ? 5 11 pc in
542    if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then
543      let address ≝ ADDR11 resta in
544        [ ACALL address ]
545    else
546      let address ≝ ADDR16 (sigma (lookup_labels call)) in
547        [ LCALL address ]
548  | Mov d trgt ⇒
549    let address ≝ DATA16 (lookup_datalabels trgt) in
550      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
551  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
552  | Jmp jmp ⇒
553    let pc ≝ sigma ppc in
554    let do_a_long ≝ policy ppc in
555    let lookup_address ≝ sigma (lookup_labels jmp) in
556    let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
557    let 〈upper, lower〉 ≝ split ? 8 8 result in
558    if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then
559      let address ≝ RELATIVE lower in
560        [ SJMP address ]
561    else
562      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) in
563      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
564      if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then
565        let address ≝ ADDR11 rest_addr in
566          [ AJMP address ]
567      else   
568        let address ≝ ADDR16 lookup_address in
569        [ LJMP address ]
570  ].
571  %
572qed.
573
574(*
575(*X?
576definition jump_length_ok ≝
577 λlookup_labels:Identifier → Word.
578 λpc:Word.
579 Σjump_len:jump_length.
580  (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)
581  ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.
582*)
583
584lemma eject_jump_length: ∀x,y. jump_length_ok x y → jump_length.
585 #x #y #p @(pi1 … p)
586qed.
587
588coercion eject_jump_length nocomposites:
589 ∀x,y.∀pol:jump_length_ok x y. jump_length ≝
590 eject_jump_length on _pol:(jump_length_ok ??) to jump_length.
591
592definition expand_pseudo_instruction:
593 ∀lookup_labels:Identifier → Word. ∀pc:Word. jump_length_ok lookup_labels pc →
594 ? → pseudo_instruction → list instruction ≝
595 λlookup_labels,pc,jump_len,lookup_datalabels,i.
596   match expand_pseudo_instruction_safe lookup_labels pc jump_len lookup_datalabels i
597   return λres. res ≠ None ? → ?
598   with
599   [ None ⇒ λabs.⊥
600   | Some res ⇒ λ_.res ] (pi2 … jump_len lookup_datalabels i).
601 cases abs /2/
602qed.
603*)
604(*X?
605definition policy_type ≝
606 λlookup_labels:Identifier → Word.
607 ∀pc:Word. jump_length_ok lookup_labels pc.
608*)
609
610(*definition policy_type2 ≝
611 λprogram.
612  Σpol:Word → jump_length.
613   let lookup_labels ≝
614    (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) in
615   ∀pc:Word. let jump_len ≝ pol pc in
616    ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.*)
617 
618definition assembly_1_pseudoinstruction ≝
619  λlookup_labels.
620  λsigma: Word → Word.
621  λpolicy: Word → bool.
622  λppc: Word.
623  λlookup_datalabels.
624  λi.
625  let pseudos ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels i in
626  let mapped ≝ map ? ? assembly1 pseudos in
627  let flattened ≝ flatten ? mapped in
628  let pc_len ≝ length ? flattened in
629   〈pc_len, flattened〉.
630
631definition instruction_size ≝
632  λlookup_labels.
633  λsigma: Word → Word.
634  λpolicy: Word → bool.
635  λppc.
636  λi.
637    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
638
639(* Jaap: never used
640lemma fetch_pseudo_instruction_prefix:
641  ∀prefix.∀x.∀ppc.ppc < (|prefix|) →
642  fetch_pseudo_instruction prefix (bitvector_of_nat ? ppc) =
643  fetch_pseudo_instruction (prefix@x) (bitvector_of_nat ? ppc).
644 #prefix #x #ppc elim prefix
645 [ #Hppc @⊥ @(absurd … Hppc) @le_to_not_lt @le_O_n
646 | #h #t #Hind #Hppc whd in match (fetch_pseudo_instruction ??);
647   whd in match (fetch_pseudo_instruction ((h::t)@x) ?);
648   >nth_append_first
649   [ //
650   | >nat_of_bitvector_bitvector_of_nat
651     [ @Hppc
652     | cases daemon (* XXX invariant *)
653     ]
654   ]
655 ]
656qed.
657*)
658
659(*
660(* This establishes the correspondence between pseudo program counters and
661   program counters. It is at the heart of the proof. *)
662(*CSC: code taken from build_maps *)
663definition sigma00:
664 ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? →
665 (Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)).
666  let 〈ppc,pc_map〉 ≝ ppc_pc_map in
667  let 〈program_counter, sigma_map〉 ≝ pc_map in
668  ppc = |l| ∧
669  (ppc = |l| →
670   (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧
671   (∀x.x < |l| →
672    ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi →
673   let pc_x ≝ bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in
674   bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) =
675   bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) +
676   (\fst (assembly_1_pseudoinstruction lookup_labels(*X?(λx.pc_x)*) (jump_expansion (*?(λx.pc_x)*)) pc_x
677     (λx.zero ?) pi)))))
678 ) ≝
679 (*?*)λlookup_labels.
680 λjump_expansion(*X?: policy_type2*).
681 λl:list labelled_instruction.
682 λacc.
683  foldl_strong ?
684   (λprefix.(Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)).
685     let 〈ppc,pc_map〉 ≝ ppc_pc_map in
686     let 〈program_counter, sigma_map〉 ≝ pc_map in
687     (ppc = |prefix|) ∧
688     (ppc = |prefix| →
689      (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧
690      (∀x.x < |prefix| →
691       ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi →
692       let pc_x ≝  bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in
693       bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) =
694       bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) +
695       (\fst (assembly_1_pseudoinstruction (*X?(λx.pc_x)*)lookup_labels (jump_expansion (*X?(λx.pc_x)*)) pc_x
696        (λx.zero ?) pi))))))
697    )
698   l
699   (λhd.λi.λtl.λp.λppc_pc_map.
700     let 〈ppc,pc_map〉 ≝ ppc_pc_map in
701     let 〈program_counter, sigma_map〉 ≝ pc_map in
702     let 〈label, i〉 ≝ i in
703      let 〈pc,ignore〉 ≝ construct_costs lookup_labels program_counter (jump_expansion (*X?(λx.bitvector_of_nat ? program_counter)*)) ppc (Stub …) i in
704         〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 (S ppc)) (bitvector_of_nat 16 pc) sigma_map〉〉
705   ) acc.
706cases i in p; #label #ins #p @pair_elim #new_ppc #x normalize nodelta cases x -x #old_pc #old_map
707@pair_elim #new_pc #ignore #Hc #Heq normalize nodelta @conj
708[ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind
709  <(pair_eq1 ?????? Heq) >(proj1 ?? Hind) >append_length <commutative_plus normalize @refl
710| #Hnew <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) @conj
711  [ >lookup_insert_hit >(pair_eq1 ?????? (pair_eq2 ?????? Heq)) @refl
712  | #x <(pair_eq1 ?????? Heq) >append_length <commutative_plus #Hx normalize in Hx;
713    #pi #Hpi <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) in Hnew;
714    >append_length <commutative_plus #Hnew normalize in Hnew; >(injective_S … Hnew)
715    elim (le_to_or_lt_eq … Hx) -Hx #Hx
716    [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind
717      lapply (proj2 ?? ((proj2 ?? Hind) (proj1 ?? Hind)) x (le_S_S_to_le … Hx) pi Hpi)
718      -Hind #Hind >lookup_insert_miss
719      [2: @bitvector_of_nat_abs
720        [3: @lt_to_not_eq @Hx
721        |1: @(transitive_le … Hx)
722        ]
723        cases daemon (* XXX invariant *)
724      ]
725      >lookup_insert_miss
726      [2: @bitvector_of_nat_abs
727        [3: @lt_to_not_eq @(transitive_le … (le_S_S_to_le … Hx)) @le_S @le_n
728        |1: @(transitive_le … (le_S_S_to_le … Hx))
729        ]
730        cases daemon (* XXX invariant *)
731      ]
732      @Hind
733    | lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta
734      #Hind lapply (proj1 ?? ((proj2 ?? Hind) (proj1 ?? Hind))) -Hind
735      >(injective_S … Hnew) #Hind <(injective_S … Hx) >lookup_insert_hit >lookup_insert_miss
736      [2: @bitvector_of_nat_abs
737        [3: @lt_to_not_eq @le_n
738        |1: @(transitive_le ??? (le_n (S x)))
739        ]
740        cases daemon (* XXX invariant *)
741      ]
742      >p in Hpi; whd in match (fetch_pseudo_instruction ??); >nth_append_second
743      >nat_of_bitvector_bitvector_of_nat >(injective_S … Hx)
744      [3: @le_n]
745      [2,3: cases daemon (* XXX invariant *)]
746      <minus_n_n cases (half_add ???) #x #y normalize nodelta -x -y #Heq <Heq
747      whd in match (construct_costs ?????) in Hc; whd in match (assembly_1_pseudoinstruction ?????);
748      cases ins in p Hc; normalize nodelta
749      [1,2,4,5: #x #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat
750        [1,3,5,7: @refl
751        |2,4,6,8: cases daemon (* XXX invariant *)
752        ]
753      |3: #c #p >Hind #H <(pair_eq1 ?????? H) >nat_of_bitvector_bitvector_of_nat
754        [2: cases daemon (* XXX invariant *) ]
755        whd in match (expand_pseudo_instruction ?????); normalize <plus_n_O @refl
756      |6: #x #y #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat
757        [ @refl
758        | cases daemon (* XXX invariant *)
759        ]
760      ]
761    ]
762  ]
763]
764qed.
765
766definition sigma0: pseudo_assembly_program → policy_type2 → (nat × (nat × (BitVectorTrie Word 16))) ≝
767  λprog.
768  λjump_expansion.
769    sigma00 jump_expansion (\snd prog)
770    〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉.
771 normalize nodelta @conj
772 [ / by refl/
773 | #H @conj
774   [ >lookup_insert_hit @refl
775   | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
776   ]
777 ]
778qed.
779
780definition tech_pc_sigma00: pseudo_assembly_program → policy_type2 →
781 list labelled_instruction → (nat × nat) ≝
782 λprogram,jump_expansion,instr_list.
783   let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list
784   〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub ? ?))〉〉 in
785   (* acc copied from sigma0 *)
786   let 〈pc,map〉 ≝ pc_sigma_map in
787     〈ppc,pc〉.
788 normalize nodelta @conj
789 [ / by refl/
790 | #H @conj
791   [ >lookup_insert_hit @refl
792   | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
793   ]
794 ]
795qed.
796
797definition sigma_safe: pseudo_assembly_program → policy_type2 →
798 option (Word → Word) ≝
799 λinstr_list,jump_expansion.
800  let 〈ppc,pc_sigma_map〉 ≝ sigma0 instr_list jump_expansion in
801  let 〈pc, sigma_map〉 ≝ pc_sigma_map in
802    if gtb pc (2^16) then
803      None ?
804    else
805      Some ? (λx. lookup … x sigma_map (zero …)). *)
806
807(* stuff about policy *)
808
809(*definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….*)
810
811(*definition policy ≝ λp. Σjump_expansion:policy_type2. policy_ok jump_expansion p.*)
812
813(*lemma eject_policy: ∀p. policy p → policy_type2.
814 #p #pol @(pi1 … pol)
815qed.
816
817coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type2 ≝ eject_policy on _pol:(policy ?) to policy_type2.
818
819definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
820 λp,policy.
821  match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
822   [ None ⇒ λabs. ⊥
823   | Some r ⇒ λ_.r] (pi2 … policy).
824 cases abs /2 by /
825qed.*)
826
827(*CSC: Main axiom here, needs to be proved soon! *)
828(*lemma snd_assembly_1_pseudoinstruction_ok:
829 ∀program:pseudo_assembly_program.∀pol: policy program.
830 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
831  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
832  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
833  (nat_of_bitvector 16 ppc) < |\snd program| →
834  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
835   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
836    sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =
837     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
838 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl #Hppc
839 lapply (refl … (sigma0 program pol)) whd in match (sigma0 ??) in ⊢ (??%? → ?);
840 cases (sigma00 ???) #x #Hpmap #EQ
841 whd in match (sigma ???);
842 whd in match (sigma program pol (add ???));
843 whd in match sigma_safe; normalize nodelta
844 (*Problem1: backtracking cases (sigma0 program pol)*)
845 generalize in match (pi2 ???); whd in match policy_ok; normalize nodelta
846 whd in match sigma_safe; normalize nodelta <EQ cases x in Hpmap EQ; -x #final_ppc #x
847 cases x -x #final_pc #smap normalize nodelta #Hpmap #EQ #Heq #Hfetch cases (gtb final_pc (2^16)) in Heq;
848 normalize nodelta
849 [ #abs @⊥ @(absurd ?? abs) @refl
850 | #_ lapply (proj1 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) #Hpmap1
851   lapply ((proj2 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) (nat_of_bitvector 16 ppc) Hppc) #Hpmap2 -Hpmap
852   <(bitvector_of_nat_nat_of_bitvector 16 ppc) >add_SO
853   
854   >(Hpmap2 ? (refl …)) @eq_f @eq_f2 [%]
855   >bitvector_of_nat_nat_of_bitvector
856   >Hfetch lapply Hfetch lapply pi
857
858   
859   whd in match assembly_1_pseudoinstruction; normalize nodelta
860 
861qed.*)
862
863
864(*example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
865 cases daemon.
866qed.*)
867
868(*CSC: FALSE!!!*)
869axiom fetch_pseudo_instruction_split:
870 ∀instr_list,ppc.
871  ∃pre,suff,lbl.
872   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
873
874(*lemma sigma00_append:
875 ∀jump_expansion,l1,l2.
876 ∀acc:ℕ×ℕ×(BitVectorTrie Word 16).
877  sigma00 jump_expansion (l1@l2) acc =
878  sigma00 jump_expansion
879    l2 (pi1 ?? (sigma00 jump_expansion l1 acc)).*)
880
881(* lemma sigma00_strict:
882 ∀jump_expansion,l,acc. acc = None ? →
883  sigma00 jump_expansion l acc = None ….
884 #jump_expansion #l elim l
885  [ #acc #H >H %
886  | #hd #tl #IH #acc #H >H change with (sigma00 ? tl ? = ?) @IH % ]
887qed.
888
889lemma policy_ok_prefix_ok:
890 ∀program.∀pol:policy program.∀suffix,prefix.
891  prefix@suffix = \snd program →
892   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
893 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
894 generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol
895 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
896 normalize nodelta >sigma00_append
897 cases (sigma00 ?? prefix ?)
898  [2: #x #_ % #abs destruct(abs)
899  | * #abs @⊥ @abs >sigma00_strict % ]
900qed.
901
902lemma policy_ok_prefix_hd_ok:
903 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
904  (prefix@[hd])@suffix = \snd program →
905   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
906    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
907    let 〈program_counter, sigma_map〉 ≝ pc_map in
908    let 〈label, i〉 ≝ hd in
909     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
910 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
911 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
912  (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
913 @pair_elim #ppc #pc_map #EQ3 normalize nodelta
914 @pair_elim #pc #map #EQ4 normalize nodelta
915 @pair_elim #l' #i' #EQ5 normalize nodelta
916 cases (construct_costs_safe ??????) normalize
917  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
918qed. *)
919
920(* JPB,CSC: this definition is now replaced by the expand_pseudo_instruction higher up
921definition expand_pseudo_instruction:
922 ∀program:pseudo_assembly_program.∀pol: policy program.
923  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
924  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
925  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
926  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
927  pc = sigma program pol ppc →
928  Σres:list instruction. Some … res = expand_pseudo_instruction_safe pc (lookup_labels pi) lookup_datalabels (pol ppc) pi
929≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
930   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
931    [ None ⇒ let dummy ≝ [ ] in dummy
932    | Some res ⇒ res ].
933 [ @⊥ whd in p:(??%??);
934   generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);
935   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
936   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
937   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
938   #res #K
939   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
940   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
941   cases daemon (* CSC: XXXXXXXX Ero qui
942   
943    [3: @policy_ok_prefix_ok ]
944    | sigma00 program pol pre
945
946
947
948   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
949   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
950   per concludere construct_costs_safe ≠ None *)
951 | >p %]
952qed. *)
953
954(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
955(* definition assembly_1_pseudoinstruction':
956 ∀program:pseudo_assembly_program.∀pol: policy program.
957  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
958  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
959  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
960  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
961  Σres:(nat × (list Byte)).
962   res = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
963   let 〈len,code〉 ≝ res in
964    sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =
965     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
966≝ λprogram: pseudo_assembly_program.
967  λpol: policy program.
968  λppc: Word.
969  λlookup_labels.
970  λlookup_datalabels.
971  λpi.
972  λprf1,prf2,prf3.
973   assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
974 [ @⊥ elim pi in p; [*]
975   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
976   generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
977   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
978   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
979   cases daemon
980 | % [ >p %]
981   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
982   (* THIS SHOULD BE TRUE INSTEAD *)
983   cases daemon]
984qed.
985
986definition assembly_1_pseudoinstruction:
987 ∀program:pseudo_assembly_program.∀pol: policy program.
988  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
989  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
990  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
991  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
992   nat × (list Byte)
993≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
994   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
995    prf2 prf3.
996
997lemma assembly_1_pseudoinstruction_ok1:
998 ∀program:pseudo_assembly_program.∀pol: policy program.
999  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1000  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
1001  ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
1002  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
1003     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
1004   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
1005 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
1006 cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
1007 #H1 #_ @H1
1008qed. *)
1009
1010(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1011(* definition construct_costs':
1012 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
1013  Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
1014
1015  λprogram.λpol: policy program.λppc,pc,costs,i.
1016   match construct_costs_safe program pol ppc pc costs i with
1017    [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
1018    | Some res ⇒ res ].
1019 [ cases daemon
1020 | >p %]
1021qed.
1022
1023definition construct_costs ≝
1024 λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i). *)
1025
1026(*
1027axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
1028axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
1029
1030axiom foldl_strong_step:
1031 ∀A:Type[0].
1032  ∀P: list A → Type[0].
1033   ∀l: list A.
1034    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
1035     ∀acc: P [ ].
1036      ∀Q: ∀prefix. P prefix → Prop.
1037       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
1038        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
1039       Q [ ] acc →
1040        Q l (foldl_strong A P l H acc).
1041(*
1042 #A #P #l #H #acc #Q #HQ #Hacc normalize;
1043 generalize in match
1044  (foldl_strong ?
1045   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
1046   l ? Hacc)
1047 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
1048 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
1049 #K
1050
1051 generalize in match
1052  (foldl_strong ?
1053   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
1054 [2: @H
1055*)
1056
1057axiom foldl_elim:
1058 ∀A:Type[0].
1059  ∀B: Type[0].
1060   ∀H: A → B → A.
1061    ∀acc: A.
1062     ∀l: list B.
1063      ∀Q: A → Prop.
1064       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
1065         Q acc →
1066          Q (foldl A B H acc l).
1067*)
1068
1069(*
1070lemma tech_pc_sigma00_append_Some:
1071 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1072  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1073   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1074 #program #pol #prefix #costs #label #i #ppc #pc #H
1075  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
1076  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
1077  generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
1078  whd in match sigma0; normalize nodelta;
1079  >foldl_step
1080  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
1081  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
1082  cases (sigma00 program pol prefix) in H ⊢ %
1083   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
1084   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
1085     
1086     normalize nodelta; -H;
1087     
1088 
1089   generalize in match H; -H;
1090  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
1091   [2: whd in ⊢ (??%%)
1092XXX
1093*)
1094
1095(* axiom construct_costs_sigma:
1096 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
1097  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
1098   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
1099
1100axiom tech_pc_sigma00_append_Some:
1101 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1102  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1103   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. *)
1104
1105axiom eq_identifier_eq:
1106  ∀tag: String.
1107  ∀l.
1108  ∀r.
1109    eq_identifier tag l r = true → l = r.
1110
1111axiom neq_identifier_neq:
1112  ∀tag: String.
1113  ∀l, r: identifier tag.
1114    eq_identifier tag l r = false → (l = r → False).
1115
1116(* label_map: identifier ↦ pseudo program counter *)
1117definition label_map ≝ identifier_map ASMTag ℕ.
1118
1119(* Labels *)
1120definition is_label ≝
1121  λx:labelled_instruction.λl:Identifier.
1122  let 〈lbl,instr〉 ≝ x in
1123  match lbl with
1124  [ Some l' ⇒ l' = l
1125  | _       ⇒ False
1126  ].
1127
1128lemma label_does_not_occur:
1129  ∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier.
1130  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false.
1131 #i #p #l generalize in match i; elim p
1132 [ #i >nth_nil #H cases H
1133 | #h #t #IH #i cases i -i
1134   [ cases h #hi #hp cases hi
1135     [ normalize #H cases H
1136     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????);
1137       whd in Heq; >Heq
1138       >eq_identifier_refl / by refl/
1139     ]
1140   | #i #H whd in match (does_not_occur ????);
1141     whd in match (instruction_matches_identifier ????);
1142     cases h #hi #hp cases hi normalize nodelta
1143     [ @(IH i) @H
1144     | #l' @eq_identifier_elim
1145       [ normalize / by /
1146       | normalize #_ @(IH i) @H
1147       ]
1148     ]
1149   ]
1150 ]
1151qed.
1152
1153(* The function that creates the label-to-address map *)
1154definition create_label_cost_map0: ∀program:list labelled_instruction.
1155  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
1156    let 〈labels,costs〉 ≝ labels_costs in
1157    ∀l.occurs_exactly_once ?? l program →
1158    bitvector_of_nat ? (lookup_def ?? labels l 0) =
1159     address_of_word_labels_code_mem program l
1160  ) ≝
1161  λprogram.
1162  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
1163  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
1164    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
1165    ppc = |prefix| ∧
1166    ∀l.occurs_exactly_once ?? l prefix →
1167    bitvector_of_nat ? (lookup_def ?? labels l 0) =
1168     address_of_word_labels_code_mem prefix l)
1169  program
1170  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
1171   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
1172   let 〈label,instr〉 ≝ x in
1173   let labels ≝
1174     match label with
1175     [ None   ⇒ labels
1176     | Some l ⇒ add … labels l ppc
1177     ] in
1178   let costs ≝
1179     match instr with
1180     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
1181     | _ ⇒ costs ] in
1182      〈labels,costs,S ppc〉
1183   ) 〈(empty_map …),(Stub ??),0〉)).
1184[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2
1185  -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
1186 inversion label [#EQ | #l #EQ]
1187 [ #lbl #Hocc <address_of_word_labels_code_mem_None [2: @Hocc] normalize nodelta
1188   >occurs_exactly_once_None in Hocc; @(IH2 lbl)
1189 | #lbl normalize nodelta inversion (eq_identifier ? lbl l)
1190   [ #Heq #Hocc >(eq_identifier_eq … Heq)
1191     >address_of_word_labels_code_mem_Some_hit
1192     [ >IH1 >lookup_def_add_hit %
1193     | <(eq_identifier_eq … Heq) in Hocc; //
1194     ]
1195   | #Hneq #Hocc
1196     <address_of_word_labels_code_mem_Some_miss
1197     [ >lookup_def_add_miss
1198       [ @IH2 >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym> Hneq //
1199       | % @neq_identifier_neq @Hneq
1200       ]
1201     | @Hocc
1202     | >eq_identifier_sym @Hneq
1203     ]
1204   ]
1205 ]
1206| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
1207  #l #abs cases (abs)
1208| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
1209  #_ #H @H
1210]
1211qed.
1212
1213(* The function that creates the label-to-address map *)
1214definition create_label_cost_map: ∀program:list labelled_instruction.
1215  label_map × (BitVectorTrie costlabel 16) ≝
1216    λprogram.
1217      pi1 … (create_label_cost_map0 program).
1218
1219theorem create_label_cost_map_ok:
1220 ∀pseudo_program: pseudo_assembly_program.
1221   let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in
1222    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
1223     bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id.
1224 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2
1225qed.
1226 
1227definition assembly:
1228    ∀p: pseudo_assembly_program.
1229    ∀sigma: Word → Word.
1230    ∀policy: Word → bool.
1231      list Byte × (BitVectorTrie costlabel 16) ≝
1232  λp.
1233  λsigma.
1234  λpolicy.
1235  let 〈preamble, instr_list〉 ≝ p in
1236  let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
1237  let datalabels ≝ construct_datalabels preamble in
1238  let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
1239  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
1240  let result ≝
1241     pi1 ?? (foldl_strong
1242      (option Identifier × pseudo_instruction)
1243      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
1244        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
1245        let 〈ppc,code〉 ≝ ppc_code in
1246         ∀ppc'.
1247          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
1248          let 〈len,assembledi〉 ≝
1249           assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
1250           True)
1251      instr_list
1252      (λprefix,hd,tl,prf,pc_ppc_code.
1253        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
1254        let 〈ppc, code〉 ≝ ppc_code in
1255        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (\snd hd) in
1256        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
1257        let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in
1258         〈new_pc, 〈new_ppc, (code @ program)〉〉)
1259      〈(zero ?), 〈(zero ?), [ ]〉〉)
1260    in
1261     〈\snd (\snd result),
1262      fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
1263  @pair_elim normalize nodelta #x #y #z
1264  @pair_elim normalize nodelta #w1 #w2 #w3 #w4
1265  @pair_elim //
1266qed.
1267
1268definition assembly_unlabelled_program:
1269    assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
1270  λp.
1271    Some … (〈foldr … (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.