source: src/ASM/PolicyStep.ma @ 2059

Last change on this file since 2059 was 2059, checked in by boender, 7 years ago
  • updated Policy to work better
File size: 42.5 KB
Line 
1include "ASM/PolicyFront.ma".
2include alias "basics/lists/list.ma".
3include alias "arithmetics/nat.ma".
4include alias "basics/logic.ma".
5
6(* One step in the search for a jump expansion fixpoint. *)
7definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
8  ∀labels:(Σlm:label_map.∀l.
9    occurs_exactly_once ?? l program →
10    bitvector_of_nat ? (lookup_def … lm l 0) =
11    address_of_word_labels_code_mem program l).
12  ∀old_policy:(Σpolicy:ppc_pc_map.
13    And (And (And (And (out_of_program_none program policy)
14    (jump_not_in_policy program policy))
15    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
16    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
17    (\fst policy < 2^16)).
18  (Σx:bool × (option ppc_pc_map).
19    let 〈no_ch,y〉 ≝ x in
20    match y with
21    [ None ⇒ nec_plus_ultra program old_policy
22    | Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p)
23       (jump_not_in_policy program p))
24       (policy_increase program old_policy p))
25       (no_ch = true → policy_compact program labels p))
26       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
27       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
28       (no_ch = true → policy_pc_equal program old_policy p))
29       (policy_jump_equal program old_policy p → no_ch = true))
30       (\fst p < 2^16)
31    ])
32    ≝
33  λprogram.λlabels.λold_sigma.
34  let 〈final_added, final_policy〉 ≝
35    pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
36    (λprefix.Σx:ℕ × ppc_pc_map.
37      let 〈added,policy〉 ≝ x in
38      And (And (And (And (And (And (And (And (out_of_program_none prefix policy)
39      (jump_not_in_policy prefix policy))
40      (policy_increase prefix old_sigma policy))
41      (policy_compact_unsafe prefix labels policy))
42      (policy_safe prefix labels added old_sigma policy))
43      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
44      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
45      (added = 0 → policy_pc_equal prefix old_sigma policy))
46      (policy_jump_equal prefix old_sigma policy → added = 0))
47    program
48    (λprefix.λx.λtl.λprf.λacc.
49      let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
50      let 〈label,instr〉 ≝ x in
51      (* Now, we must add the current ppc and its pc translation.
52       * Three possibilities:
53       *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
54       *   - Instruction is a backward jump; we can use the sigma we're constructing,
55       *     since it will already know the translation of its destination;
56       *   - Instruction is a forward jump; we must use the old sigma (the new sigma
57       *     does not know the translation yet), but compensate for the jumps we
58       *     have lengthened.
59       *)
60      let add_instr ≝ match instr with
61      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
62      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
63      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
64      | _             ⇒ None ?
65      ] in
66      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
67      let old_length ≝
68        \snd (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
69      let old_size ≝ instruction_size_jmplen old_length instr in
70      let 〈new_length, isize〉 ≝ match add_instr with
71      [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
72      | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
73      ] in
74      let new_added ≝ match add_instr with
75      [ None   ⇒ inc_added
76      | Some x ⇒ plus inc_added (minus isize old_size)
77      ] in
78      let old_Slength ≝
79        \snd (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
80      let updated_sigma ≝
81        (* we add the new PC to the next position and the new jump length to this one *)
82        bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, old_Slength〉
83        (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
84      〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
85    ) 〈0, 〈0,
86      bvt_insert …
87        (bitvector_of_nat ? 0)
88        〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
89        (Stub ??)〉〉
90    ) in
91    if geb (\fst final_policy) 2^16 then
92      〈eqb final_added 0, None ?〉
93    else
94      〈eqb final_added 0, Some ? final_policy〉.
95[ normalize nodelta @nmk #Habs lapply p generalize in match (foldl_strong ?????); *
96  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
97  (* USE: inc_pc = fst of policy (from fold) *)
98  >(proj2 ?? (proj1 ?? (proj1 ?? Hind))) in p1;
99  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
100  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (pi2 ?? old_sigma)))
101  #Hsig #Hge
102  (* USE: added = 0 → policy_pc_equal (from fold) *)
103  lapply ((proj2 ?? (proj1 ?? Hind)) ? (|program|) (le_n (|program|)))
104  [ @(proj2 ?? Hind) #i #Hi
105    cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
106    [ #Hj
107      (* USE: policy_increase (from fold) *)
108      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
109      lapply (Habs i Hi Hj)
110      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
111      #opc #oj
112      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉)
113      #pc #j normalize nodelta #Heq >Heq cases j
114      [1,2: #abs cases abs #abs2 try (cases abs2) @refl
115      |3: #_ @refl
116      ]
117    | #Hnj
118      (* USE: jump_not_in_policy (from fold and old_sigma) *)
119      >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) i Hi Hnj)
120      >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)
121      @refl
122    ]
123  | #abs >abs in Hsig; #Hsig
124    @(absurd ? Hsig) @le_to_not_lt @leb_true_to_le <geb_to_leb @Hge
125  ]
126| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
127  >H2 in H; normalize nodelta -H2 -x #H @conj
128  [ @conj [ @conj [ @conj [ @conj [ @conj
129  [ (* USE[pass]: out_of_program_none, jump_not_in_policy, policy_increase (from fold) *)
130    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
131  | (* policy_compact_unsafe → policy_compact (in the end) *)
132    #Hch #i #Hi
133    (* USE: policy_compact_unsafe (from fold) *)
134    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) i Hi)
135    (* USE: policy_safe (from fold) *)
136    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) i Hi)
137    lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)))
138    cases (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)) in ⊢ (???% → %);
139    [ / by /
140    | #x cases x -x #x1 #x2 #EQ
141      cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd final_policy))
142      [ / by /
143      | #y cases y -y #y1 #y2 normalize nodelta #H #H2
144        cut (instruction_size_jmplen x2
145         (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)) =
146         instruction_size … (bitvector_of_nat ? i)
147         (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)))
148        [5: #H3 <H3 @H2
149        |4: whd in match (instruction_size_jmplen ??);
150            whd in match (instruction_size …);
151            whd in match (assembly_1_pseudoinstruction …);
152            whd in match (expand_pseudo_instruction …);
153            normalize nodelta whd in match (append …) in H;
154            cases (nth i ? (pi1 ?? program) 〈None ?,Comment []〉) in H;
155            #lbl #instr cases instr
156            [2,3,6: #x [3: #y] normalize nodelta #H @refl
157            |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj
158              lapply (Hj x (refl ? x)) -Hj normalize nodelta
159              >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
160              cases x2 normalize nodelta
161              [1,4: whd in match short_jump_cond; normalize nodelta
162                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
163                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
164                normalize nodelta
165                (* USE: added = 0 → policy_pc_equal *)
166                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
167                [2,4,6,8: cases daemon (* XXX *) ]
168                [1,5: >(eqb_true_to_eq … Hch) <plus_n_O]
169                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
170                #result #flags normalize nodelta
171                cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
172                cases (get_index' bool 2 0 flags) normalize nodelta
173                [1,3,5,7: cases (eq_bv 9 upper ?)
174                |2,4,6,8: cases (eq_bv 9 upper (zero 9))]
175                [2,4,6,8,10,12,14,16: #H lapply (proj1 ?? H) #H3 destruct (H3)
176                |5,7,13,15: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
177                |1,3,9,11: #_ normalize nodelta @refl
178                ]
179             |2,5: whd in match short_jump_cond; whd in match medium_jump_cond;
180                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
181                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
182                normalize nodelta
183                (* USE: added = 0 → policy_pc_equal *)
184                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
185                [2,4,6,8: cases daemon (* XXX *)]
186                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
187                normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
188                cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
189                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
190                #result #flags normalize nodelta
191                cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
192                cases (get_index' bool 2 0 flags) normalize nodelta
193                #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
194             |3,6: whd in match short_jump_cond; whd in match medium_jump_cond;
195                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
196                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
197                normalize nodelta
198                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
199                [2,4,6,8: cases daemon (* XXX *)]
200                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
201                normalize nodelta
202                cases (vsplit bool 5 11 ?) #addr1 #addr2
203                cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
204                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
205                #result #flags normalize nodelta
206                cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
207                cases (get_index' bool 2 0 flags) normalize nodelta
208                #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
209             ]
210           |1: #pi cases pi
211             [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:
212               [1,2,3,6,7,24,25: #x #y
213               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
214               normalize nodelta #H @refl
215             |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
216               normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
217               #Hj lapply (Hj x (refl ? x)) -Hj
218               whd in match expand_relative_jump; normalize nodelta
219               whd in match expand_relative_jump_internal; normalize nodelta
220               whd in match expand_relative_jump_unsafe; normalize nodelta
221               whd in match expand_relative_jump_internal_unsafe;
222               normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
223               <(plus_n_Sm i 0) <plus_n_O
224               cases daemon (* XXX *)
225             ]
226           ]
227         ]
228       ]
229     ]
230   ]
231   | (* USE: 0 ↦ 0 (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
232   ]
233   | (* USE: inc_pc = fst of policy (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? H)))
234   ]
235   | #H2 (* USE: added = 0 → policy_pc_equal (from fold) *)
236     @(proj2 ?? (proj1 ?? H)) @eqb_true_to_eq @H2
237   ]
238   | #H2 (* USE: policy_jump_equal → added = 0 (from fold *)
239     @eq_to_eqb_true @(proj2 ?? H) @H2
240   ]
241   | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
242   ]
243|4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
244  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
245  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);
246  #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta
247  @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
248  @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
249  [ (* out_of_program_none *) #i #Hi2 >append_length <commutative_plus @conj
250    [ (* → *) #Hi normalize in Hi;
251      cases instr in Heq2; normalize nodelta
252      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
253      [1,3,5,7,9,11: >lookup_opt_insert_miss
254        [1,3,5,7,9,11: (* USE: out_of_program_none → *)
255          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2))
256          @le_S_to_le @Hi
257        |2,4,6,8,10,12: @bitvector_of_nat_abs
258          [1,4,7,10,13,16: @Hi2
259          |2,5,8,11,14,17: @(transitive_lt … Hi2)
260          |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
261          ] @le_S_to_le @Hi
262        ]
263      |2,4,6,8,10,12: @bitvector_of_nat_abs
264        [1,4,7,10,13,16: @Hi2
265        |2,5,8,11,14,17: @(transitive_lt … Hi2)
266        |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
267        ] @Hi
268      ]
269    | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
270      elim (decidable_lt i (|prefix|))
271      [ #Hi
272        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
273        #Hl2 (* USE: out_of_program_none ← *)
274        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2) Hl2)
275        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
276      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
277        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
278          [ / by /
279          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
280          ]
281        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
282          >X >eq_bv_refl #H normalize in H; destruct (H)
283        ]
284      ]
285    ]
286  | (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi;
287    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
288    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
289      [ >lookup_insert_miss
290        [ >(nth_append_first ? i prefix ?? Hi)
291          (* USE: jump_not_in_policy *)
292          @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi)
293        | @bitvector_of_nat_abs
294          [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
295            >commutative_plus @le_plus_a @Hi
296          | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
297            @le_plus_n_r
298          | @lt_to_not_eq @Hi
299          ]
300        ]
301      | @bitvector_of_nat_abs
302        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
303          >commutative_plus @le_plus_a @Hi
304        | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm
305          @le_S_S @le_plus_n_r
306        | @lt_to_not_eq @le_S @Hi
307        ]
308      ]
309    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
310      [ >lookup_insert_hit cases instr in Heq1;
311        [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
312        |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
313          [1,3: <minus_n_n whd in match (nth ????); / by I/
314          |2,4: @le_n
315          ]
316        |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
317          [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:
318            [1,2,3,6,7,24,25: #x #y
319            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
320            <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
321          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
322            #_ #H @⊥ cases H #H2 @H2 / by I/
323          ]
324        ]
325      | @bitvector_of_nat_abs
326        [ @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r
327        | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
328          @le_S_S @le_plus_n_r
329        | @lt_to_not_eq @le_n
330        ]
331      ]
332    ]
333  ]
334  | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
335    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
336    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
337      [ (* USE: policy_increase *)
338        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
339        <(proj2 ?? (pair_destruct ?????? Heq2))
340        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
341        [ >lookup_insert_miss
342          [ @pair_elim #pc #j #EQ2 / by /
343          | @bitvector_of_nat_abs
344            [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S
345              >commutative_plus @le_plus_a @Hi
346            | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
347            | @lt_to_not_eq @Hi
348            ]
349          ]
350        | @bitvector_of_nat_abs
351          [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus
352            @le_plus_a @Hi
353          | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r
354          | @lt_to_not_eq @le_S @Hi
355          ]
356        ]
357      | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) @pair_elim #opc #oj #EQ1
358        >lookup_insert_miss
359        [ >lookup_insert_hit cases (dec_is_jump instr)
360          [ cases instr in Heq1; normalize nodelta
361            [ #pi cases pi
362              [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:
363                [1,2,3,6,7,24,25: #x #y
364                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
365              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
366                whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
367                #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1; normalize nodelta
368                #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
369              ]
370            |2,3,6: #x [3: #y] #_ #Hj cases Hj
371            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1;
372              normalize nodelta #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
373            ]
374          | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
375            [ #pi cases pi
376              [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:
377                [1,2,3,6,7,24,25: #x #y
378                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
379                whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
380                #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
381                (* USE: jump_not_in_policy (from old_sigma) *)
382                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
383                [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:
384                  >prf >nth_append_second
385                  [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:
386                    <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
387                  |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:
388                    @le_n
389                  ]
390                |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
391                  >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
392                |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:
393                  cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
394                  #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2
395                  %2 @refl
396                ]
397              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
398                #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
399              ]
400            |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
401              (* USE: jump_not_in_policy (from old_sigma) *)
402              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
403              [1,4,7: >prf >nth_append_second
404                [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
405                |2,4,6: @le_n
406                ]
407              |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
408              |3,6,9:
409                cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
410                #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2 %2 @refl
411              ]
412            |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
413            ]
414          ]
415        | @bitvector_of_nat_abs
416          [ @(transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r
417          | @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm
418            @le_S_S @le_plus_n_r
419          | @lt_to_not_eq @le_n
420          ]
421        ]
422      ]
423    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
424      normalize nodelta
425      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
426      #a #b normalize nodelta %2 @refl
427    ]
428  ]
429  | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
430    <(proj2 ?? (pair_destruct ?????? Heq2))
431    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
432    [ >lookup_opt_insert_miss
433      [ >lookup_opt_insert_miss
434        [ >lookup_opt_insert_miss
435          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
436            [ >lookup_opt_insert_miss
437              [ (* USE: policy_compact_unsafe *)
438                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
439                [ @le_S_to_le @Hi ]
440                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
441                [ normalize nodelta / by /
442                | #x cases x -x #x1 #x2
443                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
444                  normalize nodelta
445                  [ / by /
446                  | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
447                    [ / by /
448                    | @le_S_to_le @Hi
449                    ]
450                  ]
451                ]
452              | @bitvector_of_nat_abs
453                [3: @lt_to_not_eq @Hi ]
454              ]
455            | >Hi >lookup_opt_insert_hit normalize nodelta
456              (* USE: policy_compact_unsafe *)
457              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
458              [ <Hi @le_n
459              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
460                [ normalize nodelta / by /
461                | #x cases x -x #x1 #x2
462                  (* USE: inc_pc = fst inc_sigma *)
463                  lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Hi
464                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
465                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
466                  [ normalize nodelta #_  #_ #H cases H
467                  | #y cases y -y #y1 #y2 #Heq >nth_append_first
468                    [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
469                      #Heq2 <Heq2 / by /
470                    | <Hi @le_n
471                    ]
472                  ]
473                ]
474              ]
475            ]
476          ]
477        ]
478      ]
479      [3,4,5: @bitvector_of_nat_abs]
480      [1: (* Si < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
481        >commutative_plus @le_plus_a @Hi
482      |2,8: (* Spref < 2*16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
483        <plus_n_Sm @le_S_S @le_plus_n_r
484      | (* Si ≠ Spref *) @lt_to_not_eq @le_S_S @Hi
485      |4,7: (* i < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
486        >commutative_plus @le_plus_a @le_S_to_le @Hi
487      |5,11: (* pref < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
488        @le_plus_n_r
489      | @lt_to_not_eq @Hi
490      | @lt_to_not_eq @le_S_to_le @le_S_S @Hi
491      | @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
492        >commutative_plus @le_plus_a @Hi
493      ]
494    | >Hi >lookup_opt_insert_miss
495      [2: @bitvector_of_nat_abs
496        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
497        | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
498          <plus_n_Sm @le_S_S @le_plus_n_r
499        | @lt_to_not_eq @le_n
500        ]
501      ]
502      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
503      (* USE: out_of_program_none ← *)
504      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i ?))
505      [ >Hi @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
506      | >Hi
507        (* USE: inc_pc = fst policy *)
508        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
509        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
510        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
511        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
512          [ @H @refl
513          | @le_to_not_lt @le_n
514          ]
515        | #x cases x -x #x1 #x2 #Heq #Hip #_ >nth_append_second
516          [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
517          >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
518          cases instr in Heq1;
519          [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
520            / by refl/
521          |4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
522            <(proj1 ?? (pair_destruct ?????? Heq1)) @refl
523          |1: #pi cases pi normalize nodelta
524            [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:
525              [1,2,3,6,7,24,25: #x #y
526              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
527              #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
528              / by /
529            |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
530              <(proj2 ?? (pair_destruct ?????? Heq1))
531              <(proj1 ?? (pair_destruct ?????? Heq1))
532              / by /
533            ]
534          ]
535        ]   
536      ]
537    ]
538  ]
539  | (* policy_safe *) cases daemon
540    (* #i >append_length >commutative_plus #Hi normalize in Hi;
541    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
542    [ >nth_append_first
543      [2: @Hi]
544      <(proj2 ?? (pair_destruct ?????? Heq2))
545      >lookup_insert_miss
546      [ >lookup_insert_miss
547        [ >lookup_insert_miss
548          [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
549            cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
550            #pc #j cases (nth i ? prefix 〈None ?, Comment []〉) #label #instr cases j
551            normalize nodelta
552            [ #H cases (le_to_or_lt_eq … Hi) -Hi #Hi
553              [ >lookup_insert_miss
554                [ #dest #Hjmp <(proj1 ?? (pair_destruct ?????? Heq2))
555
556      |
557      ]
558    |
559    ] *)
560  ]
561  | (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
562    [ cases (decidable_eq_nat 0 (|prefix|))
563      [ #Heq <Heq >lookup_insert_hit
564        (* USE: inc_pc = fst policy *)
565        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
566        (* USE: 0 ↦ 0 *)
567        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) <Heq
568        #ONE #TWO >TWO >ONE @refl
569      | #Hneq >lookup_insert_miss
570        [ (* USE: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
571        | @bitvector_of_nat_abs
572          [3: @Hneq]
573        ]
574      ]
575    | @bitvector_of_nat_abs
576      [3: @lt_to_not_eq / by / ]
577    ]     
578    [1,3: / by /
579    |2,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
580      [2: <plus_n_Sm @le_S_S]
581      @le_plus_n_r
582    ]
583  ]
584  | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
585    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
586  ]
587  | (* added = 0 → policy_pc_equal *)
588    (* USE: added = 0 → policy_pc_equal *)
589    lapply (proj2 ?? (proj1 ?? Hpolicy))
590    lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr)
591    cases daemon
592    (*cases instr in ⊢ (???% → % → % → %); normalize nodelta
593    [ #pi cases pi normalize nodelta
594      [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:
595        [1,2,3,6,7,24,25: #x #y
596        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
597        #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded
598        #i >append_length >commutative_plus #Hi normalize in Hi;
599        cases (le_to_or_lt_eq … Hi) -Hi #Hi
600        [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:
601          <(proj2 ?? (pair_destruct ?????? Heq2))
602          >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
603            (bitvector_of_nat 16 (S (|prefix|)))
604            (bitvector_of_nat 16 i))
605          [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:
606            (* le_to_or_lt_eq, part 2 *)
607            >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16
608              (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i))
609            [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:
610              @(Hold Hadded i (le_S_S_to_le … Hi))
611            |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:
612              @bitvector_of_nat_abs
613              [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:
614                @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
615                @le_S_S @le_plus_a @(le_S_S_to_le … Hi)
616              |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
617                @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
618                @le_plus_n_r
619              |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:
620                @lt_to_not_eq  @(le_S_to_le … Hi)
621              ]
622            ]
623          |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:
624            @bitvector_of_nat_abs
625            [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:
626              @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
627              @le_S_S @le_plus_a @le_S_to_le @(le_S_S_to_le … Hi)
628            |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
629              @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
630              @le_S_S @le_plus_n_r
631            |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:
632              @lt_to_not_eq @le_S_to_le @Hi
633            ]
634          ]
635        |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:
636           <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi)
637           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
638             (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat ? (|prefix|)))
639           [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:
640             >lookup_insert_hit
641             lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
642             [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:
643               >prf >nth_append_second
644               [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:
645                 <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
646               |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:
647                 @le_n
648               ]
649             |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
650               >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
651             |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:
652               cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
653               #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
654             ]
655           |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:
656             @bitvector_of_nat_abs
657             [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:
658               @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
659             |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
660               @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
661               @le_S_S @le_plus_n_r
662             |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:
663               @lt_to_not_eq @le_n
664             ]
665           ]
666         ]
667       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold
668         <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
669         #H #i >append_length >commutative_plus #Hi normalize in Hi;
670         cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
671         [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2))
672           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
673              (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
674           [1,3,5,7,9,11,13,15,17:
675             >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16
676               (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i))
677             [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi)
678             [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
679             ]
680             @bitvector_of_nat_abs
681             [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
682               >append_length >commutative_plus @le_S @le_plus_a @Hi
683             |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
684               >append_length @le_S <plus_n_Sm @le_S_S @le_plus_n_r
685             |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
686             ]
687           |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
688             [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
689               >append_length >commutative_plus @le_S @le_plus_a @Hi
690             |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
691               >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
692             |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
693             ]
694           ]
695         |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi
696           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
697              (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
698           [1,3,5,7,9,11,13,15,17: >lookup_insert_hit
699             <(proj1 ?? (pair_destruct ?????? Heq1))
700             >Holdeq normalize nodelta @sym_eq @blerpque
701             [3,6,9,12,15,18,21,24,27:
702               elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
703               [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
704               |2,4,6,8,10,12,14,16,18: #H @H
705               ]
706               / by I/
707             |2,5,8,11,14,17,20,23,26: / by I/
708             ]
709           |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
710             [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
711               >append_length @le_S_S @le_plus_n_r
712             |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
713               >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
714             |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S_S @le_n
715             ]
716           ]
717         ]
718       ]
719     |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2))
720       #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
721       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
722       [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
723         [1,3,5: >lookup_insert_miss
724           [1,3,5: @(Hold Hadded i Hi)
725           |2,4,6: @bitvector_of_nat_abs
726             [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length
727               >commutative_plus @le_S @le_plus_a @Hi
728             |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
729               @le_S <plus_n_Sm @le_S_S @le_plus_n_r
730             |3,6,9: @lt_to_not_eq @Hi
731             ]
732           ]
733         |2,4,6: @bitvector_of_nat_abs
734           [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length
735             >commutative_plus @le_S @le_plus_a @Hi
736           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
737             @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
738           |3,6,9: @lt_to_not_eq @le_S @Hi
739           ]
740         ]
741       |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
742         [1,3,5: >lookup_insert_hit
743           lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
744           [1,4,7: >prf >nth_append_second
745             [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
746             |2,4,6: @le_n
747             ]
748           |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
749           |3,6,9:
750             cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
751             #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
752           ]
753         |2,4,6: @bitvector_of_nat_abs
754           [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf
755             >append_length @le_S_S @le_plus_n_r
756           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf
757             >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
758           |3,6,9: @lt_to_not_eq @le_S_S @le_n
759           ]
760         ]
761       ]
762     |4,5: #x #Hins #Heq1 #Heq2 #Hold
763       <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
764       #H #i >append_length >commutative_plus #Hi normalize in Hi;
765       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
766       [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
767         [1,3: >lookup_insert_miss
768           [1,3: @(Hold ? i Hi)
769           [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
770           ]
771           @bitvector_of_nat_abs
772           [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
773             >commutative_plus @le_S @le_plus_a @Hi
774           |2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length
775             @le_S_S @le_plus_n_r
776           |3,6: @lt_to_not_eq @Hi
777           ]
778         |2,4: @bitvector_of_nat_abs
779           [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
780             >commutative_plus @le_S @le_plus_a @Hi
781           |2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length
782             @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
783           |3,6: @lt_to_not_eq @le_S @Hi
784           ]
785         ]
786       |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
787         [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
788           >Holdeq normalize nodelta @sym_eq @blerpque
789           [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
790             [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
791             |2,4: #H @H
792             ]
793             / by I/
794           |2,5: / by I/
795           ]
796         |2,4: @bitvector_of_nat_abs
797           [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
798             @le_S_S @le_plus_n_r
799           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
800             @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
801           |3,6,9: @lt_to_not_eq @le_S_S @le_n
802           ]
803         ]
804       ]
805     ]*)
806   ]
807 | (* policy_jump_equal → added = 0 *)
808   cases daemon
809 ]
810| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
811  [ #i cases i
812    [ #Hi2 @conj
813      [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
814      | >lookup_opt_insert_hit #H destruct (H)
815      ]
816    | -i #i #Hi2 @conj
817      [ #Hi >lookup_opt_insert_miss
818        [ / by refl/
819        | @bitvector_of_nat_abs
820          [ @Hi2
821          | / by /
822          | @sym_neq @lt_to_not_eq / by /
823          ]
824        ]
825      | #_ @le_S_S @le_O_n
826      ]
827    ] 
828  | #i cases i
829    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
830    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
831    ]
832  ]
833  | #i #Hi <(le_n_O_to_eq … Hi)
834    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
835    #a #b normalize nodelta %2 @refl
836  ]
837  | #i cases i
838    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
839    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
840    ]
841  ]
842  | #i cases i
843    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
844    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
845    ]
846  ]
847  | >lookup_insert_hit @refl
848  ]
849  | >lookup_insert_hit @refl
850  ]
851  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
852    (* USE: 0 ↦ 0 (from old_sigma *)
853    @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
854  ]
855  | #_ @refl
856  ]
857]
858qed.
Note: See TracBrowser for help on using the repository browser.