Context Navigation

PolicyStep.ma @ 2264

Last change on this file since 2264 was 2264, checked in by sacerdot, 9 years ago

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

File size: 58.6 KB

Line
1	include "ASM/PolicyFront.ma".
2	include alias "basics/lists/list.ma".
3	include alias "arithmetics/nat.ma".
4	include alias "basics/logic.ma".
5
6	lemma not_is_jump_to_destination_of_None:
7	∀pi. ¬is_jump (Instruction pi) → destination_of pi = None ….
8	* try (#x #y #H) try (#y #H) try #H cases H %
9	qed.
10
11	lemma destination_of_None_to_is_jump_false:
12	∀instr. destination_of instr = None … → is_jump' instr = false.
13	* normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs)
14	qed.
15
16	lemma destination_of_Some_to_is_jump_true:
17	∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true.
18	#instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs
19	destruct(abs)
20	qed.
21
22	lemma jump_expansion_step1:
23	∀prefix: list labelled_instruction. S (\|prefix\|) < 2^16 → \|prefix\| < 2^16 → (redundant)
24	∀labels: label_map.
25	∀old_sigma : ppc_pc_map.
26	∀inc_added : ℕ.
27	∀inc_pc_sigma : ppc_pc_map.
28	∀label : (option Identifier).
29	∀instr : pseudo_instruction.
30	∀inc_pc : ℕ.
31	∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
32	∀old_length : jump_length.
33	∀Hpolicy : not_jump_default prefix 〈inc_pc,inc_sigma〉.
34	∀policy : ppc_pc_map.
35	∀new_length : jump_length.
36	∀isize : ℕ.
37	let add_instr ≝ match instr with
38	[ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
39	\| Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
40	\| Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (\|prefix\|) i
41	\| _ ⇒ None ?
42	] in
43	∀Heq1 :
44	match add_instr with
45	[None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
46	\|Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉]
47	=〈new_length,isize〉.
48	∀Heq2 :
49	〈inc_pc+isize,
50	insert … (bitvector_of_nat … (S (\|prefix\|)))
51	〈inc_pc+isize, \snd (lookup … (bitvector_of_nat … (S (\|prefix\|))) (\snd old_sigma) 〈O,short_jump〉)〉
52	(insert … (bitvector_of_nat … (\|prefix\|)) 〈inc_pc,new_length〉 inc_sigma)〉
53	= policy.
54	not_jump_default (prefix@[〈label,instr〉]) policy.
55	#prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
56	#inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2
57	#i >append_length <commutative_plus #Hi normalize in Hi;
58	cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
59	[ <Heq2 >lookup_insert_miss
60	[ >lookup_insert_miss
61	[ >(nth_append_first ? i prefix ?? Hi)
62	@(Hpolicy i Hi)
63	\| @bitvector_of_nat_abs try assumption
64	[ @(transitive_lt ??? Hi) assumption ]
65	@lt_to_not_eq @Hi
66	]
67	\| @bitvector_of_nat_abs try assumption
68	[ @(transitive_lt ??? Hi) assumption ]
69	@lt_to_not_eq @le_S @Hi
70	]
71	\| <Heq2 >Hi >lookup_insert_miss
72	[ >lookup_insert_hit cases instr in Heq1;
73	[2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
74	\|4,5: #x normalize nodelta #Heq1 >nth_append_second try %
75	<minus_n_n #abs cases abs
76	\|1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
77	#H #non_jump whd in match (jump_expansion_step_instruction ??????) in H;
78	>not_is_jump_to_destination_of_None in H; normalize nodelta // ]
79	\| @bitvector_of_nat_abs [3: // \| @le_S_to_le ] assumption ]]
80	qed.
81
82	lemma jump_expansion_step2:
83	∀prefix: list labelled_instruction. S (\|prefix\|) < 2^16 → \|prefix\| < 2^16 → (redundant)
84	∀labels : label_map.
85	∀old_sigma : ppc_pc_map.
86	∀inc_pc : ℕ.
87	∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
88	∀Hpolicy1 :
89	\fst (lookup … (bitvector_of_nat … O) inc_sigma 〈O,short_jump〉) = O.
90	∀Hpolicy2:
91	inc_pc =\fst (lookup … (bitvector_of_nat … (\|prefix\|)) inc_sigma 〈O,short_jump〉).
92	∀policy : ppc_pc_map.
93	∀new_length : jump_length.
94	∀isize : ℕ.
95	∀Heq2 :
96	〈inc_pc+isize,
97	insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
98	〈inc_pc+isize,
99	\snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
100	(\snd old_sigma) 〈O,short_jump〉)〉
101	(insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
102	〈inc_pc,new_length〉 inc_sigma)〉
103	= policy.
104	\fst (lookup … (bitvector_of_nat … O) (\snd policy) 〈O,short_jump〉) = O.
105	#prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_pc
106	#inc_sigma #Hpolicy1 #Hpolicy2 #policy #new_length #isize #Heq2
107	<Heq2 >lookup_insert_miss
108	[ cases (decidable_eq_nat 0 (\|prefix\|))
109	[ #Heq <Heq >lookup_insert_hit >Hpolicy2 <Heq @Hpolicy1
110	\| #Hneq >lookup_insert_miss
111	[ @Hpolicy1
112	\| @bitvector_of_nat_abs try assumption @lt_O_S ]]
113	\| @bitvector_of_nat_abs [ @lt_O_S \| @prefix_ok1 \| 3: @lt_to_not_eq @lt_O_S ] ]
114	qed.
115
116	lemma jump_expansion_step3:
117	∀program.
118	∀labels : label_map.
119	∀old_sigma : Σpolicy:ppc_pc_map.not_jump_default program policy.
120	∀prefix,x,tl. program=prefix@[x]@tl →
121	∀inc_added : ℕ.
122	∀inc_pc_sigma : ppc_pc_map.
123	∀label : option Identifier.
124	∀instr : pseudo_instruction.
125	∀p1 : x≃〈label,instr〉.
126	∀inc_pc : ℕ.
127	∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
128	∀old_pc : ℕ.
129	∀old_length : jump_length.
130	∀Holdeq :
131	lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|)) (\snd old_sigma)
132	〈O,short_jump〉 =〈old_pc,old_length〉.
133	∀Hpolicy : jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉.
134	∀policy : ppc_pc_map.
135	∀new_length : jump_length.
136	∀isize : ℕ.
137	∀Heq1 :
138	match
139	match instr
140	in pseudo_instruction
141	return λ_:pseudo_instruction.(option jump_length)
142	with
143	[Instruction (i:(preinstruction Identifier))⇒
144	jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
145	(\|prefix\|) i
146	\|Comment (_:String)⇒None jump_length
147	\|Cost (_:costlabel)⇒None jump_length
148	\|Jmp (j:Identifier)⇒
149	Some jump_length
150	(select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
151	\|Call (c:Identifier)⇒
152	Some jump_length
153	(select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
154	\|Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length]
155	in option
156	return λ_:(option jump_length).(jump_length×ℕ)
157	with
158	[None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
159	\|Some (pl:jump_length)⇒
160	〈max_length old_length pl,
161	instruction_size_jmplen (max_length old_length pl) instr〉]
162	=〈new_length,isize〉.
163	∀prefix_ok1 : S (\|prefix\|)< 2 \sup 16.
164	∀prefix_ok : \|prefix\|< 2 \sup 16.
165	∀Heq2b :
166	〈inc_pc+isize,
167	insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
168	〈inc_pc+isize,
169	\snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
170	(\snd old_sigma) 〈O,short_jump〉)〉
171	(insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
172	〈inc_pc,new_length〉 inc_sigma)〉
173	=policy.
174	jump_increase (prefix@[〈label,instr〉]) old_sigma policy.
175	#program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label
176	#instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy #policy #new_length
177	#isize #Heq1 #prefix_ok1 #prefix_ok #Heq2
178	#i >append_length >commutative_plus #Hi normalize in Hi;
179	cases (le_to_or_lt_eq … Hi) -Hi; #Hi
180	[ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
181	[ (* USE[pass]: jump_increase *)
182	lapply (Hpolicy i (le_S_to_le … Hi))
183	<Heq2
184	@pair_elim #opc #oj #EQ1 >lookup_insert_miss
185	[ >lookup_insert_miss
186	[ @pair_elim #pc #j #EQ2 #X @X
187	\| @bitvector_of_nat_abs
188	[ @(transitive_lt ??? Hi) ]
189	[1,2: assumption
190	\| @lt_to_not_eq @Hi
191	]
192	]
193	\| @bitvector_of_nat_abs
194	[ @(transitive_lt ??? Hi) @le_S_to_le ]
195	[1,2: assumption
196	\| @lt_to_not_eq @le_S @Hi
197	]
198	]
199	\| >Hi <Heq2 >Holdeq normalize nodelta
200	cut (\|prefix\| < \|program\|)
201	[ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] #lt_prefix_program
202	>lookup_insert_miss
203	[ >lookup_insert_hit normalize nodelta
204	inversion instr in Heq1; normalize nodelta
205	[4,5: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
206	\| #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
207	lapply (destination_of_None_to_is_jump_false pi)
208	lapply (destination_of_Some_to_is_jump_true pi)
209	cases (destination_of ?) normalize nodelta
210	[ #tgt #Hx
211	\| #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
212	]
213	\|2,3,6: #x [3: #y] #Heqi ]
214	#Hj <(proj1 ?? (pair_destruct ?????? Hj))
215	lapply (pi2 ?? old_sigma (\|prefix\|) ??) try assumption
216	[1,3,5,7: >prf >nth_append_second try @le_n
217	<minus_n_n whd in match (nth ????); >p1 >Heqi
218	whd in match is_jump; normalize nodelta try % >Hx %
219	\|*: >Holdeq #EQ2 >EQ2 %2 %]
220	\| @bitvector_of_nat_abs
221	[ @le_S_to_le ]
222	[1,2: assumption
223	\| @lt_to_not_eq @le_n
224	]
225	]
226	]
227	\| <Heq2 >Hi >lookup_insert_hit
228	normalize nodelta
229	cases (bvt_lookup … (bitvector_of_nat ? (S (\|prefix\|))) (\snd old_sigma) 〈0,short_jump〉)
230	#a #b normalize nodelta %2 @refl
231	]
232	qed.
233
234	lemma jump_expansion_step4:
235	∀labels : label_map.
236	∀old_sigma : ppc_pc_map.
237	∀prefix : list (option Identifier×pseudo_instruction).
238	∀inc_added : ℕ.
239	∀inc_pc_sigma : ppc_pc_map.
240	∀label : option Identifier.
241	∀instr : pseudo_instruction.
242	∀inc_pc : ℕ.
243	∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
244	∀old_length : jump_length.
245	∀Hpolicy1 : sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉.
246	∀Hpolicy2: inc_pc
247	=\fst (lookup … (bitvector_of_nat … (\|prefix\|)) inc_sigma
248	〈O,short_jump〉).
249	∀Hpolicy3: out_of_program_none prefix 〈inc_pc,inc_sigma〉.
250	∀policy : ppc_pc_map.
251	∀new_length : jump_length.
252	∀isize : ℕ.
253	∀Heq1 :
254	match
255	match instr
256	in pseudo_instruction
257	return λ_:pseudo_instruction.(option jump_length)
258	with
259	[Instruction (i:(preinstruction Identifier))⇒
260	jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
261	(\|prefix\|) i
262	\|Comment (_:String)⇒None jump_length
263	\|Cost (_:costlabel)⇒None jump_length
264	\|Jmp (j:Identifier)⇒
265	Some jump_length
266	(select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
267	\|Call (c:Identifier)⇒
268	Some jump_length
269	(select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
270	\|Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length]
271	in option
272	return λ_:(option jump_length).(jump_length×ℕ)
273	with
274	[None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
275	\|Some (pl:jump_length)⇒
276	〈max_length old_length pl,
277	instruction_size_jmplen (max_length old_length pl) instr〉]
278	=〈new_length,isize〉.
279	∀prefix_ok1 : S (\|prefix\|)< 2 \sup 16.
280	∀prefix_ok : \|prefix\|< 2 \sup 16.
281	∀Heq2b :
282	〈inc_pc+isize,
283	insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
284	〈inc_pc+isize,
285	\snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
286	(\snd old_sigma) 〈O,short_jump〉)〉
287	(insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
288	〈inc_pc,new_length〉 inc_sigma)〉
289	=policy.
290	sigma_compact_unsafe (prefix@[〈label,instr〉]) labels policy.
291	#labels #old_sigma #prefix #inc_added #inc_pc_sigma #label #instr #inc_pc #inc_sigma
292	#old_length #Hpolicy1 #Hpolicy2 #Hpolicy3 #policy #new_length #isize
293	#Heq1 #prefix_ok1 #prefix_ok #Heq2b
294	#i >append_length <commutative_plus #Hi normalize in Hi;
295	<Heq2b
296	cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
297	[ >lookup_opt_insert_miss
298	[ >lookup_opt_insert_miss
299	[ >lookup_opt_insert_miss
300	[ cases (le_to_or_lt_eq … Hi) -Hi #Hi
301	[ >lookup_opt_insert_miss
302	[ (* USE[pass]: sigma_compact_unsafe *)
303	lapply (Hpolicy1 i ?)
304	[ @le_S_to_le @Hi ]
305	cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
306	[ normalize nodelta #X @X
307	\| #x cases x -x #x1 #x2
308	cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
309	normalize nodelta
310	[ #X @X
311	\| #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
312	[ #X @X
313	\| @le_S_to_le @Hi
314	]
315	]
316	]
317	\| @bitvector_of_nat_abs
318	[3: @lt_to_not_eq @Hi ]
319	]
320	\| >Hi >lookup_opt_insert_hit normalize nodelta
321	(* USE[pass]: sigma_compact_unsafe *)
322	lapply (Hpolicy1 i ?)
323	[ <Hi @le_n
324	\| cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
325	[ normalize nodelta #X @X
326	\| #x cases x -x #x1 #x2
327	(* USE: inc_pc = fst inc_sigma *)
328	lapply Hpolicy2
329	<Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
330	cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
331	[ normalize nodelta #_ #_ #H cases H
332	\| #y cases y -y #y1 #y2 #Heq >nth_append_first
333	[ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
334	#Heq2 <Heq2 #X @X
335	\| <Hi @le_n]]]]]]]]
336	[3,4,5: @bitvector_of_nat_abs]
337	[ @(transitive_lt ??? (le_S_S … Hi))
338	\|3: @lt_to_not_eq @le_S_S @Hi
339	\|4,7,10: @(transitive_lt ??? Hi) assumption
340	\|5,11: @le_S_to_le
341	\|6: @lt_to_not_eq @Hi
342	\|9: @lt_to_not_eq @le_S @Hi
343	]
344	assumption
345	\| >Hi >lookup_opt_insert_miss
346	[2: @bitvector_of_nat_abs try assumption @lt_to_not_eq % ]
347	>lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
348	(* USE: out_of_program_none ← *)
349	lapply (Hpolicy3 i ?)
350	[ >Hi assumption
351	\| >Hi
352	(* USE: inc_pc = fst policy *)
353	lapply Hpolicy2
354	inversion (bvt_lookup_opt … (bitvector_of_nat ? (\|prefix\|)) inc_sigma)
355	[ #Heq #_ #H @⊥ @(absurd (\|prefix\| > \|prefix\|))
356	[ cases H #_ #X @X %
357	\| @le_to_not_lt @le_n]
358	\| * #x1 #x2 #Heq #Hip #_ >nth_append_second
359	[2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
360	>Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
361	cases instr in Heq1; normalize nodelta
362	[1: #pi cases (jump_expansion_step_instruction ??????) normalize nodelta]
363	try (#x #y #Heq1) try (#x #Heq1) try #Heq1
364	@eq_f <(proj2 ?? (pair_destruct ?????? Heq1))
365	try % <(proj1 ?? (pair_destruct ?????? Heq1)) %]]]
366	qed.
367
368	lemma jump_expansion_step5:
369	∀labels : label_map.
370	∀old_sigma : ppc_pc_map.
371	∀prefix : list (option Identifier×pseudo_instruction).
372	∀inc_added : ℕ.
373	∀inc_pc_sigma : ppc_pc_map.
374	∀label : option Identifier.
375	∀instr : pseudo_instruction.
376	∀inc_pc : ℕ.
377	∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
378	∀old_pc : ℕ.
379	∀old_length : jump_length.
380	∀Holdeq :
381	lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|)) (\snd old_sigma)
382	〈O,short_jump〉
383	=〈old_pc,old_length〉.
384	∀Hpolicy1 : sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O.
385	∀Hpolicy2: inc_pc
386	=\fst (lookup … (bitvector_of_nat … (\|prefix\|)) inc_sigma 〈O,short_jump〉).
387	∀added : ℕ.
388	∀policy : ppc_pc_map.
389	∀new_length : jump_length.
390	∀isize : ℕ.
391	let add_instr ≝ match instr with
392	[ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
393	\| Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
394	\| Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (\|prefix\|) i
395	\| _ ⇒ None ?
396	] in
397	∀Heq1 :
398	match add_instr with
399	[None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
400	\|Some (pl:jump_length)⇒
401	〈max_length old_length pl,
402	instruction_size_jmplen (max_length old_length pl) instr〉]
403	=〈new_length,isize〉.
404	∀prefix_ok1 : S (\|prefix\|)< 2 \sup 16.
405	∀prefix_ok : \|prefix\|< 2 \sup 16.
406	∀Heq2a :
407	match add_instr with
408	[None⇒inc_added
409	\|Some (x0:jump_length)⇒
410	inc_added+(isize-instruction_size_jmplen old_length instr)]
411	=added.
412	∀Heq2b :
413	〈inc_pc+isize,
414	insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
415	〈inc_pc+isize,
416	\snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
417	(\snd old_sigma) 〈O,short_jump〉)〉
418	(insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
419	〈inc_pc,new_length〉 inc_sigma)〉
420	=policy.
421	sigma_jump_equal (prefix@[〈label,instr〉]) old_sigma policy→added=O.
422	#labels #old_sigma #prefix #inc_added #inc_pc #label #instr #inc_pc #inc_sigma
423	#old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added #policy #new_length #isize
424	#Heq1 #prefix_ok1 #prefix_ok #Heq2a #Heq2b
425	<Heq2b #Heq <Heq2a
426	(* USE[pass]: policy_jump_equal → added = 0 *)
427	>Hpolicy1
428	[ cases instr in Heq1 Heq;
429	[2,3,6: #x [3: #y] normalize nodelta #_ #_ %
430	\|1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
431	normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]]
432	#x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
433	#Heq (CSC: make a lemma here!) lapply Holdeq -Holdeq
434	(* USE: inc_pc = fst inc_sigma *)
435	>Hpolicy2
436	lapply (Heq (\|prefix\|) ?)
437	[1,3,5: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
438	-Heq >lookup_insert_miss
439	[1,3,5: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
440	#Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (\|prefix\|)) (\snd old_sigma) 〈0,short_jump〉)
441	#y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n %
442	\|*: @bitvector_of_nat_abs try assumption @lt_to_not_eq %]
443	\| #i #Hi lapply (Heq i ?)
444	[ >append_length <plus_n_Sm @le_S <plus_n_O @Hi
445	\| >lookup_insert_miss
446	[ >lookup_insert_miss
447	[ #X @X
448	\| @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption
449	@lt_to_not_eq @Hi]
450	\| @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption
451	@lt_to_not_eq @le_S @Hi ]]]
452	qed.
453
454	lemma jump_expansion_step6:
455	∀program : list labelled_instruction.
456	∀labels : label_map.
457	∀old_sigma : Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy.
458	∀prefix : list (option Identifier×pseudo_instruction).
459	∀x : option Identifier×pseudo_instruction.
460	∀tl : list (option Identifier×pseudo_instruction).
461	∀prf : program=prefix@[x]@tl.
462	∀inc_added : ℕ.
463	∀inc_pc_sigma : ppc_pc_map.
464	∀label : option Identifier.
465	∀instr : pseudo_instruction.
466	∀p1 : x≃〈label,instr〉.
467	∀inc_pc : ℕ.
468	∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
469	∀old_pc : ℕ.
470	∀old_length : jump_length.
471	∀Holdeq :
472	lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|)) (\snd old_sigma)
473	〈O,short_jump〉
474	=〈old_pc,old_length〉.
475	∀Hpolicy1 : inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉.
476	∀Hpolic2: inc_pc =\fst (lookup … (bitvector_of_nat … (\|prefix\|)) inc_sigma 〈O,short_jump〉).
477	∀added : ℕ.
478	∀policy : ppc_pc_map.
479	∀new_length : jump_length.
480	∀isize : ℕ.
481	let add_instr ≝ match instr with
482	[ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
483	\| Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
484	\| Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (\|prefix\|) i
485	\| _ ⇒ None ?
486	] in
487	∀Heq1 :
488	match add_instr with
489	[None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
490	\|Some (pl:jump_length)⇒
491	〈max_length old_length pl,
492	instruction_size_jmplen (max_length old_length pl) instr〉]
493	=〈new_length,isize〉.
494	∀prefix_ok1 : S (\|prefix\|)< 2 \sup 16.
495	∀prefix_ok : \|prefix\|< 2 \sup 16.
496	∀Heq2a :
497	match add_instr with
498	[None⇒inc_added
499	\|Some (x0:jump_length)⇒
500	inc_added+(isize-instruction_size_jmplen old_length instr)]
501	=added.
502	∀Heq2b :
503	〈inc_pc+isize,
504	insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
505	〈inc_pc+isize,
506	\snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
507	(\snd old_sigma) 〈O,short_jump〉)〉
508	(insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
509	〈inc_pc,new_length〉 inc_sigma)〉
510	=policy.
511	added=O→sigma_pc_equal (prefix@[〈label,instr〉]) old_sigma policy.
512	#program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label
513	#instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2
514	#added #policy #new_length #isize #Heq1 #prefix_ok #prefix_ok1 #Heq2a #Heq2b
515	(* USE[pass]: added = 0 → policy_pc_equal *)
516	lapply Hpolicy1 <Heq2b <Heq2a lapply Heq1 -Heq1
517	#Hins #Hold #Hadded #i #Hi
518	>append_length in Hi; >commutative_plus #Hi normalize in Hi;
519	cases (le_to_or_lt_eq … Hi) -Hi #Hi
520	[ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
521	[ <Heq2b >lookup_insert_miss
522	[ >lookup_insert_miss
523	[ cases instr in Hadded; normalize nodelta
524	[ whd in match jump_expansion_step_instruction; normalize nodelta
525	#pi cases (destination_of ?) normalize nodelta ]
526	try (#x #y #Hadded) try (#x #Hadded) try #Hadded
527	try @(Hold Hadded i (le_S_to_le … Hi))
528	@(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded; @plus_zero_zero
529	\| @bitvector_of_nat_abs try assumption
530	[2: @lt_to_not_eq @Hi
531	\| @(transitive_lt ??? Hi) assumption ]]
532	\| @bitvector_of_nat_abs try assumption
533	[2: @lt_to_not_eq @le_S @Hi
534	\| @(transitive_lt … Hi) assumption ]]
535	\| >Hi >lookup_insert_miss
536	[ cases instr in Hadded; normalize nodelta
537	[ whd in match jump_expansion_step_instruction; normalize nodelta
538	#pi cases (destination_of ?) normalize nodelta ]
539	try (#x #y #Hadded) try (#x #Hadded) try #Hadded
540	>lookup_insert_hit
541	try (>(Hold Hadded (\|prefix\|) (le_n (\|prefix\|)))
542	@sym_eq (* USE: fst p = lookup \|prefix\| *)
543	@Hpolicy2)
544	>(Hold ? (\|prefix\|) (le_n (\|prefix\|)))
545	[2,4,6,8: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
546	(* USE: fst p = lookup \|prefix\| *)
547	@Hpolicy2
548	\|*: @bitvector_of_nat_abs try assumption
549	@lt_to_not_eq %]]
550	\|*: >Hi >lookup_insert_hit
551	(* USE fst p = lookup \|prefix\| *)
552	>Hpolicy2
553	<(Hold ? (\|prefix\|) (le_n (\|prefix\|)))
554	[2: cases instr in Hadded; normalize nodelta
555	[ whd in match jump_expansion_step_instruction; normalize nodelta
556	#pi cases (destination_of ?) normalize nodelta ]
557	try (#x #y #Hadded) try (#x #Hadded) try #Hadded
558	try @Hadded
559	@plus_zero_zero [2,4,6: >commutative_plus @Hadded \|*: skip]]
560	(* USE: sigma_compact (from old_sigma) *)
561	lapply (pi2 ?? old_sigma (\|prefix\|) ?)
562	[ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
563	\| inversion (bvt_lookup_opt … (bitvector_of_nat ? (\|prefix\|)) (\snd old_sigma))
564	[ normalize nodelta #_ #ABS cases ABS
565	\| inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (\|prefix\|))) (\snd old_sigma))
566	[ normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS
567	\| normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ
568	normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
569	>(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
570	>prf >p1 >Hins >nth_append_second try %
571	<minus_n_n whd in match (nth ????);
572	cases instr in Hins Hadded; normalize nodelta
573	[ whd in match jump_expansion_step_instruction; normalize nodelta
574	#pi lapply (destination_of_None_to_is_jump_false pi)
575	lapply (destination_of_Some_to_is_jump_true pi)
576	cases (destination_of ?) normalize nodelta
577	[ #_ #dest_None \| #tgt #dest_Some #_ ]]
578	try (#x #y #Heq1 #Hadded #X) try (#x #Heq1 #Hadded #X) try (#Heq1 #Hadded #X)
579	<(proj2 ?? (pair_destruct ?????? Heq1)) >X @plus_left_monotone
580	[1,3,4,7: @instruction_size_irrelevant try %
581	whd in match is_jump; normalize nodelta >dest_None %
582	\|*: >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ'
583	>(proj2 … (pair_destruct … EQ'))
584	elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
585	[1,3,5: #H @⊥ @(absurd ? H) @le_to_not_lt
586	<(proj2 ?? (pair_destruct ?????? Heq1))
587	@jump_length_le_max try %
588	whd in match is_jump; normalize nodelta >dest_Some %]
589	#EQisize >(proj2 … (pair_destruct … Heq1)) >EQisize % ]]]]]
590	qed.
591
592	lemma jump_expansion_step7:
593	∀old_sigma : ppc_pc_map.
594	∀prefix : list (option Identifier×pseudo_instruction).
595	∀label : option Identifier.
596	∀instr : pseudo_instruction.
597	∀inc_pc : ℕ.
598	∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
599	∀Hpolicy1 : out_of_program_none prefix 〈inc_pc,inc_sigma〉.
600	∀policy : ppc_pc_map.
601	∀new_length : jump_length.
602	∀isize : ℕ.
603	∀Heq2b :
604	〈inc_pc+isize,
605	insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
606	〈inc_pc+isize,
607	\snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
608	(\snd old_sigma) 〈O,short_jump〉)〉
609	(insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
610	〈inc_pc,new_length〉 inc_sigma)〉
611	=policy.
612	out_of_program_none (prefix@[〈label,instr〉]) policy.
613	#old_sigma #prefix #label #instr #inc_pc #inc_sigma #Hpolicy1 #policy #new_length
614	#isize #Heq2b
615	#i #Hi2 >append_length <commutative_plus @conj
616	[ (* → *) #Hi normalize in Hi; <Heq2b >lookup_opt_insert_miss
617	[ >lookup_opt_insert_miss
618	[ cases (Hpolicy1 i Hi2) #X #_ @X @le_S_to_le @Hi
619	\| @bitvector_of_nat_abs try assumption
620	[ @(transitive_lt … Hi2) @le_S_to_le assumption
621	\| % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n (S i)))
622	@(transitive_le … abs) %2 % ]]
623	\| @bitvector_of_nat_abs try assumption
624	[ @(transitive_lt … Hi2) assumption
625	\| % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n i)) assumption ]]
626	\| (* ← *) <Heq2b #Hl normalize
627	@(leb_elim (S i) (\|prefix\|))
628	[ #Hi
629	lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
630	#Hl2 (* USE[pass]: out_of_program_none ← *)
631	cases (Hpolicy1 i Hi2) #_
632	#Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 assumption
633	\| #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
634	[ #Hi3 elim (le_to_or_lt_eq … Hi3)
635	[ #X @X
636	\| #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
637	]
638	\| #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
639	>X >eq_bv_refl #H normalize in H; destruct (H)]]]
640	qed.
641
642	lemma jump_expansion_step8:
643	∀program : list labelled_instruction.
644	∀labels : label_map.
645	∀old_sigma :
646	Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy ∧\fst policy≤ 2 \sup 16.
647	∀prefix : list (option Identifier×pseudo_instruction).
648	∀x : option Identifier×pseudo_instruction.
649	∀tl : list (option Identifier×pseudo_instruction).
650	∀prf : program=prefix@[x]@tl.
651	∀inc_added : ℕ.
652	∀inc_pc_sigma : ppc_pc_map.
653	∀label : option Identifier.
654	∀instr : pseudo_instruction.
655	∀p1 : x≃〈label,instr〉.
656	∀inc_pc : ℕ.
657	∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
658	∀old_pc : ℕ.
659	∀old_length : jump_length.
660	∀Holdeq :
661	lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|)) (\snd old_sigma)
662	〈O,short_jump〉
663	=〈old_pc,old_length〉.
664	∀Hpolicy1 : inc_pc
665	=\fst (lookup … (bitvector_of_nat … (\|prefix\|)) inc_sigma 〈O,short_jump〉).
666	∀Hpolicy2: \fst (lookup … (bitvector_of_nat … (\|prefix\|)) inc_sigma 〈O,short_jump〉)
667	=old_pc+inc_added.
668	∀added : ℕ.
669	∀policy : ppc_pc_map.
670	∀new_length : jump_length.
671	∀isize : ℕ.
672	let add_instr ≝ match instr with
673	[ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
674	\| Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
675	\| Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (\|prefix\|) i
676	\| _ ⇒ None ?
677	] in
678	∀Heq1 :
679	match add_instr with
680	[None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
681	\|Some (pl:jump_length)⇒
682	〈max_length old_length pl,
683	instruction_size_jmplen (max_length old_length pl) instr〉]
684	=〈new_length,isize〉.
685	∀Heq2a :
686	match add_instr with
687	[None⇒inc_added
688	\|Some (x0:jump_length)⇒
689	inc_added+(isize-instruction_size_jmplen old_length instr)]
690	=added.
691	∀Heq2b :
692	〈inc_pc+isize,
693	insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
694	〈inc_pc+isize,
695	\snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
696	(\snd old_sigma) 〈O,short_jump〉)〉
697	(insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
698	〈inc_pc,new_length〉 inc_sigma)〉
699	=policy.
700	\fst (lookup (ℕ×jump_length) 16
701	(bitvector_of_nat 16 (\|(prefix@[〈label,instr〉])\|)) (\snd policy)
702	〈O,short_jump〉)
703	=\fst (lookup (ℕ×jump_length) 16
704	(bitvector_of_nat 16 (\|(prefix@[〈label,instr〉])\|)) (\snd old_sigma)
705	〈O,short_jump〉)
706	+added.
707	#program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label #instr
708	#p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added
709	#policy #new_length #isize #Heq1 #Heq2a #Heq2b
710	<Heq2b >append_length <plus_n_Sm <plus_n_O
711	>lookup_insert_hit
712	<Heq2a cases instr in p1 Heq1;
713	[1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
714	normalize nodelta lapply (destination_of_None_to_is_jump_false pi)
715	lapply (destination_of_Some_to_is_jump_true pi)
716	cases (destination_of ?) normalize nodelta ]
717	try (#x #y #z #p1 #Heq1) try (#x #y #p1 #Heq1) try (#x #p1 #Heq1) try (#p1 #Heq1)
718	<(proj2 ?? (pair_destruct ?????? Heq1))
719	(* USE: sigma_compact_unsafe (from old_sigma) *)
720	lapply (proj1 ?? (pi2 ?? old_sigma) (\|prefix\|) ?)
721	[1,3,5,7,9,11,13,15: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
722	lapply Holdeq -Holdeq
723	inversion (bvt_lookup_opt … (bitvector_of_nat ? (\|prefix\|)) (\snd old_sigma))
724	[1,3,5,7,9,11,13,15: normalize nodelta #_ #_ #abs cases abs]
725	inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (\|prefix\|))) (\snd old_sigma))
726	[1,3,5,7,9,11,13,15: normalize nodelta #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs]
727	* #Spc #Sj #EQS * #pc #j #Holdeq #EQ normalize nodelta
728	#H (* USE: fst p = lookup \|prefix\| ) (CSC: This part of the proof is repeated somewhere else*)
729	>Hpolicy1
730	(* USE[pass]: lookup p = lookup old_sigma + added *)
731	>Hpolicy2
732	[1,3,4,7:
733	>(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
734	-Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
735	>(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second try %
736	<minus_n_n >p1 whd in match (nth ????); >associative_plus
737	>(associative_plus pc) @plus_left_monotone >commutative_plus
738	@plus_right_monotone @instruction_size_irrelevant try %
739	whd in match is_jump; normalize nodelta >y %
740	\|2,5,6:
741	>(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H
742	>(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ
743	-Holdeq <(proj1 ?? (pair_destruct ?????? EQ))
744	>associative_plus
745	>(associative_plus pc) @plus_left_monotone >assoc_plus1
746	>(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
747	[1,3,5: >(proj2 ?? (pair_destruct ?????? EQ)) >prf in old_sigma; #old_sigma
748	>nth_append_second try %
749	<minus_n_n whd in match (nth ????); >p1 in old_sigma; #old_sigma
750	>commutative_plus @minus_plus_m_m
751	\|*: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max try %
752	whd in match is_jump; normalize nodelta >y %]]
753	qed.
754
755	lemma jump_expansion_step9:
756	(*
757	program :
758	(Σl:list labelled_instruction.S (\|l\|)< 2 \sup 16 ∧is_well_labelled_p l)*)
759	∀labels : label_map.(*
760	(Σlm:label_map
761	.(∀l:identifier ASMTag
762	.occurs_exactly_once ASMTag pseudo_instruction l program
763	→bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
764	=address_of_word_labels_code_mem program l))*)
765	∀old_sigma : ppc_pc_map.(*
766	(Σpolicy:ppc_pc_map
767	.not_jump_default program policy
768	∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy)
769	〈O,short_jump〉)
770	=O
771	∧\fst policy
772	=\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|program\|))
773	(\snd policy) 〈O,short_jump〉)
774	∧sigma_compact_unsafe program labels policy
775	∧\fst policy≤ 2 \sup 16 )*)
776	∀prefix : list (option Identifier×pseudo_instruction).(*
777	x : (option Identifier×pseudo_instruction)
778	tl : (list (option Identifier×pseudo_instruction))
779	prf : (program=prefix@[x]@tl)
780	acc :
781	(Σx0:ℕ×ppc_pc_map
782	.(let 〈added,policy〉 ≝x0 in
783	not_jump_default prefix policy
784	∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy)
785	〈O,short_jump〉)
786	=O
787	∧\fst policy
788	=\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
789	(\snd policy) 〈O,short_jump〉)
790	∧jump_increase prefix old_sigma policy
791	∧sigma_compact_unsafe prefix labels policy
792	∧(sigma_jump_equal prefix old_sigma policy→added=O)
793	∧(added=O→sigma_pc_equal prefix old_sigma policy)
794	∧out_of_program_none prefix policy
795	∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
796	(\snd policy) 〈O,short_jump〉)
797	=\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
798	(\snd old_sigma) 〈O,short_jump〉)
799	+added
800	∧sigma_safe prefix labels added old_sigma policy))
801	inc_added : ℕ
802	inc_pc_sigma : ppc_pc_map
803	p : (acc≃〈inc_added,inc_pc_sigma〉)*)
804	∀label : option Identifier.
805	∀instr : pseudo_instruction.(*
806	p1 : (x≃〈label,instr〉)
807	add_instr ≝
808	match instr
809	in pseudo_instruction
810	return λ_:pseudo_instruction.(option jump_length)
811	with
812	[Instruction (i:(preinstruction Identifier))⇒
813	jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
814	(\|prefix\|) i
815	\|Comment (_:String)⇒None jump_length
816	\|Cost (_:costlabel)⇒None jump_length
817	\|Jmp (j:Identifier)⇒
818	Some jump_length
819	(select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
820	\|Call (c:Identifier)⇒
821	Some jump_length
822	(select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
823	\|Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length]
824	inc_pc : ℕ
825	inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
826	Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
827	old_pc : ℕ
828	old_length : jump_length
829	Holdeq :
830	(lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|)) (\snd old_sigma)
831	〈O,short_jump〉
832	=〈old_pc,old_length〉)
833	Hpolicy :
834	(not_jump_default prefix 〈inc_pc,inc_sigma〉
835	∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
836	〈O,short_jump〉)
837	=O
838	∧inc_pc
839	=\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|)) inc_sigma
840	〈O,short_jump〉)
841	∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
842	∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
843	∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
844	∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
845	∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
846	∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|)) inc_sigma
847	〈O,short_jump〉)
848	=old_pc+inc_added
849	∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
850	∀added : ℕ.
851	∀policy : ppc_pc_map.(*
852	new_length : jump_length
853	isize : ℕ
854	Heq1 :
855	(match
856	match instr
857	in pseudo_instruction
858	return λ_:pseudo_instruction.(option jump_length)
859	with
860	[Instruction (i:(preinstruction Identifier))⇒
861	jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
862	(\|prefix\|) i
863	\|Comment (_:String)⇒None jump_length
864	\|Cost (_:costlabel)⇒None jump_length
865	\|Jmp (j:Identifier)⇒
866	Some jump_length
867	(select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
868	\|Call (c:Identifier)⇒
869	Some jump_length
870	(select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
871	\|Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length]
872	in option
873	return λ_0:(option jump_length).(jump_length×ℕ)
874	with
875	[None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
876	\|Some (pl:jump_length)⇒
877	〈max_length old_length pl,
878	instruction_size_jmplen (max_length old_length pl) instr〉]
879	=〈new_length,isize〉)
880	prefix_ok1 : (S (\|prefix\|)< 2 \sup 16 )
881	prefix_ok : (\|prefix\|< 2 \sup 16 )
882	Heq2a :
883	(match
884	match instr
885	in pseudo_instruction
886	return λ_0:pseudo_instruction.(option jump_length)
887	with
888	[Instruction (i:(preinstruction Identifier))⇒
889	jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
890	(\|prefix\|) i
891	\|Comment (_0:String)⇒None jump_length
892	\|Cost (_0:costlabel)⇒None jump_length
893	\|Jmp (j:Identifier)⇒
894	Some jump_length
895	(select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
896	\|Call (c:Identifier)⇒
897	Some jump_length
898	(select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
899	\|Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length]
900	in option
901	return λ_0:(option jump_length).ℕ
902	with
903	[None⇒inc_added
904	\|Some (x0:jump_length)⇒
905	inc_added+(isize-instruction_size_jmplen old_length instr)]
906	=added)
907	Heq2b :
908	(〈inc_pc+isize,
909	insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
910	〈inc_pc+isize,
911	\snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (\|prefix\|)))
912	(\snd old_sigma) 〈O,short_jump〉)〉
913	(insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (\|prefix\|))
914	〈inc_pc,new_length〉 inc_sigma)〉
915	=policy)
916	*)
917	sigma_safe (prefix@[〈label,instr〉]) labels added old_sigma policy.
918	cases daemon(*
919	#i >append_length >commutative_plus #Hi normalize in Hi;
920	elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
921	[ >nth_append_first [2: @Hi]
922	<Heq2b >lookup_insert_miss
923	[ >lookup_insert_miss
924	[ >lookup_insert_miss
925	[ elim (le_to_or_lt_eq … Hi) -Hi #Hi
926	[ >lookup_insert_miss
927	[ (* USE[pass]: sigma_safe *)
928	lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
929	cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
930	#pc #j normalize nodelta
931	cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
932	#Spc #Sj normalize nodelta
933	cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
934	#Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj
935	lapply (refl ? (leb (lookup_def … labels dest 0) (S (\|prefix\|))))
936	cases (leb (lookup_def … labels dest 0) (S (\|prefix\|))) in ⊢ (???% → %); #H
937	[ cases (le_to_or_lt_eq … (leb_true_to_le … H)) -H #H
938	[ >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
939	>lookup_insert_miss
940	[ cases (le_to_or_lt_eq … (le_S_S_to_le … H)) -H #H
941	[ >lookup_insert_miss
942	[ #H2 @H2
943	\| @bitvector_of_nat_abs
944	[3: @lt_to_not_eq @H
945	\|1: @(transitive_lt ??? H)
946	]
947	@prefix_ok
948	]
949	\| >H >lookup_insert_hit
950	(* USE: inc_pc = lookup \|prefix\| *)
951	>(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
952	#H2 @H2
953	]
954	\| @bitvector_of_nat_abs
955	[3: @lt_to_not_eq @H
956	\|1: @(transitive_lt ??? H)
957	]
958	@prefix_ok1
959	]
960	\| >H >lookup_insert_hit normalize nodelta
961	>(not_le_to_leb_false … (lt_to_not_le ?? (le_S_S ?? (le_n (\|prefix\|)))))
962	normalize nodelta
963	>(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
964	#H2 >(proj2 ?? (proj1 ?? Hpolicy))
965	]
966	\|
967
968
969
970	[2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
971	[1,4,7: cases (decidable_le (lookup_def … labels dest 0) (S (\|prefix\|))) #H
972	[1,3,5: >(le_to_leb_true … H) normalize nodelta cases (le_to_or_lt_eq … H) -H #H
973	[1,3,5: >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
974	>lookup_insert_miss
975	[2,4,6: @bitvector_of_nat_abs
976	[3,6,9: @lt_to_not_eq @H
977	\|1,4,7: @(transitive_lt ??? H)
978	]
979	@(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
980	@le_S_S >append_length <plus_n_Sm @le_S_S @le_plus_n_r
981	]
982	cases (le_to_or_lt_eq … H) -H #H
983	[1,3,5: >lookup_insert_miss
984	[1,3,5: #H @H
985	\|2,4,6: @bitvector_of_nat_abs
986	[3,6,9: @lt_to_not_eq @(le_S_S_to_le … H)
987	\|1,4,7: @(transitive_lt ??? (le_S_S_to_le … H))
988	]
989	@(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
990	>append_length @le_S_S @le_plus_n_r
991	]
992	\|2,4,6: >(injective_S … H) >lookup_insert_hit
993	(* USE: blerp *)
994	>(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
995	#H @H
996	]
997	\|2,4,6: >H >lookup_insert_hit >(not_le_to_leb_false)
998	[2,4,6: @le_to_not_lt @le_n]
999	normalize nodelta
1000	lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (\|prefix\|) ?)
1001	[1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
1002	lapply (refl ? (lookup_opt … (bitvector_of_nat ? (\|prefix\|)) (\snd old_sigma)))
1003	cases (lookup_opt … (bitvector_of_nat ? (\|prefix\|)) (\snd old_sigma)) in ⊢ (???% → %);
1004	[1,3,5: normalize nodelta #_ #abs cases abs
1005	\|2,4,6: #x cases x -x #ppc #pj normalize nodelta #PEQ
1006	lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (\|prefix\|))) (\snd old_sigma)))
1007	cases (lookup_opt … (bitvector_of_nat ? (S (\|prefix\|))) (\snd old_sigma)) in ⊢ (???% → %);
1008	[1,3,5: normalize nodelta #_ #abs cases abs
1009	\|2,4,6: #x cases x -x #Sppc #Spj normalize nodelta #SPEQ #Pcompact
1010	>(lookup_opt_lookup_hit … SPEQ 〈0,short_jump〉)
1011	>(lookup_opt_lookup_hit … PEQ 〈0,short_jump〉) in Holdeq;
1012	#H >Pcompact >(proj1 ?? (pair_destruct ?????? H))
1013	>commutative_plus >assoc_plus1 <(proj2 ?? (proj1 ?? Hpolicy))
1014	<(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1015	>prf >nth_append_second
1016	[1,3,5: <minus_n_n whd in match (nth ????); >p1
1017	cases daemon (* to be lemmatized *)
1018	\|2,4,6: @le_n
1019	]
1020	]
1021	]
1022	]
1023	\|2,4,6: >(not_le_to_leb_false … H)
1024	>not_le_to_leb_false
1025	[2,4,6: @lt_to_not_le @le_S_to_le @not_le_to_lt @H
1026	\|1,3,5: normalize nodelta #H @H
1027	]
1028	]
1029	\|2,5,8: cases daemon (* like previous case *)
1030	\|3,6,9: cases daemon (* like previous case *)
1031	]
1032	\|4,5: #x normalize nodelta cases daemon (* blerp *)
1033	\|1: cases daemon (* blerp *)
1034	]
1035
1036
1037
1038
1039	(*(\fst (short_jump_cond (bitvector_of_nat 16 Spc)
1040	(bitvector_of_nat 16
1041	(inc_pc
1042	+instruction_size_jmplen
1043	(max_length old_length
1044	(select_jump_length labels old_sigma inc_pc_sigma inc_added
1045	(\|prefix\|) xx)) (Jmp xx))))
1046	=true *)
1047
1048
1049	]
1050	[ >lookup_insert_miss
1051	[ (* USE[pass]: sigma_safe *)
1052	lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
1053	cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
1054	#pc #j normalize nodelta
1055	cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
1056	#Spc #Sj normalize nodelta
1057	cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
1058	#Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
1059	[2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
1060	[1,4,7: *)
1061	qed.
1062
1063	(* One step in the search for a jump expansion fixpoint. *)
1064	definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.
1065	S (\|l\|) < 2^16 ∧ is_well_labelled_p l).
1066	∀labels:(Σlm:label_map.∀l.
1067	occurs_exactly_once ?? l program →
1068	bitvector_of_nat ? (lookup_def … lm l 0) =
1069	address_of_word_labels program l).
1070	∀old_policy:(Σpolicy:ppc_pc_map.
1071	(* out_of_program_none program policy *)
1072	And (And (And (And (not_jump_default program policy)
1073	(\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
1074	(\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (\|program\|)) (\snd policy) 〈0,short_jump〉)))
1075	(sigma_compact_unsafe program labels policy))
1076	(\fst policy ≤ 2^16)).
1077	(Σx:bool × (option ppc_pc_map).
1078	let 〈no_ch,y〉 ≝ x in
1079	match y with
1080	[ None ⇒ nec_plus_ultra program old_policy
1081	\| Some p ⇒ And (And (And (And (And (And (And
1082	(not_jump_default program p)
1083	(\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
1084	(\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (\|program\|)) (\snd p) 〈0,short_jump〉)))
1085	(jump_increase program old_policy p))
1086	(sigma_compact_unsafe program labels p))
1087	(sigma_jump_equal program old_policy p → no_ch = true))
1088	(no_ch = true → sigma_pc_equal program old_policy p))
1089	(\fst p ≤ 2^16)
1090	])
1091	≝
1092	λprogram.λlabels.λold_sigma.
1093	let 〈final_added, final_policy〉 ≝
1094	pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
1095	(λprefix.Σx:ℕ × ppc_pc_map.
1096	let 〈added,policy〉 ≝ x in
1097	And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
1098	(\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
1099	(\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (\|prefix\|)) (\snd policy) 〈0,short_jump〉)))
1100	(jump_increase prefix old_sigma policy))
1101	(sigma_compact_unsafe prefix labels policy))
1102	(sigma_jump_equal prefix old_sigma policy → added = 0))
1103	(added = 0 → sigma_pc_equal prefix old_sigma policy))
1104	(out_of_program_none prefix policy))
1105	(\fst (bvt_lookup … (bitvector_of_nat ? (\|prefix\|)) (\snd policy) 〈0,short_jump〉) =
1106	\fst (bvt_lookup … (bitvector_of_nat ? (\|prefix\|)) (\snd old_sigma) 〈0,short_jump〉) + added))
1107	(sigma_safe prefix labels added old_sigma policy))
1108	program
1109	(λprefix.λx.λtl.λprf.λacc.
1110	let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
1111	let 〈label,instr〉 ≝ x in
1112	(* Now, we must add the current ppc and its pc translation.
1113	* Three possibilities:
1114	* - Instruction is not a jump; i.e. constant size whatever the sigma we use;
1115	* - Instruction is a backward jump; we can use the sigma we're constructing,
1116	* since it will already know the translation of its destination;
1117	* - Instruction is a forward jump; we must use the old sigma (the new sigma
1118	* does not know the translation yet), but compensate for the jumps we
1119	* have lengthened.
1120	*)
1121	let add_instr ≝ match instr with
1122	[ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) j)
1123	\| Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (\|prefix\|) c)
1124	\| Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (\|prefix\|) i
1125	\| _ ⇒ None ?
1126	] in
1127	let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
1128	let old_length ≝
1129	\snd (bvt_lookup … (bitvector_of_nat ? (\|prefix\|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
1130	let old_size ≝ instruction_size_jmplen old_length instr in
1131	let 〈new_length, isize〉 ≝ match add_instr with
1132	[ None ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
1133	\| Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
1134	] in
1135	let new_added ≝ match add_instr with
1136	[ None ⇒ inc_added
1137	\| Some x ⇒ plus inc_added (minus isize old_size)
1138	] in
1139	let old_Slength ≝
1140	\snd (bvt_lookup … (bitvector_of_nat ? (S (\|prefix\|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
1141	let updated_sigma ≝
1142	(* we add the new PC to the next position and the new jump length to this one *)
1143	bvt_insert … (bitvector_of_nat ? (S (\|prefix\|))) 〈inc_pc + isize, old_Slength〉
1144	(bvt_insert … (bitvector_of_nat ? (\|prefix\|)) 〈inc_pc, new_length〉 inc_sigma) in
1145	〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
1146	) 〈0, 〈0,
1147	bvt_insert …
1148	(bitvector_of_nat ? 0)
1149	〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
1150	(Stub ??)〉〉
1151	) in
1152	if gtb (\fst final_policy) 2^16 then
1153	〈eqb final_added 0, None ?〉
1154	else
1155	〈eqb final_added 0, Some ? final_policy〉.
1156	[ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
1157	#x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
1158	(* USE: inc_pc = fst of policy (from fold) *)
1159	>(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1;
1160	(* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
1161	lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
1162	#Hsig #Hge
1163	(* USE: added = 0 → policy_pc_equal (from fold) *)
1164	lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (\|program\|) (le_n (\|program\|)))
1165	[ (* USE: policy_jump_equal → added = 0 (from fold) *)
1166	@(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
1167	inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
1168	[ #Hj
1169	(* USE: policy_increase (from fold) *)
1170	lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
1171	lapply (Habs i Hi ?) [ >Hj %]
1172	cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
1173	#opc #oj
1174	cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉)
1175	#pc #j normalize nodelta #Heq >Heq cases j
1176	[1,2: #abs cases abs #abs2 try (cases abs2) @refl
1177	\|3: #_ @refl
1178	]
1179	\| #Hnj
1180	(* USE: not_jump_default (from fold and old_sigma) *)
1181	>(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?)
1182	[2: >Hnj %]
1183	>(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try %
1184	>Hnj %
1185	]
1186	\| #abs >abs in Hsig; #Hsig
1187	@(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
1188	]
1189	\| normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
1190	>H2 in H; normalize nodelta -H2 -x #H @conj
1191	[ @conj [ @conj
1192	[ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy,
1193	* jump_increase, sigma_compact_unsafe (from fold) *)
1194	@(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
1195	\| #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *)
1196	@eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2
1197	]
1198	\| (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *)
1199	#H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
1200	]
1201	\| @not_lt_to_le @ltb_false_to_not_lt @p1
1202	]
1203	\|4: lapply (pi2 ?? acc) >p -acc inversion inc_pc_sigma
1204	#inc_pc #inc_sigma #Hips normalize nodelta
1205	inversion (bvt_lookup … (bitvector_of_nat ? (\|prefix\|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
1206	#old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
1207	#added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
1208	#Heq1 #Heq2
1209	cut (S (\|prefix\|) < 2^16)
1210	[ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length
1211	<plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1
1212	cut (\|prefix\| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok
1213	cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
1214	% [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
1215	[ (* not_jump_default *)
1216	@(jump_expansion_step1 … Heq1 Heq2b) try assumption
1217	@(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
1218	\| (* 0 ↦ 0 *)
1219	@(jump_expansion_step2 … Heq2b) try assumption
1220	[ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
1221	\| @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ]
1222	\| (* inc_pc = fst of policy *)
1223	<Heq2b >append_length >(commutative_plus (\|prefix\|)) >lookup_insert_hit @refl
1224	\| (* jump_increase *)
1225	@(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq
1226	… Heq1 prefix_ok1 prefix_ok Heq2b)
1227	try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
1228	cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
1229	\| (* sigma_compact_unsafe *)
1230	@(jump_expansion_step4 … Heq1 … Heq2b) try assumption
1231	try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1232	try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))
1233	@(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
1234	\| (* policy_jump_equal → added = 0 *)
1235	@(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption
1236	try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
1237	@(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1238	\| (* added = 0 → policy_pc_equal *)
1239	@(jump_expansion_step6 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 … Heq2a Heq2b) try assumption
1240	try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
1241	try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1242	cases (pi2 … old_sigma) * #_ #X #_ @X
1243	\| (* out_of_program_none *)
1244	@(jump_expansion_step7 … Heq2b)
1245	@(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
1246	\| (* lookup p = lookup old_sigma + added *)
1247	@(jump_expansion_step8 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 Heq2a Heq2b) try assumption
1248	[ cases (pi2 … old_sigma) * #_ #H1 #H2 % assumption
1249	\| @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1250	\| @(proj2 ?? (proj1 ?? Hpolicy)) ]
1251	\| (* sigma_safe *)
1252	@jump_expansion_step9 (*try assumption
1253	@(proj2 ?? Hpolicy) *)
1254	]
1255	\| normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
1256	[ #i cases i
1257	[ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1258	\| -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
1259	]
1260	\| >lookup_insert_hit @refl
1261	\| >lookup_insert_hit @refl
1262	\| #i #Hi <(le_n_O_to_eq … Hi)
1263	>lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
1264	#a #b normalize nodelta %2 @refl
1265	\| #i cases i
1266	[ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1267	\| -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1268	]
1269	\| #_ %
1270	\| #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
1271	(* USE: 0 ↦ 0 (from old_sigma) *)
1272	@(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
1273	\| #i cases i
1274	[ #Hi2 @conj
1275	[ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
1276	\| >lookup_opt_insert_hit #H destruct (H)
1277	]
1278	\| -i #i #Hi2 @conj
1279	[ #Hi >lookup_opt_insert_miss
1280	[ / by refl/
1281	\| @bitvector_of_nat_abs
1282	[ @Hi2
1283	\| / by /
1284	\| @sym_neq @lt_to_not_eq / by /
1285	]
1286	]
1287	\| #_ @le_S_S @le_O_n
1288	]
1289	]
1290	\| >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *)
1291	>(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O %
1292	\| #i cases i
1293	[ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1294	\| -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1295	]
1296	]
1297	]
1298	qed.

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

Download in other formats:

Original Format