source: src/ASM/PolicyStep.ma @ 2239

Last change on this file since 2239 was 2239, checked in by sacerdot, 7 years ago

One more lemma polished.

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