source: src/ASM/PolicyStep.ma @ 2245

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

Temporary commit to have a backtracking point. Yes, I know this breaks
PolicyStep? temporarily.

File size: 73.3 KB
Line 
1include "ASM/PolicyFront.ma".
2include alias "basics/lists/list.ma".
3include alias "arithmetics/nat.ma".
4include alias "basics/logic.ma".
5
6lemma not_is_jump_to_destination_of_None:
7 ∀pi. ¬is_jump (Instruction pi) → destination_of pi = None ….
8 * try (#x #y #H) try (#y #H) try #H cases H %
9qed.
10
11lemma destination_of_None_to_is_jump_false:
12 ∀instr. destination_of instr = None … → is_jump' instr = false.
13 * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs)
14qed.
15
16lemma destination_of_Some_to_is_jump_true:
17 ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true.
18 #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs
19 destruct(abs)
20qed.
21
22lemma jump_expansion_step1:
23 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
24 ∀labels: label_map.
25 ∀old_sigma : ppc_pc_map.
26 ∀inc_added : ℕ.
27 ∀inc_pc_sigma : ppc_pc_map.
28 ∀label : (option Identifier).
29 ∀instr : pseudo_instruction.
30 ∀inc_pc : ℕ.
31 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
32 ∀old_length : jump_length.
33 ∀Hpolicy : not_jump_default prefix 〈inc_pc,inc_sigma〉.
34 ∀policy : ppc_pc_map.
35 ∀new_length : jump_length.
36 ∀isize : ℕ.
37 let add_instr ≝ match instr with
38  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
39  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
40  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
41  | _             ⇒ None ?
42  ] in
43 ∀Heq1 :
44  match add_instr with 
45   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
46   |Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉]
47   =〈new_length,isize〉.
48 ∀Heq2 :
49   〈inc_pc+isize,
50     insert … (bitvector_of_nat … (S (|prefix|)))
51      〈inc_pc+isize, \snd  (lookup … (bitvector_of_nat … (S (|prefix|))) (\snd  old_sigma) 〈O,short_jump〉)〉
52      (insert … (bitvector_of_nat … (|prefix|)) 〈inc_pc,new_length〉 inc_sigma)〉
53   = policy.
54  not_jump_default (prefix@[〈label,instr〉]) policy.
55 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
56 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2
57 #i >append_length <commutative_plus #Hi normalize in Hi;
58 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
59 [ <Heq2 >lookup_insert_miss
60   [ >lookup_insert_miss
61     [ >(nth_append_first ? i prefix ?? Hi)
62       @(Hpolicy i Hi)
63     | @bitvector_of_nat_abs try assumption
64       [ @(transitive_lt ??? Hi) assumption ]
65       @lt_to_not_eq @Hi
66     ]
67   | @bitvector_of_nat_abs try assumption
68     [ @(transitive_lt ??? Hi) assumption ]
69     @lt_to_not_eq @le_S @Hi
70   ]
71 | <Heq2 >Hi >lookup_insert_miss
72   [ >lookup_insert_hit cases instr in Heq1;
73     [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
74     |4,5: #x normalize nodelta #Heq1 >nth_append_second try %
75           <minus_n_n #abs cases abs
76     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
77         #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H;
78         >not_is_jump_to_destination_of_None in H; normalize nodelta // ]         
79   | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]]
80qed.
81
82lemma jump_expansion_step2:
83 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
84 ∀labels : label_map.
85 ∀old_sigma : ppc_pc_map.
86 ∀inc_pc : ℕ.
87 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
88 ∀Hpolicy1 :
89  \fst  (lookup … (bitvector_of_nat … O) inc_sigma 〈O,short_jump〉) = O.
90 ∀Hpolicy2:
91   inc_pc =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
92 ∀policy : ppc_pc_map.
93 ∀new_length : jump_length.
94 ∀isize : ℕ.
95 ∀Heq2 :
96  〈inc_pc+isize,
97   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
98   〈inc_pc+isize,
99   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
100               (\snd  old_sigma) 〈O,short_jump〉)〉
101   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
102    〈inc_pc,new_length〉 inc_sigma)〉
103   = policy.
104 \fst  (lookup … (bitvector_of_nat … O) (\snd  policy) 〈O,short_jump〉) = O.
105 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_pc
106 #inc_sigma #Hpolicy1 #Hpolicy2 #policy #new_length #isize #Heq2
107 <Heq2 >lookup_insert_miss
108 [ cases (decidable_eq_nat 0 (|prefix|))
109   [ #Heq <Heq >lookup_insert_hit >Hpolicy2 <Heq @Hpolicy1
110   | #Hneq >lookup_insert_miss
111     [ @Hpolicy1
112     | @bitvector_of_nat_abs try assumption @lt_O_S ]]
113 | @bitvector_of_nat_abs [ @lt_O_S | @prefix_ok1 | 3: @lt_to_not_eq @lt_O_S ] ]
114qed.
115
116lemma jump_expansion_step3:
117 ∀program.
118 ∀labels : label_map.
119 ∀old_sigma : Σpolicy:ppc_pc_map.not_jump_default program policy.
120 ∀prefix,x,tl. program=prefix@[x]@tl →
121 ∀inc_added : ℕ.
122 ∀inc_pc_sigma : ppc_pc_map.
123 ∀label : option Identifier.
124 ∀instr : pseudo_instruction.
125 ∀p1 : x≃〈label,instr〉.
126 ∀inc_pc : ℕ.
127 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
128 ∀old_pc : ℕ.
129 ∀old_length : jump_length.
130 ∀Holdeq :
131  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
132   〈O,short_jump〉 =〈old_pc,old_length〉.
133 ∀Hpolicy : jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉.
134 ∀policy : ppc_pc_map.
135 ∀new_length : jump_length.
136 ∀isize : ℕ.
137 ∀Heq1 :
138   match 
139   match instr
140    in pseudo_instruction
141    return λ_:pseudo_instruction.(option jump_length)
142    with 
143   [Instruction (i:(preinstruction Identifier))⇒
144    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
145    (|prefix|) i
146   |Comment (_:String)⇒None jump_length
147   |Cost (_:costlabel)⇒None jump_length
148   |Jmp (j:Identifier)⇒
149    Some jump_length
150    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
151   |Call (c:Identifier)⇒
152    Some jump_length
153    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
154   |Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length]
155    in option
156    return λ_:(option jump_length).(jump_length×ℕ)
157    with 
158   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
159   |Some (pl:jump_length)⇒
160    〈max_length old_length pl,
161    instruction_size_jmplen (max_length old_length pl) instr〉]
162   =〈new_length,isize〉.
163 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
164 ∀prefix_ok : |prefix|< 2 \sup 16.
165 ∀Heq2b :
166  〈inc_pc+isize,
167   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
168   〈inc_pc+isize,
169   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
170               (\snd  old_sigma) 〈O,short_jump〉)〉
171   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
172    〈inc_pc,new_length〉 inc_sigma)〉
173   =policy.
174 jump_increase (prefix@[〈label,instr〉]) old_sigma policy.
175 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label
176 #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy #policy #new_length
177 #isize #Heq1 #prefix_ok1 #prefix_ok #Heq2
178    #i >append_length >commutative_plus #Hi normalize in Hi;
179    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
180    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
181      [ (* USE[pass]: jump_increase *)
182        lapply (Hpolicy i (le_S_to_le … Hi))
183        <Heq2
184        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
185        [ >lookup_insert_miss
186          [ @pair_elim #pc #j #EQ2 #X @X
187          | @bitvector_of_nat_abs
188            [ @(transitive_lt ??? Hi) ]
189            [1,2: assumption
190            | @lt_to_not_eq @Hi
191            ]
192          ]
193        | @bitvector_of_nat_abs
194          [ @(transitive_lt ??? Hi) @le_S_to_le ]
195          [1,2: assumption
196          | @lt_to_not_eq @le_S @Hi
197          ]
198        ]
199      | >Hi <Heq2 >Holdeq normalize nodelta
200        cut (|prefix| < |program|)
201        [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] #lt_prefix_program
202        >lookup_insert_miss
203        [ >lookup_insert_hit normalize nodelta
204          inversion instr in Heq1; normalize nodelta
205          [4,5: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
206          | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
207            lapply (destination_of_None_to_is_jump_false pi)
208            lapply (destination_of_Some_to_is_jump_true pi)
209            cases (destination_of ?) normalize nodelta
210            [ #tgt #Hx
211            | #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
212            ]
213          |2,3,6: #x [3: #y] #Heqi ]
214          #Hj <(proj1 ?? (pair_destruct ?????? Hj))
215          lapply (pi2 ?? old_sigma (|prefix|) ??) try assumption
216          [1,3,5,7: >prf >nth_append_second try @le_n
217            <minus_n_n whd in match (nth ????); >p1 >Heqi
218            whd in match is_jump; normalize nodelta try % >Hx %
219          |*: >Holdeq #EQ2 >EQ2 %2 %]
220        | @bitvector_of_nat_abs
221          [ @le_S_to_le ]
222          [1,2: assumption
223          | @lt_to_not_eq @le_n
224          ]
225        ]
226      ]
227    | <Heq2 >Hi >lookup_insert_hit
228      normalize nodelta
229      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
230      #a #b normalize nodelta %2 @refl
231    ]
232qed.
233
234lemma jump_expansion_step4:
235 ∀labels : label_map.
236 ∀old_sigma : ppc_pc_map.
237 ∀prefix : list (option Identifier×pseudo_instruction).
238 ∀inc_added : ℕ.
239 ∀inc_pc_sigma : ppc_pc_map.
240 ∀label : option Identifier.
241 ∀instr : pseudo_instruction.
242 ∀inc_pc : ℕ.
243 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
244 ∀old_length : jump_length.
245 ∀Hpolicy1 : sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉.
246 ∀Hpolicy2: inc_pc
247    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma
248                 〈O,short_jump〉).
249 ∀Hpolicy3: out_of_program_none prefix 〈inc_pc,inc_sigma〉.
250 ∀policy : ppc_pc_map.
251 ∀new_length : jump_length.
252 ∀isize : ℕ.
253 ∀Heq1 :
254  match 
255   match instr
256    in pseudo_instruction
257    return λ_:pseudo_instruction.(option jump_length)
258    with 
259   [Instruction (i:(preinstruction Identifier))⇒
260    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
261    (|prefix|) i
262   |Comment (_:String)⇒None jump_length
263   |Cost (_:costlabel)⇒None jump_length
264   |Jmp (j:Identifier)⇒
265    Some jump_length
266    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
267   |Call (c:Identifier)⇒
268    Some jump_length
269    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
270   |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
271    in option
272    return λ_:(option jump_length).(jump_length×ℕ)
273    with 
274   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
275   |Some (pl:jump_length)⇒
276    〈max_length old_length pl,
277    instruction_size_jmplen (max_length old_length pl) instr〉]
278   =〈new_length,isize〉.
279 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
280 ∀prefix_ok : |prefix|< 2 \sup 16.
281 ∀Heq2b :
282   〈inc_pc+isize,
283   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
284   〈inc_pc+isize,
285   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
286               (\snd  old_sigma) 〈O,short_jump〉)〉
287   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
288    〈inc_pc,new_length〉 inc_sigma)〉
289   =policy.
290 sigma_compact_unsafe (prefix@[〈label,instr〉]) labels policy.
291 #labels #old_sigma #prefix #inc_added #inc_pc_sigma #label #instr #inc_pc #inc_sigma
292 #old_length #Hpolicy1 #Hpolicy2 #Hpolicy3 #policy #new_length #isize
293 #Heq1 #prefix_ok1 #prefix_ok #Heq2b
294    #i >append_length <commutative_plus #Hi normalize in Hi;
295    <Heq2b
296    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
297    [ >lookup_opt_insert_miss
298      [ >lookup_opt_insert_miss
299        [ >lookup_opt_insert_miss
300          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
301            [ >lookup_opt_insert_miss
302              [ (* USE[pass]: sigma_compact_unsafe *)
303                lapply (Hpolicy1 i ?)
304                [ @le_S_to_le @Hi ]
305                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
306                [ normalize nodelta #X @X
307                | #x cases x -x #x1 #x2
308                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
309                  normalize nodelta
310                  [ #X @X
311                  | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
312                    [ #X @X
313                    | @le_S_to_le @Hi
314                    ]
315                  ]
316                ]
317              | @bitvector_of_nat_abs
318                [3: @lt_to_not_eq @Hi ]
319              ]
320            | >Hi >lookup_opt_insert_hit normalize nodelta
321              (* USE[pass]: sigma_compact_unsafe *)
322              lapply (Hpolicy1 i ?)
323              [ <Hi @le_n
324              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
325                [ normalize nodelta #X @X
326                | #x cases x -x #x1 #x2
327                  (* USE: inc_pc = fst inc_sigma *)
328                  lapply Hpolicy2
329                  <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
330                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
331                  [ normalize nodelta #_  #_ #H cases H
332                  | #y cases y -y #y1 #y2 #Heq >nth_append_first
333                    [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
334                      #Heq2 <Heq2 #X @X
335                    | <Hi @le_n]]]]]]]]
336      [3,4,5: @bitvector_of_nat_abs]
337      [ @(transitive_lt ??? (le_S_S … Hi))
338      |3: @lt_to_not_eq @le_S_S @Hi
339      |4,7,10: @(transitive_lt ??? Hi) assumption
340      |5,11: @le_S_to_le
341      |6: @lt_to_not_eq @Hi
342      |9: @lt_to_not_eq @le_S @Hi
343      ]
344      assumption
345    | >Hi >lookup_opt_insert_miss
346      [2: @bitvector_of_nat_abs try assumption @lt_to_not_eq % ]
347      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
348      (* USE: out_of_program_none ← *)
349      lapply (Hpolicy3 i ?)
350      [ >Hi assumption
351      | >Hi
352        (* USE: inc_pc = fst policy *)
353        lapply Hpolicy2
354        inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma)
355        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
356          [ cases H #_ #X @X %
357          | @le_to_not_lt @le_n]
358        | * #x1 #x2 #Heq #Hip #_ >nth_append_second
359          [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
360          >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
361          cases instr in Heq1; normalize nodelta
362          [1: #pi cases (jump_expansion_step_instruction ??????) normalize nodelta]
363          try (#x #y #Heq1) try (#x #Heq1) try #Heq1
364          @eq_f <(proj2 ?? (pair_destruct ?????? Heq1))
365          try % <(proj1 ?? (pair_destruct ?????? Heq1)) %]]]
366qed.
367
368lemma jump_expansion_step5:
369 ∀labels : label_map.
370 ∀old_sigma : ppc_pc_map.
371 ∀prefix : list (option Identifier×pseudo_instruction).
372 ∀inc_added : ℕ.
373 ∀inc_pc_sigma : ppc_pc_map.
374 ∀label : option Identifier.
375 ∀instr : pseudo_instruction.
376 ∀inc_pc : ℕ.
377 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
378 ∀old_pc : ℕ.
379 ∀old_length : jump_length.
380 ∀Holdeq :
381  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
382   〈O,short_jump〉
383   =〈old_pc,old_length〉.
384 ∀Hpolicy1 : sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O.
385 ∀Hpolicy2: inc_pc
386    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
387 ∀added : ℕ.
388 ∀policy : ppc_pc_map.
389 ∀new_length : jump_length.
390 ∀isize : ℕ.
391 let add_instr ≝ match instr with
392  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
393  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
394  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
395  | _             ⇒ None ?
396  ] in
397 ∀Heq1 :
398  match add_instr with 
399   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
400   |Some (pl:jump_length)⇒
401    〈max_length old_length pl,
402    instruction_size_jmplen (max_length old_length pl) instr〉]
403   =〈new_length,isize〉.
404 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
405 ∀prefix_ok : |prefix|< 2 \sup 16.
406 ∀Heq2a :
407  match add_instr with 
408   [None⇒inc_added
409   |Some (x0:jump_length)⇒
410    inc_added+(isize-instruction_size_jmplen old_length instr)]
411   =added.
412 ∀Heq2b :
413  〈inc_pc+isize,
414   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
415   〈inc_pc+isize,
416   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
417               (\snd  old_sigma) 〈O,short_jump〉)〉
418   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
419    〈inc_pc,new_length〉 inc_sigma)〉
420   =policy.
421 sigma_jump_equal (prefix@[〈label,instr〉]) old_sigma policy→added=O.
422 #labels #old_sigma #prefix #inc_added #inc_pc #label #instr #inc_pc #inc_sigma
423 #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added #policy #new_length #isize
424 #Heq1 #prefix_ok1 #prefix_ok #Heq2a #Heq2b
425    <Heq2b #Heq <Heq2a
426    (* USE[pass]: policy_jump_equal → added = 0 *)
427    >Hpolicy1
428    [ cases instr in Heq1 Heq;
429      [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
430      |1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
431          normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]]
432      #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
433      #Heq (*CSC: make a lemma here!*) lapply Holdeq -Holdeq
434      (* USE: inc_pc = fst inc_sigma *)
435      >Hpolicy2
436      lapply (Heq (|prefix|) ?)
437      [1,3,5: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
438      -Heq >lookup_insert_miss
439      [1,3,5: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
440        #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
441        #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n %
442      |*: @bitvector_of_nat_abs try assumption @lt_to_not_eq %]
443    | #i #Hi lapply (Heq i ?)
444      [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi
445      | >lookup_insert_miss
446        [ >lookup_insert_miss
447          [ #X @X
448          | @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption
449            @lt_to_not_eq @Hi]
450        | @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption
451          @lt_to_not_eq @le_S @Hi ]]]
452qed.
453
454lemma jump_expansion_step6:
455 ∀program : list labelled_instruction.(*
456  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
457 ∀labels : label_map.(*
458  (Σlm:label_map
459   .(∀l:identifier ASMTag
460     .occurs_exactly_once ASMTag pseudo_instruction l program
461      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
462       =address_of_word_labels_code_mem program l))*)
463 ∀old_sigma :
464   Σpolicy:ppc_pc_map
465   .(*not_jump_default program policy
466    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
467                 〈O,short_jump〉)
468     =O
469    ∧\fst  policy
470     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
471                  (\snd  policy) 〈O,short_jump〉)
472    ∧*)sigma_compact_unsafe program labels policy
473    (*∧\fst  policy≤ 2 \sup 16*).
474 ∀prefix : list (option Identifier×pseudo_instruction).
475 ∀x : option Identifier×pseudo_instruction.
476 ∀tl : list (option Identifier×pseudo_instruction).
477 ∀prf : program=prefix@[x]@tl.(*
478 acc :
479  (Σx0:ℕ×ppc_pc_map
480   .(let 〈added,policy〉 ≝x0 in 
481     not_jump_default prefix policy
482     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
483                  〈O,short_jump〉)
484      =O
485     ∧\fst  policy
486      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
487                   (\snd  policy) 〈O,short_jump〉)
488     ∧jump_increase prefix old_sigma policy
489     ∧sigma_compact_unsafe prefix labels policy
490     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
491     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
492     ∧out_of_program_none prefix policy
493     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
494                  (\snd  policy) 〈O,short_jump〉)
495      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
496                   (\snd  old_sigma) 〈O,short_jump〉)
497       +added
498     ∧sigma_safe prefix labels added old_sigma policy))*)
499 ∀inc_added : ℕ.
500 ∀inc_pc_sigma : ppc_pc_map.(*
501 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
502 ∀label : option Identifier.
503 ∀instr : pseudo_instruction.
504 ∀p1 : x≃〈label,instr〉.(*
505 add_instr ≝
506  match instr
507   in pseudo_instruction
508   return λ_:pseudo_instruction.(option jump_length)
509   with 
510  [Instruction (i:(preinstruction Identifier))⇒
511   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
512   (|prefix|) i
513  |Comment (_:String)⇒None jump_length
514  |Cost (_:costlabel)⇒None jump_length
515  |Jmp (j:Identifier)⇒
516   Some jump_length
517   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
518  |Call (c:Identifier)⇒
519   Some jump_length
520   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
521  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]*)
522 ∀inc_pc : ℕ.
523 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.(*
524 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*)
525 ∀old_pc : ℕ.
526 ∀old_length : jump_length.
527 ∀Holdeq :
528  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
529   〈O,short_jump〉
530   =〈old_pc,old_length〉.
531 ∀Hpolicy1 :(*
532  (not_jump_default prefix 〈inc_pc,inc_sigma〉
533   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
534                〈O,short_jump〉)
535    =O
536   ∧inc_pc
537    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
538                 〈O,short_jump〉)
539   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
540   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
541   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
542   ∧( *)inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉.(*)
543   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
544   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
545                〈O,short_jump〉)
546    =old_pc+inc_added
547   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
548 ∀Hpolic2: inc_pc
549    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
550 ∀added : ℕ.
551 ∀policy : ppc_pc_map.
552 ∀new_length : jump_length.
553 ∀isize : ℕ.
554 let add_instr ≝ match instr with
555  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
556  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
557  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
558  | _             ⇒ None ?
559  ] in
560 ∀Heq1 :
561  match add_instr with 
562   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
563   |Some (pl:jump_length)⇒
564    〈max_length old_length pl,
565    instruction_size_jmplen (max_length old_length pl) instr〉]
566   =〈new_length,isize〉.
567 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
568 ∀prefix_ok : |prefix|< 2 \sup 16.
569 ∀Heq2a :
570  match add_instr with
571   [None⇒inc_added
572   |Some (x0:jump_length)⇒
573    inc_added+(isize-instruction_size_jmplen old_length instr)]
574   =added.
575 ∀Heq2b :
576  〈inc_pc+isize,
577   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
578   〈inc_pc+isize,
579   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
580               (\snd  old_sigma) 〈O,short_jump〉)〉
581   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
582    〈inc_pc,new_length〉 inc_sigma)〉
583   =policy.
584 added=O→sigma_pc_equal (prefix@[〈label,instr〉]) old_sigma policy.
585 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label
586 #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2
587 #added #policy #new_length #isize #Heq1 #prefix_ok #prefix_ok1 #Heq2a #Heq2b
588    (* USE[pass]: added = 0 → policy_pc_equal *)
589    lapply Hpolicy1 <Heq2b <Heq2a lapply Heq1 -Heq1
590    inversion instr normalize nodelta
591    [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
592      #Hi normalize in Hi;
593      cases (le_to_or_lt_eq … Hi) -Hi #Hi
594      [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
595        [1,3,5: <Heq2b >lookup_insert_miss
596          [1,3,5: >lookup_insert_miss
597            [1,3,5: @(Hold Hadded i (le_S_to_le … Hi))
598            |*: @bitvector_of_nat_abs try assumption
599              [2,4,6: @lt_to_not_eq @Hi
600              |*: @(transitive_lt ??? Hi) assumption ]]
601          |*: @bitvector_of_nat_abs try assumption
602            [2,4,6: @lt_to_not_eq @le_S @Hi
603            |*: @(transitive_lt … Hi) assumption ]]
604        |*: >Hi >lookup_insert_miss
605          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
606            @sym_eq (* USE: fst p = lookup |prefix| *)
607            @Hpolicy2
608          |*: @bitvector_of_nat_abs try assumption
609              @lt_to_not_eq %]]
610      |2,4,6: >Hi >lookup_insert_hit
611        (* USE fst p = lookup |prefix| *)
612        >Hpolicy2
613        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
614        (* USE: sigma_compact (from old_sigma) *)
615        lapply (pi2 ?? old_sigma (|prefix|) ?)
616        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
617        |*:
618          inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
619          [1,3,5: normalize nodelta #_ #ABS cases ABS
620          |*: inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
621            [1,3,5: normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS
622            |*: normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ
623              normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
624              >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
625              >prf >p1 >Hins >nth_append_second try %
626              <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
627                 #H >H @plus_left_monotone @instruction_size_irrelevant % ]]]]
628    |4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
629       #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
630       [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
631         [1,3: >lookup_insert_miss
632           [1,3: >lookup_insert_miss
633             [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded;
634               @plus_zero_zero
635             |2,4: @bitvector_of_nat_abs
636               [3,6: @lt_to_not_eq @Hi
637               |1,4: @(transitive_lt ??? Hi)
638               ]
639               assumption
640             ]
641           |2,4: @bitvector_of_nat_abs
642             [3,6: @lt_to_not_eq @le_S @Hi
643             |1,4: @(transitive_lt ??? Hi) assumption]
644             assumption ]
645         |2,4: >Hi >lookup_insert_miss
646           [1,3: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
647             [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
648             (* USE: fst p = lookup |prefix| *)
649             @Hpolicy2
650           |2,4: @bitvector_of_nat_abs try assumption
651             @lt_to_not_eq @le_n]]
652       |2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
653         elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
654         [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1))
655           @jump_length_le_max %
656         |*: #H (* USE: fst p = lookup |prefix| *)
657           >Hpolicy2
658           <(Hold ? (|prefix|) (le_n (|prefix|)))
659           [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
660             >(jump_length_equal_max … H) try %
661             (* USE: sigma_compact_unsafe (from old_sigma) *)
662             lapply (pi2 ?? old_sigma (|prefix|) ?)
663             [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
664             |2,4: inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
665               [1,3: normalize nodelta #_ #ABS cases ABS
666               |2,4: normalize nodelta
667                 inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
668                 [1,3: #_ * #pc #j normalize nodelta #_ #ABS cases ABS
669                 |2,4: * #Spc #Sj #EQS #x cases x -x #pc #j #EQ
670                   normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
671                   >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
672                   >EQpair @eq_f >prf >nth_append_second try %
673                   <minus_n_n >p1 whd in match (nth ????); >Hins
674                   >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ'
675                   >(proj2 … (pair_destruct … EQ')) % ]]]
676           |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded |*: skip]]]]
677     |1: #pi cases pi normalize nodelta
678      [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:
679        [1,2,3,6,7,24,25: #x #y
680        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
681        #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
682        cases (le_to_or_lt_eq … Hi) -Hi #Hi
683        [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:
684          cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
685          [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:
686            <(proj2 ?? (pair_destruct ?????? Heq2))
687            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
688            [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:
689              >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i) inc_sigma)
690              [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:
691                @(Hold Hadded i (le_S_to_le … Hi))
692              |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:
693                @bitvector_of_nat_abs
694                [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:
695                  @lt_to_not_eq @Hi
696                |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:
697                  @(transitive_lt ??? Hi)
698                ]
699                @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
700                @le_S_S <plus_n_Sm @le_S @le_plus_n_r
701              ]
702            |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:
703              @bitvector_of_nat_abs
704              [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:
705                @lt_to_not_eq @le_S @Hi
706              |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:
707                @(transitive_lt … Hi) @le_S_to_le
708              ]
709              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
710              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
711            ]
712          |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:
713            >Hi >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
714            [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:
715              >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq
716              (* USE: fst p = lookup |prefix| *)
717              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
718            |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:
719              @bitvector_of_nat_abs
720              [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:
721                @lt_to_not_eq @le_n
722              |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:
723                @le_S_to_le
724              ]
725              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
726                @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
727            ]
728          ]
729        |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:
730          >Hi >lookup_insert_hit
731          (* USE fst p = lookup |prefix| *)
732          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
733          <(Hold Hadded (|prefix|) (le_n (|prefix|)))
734          (* USE: sigma_compact (from old_sigma) *)
735          lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
736          [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:
737            >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
738          |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:
739            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
740            cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
741            [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:
742              normalize nodelta #_ #ABS cases ABS
743            |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:
744              lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
745              cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
746              [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:
747                normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
748              |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:
749                normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
750                normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
751                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
752                >prf >p1 >Hins >nth_append_second
753                [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:
754                  @(le_n (|prefix|))
755                |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:
756                  <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
757                  #H >H @plus_left_monotone @instruction_size_irrelevant @nmk #H @H
758                ]
759              ]
760            ]
761          ]
762        ]
763      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Hold #Hadded
764        #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
765        -Hi #Hi
766        [1,3,5,7,9,11,13,15,17: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
767          [1,3,5,7,9,11,13,15,17:
768            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
769            [1,3,5,7,9,11,13,15,17:
770              >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i) inc_sigma)
771              [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_to_le … Hi))
772                >commutative_plus in Hadded; @plus_zero_zero
773              |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
774                [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
775                |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi)
776                ]
777                @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
778                >append_length @le_plus_n_r
779              ]
780            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
781              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
782              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) @le_S_to_le
783              ]
784              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
785              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
786            ]
787          |2,4,6,8,10,12,14,16,18: >Hi
788            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
789            [1,3,5,7,9,11,13,15,17: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
790              [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
791              (* USE: fst p = lookup |prefix| *)
792              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
793            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
794              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
795              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
796              ]
797              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
798              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
799            ]
800          ]
801        |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
802          elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
803          [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt
804            <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max / by I/
805          |2,4,6,8,10,12,14,16,18: #H (* USE: fst p = lookup |prefix| *)
806            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
807            <(Hold ? (|prefix|) (le_n (|prefix|)))
808            [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
809              >(jump_length_equal_max … H)
810              [1,3,5,7,9,11,13,15,17: (* USE: sigma_compact_unsafe (from old_sigma) *)
811                lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
812                [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
813                |2,4,6,8,10,12,14,16,18: lapply Holdeq
814                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
815                  cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
816                  [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #ABS cases ABS
817                  |2,4,6,8,10,12,14,16,18: normalize nodelta
818                    lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
819                    cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
820                    [1,3,5,7,9,11,13,15,17: #_ #x cases x -x #pc #j normalize nodelta
821                      #_ #_ #ABS cases ABS
822                    |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x
823                      #pc #j #EQ
824                      normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
825                      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
826                      >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
827                      [1,3,5,7,9,11,13,15,17: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
828                      |2,4,6,8,10,12,14,16,18: @le_n
829                      ]
830                    ]
831                  ]
832                ]
833              |2,4,6,8,10,12,14,16,18: / by I/
834              ]
835            |2,4,6,8,10,12,14,16,18: @plus_zero_zero
836              [2,4,6,8,10,12,14,16,18: >commutative_plus @Hadded]
837            ]
838          ]
839        ]
840      ]
841    ]
842qed.
843
844lemma jump_expansion_step7:
845 ∀old_sigma : ppc_pc_map.
846 ∀prefix : list (option Identifier×pseudo_instruction).
847 ∀label : option Identifier.
848 ∀instr : pseudo_instruction.
849 ∀inc_pc : ℕ.
850 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
851 ∀Hpolicy1 : out_of_program_none prefix 〈inc_pc,inc_sigma〉.
852 ∀policy : ppc_pc_map.
853 ∀new_length : jump_length.
854 ∀isize : ℕ.
855 ∀Heq2b :
856  〈inc_pc+isize,
857   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
858   〈inc_pc+isize,
859   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
860               (\snd  old_sigma) 〈O,short_jump〉)〉
861   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
862    〈inc_pc,new_length〉 inc_sigma)〉
863   =policy.
864 out_of_program_none (prefix@[〈label,instr〉]) policy.
865 #old_sigma #prefix #label #instr #inc_pc #inc_sigma #Hpolicy1 #policy #new_length
866 #isize #Heq2b
867    #i #Hi2 >append_length <commutative_plus @conj
868    [ (* → *) #Hi normalize in Hi; <Heq2b >lookup_opt_insert_miss
869      [ >lookup_opt_insert_miss
870        [ cases (Hpolicy1 i Hi2) #X #_ @X @le_S_to_le @Hi
871        | @bitvector_of_nat_abs try assumption
872          [ @(transitive_lt … Hi2) @le_S_to_le assumption
873          | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n (S i)))
874            @(transitive_le … abs) %2 % ]]
875      | @bitvector_of_nat_abs try assumption
876          [ @(transitive_lt … Hi2) assumption
877          | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n i)) assumption ]]
878    | (* ← *) <Heq2b #Hl normalize
879      @(leb_elim (S i) (|prefix|))
880      [ #Hi
881        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
882        #Hl2 (* USE[pass]: out_of_program_none ← *)
883        cases (Hpolicy1 i Hi2) #_
884        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 assumption
885      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
886        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
887          [ #X @X
888          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
889          ]
890        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
891          >X >eq_bv_refl #H normalize in H; destruct (H)]]]
892qed.
893
894lemma jump_expansion_step8:
895 ∀program : list labelled_instruction.
896 ∀labels : label_map.
897 ∀old_sigma :
898  Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy ∧\fst  policy≤ 2 \sup 16.
899 ∀prefix : list (option Identifier×pseudo_instruction).
900 ∀x : option Identifier×pseudo_instruction.
901 ∀tl : list (option Identifier×pseudo_instruction).
902 ∀prf : program=prefix@[x]@tl.
903 ∀inc_added : ℕ.
904 ∀inc_pc_sigma : ppc_pc_map.
905 ∀label : option Identifier.
906 ∀instr : pseudo_instruction.
907 ∀p1 : x≃〈label,instr〉.
908 ∀inc_pc : ℕ.
909 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
910 ∀old_pc : ℕ.
911 ∀old_length : jump_length.
912 ∀Holdeq :
913  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
914   〈O,short_jump〉
915   =〈old_pc,old_length〉.
916 ∀Hpolicy1 : inc_pc
917    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
918 ∀Hpolicy2: \fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉)
919    =old_pc+inc_added.
920 ∀added : ℕ.
921 ∀policy : ppc_pc_map.
922 ∀new_length : jump_length.
923 ∀isize : ℕ.
924 let add_instr ≝ match instr with
925  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
926  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
927  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
928  | _             ⇒ None ?
929  ] in
930 ∀Heq1 :
931  match add_instr with 
932   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
933   |Some (pl:jump_length)⇒
934    〈max_length old_length pl,
935    instruction_size_jmplen (max_length old_length pl) instr〉]
936   =〈new_length,isize〉.
937 ∀Heq2a :
938  match add_instr with
939   [None⇒inc_added
940   |Some (x0:jump_length)⇒
941    inc_added+(isize-instruction_size_jmplen old_length instr)]
942   =added.
943 ∀Heq2b :
944  〈inc_pc+isize,
945   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
946   〈inc_pc+isize,
947   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
948               (\snd  old_sigma) 〈O,short_jump〉)〉
949   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
950    〈inc_pc,new_length〉 inc_sigma)〉
951   =policy.
952   \fst  (lookup (ℕ×jump_length) 16
953              (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd  policy)
954              〈O,short_jump〉)
955  =\fst  (lookup (ℕ×jump_length) 16
956               (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd  old_sigma)
957               〈O,short_jump〉)
958   +added.
959 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label #instr
960 #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added
961 #policy #new_length #isize #Heq1 #Heq2a #Heq2b
962    <Heq2b >append_length <plus_n_Sm <plus_n_O
963    >lookup_insert_hit
964    <Heq2a cases instr in p1 Heq1;
965    [1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
966        normalize nodelta lapply (destination_of_None_to_is_jump_false pi)
967        lapply (destination_of_Some_to_is_jump_true pi)
968        cases (destination_of ?) normalize nodelta ]
969    try (#x #y #z #p1 #Heq1) try (#x #y #p1 #Heq1) try (#x #p1 #Heq1) try (#p1 #Heq1)
970    <(proj2 ?? (pair_destruct ?????? Heq1))
971    (* USE: sigma_compact_unsafe (from old_sigma) *)
972    lapply (proj1 ?? (pi2 ?? old_sigma) (|prefix|) ?)
973    [1,3,5,7,9,11,13,15: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
974    lapply Holdeq -Holdeq
975    inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
976    [1,3,5,7,9,11,13,15: normalize nodelta #_ #_ #abs cases abs]
977    inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
978    [1,3,5,7,9,11,13,15: normalize nodelta #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs]
979    * #Spc #Sj #EQS * #pc #j #Holdeq #EQ normalize nodelta
980    #H (* USE: fst p = lookup |prefix| *) (*CSC: This part of the proof is repeated somewhere else*)
981    >Hpolicy1
982    (* USE[pass]: lookup p = lookup old_sigma + added *)
983    >Hpolicy2
984    [1,3,4,7:
985      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
986      -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
987      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second try %
988      <minus_n_n >p1 whd in match (nth ????); >associative_plus
989      >(associative_plus pc) @plus_left_monotone >commutative_plus
990      @plus_right_monotone @instruction_size_irrelevant try %
991      whd in match is_jump; normalize nodelta >y %
992    |2,5,6:
993      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H
994      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ
995      -Holdeq <(proj1 ?? (pair_destruct ?????? EQ))
996      >associative_plus
997      >(associative_plus pc) @plus_left_monotone >assoc_plus1
998      >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
999      [1,3,5: >(proj2 ?? (pair_destruct ?????? EQ)) >prf in old_sigma; #old_sigma
1000        >nth_append_second try %
1001        <minus_n_n whd in match (nth ????); >p1 in old_sigma; #old_sigma
1002        >commutative_plus @minus_plus_m_m
1003      |*: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max try %
1004        whd in match is_jump; normalize nodelta >y %]]
1005qed.
1006
1007lemma jump_expansion_step9:
1008(*
1009 program :
1010  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
1011 ∀labels : label_map.(*
1012  (Σlm:label_map
1013   .(∀l:identifier ASMTag
1014     .occurs_exactly_once ASMTag pseudo_instruction l program
1015      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
1016       =address_of_word_labels_code_mem program l))*)
1017 ∀old_sigma : ppc_pc_map.(*
1018  (Σpolicy:ppc_pc_map
1019   .not_jump_default program policy
1020    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
1021                 〈O,short_jump〉)
1022     =O
1023    ∧\fst  policy
1024     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
1025                  (\snd  policy) 〈O,short_jump〉)
1026    ∧sigma_compact_unsafe program labels policy
1027    ∧\fst  policy≤ 2 \sup 16 )*)
1028 ∀prefix : list (option Identifier×pseudo_instruction).(*
1029 x : (option Identifier×pseudo_instruction)
1030 tl : (list (option Identifier×pseudo_instruction))
1031 prf : (program=prefix@[x]@tl)
1032 acc :
1033  (Σx0:ℕ×ppc_pc_map
1034   .(let 〈added,policy〉 ≝x0 in 
1035     not_jump_default prefix policy
1036     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
1037                  〈O,short_jump〉)
1038      =O
1039     ∧\fst  policy
1040      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1041                   (\snd  policy) 〈O,short_jump〉)
1042     ∧jump_increase prefix old_sigma policy
1043     ∧sigma_compact_unsafe prefix labels policy
1044     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
1045     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
1046     ∧out_of_program_none prefix policy
1047     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1048                  (\snd  policy) 〈O,short_jump〉)
1049      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1050                   (\snd  old_sigma) 〈O,short_jump〉)
1051       +added
1052     ∧sigma_safe prefix labels added old_sigma policy))
1053 inc_added : ℕ
1054 inc_pc_sigma : ppc_pc_map
1055 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
1056 ∀label : option Identifier.
1057 ∀instr : pseudo_instruction.(*
1058 p1 : (x≃〈label,instr〉)
1059 add_instr ≝
1060  match instr
1061   in pseudo_instruction
1062   return λ_:pseudo_instruction.(option jump_length)
1063   with 
1064  [Instruction (i:(preinstruction Identifier))⇒
1065   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1066   (|prefix|) i
1067  |Comment (_:String)⇒None jump_length
1068  |Cost (_:costlabel)⇒None jump_length
1069  |Jmp (j:Identifier)⇒
1070   Some jump_length
1071   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1072  |Call (c:Identifier)⇒
1073   Some jump_length
1074   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1075  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
1076 inc_pc : ℕ
1077 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
1078 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
1079 old_pc : ℕ
1080 old_length : jump_length
1081 Holdeq :
1082  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
1083   〈O,short_jump〉
1084   =〈old_pc,old_length〉)
1085 Hpolicy :
1086  (not_jump_default prefix 〈inc_pc,inc_sigma〉
1087   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
1088                〈O,short_jump〉)
1089    =O
1090   ∧inc_pc
1091    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
1092                 〈O,short_jump〉)
1093   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
1094   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
1095   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
1096   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
1097   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
1098   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
1099                〈O,short_jump〉)
1100    =old_pc+inc_added
1101   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
1102 ∀added : ℕ.
1103 ∀policy : ppc_pc_map.(*
1104 new_length : jump_length
1105 isize : ℕ
1106 Heq1 :
1107  (match 
1108   match instr
1109    in pseudo_instruction
1110    return λ_:pseudo_instruction.(option jump_length)
1111    with 
1112   [Instruction (i:(preinstruction Identifier))⇒
1113    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1114    (|prefix|) i
1115   |Comment (_:String)⇒None jump_length
1116   |Cost (_:costlabel)⇒None jump_length
1117   |Jmp (j:Identifier)⇒
1118    Some jump_length
1119    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1120   |Call (c:Identifier)⇒
1121    Some jump_length
1122    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1123   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
1124    in option
1125    return λ_0:(option jump_length).(jump_length×ℕ)
1126    with 
1127   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
1128   |Some (pl:jump_length)⇒
1129    〈max_length old_length pl,
1130    instruction_size_jmplen (max_length old_length pl) instr〉]
1131   =〈new_length,isize〉)
1132 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
1133 prefix_ok : (|prefix|< 2 \sup 16 )
1134 Heq2a :
1135  (match 
1136   match instr
1137    in pseudo_instruction
1138    return λ_0:pseudo_instruction.(option jump_length)
1139    with 
1140   [Instruction (i:(preinstruction Identifier))⇒
1141    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1142    (|prefix|) i
1143   |Comment (_0:String)⇒None jump_length
1144   |Cost (_0:costlabel)⇒None jump_length
1145   |Jmp (j:Identifier)⇒
1146    Some jump_length
1147    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1148   |Call (c:Identifier)⇒
1149    Some jump_length
1150    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1151   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
1152    in option
1153    return λ_0:(option jump_length).ℕ
1154    with 
1155   [None⇒inc_added
1156   |Some (x0:jump_length)⇒
1157    inc_added+(isize-instruction_size_jmplen old_length instr)]
1158   =added)
1159 Heq2b :
1160  (〈inc_pc+isize,
1161   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
1162   〈inc_pc+isize,
1163   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
1164               (\snd  old_sigma) 〈O,short_jump〉)〉
1165   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1166    〈inc_pc,new_length〉 inc_sigma)〉
1167   =policy)
1168*)
1169 sigma_safe (prefix@[〈label,instr〉]) labels added old_sigma policy.
1170cases daemon(*
1171    #i >append_length >commutative_plus #Hi normalize in Hi;
1172    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
1173    [ >nth_append_first [2: @Hi]
1174      <Heq2b >lookup_insert_miss
1175      [ >lookup_insert_miss
1176        [ >lookup_insert_miss
1177          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
1178            [ >lookup_insert_miss
1179              [ (* USE[pass]: sigma_safe *)
1180                lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
1181                cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
1182                #pc #j normalize nodelta
1183                cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
1184                #Spc #Sj normalize nodelta
1185                cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
1186                #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj
1187                lapply (refl ? (leb (lookup_def … labels dest 0) (S (|prefix|))))
1188                cases (leb (lookup_def … labels dest 0) (S (|prefix|))) in ⊢ (???% → %); #H
1189                [ cases (le_to_or_lt_eq … (leb_true_to_le … H)) -H #H
1190                  [ >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
1191                    >lookup_insert_miss
1192                    [ cases (le_to_or_lt_eq … (le_S_S_to_le … H)) -H #H
1193                      [ >lookup_insert_miss
1194                        [ #H2 @H2
1195                        | @bitvector_of_nat_abs
1196                          [3: @lt_to_not_eq @H
1197                          |1: @(transitive_lt ??? H)
1198                          ]
1199                          @prefix_ok
1200                        ]
1201                      | >H >lookup_insert_hit
1202                        (* USE: inc_pc = lookup |prefix| *)
1203                        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1204                        #H2 @H2
1205                      ]
1206                    | @bitvector_of_nat_abs
1207                      [3: @lt_to_not_eq @H
1208                      |1: @(transitive_lt ??? H)
1209                      ]
1210                      @prefix_ok1
1211                    ]
1212                  | >H >lookup_insert_hit normalize nodelta
1213                    >(not_le_to_leb_false … (lt_to_not_le ?? (le_S_S ?? (le_n (|prefix|)))))
1214                    normalize nodelta
1215                    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1216                    #H2 >(proj2 ?? (proj1 ?? Hpolicy))
1217                  ]
1218                |
1219                       
1220                       
1221                       
1222                [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
1223                  [1,4,7: cases (decidable_le (lookup_def … labels dest 0) (S (|prefix|))) #H
1224                    [1,3,5: >(le_to_leb_true … H) normalize nodelta cases (le_to_or_lt_eq … H) -H #H
1225                      [1,3,5: >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
1226                        >lookup_insert_miss
1227                        [2,4,6: @bitvector_of_nat_abs
1228                          [3,6,9: @lt_to_not_eq @H
1229                          |1,4,7: @(transitive_lt ??? H)
1230                          ]
1231                          @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
1232                          @le_S_S >append_length <plus_n_Sm @le_S_S @le_plus_n_r
1233                        ]
1234                        cases (le_to_or_lt_eq … H) -H #H
1235                        [1,3,5: >lookup_insert_miss
1236                          [1,3,5: #H @H
1237                          |2,4,6: @bitvector_of_nat_abs
1238                            [3,6,9: @lt_to_not_eq @(le_S_S_to_le … H)
1239                            |1,4,7: @(transitive_lt ??? (le_S_S_to_le … H))
1240                            ]
1241                            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
1242                            >append_length @le_S_S @le_plus_n_r
1243                          ]
1244                        |2,4,6: >(injective_S … H) >lookup_insert_hit
1245                          (* USE: blerp *)
1246                          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1247                          #H @H
1248                        ]
1249                      |2,4,6: >H >lookup_insert_hit >(not_le_to_leb_false)
1250                        [2,4,6: @le_to_not_lt @le_n]
1251                        normalize nodelta
1252                        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
1253                        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
1254                         lapply (refl ? (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
1255                          cases (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
1256                          [1,3,5: normalize nodelta #_ #abs cases abs
1257                          |2,4,6: #x cases x -x #ppc #pj normalize nodelta #PEQ
1258                            lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
1259                            cases (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
1260                            [1,3,5: normalize nodelta #_ #abs cases abs
1261                            |2,4,6: #x cases x -x #Sppc #Spj normalize nodelta #SPEQ #Pcompact
1262                              >(lookup_opt_lookup_hit … SPEQ 〈0,short_jump〉)
1263                              >(lookup_opt_lookup_hit … PEQ 〈0,short_jump〉) in Holdeq;
1264                              #H >Pcompact >(proj1 ?? (pair_destruct ?????? H))
1265                              >commutative_plus >assoc_plus1 <(proj2 ?? (proj1 ?? Hpolicy))
1266                              <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1267                              >prf >nth_append_second
1268                              [1,3,5: <minus_n_n whd in match (nth ????); >p1
1269                                cases daemon (* to be lemmatized *)
1270                              |2,4,6: @le_n
1271                              ]
1272                            ]
1273                          ]
1274                        ]
1275                      |2,4,6: >(not_le_to_leb_false … H)
1276                        >not_le_to_leb_false
1277                        [2,4,6: @lt_to_not_le @le_S_to_le @not_le_to_lt @H
1278                        |1,3,5: normalize nodelta #H @H
1279                        ]
1280                      ]
1281                    |2,5,8: cases daemon (* like previous case *)
1282                    |3,6,9: cases daemon (* like previous case *)
1283                    ]
1284                  |4,5: #x normalize nodelta cases daemon (* blerp *)
1285                  |1: cases daemon (* blerp *)
1286                  ]
1287               
1288                               
1289                         
1290
1291   (*(\fst  (short_jump_cond (bitvector_of_nat 16 Spc)
1292              (bitvector_of_nat 16
1293               (inc_pc
1294                +instruction_size_jmplen
1295                 (max_length old_length
1296                  (select_jump_length labels old_sigma inc_pc_sigma inc_added
1297                   (|prefix|) xx)) (Jmp xx))))
1298  =true                   *)
1299                       
1300                 
1301  ]       
1302              [ >lookup_insert_miss
1303                [ (* USE[pass]: sigma_safe *)
1304                  lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
1305                  cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
1306                  #pc #j normalize nodelta
1307                  cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
1308                  #Spc #Sj normalize nodelta
1309                  cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
1310                  #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
1311                  [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
1312                    [1,4,7: *)
1313qed.
1314
1315(* One step in the search for a jump expansion fixpoint. *)
1316definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.
1317  S (|l|) < 2^16 ∧ is_well_labelled_p l).
1318  ∀labels:(Σlm:label_map.∀l.
1319    occurs_exactly_once ?? l program →
1320    bitvector_of_nat ? (lookup_def … lm l 0) =
1321    address_of_word_labels_code_mem program l).
1322  ∀old_policy:(Σpolicy:ppc_pc_map.
1323    (* out_of_program_none program policy *)
1324    And (And (And (And (not_jump_default program policy)
1325    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
1326    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
1327    (sigma_compact_unsafe program labels policy))
1328    (\fst policy ≤ 2^16)).
1329  (Σx:bool × (option ppc_pc_map).
1330    let 〈no_ch,y〉 ≝ x in
1331    match y with
1332    [ None ⇒ nec_plus_ultra program old_policy
1333    | Some p ⇒ And (And (And (And (And (And (And
1334       (not_jump_default program p)
1335       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
1336       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
1337       (jump_increase program old_policy p))
1338       (sigma_compact_unsafe program labels p))
1339       (sigma_jump_equal program old_policy p → no_ch = true))
1340       (no_ch = true → sigma_pc_equal program old_policy p))
1341       (\fst p ≤ 2^16)
1342    ])
1343    ≝
1344  λprogram.λlabels.λold_sigma.
1345  let 〈final_added, final_policy〉 ≝
1346    pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
1347    (λprefix.Σx:ℕ × ppc_pc_map.
1348      let 〈added,policy〉 ≝ x in
1349      And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
1350      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
1351      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
1352      (jump_increase prefix old_sigma policy))
1353      (sigma_compact_unsafe prefix labels policy))
1354      (sigma_jump_equal prefix old_sigma policy → added = 0))
1355      (added = 0 → sigma_pc_equal prefix old_sigma policy))
1356      (out_of_program_none prefix policy))
1357      (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) =
1358       \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added))
1359      (sigma_safe prefix labels added old_sigma policy))
1360    program
1361    (λprefix.λx.λtl.λprf.λacc.
1362      let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
1363      let 〈label,instr〉 ≝ x in
1364      (* Now, we must add the current ppc and its pc translation.
1365       * Three possibilities:
1366       *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
1367       *   - Instruction is a backward jump; we can use the sigma we're constructing,
1368       *     since it will already know the translation of its destination;
1369       *   - Instruction is a forward jump; we must use the old sigma (the new sigma
1370       *     does not know the translation yet), but compensate for the jumps we
1371       *     have lengthened.
1372       *)
1373      let add_instr ≝ match instr with
1374      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1375      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1376      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
1377      | _             ⇒ None ?
1378      ] in
1379      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
1380      let old_length ≝
1381        \snd (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
1382      let old_size ≝ instruction_size_jmplen old_length instr in
1383      let 〈new_length, isize〉 ≝ match add_instr with
1384      [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
1385      | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
1386      ] in
1387      let new_added ≝ match add_instr with
1388      [ None   ⇒ inc_added
1389      | Some x ⇒ plus inc_added (minus isize old_size)
1390      ] in
1391      let old_Slength ≝
1392        \snd (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
1393      let updated_sigma ≝
1394        (* we add the new PC to the next position and the new jump length to this one *)
1395        bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, old_Slength〉
1396        (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
1397      〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
1398    ) 〈0, 〈0,
1399      bvt_insert …
1400        (bitvector_of_nat ? 0)
1401        〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
1402        (Stub ??)〉〉
1403    ) in
1404    if gtb (\fst final_policy) 2^16 then
1405      〈eqb final_added 0, None ?〉
1406    else
1407      〈eqb final_added 0, Some ? final_policy〉.
1408[ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
1409  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
1410  (* USE: inc_pc = fst of policy (from fold) *)
1411  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1;
1412  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
1413  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
1414  #Hsig #Hge
1415  (* USE: added = 0 → policy_pc_equal (from fold) *)
1416  lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (|program|) (le_n (|program|)))
1417  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
1418    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
1419    inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
1420    [ #Hj
1421      (* USE: policy_increase (from fold) *)
1422      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
1423      lapply (Habs i Hi ?) [ >Hj %]
1424      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
1425      #opc #oj
1426      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉)
1427      #pc #j normalize nodelta #Heq >Heq cases j
1428      [1,2: #abs cases abs #abs2 try (cases abs2) @refl
1429      |3: #_ @refl
1430      ]
1431    | #Hnj
1432      (* USE: not_jump_default (from fold and old_sigma) *)
1433      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?)
1434      [2: >Hnj %]
1435      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try %
1436      >Hnj %
1437    ]
1438  | #abs >abs in Hsig; #Hsig
1439    @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
1440  ]
1441| normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
1442  >H2 in H; normalize nodelta -H2 -x #H @conj
1443  [ @conj [ @conj
1444  [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy,
1445     * jump_increase, sigma_compact_unsafe (from fold) *)
1446    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
1447  | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *)
1448    @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2
1449  ]
1450  | (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *)
1451     #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
1452  ]
1453  | @not_lt_to_le @ltb_false_to_not_lt @p1
1454  ]
1455|4: lapply (pi2 ?? acc) >p -acc inversion inc_pc_sigma
1456  #inc_pc #inc_sigma #Hips normalize nodelta
1457  inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
1458  #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
1459  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
1460  #Heq1 #Heq2
1461 cut (S (|prefix|) < 2^16)
1462 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length
1463   <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1
1464 cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok
1465 cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
1466  % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
1467  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
1468   * commented out for full proofs, but this needs a lot of memory and time *)
1469  [ (* not_jump_default *)
1470    @(jump_expansion_step1 … Heq1 Heq2b) try assumption
1471    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
1472  | (* 0 ↦ 0 *)
1473    @(jump_expansion_step2 … Heq2b) try assumption
1474    [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
1475    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ]
1476  | (* inc_pc = fst of policy *)
1477    <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
1478  | (* jump_increase *)
1479    @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq
1480      … Heq1 prefix_ok1 prefix_ok Heq2b)
1481    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
1482    cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
1483  | (* sigma_compact_unsafe *)
1484    @(jump_expansion_step4 … Heq1 … Heq2b) try assumption
1485    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1486    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))
1487    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
1488  | (* policy_jump_equal → added = 0 *)
1489    @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption
1490    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
1491    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1492  | (* added = 0 → policy_pc_equal *) cases daemon (*
1493    @(jump_expansion_step6 … Heq1 … Heq2b) try assumption
1494    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
1495    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1496    *)
1497  | (* out_of_program_none *)
1498    @(jump_expansion_step7 … Heq2b)
1499    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
1500  | (* lookup p = lookup old_sigma + added *)
1501    @(jump_expansion_step8 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 Heq2a Heq2b) try assumption
1502    [ cases (pi2 … old_sigma) * #_ #H1 #H2 % assumption
1503    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1504    | @(proj2 ?? (proj1 ?? Hpolicy)) ]
1505  | (* sigma_safe *) cases daemon (*
1506    @jump_expansion_step9 try assumption
1507    @(proj2 ?? Hpolicy) *)
1508  ]     
1509| normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
1510  [ #i cases i
1511    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1512    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
1513    ]
1514  | >lookup_insert_hit @refl
1515  | >lookup_insert_hit @refl
1516  | #i #Hi <(le_n_O_to_eq … Hi)
1517    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
1518    #a #b normalize nodelta %2 @refl
1519  | #i cases i
1520    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1521    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1522    ]
1523  | #_ %
1524  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
1525    (* USE: 0 ↦ 0 (from old_sigma) *)
1526    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
1527  | #i cases i
1528    [ #Hi2 @conj
1529      [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
1530      | >lookup_opt_insert_hit #H destruct (H)
1531      ]
1532    | -i #i #Hi2 @conj
1533      [ #Hi >lookup_opt_insert_miss
1534        [ / by refl/
1535        | @bitvector_of_nat_abs
1536          [ @Hi2
1537          | / by /
1538          | @sym_neq @lt_to_not_eq / by /
1539          ]
1540        ]
1541      | #_ @le_S_S @le_O_n
1542      ]
1543    ]
1544  | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *)
1545    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O %
1546  | #i cases i
1547    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1548    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1549    ]
1550  ]
1551]
1552qed.
Note: See TracBrowser for help on using the repository browser.