source: src/ASM/PolicyStep.ma @ 2101

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