source: src/ASM/PolicyStep.ma @ 2237

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

Even shorter version.

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