Context Navigation

Assembly.ma @ 1578

Last change on this file since 1578 was 1578, checked in by boender, 9 years ago
proof of termination of policy completed (needs some clean-up work though)
File size: 90.7 KB

Line
1	include "ASM/ASM.ma".
2	include "ASM/Arithmetic.ma".
3	include "ASM/Fetch.ma".
4	include "ASM/Status.ma".
5	include alias "basics/logic.ma".
6	include alias "arithmetics/nat.ma".
7
8	definition assembly_preinstruction ≝
9	λA: Type[0].
10	λaddr_of: A → Byte. (* relative *)
11	λpre: preinstruction A.
12	match pre with
13	[ ADD addr1 addr2 ⇒
14	match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
15	[ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
16	\| DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
17	\| INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
18	\| DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
19	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
20	\| ADDC addr1 addr2 ⇒
21	match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
22	[ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
23	\| DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
24	\| INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
25	\| DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
26	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
27	\| ANL addrs ⇒
28	match addrs with
29	[ inl addrs ⇒ match addrs with
30	[ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
31	match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
32	[ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
33	\| DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
34	\| INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
35	\| DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
36	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
37	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
38	let b1 ≝
39	match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
40	[ DIRECT b1 ⇒ λ_.b1
41	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
42	match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
43	[ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
44	\| DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
45	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
46	]
47	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
48	match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
49	[ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
50	\| N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
51	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
52	\| CLR addr ⇒
53	match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
54	[ ACC_A ⇒ λ_.
55	[ ([[true; true; true; false; false; true; false; false]]) ]
56	\| CARRY ⇒ λ_.
57	[ ([[true; true; false; false; false; false; true; true]]) ]
58	\| BIT_ADDR b1 ⇒ λ_.
59	[ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
60	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
61	\| CPL addr ⇒
62	match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
63	[ ACC_A ⇒ λ_.
64	[ ([[true; true; true; true; false; true; false; false]]) ]
65	\| CARRY ⇒ λ_.
66	[ ([[true; false; true; true; false; false; true; true]]) ]
67	\| BIT_ADDR b1 ⇒ λ_.
68	[ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
69	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
70	\| DA addr ⇒
71	[ ([[true; true; false; true; false; true; false; false]]) ]
72	\| DEC addr ⇒
73	match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
74	[ ACC_A ⇒ λ_.
75	[ ([[false; false; false; true; false; true; false; false]]) ]
76	\| REGISTER r ⇒ λ_.
77	[ ([[false; false; false; true; true]]) @@ r ]
78	\| DIRECT b1 ⇒ λ_.
79	[ ([[false; false; false; true; false; true; false; true]]); b1 ]
80	\| INDIRECT i1 ⇒ λ_.
81	[ ([[false; false; false; true; false; true; true; i1]]) ]
82	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
83	\| DJNZ addr1 addr2 ⇒
84	let b2 ≝ addr_of addr2 in
85	match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
86	[ REGISTER r ⇒ λ_.
87	[ ([[true; true; false; true; true]]) @@ r ; b2 ]
88	\| DIRECT b1 ⇒ λ_.
89	[ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
90	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
91	\| JC addr ⇒
92	let b1 ≝ addr_of addr in
93	[ ([[false; true; false; false; false; false; false; false]]); b1 ]
94	\| JNC addr ⇒
95	let b1 ≝ addr_of addr in
96	[ ([[false; true; false; true; false; false; false; false]]); b1 ]
97	\| JZ addr ⇒
98	let b1 ≝ addr_of addr in
99	[ ([[false; true; true; false; false; false; false; false]]); b1 ]
100	\| JNZ addr ⇒
101	let b1 ≝ addr_of addr in
102	[ ([[false; true; true; true; false; false; false; false]]); b1 ]
103	\| JB addr1 addr2 ⇒
104	let b2 ≝ addr_of addr2 in
105	match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
106	[ BIT_ADDR b1 ⇒ λ_.
107	[ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
108	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
109	\| JNB addr1 addr2 ⇒
110	let b2 ≝ addr_of addr2 in
111	match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
112	[ BIT_ADDR b1 ⇒ λ_.
113	[ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
114	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
115	\| JBC addr1 addr2 ⇒
116	let b2 ≝ addr_of addr2 in
117	match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
118	[ BIT_ADDR b1 ⇒ λ_.
119	[ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
120	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
121	\| CJNE addrs addr3 ⇒
122	let b3 ≝ addr_of addr3 in
123	match addrs with
124	[ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
125	match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
126	[ DIRECT b1 ⇒ λ_.
127	[ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
128	\| DATA b1 ⇒ λ_.
129	[ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
130	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
131	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
132	let b2 ≝
133	match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
134	[ DATA b2 ⇒ λ_. b2
135	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
136	match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
137	[ REGISTER r ⇒ λ_.
138	[ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
139	\| INDIRECT i1 ⇒ λ_.
140	[ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
141	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
142	]
143	\| DIV addr1 addr2 ⇒
144	[ ([[true;false;false;false;false;true;false;false]]) ]
145	\| INC addr ⇒
146	match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
147	[ ACC_A ⇒ λ_.
148	[ ([[false;false;false;false;false;true;false;false]]) ]
149	\| REGISTER r ⇒ λ_.
150	[ ([[false;false;false;false;true]]) @@ r ]
151	\| DIRECT b1 ⇒ λ_.
152	[ ([[false; false; false; false; false; true; false; true]]); b1 ]
153	\| INDIRECT i1 ⇒ λ_.
154	[ ([[false; false; false; false; false; true; true; i1]]) ]
155	\| DPTR ⇒ λ_.
156	[ ([[true;false;true;false;false;false;true;true]]) ]
157	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
158	\| MOV addrs ⇒
159	match addrs with
160	[ inl addrs ⇒
161	match addrs with
162	[ inl addrs ⇒
163	match addrs with
164	[ inl addrs ⇒
165	match addrs with
166	[ inl addrs ⇒
167	match addrs with
168	[ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
169	match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
170	[ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
171	\| DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
172	\| INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
173	\| DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
174	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
175	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
176	match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
177	[ REGISTER r ⇒ λ_.
178	match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
179	[ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
180	\| DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
181	\| DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
182	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
183	\| INDIRECT i1 ⇒ λ_.
184	match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
185	[ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
186	\| DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
187	\| DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
188	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
189	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
190	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
191	let b1 ≝
192	match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
193	[ DIRECT b1 ⇒ λ_. b1
194	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
195	match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
196	[ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
197	\| REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
198	\| DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
199	\| INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
200	\| DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
201	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
202	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
203	match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
204	[ DATA16 w ⇒ λ_.
205	let b1_b2 ≝ split ? 8 8 w in
206	let b1 ≝ \fst b1_b2 in
207	let b2 ≝ \snd b1_b2 in
208	[ ([[true;false;false;true;false;false;false;false]]); b1; b2]
209	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
210	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
211	match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
212	[ BIT_ADDR b1 ⇒ λ_.
213	[ ([[true;false;true;false;false;false;true;false]]); b1 ]
214	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
215	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
216	match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
217	[ BIT_ADDR b1 ⇒ λ_.
218	[ ([[true;false;false;true;false;false;true;false]]); b1 ]
219	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
220	\| MOVX addrs ⇒
221	match addrs with
222	[ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
223	match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
224	[ EXT_INDIRECT i1 ⇒ λ_.
225	[ ([[true;true;true;false;false;false;true;i1]]) ]
226	\| EXT_INDIRECT_DPTR ⇒ λ_.
227	[ ([[true;true;true;false;false;false;false;false]]) ]
228	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
229	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
230	match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
231	[ EXT_INDIRECT i1 ⇒ λ_.
232	[ ([[true;true;true;true;false;false;true;i1]]) ]
233	\| EXT_INDIRECT_DPTR ⇒ λ_.
234	[ ([[true;true;true;true;false;false;false;false]]) ]
235	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
236	\| MUL addr1 addr2 ⇒
237	[ ([[true;false;true;false;false;true;false;false]]) ]
238	\| NOP ⇒
239	[ ([[false;false;false;false;false;false;false;false]]) ]
240	\| ORL addrs ⇒
241	match addrs with
242	[ inl addrs ⇒
243	match addrs with
244	[ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
245	match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
246	[ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
247	\| DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
248	\| INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
249	\| DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
250	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
251	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
252	let b1 ≝
253	match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
254	[ DIRECT b1 ⇒ λ_. b1
255	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
256	match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
257	[ ACC_A ⇒ λ_.
258	[ ([[false;true;false;false;false;false;true;false]]); b1 ]
259	\| DATA b2 ⇒ λ_.
260	[ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
261	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
262	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
263	match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
264	[ BIT_ADDR b1 ⇒ λ_.
265	[ ([[false;true;true;true;false;false;true;false]]); b1 ]
266	\| N_BIT_ADDR b1 ⇒ λ_.
267	[ ([[true;false;true;false;false;false;false;false]]); b1 ]
268	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
269	\| POP addr ⇒
270	match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
271	[ DIRECT b1 ⇒ λ_.
272	[ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
273	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
274	\| PUSH addr ⇒
275	match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
276	[ DIRECT b1 ⇒ λ_.
277	[ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
278	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
279	\| RET ⇒
280	[ ([[false;false;true;false;false;false;true;false]]) ]
281	\| RETI ⇒
282	[ ([[false;false;true;true;false;false;true;false]]) ]
283	\| RL addr ⇒
284	[ ([[false;false;true;false;false;false;true;true]]) ]
285	\| RLC addr ⇒
286	[ ([[false;false;true;true;false;false;true;true]]) ]
287	\| RR addr ⇒
288	[ ([[false;false;false;false;false;false;true;true]]) ]
289	\| RRC addr ⇒
290	[ ([[false;false;false;true;false;false;true;true]]) ]
291	\| SETB addr ⇒
292	match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
293	[ CARRY ⇒ λ_.
294	[ ([[true;true;false;true;false;false;true;true]]) ]
295	\| BIT_ADDR b1 ⇒ λ_.
296	[ ([[true;true;false;true;false;false;true;false]]); b1 ]
297	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
298	\| SUBB addr1 addr2 ⇒
299	match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
300	[ REGISTER r ⇒ λ_.
301	[ ([[true;false;false;true;true]]) @@ r ]
302	\| DIRECT b1 ⇒ λ_.
303	[ ([[true;false;false;true;false;true;false;true]]); b1]
304	\| INDIRECT i1 ⇒ λ_.
305	[ ([[true;false;false;true;false;true;true;i1]]) ]
306	\| DATA b1 ⇒ λ_.
307	[ ([[true;false;false;true;false;true;false;false]]); b1]
308	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
309	\| SWAP addr ⇒
310	[ ([[true;true;false;false;false;true;false;false]]) ]
311	\| XCH addr1 addr2 ⇒
312	match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
313	[ REGISTER r ⇒ λ_.
314	[ ([[true;true;false;false;true]]) @@ r ]
315	\| DIRECT b1 ⇒ λ_.
316	[ ([[true;true;false;false;false;true;false;true]]); b1]
317	\| INDIRECT i1 ⇒ λ_.
318	[ ([[true;true;false;false;false;true;true;i1]]) ]
319	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
320	\| XCHD addr1 addr2 ⇒
321	match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
322	[ INDIRECT i1 ⇒ λ_.
323	[ ([[true;true;false;true;false;true;true;i1]]) ]
324	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
325	\| XRL addrs ⇒
326	match addrs with
327	[ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
328	match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
329	[ REGISTER r ⇒ λ_.
330	[ ([[false;true;true;false;true]]) @@ r ]
331	\| DIRECT b1 ⇒ λ_.
332	[ ([[false;true;true;false;false;true;false;true]]); b1]
333	\| INDIRECT i1 ⇒ λ_.
334	[ ([[false;true;true;false;false;true;true;i1]]) ]
335	\| DATA b1 ⇒ λ_.
336	[ ([[false;true;true;false;false;true;false;false]]); b1]
337	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
338	\| inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
339	let b1 ≝
340	match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
341	[ DIRECT b1 ⇒ λ_. b1
342	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
343	match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
344	[ ACC_A ⇒ λ_.
345	[ ([[false;true;true;false;false;false;true;false]]); b1 ]
346	\| DATA b2 ⇒ λ_.
347	[ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
348	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
349	].
350
351	definition assembly1 ≝
352	λi: instruction.
353	match i with
354	[ ACALL addr ⇒
355	match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
356	[ ADDR11 w ⇒ λ_.
357	let v1_v2 ≝ split ? 3 8 w in
358	let v1 ≝ \fst v1_v2 in
359	let v2 ≝ \snd v1_v2 in
360	[ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
361	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
362	\| AJMP addr ⇒
363	match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
364	[ ADDR11 w ⇒ λ_.
365	let v1_v2 ≝ split ? 3 8 w in
366	let v1 ≝ \fst v1_v2 in
367	let v2 ≝ \snd v1_v2 in
368	[ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
369	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
370	\| JMP adptr ⇒
371	[ ([[false;true;true;true;false;false;true;true]]) ]
372	\| LCALL addr ⇒
373	match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
374	[ ADDR16 w ⇒ λ_.
375	let b1_b2 ≝ split ? 8 8 w in
376	let b1 ≝ \fst b1_b2 in
377	let b2 ≝ \snd b1_b2 in
378	[ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]
379	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
380	\| LJMP addr ⇒
381	match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
382	[ ADDR16 w ⇒ λ_.
383	let b1_b2 ≝ split ? 8 8 w in
384	let b1 ≝ \fst b1_b2 in
385	let b2 ≝ \snd b1_b2 in
386	[ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]
387	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
388	\| MOVC addr1 addr2 ⇒
389	match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
390	[ ACC_DPTR ⇒ λ_.
391	[ ([[true;false;false;true;false;false;true;true]]) ]
392	\| ACC_PC ⇒ λ_.
393	[ ([[true;false;false;false;false;false;true;true]]) ]
394	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
395	\| SJMP addr ⇒
396	match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
397	[ RELATIVE b1 ⇒ λ_.
398	[ ([[true;false;false;false;false;false;false;false]]); b1 ]
399	\| _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
400	\| RealInstruction instr ⇒
401	assembly_preinstruction [[ relative ]]
402	(λx.
403	match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
404	[ RELATIVE r ⇒ λ_. r
405	\| _ ⇒ λabsd. ⊥
406	] (subaddressing_modein … x)) instr
407	].
408	cases absd
409	qed.
410
411	inductive jump_length: Type[0] ≝
412	\| short_jump: jump_length
413	\| medium_jump: jump_length
414	\| long_jump: jump_length.
415
416	(* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
417	definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16.
418
419	definition expand_relative_jump_internal:
420	(Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
421	option (list instruction)
422	≝
423	λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
424	match jmp_len with
425	[ short_jump ⇒
426	let lookup_address ≝ lookup_labels jmp in
427	let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
428	let 〈upper, lower〉 ≝ split ? 8 8 result in
429	if eq_bv ? upper (zero 8) then
430	let address ≝ RELATIVE lower in
431	Some ? [ RealInstruction (i address) ]
432	else
433	None ?
434	\| medium_jump ⇒ None …
435	\| long_jump ⇒
436	Some ?
437	[ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
438	SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
439	LJMP (ADDR16 (lookup_labels jmp))
440	]
441	].
442	@ I
443	qed.
444
445	definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
446	λlookup_labels.
447	λjmp_len: jump_length.
448	λpc.
449	λi: preinstruction Identifier.
450	let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
451	match i with
452	[ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
453	\| JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
454	\| JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
455	\| JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
456	\| JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
457	\| JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
458	\| JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
459	\| CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
460	\| DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
461	\| ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
462	\| ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
463	\| SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
464	\| INC arg ⇒ Some ? [ INC ? arg ]
465	\| DEC arg ⇒ Some ? [ DEC ? arg ]
466	\| MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
467	\| DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
468	\| DA arg ⇒ Some ? [ DA ? arg ]
469	\| ANL arg ⇒ Some ? [ ANL ? arg ]
470	\| ORL arg ⇒ Some ? [ ORL ? arg ]
471	\| XRL arg ⇒ Some ? [ XRL ? arg ]
472	\| CLR arg ⇒ Some ? [ CLR ? arg ]
473	\| CPL arg ⇒ Some ? [ CPL ? arg ]
474	\| RL arg ⇒ Some ? [ RL ? arg ]
475	\| RR arg ⇒ Some ? [ RR ? arg ]
476	\| RLC arg ⇒ Some ? [ RLC ? arg ]
477	\| RRC arg ⇒ Some ? [ RRC ? arg ]
478	\| SWAP arg ⇒ Some ? [ SWAP ? arg ]
479	\| MOV arg ⇒ Some ? [ MOV ? arg ]
480	\| MOVX arg ⇒ Some ? [ MOVX ? arg ]
481	\| SETB arg ⇒ Some ? [ SETB ? arg ]
482	\| PUSH arg ⇒ Some ? [ PUSH ? arg ]
483	\| POP arg ⇒ Some ? [ POP ? arg ]
484	\| XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
485	\| XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
486	\| RET ⇒ Some ? [ RET ? ]
487	\| RETI ⇒ Some ? [ RETI ? ]
488	\| NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
489	].
490
491	definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
492	λlookup_labels.
493	λlookup_datalabels.
494	λpc.
495	λjmp_len.
496	λi.
497	match i with
498	[ Cost cost ⇒ Some ? [ ]
499	\| Comment comment ⇒ Some ? [ ]
500	\| Call call ⇒
501	match jmp_len with
502	[ short_jump ⇒ None ?
503	\| medium_jump ⇒
504	let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
505	let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
506	if eq_bv ? ignore fst_5 then
507	let address ≝ ADDR11 address in
508	Some ? ([ ACALL address ])
509	else
510	None ?
511	\| long_jump ⇒
512	let address ≝ ADDR16 (lookup_labels call) in
513	Some ? [ LCALL address ]
514	]
515	\| Mov d trgt ⇒
516	let address ≝ DATA16 (lookup_datalabels trgt) in
517	Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
518	\| Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
519	\| Jmp jmp ⇒
520	match jmp_len with
521	[ short_jump ⇒
522	let lookup_address ≝ lookup_labels jmp in
523	let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
524	let 〈upper, lower〉 ≝ split ? 8 8 result in
525	if eq_bv ? upper (zero 8) then
526	let address ≝ RELATIVE lower in
527	Some ? [ SJMP address ]
528	else
529	None ?
530	\| medium_jump ⇒
531	let address ≝ lookup_labels jmp in
532	let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
533	let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
534	if eq_bv ? fst_5_addr fst_5_pc then
535	let address ≝ ADDR11 rest_addr in
536	Some ? ([ AJMP address ])
537	else
538	None ?
539	\| long_jump ⇒
540	let address ≝ ADDR16 (lookup_labels jmp) in
541	Some ? [ LJMP address ]
542	]
543	].
544	@ I
545	qed.
546
547	(* label_map: identifier ↦ 〈instruction number, address〉 *)
548	definition label_map ≝ identifier_map ASMTag (nat × nat).
549
550	definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
551	λpc.λjmp_len.λinstr.
552	let bv_pc ≝ bitvector_of_nat 16 pc in
553	let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
554	let bv: list (BitVector 8) ≝ match ilist with
555	[ None ⇒ (* hmm, this shouldn't happen *) [ ]
556	\| Some l ⇒ flatten … (map … assembly1 l)
557	] in
558	pc + (\|bv\|).
559
560	definition is_label ≝
561	λx:labelled_instruction.λl:Identifier.
562	let 〈lbl,instr〉 ≝ x in
563	match lbl with
564	[ Some l' ⇒ l' = l
565	\| _ ⇒ False
566	].
567
568	lemma label_does_not_occur:
569	∀i,p,l.
570	is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
571	#i #p #l generalize in match i; elim p
572	[ #i >nth_nil #H @⊥ @H
573	\| #h #t #IH #i cases i -i
574	[ cases h #hi #hp cases hi
575	[ normalize #H @⊥ @H
576	\| #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
577	whd in Heq; >Heq
578	>eq_identifier_refl //
579	]
580	\| #i #H whd in match (does_not_occur ??);
581	whd in match (instruction_matches_identifier ??);
582	cases h #hi #hp cases hi normalize nodelta
583	[ @(IH i) @H
584	\| #l' @eq_identifier_elim
585	[ normalize //
586	\| normalize #_ @(IH i) @H
587	]
588	]
589	]
590	]
591	qed.
592
593	lemma coerc_pair_sigma:
594	∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
595	#A #B #P * #a #b #p % [@a \| /2/]
596	qed.
597	coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
598	≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
599
600	definition create_label_map: ∀program:list labelled_instruction.
601	∀policy:jump_expansion_policy.
602	(Σlabels:label_map.
603	∀i:ℕ.lt i (\|program\|) →
604	∀l.occurs_exactly_once l program →
605	is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
606	∃a.lookup … labels l = Some ? 〈i,a〉
607	) ≝
608	λprogram.λpolicy.
609	let 〈final_pc, final_labels〉 ≝
610	foldl_strong (option Identifier × pseudo_instruction)
611	(λprefix.ℕ × (Σlabels.
612	∀i:ℕ.lt i (\|prefix\|) →
613	∀l.occurs_exactly_once l prefix →
614	is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
615	∃a.lookup … labels l = Some ? 〈i,a〉)
616	)
617	program
618	(λprefix.λx.λtl.λprf.λacc.
619	let 〈pc,labels〉 ≝ acc in
620	let 〈label,instr〉 ≝ x in
621	let new_labels ≝
622	match label with
623	[ None ⇒ labels
624	\| Some l ⇒ add … labels l 〈\|prefix\|, pc〉
625	] in
626	let jmp_len ≝ \snd (bvt_lookup ?? (bitvector_of_nat 16 (\|prefix\|)) policy 〈pc, long_jump〉) in
627	〈add_instruction_size pc jmp_len instr, new_labels〉
628	) 〈0, empty_map …〉 in
629	final_labels.
630	[ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
631	[ #Hi #l normalize nodelta; cases label normalize nodelta
632	[ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
633	lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr
634	% [ @addr \| @Haddr ]
635	\| #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
636	@eq_identifier_elim #Heq #Hocc
637	[ normalize in Hocc;
638	>(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl
639	@⊥ @(absurd … Hocc)
640	\| normalize nodelta lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
641	[ #addr #Haddr % [ @addr \| <Haddr @lookup_add_miss /2/ ]
642	\| >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
643	]
644	]
645	>(label_does_not_occur i … Hl) normalize nodelta @nmk //
646	]
647	\| #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
648	[ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
649	[ normalize nodelta #H @⊥ @H
650	\| #l' normalize nodelta #Heq % [ @pc \| <Heq normalize nodelta @lookup_add_hit ]
651	]
652	\| @le_n
653	]
654	]
655	\| #i #Hi #l #Hl @⊥ @Hl
656	]
657	qed.
658
659	definition select_reljump_length: label_map → ℕ → Identifier → jump_length ≝
660	λlabels.λpc.λlbl.
661	let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
662	if leb pc addr (* forward jump *)
663	then if leb (addr - pc) 126
664	then short_jump
665	else long_jump
666	else if leb (pc - addr) 129
667	then short_jump
668	else long_jump.
669
670	definition select_call_length: label_map → ℕ → Identifier → jump_length ≝
671	λlabels.λpc_nat.λlbl.
672	let pc ≝ bitvector_of_nat 16 pc_nat in
673	let addr ≝ bitvector_of_nat 16 (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
674	let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
675	let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
676	if eq_bv ? fst_5_addr fst_5_pc
677	then medium_jump
678	else long_jump.
679
680	definition select_jump_length: label_map → ℕ → Identifier → jump_length ≝
681	λlabels.λpc.λlbl.
682	let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
683	if leb pc addr
684	then if leb (addr - pc) 126
685	then short_jump
686	else select_call_length labels pc lbl
687	else if leb (pc - addr) 129
688	then short_jump
689	else select_call_length labels pc lbl.
690
691	definition jump_expansion_step_instruction: label_map → ℕ →
692	preinstruction Identifier → option jump_length ≝
693	λlabels.λpc.λi.
694	match i with
695	[ JC j ⇒ Some ? (select_reljump_length labels pc j)
696	\| JNC j ⇒ Some ? (select_reljump_length labels pc j)
697	\| JZ j ⇒ Some ? (select_reljump_length labels pc j)
698	\| JNZ j ⇒ Some ? (select_reljump_length labels pc j)
699	\| JB _ j ⇒ Some ? (select_reljump_length labels pc j)
700	\| JBC _ j ⇒ Some ? (select_reljump_length labels pc j)
701	\| JNB _ j ⇒ Some ? (select_reljump_length labels pc j)
702	\| CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
703	\| DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
704	\| _ ⇒ None ?
705	].
706
707	definition max_length: jump_length → jump_length → jump_length ≝
708	λj1.λj2.
709	match j1 with
710	[ long_jump ⇒ long_jump
711	\| medium_jump ⇒
712	match j2 with
713	[ long_jump ⇒ long_jump
714	\| _ ⇒ medium_jump
715	]
716	\| short_jump ⇒ j2
717	].
718
719	definition jmple: jump_length → jump_length → Prop ≝
720	λj1.λj2.
721	match j1 with
722	[ short_jump ⇒
723	match j2 with
724	[ short_jump ⇒ False
725	\| _ ⇒ True
726	]
727	\| medium_jump ⇒
728	match j2 with
729	[ long_jump ⇒ True
730	\| _ ⇒ False
731	]
732	\| long_jump ⇒ False
733	].
734
735	definition jmpleq: jump_length → jump_length → Prop ≝
736	λj1.λj2.jmple j1 j2 ∨ j1 = j2.
737
738	lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
739	#x #y cases x cases y /3 by inl, inr, nmk, I/
740	qed.
741
742	lemma jmpleq_max_length: ∀ol,nl.
743	jmpleq ol (max_length ol nl).
744	#ol #nl cases ol cases nl
745	/2 by or_introl, or_intror, I/
746	qed.
747
748	definition is_jump' ≝
749	λx:preinstruction Identifier.
750	match x with
751	[ JC _ ⇒ True
752	\| JNC _ ⇒ True
753	\| JZ _ ⇒ True
754	\| JNZ _ ⇒ True
755	\| JB _ _ ⇒ True
756	\| JNB _ _ ⇒ True
757	\| JBC _ _ ⇒ True
758	\| CJNE _ _ ⇒ True
759	\| DJNZ _ _ ⇒ True
760	\| _ ⇒ False
761	].
762
763	definition is_jump ≝
764	λx:labelled_instruction.
765	let 〈label,instr〉 ≝ x in
766	match instr with
767	[ Instruction i ⇒ is_jump' i
768	\| Call _ ⇒ True
769	\| Jmp _ ⇒ True
770	\| _ ⇒ False
771	].
772
773	definition jump_in_policy ≝
774	λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
775	∀i:ℕ.i < \|prefix\| →
776	(is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
777	∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉).
778
779	axiom bitvector_of_nat_abs:
780	∀x,y:ℕ.x ≠ y → ¬eq_bv 16 (bitvector_of_nat 16 x) (bitvector_of_nat 16 y).
781
782	lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m.
783	/2/ qed.
784
785	lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
786	∀policy:(Σp:jump_expansion_policy.
787	(∀i.i ≥ \|prefix\| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
788	jump_in_policy prefix p).
789	∀i:ℕ.i < \|prefix\| →
790	¬is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
791	lookup_opt … (bitvector_of_nat 16 i) policy = None ?.
792	#prefix #policy #i #Hi @conj
793	[ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
794	cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
795	[ #H @H
796	\| #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (sig2 ?? policy) i Hi))
797	@(ex_intro … y (ex_intro … z H))
798	]
799	\| #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (sig2 ?? policy) i Hi) Hj)
800	#H elim H -H; #x #H elim H -H; #y #H >H in Hnone; #abs destruct (abs)
801	]
802	qed.
803
804	definition jump_expansion_start: ∀program:list labelled_instruction.
805	Σpolicy:jump_expansion_policy.
806	(∀i.i ≥ \|program\| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
807	jump_in_policy program policy ∧
808	∀i.i < \|program\| → is_jump (nth i ? program 〈None ?, Comment []〉) →
809	lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,short_jump〉 ≝
810	λprogram.
811	foldl_strong (option Identifier × pseudo_instruction)
812	(λprefix.Σpolicy:jump_expansion_policy.
813	(∀i.i ≥ \|prefix\| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
814	jump_in_policy prefix policy ∧
815	∀i.i < \|prefix\| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
816	lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,short_jump〉)
817	program
818	(λprefix.λx.λtl.λprf.λpolicy.
819	let 〈label,instr〉 ≝ x in
820	match instr with
821	[ Instruction i ⇒ match i with
822	[ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
823	\| JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
824	\| JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
825	\| JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
826	\| JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
827	\| JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
828	\| JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
829	\| CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
830	\| DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
831	\| _ ⇒ (eject … policy)
832	]
833	\| Call c ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
834	\| Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,short_jump〉 policy
835	\| _ ⇒ (eject … policy)
836	]
837	) (Stub ? ?).
838	[1,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,35,36,37,38,39,40,41,42:
839	@conj
840	[1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
841	@conj
842	#i >append_length <commutative_plus #Hi normalize in Hi;
843	[1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
844	cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i)
845	[2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62:
846	<Hi @le_n_Sn
847	]
848	@le_S_to_le @le_S_to_le @Hi
849	]
850	cases (le_to_or_lt_eq … Hi) -Hi; #Hi
851	[1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
852	>(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
853	@(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
854	]
855	@conj >(injective_S … Hi)
856	[1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
857	>(nth_append_second ? ? prefix ? ? (le_n (\|prefix\|))) <minus_n_n #H @⊥ @H
858	]
859	#H elim H; -H; #t1 #H elim H; -H #t2 #H
860	lapply (proj1 ?? (proj1 ?? (sig2 ?? policy)) (\|prefix\|) (le_n (\|prefix\|)))
861	#H2 >H2 in H; #H destruct (H)
862	]
863	#i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
864	-Hi; #Hi
865	[1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
866	#Hj @(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi))
867	>(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; //
868	]
869	>(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (\|prefix\|))) <minus_n_n
870	#H @⊥ @H
871	\|2,3,26,27,28,29,30,31,32,33,34: @conj
872	[1,3,5,7,9,11,13,15,17,19,21: @conj
873	[1,3,5,7,9,11,13,15,17,19,21:
874	#i >append_length <commutative_plus #Hi normalize in Hi; >lookup_opt_insert_miss
875	[1,3,5,7,9,11,13,15,17,19,21:
876	@(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
877	]
878	>eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi
879	]
880	#i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
881	-Hi #Hi
882	[1,3,5,7,9,11,13,15,17,19,21:
883	>(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
884	[1,3,5,7,9,11,13,15,17,19,21:
885	@(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
886	]
887	@bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi))
888	]
889	@conj >(injective_S … Hi) #H
890	[2,4,6,8,10,12,14,16,18,20,22:
891	>(nth_append_second ?? prefix ?? (le_n (\|prefix\|))) <minus_n_n //
892	]
893	@(ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy)))
894	]
895	#i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
896	-Hi #Hi
897	[1,3,5,7,9,11,13,15,17,19,21:
898	>(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss
899	[1,3,5,7,9,11,13,15,17,19,21:
900	@(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi) Hj)
901	]
902	@bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi))
903	]
904	#_ >(injective_S … Hi) @lookup_opt_insert_hit
905	\|@conj
906	[@conj
907	[ #i #Hi //
908	\| whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
909	]
910	\| #i #Hi >nth_nil #Hj @⊥ @Hj
911	]
912	qed.
913
914	definition policy_increase: list labelled_instruction → jump_expansion_policy →
915	jump_expansion_policy → Prop ≝
916	λprogram.λop.λp.
917	(* (∀i:ℕ.i < \|program\| →
918	lookup_opt … (bitvector_of_nat ? i) op = lookup_opt … (bitvector_of_nat ? i) p) ∨ *)
919	(∀i:ℕ.i < \|program\| →
920	jmpleq
921	(\snd (bvt_lookup … (bitvector_of_nat ? i) op 〈0,short_jump〉))
922	(\snd (bvt_lookup … (bitvector_of_nat ? i) p 〈0,short_jump〉))).
923
924	definition jump_expansion_step: ∀program:list labelled_instruction.
925	∀old_policy:(Σpolicy.
926	(∀i.i ≥ \|program\| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
927	jump_in_policy program policy).
928	(Σpolicy.
929	(∀i.i ≥ \|program\| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
930	jump_in_policy program policy ∧
931	policy_increase program old_policy policy)
932	≝
933	λprogram.λold_policy.
934	let labels ≝ create_label_map program old_policy in
935	let 〈final_pc, final_policy〉 ≝
936	foldl_strong (option Identifier × pseudo_instruction)
937	(λprefix.ℕ × Σpolicy.
938	(∀i.i ≥ \|prefix\| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
939	jump_in_policy prefix policy ∧
940	policy_increase prefix old_policy policy
941	)
942	program
943	(λprefix.λx.λtl.λprf.λacc.
944	let 〈pc, policy〉 ≝ acc in
945	let 〈label,instr〉 ≝ x in
946	let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (\|prefix\|)) old_policy in
947	let add_instr ≝
948	match instr with
949	[ Instruction i ⇒ jump_expansion_step_instruction labels pc i
950	\| Call c ⇒ Some ? (select_call_length labels pc c)
951	\| Jmp j ⇒ Some ? (select_jump_length labels pc j)
952	\| _ ⇒ None ?
953	] in
954	let 〈new_pc, new_policy〉 ≝
955	let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (\|prefix\|)) old_policy 〈0, short_jump〉 in
956	match add_instr with
957	[ None ⇒ (* i.e. it's not a jump *)
958	〈add_instruction_size pc long_jump instr, policy〉
959	\| Some ai ⇒
960	let new_length ≝ max_length old_length ai in
961	〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (\|prefix\|)) 〈pc, new_length〉 policy〉
962	] in
963	〈new_pc, new_policy〉
964	) 〈0, Stub ? ?〉 in
965	final_policy.
966	[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
967	[ cases (lookup ??? old_policy ?) #h #n cases add_instr
968	[ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
969	\| #z normalize nodelta >lookup_opt_insert_miss
970	[ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
971	\| >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi
972	]
973	]
974	\| cases (le_to_or_lt_eq … Hi) -Hi;
975	[ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
976	[ #Hj lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
977	cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
978	[ @(proj1 ?? Hacc Hj)
979	\| #z elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #Hn
980	% [ @h \| % [ @n \| <Hn @lookup_opt_insert_miss @bitvector_of_nat_abs
981	@(lt_to_not_eq i (\|prefix\|)) @(le_S_S_to_le … Hi) ] ]
982	]
983	\| lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
984	#H elim H -H; #h #H elim H -H; #n cases add_instr cases (lookup ??? old_policy ?)
985	normalize nodelta #x #y [2: #z]
986	#Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n ?))
987	[ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi)
988	\| @Hl
989	]
990	]
991	\| #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (\|prefix\|)))
992	<minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr
993	[1: #pi \| 2,3: #x \| 4,5: #id \| 6: #x #y] @conj normalize nodelta
994	[3,5,11: #H @⊥ @H (* instr is not a jump *)
995	\|4,6,12: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
996	#x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (\|prefix\|) (le_n (\|prefix\|)))
997	#H destruct (H)
998	\|7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n
999	whd in match (snd ???); @(ex_intro ?? pc)
1000	[ @(ex_intro ?? (max_length n (select_jump_length (create_label_map program old_policy) pc id)))
1001	\| @(ex_intro ?? (max_length n (select_call_length (create_label_map program old_policy) pc id)))
1002	] @lookup_opt_insert_hit
1003	\|8,10: #_ //
1004	\|1,2: cases pi
1005	[35,36,37: #H @⊥ @H
1006	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
1007	\|1,2,3,6,7,33,34: #x #y #H @⊥ @H
1008	\|9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #h #n
1009	whd in match (snd ???);
1010	@(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
1011	@lookup_opt_insert_hit
1012	\|11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #h #n
1013	whd in match (snd ???);
1014	@(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
1015	@lookup_opt_insert_hit
1016	\|72,73,74: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
1017	#x #y normalize nodelta
1018	>(proj1 ?? (proj1 ?? (sig2 ?? policy)) (\|prefix\|) (le_n (\|prefix\|))) #H destruct (H)
1019	\|41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
1020	#H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
1021	#x #y normalize nodelta
1022	>(proj1 ?? (proj1 ?? (sig2 ?? policy)) (\|prefix\|) (le_n (\|prefix\|))) #H destruct (H)
1023	\|38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n
1024	cases (lookup ??? old_policy ?) #x #y normalize nodelta
1025	>(proj1 ?? (proj1 ?? (sig2 ?? policy)) (\|prefix\|) (le_n (\|prefix\|))) #H destruct (H)
1026	\|46,47,51,52: #id #_ //
1027	\|48,49,50,53,54: #x #id #_ //
1028	]
1029	]
1030	]
1031	]
1032	\| lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %);
1033	[ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
1034	cases (le_to_or_lt_eq … Hi) -Hi; #Hi
1035	[ cases (lookup … (bitvector_of_nat ? (\|prefix\|)) old_policy 〈0,short_jump〉)
1036	#x #y @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
1037	\| normalize nodelta >(injective_S … Hi)
1038	>lookup_opt_lookup_miss
1039	[ >lookup_opt_lookup_miss
1040	[ //
1041	\| cases (lookup ?? (bitvector_of_nat ? (\|prefix\|)) old_policy 〈0,short_jump〉)
1042	#x #y normalize nodelta
1043	>(proj1 ?? (proj1 ?? (sig2 ?? policy)) (\|prefix\|) (le_n (\|prefix\|))) //
1044	]
1045	\| >(proj1 ?? (jump_not_in_policy program old_policy (\|prefix\|) ?))
1046	[ //
1047	\| >prf >p1 >nth_append_second [ <minus_n_n
1048	generalize in match Ha; normalize nodelta cases instr normalize nodelta
1049	[1: #pi cases pi
1050	[1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/
1051	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/
1052	\|35,36,37: #H normalize /2 by nmk/
1053	\|9,10,14,15: #id whd in match (jump_expansion_step_instruction ???);
1054	#H destruct (H)
1055	\|11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???);
1056	#H destruct (H)
1057	]
1058	\|2,3: #x #H normalize /2 by nmk/
1059	\|6: #x #y #H normalize /2 by nmk/
1060	\|4,5: #id #H destruct (H)
1061	] \| @le_n ]
1062	\| >prf >append_length normalize <plus_n_Sm @le_plus_n_r
1063	]
1064	]
1065	]
1066	\| #x #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
1067	cases (le_to_or_lt_eq … Hi) -Hi; #Hi
1068	[ cases (lookup … (bitvector_of_nat ? (\|prefix\|)) old_policy 〈0,short_jump〉)
1069	#y #z normalize nodelta normalize nodelta >lookup_insert_miss
1070	[ @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
1071	\| @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi)
1072	]
1073	\| >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (sig2 ?? old_policy) (\|prefix\|) ?) ?)
1074	[ #a #H elim H -H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H)
1075	normalize nodelta >lookup_insert_hit @jmpleq_max_length
1076	\| >prf >p1 >nth_append_second
1077	[ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta
1078	[1: #pi cases pi
1079	[1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H)
1080	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize in H; destruct (H)
1081	\|35,36,37: #H normalize in H; destruct (H)
1082	\|9,10,14,15: #id #H //
1083	\|11,12,13,16,17: #x #id #H //
1084	]
1085	\|2,3: #x #H normalize in H; destruct (H)
1086	\|6: #x #y #H normalize in H; destruct (H)
1087	\|4,5: #id #H //
1088	]
1089	\| @le_n ]
1090	\| >prf >append_length normalize <plus_n_Sm @le_plus_n_r
1091	]
1092	]
1093	] ]
1094	\| @conj [ @conj
1095	[ #i #Hi //
1096	\| #i #Hi @conj [ >nth_nil #H @⊥ @H \| #H elim H #x #H1 elim H1 #y #H2
1097	normalize in H2; destruct (H2) ]
1098	]
1099	\| #i #Hi @⊥ @(absurd (i<0)) [ @Hi \| @(not_le_Sn_O) ]
1100	]
1101	qed.
1102
1103	let rec jump_expansion_internal (program: list labelled_instruction)
1104	(n: ℕ) on n: (Σpolicy:jump_expansion_policy.
1105	And
1106	(∀i:ℕ.i ≥ \|program\| → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
1107	(jump_in_policy program policy)) ≝
1108	match n with
1109	[ O ⇒ jump_expansion_start program
1110	\| S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
1111	].
1112	[ @(proj1 ?? (sig2 ?? (jump_expansion_start program)))
1113	\| @(proj1 ?? (sig2 ?? (jump_expansion_step program (jump_expansion_internal program m))))
1114	]
1115	qed.
1116
1117	definition policy_equal ≝
1118	λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
1119	∀n:ℕ.n < \|program\| →
1120	(\snd (bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,short_jump〉)) =
1121	(\snd (bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,short_jump〉)).
1122
1123	lemma pe_refl:
1124	∀program.reflexive ? (policy_equal program).
1125	#program whd #x whd #n #Hn @refl
1126	qed.
1127
1128	lemma pe_sym:
1129	∀program.symmetric ? (policy_equal program).
1130	#program whd #x #y #Hxy whd #n #Hn
1131	>(Hxy n Hn) @refl
1132	qed.
1133
1134	lemma pe_trans:
1135	∀program.transitive ? (policy_equal program).
1136	#program whd #x #y #z #Hxy #Hyz whd #n #Hn
1137	>(Hxy n Hn) @(Hyz n Hn)
1138	qed.
1139
1140	lemma le_plus:
1141	∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k.
1142	#n #m elim m -m;
1143	[ #Hn % [ @O \| <(le_n_O_to_eq n Hn) // ]
1144	\| #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn
1145	[ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) \| >Hk // ]
1146	\| % [ @O \| <Hn // ]
1147	]
1148	]
1149	qed.
1150
1151	theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
1152	#n (elim n) normalize /2 by S_pred/ qed.
1153
1154	lemma pe_step: ∀program:list labelled_instruction.
1155	∀p1,p2:Σpolicy.
1156	(∀i:ℕ.i ≥ \|program\| → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
1157	∧jump_in_policy program policy.
1158	policy_equal program p1 p2 →
1159	policy_equal program (jump_expansion_step program p1) (jump_expansion_step program p2).
1160	#program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
1161	lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
1162	cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?);
1163	[ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl)
1164	#Hnotjmp >lookup_opt_lookup_miss
1165	[ >lookup_opt_lookup_miss
1166	[ @refl
1167	\| @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p2)) n Hn))
1168	[ @(proj1 ?? (sig2 … (jump_expansion_step program p2)))
1169	\| @Hnotjmp
1170	]
1171	]
1172	\| @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p1)) n Hn))
1173	[ @(proj1 ?? (sig2 ?? (jump_expansion_step program p1)))
1174	\| @Hnotjmp
1175	]
1176	]
1177	\| #x #Hl cases daemon
1178	]
1179	qed.
1180
1181	lemma equal_remains_equal: ∀program:list labelled_instruction.∀n:ℕ.
1182	policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
1183	∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
1184	#program #n #Heq #k #Hk elim (le_plus … Hk); #z #H >H -H -Hk -k;
1185	lapply Heq -Heq; lapply n -n; elim z -z;
1186	[ #n #Heq <plus_n_O @pe_refl
1187	\| #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n)))
1188	[ @Heq
1189	\| @pe_step @Hind @Heq
1190	]
1191	]
1192	qed.
1193
1194	lemma dec_bounded_forall:
1195	∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n).
1196	#P #HP_dec #k elim k -k
1197	[ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O
1198	\| #k #Hind cases Hind
1199	[ #Hk cases (HP_dec k)
1200	[ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn)
1201	[ #H @(Hk … (le_S_S_to_le … H))
1202	\| #H >(injective_S … H) @HPk
1203	]
1204	\| #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k))) \| @HPk ]
1205	]
1206	\| #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) \| @Hk ]
1207	]
1208	]
1209	qed.
1210
1211	lemma dec_bounded_exists:
1212	∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n).
1213	#P #HP_dec #k elim k -k
1214	[ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O
1215	\| #k #Hind cases Hind
1216	[ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn) \| @(proj2 … Hn) ]
1217	\| #Hk cases (HP_dec k)
1218	[ #HPk %1 @(ex_intro … k) @conj [ @le_n \| @HPk ]
1219	\| #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn))
1220	[ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj
1221	[ @(le_S_S_to_le … H) \| @(proj2 … Hn) ] \| @Hk ]
1222	\| #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn) \| @HPk ]
1223	]
1224	]
1225	]
1226	]
1227	qed.
1228
1229	lemma not_exists_forall:
1230	∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x.
1231	#k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x)
1232	@conj [ @Hx \| @Habs ]
1233	qed.
1234
1235	lemma not_forall_exists:
1236	∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x.
1237	#k #P #Hdec elim k
1238	[ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O
1239	\| -k #k #Hind #Hfa cases (Hdec k)
1240	[ #HP elim (Hind ?)
1241	[ -Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx) \| @(proj2 ?? Hx) ]
1242	\| @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx)
1243	[ #H2 @H @(le_S_S_to_le … H2)
1244	\| #H2 >(injective_S … H2) @HP
1245	]
1246	]
1247	\| #HP @(ex_intro … k) @conj [ @le_n \| @HP ]
1248	]
1249	]
1250	qed.
1251
1252	(* lemma de_morgan1:
1253	∀A,B:Prop.¬(A ∧ ¬B) → A → ¬¬B.
1254	#A #B #Hnot #HA @nmk #H @(absurd (A∧¬B)) [ % [ @HA \| @H ] \| @Hnot ]
1255	qed. *)
1256
1257	lemma thingie:
1258	∀A:Prop.(A + ¬A) → (¬¬A) → A.
1259	#A #Adec #nnA cases Adec
1260	[ //
1261	\| #H @⊥ @(absurd (¬A) H nnA)
1262	]
1263	qed.
1264
1265	lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
1266	#a #b cases a cases b /2/
1267	%2 @nmk #H destruct (H)
1268	qed.
1269
1270	(* lemma incr_or_equal: ∀program:list labelled_instruction.
1271	∀policy:(Σp:jump_expansion_policy.
1272	(∀i.i ≥ \|program\| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1273	jump_in_policy program p).
1274	policy_equal program policy (jump_expansion_step program policy) ∨
1275	∃n:ℕ.n < (\|program\|) ∧ jmple
1276	(\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉))
1277	(\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)).
1278	#program #policy cases (dec_bounded_exists
1279	(λk.
1280	\snd (bvt_lookup ?? (bitvector_of_nat ? k) policy 〈0,short_jump〉) ≠
1281	\snd (bvt_lookup ?? (bitvector_of_nat ? k) (jump_expansion_step program policy) 〈0,short_jump〉))
1282	? (\|program\|))
1283	[ #H %2 elim H -H; #i #Hi
1284	cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) i (proj1 ?? Hi))
1285	[ #H @(ex_intro ?? i (conj ?? (proj1 ?? Hi) H))
1286	\| #H @⊥ @(absurd ? H (proj2 ?? Hi))
1287	]
1288	\| #H %1 whd #i #Hi @(thingie ? (dec_eq_jump_length ??)) elim H -H #H; @nmk #H2 @H
1289	@(ex_intro … i) @conj [ @Hi \| @H2 ]
1290	\| #n cases (dec_eq_jump_length (\snd (lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉))
1291	(\snd (lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)))
1292	[ #H %2 @nmk #H1 elim H1 #H2 @H2 @H
1293	\| #H %1 @H
1294	]
1295	]
1296	qed. *)
1297
1298	lemma policy_not_equal_incr: ∀program:list labelled_instruction.
1299	∀policy:(Σp:jump_expansion_policy.
1300	(∀i.i ≥ \|program\| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1301	jump_in_policy program p).
1302	¬policy_equal program policy (jump_expansion_step program policy) →
1303	∃n:ℕ.n < (\|program\|) ∧ jmple
1304	(\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉))
1305	(\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)).
1306	#program #policy #Hp
1307	cases (dec_bounded_exists (λn.jmple
1308	(\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉))
1309	(\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) ? (\|program\|))
1310	[ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
1311	\| #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) n Hn)
1312	[ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn \| @Hj ]
1313	\| #H @H
1314	]
1315	\| #n @dec_jmple
1316	]
1317	qed.
1318
1319	lemma stupid:
1320	∀program,n.
1321	eject … (jump_expansion_step program (jump_expansion_internal program n)) =
1322	eject … (jump_expansion_internal program (S n)).
1323	//
1324	qed.
1325
1326	let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
1327	on program: ℕ ≝
1328	match program with
1329	[ nil ⇒ acc
1330	\| cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) policy 〈0,short_jump〉)) with
1331	[ long_jump ⇒ measure_int t policy (acc + 2)
1332	\| medium_jump ⇒ measure_int t policy (acc + 1)
1333	\| _ ⇒ measure_int t policy acc
1334	]
1335	].
1336
1337	definition measure ≝
1338	λprogram.λpolicy.measure_int program policy 0.
1339
1340	(* lemma measure_le: ∀program.∀policy.∀x,y:ℕ.
1341	x ≤ y → measure_int program policy x ≤ measure_int program policy y.
1342	#program #policy
1343	elim program
1344	[ //
1345	\| #h #t #Hind #x #y #Hxy whd in match (measure_int ??x); whd in match (measure_int ??y);
1346	cases (\snd (lookup … (bitvector_of_nat ? (\|t\|)) policy 〈0,short_jump〉))
1347	[ @Hind @Hxy
1348	\|2,3: @Hind @monotonic_le_plus_l @Hxy
1349	]
1350	]
1351	qed. *)
1352
1353	lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
1354	measure_int program policy (x+d) = measure_int program policy x + d.
1355	#program #policy #x #d generalize in match x; -x elim d
1356	[ //
1357	\| -d; #d #Hind elim program
1358	[ //
1359	\| #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
1360	cases (\snd (lookup … (bitvector_of_nat ? (\|t\|)) policy 〈0,short_jump〉))
1361	[ normalize nodelta @Hd
1362	\|2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
1363	@Hd
1364	]
1365	]
1366	]
1367	qed.
1368
1369	lemma measure_incr_or_equal: ∀program.∀policy:Σp:jump_expansion_policy.
1370	(∀i.i ≥ \|program\| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1371	jump_in_policy program p.∀l.\|l\| ≤ \|program\| → ∀acc:ℕ.
1372	measure_int l policy acc ≤ measure_int l (jump_expansion_step program policy) acc.
1373	#program #policy #l (* lapply (le_n (\|program\|)) *) elim l -l;
1374	[ #Hp #acc normalize @le_n
1375	\| #h #t #Hind #Hp #acc
1376	cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (\|t\|) ?)
1377	[ whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?);
1378	cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) policy 〈0,short_jump〉))
1379	cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) (jump_expansion_step program policy) 〈0,short_jump〉))
1380	[1,4,5,7,8,9: #H @⊥ @H
1381	\|2,3,6: #_ normalize nodelta
1382	[1,2: @(transitive_le ? (measure_int t (jump_expansion_step program policy) acc))
1383	\|3: @(transitive_le ? (measure_int t (jump_expansion_step program policy) (acc+1)))
1384	]
1385	[1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn
1386	\|2,4,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus [ @le_n \| //]
1387	]
1388	]
1389	\| #Heq whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?);
1390	>Heq cases (\snd (lookup … (bitvector_of_nat ? (\|t\|)) ? 〈0,short_jump〉))
1391	[ normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
1392	\| normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
1393	\| normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
1394	]
1395	\| @Hp
1396	]
1397	]
1398	qed.
1399
1400	lemma measure_le: ∀program.∀policy.
1401	measure_int program policy 0 ≤ 2*\|program\|.
1402	#program #policy elim program
1403	[ normalize @le_n
1404	\| #h #t #Hind whd in match (measure_int ???);
1405	cases (\snd (lookup ?? (bitvector_of_nat ? (\|t\|)) policy 〈0,short_jump〉))
1406	[ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
1407	\|2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
1408	@le_plus [1,3: @Hind \|2,4: // ]
1409	]
1410	]
1411	qed.
1412
1413	lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
1414	#a elim a
1415	[ normalize #b //
1416	\| -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ \| -b #b normalize
1417	<plus_n_Sm <plus_n_Sm #H
1418	>(Hind b (injective_S ?? (injective_S ?? H))) // ]
1419	]
1420	qed.
1421
1422	lemma sth_not_s: ∀x.x ≠ S x.
1423	#x cases x
1424	[ // \| #y // ]
1425	qed.
1426
1427	lemma measure_full: ∀program.∀policy.
1428	measure_int program policy 0 = 2*\|program\| → ∀i.i<\|program\| →
1429	(\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,short_jump〉)) = long_jump.
1430	#program #policy elim program
1431	[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1432	\| #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*\|t\|)
1433	[ whd in match (measure_int ???) in Hm;
1434	cases (\snd (lookup … (bitvector_of_nat ? (\|t\|)) policy 〈0,short_jump〉)) in Hm;
1435	normalize nodelta
1436	[ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
1437	\| >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
1438	<(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
1439	>(commutative_plus (\|t\|) 0) <plus_O_n <minus_n_O
1440	>plus_n_Sm @le_n
1441	\| >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
1442	]
1443	\| #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
1444	[ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
1445	\| #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1446	cases (\snd (lookup … (bitvector_of_nat ? (\|t\|)) policy 〈0,short_jump〉)) in Hm;
1447	normalize nodelta
1448	[ >Hmt normalize <plus_n_O >(commutative_plus (\|t\|) (S (\|t\|)))
1449	>plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
1450	\| >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
1451	#H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
1452	\| #_ //
1453	]
1454	]]
1455	]
1456	qed.
1457
1458	lemma eq_plus_S_to_lt:
1459	∀n,m,p:ℕ.n = m + (S p) → m < n.
1460	//
1461	qed.
1462
1463	lemma measure_special: ∀program.∀policy:Σp:jump_expansion_policy.
1464	(∀i.i ≥ \|program\| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
1465	jump_in_policy program p.
1466	measure_int program policy 0 = measure_int program (jump_expansion_step program policy) 0 →
1467	policy_equal program policy (jump_expansion_step program policy).
1468	#program lapply (le_n (\|program\|)) elim program in ⊢ (?%? → ∀policy.??(?%??)(?%??) → ?%??);
1469	[ #_ #policy #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
1470	\| #h #t #Hind #Hp #policy #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
1471	[ #Hi @Hind
1472	[ @(transitive_le … Hp) //
1473	\| whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
1474	lapply (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (\|t\|) ?)
1475	[ @(lt_to_le_to_lt … (\|h::t\|)) [ // \| @Hp ]
1476	\| cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) policy 〈0,short_jump〉)) in Hm;
1477	cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) (jump_expansion_step program policy) 〈0,short_jump〉));
1478	normalize nodelta
1479	[1: #H #_ @H
1480	\|2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1481	@measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1482	\|4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 \|2,4,6: destruct (H2) ]
1483	\|5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
1484	#H #_ @(injective_plus_r … H)
1485	\|6: >measure_plus >measure_plus
1486	change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1487	#H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1488	@measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1489	\|9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
1490	#H #_ @(injective_plus_r … H)
1491	]
1492	]
1493	\| @(le_S_S_to_le … Hi)
1494	]
1495	\| #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1496	whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
1497	lapply (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (\|t\|) ?)
1498	[ @(lt_to_le_to_lt … (\|h::t\|)) [ // \| @Hp ]
1499	\| cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) policy 〈0,short_jump〉)) in Hm;
1500	cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) (jump_expansion_step program policy) 〈0,short_jump〉));
1501	normalize nodelta
1502	[1,5,9: #_ #_ //
1503	\|4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 \|2,4,6: destruct (H2) ]
1504	\|2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1505	@measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1506	\|6: >measure_plus >measure_plus
1507	change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1508	#H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1509	@measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
1510	]
1511	]
1512	]
1513	]
1514	qed.
1515
1516	lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
1517	#x cases x #l #i cases i
1518	[#id cases id
1519	[1,2,3,6,7,33,34:
1520	#x #y %2 whd in match (is_jump ?); /2 by nmk/
1521	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
1522	#x %2 whd in match (is_jump ?); /2 by nmk/
1523	\|35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
1524	\|9,10,14,15: #x %1 //
1525	\|11,12,13,16,17: #x #y %1 //
1526	]
1527	\|2,3: #x %2 /2 by nmk/
1528	\|4,5: #x %1 //
1529	\|6: #x #y %2 /2 by nmk/
1530	]
1531	qed.
1532
1533	lemma measure_zero: ∀l.∀program.
1534	\|l\| ≤ \|program\| → measure_int l (jump_expansion_internal program 0) 0 = 0.
1535	#l #program elim l (* lapply (le_n (\|program\|)) elim program in ⊢ (?%? → ?%(?%??)?); *)
1536	[ //
1537	\| #h #t #Hind #Hp whd in match (measure_int ???);
1538	cases (dec_is_jump (nth (\|t\|) ? program 〈None ?, Comment []〉)) #Hj
1539	[ >(lookup_opt_lookup_hit … (proj2 ?? (sig2 ?? (jump_expansion_start program)) (\|t\|) ? Hj) 〈0,short_jump〉)
1540	[ normalize nodelta @Hind @le_S_to_le ]
1541	@Hp
1542	\| >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (\|t\|) ?) Hj) 〈0,short_jump〉)
1543	[ normalize nodelta @Hind @le_S_to_le ]
1544	@Hp
1545	]
1546	]
1547	qed.
1548
1549	definition je_fixpoint: ∀program:list labelled_instruction.
1550	Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
1551	#program @(dp … (jump_expansion_internal program (2*\|program\|)))
1552	@(ex_intro … (2*\|program\|)) #k #Hk
1553	cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
1554	(jump_expansion_internal program (S k))) ? (2*\|program\|))
1555	[ #H elim H -H #x #Hx @pe_trans
1556	[ @(jump_expansion_internal program x)
1557	\| @pe_sym @equal_remains_equal
1558	[ @(proj2 ?? Hx)
1559	\| @(transitive_le ? (2*\|program\|))
1560	[ @le_S_S_to_le @le_S @(proj1 ?? Hx)
1561	\| @le_S_S_to_le @le_S @Hk
1562	]
1563	]
1564	\| @equal_remains_equal
1565	[ @(proj2 ?? Hx)
1566	\| @le_S_S_to_le @le_S @(proj1 ?? Hx)
1567	]
1568	]
1569	\| #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @pe_sym @equal_remains_equal
1570	[ lapply (measure_full program (jump_expansion_internal program (2*\|program\|)))
1571	#Hfull #i #Hi
1572	lapply (proj2 ?? (sig2 ?? (jump_expansion_step program (jump_expansion_internal program (2*\|program\|)))) i Hi)
1573	>(Hfull ? i Hi)
1574	[ cases (\snd (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_step program (jump_expansion_internal program (2*\|program\|))) 〈0,short_jump〉))
1575	[1,2: #H elim H #H2 [1,3: @⊥ @H2 \|2,4: destruct (H2) ]
1576	\| #_ //
1577	]
1578	\| -i @le_to_le_to_eq
1579	[ @measure_le
1580	\| lapply (le_n (2\|program\|)) elim (2\|program\|) in ⊢ (?%? → %);
1581	[ #_ >measure_zero @le_n
1582	\| #x #Hind #Hx
1583	cut (measure_int program (jump_expansion_internal program x) 0 <
1584	measure_int program (jump_expansion_internal program (S x)) 0)
1585	[ elim (le_to_or_lt_eq …
1586	(measure_incr_or_equal program (jump_expansion_internal program x) program (le_n (\|program\|)) 0))
1587	[ //
1588	\| #H @⊥ @(absurd ?? (Hfa x Hx)) @measure_special @H
1589	]
1590	\| #H lapply (Hind (le_S_to_le … Hx)) #H2 @(le_to_lt_to_lt … H) @H2
1591	]
1592	]
1593	]
1594	]
1595	\| @le_S_to_le @Hk
1596	]
1597	\| #n @dec_bounded_forall #m @dec_eq_jump_length
1598	]
1599	qed.
1600
1601	(************************************** START OF POLICY ABSTRACTION ******************)
1602
1603	definition policy_type≝ Word → jump_length.
1604
1605	definition jump_expansion': pseudo_assembly_program → policy_type ≝
1606	λprogram.λpc.
1607	let policy ≝ jump_expansion_internal (\snd program) (\|\snd program\|) in
1608	let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in
1609	j.
1610
1611	definition assembly_1_pseudoinstruction_safe ≝
1612	λprogram: pseudo_assembly_program.
1613	λjump_expansion: policy_type.
1614	λppc: Word.
1615	λpc: Word.
1616	λlookup_labels.
1617	λlookup_datalabels.
1618	λi.
1619	let expansion ≝ jump_expansion ppc in
1620	match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
1621	[ None ⇒ None ?
1622	\| Some pseudos ⇒
1623	let mapped ≝ map ? ? assembly1 pseudos in
1624	let flattened ≝ flatten ? mapped in
1625	let pc_len ≝ length ? flattened in
1626	Some ? (〈pc_len, flattened〉)
1627	].
1628
1629	definition construct_costs_safe ≝
1630	λprogram.
1631	λjump_expansion: policy_type.
1632	λpseudo_program_counter: nat.
1633	λprogram_counter: nat.
1634	λcosts: BitVectorTrie costlabel 16.
1635	λi.
1636	match i with
1637	[ Cost cost ⇒
1638	let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1639	Some ? 〈program_counter, (insert … program_counter_bv cost costs)〉
1640	\| _ ⇒
1641	let pc_bv ≝ bitvector_of_nat ? program_counter in
1642	let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
1643	let lookup_labels ≝ λx.pc_bv in
1644	let lookup_datalabels ≝ λx.zero ? in
1645	let pc_delta_assembled ≝
1646	assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
1647	lookup_labels lookup_datalabels i
1648	in
1649	match pc_delta_assembled with
1650	[ None ⇒ None ?
1651	\| Some pc_delta_assembled ⇒
1652	let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
1653	Some ? 〈pc_delta + program_counter, costs〉
1654	]
1655	].
1656
1657	(* This establishes the correspondence between pseudo program counters and
1658	program counters. It is at the heart of the proof. *)
1659	(CSC: code taken from build_maps )
1660	definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
1661	λinstr_list.
1662	λjump_expansion: policy_type.
1663	λl:list labelled_instruction.
1664	λacc.
1665	foldl …
1666	(λt,i.
1667	match t with
1668	[ None ⇒ None …
1669	\| Some ppc_pc_map ⇒
1670	let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1671	let 〈program_counter, sigma_map〉 ≝ pc_map in
1672	let 〈label, i〉 ≝ i in
1673	match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
1674	[ None ⇒ None ?
1675	\| Some pc_ignore ⇒
1676	let 〈pc,ignore〉 ≝ pc_ignore in
1677	Some … 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ]
1678	]) acc l.
1679
1680	definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) ≝
1681	λprog.
1682	λjump_expansion.
1683	sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, Stub …〉〉).
1684
1685	definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
1686	λprogram,jump_expansion,instr_list.
1687	match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
1688	[ None ⇒ None …
1689	\| Some result ⇒
1690	let 〈ppc,pc_sigma_map〉 ≝ result in
1691	let 〈pc,map〉 ≝ pc_sigma_map in
1692	Some … 〈ppc,pc〉 ].
1693
1694	definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
1695	λinstr_list,jump_expansion.
1696	match sigma0 instr_list jump_expansion with
1697	[ None ⇒ None ?
1698	\| Some result ⇒
1699	let 〈ppc,pc_sigma_map〉 ≝ result in
1700	let 〈pc, sigma_map〉 ≝ pc_sigma_map in
1701	if gtb pc (2^16) then
1702	None ?
1703	else
1704	Some ? (λx. lookup … x sigma_map (zero …)) ].
1705
1706	(* stuff about policy *)
1707
1708	definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
1709
1710	definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
1711
1712	lemma eject_policy: ∀p. policy p → policy_type.
1713	#p #pol @(eject … pol)
1714	qed.
1715
1716	coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
1717
1718	definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
1719	λp,policy.
1720	match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
1721	[ None ⇒ λabs. ⊥
1722	\| Some r ⇒ λ_.r] (sig2 … policy).
1723	cases abs /2/
1724	qed.
1725
1726	example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
1727	cases daemon.
1728	qed.
1729
1730	axiom fetch_pseudo_instruction_split:
1731	∀instr_list,ppc.
1732	∃pre,suff,lbl.
1733	(pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
1734
1735	lemma sigma00_append:
1736	∀instr_list,jump_expansion,l1,l2,acc.
1737	sigma00 instr_list jump_expansion (l1@l2) acc =
1738	sigma00 instr_list jump_expansion
1739	l2 (sigma00 instr_list jump_expansion l1 acc).
1740	whd in match sigma00; normalize nodelta;
1741	#instr_list #jump_expansion #l1 #l2 #acc @foldl_append
1742	qed.
1743
1744	lemma sigma00_strict:
1745	∀instr_list,jump_expansion,l,acc. acc = None ? →
1746	sigma00 instr_list jump_expansion l acc = None ….
1747	#instr_list #jump_expansion #l elim l
1748	[ #acc #H >H %
1749	\| #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
1750	qed.
1751
1752	lemma policy_ok_prefix_ok:
1753	∀program.∀pol:policy program.∀suffix,prefix.
1754	prefix@suffix = \snd program →
1755	sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
1756	* #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
1757	generalize in match (sig2 ?? pol); whd in prf:(???%); <prf in pol; #pol
1758	whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
1759	normalize nodelta >sigma00_append
1760	cases (sigma00 ?? prefix ?)
1761	[2: #x #_ % #abs destruct(abs)
1762	\| * #abs @⊥ @abs >sigma00_strict % ]
1763	qed.
1764
1765	lemma policy_ok_prefix_hd_ok:
1766	∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
1767	(prefix@[hd])@suffix = \snd program →
1768	Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
1769	let 〈ppc,pc_map〉 ≝ ppc_pc_map in
1770	let 〈program_counter, sigma_map〉 ≝ pc_map in
1771	let 〈label, i〉 ≝ hd in
1772	construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
1773	* #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
1774	generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
1775	(prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
1776	@pair_elim' #ppc #pc_map #EQ3 normalize nodelta
1777	@pair_elim' #pc #map #EQ4 normalize nodelta
1778	@pair_elim' #l' #i' #EQ5 normalize nodelta
1779	cases (construct_costs_safe ??????) normalize
1780	[* #abs @⊥ @abs % \| #X #_ % #abs destruct(abs)]
1781	qed.
1782
1783	definition expand_pseudo_instruction:
1784	∀program:pseudo_assembly_program.∀pol: policy program.
1785	∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
1786	lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1787	lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1788	let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
1789	pc = sigma program pol ppc →
1790	Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
1791	≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
1792	match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
1793	[ None ⇒ let dummy ≝ [ ] in dummy
1794	\| Some res ⇒ res ].
1795	[ @⊥ whd in p:(??%??);
1796	generalize in match (sig2 ?? pol); whd in ⊢ (% → ?);
1797	whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? \| _ ⇒ ?])?) → ?);
1798	generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
1799	cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
1800	#res #K
1801	cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
1802	generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
1803	cases daemon (* CSC: XXXXXXXX Ero qui
1804
1805	[3: @policy_ok_prefix_ok ]
1806	\| sigma00 program pol pre
1807
1808
1809
1810	QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
1811	fetch ppc = hd sse program = pre @ [hd] @ tl e \|pre\| = ppc
1812	per concludere construct_costs_safe ≠ None *)
1813	\| >p %]
1814	qed.
1815
1816	(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1817	definition assembly_1_pseudoinstruction':
1818	∀program:pseudo_assembly_program.∀pol: policy program.
1819	∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1820	lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1821	lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1822	\fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1823	Σres:(nat × (list Byte)).
1824	Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
1825	let 〈len,code〉 ≝ res in
1826	sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
1827	bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
1828	≝ λprogram: pseudo_assembly_program.
1829	λpol: policy program.
1830	λppc: Word.
1831	λlookup_labels.
1832	λlookup_datalabels.
1833	λpi.
1834	λprf1,prf2,prf3.
1835	match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
1836	[ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
1837	\| Some res ⇒ res ].
1838	[ @⊥ elim pi in p; [*]
1839	try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
1840	generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
1841	whd in abs:(??match % with [_ ⇒ ? \| _ ⇒ ?]?);
1842	(* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
1843	cases daemon
1844	\| % [ >p %]
1845	cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
1846	(* THIS SHOULD BE TRUE INSTEAD *)
1847	cases daemon]
1848	qed.
1849
1850	definition assembly_1_pseudoinstruction:
1851	∀program:pseudo_assembly_program.∀pol: policy program.
1852	∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1853	lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
1854	lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1855	\fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
1856	nat × (list Byte)
1857	≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
1858	assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
1859	prf2 prf3.
1860
1861	lemma assembly_1_pseudoinstruction_ok1:
1862	∀program:pseudo_assembly_program.∀pol: policy program.
1863	∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
1864	∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
1865	∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
1866	∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
1867	Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
1868	= assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
1869	#program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
1870	cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
1871	#H1 #_ @H1
1872	qed.
1873
1874	(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
1875	definition construct_costs':
1876	∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
1877	Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
1878	≝
1879	λprogram.λpol: policy program.λppc,pc,costs,i.
1880	match construct_costs_safe program pol ppc pc costs i with
1881	[ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
1882	\| Some res ⇒ res ].
1883	[ cases daemon
1884	\| >p %]
1885	qed.
1886
1887	definition construct_costs ≝
1888	λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
1889
1890	(*
1891	axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
1892	axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
1893
1894	axiom foldl_strong_step:
1895	∀A:Type[0].
1896	∀P: list A → Type[0].
1897	∀l: list A.
1898	∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
1899	∀acc: P [ ].
1900	∀Q: ∀prefix. P prefix → Prop.
1901	∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
1902	∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
1903	Q [ ] acc →
1904	Q l (foldl_strong A P l H acc).
1905	(*
1906	#A #P #l #H #acc #Q #HQ #Hacc normalize;
1907	generalize in match
1908	(foldl_strong ?
1909	(λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
1910	l ? Hacc)
1911	[3: >suffix_of_ok % \| 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
1912	[2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
1913	#K
1914
1915	generalize in match
1916	(foldl_strong ?
1917	(λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
1918	[2: @H
1919	*)
1920
1921	axiom foldl_elim:
1922	∀A:Type[0].
1923	∀B: Type[0].
1924	∀H: A → B → A.
1925	∀acc: A.
1926	∀l: list B.
1927	∀Q: A → Prop.
1928	(∀acc:A.∀b:B. Q acc → Q (H acc b)) →
1929	Q acc →
1930	Q (foldl A B H acc l).
1931	*)
1932
1933	lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1934	#A #a #b #EQ destruct //
1935	qed.
1936
1937	(*
1938	lemma tech_pc_sigma00_append_Some:
1939	∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1940	tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1941	tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1942	#program #pol #prefix #costs #label #i #ppc #pc #H
1943	whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
1944	whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
1945	generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
1946	whd in match sigma0; normalize nodelta;
1947	>foldl_step
1948	change with (? → match match sigma00 program pol prefix with [None ⇒ ? \| Some res ⇒ ?] with [ None ⇒ ? \| Some res ⇒ ? ] = ?)
1949	whd in match tech_pc_sigma00 in H; normalize nodelta in H;
1950	cases (sigma00 program pol prefix) in H ⊢ %
1951	[ whd in ⊢ (??%% → ?) #abs destruct(abs)
1952	\| * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
1953
1954	normalize nodelta; -H;
1955
1956
1957	generalize in match H; -H;
1958	generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? \| _ ⇒ ?] with [_ ⇒ ? \| _ ⇒ ?]?)
1959	[2: whd in ⊢ (??%%)
1960	XXX
1961	*)
1962
1963	axiom construct_costs_sigma:
1964	∀p.∀pol:policy p.∀ppc,pc,costs,i.
1965	bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
1966	bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
1967
1968	axiom tech_pc_sigma00_append_Some:
1969	∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
1970	tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
1971	tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
1972
1973	axiom eq_identifier_eq:
1974	∀tag: String.
1975	∀l.
1976	∀r.
1977	eq_identifier tag l r = true → l = r.
1978
1979	axiom neq_identifier_neq:
1980	∀tag: String.
1981	∀l, r: identifier tag.
1982	eq_identifier tag l r = false → (l = r → False).
1983
1984	definition build_maps:
1985	∀pseudo_program.∀pol:policy pseudo_program.
1986	Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
1987	let 〈labels, costs〉 ≝ res in
1988	∀id. occurs_exactly_once id (\snd pseudo_program) →
1989	lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
1990	λpseudo_program.
1991	λpol:policy pseudo_program.
1992	let result ≝
1993	foldl_strong
1994	(option Identifier × pseudo_instruction)
1995	(λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))).
1996	let 〈labels,ppc_pc_costs〉 ≝ res in
1997	let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
1998	let 〈pc',costs〉 ≝ pc_costs in
1999	And ( And (
2000	And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (∧)
2001	(ppc' = length … pre)) (∧ )
2002	(tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (∧)
2003	(∀id. occurs_exactly_once id pre →
2004	lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
2005	(\snd pseudo_program)
2006	(λprefix,i,tl,prf,t.
2007	let 〈labels, ppc_pc_costs〉 ≝ t in
2008	let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
2009	let 〈pc,costs〉 ≝ pc_costs in
2010	let 〈label, i'〉 ≝ i in
2011	let labels ≝
2012	match label with
2013	[ None ⇒ labels
2014	\| Some label ⇒
2015	let program_counter_bv ≝ bitvector_of_nat ? pc in
2016	add ? ? labels label program_counter_bv
2017	]
2018	in
2019	let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
2020	〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
2021	in
2022	let 〈labels, ppc_pc_costs〉 ≝ result in
2023	let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
2024	let 〈pc, costs〉 ≝ pc_costs in
2025	〈labels, costs〉.
2026	[2: whd generalize in match (sig2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
2027	generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
2028	[ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
2029	\| >append_length <IH0 normalize; -IHn1; (CSC: otherwise it diverges!) //
2030	\| >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
2031	\| #id normalize nodelta; -labels1; cases label; normalize nodelta
2032	[ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (CSC: otherwise it diverges!) //
2033	\| #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
2034	generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
2035	[ #EQ #_ <(eq_identifier_eq … EQ) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit
2036	<IH0 [@IHn1 \| <(eq_identifier_eq … EQ) in H; #H @H]
2037	\| #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: -IHn1;
2038	(Andrea:XXXX used to work /2/)@nmk #IDL lapply (sym_eq ? ? ? IDL)
2039	lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ]
2040	<(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
2041	\|3: whd % [% [%]] [>sigma_0 % \| % \| % \| #id normalize in ⊢ (% → ?); #abs @⊥ // ]
2042	\| generalize in match (sig2 … result) in ⊢ ?;
2043	normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
2044	normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
2045	qed.
2046
2047	definition assembly:
2048	∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝
2049	λp.let 〈preamble, instr_list〉 ≝ p in
2050	λpol.
2051	let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
2052	let datalabels ≝ construct_datalabels preamble in
2053	let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in
2054	let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
2055	let result ≝
2056	foldl_strong
2057	(option Identifier × pseudo_instruction)
2058	(λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
2059	let 〈pc,ppc_code〉 ≝ pc_ppc_code in
2060	let 〈ppc,code〉 ≝ ppc_code in
2061	∀ppc'.
2062	let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
2063	let 〈len,assembledi〉 ≝
2064	assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
2065	True)
2066	instr_list
2067	(λprefix,hd,tl,prf,pc_ppc_code.
2068	let 〈pc, ppc_code〉 ≝ pc_ppc_code in
2069	let 〈ppc, code〉 ≝ ppc_code in
2070	let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
2071	let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
2072	let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
2073	〈new_pc, 〈new_ppc, (code @ program)〉〉)
2074	〈(zero ?), 〈(zero ?), [ ]〉〉
2075	in
2076	〈\snd (\snd result), costs〉.
2077	[2,5: %
2078	\|*: cases daemon ]
2079	qed.
2080
2081	definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
2082	λ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