Context Navigation

Policy.ma @ 1892

Last change on this file since 1892 was 1886, checked in by boender, 9 years ago
improvements for disambiguation and quick(er) typing
File size: 77.2 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	include "utilities/extralib.ma".
8	include "ASM/Assembly.ma".
9
10	(* Internal types *)
11
12	(* label_map: identifier ↦ 〈instruction number, address〉 *)
13	definition label_map ≝ identifier_map ASMTag (ℕ × ℕ).
14
15	(* jump_expansion_policy: instruction number ↦ 〈pc, [addr, jump_length]〉 *)
16	definition jump_expansion_policy ≝ ℕ × (BitVectorTrie (ℕ × ℕ × jump_length) 16).
17
18	(* The different properties that we want/need to prove at some point *)
19	(* Anything that's not in the program doesn't end up in the policy *)
20	definition out_of_program_none: list labelled_instruction → jump_expansion_policy → Prop ≝
21	λprefix.λpolicy.
22	∀i.i ≥ \|prefix\| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) (\snd policy) = None ?.
23
24	(* If instruction i is a jump, then there will be something in the policy at
25	* position i *)
26	definition is_jump' ≝
27	λx:preinstruction Identifier.
28	match x with
29	[ JC _ ⇒ True
30	\| JNC _ ⇒ True
31	\| JZ _ ⇒ True
32	\| JNZ _ ⇒ True
33	\| JB _ _ ⇒ True
34	\| JNB _ _ ⇒ True
35	\| JBC _ _ ⇒ True
36	\| CJNE _ _ ⇒ True
37	\| DJNZ _ _ ⇒ True
38	\| _ ⇒ False
39	].
40
41	definition is_jump ≝
42	λx:labelled_instruction.
43	let 〈label,instr〉 ≝ x in
44	match instr with
45	[ Instruction i ⇒ is_jump' i
46	\| Call _ ⇒ True
47	\| Jmp _ ⇒ True
48	\| _ ⇒ False
49	].
50
51	definition jump_in_policy: list labelled_instruction → jump_expansion_policy → Prop ≝
52	λprefix.λpolicy.
53	∀i:ℕ.i < \|prefix\| →
54	iff (is_jump (nth i ? prefix 〈None ?, Comment []〉))
55	(∃p:ℕ.∃a:ℕ.∃j:jump_length.
56	lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈p,a,j〉).
57
58	definition labels_okay: label_map → jump_expansion_policy → Prop ≝
59	λlabels.λpolicy.
60	bvt_forall ?? (\snd policy) (λn.λx.
61	let 〈pc,addr_nat,j〉 ≝ x in
62	∃id:Identifier.\snd (lookup_def … labels id 〈0,pc〉) = addr_nat
63	).
64
65	(* Between two policies, jumps cannot decrease *)
66	definition jmple: jump_length → jump_length → Prop ≝
67	λj1.λj2.
68	match j1 with
69	[ short_jump ⇒
70	match j2 with
71	[ short_jump ⇒ False
72	\| _ ⇒ True
73	]
74	\| medium_jump ⇒
75	match j2 with
76	[ long_jump ⇒ True
77	\| _ ⇒ False
78	]
79	\| long_jump ⇒ False
80	].
81
82	definition jmpleq: jump_length → jump_length → Prop ≝
83	λj1.λj2.jmple j1 j2 ∨ j1 = j2.
84
85	definition policy_increase: list labelled_instruction → jump_expansion_policy →
86	jump_expansion_policy → Prop ≝
87	λprogram.λop.λp.
88	(∀i:ℕ.i < \|program\| →
89	let 〈pc1,i1,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) (\snd op) 〈0,0,short_jump〉 in
90	let 〈pc2,i2,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) (\snd p) 〈0,0,short_jump〉 in
91	jmpleq oj j
92	).
93
94	(* Policy safety *)
95	definition policy_safe: jump_expansion_policy → Prop ≝
96	λpolicy.
97	bvt_forall ?? (\snd policy) (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
98	match jmp_len with
99	[ short_jump ⇒ if leb pc_nat addr_nat
100	then le (addr_nat - pc_nat) 126
101	else le (pc_nat - addr_nat) 129
102	\| medium_jump ⇒
103	let addr ≝ bitvector_of_nat 16 addr_nat in
104	let pc ≝ bitvector_of_nat 16 pc_nat in
105	let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
106	let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
107	eq_bv 5 fst_5_addr fst_5_pc = true
108	\| long_jump ⇒ True
109	]
110	).
111
112	(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
113	definition max_length: jump_length → jump_length → jump_length ≝
114	λj1.λj2.
115	match j1 with
116	[ long_jump ⇒ long_jump
117	\| medium_jump ⇒
118	match j2 with
119	[ medium_jump ⇒ medium_jump
120	\| _ ⇒ long_jump
121	]
122	\| short_jump ⇒
123	match j2 with
124	[ short_jump ⇒ short_jump
125	\| _ ⇒ long_jump
126	]
127	].
128
129	lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
130	#x #y cases x cases y /3 by inl, inr, nmk, I/
131	qed.
132
133	lemma jmpleq_max_length: ∀ol,nl.
134	jmpleq ol (max_length ol nl).
135	#ol #nl cases ol cases nl
136	/2 by or_introl, or_intror, I/
137	qed.
138
139	lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
140	#a #b cases a cases b /2/
141	%2 @nmk #H destruct (H)
142	qed.
143
144	(* Labels *)
145	definition is_label ≝
146	λx:labelled_instruction.λl:Identifier.
147	let 〈lbl,instr〉 ≝ x in
148	match lbl with
149	[ Some l' ⇒ l' = l
150	\| _ ⇒ False
151	].
152
153	lemma label_does_not_occur:
154	∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier.
155	is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false.
156	#i #p #l generalize in match i; elim p
157	[ #i >nth_nil #H @⊥ @H
158	\| #h #t #IH #i cases i -i
159	[ cases h #hi #hp cases hi
160	[ normalize #H @⊥ @H
161	\| #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????);
162	whd in Heq; >Heq
163	>eq_identifier_refl / by refl/
164	]
165	\| #i #H whd in match (does_not_occur ????);
166	whd in match (instruction_matches_identifier ????);
167	cases h #hi #hp cases hi normalize nodelta
168	[ @(IH i) @H
169	\| #l' @eq_identifier_elim
170	[ normalize / by /
171	\| normalize #_ @(IH i) @H
172	]
173	]
174	]
175	]
176	qed.
177
178	definition expand_relative_jump_internal_unsafe:
179	jump_length → ([[relative]] → preinstruction [[relative]]) → option (list instruction) ≝
180	λjmp_len:jump_length.λi.
181	match jmp_len with
182	[ short_jump ⇒ Some ? [ RealInstruction (i (RELATIVE (zero 8))) ]
183	\| medium_jump ⇒ None …
184	\| long_jump ⇒ Some ?
185	[ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
186	SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
187	LJMP (ADDR16 (zero 16))
188	]
189	].
190	@I
191	qed.
192
193	definition expand_relative_jump_unsafe:
194	jump_length → preinstruction Identifier → option (list instruction) ≝
195	λjmp_len:jump_length.λi.
196	match i with
197	[ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?)
198	\| JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?)
199	\| JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr)
200	\| JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?)
201	\| JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?)
202	\| JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr)
203	\| JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr)
204	\| CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr)
205	\| DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr)
206	\| ADD arg1 arg2 ⇒ Some … [ ADD ? arg1 arg2 ]
207	\| ADDC arg1 arg2 ⇒ Some … [ ADDC ? arg1 arg2 ]
208	\| SUBB arg1 arg2 ⇒ Some … [ SUBB ? arg1 arg2 ]
209	\| INC arg ⇒ Some … [ INC ? arg ]
210	\| DEC arg ⇒ Some … [ DEC ? arg ]
211	\| MUL arg1 arg2 ⇒ Some … [ MUL ? arg1 arg2 ]
212	\| DIV arg1 arg2 ⇒ Some … [ DIV ? arg1 arg2 ]
213	\| DA arg ⇒ Some … [ DA ? arg ]
214	\| ANL arg ⇒ Some … [ ANL ? arg ]
215	\| ORL arg ⇒ Some … [ ORL ? arg ]
216	\| XRL arg ⇒ Some … [ XRL ? arg ]
217	\| CLR arg ⇒ Some … [ CLR ? arg ]
218	\| CPL arg ⇒ Some … [ CPL ? arg ]
219	\| RL arg ⇒ Some … [ RL ? arg ]
220	\| RR arg ⇒ Some … [ RR ? arg ]
221	\| RLC arg ⇒ Some … [ RLC ? arg ]
222	\| RRC arg ⇒ Some … [ RRC ? arg ]
223	\| SWAP arg ⇒ Some … [ SWAP ? arg ]
224	\| MOV arg ⇒ Some … [ MOV ? arg ]
225	\| MOVX arg ⇒ Some … [ MOVX ? arg ]
226	\| SETB arg ⇒ Some … [ SETB ? arg ]
227	\| PUSH arg ⇒ Some … [ PUSH ? arg ]
228	\| POP arg ⇒ Some … [ POP ? arg ]
229	\| XCH arg1 arg2 ⇒ Some … [ XCH ? arg1 arg2 ]
230	\| XCHD arg1 arg2 ⇒ Some … [ XCHD ? arg1 arg2 ]
231	\| RET ⇒ Some … [ RET ? ]
232	\| RETI ⇒ Some … [ RETI ? ]
233	\| NOP ⇒ Some … [ RealInstruction (NOP ?) ]
234	].
235
236	definition expand_pseudo_instruction_unsafe:
237	jump_length → pseudo_instruction → option (list instruction) ≝
238	λjmp_len.
239	λi.
240	match i with
241	[ Cost cost ⇒ Some ? [ ]
242	\| Comment comment ⇒ Some ? [ ]
243	\| Call call ⇒
244	match jmp_len with
245	[ short_jump ⇒ None ?
246	\| medium_jump ⇒ Some ? [ ACALL (ADDR11 (zero 11)) ]
247	\| long_jump ⇒ Some ? [ LCALL (ADDR16 (zero 16)) ]
248	]
249	\| Mov d trgt ⇒
250	Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
251	\| Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
252	\| Jmp jmp ⇒
253	match jmp_len with
254	[ short_jump ⇒ Some ? [ SJMP (RELATIVE (zero 8)) ]
255	\| medium_jump ⇒ Some ? ([ AJMP (ADDR11 (zero 11)) ])
256	\| long_jump ⇒ Some ? [ LJMP (ADDR16 (zero 16)) ]
257	]
258	].
259	@I
260	qed.
261
262	definition instruction_size: (* ℕ → *) jump_length → pseudo_instruction → ℕ ≝
263	λjmp_len.λinstr.
264	let ilist ≝ expand_pseudo_instruction_unsafe jmp_len instr in
265	let bv: list (BitVector 8) ≝ match ilist with
266	[ None ⇒ (* this shouldn't happen *) [ ]
267	\| Some l ⇒ flatten … (map … assembly1 l)
268	] in
269	\|bv\|.
270
271	definition policy_isize_sum ≝
272	λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
273	(\fst policy) = foldl_strong (option Identifier × pseudo_instruction)
274	(λacc.ℕ)
275	prefix
276	(λhd.λx.λtl.λp.λacc.
277	let 〈i1,i2,jl〉 ≝ bvt_lookup … (bitvector_of_nat ? (\|hd\|)) (\snd policy) 〈0,0,short_jump〉 in
278	acc + (instruction_size jl (\snd x)))
279	0.
280
281	(* The function that creates the label-to-address map *)
282	definition create_label_map: ∀program:list labelled_instruction.
283	∀policy:jump_expansion_policy.
284	(Σlabels:label_map.
285	∀i:ℕ.lt i (\|program\|) →
286	∀l.occurs_exactly_once ?? l program →
287	is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
288	∃a.lookup … labels l = Some ? 〈i,a〉
289	) ≝
290	λprogram.λpolicy.
291	let 〈final_pc, final_labels〉 ≝
292	foldl_strong (option Identifier × pseudo_instruction)
293	(λprefix.ℕ × (Σlabels.
294	∀i:ℕ.lt i (\|prefix\|) →
295	∀l.occurs_exactly_once ?? l prefix →
296	is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
297	∃a.lookup … labels l = Some ? 〈i,a〉)
298	)
299	program
300	(λprefix.λx.λtl.λprf.λacc.
301	let 〈pc,labels〉 ≝ acc in
302	let 〈label,instr〉 ≝ x in
303	let new_labels ≝
304	match label with
305	[ None ⇒ labels
306	\| Some l ⇒ add ? (ℕ×ℕ) labels l 〈\|prefix\|, pc〉
307	] in
308	let 〈i1,i2,jmp_len〉 ≝
309	bvt_lookup ?? (bitvector_of_nat 16 (\|prefix\|)) (\snd policy) 〈0,0,short_jump〉 in
310	〈pc + (instruction_size jmp_len instr), new_labels〉
311	) 〈0, empty_map …〉 in
312	final_labels.
313	[#i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
314	[ #Hi #l normalize nodelta; cases label normalize nodelta
315	[ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
316	lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr
317	% [ @addr \| @Haddr ]
318	\| #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) -Hocc;
319	@eq_identifier_elim #Heq #Hocc
320	[ normalize in Hocc;
321	>(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl
322	@⊥ @(absurd … Hocc)
323	\| normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
324	[ #addr #Haddr % [ @addr \| <Haddr @lookup_add_miss /2/ ]
325	\| >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; / by /
326	]
327	]
328	>(label_does_not_occur i … Hl) normalize nodelta @nmk / by /
329	]
330	\| #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
331	[ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
332	[ normalize nodelta #H @⊥ @H
333	\| #l' normalize nodelta #Heq % [ @pc \| <Heq normalize nodelta @lookup_add_hit ]
334	]
335	\| @le_n
336	]
337	]
338	\| #i #Hi #l #Hl @⊥ @Hl
339	]
340	qed.
341
342	definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
343	λlabels.λpc.λlbl.
344	let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
345	if leb pc addr (* forward jump *)
346	then if leb (addr - pc) 126
347	then 〈addr, short_jump〉
348	else 〈addr, long_jump〉
349	else if leb (pc - addr) 129
350	then 〈addr, short_jump〉
351	else 〈addr, long_jump〉.
352
353	definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
354	λlabels.λpc_nat.λlbl.
355	let pc ≝ bitvector_of_nat 16 pc_nat in
356	let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
357	let addr ≝ bitvector_of_nat 16 addr_nat in
358	let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
359	let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
360	if eq_bv ? fst_5_addr fst_5_pc
361	then 〈addr_nat, medium_jump〉
362	else 〈addr_nat, long_jump〉.
363
364	definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
365	λlabels.λpc.λlbl.
366	let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
367	if leb pc addr
368	then if leb (addr - pc) 126
369	then 〈addr, short_jump〉
370	else select_call_length labels pc lbl
371	else if leb (pc - addr) 129
372	then 〈addr, short_jump〉
373	else select_call_length labels pc lbl.
374
375	definition jump_expansion_step_instruction: label_map → ℕ →
376	preinstruction Identifier → option (ℕ × jump_length) ≝
377	λlabels.λpc.λi.
378	match i with
379	[ JC j ⇒ Some ? (select_reljump_length labels pc j)
380	\| JNC j ⇒ Some ? (select_reljump_length labels pc j)
381	\| JZ j ⇒ Some ? (select_reljump_length labels pc j)
382	\| JNZ j ⇒ Some ? (select_reljump_length labels pc j)
383	\| JB _ j ⇒ Some ? (select_reljump_length labels pc j)
384	\| JBC _ j ⇒ Some ? (select_reljump_length labels pc j)
385	\| JNB _ j ⇒ Some ? (select_reljump_length labels pc j)
386	\| CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
387	\| DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
388	\| _ ⇒ None ?
389	].
390
391	lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
392	#x cases x #l #i cases i
393	[#id cases id
394	[1,2,3,6,7,33,34:
395	#x #y %2 whd in match (is_jump ?); /2 by nmk/
396	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
397	#x %2 whd in match (is_jump ?); /2 by nmk/
398	\|35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
399	\|9,10,14,15: #x %1 / by I/
400	\|11,12,13,16,17: #x #y %1 / by I/
401	]
402	\|2,3: #x %2 /2 by nmk/
403	\|4,5: #x %1 / by I/
404	\|6: #x #y %2 /2 by nmk/
405	]
406	qed.
407
408	lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
409	∀policy:(Σp:jump_expansion_policy.
410	out_of_program_none prefix p ∧ jump_in_policy prefix p).
411	∀i:ℕ.i < \|prefix\| →
412	iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
413	(lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = None ?).
414	#prefix #policy #i #Hi @conj
415	[ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) (\snd policy)))
416	cases (lookup_opt … (bitvector_of_nat 16 i) (\snd policy)) in ⊢ (???% → ?);
417	[ #H @H
418	\| #x cases x -x #x cases x -x #x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
419	@(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
420	]
421	\| #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
422	#H elim H -H; #x #H elim H -H; #y #H elim H -H #z #H >H in Hnone; #abs destruct (abs)
423	]
424	qed.
425
426	(* these two obviously belong somewhere else *)
427	lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2.
428	s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2).
429	#A #P #s1 #s2 / by /
430	qed.
431
432	lemma Some_eq:
433	∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.
434	#T #x #y #H @option_destruct_Some @H
435	qed.
436
437	(* The first step of the jump expansion: everything to short.
438	* The third condition of the dependent type implies jump_in_policy;
439	* I've left it in for convenience of type-checking. *)
440	definition jump_expansion_start:
441	∀program:(Σl:list labelled_instruction.\|l\| < 2^16).
442	Σpolicy:jump_expansion_policy.
443	And (And (out_of_program_none (pi1 ?? program) policy)
444	(jump_in_policy (pi1 ?? program) policy))
445	(∀i.i < \|pi1 ?? program\| → is_jump (nth i ? (pi1 ?? program) 〈None ?, Comment []〉) →
446	lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉) ≝
447	λprogram.
448	foldl_strong (option Identifier × pseudo_instruction)
449	(λprefix.Σpolicy:jump_expansion_policy.
450	And (And (out_of_program_none prefix policy)
451	(jump_in_policy prefix policy))
452	(∀i.i < \|prefix\| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
453	lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉))
454	program
455	(λprefix.λx.λtl.λprf.λp.
456	let 〈pc,policy〉 ≝ p in
457	let 〈label,instr〉 ≝ x in
458	〈pc + instruction_size short_jump instr,match instr with
459	[ Instruction i ⇒ match i with
460	[ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
461	\| JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
462	\| JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
463	\| JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
464	\| JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
465	\| JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
466	\| JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
467	\| CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
468	\| DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
469	\| _ ⇒ policy
470	]
471	\| Call c ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
472	\| Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (\|prefix\|)) 〈0,0,short_jump〉 policy
473	\| _ ⇒ policy
474	]〉
475	) 〈0, Stub ? ?〉.
476	[ @conj
477	[ @conj
478	#i >append_length <commutative_plus #Hi normalize in Hi;
479	[ #Hi2 cases (le_to_or_lt_eq … Hi) -Hi #Hi
480	cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi cases pi
481	[1,7: #id cases id normalize nodelta
482	[1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
483	[1,2,3,6,7,24,25: #x #y
484	\|4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
485	@(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
486	\|38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74:
487	[1,2,3,6,7,24,25: #x #y
488	\|4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
489	<Hi @(proj1 ?? (proj1 ?? Hp) (S (\|prefix\|)) (le_S ?? (le_n (\|prefix\|))) ?)
490	>Hi @Hi2
491	\|9,10,11,12,13,14,15,16,17:
492	[1,2,6,7: #x \|3,4,5,8,9: #x #id] >lookup_opt_insert_miss
493	[2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
494	[1,4,7,10,13,16,19,22,25: @Hi2
495	\|2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) @le_S_to_le @Hi
496	\|3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq @le_S_to_le @Hi
497	]
498	\|1,3,5,7,9,11,13,15,17:
499	@(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
500	]
501	\|46,47,48,49,50,51,52,53,54:
502	[1,2,6,7: #x \|3,4,5,8,9: #x #id] >lookup_opt_insert_miss
503	[2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
504	[1,4,7,10,13,16,19,22,25: @Hi2
505	\|2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) <Hi @le_n
506	\|3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq <Hi @le_n
507	]
508	\|1,3,5,7,9,11,13,15,17:
509	@(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
510	]
511	]
512	\|2,3,6,8,9,12: [3,6: #w] #z normalize nodelta
513	[1,3,4: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
514	\|2,5,6:
515	<Hi @(proj1 ?? (proj1 ?? Hp) (S (\|prefix\|)) (le_S ?? (le_n (\|prefix\|))) ?)
516	>Hi @Hi2
517	]
518	\|4,5,10,11: #dst normalize nodelta >lookup_opt_insert_miss
519	[2,4,6,8: @bitvector_of_nat_abs
520	[1,4,7,10: @Hi2
521	\|2,5: @(transitive_lt … Hi2) @le_S_to_le @Hi
522	\|8,11: @(transitive_lt … Hi2) <Hi @le_n
523	\|3,6: @sym_neq @lt_to_not_eq @le_S_to_le @Hi
524	\|9,12: @sym_neq @lt_to_not_eq <Hi @le_n
525	]
526	\|1,3: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
527	\|5,7: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
528	]
529	]
530	\| cases (le_to_or_lt_eq … Hi) -Hi #Hi
531	[ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) @conj
532	[ #Hj @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?)))
533	cases p -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
534	[1: #pi cases pi normalize nodelta
535	[1,2,3,6,7,33,34: #x #y
536	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x
537	\|9,10,11,12,13,14,15,16,17:
538	[1,2,6,7: #x \| 3,4,5,8,9: #x #id] >lookup_opt_insert_miss
539	[2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
540	[1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
541	>append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
542	@le_S_S_to_le @le_plus_n_r
543	\|2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
544	>append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
545	\|3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
546	]
547	]
548	]
549	\|2,3: #x
550	\|4,5: #id >lookup_opt_insert_miss
551	[2,4: @bitvector_of_nat_abs
552	[1,4: @(transitive_lt … (pi2 ?? program)) >prf
553	>append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
554	@le_S_S_to_le @le_plus_n_r
555	\|2,5: @(transitive_lt … (pi2 ?? program)) >prf
556	>append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
557	\|3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
558	]
559	]
560	\|6: #x #id
561	]
562	@((proj2 ?? Hp) i (le_S_S_to_le … Hi) Hj)
563	\| #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i ?))
564	[ @(le_S_S_to_le … Hi)
565	\| cases p in H; -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
566	[1: #id cases id
567	[1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
568	[1,2,3,6,7,24,25: #x #y
569	\|4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
570	normalize nodelta / by /
571	\|9,10,11,12,13,14,15,16,17: [1,2,6,7: #x \|3,4,5,8,9: #x #id]
572	normalize nodelta >lookup_opt_insert_miss
573	[1,3,5,7,9,11,13,15,17: / by /
574	\|2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
575	[1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
576	>append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
577	@le_S_S_to_le @le_plus_n_r
578	\|2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
579	>append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
580	\|3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
581	]
582	]
583	]
584	\|2,3: #x / by /
585	\|4,5: #id >lookup_opt_insert_miss
586	[2,4: @bitvector_of_nat_abs
587	[1,4: @(transitive_lt … (pi2 ?? program)) >prf
588	>append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
589	@le_S_S_to_le @le_plus_n_r
590	\|2,5: @(transitive_lt … (pi2 ?? program)) >prf
591	>append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
592	\|3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
593	]
594	\|1,3: / by /
595	]
596	\|6: #x #id / by /
597	]
598	]
599	]
600	\| >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (\|prefix\|)))
601	<minus_n_n whd in match (nth ????);
602	cases x #l #ins cases ins
603	[1: #pi cases pi
604	[1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
605	[1,2,3,6,7,24,25: #x #y
606	\|4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
607	@conj
608	[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:
609	#H @⊥ @H
610	\|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:
611	cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p #H elim H -H #a #H elim H -H #j
612	normalize nodelta >(proj1 ?? (proj1 ?? Hp) (\|prefix\|) (le_n (\|prefix\|)) ?)
613	[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:
614	#H destruct (H)
615	\|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:
616	@(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
617	@le_S_S_to_le @le_plus_n_r
618	]
619	]
620	\|9,10,11,12,13,14,15,16,17: [1,2,6,7: #x \| 3,4,5,8,9: #x #id]
621	@conj
622	[1,3,5,7,9,11,13,15,17:
623	#_ @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?)))
624	cases p -p #p cases p -p #pc #pol #Hp @lookup_opt_insert_hit
625	\|2,4,6,8,10,12,14,16,18:
626	#_ / by I/
627	]
628	]
629	\|2,3,6: #x [3: #id] @conj
630	[1,3,5: #H @⊥ @H
631	\|2,4,6:
632	cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p #H elim H -H #a #H elim H -H #j
633	normalize nodelta >(proj1 ?? (proj1 ?? Hp) (\|prefix\|) (le_n (\|prefix\|)) ?)
634	[1,3,5: #H destruct (H)
635	\|2,4,6: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
636	@le_S_S_to_le @le_plus_n_r
637	]
638	]
639	\|4,5: #x @conj
640	[1,3: #_ @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?)))
641	cases p -p #p cases p -p #pc #pol #Hp @lookup_opt_insert_hit
642	\|2,4: #_ / by I/
643	]
644	]
645	]
646	]
647	\| #i >append_length <commutative_plus #Hi normalize in Hi;
648	elim (le_to_or_lt_eq … Hi) -Hi #Hi
649	[ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #H
650	cases p -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
651	[1: #pi cases pi
652	[1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
653	[1,2,3,6,7,24,25: #x #y
654	\|4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
655	normalize nodelta
656	@((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
657	\|9,10,11,12,13,14,15,16,17: [1,2,6,7: #x \| 3,4,5,8,9: #x #id]
658	normalize nodelta >lookup_opt_insert_miss
659	[1,3,5,7,9,11,13,15,17: @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
660	\|2,4,6,8,10,12,14,16,18,20: @bitvector_of_nat_abs
661	[1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
662	>append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
663	@le_S_S_to_le @le_plus_n_r
664	\|2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
665	>append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
666	\|3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
667	]
668	]
669	]
670	\|2,3,6: #x [3: #id]
671	normalize nodelta @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
672	\|4,5: #x >lookup_opt_insert_miss
673	[1,3: @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
674	\|2,4: @bitvector_of_nat_abs
675	[1,4: @(transitive_lt … (pi2 ?? program)) >prf
676	>append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
677	@le_S_S_to_le @le_plus_n_r
678	\|2,5: @(transitive_lt … (pi2 ?? program)) >prf
679	>append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
680	\|3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
681	]
682	]
683	]
684	\| >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (\|prefix\|)))
685	<minus_n_n whd in match (nth ????); cases x #l #ins cases ins
686	[1: #pi cases pi
687	[1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
688	[1,2,3,6,7,24,25: #x #y
689	\|4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
690	#H @⊥ @H
691	\|9,10,11,12,13,14,15,16,17: [1,2,6,7: #x \| 3,4,5,8,9: #x #id]
692	#_ cases p -p #p cases p -p #pc #pol #Hp >lookup_opt_insert_hit / by /
693	]
694	\|2,3,6: #x [3: #id] #H @⊥ @H
695	\|4,5: #id #_ cases p -p #p cases p -p #pc #pol #Hp >lookup_opt_insert_hit / by /
696	]
697	]
698	]
699	\| @conj
700	[ @conj
701	[ #i #_ #Hi2 / by refl/
702	\| #i #_ @conj
703	[ >nth_nil #H @⊥ @H
704	\| #H elim H -H #p #H elim H -H #a #H elim H -H #j #H normalize in H; destruct (H)
705	]
706	]
707	\| #i #Hi >nth_nil #H @⊥ @H
708	]
709	]
710	qed.
711
712	definition policy_equal_int ≝
713	λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
714	∀n:ℕ.n < \|program\| →
715	let 〈pc1,i1,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,0,short_jump〉 in
716	let 〈pc2,i2,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,0,short_jump〉 in
717	j1 = j2.
718
719	definition nec_plus_ultra ≝
720	λprogram:list labelled_instruction.λp:jump_expansion_policy.
721	¬(∀i.i < \|program\| → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump).
722
723	lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
724	#a #b / by refl/
725	qed.
726
727	(*lemma foldl_strong_eq:
728	∀A: Type[0].
729	∀P: list A → Type[0].
730	∀l: list A.
731	∀H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
732	∀acc: P [ ].
733	foldl_strong_internal A P l H [ ] l acc (refl …).*)
734
735
736	(* One step in the search for a jump expansion fixpoint. *)
737	definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.\|l\| < 2^16).
738	∀labels:(Σlm:label_map.∀i:ℕ.lt i (\|pi1 ?? program\|) →
739	∀l.occurs_exactly_once ?? l (pi1 ?? program) →
740	is_label (nth i ? (pi1 ?? program) 〈None ?, Comment [ ]〉) l →
741	∃a.lookup … lm l = Some ? 〈i,a〉).
742	∀old_policy:(Σpolicy:jump_expansion_policy.
743	out_of_program_none (pi1 ?? program) policy ∧
744	jump_in_policy (pi1 ?? program) policy ∧ (\fst policy < 2^16) ∧
745	policy_isize_sum (pi1 ?? program) policy).
746	(Σx:bool × (option jump_expansion_policy).
747	let 〈ch,y〉 ≝ x in
748	match y with
749	[ None ⇒ nec_plus_ultra program old_policy
750	\| Some p ⇒ out_of_program_none (pi1 ?? program) p ∧ labels_okay labels p ∧
751	jump_in_policy (pi1 ?? program) p ∧
752	policy_increase (pi1 ?? program) old_policy p ∧ policy_safe p ∧
753	(ch = false → policy_equal_int (pi1 ?? program) old_policy p) ∧
754	policy_isize_sum (pi1 ?? program) p ∧ \fst p < 2^16
755	])
756	≝
757	λprogram.λlabels.λold_policy.
758	let 〈final_changed, final_policy〉 ≝
759	foldl_strong (option Identifier × pseudo_instruction)
760	(λprefix.Σx:bool × jump_expansion_policy.
761	let 〈changed,policy〉 ≝ x in
762	out_of_program_none prefix policy ∧ labels_okay labels policy ∧
763	jump_in_policy prefix policy ∧
764	policy_increase prefix old_policy policy ∧
765	policy_safe policy ∧
766	(changed = false → policy_equal_int prefix old_policy policy) ∧
767	policy_isize_sum prefix policy)
768	program
769	(λprefix.λx.λtl.λprf.λacc.
770	let 〈changed, pol〉 ≝ acc in
771	(* let 〈pc,pol〉 ≝ p in *)
772	let 〈label,instr〉 ≝ x in
773	let add_instr ≝
774	match instr with
775	[ Instruction i ⇒ jump_expansion_step_instruction labels (\fst pol) i
776	\| Call c ⇒ Some ? (select_call_length labels (\fst pol) c)
777	\| Jmp j ⇒ Some ? (select_jump_length labels (\fst pol) j)
778	\| _ ⇒ None ?
779	] in
780	let old_length ≝ \snd (bvt_lookup … (bitvector_of_nat 16 (\|prefix\|)) (\snd old_policy) 〈0,0,short_jump〉) in
781	match add_instr with
782	[ None ⇒ (* i.e. it's not a jump *)
783	let isize ≝ instruction_size short_jump instr in
784	〈changed, 〈(\fst pol) + isize, (\snd pol)〉〉
785	\| Some z ⇒ let 〈addr,ai〉 ≝ z in
786	let new_length ≝ max_length old_length ai in
787	let isize ≝ instruction_size new_length instr in
788	〈match dec_eq_jump_length new_length old_length with
789	[ inl _ ⇒ changed
790	\| inr _ ⇒ true], 〈(\fst pol) + isize,
791	insert … (bitvector_of_nat 16 (\|prefix\|)) 〈(\fst pol), addr, new_length〉 (\snd pol)〉〉
792	]
793	) 〈false, 〈0, Stub ? ?〉〉 in
794	if geb (\fst final_policy) 2^16 then
795	〈final_changed,None ?〉
796	else
797	〈final_changed,Some ? final_policy〉.
798	[ @pair_elim #fch #x #Heq <(pair_eq2 ?????? Heq) normalize nodelta
799	@nmk #Hfull lapply p generalize in match (foldl_strong ?????); * #x #H #H2
800	>H2 in H; normalize nodelta -H2 -x #H
801	@(absurd ((\fst final_policy) ≥ 2^16))
802	[ @leb_true_to_le <geb_to_leb @p1
803	\| @lt_to_not_le @(le_to_lt_to_lt … (proj2 ?? (proj1 ?? (pi2 ?? old_policy))))
804	>(proj2 ?? H) >(proj2 ?? (pi2 ?? old_policy)) cases daemon (* XXX *)
805	]
806	\| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
807	>H2 in H; normalize nodelta #H @conj
808	[ @H
809	\| @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
810	]
811	\| lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy;
812	cases (dec_eq_jump_length new_length old_length) #Hlength normalize nodelta
813	@conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj
814	[1,3: (* out_of_policy_none *)
815	#i >append_length <commutative_plus #Hi normalize in Hi;
816	#Hi2 >lookup_opt_insert_miss
817	[1,3: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi)) @Hi2
818	\|2,4: >eq_bv_sym @bitvector_of_nat_abs
819	[1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
820	@le_S_S @le_plus_n_r
821	\|2,5: @Hi2
822	\|3,6: @lt_to_not_eq @Hi
823	]
824	]
825	\|2,4: (* labels_okay *)
826	@lookup_forall #i cases i -i #i cases i -i #p #a #j #n #Hl
827	elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
828	[1,3: elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? n Hl)
829	#i #Hi @(ex_intro ?? i Hi)
830	\|2,4: normalize nodelta normalize nodelta in p2; cases instr in p2;
831	[2,3,8,9: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
832	\|6,12: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
833	\|1,7: #pi cases pi
834	[35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
835	\|1,2,3,6,7,33,34,38,39,40,43,44,70,71:
836	#x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
837	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69:
838	#x #abs normalize in abs;lapply (jmeq_to_eq ??? abs) #H destruct (H)
839	\|9,10,14,15,46,47,51,52:
840	#id normalize nodelta whd in match (jump_expansion_step_instruction ???);
841	whd in match (select_reljump_length ???); >p3
842	lapply (refl ? (lookup_def ?? (pi1 ?? labels) id 〈0,\fst pol〉))
843	cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2
844	normalize nodelta #H
845	>(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
846	>(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
847	cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
848	[1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
849	\|2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
850	]
851	#Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
852	<(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
853	\|11,12,13,16,17,48,49,50,53,54:
854	#x #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
855	whd in match (select_reljump_length ???); >p3
856	lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉))
857	cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2
858	normalize nodelta #H
859	>(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
860	>(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
861	cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
862	[1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
863	\|2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
864	]
865	#Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
866	<(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
867	]
868	\|4,5,10,11: #id normalize nodelta whd in match (select_jump_length ???);
869	whd in match (select_call_length ???); >p3
870	lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉))
871	cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2
872	normalize nodelta #H
873	[1,3: cases (leb (\fst pol) q2)
874	[1,3: cases (leb (q2-\fst pol) 126) \|2,4: cases (leb (\fst pol-q2) 129) ]
875	[1,3,5,7: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H;
876	#Hli @(ex_intro ?? id) lapply (proj2 ?? Hl)
877	#H >(pair_eq1 ?????? (pair_eq1 ?????? H))
878	>(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl]
879	]
880	cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2
881	cases (split ? 5 11 (bitvector_of_nat 16 (\fst pol))) #m1 #m2
882	normalize nodelta cases (eq_bv ? n1 m1)
883	normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H
884	@(ex_intro ?? id) lapply (proj2 ?? Hl) #H2
885	>(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2))
886	>H @refl
887	]
888	]
889	]
890	\|2,4: (* jump_in_policy *)
891	#i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
892	[1,3: >append_length <commutative_plus #Hi normalize in Hi;
893	>(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj
894	[1,3: #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi))
895	#Hacc elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
896	@(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
897	>lookup_opt_insert_miss [1,3: @Hj \|2,4: @bitvector_of_nat_abs ]
898	[3,6: @(lt_to_not_eq i (\|prefix\|)) @(le_S_S_to_le … Hi)
899	\|1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
900	]
901	@(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
902	@le_S_S @le_plus_n_r
903	\|2,4: lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi))
904	#Hacc #H elim H -H; #h #H elim H -H; #n #H elim H -H #j #Hl
905	@(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
906	<Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs
907	[3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
908	\|1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
909	]
910	@(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
911	@le_S_S @le_plus_n_r
912	]
913	\|2,4: >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi)
914	>(nth_append_second ?? prefix ?? (le_n (\|prefix\|)))
915	<minus_n_n whd in match (nth ????); normalize nodelta in p2; cases instr in p2;
916	[1,7: #pi \| 2,3,8,9: #x \| 4,5,10,11: #id \| 6,12: #x #y] #Hinstr @conj normalize nodelta
917	[5,7,9,11,21,23: #H @⊥ @H (* instr is not a jump *)
918	\|6,8,10,12,22,24: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr)
919	#H destruct (H)
920	\|13,15,17,19: (* instr is a jump *) #_ @(ex_intro ?? (\fst pol))
921	@(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
922	@lookup_opt_insert_hit
923	\|14,16,18,20: #_ / by I/
924	\|1,2,3,4: cases pi in Hinstr;
925	[35,36,37,109,110,111: #Hinstr #H @⊥ @H
926	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,78,79,82,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106:
927	#x #Hinstr #H @⊥ @H
928	\|1,2,3,6,7,33,34,75,76,77,80,81,107,108: #x #y #Hinstr #H @⊥ @H
929	\|9,10,14,15,83,84,88,89: #id #Hinstr #_
930	@(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
931	@lookup_opt_insert_hit
932	\|11,12,13,16,17,85,86,87,90,91: #x #id #Hinstr #_
933	@(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
934	@lookup_opt_insert_hit
935	\|72,73,74,146,147,148: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
936	\|41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,115,116,119,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143:
937	#x #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
938	\|38,39,40,43,44,70,71,112,113,114,117,118,144,145: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H
939	normalize in H; destruct (H)
940	\|46,47,51,52,120,121,125,126: #id #Hinstr #_ / by I/
941	\|48,49,50,53,54,122,123,124,127,128: #x #id #Hinstr #_ / by I/
942	]
943	]
944	]
945	]
946	\|2,4: (* policy increase *)
947	#i >append_length >commutative_plus #Hi normalize in Hi;
948	cases (le_to_or_lt_eq … Hi) -Hi; #Hi
949	[1,3: >lookup_insert_miss
950	[1,3: @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
951	\|2,4: @bitvector_of_nat_abs
952	[3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
953	\|1,4: @(transitive_lt ??? (le_S_S_to_le … Hi))
954	]
955	@(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
956	@le_S_S @le_plus_n_r
957	]
958	\|2: >(injective_S … Hi) normalize nodelta in Hlength; >lookup_insert_hit normalize nodelta
959	>Hlength @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy
960	>Hl %2 @refl
961	\|4: cases daemon (* XXX get rest of proof done first *)
962	]
963	]
964	\|2,4: (* policy_safe *)
965	@lookup_forall #x cases x -x #x cases x -x #p #a #j #n normalize nodelta #Hl
966	elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
967	[1,3: @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl)
968	\|2,4: normalize nodelta in p2; cases instr in p2;
969	[2,3,8,9: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
970	\|6,12: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
971	\|1,7: #pi cases pi normalize nodelta
972	[35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
973	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69:
974	#x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
975	\|1,2,3,6,7,33,34,38,39,40,43,44,70,71:
976	#x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
977	\|9,10,14,15,46,47,51,52: #id >p3 whd in match (jump_expansion_step_instruction ???);
978	whd in match (select_reljump_length ???);
979	cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta
980	>(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
981	>(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
982	cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
983	[1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
984	\|2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
985	]
986	#Hle2 normalize nodelta #Hli
987	<(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1
988	>(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli))
989	cases (\snd (lookup ?? (bitvector_of_nat ? (\|prefix\|)) (\snd old_policy) ?))
990	[1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91: @(leb_true_to_le … Hle2)
991	] normalize @I (* much faster than / by I/, strangely enough *)
992	\|11,12,13,16,17,48,49,50,53,54: #x #id >p3 whd in match (jump_expansion_step_instruction ???);
993	whd in match (select_reljump_length ???);
994	cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta
995	>(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
996	>(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
997	cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
998	[1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
999	\|2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
1000	]
1001	#Hle2 normalize nodelta #Hli
1002	<(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl))
1003	<(pair_eq2 ?????? (Some_eq ??? Hli))
1004	cases (\snd (lookup ?? (bitvector_of_nat ? (\|prefix\|)) (\snd old_policy) ?))
1005	[1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91,97,103,109,115: @(leb_true_to_le … Hle2)
1006	] normalize @I (* vide supra *)
1007	]
1008	\|4,5,10,11: #id >p3 normalize nodelta whd in match (select_jump_length ???);
1009	whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,\fst pol〉)
1010	#q1 #q2 normalize nodelta
1011	>(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
1012	>(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
1013	[1,3: lapply (refl ? (leb (\fst pol) q2)) cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
1014	[1,3: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
1015	\|2,4: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
1016	]
1017	#Hle2 normalize nodelta
1018	]
1019	[2,4,6,8,9,10: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2)))
1020	cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3
1021	lapply (refl ? (split ? 5 11 (bitvector_of_nat ? (\fst pol))))
1022	cases (split ??? (bitvector_of_nat ? (\fst pol))) in ⊢ (???% → %); #y1 #y2 #Hle4
1023	normalize nodelta lapply (refl ? (eq_bv 5 x1 y1))
1024	cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5
1025	]
1026	#Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl))
1027	<(pair_eq2 ?????? (Some_eq ??? Hli))
1028	cases (\snd (lookup ?? (bitvector_of_nat ? (\|prefix\|)) (\snd old_policy) ?))
1029	[2,8,14,20,26,32: >Hle3 @Hle5
1030	\|37,40,43,46: >Hle1 @(leb_true_to_le … Hle2)
1031	] normalize @I (* here too *)
1032	]
1033	]
1034	]
1035	\|2,4: (* changed *)
1036	normalize nodelta #Hc [2: destruct (Hc)] #i #Hi cases (le_to_or_lt_eq … Hi) -Hi
1037	>append_length >commutative_plus #Hi
1038	normalize in Hi;
1039	[ >lookup_insert_miss
1040	[ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
1041	\| @bitvector_of_nat_abs
1042	[3: @lt_to_not_eq @(le_S_S_to_le … Hi)
1043	\|1: @(transitive_lt ??? (le_S_S_to_le … Hi))
1044	]
1045	@(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1046	@le_S_S @le_plus_n_r
1047	]
1048	\| >(injective_S … Hi) >lookup_insert_hit normalize nodelta in Hlength; >Hlength
1049	normalize nodelta @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy >Hl @refl
1050	]
1051	]
1052	\|2,4: (* policy_isize_sum XXX *) cases daemon
1053	]
1054	\| (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1
1055	normalize nodelta #Hpolicy
1056	@conj [ @conj [ @conj [ @conj [ @conj [ @conj
1057	[ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi;
1058	#Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le ?? Hi) Hi2)
1059	\| (* labels_okay *) @lookup_forall #x cases x -x #x cases x #p #a #j #lbl #Hl normalize nodelta
1060	elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? lbl Hl)
1061	#id #Hid @(ex_intro … id Hid)
1062	]
1063	\| (* jump_in_policy *) #i >append_length >commutative_plus #Hi normalize in Hi;
1064	elim (le_to_or_lt_eq … Hi) -Hi #Hi
1065	[ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi))
1066	@(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le ?? Hi))
1067	\| >(injective_S … Hi) @conj
1068	[ >(nth_append_second ?? prefix ?? (le_n (\|prefix\|))) <minus_n_n whd in match (nth ????);
1069	normalize nodelta in p2; cases instr in p2;
1070	[ #pi cases pi
1071	[1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H
1072	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ #H @⊥ @H
1073	\|9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
1074	whd in match (jump_expansion_step_instruction ???);
1075	#H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
1076	\|11,12,13,16,17: #x #id normalize nodelta
1077	whd in match (jump_expansion_step_instruction ???);
1078	#H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
1079	\|35,36,37: #_ #H @⊥ @H
1080	]
1081	\|2,3: #x #_ #H @⊥ @H
1082	\|4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
1083	\|6: #x #id #_ #H @⊥ @H
1084	]
1085	\| #H elim H -H #p #H elim H -H #a #H elim H -H #j #H
1086	>(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (\|prefix\|) (le_n (\|prefix\|)) ?) in H;
1087	[ #H destruct (H)
1088	\| @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1089	@le_S_S @le_plus_n_r
1090	]
1091	]
1092	]
1093	]
1094	\| (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
1095	elim (le_to_or_lt_eq … Hi) -Hi #Hi
1096	[ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
1097	\| >(injective_S … Hi) >lookup_opt_lookup_miss
1098	[ >lookup_opt_lookup_miss
1099	[ normalize nodelta %2 @refl
1100	\| @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (\|prefix\|) (le_n (\|prefix\|)) ?)
1101	@(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1102	@le_S_S @le_plus_n_r
1103	]
1104	\| @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (\|prefix\|) ?)) >prf
1105	[ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
1106	\| >(nth_append_second ?? prefix ?? (le_n (\|prefix\|))) <minus_n_n >p1
1107	whd in match (nth ????); normalize nodelta in p2; cases instr in p2;
1108	[ #pi cases pi
1109	[1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
1110	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
1111	\|9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
1112	whd in match (jump_expansion_step_instruction ???);
1113	#H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
1114	\|11,12,13,16,17: #x #id normalize nodelta
1115	whd in match (jump_expansion_step_instruction ???);
1116	#H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
1117	\|35,36,37: #_ normalize /2 by nmk/
1118	]
1119	\|2,3: #x #_ normalize /2 by nmk/
1120	\|4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
1121	\|6: #x #id #_ normalize /2 by nmk/
1122	]
1123	]
1124	]
1125	]
1126	]
1127	\| (* policy_safe *) @lookup_forall #x cases x -x #x cases x -x #p #a #j #n #Hl
1128	@(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl)
1129	]
1130	\| (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi;
1131	elim (le_to_or_lt_eq … Hi) -Hi #Hi
1132	[ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
1133	\| >(injective_S … Hi) >lookup_opt_lookup_miss
1134	[ >lookup_opt_lookup_miss
1135	[ normalize nodelta @refl
1136	\| @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (\|prefix\|) (le_n (\|prefix\|)) ?)
1137	@(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
1138	@le_S_S @le_plus_n_r
1139	]
1140	\| @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (\|prefix\|) ?)) >prf
1141	[ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
1142	\| >(nth_append_second ?? prefix ?? (le_n (\|prefix\|))) <minus_n_n >p1
1143	whd in match (nth ????); normalize nodelta in p2; cases instr in p2;
1144	[ #pi cases pi
1145	[1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
1146	\|4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
1147	\|9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
1148	whd in match (jump_expansion_step_instruction ???);
1149	#H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
1150	\|11,12,13,16,17: #x #id normalize nodelta
1151	whd in match (jump_expansion_step_instruction ???);
1152	#H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
1153	\|35,36,37: #_ normalize /2 by nmk/
1154	]
1155	\|2,3: #x #_ normalize /2 by nmk/
1156	\|4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
1157	\|6: #x #id #_ normalize /2 by nmk/
1158	]
1159	]
1160	]
1161	]
1162	]
1163	\| (* XXX policy_isize_sum *) cases daemon
1164	]
1165	\| @conj [ @conj [ @conj [ @conj [ @conj [ @conj
1166	[ #i #Hi / by refl/
1167	\| / by I/
1168	]
1169	\| #i #Hi @conj [ >nth_nil #H @⊥ @H \| #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
1170	normalize in H3; destruct (H3) ]
1171	]
1172	\| #i #Hi @⊥ @(absurd (i<0)) [ @Hi \| @(not_le_Sn_O) ]
1173	]
1174	\| / by I/
1175	]
1176	\| #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi \| @not_le_Sn_O ]
1177	]
1178	\| / by refl/
1179	]
1180	]
1181	qed.
1182
1183	(* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *)
1184	(* definition weaken_policy:
1185	∀program,op.
1186	option (Σp:jump_expansion_policy.
1187	And (And (And (And (out_of_program_none program p)
1188	(labels_okay (create_label_map program op) p))
1189	(jump_in_policy program p)) (policy_increase program op p))
1190	(policy_safe p)) →
1191	option (Σp:jump_expansion_policy.And (out_of_program_none program p)
1192	(jump_in_policy program p)) ≝
1193	λprogram.λop.λx.
1194	match x return λ_.option (Σp.And (out_of_program_none program p) (jump_in_policy program p)) with
1195	[ None ⇒ None ?
1196	\| Some z ⇒ Some ? (mk_Sig ?? (pi1 ?? z) ?)
1197	].
1198	@conj
1199	[ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? z)))))
1200	\| @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? z))))
1201	]
1202	qed. *)
1203
1204	(* This function executes n steps from the starting point. *)
1205	(*let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (\|l\|) 2^16)
1206	(n: ℕ) on n:(Σx:bool × ℕ × (option jump_expansion_policy).
1207	let 〈ch,pc,y〉 ≝ x in
1208	match y with
1209	[ None ⇒ pc > 2^16
1210	\| Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p)
1211	]) ≝
1212	match n with
1213	[ O ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉
1214	\| S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
1215	match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with
1216	[ None ⇒ λp2.〈pc,None ?〉
1217	\| Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?»)
1218	] (refl … z)
1219	].*)
1220
1221	let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ)
1222	on n:(Σx:bool × (option jump_expansion_policy).
1223	let 〈c,pol〉 ≝ x in
1224	match pol with
1225	[ None ⇒ True
1226	\| Some x ⇒ And (And (And (out_of_program_none program x) (jump_in_policy program x)) (\fst x < 2^16)) (policy_isize_sum program x)
1227	]) ≝
1228	match n with
1229	[ O ⇒ 〈true,Some ? (pi1 ?? (jump_expansion_start program))〉
1230	\| S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
1231	match z return λx. z=x → Σa:bool × (option jump_expansion_policy).? with
1232	[ None ⇒ λp2.〈false,None ?〉
1233	\| Some op ⇒ λp2.if ch
1234	then pi1 ?? (jump_expansion_step program (create_label_map program op) «op,?»)
1235	else (jump_expansion_internal program m)
1236	] (refl … z)
1237	].
1238	[ normalize nodelta @conj
1239	[ @conj
1240	[ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
1241	\| (* XXX *) cases daemon
1242	]
1243	\| (* XXX *) cases daemon
1244	]
1245	\| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
1246	\| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
1247	\| normalize nodelta cases (jump_expansion_step program (create_label_map program op) «op,?»)
1248	#p cases p -p #p #r cases r normalize nodelta
1249	[ #H / by I/
1250	\| #j #H @conj
1251	[ @conj
1252	[ @conj
1253	[ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))))
1254	\| @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
1255	]
1256	\| @(proj2 ?? H)
1257	]
1258	\| @(proj2 ?? (proj1 ?? H))
1259	]
1260	]
1261	]
1262	qed.
1263
1264	lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program).
1265	#program whd #x whd #n #Hn
1266	cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,0,short_jump〉)
1267	#y cases y -y #y #z normalize nodelta @refl
1268	qed.
1269
1270	lemma pe_int_sym: ∀program.symmetric ? (policy_equal_int program).
1271	#program whd #x #y #Hxy whd #n #Hn
1272	lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,0,short_jump〉)
1273	#z cases z -z #x1 #x2 #x3
1274	cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,0,short_jump〉)
1275	#z cases z -z #y1 #y2 #y3 normalize nodelta //
1276	qed.
1277
1278	lemma pe_int_trans: ∀program.transitive ? (policy_equal_int program).
1279	#program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?);
1280	whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
1281	lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,0,short_jump〉)
1282	#z cases z -z #x1 #x2 #x3
1283	cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,0,short_jump〉) #z cases z -z
1284	#y1 #y2 #y3
1285	cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,0,short_jump〉) #z cases z -z
1286	#z1 #z2 #z3 normalize nodelta //
1287	qed.
1288
1289	definition policy_equal ≝
1290	λprogram:list labelled_instruction.λp1,p2:option jump_expansion_policy.
1291	match p1 with
1292	[ Some x1 ⇒ match p2 with
1293	[ Some x2 ⇒ policy_equal_int program x1 x2
1294	\| _ ⇒ False
1295	]
1296	\| None ⇒ p2 = None ?
1297	].
1298
1299	lemma pe_refl: ∀program.reflexive ? (policy_equal program).
1300	#program whd #x whd cases x
1301	[ //
1302	\| #y @pe_int_refl
1303	]
1304	qed.
1305
1306	lemma pe_sym: ∀program.symmetric ? (policy_equal program).
1307	#program whd #x #y #Hxy whd cases y in Hxy;
1308	[ cases x
1309	[ //
1310	\| #x' #H @⊥ @(absurd ? H) /2 by nmk/
1311	]
1312	\| #y' cases x
1313	[ #H @⊥ @(absurd ? H) whd in match (policy_equal ???); @nmk #H destruct (H)
1314	\| #x' #H @pe_int_sym @H
1315	]
1316	]
1317	qed.
1318
1319	lemma pe_trans: ∀program.transitive ? (policy_equal program).
1320	#program whd #x #y #z cases x
1321	[ #Hxy #Hyz >Hxy in Hyz; //
1322	\| #x' cases y
1323	[ #H @⊥ @(absurd ? H) /2 by nmk/
1324	\| #y' cases z
1325	[ #_ #H @⊥ @(absurd ? H) /2 by nmk/
1326	\| #z' @pe_int_trans
1327	]
1328	]
1329	]
1330	qed.
1331
1332	definition step_none: ∀program.∀n.
1333	(\snd (pi1 ?? (jump_expansion_internal program n))) = None ? →
1334	∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?.
1335	#program #n lapply (refl ? (jump_expansion_internal program n))
1336	cases (jump_expansion_internal program n) in ⊢ (???% → %);
1337	#x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
1338	[ <plus_n_O >Heqj @Hj
1339	\| #k' -k <plus_n_Sm whd in match (jump_expansion_internal program (S (n+k')));
1340	lapply (refl ? (jump_expansion_internal program (n+k')))
1341	cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %);
1342	#x2 cases x2 -x2 #c2 #p2 normalize nodelta #H #Heqj2
1343	cases p2 in H Heqj2;
1344	[ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
1345	>Heqj2 normalize nodelta @refl
1346	\| #x #H #Heqj2 #abs destruct (abs)
1347	]
1348	]
1349	qed.
1350
1351	lemma pe_step: ∀program:(Σl:list labelled_instruction.\|l\| < 2^16).
1352	∀n.policy_equal program (\snd (pi1 ?? (jump_expansion_internal program n)))
1353	(\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
1354	policy_equal program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
1355	(\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
1356	#program #n #Heq
1357	cases daemon (* XXX *)
1358	qed.
1359
1360	(* this is in the stdlib, but commented out, why? *)
1361	theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
1362	#n (elim n) normalize /2 by S_pred/ qed.
1363
1364	lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.\|l\| < 2^16).∀n:ℕ.
1365	policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
1366	(\snd (pi1 … (jump_expansion_internal program (S n)))) →
1367	∀k.k ≥ n → policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
1368	(\snd (pi1 … (jump_expansion_internal program k))).
1369	#program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
1370	lapply Heq -Heq; lapply n -n; elim z -z;
1371	[ #n #Heq <plus_n_O @pe_refl
1372	\| #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z);
1373	@(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n)))))
1374	[ @Heq
1375	\| @Hind @pe_step @Heq
1376	]
1377	]
1378	qed.
1379
1380	(* this number monotonically increases over iterations, maximum 2\|program\| )
1381	let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
1382	on program: ℕ ≝
1383	match program with
1384	[ nil ⇒ acc
1385	\| cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) (\snd policy) 〈0,00
1386	,short_jump〉)) with
1387	[ long_jump ⇒ measure_int t policy (acc + 2)
1388	\| medium_jump ⇒ measure_int t policy (acc + 1)
1389	\| _ ⇒ measure_int t policy acc
1390	]
1391	].
1392
1393	lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
1394	measure_int program policy (x+d) = measure_int program policy x + d.
1395	#program #policy #x #d generalize in match x; -x elim d
1396	[ //
1397	\| -d; #d #Hind elim program
1398	[ / by refl/
1399	\| #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
1400	cases (\snd (bvt_lookup … (bitvector_of_nat ? (\|t\|)) (\snd policy) 〈0,0,short_jump〉))
1401	[ normalize nodelta @Hd
1402	\|2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
1403	@Hd
1404	]
1405	]
1406	]
1407	qed.
1408
1409	lemma measure_le: ∀program.∀policy.
1410	measure_int program policy 0 ≤ 2*\|program\|.
1411	#program #policy elim program
1412	[ normalize @le_n
1413	\| #h #t #Hind whd in match (measure_int ???);
1414	cases (\snd (lookup ?? (bitvector_of_nat ? (\|t\|)) (\snd policy) 〈0,0,short_jump〉))
1415	[ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
1416	\|2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
1417	@le_plus [1,3: @Hind \|2,4: / by le_n/ ]
1418	]
1419	]
1420	qed.
1421
1422	lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.\|l\|<2^16.
1423	∀policy:Σp:jump_expansion_policy.
1424	out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p.
1425	∀l.\|l\| ≤ \|program\| → ∀acc:ℕ.
1426	match \snd (jump_expansion_step program (create_label_map program policy) policy) with
1427	[ None ⇒ True
1428	\| Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
1429	].
1430	#program #policy #l elim l -l;
1431	[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // \| #x #_ @le_n ]
1432	\| #h #t #Hind #Hp #acc
1433	lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy))
1434	cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r
1435	[ / by I/
1436	\| #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (\|t\|) Hp)
1437	whd in match (measure_int ???); whd in match (measure_int ? x ?);
1438	cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) (\snd policy) 〈0,0,short_jump〉)
1439	#z cases z -z #x1 #x2 #x3
1440	cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) (\snd x) 〈0,0,short_jump〉)
1441	#z cases z -z #y1 #y2 #y3
1442	normalize nodelta #Hj cases Hj
1443	[ cases x3 cases y3
1444	[1,4,5,7,8,9: #H @⊥ @H
1445	\|2,3,6: #_ normalize nodelta
1446	[1,2: @(transitive_le ? (measure_int t x acc))
1447	\|3: @(transitive_le ? (measure_int t x (acc+1)))
1448	]
1449	[2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
1450	>Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
1451	]
1452	\| #Heq >Heq cases y3 normalize nodelta
1453	[2,3: >measure_plus >measure_plus @le_plus / by le_n/]
1454	>Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
1455	]
1456	]
1457	]
1458	qed.
1459
1460	(* these lemmas seem superfluous, but not sure how *)
1461	lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
1462	#a elim a
1463	[ normalize #b //
1464	\| -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ \| -b #b normalize
1465	<plus_n_Sm <plus_n_Sm #H
1466	>(Hind b (injective_S ?? (injective_S ?? H))) // ]
1467	]
1468	qed.
1469
1470	lemma sth_not_s: ∀x.x ≠ S x.
1471	#x cases x
1472	[ // \| #y // ]
1473	qed.
1474
1475	lemma measure_full: ∀program.∀policy.
1476	measure_int program policy 0 = 2*\|program\| → ∀i.i<\|program\| →
1477	(\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,0,short_jump〉)) = long_jump.
1478	#program #policy elim program
1479	[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1480	\| #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*\|t\|)
1481	[ whd in match (measure_int ???) in Hm;
1482	cases (\snd (bvt_lookup … (bitvector_of_nat ? (\|t\|)) (\snd policy) 〈0,0,short_jump〉)) in Hm;
1483	normalize nodelta
1484	[ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
1485	\| >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
1486	<(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
1487	>(commutative_plus (\|t\|) 0) <plus_O_n <minus_n_O
1488	>plus_n_Sm @le_n
1489	\| >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
1490	]
1491	\| #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
1492	[ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
1493	\| #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1494	cases (\snd (bvt_lookup … (bitvector_of_nat ? (\|t\|)) (\snd policy) 〈0,0,short_jump〉)) in Hm;
1495	normalize nodelta
1496	[ >Hmt normalize <plus_n_O >(commutative_plus (\|t\|) (S (\|t\|)))
1497	>plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
1498	\| >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
1499	#H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
1500	\| #_ //
1501	]
1502	]]
1503	]
1504	qed.
1505
1506	lemma measure_special: ∀program:(Σl:list labelled_instruction.\|l\| < 2^16).
1507	∀policy:Σp:jump_expansion_policy.
1508	out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p.
1509	match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with
1510	[ None ⇒ True
1511	\| Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal_int program policy p ].
1512	#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy)))
1513	cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %);
1514	#p cases p -p #ch #pol normalize nodelta cases pol
1515	[ / by I/
1516	\| #p normalize nodelta #Hpol #eqpol lapply (le_n (\|program\|))
1517	@(list_ind ? (λx.\|x\| ≤ \|pi1 ?? program\| →
1518	measure_int x policy 0 = measure_int x p 0 →
1519	policy_equal_int x policy p) ?? (pi1 ?? program))
1520	[ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
1521	\| #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
1522	[ #Hi @Hind
1523	[ @(transitive_le … Hp) / by /
1524	\| whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
1525	lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (\|t\|) Hp)
1526	cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) ? 〈0,0,short_jump〉) in Hm;
1527	#x cases x -x #x1 #x2 #x3
1528	cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) ? 〈0,0,short_jump〉);
1529	#y cases y -y #y1 #y2 #y3
1530	cases x3 cases y3 normalize nodelta
1531	[1: #H #_ @H
1532	\|2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1533	lapply (measure_incr_or_equal program policy t ? 0)
1534	[1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1535	\|4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 \|2,4,6: destruct (H2) ]
1536	\|5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
1537	#H #_ @(injective_plus_r … H)
1538	\|6: >measure_plus >measure_plus
1539	change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1540	#H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1541	lapply (measure_incr_or_equal program policy t ? 0)
1542	[ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1543	\|9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
1544	#H #_ @(injective_plus_r … H)
1545	]
1546	\| @(le_S_S_to_le … Hi)
1547	]
1548	\| #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1549	whd in match (measure_int ? p ?) in Hm;
1550	lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (\|t\|) Hp)
1551	cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) ? 〈0,0,short_jump〉) in
1552	Hm;
1553	#x cases x -x #x1 #x2 #x3
1554	cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) ? 〈0,0,short_jump〉);
1555	#y cases y -y #y1 #y2 #y3
1556	normalize nodelta cases x3 cases y3 normalize nodelta
1557	[1,5,9: #_ #_ //
1558	\|4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 \|2,4,6: destruct (H2) ]
1559	\|2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1560	lapply (measure_incr_or_equal program policy t ? 0)
1561	[1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1562	\|6: >measure_plus >measure_plus
1563	change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1564	#H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1565	lapply (measure_incr_or_equal program policy t ? 0)
1566	[ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1567	]
1568	]
1569	]
1570	qed.
1571
1572	lemma le_to_eq_plus: ∀n,z.
1573	n ≤ z → ∃k.z = n + k.
1574	#n #z elim z
1575	[ #H cases (le_to_or_lt_eq … H)
1576	[ #H2 @⊥ @(absurd … H2) @not_le_Sn_O
1577	\| #H2 @(ex_intro … 0) >H2 //
1578	]
1579	\| #z' #Hind #H cases (le_to_or_lt_eq … H)
1580	[ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k'))
1581	>H2 >plus_n_Sm //
1582	\| #H' @(ex_intro … 0) >H' //
1583	]
1584	]
1585	qed.
1586
1587	lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.\|l\| < 2^16.
1588	\|l\| ≤ \|program\| → measure_int l (jump_expansion_start program) 0 = 0.
1589	#l #program elim l
1590	[ //
1591	\| #h #t #Hind #Hp whd in match (measure_int ???);
1592	cases (dec_is_jump (nth (\|t\|) ? program 〈None ?, Comment []〉)) #Hj
1593	[ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (\|t\|) ? Hj) 〈0,0,short_jump〉)
1594	[ normalize nodelta @Hind @le_S_to_le ]
1595	@Hp
1596	\| >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (\|t\|) ?) Hj) 〈0,0,short_jump〉)
1597	[ normalize nodelta @Hind @le_S_to_le @Hp
1598	\| @Hp
1599	\| %
1600	[ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
1601	\| @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
1602	]
1603	]
1604	]
1605	]
1606	qed.
1607
1608	(* the actual computation of the fixpoint *)
1609	definition je_fixpoint: ∀program:(Σl:list labelled_instruction.\|l\| < 2^16).
1610	Σp:option jump_expansion_policy.∃n.∀k.n < k →
1611	policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p.
1612	#program @(\snd (pi1 ?? (jump_expansion_internal program (2*\|program\|))))
1613	cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program)
1614	(\snd (pi1 ?? (jump_expansion_internal program k)))
1615	(\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*\|program\|))
1616	[ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k #Hk
1617	@pe_trans
1618	[ @(\snd (pi1 ?? (jump_expansion_internal program x)))
1619	\| @pe_sym @equal_remains_equal
1620	[ @(proj2 ?? Hx)
1621	\| @le_S_S_to_le @le_S @Hk
1622	]
1623	\| @equal_remains_equal
1624	[ @(proj2 ?? Hx)
1625	\| @le_S_S_to_le @le_S @(proj1 ?? Hx)
1626	]
1627	]
1628	\| #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @(ex_intro … (2*\|program\|)) #k #Hk
1629	@pe_sym @equal_remains_equal
1630	[ lapply (refl ? (jump_expansion_internal program (2*\|program\|)))
1631	cases (jump_expansion_internal program (2*\|program\|)) in ⊢ (???% → %);
1632	#x cases x -x #Fch #Fpol normalize nodelta #HFpol cases Fpol in HFpol; normalize nodelta
1633	[ (* if we're at None in 2\|program\|, we're at None in S 2\|program\| too *)
1634	#HFpol #EQ whd in match (jump_expansion_internal ??); >EQ
1635	normalize nodelta / by /
1636	\| #Fp #HFp #EQ whd in match (jump_expansion_internal ??);
1637	>EQ normalize nodelta
1638	lapply (refl ? (jump_expansion_step program (create_label_map program Fp) «Fp,?»))
1639	[ @HFp
1640	\| lapply (measure_full program Fp ?)
1641	[ @le_to_le_to_eq
1642	[ @measure_le
1643	\| cut (∀x:ℕ.x ≤ 2*\|program\| →
1644	∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
1645	x ≤ measure_int program p 0))
1646	[ #x elim x
1647	[ #Hx @(ex_intro ?? (jump_expansion_start program)) @conj
1648	[ whd in match (jump_expansion_internal ??); @refl
1649	\| @le_O_n
1650	]
1651	\| -x #x #Hind #Hx
1652	lapply (refl ? (jump_expansion_internal program (S x)))
1653	cases (jump_expansion_internal program (S x)) in ⊢ (???% → %);
1654	#z cases z -z #Sxch #Sxpol cases Sxpol -Sxpol normalize nodelta
1655	[ #H #HeqSxpol @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
1656	@(absurd … (step_none program (S x) ? k))
1657	[ >HeqSxpol / by /
1658	\| <Hk >EQ @nmk #H destruct (H)
1659	]
1660	\| #Sxpol #HSxpol #HeqSxpol @(ex_intro ?? Sxpol) @conj
1661	[ @refl
1662	\| elim (Hind (transitive_le … (le_n_Sn x) Hx))
1663	#xpol #Hxpol @(le_to_lt_to_lt … (proj2 ?? Hxpol))
1664	lapply (measure_incr_or_equal program xpol program (le_n (\|program\|)) 0)
1665	[ cases (jump_expansion_internal program x) in Hxpol;
1666	#z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H;
1667	normalize nodelta / by /
1668	\| lapply (Hfa x Hx) lapply HeqSxpol -HeqSxpol
1669	whd in match (jump_expansion_internal program (S x));
1670	lapply (refl ? (jump_expansion_internal program x))
1671	lapply Hxpol -Hxpol cases (jump_expansion_internal program x) in ⊢ (% → ???% → %);
1672	#z cases z -z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H;
1673	#H #Heq cases xch in Heq; #Heq normalize nodelta
1674	[ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»))
1675	cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
1676	normalize nodelta cases c normalize nodelta
1677	[ #H1 #Heq #H2 destruct (H2)
1678	\| #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2)
1679	[ / by /
1680	\| #H3 lapply (measure_special program «xpol,H») >Heq
1681	normalize nodelta #H4 @⊥
1682	@(absurd … (H4 H3))
1683	@Hfull
1684	]
1685	]
1686	\| lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»))
1687	cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
1688	normalize nodelta cases c normalize nodelta
1689	[ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl
1690	\| #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl
1691	]
1692	]
1693	]
1694	]
1695	]
1696	]
1697	\| #H elim (H (2*\|program\|) (le_n ?)) #plp >EQ #Hplp
1698	>(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp)
1699	]
1700	]
1701	\| #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %);
1702	#x cases x -x #Gch #Gpol cases Gpol normalize nodelta
1703	[ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
1704	\| #Gp #HGp #EQ2 cases Fch
1705	[ normalize nodelta #i #Hi
1706	lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉))
1707	cases (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉) in ⊢ (???% → %);
1708	#x cases x -x #p #a #j normalize nodelta #H
1709	lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi) lapply (Hfull i Hi) >H
1710	#H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) (\snd Gp) 〈0,0,short_jump〉)
1711	#x cases x -x #p #a #j' cases j' normalize nodelta #H elim H -H #H
1712	[1,3: @⊥ @H
1713	\|2,4: destruct (H)
1714	\|5,6: @refl
1715	]
1716	\| normalize nodelta /2 by pe_int_refl/
1717	]
1718	]
1719	]
1720	]
1721	]
1722	\| @le_S_S_to_le @le_S @Hk
1723	]
1724	\| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
1725	#x cases x -x #nch #npol normalize nodelta #Hnpol
1726	#x cases x -x #Sch #Spol normalize nodelta #HSpol
1727	cases npol in Hnpol; cases Spol in HSpol;
1728	[ #Hnpol #HSpol %1 //
1729	\|2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); //
1730	#H destruct (H)
1731	\|4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m
1732	cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
1733	#x cases x -x #x1 #x2 #x3
1734	cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
1735	#y cases y -y #y1 #y2 #y3 normalize nodelta
1736	@dec_eq_jump_length
1737	]
1738	]
1739	qed.
1740
1741	(* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into
1742	* a map from pc to jump_length. This cannot be done earlier because the pc
1743	* changes between iterations. *)
1744	let rec transform_policy (n: nat) (policy: jump_expansion_policy) (acc: BitVectorTrie jump_length 16) on n:
1745	BitVectorTrie jump_length 16 ≝
1746	match n with
1747	[ O ⇒ acc
1748	\| S n' ⇒
1749	match lookup_opt … (bitvector_of_nat 16 n') (\snd policy) with
1750	[ None ⇒ transform_policy n' policy acc
1751	\| Some x ⇒ let 〈pc,addr,length〉 ≝ x in
1752	transform_policy n' policy (insert … (bitvector_of_nat 16 pc) length acc)
1753	]
1754	].
1755
1756	(* The glue between Policy and Assembly. *)
1757	definition jump_expansion':
1758	∀program:preamble × (Σl:list labelled_instruction.\|l\| < 2^16).
1759	∀lookup_labels.policy_type lookup_labels ≝
1760	λprogram.λlookup_labels.λpc.
1761	let policy ≝
1762	transform_policy (\|\snd program\|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
1763	«bvt_lookup ? ? pc policy long_jump,?».
1764	cases daemon (* XXX later *)
1765	qed.

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

Download in other formats:

Original Format