source: src/ASM/PolicyStep.ma @ 2139

Last change on this file since 2139 was 2102, checked in by boender, 8 years ago
  • some small changes
File size: 42.8 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    (not_jump_default 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       (not_jump_default program p))
24       (jump_increase program old_policy p))
25       (no_ch = true → sigma_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 → sigma_pc_equal program old_policy p))
29       (sigma_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      (not_jump_default prefix policy))
40      (jump_increase prefix old_sigma policy))
41      (sigma_compact_unsafe prefix labels policy))
42      (sigma_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 → sigma_pc_equal prefix old_sigma policy))
46      (sigma_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: not_jump_default (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, not_jump_default, 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: @(label_in_program program labels x)
168                  cases daemon (* XXX this has to come from somewhere else *)
169                ]
170                [1,5: >(eqb_true_to_eq … Hch) <plus_n_O]
171                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
172                #result #flags normalize nodelta
173                cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
174                cases (get_index' bool 2 0 flags) normalize nodelta
175                [1,3,5,7: cases (eq_bv 9 upper ?)
176                |2,4,6,8: cases (eq_bv 9 upper (zero 9))]
177                [2,4,6,8,10,12,14,16: #H lapply (proj1 ?? H) #H3 destruct (H3)
178                |5,7,13,15: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
179                |1,3,9,11: #_ normalize nodelta @refl
180                ]
181             |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
182                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
183                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
184                normalize nodelta
185                (* USE: added = 0 → policy_pc_equal *)
186                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
187                [2,4,6,8: @(label_in_program program labels x)
188                  cases daemon (* XXX this has to come from somewhere else *)]
189                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
190                normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
191                cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
192                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
193                #result #flags normalize nodelta
194                cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
195                cases (get_index' bool 2 0 flags) normalize nodelta
196                #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
197             |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
198                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
199                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
200                normalize nodelta
201                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
202                [2,4,6,8: @(label_in_program program labels x)
203                  cases daemon (* XXX this has to come from somewhere else *)]
204                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
205                normalize nodelta
206                cases (vsplit bool 5 11 ?) #addr1 #addr2
207                cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
208                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
209                #result #flags normalize nodelta
210                cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
211                cases (get_index' bool 2 0 flags) normalize nodelta
212                #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
213             ]
214           |1: #pi cases pi
215             [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:
216               [1,2,3,6,7,24,25: #x #y
217               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
218               normalize nodelta #H @refl
219             |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
220               normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
221               #Hj lapply (Hj x (refl ? x)) -Hj
222               whd in match expand_relative_jump; normalize nodelta
223               whd in match expand_relative_jump_internal; normalize nodelta
224               whd in match expand_relative_jump_unsafe; normalize nodelta
225               whd in match expand_relative_jump_internal_unsafe;
226               normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
227               <(plus_n_Sm i 0) <plus_n_O
228               cases daemon (* XXX this needs subadressing mode magic, see above *)
229             ]
230           ]
231         ]
232       ]
233     ]
234   ]
235   | (* USE: 0 ↦ 0 (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
236   ]
237   | (* USE: inc_pc = fst of policy (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? H)))
238   ]
239   | #H2 (* USE: added = 0 → policy_pc_equal (from fold) *)
240     @(proj2 ?? (proj1 ?? H)) @eqb_true_to_eq @H2
241   ]
242   | #H2 (* USE: policy_jump_equal → added = 0 (from fold *)
243     @eq_to_eqb_true @(proj2 ?? H) @H2
244   ]
245   | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
246   ]
247|4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
248  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
249  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);
250  #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta
251  @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
252  @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
253  [ (* out_of_program_none *) #i #Hi2 >append_length <commutative_plus @conj
254    [ (* → *) #Hi normalize in Hi;
255      cases instr in Heq2; normalize nodelta
256      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
257      [1,3,5,7,9,11: >lookup_opt_insert_miss
258        [1,3,5,7,9,11: (* USE: out_of_program_none → *)
259          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2))
260          @le_S_to_le @Hi
261        |2,4,6,8,10,12: @bitvector_of_nat_abs
262          [1,4,7,10,13,16: @Hi2
263          |2,5,8,11,14,17: @(transitive_lt … Hi2)
264          |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
265          ] @le_S_to_le @Hi
266        ]
267      |2,4,6,8,10,12: @bitvector_of_nat_abs
268        [1,4,7,10,13,16: @Hi2
269        |2,5,8,11,14,17: @(transitive_lt … Hi2)
270        |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
271        ] @Hi
272      ]
273    | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
274      elim (decidable_lt i (|prefix|))
275      [ #Hi
276        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
277        #Hl2 (* USE: out_of_program_none ← *)
278        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2) Hl2)
279        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
280      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
281        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
282          [ / by /
283          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
284          ]
285        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
286          >X >eq_bv_refl #H normalize in H; destruct (H)
287        ]
288      ]
289    ]
290  | (* not_jump_default *) #i >append_length <commutative_plus #Hi normalize in Hi;
291    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
292    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
293      [ >lookup_insert_miss
294        [ >(nth_append_first ? i prefix ?? Hi)
295          (* USE: not_jump_default *)
296          @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi)
297        | @bitvector_of_nat_abs
298          [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
299            >commutative_plus @le_plus_a @Hi
300          | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
301            @le_plus_n_r
302          | @lt_to_not_eq @Hi
303          ]
304        ]
305      | @bitvector_of_nat_abs
306        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
307          >commutative_plus @le_plus_a @Hi
308        | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm
309          @le_S_S @le_plus_n_r
310        | @lt_to_not_eq @le_S @Hi
311        ]
312      ]
313    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
314      [ >lookup_insert_hit cases instr in Heq1;
315        [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
316        |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
317          [1,3: <minus_n_n whd in match (nth ????); / by I/
318          |2,4: @le_n
319          ]
320        |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
321          [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:
322            [1,2,3,6,7,24,25: #x #y
323            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
324            <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
325          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
326            #_ #H @⊥ cases H #H2 @H2 / by I/
327          ]
328        ]
329      | @bitvector_of_nat_abs
330        [ @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r
331        | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
332          @le_S_S @le_plus_n_r
333        | @lt_to_not_eq @le_n
334        ]
335      ]
336    ]
337  ]
338  | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
339    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
340    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
341      [ (* USE: policy_increase *)
342        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
343        <(proj2 ?? (pair_destruct ?????? Heq2))
344        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
345        [ >lookup_insert_miss
346          [ @pair_elim #pc #j #EQ2 / by /
347          | @bitvector_of_nat_abs
348            [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S
349              >commutative_plus @le_plus_a @Hi
350            | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
351            | @lt_to_not_eq @Hi
352            ]
353          ]
354        | @bitvector_of_nat_abs
355          [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus
356            @le_plus_a @Hi
357          | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r
358          | @lt_to_not_eq @le_S @Hi
359          ]
360        ]
361      | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) @pair_elim #opc #oj #EQ1
362        >lookup_insert_miss
363        [ >lookup_insert_hit cases (dec_is_jump instr)
364          [ cases instr in Heq1; normalize nodelta
365            [ #pi cases pi
366              [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:
367                [1,2,3,6,7,24,25: #x #y
368                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
369              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
370                whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
371                #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1; normalize nodelta
372                #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
373              ]
374            |2,3,6: #x [3: #y] #_ #Hj cases Hj
375            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1;
376              normalize nodelta #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
377            ]
378          | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
379            [ #pi cases pi
380              [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:
381                [1,2,3,6,7,24,25: #x #y
382                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
383                whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
384                #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
385                (* USE: not_jump_default (from old_sigma) *)
386                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
387                [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:
388                  >prf >nth_append_second
389                  [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:
390                    <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
391                  |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:
392                    @le_n
393                  ]
394                |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:
395                  >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
396                |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:
397                  cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
398                  #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2
399                  %2 @refl
400                ]
401              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
402                #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
403              ]
404            |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
405              (* USE: not_jump_default (from old_sigma) *)
406              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
407              [1,4,7: >prf >nth_append_second
408                [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
409                |2,4,6: @le_n
410                ]
411              |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
412              |3,6,9:
413                cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
414                #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2 %2 @refl
415              ]
416            |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
417            ]
418          ]
419        | @bitvector_of_nat_abs
420          [ @(transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r
421          | @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm
422            @le_S_S @le_plus_n_r
423          | @lt_to_not_eq @le_n
424          ]
425        ]
426      ]
427    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
428      normalize nodelta
429      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
430      #a #b normalize nodelta %2 @refl
431    ]
432  ]
433  | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
434    <(proj2 ?? (pair_destruct ?????? Heq2))
435    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
436    [ >lookup_opt_insert_miss
437      [ >lookup_opt_insert_miss
438        [ >lookup_opt_insert_miss
439          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
440            [ >lookup_opt_insert_miss
441              [ (* USE: policy_compact_unsafe *)
442                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
443                [ @le_S_to_le @Hi ]
444                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
445                [ normalize nodelta / by /
446                | #x cases x -x #x1 #x2
447                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
448                  normalize nodelta
449                  [ / by /
450                  | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
451                    [ / by /
452                    | @le_S_to_le @Hi
453                    ]
454                  ]
455                ]
456              | @bitvector_of_nat_abs
457                [3: @lt_to_not_eq @Hi ]
458              ]
459            | >Hi >lookup_opt_insert_hit normalize nodelta
460              (* USE: policy_compact_unsafe *)
461              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
462              [ <Hi @le_n
463              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
464                [ normalize nodelta / by /
465                | #x cases x -x #x1 #x2
466                  (* USE: inc_pc = fst inc_sigma *)
467                  lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Hi
468                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
469                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
470                  [ normalize nodelta #_  #_ #H cases H
471                  | #y cases y -y #y1 #y2 #Heq >nth_append_first
472                    [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
473                      #Heq2 <Heq2 / by /
474                    | <Hi @le_n
475                    ]
476                  ]
477                ]
478              ]
479            ]
480          ]
481        ]
482      ]
483      [3,4,5: @bitvector_of_nat_abs]
484      [1: (* Si < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
485        >commutative_plus @le_plus_a @Hi
486      |2,8: (* Spref < 2*16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
487        <plus_n_Sm @le_S_S @le_plus_n_r
488      | (* Si ≠ Spref *) @lt_to_not_eq @le_S_S @Hi
489      |4,7: (* i < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
490        >commutative_plus @le_plus_a @le_S_to_le @Hi
491      |5,11: (* pref < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
492        @le_plus_n_r
493      | @lt_to_not_eq @Hi
494      | @lt_to_not_eq @le_S_to_le @le_S_S @Hi
495      | @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
496        >commutative_plus @le_plus_a @Hi
497      ]
498    | >Hi >lookup_opt_insert_miss
499      [2: @bitvector_of_nat_abs
500        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
501        | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
502          <plus_n_Sm @le_S_S @le_plus_n_r
503        | @lt_to_not_eq @le_n
504        ]
505      ]
506      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
507      (* USE: out_of_program_none ← *)
508      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i ?))
509      [ >Hi @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
510      | >Hi
511        (* USE: inc_pc = fst policy *)
512        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
513        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
514        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
515        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
516          [ @H @refl
517          | @le_to_not_lt @le_n
518          ]
519        | #x cases x -x #x1 #x2 #Heq #Hip #_ >nth_append_second
520          [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
521          >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
522          cases instr in Heq1;
523          [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
524            / by refl/
525          |4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
526            <(proj1 ?? (pair_destruct ?????? Heq1)) @refl
527          |1: #pi cases pi normalize nodelta
528            [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:
529              [1,2,3,6,7,24,25: #x #y
530              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
531              #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
532              / by /
533            |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
534              <(proj2 ?? (pair_destruct ?????? Heq1))
535              <(proj1 ?? (pair_destruct ?????? Heq1))
536              / by /
537            ]
538          ]
539        ]   
540      ]
541    ]
542  ]
543  | (* policy_safe *) cases daemon
544    (* #i >append_length >commutative_plus #Hi normalize in Hi;
545    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
546    [ >nth_append_first
547      [2: @Hi]
548      <(proj2 ?? (pair_destruct ?????? Heq2))
549      >lookup_insert_miss
550      [ >lookup_insert_miss
551        [ >lookup_insert_miss
552          [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
553            cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
554            #pc #j cases (nth i ? prefix 〈None ?, Comment []〉) #label #instr cases j
555            normalize nodelta
556            [ #H cases (le_to_or_lt_eq … Hi) -Hi #Hi
557              [ >lookup_insert_miss
558                [ #dest #Hjmp <(proj1 ?? (pair_destruct ?????? Heq2))
559
560      |
561      ]
562    |
563    ] *)
564  ]
565  | (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
566    [ cases (decidable_eq_nat 0 (|prefix|))
567      [ #Heq <Heq >lookup_insert_hit
568        (* USE: inc_pc = fst policy *)
569        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
570        (* USE: 0 ↦ 0 *)
571        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) <Heq
572        #ONE #TWO >TWO >ONE @refl
573      | #Hneq >lookup_insert_miss
574        [ (* USE: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
575        | @bitvector_of_nat_abs
576          [3: @Hneq]
577        ]
578      ]
579    | @bitvector_of_nat_abs
580      [3: @lt_to_not_eq / by / ]
581    ]     
582    [1,3: / by /
583    |2,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
584      [2: <plus_n_Sm @le_S_S]
585      @le_plus_n_r
586    ]
587  ]
588  | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
589    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
590  ]
591  | (* added = 0 → policy_pc_equal *)
592    (* USE: added = 0 → policy_pc_equal *)
593    lapply (proj2 ?? (proj1 ?? Hpolicy))
594    lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr)
595    cases daemon
596    (*cases instr in ⊢ (???% → % → % → %); normalize nodelta
597    [ #pi cases pi normalize nodelta
598      [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:
599        [1,2,3,6,7,24,25: #x #y
600        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
601        #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded
602        #i >append_length >commutative_plus #Hi normalize in Hi;
603        cases (le_to_or_lt_eq … Hi) -Hi #Hi
604        [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:
605          <(proj2 ?? (pair_destruct ?????? Heq2))
606          >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
607            (bitvector_of_nat 16 (S (|prefix|)))
608            (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            (* le_to_or_lt_eq, part 2 *)
611            >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16
612              (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i))
613            [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:
614              @(Hold Hadded i (le_S_S_to_le … Hi))
615            |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:
616              @bitvector_of_nat_abs
617              [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:
618                @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
619                @le_S_S @le_plus_a @(le_S_S_to_le … Hi)
620              |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:
621                @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
622                @le_plus_n_r
623              |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:
624                @lt_to_not_eq  @(le_S_to_le … Hi)
625              ]
626            ]
627          |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:
628            @bitvector_of_nat_abs
629            [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:
630              @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
631              @le_S_S @le_plus_a @le_S_to_le @(le_S_S_to_le … Hi)
632            |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:
633              @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
634              @le_S_S @le_plus_n_r
635            |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:
636              @lt_to_not_eq @le_S_to_le @Hi
637            ]
638          ]
639        |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:
640           <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi)
641           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
642             (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat ? (|prefix|)))
643           [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:
644             >lookup_insert_hit
645             lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
646             [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:
647               >prf >nth_append_second
648               [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:
649                 <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
650               |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:
651                 @le_n
652               ]
653             |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:
654               >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
655             |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:
656               cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
657               #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
658             ]
659           |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:
660             @bitvector_of_nat_abs
661             [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:
662               @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
663             |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:
664               @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
665               @le_S_S @le_plus_n_r
666             |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:
667               @lt_to_not_eq @le_n
668             ]
669           ]
670         ]
671       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold
672         <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
673         #H #i >append_length >commutative_plus #Hi normalize in Hi;
674         cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
675         [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2))
676           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
677              (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
678           [1,3,5,7,9,11,13,15,17:
679             >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16
680               (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i))
681             [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi)
682             [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
683             ]
684             @bitvector_of_nat_abs
685             [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
686               >append_length >commutative_plus @le_S @le_plus_a @Hi
687             |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
688               >append_length @le_S <plus_n_Sm @le_S_S @le_plus_n_r
689             |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
690             ]
691           |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
692             [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
693               >append_length >commutative_plus @le_S @le_plus_a @Hi
694             |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
695               >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
696             |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
697             ]
698           ]
699         |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi
700           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
701              (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
702           [1,3,5,7,9,11,13,15,17: >lookup_insert_hit
703             <(proj1 ?? (pair_destruct ?????? Heq1))
704             >Holdeq normalize nodelta @sym_eq @blerpque
705             [3,6,9,12,15,18,21,24,27:
706               elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
707               [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
708               |2,4,6,8,10,12,14,16,18: #H @H
709               ]
710               / by I/
711             |2,5,8,11,14,17,20,23,26: / by I/
712             ]
713           |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
714             [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
715               >append_length @le_S_S @le_plus_n_r
716             |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
717               >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
718             |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S_S @le_n
719             ]
720           ]
721         ]
722       ]
723     |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2))
724       #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
725       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
726       [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
727         [1,3,5: >lookup_insert_miss
728           [1,3,5: @(Hold Hadded i Hi)
729           |2,4,6: @bitvector_of_nat_abs
730             [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length
731               >commutative_plus @le_S @le_plus_a @Hi
732             |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
733               @le_S <plus_n_Sm @le_S_S @le_plus_n_r
734             |3,6,9: @lt_to_not_eq @Hi
735             ]
736           ]
737         |2,4,6: @bitvector_of_nat_abs
738           [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length
739             >commutative_plus @le_S @le_plus_a @Hi
740           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
741             @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
742           |3,6,9: @lt_to_not_eq @le_S @Hi
743           ]
744         ]
745       |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
746         [1,3,5: >lookup_insert_hit
747           lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
748           [1,4,7: >prf >nth_append_second
749             [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
750             |2,4,6: @le_n
751             ]
752           |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
753           |3,6,9:
754             cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
755             #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
756           ]
757         |2,4,6: @bitvector_of_nat_abs
758           [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf
759             >append_length @le_S_S @le_plus_n_r
760           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf
761             >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
762           |3,6,9: @lt_to_not_eq @le_S_S @le_n
763           ]
764         ]
765       ]
766     |4,5: #x #Hins #Heq1 #Heq2 #Hold
767       <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
768       #H #i >append_length >commutative_plus #Hi normalize in Hi;
769       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
770       [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
771         [1,3: >lookup_insert_miss
772           [1,3: @(Hold ? i Hi)
773           [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
774           ]
775           @bitvector_of_nat_abs
776           [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
777             >commutative_plus @le_S @le_plus_a @Hi
778           |2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length
779             @le_S_S @le_plus_n_r
780           |3,6: @lt_to_not_eq @Hi
781           ]
782         |2,4: @bitvector_of_nat_abs
783           [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
784             >commutative_plus @le_S @le_plus_a @Hi
785           |2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length
786             @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
787           |3,6: @lt_to_not_eq @le_S @Hi
788           ]
789         ]
790       |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
791         [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
792           >Holdeq normalize nodelta @sym_eq @blerpque
793           [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
794             [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
795             |2,4: #H @H
796             ]
797             / by I/
798           |2,5: / by I/
799           ]
800         |2,4: @bitvector_of_nat_abs
801           [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
802             @le_S_S @le_plus_n_r
803           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
804             @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
805           |3,6,9: @lt_to_not_eq @le_S_S @le_n
806           ]
807         ]
808       ]
809     ]*)
810   ]
811 | (* policy_jump_equal → added = 0 *)
812   cases daemon
813 ]
814| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
815  [ #i cases i
816    [ #Hi2 @conj
817      [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
818      | >lookup_opt_insert_hit #H destruct (H)
819      ]
820    | -i #i #Hi2 @conj
821      [ #Hi >lookup_opt_insert_miss
822        [ / by refl/
823        | @bitvector_of_nat_abs
824          [ @Hi2
825          | / by /
826          | @sym_neq @lt_to_not_eq / by /
827          ]
828        ]
829      | #_ @le_S_S @le_O_n
830      ]
831    ] 
832  | #i cases i
833    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
834    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
835    ]
836  ]
837  | #i #Hi <(le_n_O_to_eq … Hi)
838    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
839    #a #b normalize nodelta %2 @refl
840  ]
841  | #i cases i
842    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
843    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
844    ]
845  ]
846  | #i cases i
847    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
848    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
849    ]
850  ]
851  | >lookup_insert_hit @refl
852  ]
853  | >lookup_insert_hit @refl
854  ]
855  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
856    (* USE: 0 ↦ 0 (from old_sigma *)
857    @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
858  ]
859  | #_ @refl
860  ]
861]
862qed.
Note: See TracBrowser for help on using the repository browser.