source: src/ASM/PolicyStep.ma @ 2141

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