Context Navigation

Assembly.ma @ 1393

Last change on this file since 1393 was 1393, checked in by boender, 9 years ago
added invariant for policy trie to assembly change (syntax only) to status in order to make it compile added lemma + renaming to bitvectortrie
File size: 59.5 KB

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

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format