Context Navigation

PolicyStep.ma @ 2236

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

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

Download in other formats:

Original Format