source: src/ASM/PolicyStep.ma @ 2225

Last change on this file since 2225 was 2225, checked in by sacerdot, 8 years ago

Minor and major improvements everywhere, shortened proofs.

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