source: src/ASM/PolicyStep.ma @ 2236

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

One subproof made shorter.

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