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. |
---|