source: src/ASM/Assembly.ma @ 2108

Last change on this file since 2108 was 2108, checked in by mulligan, 7 years ago

Various axioms closed and others moved around. Uncommented main lemma and found that it no longer compiles due to changing how we expand jumps. Problem in proof highlighted with XXX for Claudio.

File size: 44.2 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  | absolute_jump: jump_length
15  | long_jump: jump_length.
16 
17(* Functions that define the conditions under which jumps are possible *)
18definition short_jump_cond: Word → Word → (*pseudo_instruction →*)
19  bool × (BitVector 8) ≝
20  λpc_plus_jmp_length.λaddr.(*λinstr.*)
21  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
22  let 〈upper, lower〉 ≝ vsplit ? 9 7 result in
23    if get_index' ? 2 0 flags then
24      〈eq_bv 9 upper [[true;true;true;true;true;true;true;true;true]], true:::lower〉
25    else
26      〈eq_bv 9 upper (zero …), false:::lower〉.
27 
28definition absolute_jump_cond: Word → Word → (*pseudo_instruction →*)
29  bool × (BitVector 11) ≝
30  λpc_plus_jmp_length.λaddr.(*λinstr.*)
31  let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in
32  let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in
33  〈eq_bv 5 fst_5_addr fst_5_pc, rest_addr〉.
34
35definition assembly_preinstruction ≝
36  λA: Type[0].
37  λaddr_of: A → Byte. (* relative *)
38  λpre: preinstruction A.
39  match pre with
40  [ ADD addr1 addr2 ⇒
41     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
42      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
43      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
44      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
45      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
46      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
47  | ADDC addr1 addr2 ⇒
48     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
49      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
50      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
51      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
52      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
53      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
54  | ANL addrs ⇒
55     match addrs with
56      [ inl addrs ⇒ match addrs with
57         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
58           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
59            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
60            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
61            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
62            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
63            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
64         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
65            let b1 ≝
66             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
67              [ DIRECT b1 ⇒ λ_.b1
68              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
69            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
70             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
71             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
72             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
73         ]
74      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
75         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
76          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
77          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
78          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
79  | CLR addr ⇒
80     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
81      [ ACC_A ⇒ λ_.
82         [ ([[true; true; true; false; false; true; false; false]]) ]
83      | CARRY ⇒ λ_.
84         [ ([[true; true; false; false; false; false; true; true]]) ]
85      | BIT_ADDR b1 ⇒ λ_.
86         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
87      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
88  | CPL addr ⇒
89     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
90      [ ACC_A ⇒ λ_.
91         [ ([[true; true; true; true; false; true; false; false]]) ]
92      | CARRY ⇒ λ_.
93         [ ([[true; false; true; true; false; false; true; true]]) ]
94      | BIT_ADDR b1 ⇒ λ_.
95         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
96      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
97  | DA addr ⇒
98     [ ([[true; true; false; true; false; true; false; false]]) ]
99  | DEC addr ⇒
100     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
101      [ ACC_A ⇒ λ_.
102         [ ([[false; false; false; true; false; true; false; false]]) ]
103      | REGISTER r ⇒ λ_.
104         [ ([[false; false; false; true; true]]) @@ r ]
105      | DIRECT b1 ⇒ λ_.
106         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
107      | INDIRECT i1 ⇒ λ_.
108         [ ([[false; false; false; true; false; true; true; i1]]) ]
109      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
110      | DJNZ addr1 addr2 ⇒
111         let b2 ≝ addr_of addr2 in
112         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
113          [ REGISTER r ⇒ λ_.
114             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
115          | DIRECT b1 ⇒ λ_.
116             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
117          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
118      | JC addr ⇒
119        let b1 ≝ addr_of addr in
120          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
121      | JNC addr ⇒
122         let b1 ≝ addr_of addr in
123           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
124      | JZ addr ⇒
125         let b1 ≝ addr_of addr in
126           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
127      | JNZ addr ⇒
128         let b1 ≝ addr_of addr in
129           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
130      | JB addr1 addr2 ⇒
131         let b2 ≝ addr_of addr2 in
132         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
133          [ BIT_ADDR b1 ⇒ λ_.
134             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
135          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
136      | JNB addr1 addr2 ⇒
137         let b2 ≝ addr_of addr2 in
138         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
139          [ BIT_ADDR b1 ⇒ λ_.
140             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
141          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
142      | JBC addr1 addr2 ⇒
143         let b2 ≝ addr_of addr2 in
144         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
145          [ BIT_ADDR b1 ⇒ λ_.
146             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
147          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
148      | CJNE addrs addr3 ⇒
149         let b3 ≝ addr_of addr3 in
150         match addrs with
151          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
152             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
153              [ DIRECT b1 ⇒ λ_.
154                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
155              | DATA b1 ⇒ λ_.
156                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
157              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
158          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
159             let b2 ≝
160              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
161               [ DATA b2 ⇒ λ_. b2
162               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
163             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
164              [ REGISTER r ⇒ λ_.
165                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
166              | INDIRECT i1 ⇒ λ_.
167                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
168              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
169         ]
170  | DIV addr1 addr2 ⇒
171     [ ([[true;false;false;false;false;true;false;false]]) ]
172  | INC addr ⇒
173     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
174      [ ACC_A ⇒ λ_.
175         [ ([[false;false;false;false;false;true;false;false]]) ]         
176      | REGISTER r ⇒ λ_.
177         [ ([[false;false;false;false;true]]) @@ r ]
178      | DIRECT b1 ⇒ λ_.
179         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
180      | INDIRECT i1 ⇒ λ_.
181        [ ([[false; false; false; false; false; true; true; i1]]) ]
182      | DPTR ⇒ λ_.
183        [ ([[true;false;true;false;false;false;true;true]]) ]
184      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
185  | MOV addrs ⇒
186     match addrs with
187      [ inl addrs ⇒
188         match addrs with
189          [ inl addrs ⇒
190             match addrs with
191              [ inl addrs ⇒
192                 match addrs with
193                  [ inl addrs ⇒
194                     match addrs with
195                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
196                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
197                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
198                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
199                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
200                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
201                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
202                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
203                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
204                          [ REGISTER r ⇒ λ_.
205                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
206                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
207                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
208                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
209                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
210                          | INDIRECT i1 ⇒ λ_.
211                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
212                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
213                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
214                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
215                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
216                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
217                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
218                     let b1 ≝
219                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
220                       [ DIRECT b1 ⇒ λ_. b1
221                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
222                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
223                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
224                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
225                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
226                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
227                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
228                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
229              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
230                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
231                  [ DATA16 w ⇒ λ_.
232                     let b1_b2 ≝ vsplit ? 8 8 w in
233                     let b1 ≝ \fst b1_b2 in
234                     let b2 ≝ \snd b1_b2 in
235                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
236                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
237          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
238             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
239              [ BIT_ADDR b1 ⇒ λ_.
240                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
241              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
242      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
243         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
244          [ BIT_ADDR b1 ⇒ λ_.
245             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
246          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
247  | MOVX addrs ⇒
248     match addrs with
249      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
250         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
251          [ EXT_INDIRECT i1 ⇒ λ_.
252             [ ([[true;true;true;false;false;false;true;i1]]) ]
253          | EXT_INDIRECT_DPTR ⇒ λ_.
254             [ ([[true;true;true;false;false;false;false;false]]) ]
255          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
256      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
257         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
258          [ EXT_INDIRECT i1 ⇒ λ_.
259             [ ([[true;true;true;true;false;false;true;i1]]) ]
260          | EXT_INDIRECT_DPTR ⇒ λ_.
261             [ ([[true;true;true;true;false;false;false;false]]) ]
262          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
263  | MUL addr1 addr2 ⇒
264     [ ([[true;false;true;false;false;true;false;false]]) ]
265  | NOP ⇒
266     [ ([[false;false;false;false;false;false;false;false]]) ]
267  | ORL addrs ⇒
268     match addrs with
269      [ inl addrs ⇒
270         match addrs with
271          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
272             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
273             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
274             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
275             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
276             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
277             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
278          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
279            let b1 ≝
280              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
281               [ DIRECT b1 ⇒ λ_. b1
282               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
283             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
284              [ ACC_A ⇒ λ_.
285                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
286              | DATA b2 ⇒ λ_.
287                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
288              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
289      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
290         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
291          [ BIT_ADDR b1 ⇒ λ_.
292             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
293          | N_BIT_ADDR b1 ⇒ λ_.
294             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
295          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
296  | POP addr ⇒
297     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
298      [ DIRECT b1 ⇒ λ_.
299         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
300      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
301  | PUSH addr ⇒
302     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
303      [ DIRECT b1 ⇒ λ_.
304         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
305      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
306  | RET ⇒
307     [ ([[false;false;true;false;false;false;true;false]]) ]
308  | RETI ⇒
309     [ ([[false;false;true;true;false;false;true;false]]) ]
310  | RL addr ⇒
311     [ ([[false;false;true;false;false;false;true;true]]) ]
312  | RLC addr ⇒
313     [ ([[false;false;true;true;false;false;true;true]]) ]
314  | RR addr ⇒
315     [ ([[false;false;false;false;false;false;true;true]]) ]
316  | RRC addr ⇒
317     [ ([[false;false;false;true;false;false;true;true]]) ]
318  | SETB addr ⇒     
319     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
320      [ CARRY ⇒ λ_.
321         [ ([[true;true;false;true;false;false;true;true]]) ]
322      | BIT_ADDR b1 ⇒ λ_.
323         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
324      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
325  | SUBB addr1 addr2 ⇒
326     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
327      [ REGISTER r ⇒ λ_.
328         [ ([[true;false;false;true;true]]) @@ r ]
329      | DIRECT b1 ⇒ λ_.
330         [ ([[true;false;false;true;false;true;false;true]]); b1]
331      | INDIRECT i1 ⇒ λ_.
332         [ ([[true;false;false;true;false;true;true;i1]]) ]
333      | DATA b1 ⇒ λ_.
334         [ ([[true;false;false;true;false;true;false;false]]); b1]
335      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
336  | SWAP addr ⇒
337     [ ([[true;true;false;false;false;true;false;false]]) ]
338  | XCH addr1 addr2 ⇒
339     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
340      [ REGISTER r ⇒ λ_.
341         [ ([[true;true;false;false;true]]) @@ r ]
342      | DIRECT b1 ⇒ λ_.
343         [ ([[true;true;false;false;false;true;false;true]]); b1]
344      | INDIRECT i1 ⇒ λ_.
345         [ ([[true;true;false;false;false;true;true;i1]]) ]
346      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
347  | XCHD addr1 addr2 ⇒
348     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
349      [ INDIRECT i1 ⇒ λ_.
350         [ ([[true;true;false;true;false;true;true;i1]]) ]
351      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
352  | XRL addrs ⇒
353     match addrs with
354      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
355         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
356          [ REGISTER r ⇒ λ_.
357             [ ([[false;true;true;false;true]]) @@ r ]
358          | DIRECT b1 ⇒ λ_.
359             [ ([[false;true;true;false;false;true;false;true]]); b1]
360          | INDIRECT i1 ⇒ λ_.
361             [ ([[false;true;true;false;false;true;true;i1]]) ]
362          | DATA b1 ⇒ λ_.
363             [ ([[false;true;true;false;false;true;false;false]]); b1]
364          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
365      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
366         let b1 ≝
367          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
368           [ DIRECT b1 ⇒ λ_. b1
369           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
370         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
371          [ ACC_A ⇒ λ_.
372             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
373          | DATA b2 ⇒ λ_.
374             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
375          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
376       ].
377
378definition assembly1 ≝
379 λi: instruction.
380 match i with
381  [ ACALL addr ⇒
382     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
383      [ ADDR11 w ⇒ λ_.
384         let v1_v2 ≝ vsplit ? 3 8 w in
385         let v1 ≝ \fst v1_v2 in
386         let v2 ≝ \snd v1_v2 in
387          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
388      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
389  | AJMP addr ⇒
390     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
391      [ ADDR11 w ⇒ λ_.
392         let v1_v2 ≝ vsplit ? 3 8 w in
393         let v1 ≝ \fst v1_v2 in
394         let v2 ≝ \snd v1_v2 in
395          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
396      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
397  | JMP adptr ⇒
398     [ ([[false;true;true;true;false;false;true;true]]) ]
399  | LCALL addr ⇒
400     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
401      [ ADDR16 w ⇒ λ_.
402         let b1_b2 ≝ vsplit ? 8 8 w in
403         let b1 ≝ \fst b1_b2 in
404         let b2 ≝ \snd b1_b2 in
405          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
406      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
407  | LJMP addr ⇒
408     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
409      [ ADDR16 w ⇒ λ_.
410         let b1_b2 ≝ vsplit ? 8 8 w in
411         let b1 ≝ \fst b1_b2 in
412         let b2 ≝ \snd b1_b2 in
413          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
414      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
415  | MOVC addr1 addr2 ⇒
416     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
417      [ ACC_DPTR ⇒ λ_.
418         [ ([[true;false;false;true;false;false;true;true]]) ]
419      | ACC_PC ⇒ λ_.
420         [ ([[true;false;false;false;false;false;true;true]]) ]
421      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
422  | SJMP addr ⇒
423     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
424      [ RELATIVE b1 ⇒ λ_.
425         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
426      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
427  | RealInstruction instr ⇒
428    assembly_preinstruction [[ relative ]]
429      (λx.
430        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
431        [ RELATIVE r ⇒ λ_. r
432        | _ ⇒ λabsd. ⊥
433        ] (subaddressing_modein … x)) instr
434  ].
435  cases absd
436qed.
437
438(* XXX: pc_plus_sjmp_length used to be just sigma of ppc.  This is incorrect
439        as relative lengths are computed from the *end* of the SJMP, not from
440        the beginning.
441*)
442definition expand_relative_jump_internal:
443 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
444 Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
445 list instruction
446 ≝
447  λlookup_labels.λsigma.λlbl.λppc,i.
448   let lookup_address ≝ sigma (lookup_labels lbl) in
449   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
450   let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
451   if sj_possible
452   then
453     let address ≝ RELATIVE disp in
454       [ RealInstruction (i address) ]
455   else
456    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
457      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
458      LJMP (ADDR16 lookup_address)
459    ].
460  %
461qed.
462
463definition expand_relative_jump:
464  ∀lookup_labels.∀sigma.
465  Word → (*jump_length →*)
466  preinstruction Identifier → list instruction ≝
467  λlookup_labels: Identifier → Word.
468  λsigma:Word → Word.
469  λppc: Word.
470  (*λjmp_len: jump_length.*)
471  λi: preinstruction Identifier.
472  (*let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in*)
473  match i with
474  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JC ?)
475  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNC ?)
476  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JB ? baddr)
477  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JZ ?)
478  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNZ ?)
479  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JBC ? baddr)
480  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNB ? baddr)
481  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (CJNE ? addr)
482  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (DJNZ ? addr)
483  | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
484  | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
485  | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ]
486  | INC arg ⇒ [ INC ? arg ]
487  | DEC arg ⇒ [ DEC ? arg ]
488  | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ]
489  | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ]
490  | DA arg ⇒ [ DA ? arg ]
491  | ANL arg ⇒ [ ANL ? arg ]
492  | ORL arg ⇒ [ ORL ? arg ]
493  | XRL arg ⇒ [ XRL ? arg ]
494  | CLR arg ⇒ [ CLR ? arg ]
495  | CPL arg ⇒ [ CPL ? arg ]
496  | RL arg ⇒ [ RL ? arg ]
497  | RR arg ⇒ [ RR ? arg ]
498  | RLC arg ⇒ [ RLC ? arg ]
499  | RRC arg ⇒ [ RRC ? arg ]
500  | SWAP arg ⇒ [ SWAP ? arg ]
501  | MOV arg ⇒ [ MOV ? arg ]
502  | MOVX arg ⇒ [ MOVX ? arg ]
503  | SETB arg ⇒ [ SETB ? arg ]
504  | PUSH arg ⇒ [ PUSH ? arg ]
505  | POP arg ⇒ [ POP ? arg ]
506  | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ]
507  | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ]
508  | RET ⇒ [ RET ? ]
509  | RETI ⇒ [ RETI ? ]
510  | NOP ⇒ [ RealInstruction (NOP ?) ]
511  ].
512
513definition expand_pseudo_instruction:
514    ∀lookup_labels.
515    ∀sigma: Word → Word.
516    ∀policy: Word → bool.
517      Word → ? → pseudo_instruction → list instruction ≝
518  λlookup_labels: Identifier → Word.
519  λsigma: Word → Word.
520  λpolicy: Word → bool.
521  λppc.
522  λlookup_datalabels:Identifier → Word.
523  λi.
524  match i with
525  [ Cost cost ⇒ [ ]
526  | Comment comment ⇒ [ ]
527  | Call call ⇒
528    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
529    let lookup_address ≝ sigma (lookup_labels call) in
530    let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
531    let do_a_long ≝ policy ppc in
532    if mj_possible ∧ ¬ do_a_long then
533      let address ≝ ADDR11 disp in
534        [ ACALL address ]
535    else
536      let address ≝ ADDR16 lookup_address in
537        [ LCALL address ]
538  | Mov d trgt ⇒
539    let address ≝ DATA16 (lookup_datalabels trgt) in
540      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
541  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
542  | Jmp jmp ⇒
543    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
544    let do_a_long ≝ policy ppc in
545    let lookup_address ≝ sigma (lookup_labels jmp) in
546    let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
547    if sj_possible ∧ ¬ do_a_long then
548      let address ≝ RELATIVE disp in
549        [ SJMP address ]
550    else
551      let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
552      if mj_possible ∧ ¬ do_a_long then
553        let address ≝ ADDR11 disp2 in
554          [ AJMP address ]
555      else   
556        let address ≝ ADDR16 lookup_address in
557        [ LJMP address ]
558  ].
559  %
560qed.
561 
562definition assembly_1_pseudoinstruction ≝
563  λlookup_labels.
564  λsigma: Word → Word.
565  λpolicy: Word → bool.
566  λppc: Word.
567  λlookup_datalabels.
568  λi.
569  let pseudos ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels i in
570  let mapped ≝ map ? ? assembly1 pseudos in
571  let flattened ≝ flatten ? mapped in
572  let pc_len ≝ length ? flattened in
573   〈pc_len, flattened〉.
574
575definition instruction_size ≝
576  λlookup_labels.
577  λsigma: Word → Word.
578  λpolicy: Word → bool.
579  λppc.
580  λi.
581    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
582
583(*CSC: move elsewhere *)
584lemma nth_safe_append:
585 ∀A,l,n,n_ok.
586  ∃pre,suff.
587   (pre @ [nth_safe A n l n_ok]) @ suff = l.
588#A #l elim l normalize
589 [ #n #abs cases (absurd ? abs (not_le_Sn_O ?))
590 | #hd #tl #IH #n cases n normalize
591   [ #_ %{[]} /2/
592   | #m #m_ok cases (IH m ?)
593     [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); % | skip ]]
594qed.
595
596lemma fetch_pseudo_instruction_vsplit:
597 ∀instr_list,ppc,ppc_ok.
598  ∃pre,suff,lbl.
599   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
600#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
601cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
602lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
603#EQ %{lbl0} @EQ
604qed.
605
606axiom eqb_succ_injective_Pos:
607  ∀l, r: Pos.
608    eqb (succ l) (succ r) = true → eqb l r = true.
609
610lemma eqb_true_to_refl_Pos:
611  ∀l, r: Pos.
612    eqb l r = true → l = r.
613  #l #r @(pos_elim2 … l r)
614  [1:
615    #r cases r
616    [1:
617      #_ %
618    |2,3:
619      #l normalize in ⊢ (% → ?); #absurd destruct(absurd)
620    ]
621  |2:
622    #l cases l
623    [1:
624      normalize in ⊢ (% → ?); #absurd destruct(absurd)
625    |2,3:
626      #l' normalize in ⊢ (% → ?); #absurd destruct(absurd)
627    ]
628  |3:
629    #l #r #inductive_hypothesis #relevant @eq_f
630    @inductive_hypothesis @eqb_succ_injective_Pos
631    assumption
632  ]
633qed.
634
635lemma eq_identifier_eq:
636  ∀tag: String.
637  ∀l.
638  ∀r.
639    eq_identifier tag l r = true → l = r.
640  #tag #l #r cases l cases r
641  #pos_l #pos_r
642  cases pos_l cases pos_r
643  [1:
644    #_ %
645  |2,3,4,7:
646    #p1_l normalize in ⊢ (% → ?);
647    #absurd destruct(absurd)
648  |5,9:
649    #p1_l #p1_r normalize in ⊢ (% → ?);
650    #relevant
651    >(eqb_true_to_refl_Pos … relevant) %
652  |*:
653    #p_l #p_r normalize in ⊢ (% → ?);
654    #absurd destruct(absurd)
655  ]
656qed.
657
658axiom neq_identifier_neq:
659  ∀tag: String.
660  ∀l, r: identifier tag.
661    eq_identifier tag l r = false → (l = r → False).
662 
663(* label_map: identifier ↦ pseudo program counter *)
664definition label_map ≝ identifier_map ASMTag ℕ.
665
666(* Labels *)
667definition is_label ≝
668  λx:labelled_instruction.λl:Identifier.
669  let 〈lbl,instr〉 ≝ x in
670  match lbl with
671  [ Some l' ⇒ l' = l
672  | _       ⇒ False
673  ].
674
675lemma label_does_not_occur:
676  ∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier.
677  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false.
678 #i #p #l generalize in match i; elim p
679 [ #i >nth_nil #H cases H
680 | #h #t #IH #i cases i -i
681   [ cases h #hi #hp cases hi
682     [ normalize #H cases H
683     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????);
684       whd in Heq; >Heq
685       >eq_identifier_refl / by refl/
686     ]
687   | #i #H whd in match (does_not_occur ????);
688     whd in match (instruction_matches_identifier ????);
689     cases h #hi #hp cases hi normalize nodelta
690     [ @(IH i) @H
691     | #l' @eq_identifier_elim
692       [ normalize / by /
693       | normalize #_ @(IH i) @H
694       ]
695     ]
696   ]
697 ]
698qed.
699
700(* The function that creates the label-to-address map *)
701definition create_label_cost_map0: ∀program:list labelled_instruction.
702  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
703    let 〈labels,costs〉 ≝ labels_costs in
704    ∀l.occurs_exactly_once ?? l program →
705    bitvector_of_nat ? (lookup_def ?? labels l 0) =
706     address_of_word_labels_code_mem program l
707  ) ≝
708  λprogram.
709  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
710  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
711    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
712    ppc = |prefix| ∧
713    ∀l.occurs_exactly_once ?? l prefix →
714    bitvector_of_nat ? (lookup_def ?? labels l 0) =
715     address_of_word_labels_code_mem prefix l)
716  program
717  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
718   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
719   let 〈label,instr〉 ≝ x in
720   let labels ≝
721     match label with
722     [ None   ⇒ labels
723     | Some l ⇒ add … labels l ppc
724     ] in
725   let costs ≝
726     match instr with
727     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
728     | _ ⇒ costs ] in
729      〈labels,costs,S ppc〉
730   ) 〈(empty_map …),(Stub ??),0〉)).
731[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2
732  -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
733 inversion label [#EQ | #l #EQ]
734 [ #lbl #Hocc <address_of_word_labels_code_mem_None [2: @Hocc] normalize nodelta
735   >occurs_exactly_once_None in Hocc; @(IH2 lbl)
736 | #lbl normalize nodelta inversion (eq_identifier ? lbl l)
737   [ #Heq #Hocc >(eq_identifier_eq … Heq)
738     >address_of_word_labels_code_mem_Some_hit
739     [ >IH1 >lookup_def_add_hit %
740     | <(eq_identifier_eq … Heq) in Hocc; //
741     ]
742   | #Hneq #Hocc
743     <address_of_word_labels_code_mem_Some_miss
744     [ >lookup_def_add_miss
745       [ @IH2 >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym> Hneq //
746       | % @neq_identifier_neq @Hneq
747       ]
748     | @Hocc
749     | >eq_identifier_sym @Hneq
750     ]
751   ]
752 ]
753| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
754  #l #abs cases (abs)
755| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
756  #_ #H @H
757]
758qed.
759
760(* The function that creates the label-to-address map *)
761definition create_label_cost_map: ∀program:list labelled_instruction.
762  label_map × (BitVectorTrie costlabel 16) ≝
763    λprogram.
764      pi1 … (create_label_cost_map0 program).
765
766theorem create_label_cost_map_ok:
767 ∀pseudo_program: pseudo_assembly_program.
768   let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in
769    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
770     bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id.
771 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2
772qed.
773
774
775(*CSC: move elsewhere; practically equal to shift_nth_safe but for commutation
776  of addition. One of the two lemmas should disappear. *)
777lemma nth_safe_prepend:
778 ∀A,l1,l2,j.∀H:j<|l2|.∀K:|l1|+j<|(l1@l2)|.
779  nth_safe A j l2 H =nth_safe A (|l1|+j) (l1@l2) K.
780 #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe
781qed.
782
783lemma nth_safe_cons:
784 ∀A,hd,tl,l2,j,j_ok,Sj_ok.
785  nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok.
786//
787qed.
788
789lemma eq_nth_safe_proof_irrelevant:
790 ∀A,l,i,i_ok,i_ok'.
791  nth_safe A l i i_ok = nth_safe A l i i_ok'.
792#A #l #i #i_ok #i_ok' %
793qed.
794
795(*CSC: move elsewhere *)
796axiom nat_of_bitvector_add:
797 ∀n,v1,v2.
798  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
799   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
800
801(*CSC: move elsewhere *)
802lemma fetch_pseudo_instruction_append:
803 ∀l1,l2. |l1@l2| < 2^16 → ∀ppc,ppc_ok,ppc_ok'.
804  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
805  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
806  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
807 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
808 cut (|l1| + nat_of_bitvector … ppc < 2^16)
809 [ @(transitive_lt … l1l2_ok) >length_append /2 by monotonic_lt_plus_r/ ]
810 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
811 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
812 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
813 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
814 #lbl #instr normalize nodelta >add_associative %
815qed.
816
817definition sigma_policy_specification ≝
818  λprogram: pseudo_assembly_program.
819  λsigma: Word → Word.
820  λpolicy: Word → bool.
821  sigma (zero …) = zero … ∧
822  ∀ppc: Word. ∀ppc_ok.
823    let instr_list ≝ \snd program in
824    let pc ≝ sigma ppc in
825    let labels ≝ \fst (create_label_cost_map instr_list) in
826    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
827    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
828    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
829     (nat_of_bitvector … ppc ≤ |instr_list| →
830       next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction)))
831     ∧       
832      (  (nat_of_bitvector … ppc < |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc)
833       ∨ (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
834
835definition assembly:
836    ∀p: pseudo_assembly_program.
837    ∀sigma: Word → Word.
838    ∀policy: Word → bool.
839      Σres:list Byte × (BitVectorTrie costlabel 16).
840       sigma_policy_specification p sigma policy →
841       let 〈preamble,instr_list〉 ≝ p in
842       |instr_list| < 2^16 →
843       let 〈assembled,costs〉 ≝ res in
844       let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
845       let datalabels ≝ construct_datalabels preamble in
846       let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
847       let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
848       ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < |instr_list|.
849         let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc ppc_ok in
850         let 〈len,assembledi〉 ≝
851          assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
852         ∀j:nat. ∀H: j < |assembledi|. ∀K.
853          nth_safe ? j assembledi H =
854           nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j)))
855            assembled K
856
857  λp.
858  λsigma.
859  λpolicy.
860  deplet 〈preamble, instr_list〉 as p_refl ≝ p in
861  let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
862  let datalabels ≝ construct_datalabels preamble in
863  let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
864  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
865  let 〈ignore,revcode〉 ≝ pi1 … (
866     foldl_strong
867      (option Identifier × pseudo_instruction)
868      (λpre. Σppc_code:(Word × (list Byte)).
869       sigma_policy_specification 〈preamble,instr_list〉 sigma policy →
870        |instr_list| < 2^16 →
871        let 〈ppc,code〉 ≝ ppc_code in
872         ppc = bitvector_of_nat … (|pre|) ∧
873         nat_of_bitvector … (sigma ppc) = |code| ∧
874         ∀ppc'.∀ppc_ok'.
875          nat_of_bitvector … ppc' < nat_of_bitvector … ppc →
876           let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' ppc_ok' in
877           let 〈len,assembledi〉 ≝
878            assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
879           ∀j:nat. ∀H: j < |assembledi|. ∀K.
880            nth_safe ? j assembledi H =
881             nth_safe ? (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat ? j))) (reverse … code) K)
882      instr_list
883      (λprefix,hd,tl,prf,ppc_code.
884        let 〈ppc, code〉 ≝ pi1 … ppc_code in
885        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (\snd hd) in
886        let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in
887         〈new_ppc, (reverse … program @ code)〉)
888      〈(zero ?), [ ]〉)
889    in
890     〈reverse … revcode,
891      fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
892  [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode
893    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
894    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
895    >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
896  | * #sigma_pol_ok1 #_ #instr_list_ok %
897    [ % // >sigma_pol_ok1 % ]
898    #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
899  | * #sigma_pol_ok1 #sigma_pol_ok2 #instr_list_ok cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
900    #IH cases (IH ? instr_list_ok) [2: % assumption ] * #IH1 #IH3 #IH2 whd % [%
901    [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon
902    |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]]
903    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc
904    cases (le_to_or_lt_eq … LTppc_ppc)
905    [2: #S_S_eq normalize nodelta in S_S_eq;
906        (*CSC: TRUE, NEEDS SOME WORK *)
907        cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
908        >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
909        >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
910        >fetch_pseudo_instruction_append
911        [3: @le_S_S @le_O_n
912        |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
913        |4: <prf <p_refl in instr_list_ok; #H @H ]
914        #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2
915        #j #LTj >nat_of_bitvector_add
916        >nat_of_bitvector_bitvector_of_nat_inverse
917        [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
918        |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
919        >reverse_append >reverse_reverse >IH3 <(length_reverse … code)
920        @nth_safe_prepend
921    | #LTppc''
922      cut (nat_of_bitvector … ppc' < |instr_list|)
923      [ normalize nodelta in LTppc'';
924        @(transitive_le … (nat_of_bitvector … ppc))
925        [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse
926           [ //
927           | <p_refl in instr_list_ok; #instr_list_ok
928             @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ]
929        | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
930          [ >commutative_plus #H @H
931          | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
932            @(transitive_le … (S (|instr_list|)))
933            [2: <p_refl in instr_list_ok;  #instr_list_ok assumption
934            | >IH1 >prf >length_append @le_S_S >(commutative_plus (|prefix|))
935              >length_append >nat_of_bitvector_bitvector_of_nat_inverse
936              [2: <p_refl in instr_list_ok; >prf >length_append #H
937                  @(transitive_le … H) //
938              | @le_S_S // ]]]]]
939      #X lapply (IH2 ppc' X)
940      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
941      @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
942      change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ∀j:ℕ. ∀H:j<|assembledi|.?)
943      >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
944      >IH
945      [2: >length_reverse <IH3 (*CSC: NEEDS JAAP INVARIANT PLUS SOME WORK *) cases daemon
946      | @shift_nth_prefix
947      |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
948         [ >commutative_plus %
949         | >commutative_plus >IH1 whd in ⊢ (?%?);
950           @(transitive_le … (S (|instr_list|)))
951           [2:  <p_refl in instr_list_ok;  #instr_list_ok assumption
952           | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
953             [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
954qed.
955
956definition assembly_unlabelled_program:
957    assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
958  λp.
959    Some … (〈foldr … (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.