source: src/ASM/PolicyStep.ma @ 2241

Last change on this file since 2241 was 2241, checked in by boender, 8 years ago
  • merged changes by Claudio
File size: 91.9 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_Nome:
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 jump_expansion_step1:
12 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
13 ∀labels: label_map.
14 ∀old_sigma : ppc_pc_map.
15 ∀inc_added : ℕ.
16 ∀inc_pc_sigma : ppc_pc_map.
17 ∀label : (option Identifier).
18 ∀instr : pseudo_instruction.
19 ∀inc_pc : ℕ.
20 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
21 ∀old_length : jump_length.
22 ∀Hpolicy : not_jump_default prefix 〈inc_pc,inc_sigma〉.
23 ∀policy : ppc_pc_map.
24 ∀new_length : jump_length.
25 ∀isize : ℕ.
26 let add_instr ≝ match instr with
27  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
28  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
29  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
30  | _             ⇒ None ?
31  ] in
32 ∀Heq1 :
33  match add_instr with 
34   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
35   |Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉]
36   =〈new_length,isize〉.
37 ∀Heq2 :
38   〈inc_pc+isize,
39     insert … (bitvector_of_nat … (S (|prefix|)))
40      〈inc_pc+isize, \snd  (lookup … (bitvector_of_nat … (S (|prefix|))) (\snd  old_sigma) 〈O,short_jump〉)〉
41      (insert … (bitvector_of_nat … (|prefix|)) 〈inc_pc,new_length〉 inc_sigma)〉
42   = policy.
43  not_jump_default (prefix@[〈label,instr〉]) policy.
44 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
45 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2
46 #i >append_length <commutative_plus #Hi normalize in Hi;
47 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
48 [ <Heq2 >lookup_insert_miss
49   [ >lookup_insert_miss
50     [ >(nth_append_first ? i prefix ?? Hi)
51       @(Hpolicy i Hi)
52     | @bitvector_of_nat_abs try assumption
53       [ @(transitive_lt ??? Hi) assumption ]
54       @lt_to_not_eq @Hi
55     ]
56   | @bitvector_of_nat_abs try assumption
57     [ @(transitive_lt ??? Hi) assumption ]
58     @lt_to_not_eq @le_S @Hi
59   ]
60 | <Heq2 >Hi >lookup_insert_miss
61   [ >lookup_insert_hit cases instr in Heq1;
62     [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
63     |4,5: #x normalize nodelta #Heq1 >nth_append_second try %
64           <minus_n_n #abs cases abs
65     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
66         #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H;
67         >not_is_jump_to_destination_of_Nome in H; normalize nodelta // ]         
68   | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]]
69qed.
70
71lemma jump_expansion_step2:
72 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
73 ∀labels : label_map.
74 ∀old_sigma : ppc_pc_map.
75 ∀inc_pc : ℕ.
76 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
77 ∀Hpolicy1 :
78  \fst  (lookup … (bitvector_of_nat … O) inc_sigma 〈O,short_jump〉) = O.
79 ∀Hpolicy2:
80   inc_pc =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
81 ∀policy : ppc_pc_map.
82 ∀new_length : jump_length.
83 ∀isize : ℕ.
84 ∀Heq2 :
85  〈inc_pc+isize,
86   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
87   〈inc_pc+isize,
88   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
89               (\snd  old_sigma) 〈O,short_jump〉)〉
90   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
91    〈inc_pc,new_length〉 inc_sigma)〉
92   = policy.
93 \fst  (lookup … (bitvector_of_nat … O) (\snd  policy) 〈O,short_jump〉) = O.
94 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_pc
95 #inc_sigma #Hpolicy1 #Hpolicy2 #policy #new_length #isize #Heq2
96 <Heq2 >lookup_insert_miss
97 [ cases (decidable_eq_nat 0 (|prefix|))
98   [ #Heq <Heq >lookup_insert_hit >Hpolicy2 <Heq @Hpolicy1
99   | #Hneq >lookup_insert_miss
100     [ @Hpolicy1
101     | @bitvector_of_nat_abs try assumption @lt_O_S ]]
102 | @bitvector_of_nat_abs [ @lt_O_S | @prefix_ok1 | 3: @lt_to_not_eq @lt_O_S ] ]
103qed.
104
105lemma destination_of_None_to_is_jump_false:
106 ∀instr. destination_of instr = None … → is_jump' instr = false.
107 * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs)
108qed.
109
110lemma destination_of_Some_to_is_jump_true:
111 ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true.
112 #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs
113 destruct(abs)
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(*
456 program :
457  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
458 labels :
459  (Σlm:label_map
460   .(∀l:identifier ASMTag
461     .occurs_exactly_once ASMTag pseudo_instruction l program
462      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
463       =address_of_word_labels_code_mem program l))*)
464 ∀old_sigma : ppc_pc_map.(*
465  (Σpolicy:ppc_pc_map
466   .not_jump_default program policy
467    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
468                 〈O,short_jump〉)
469     =O
470    ∧\fst  policy
471     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
472                  (\snd  policy) 〈O,short_jump〉)
473    ∧sigma_compact_unsafe program labels policy
474    ∧\fst  policy≤ 2 \sup 16 )*)
475 ∀prefix : list (option Identifier×pseudo_instruction).(*
476 x : (option Identifier×pseudo_instruction)
477 tl : (list (option Identifier×pseudo_instruction))
478 prf : (program=prefix@[x]@tl)
479 acc :
480  (Σx0:ℕ×ppc_pc_map
481   .(let 〈added,policy〉 ≝x0 in 
482     not_jump_default prefix policy
483     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
484                  〈O,short_jump〉)
485      =O
486     ∧\fst  policy
487      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
488                   (\snd  policy) 〈O,short_jump〉)
489     ∧jump_increase prefix old_sigma policy
490     ∧sigma_compact_unsafe prefix labels policy
491     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
492     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
493     ∧out_of_program_none prefix policy
494     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
495                  (\snd  policy) 〈O,short_jump〉)
496      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
497                   (\snd  old_sigma) 〈O,short_jump〉)
498       +added
499     ∧sigma_safe prefix labels added old_sigma policy))
500 inc_added : ℕ
501 inc_pc_sigma : ppc_pc_map
502 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
503 ∀label : option Identifier.
504 ∀instr : pseudo_instruction.(*
505 p1 : (x≃〈label,instr〉)
506 add_instr ≝
507  match instr
508   in pseudo_instruction
509   return λ_:pseudo_instruction.(option jump_length)
510   with 
511  [Instruction (i:(preinstruction Identifier))⇒
512   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
513   (|prefix|) i
514  |Comment (_:String)⇒None jump_length
515  |Cost (_:costlabel)⇒None jump_length
516  |Jmp (j:Identifier)⇒
517   Some jump_length
518   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
519  |Call (c:Identifier)⇒
520   Some jump_length
521   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
522  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
523 inc_pc : ℕ
524 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
525 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
526 old_pc : ℕ
527 old_length : jump_length
528 Holdeq :
529  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
530   〈O,short_jump〉
531   =〈old_pc,old_length〉)
532 Hpolicy :
533  (not_jump_default prefix 〈inc_pc,inc_sigma〉
534   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
535                〈O,short_jump〉)
536    =O
537   ∧inc_pc
538    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
539                 〈O,short_jump〉)
540   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
541   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
542   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
543   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
544   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
545   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
546                〈O,short_jump〉)
547    =old_pc+inc_added
548   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
549 ∀added : ℕ.
550 ∀policy : ppc_pc_map.(*
551 new_length : jump_length
552 isize : ℕ
553 Heq1 :
554  (match 
555   match instr
556    in pseudo_instruction
557    return λ_:pseudo_instruction.(option jump_length)
558    with 
559   [Instruction (i:(preinstruction Identifier))⇒
560    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
561    (|prefix|) i
562   |Comment (_:String)⇒None jump_length
563   |Cost (_:costlabel)⇒None jump_length
564   |Jmp (j:Identifier)⇒
565    Some jump_length
566    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
567   |Call (c:Identifier)⇒
568    Some jump_length
569    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
570   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
571    in option
572    return λ_0:(option jump_length).(jump_length×ℕ)
573    with 
574   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
575   |Some (pl:jump_length)⇒
576    〈max_length old_length pl,
577    instruction_size_jmplen (max_length old_length pl) instr〉]
578   =〈new_length,isize〉)
579 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
580 prefix_ok : (|prefix|< 2 \sup 16 )
581 Heq2a :
582  (match 
583   match instr
584    in pseudo_instruction
585    return λ_0:pseudo_instruction.(option jump_length)
586    with 
587   [Instruction (i:(preinstruction Identifier))⇒
588    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
589    (|prefix|) i
590   |Comment (_0:String)⇒None jump_length
591   |Cost (_0:costlabel)⇒None jump_length
592   |Jmp (j:Identifier)⇒
593    Some jump_length
594    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
595   |Call (c:Identifier)⇒
596    Some jump_length
597    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
598   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
599    in option
600    return λ_0:(option jump_length).ℕ
601    with 
602   [None⇒inc_added
603   |Some (x0:jump_length)⇒
604    inc_added+(isize-instruction_size_jmplen old_length instr)]
605   =added)
606 Heq2b :
607  (〈inc_pc+isize,
608   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
609   〈inc_pc+isize,
610   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
611               (\snd  old_sigma) 〈O,short_jump〉)〉
612   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
613    〈inc_pc,new_length〉 inc_sigma)〉
614   =policy)
615*)
616 added=O→sigma_pc_equal (prefix@[〈label,instr〉]) old_sigma policy.
617cases daemon(*
618    (* USE[pass]: added = 0 → policy_pc_equal *)
619     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
620    <(proj2 ?? (pair_destruct ?????? Heq2))
621    <(proj1 ?? (pair_destruct ?????? Heq2))
622    lapply Heq1 -Heq1 lapply (refl ? instr)
623    cases instr in ⊢ (???% → % → %); normalize nodelta
624    [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
625      #Hi normalize in Hi;
626      cases (le_to_or_lt_eq … Hi) -Hi #Hi
627      [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
628        [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
629          [1,3,5: >lookup_insert_miss
630            [1,3,5: @(Hold Hadded i (le_S_to_le … Hi))
631            |2,4,6: @bitvector_of_nat_abs
632              [3,6,9: @lt_to_not_eq @Hi
633              |1,4,7: @(transitive_lt ??? Hi)
634              ]
635              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
636              @le_S_S <plus_n_Sm @le_S @le_plus_n_r
637            ]
638          |2,4,6: @bitvector_of_nat_abs
639            [3,6,9: @lt_to_not_eq @le_S @Hi
640            |1,4,7: @(transitive_lt … Hi) @le_S_to_le
641            ]
642            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
643              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
644          ]
645        |2,4,6: >Hi >lookup_insert_miss
646          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
647            @sym_eq (* USE: fst p = lookup |prefix| *)
648            @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
649          |2,4,6: @bitvector_of_nat_abs
650            [3,6,9: @lt_to_not_eq @le_n
651            |1,4,7: @le_S_to_le
652            ]
653            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
654              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
655          ]
656        ]
657      |2,4,6: >Hi >lookup_insert_hit
658        (* USE fst p = lookup |prefix| *)
659        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
660        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
661        (* USE: sigma_compact (from old_sigma) *)
662        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
663        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
664        |2,4,6:
665          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
666          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
667          [1,3,5: normalize nodelta #_ #ABS cases ABS
668          |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
669            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
670            [1,3,5: normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
671            |2,4,6: normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
672              normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
673              >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
674              >prf >p1 >Hins >nth_append_second
675              [2,4,6: @(le_n (|prefix|))
676              |1,3,5: <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
677                 #H >H @plus_left_monotone @instruction_size_irrelevant @nmk / by /
678              ]
679            ]
680          ]
681        ]
682      ]
683    |4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
684       #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
685       [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
686         [1,3: >lookup_insert_miss
687           [1,3: >lookup_insert_miss
688             [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded;
689               @plus_zero_zero
690             |2,4: @bitvector_of_nat_abs
691               [3,6: @lt_to_not_eq @Hi
692               |1,4: @(transitive_lt ??? Hi)
693               ]
694               @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
695               >append_length @le_plus_n_r
696             ]
697           |2,4: @bitvector_of_nat_abs
698             [3,6: @lt_to_not_eq @le_S @Hi
699             |1,4: @(transitive_lt ??? Hi) @le_S_to_le
700             ]
701             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
702             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
703           ]
704         |2,4: >Hi >lookup_insert_miss
705           [1,3: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
706             [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
707             (* USE: fst p = lookup |prefix| *)
708             @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
709           |2,4: @bitvector_of_nat_abs
710             [3,6: @lt_to_not_eq @le_n
711             |1,4: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
712             ]
713             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
714             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
715           ]
716         ]
717       |2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
718         elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
719         [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1))
720           @jump_length_le_max / by I/
721         |2,4: #H (* USE: fst p = lookup |prefix| *)
722           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
723           <(Hold ? (|prefix|) (le_n (|prefix|)))
724           [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
725             >(jump_length_equal_max … H)
726             [1,3: (* USE: sigma_compact_unsafe (from old_sigma) *)
727               lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
728               [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
729               |2,4: lapply Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
730                 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
731                 [1,3: normalize nodelta #_ #_ #ABS cases ABS
732                 |2,4: normalize nodelta
733                   lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
734                   cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
735                   [1,3: #_ #x cases x -x #pc #j normalize nodelta #_ #_ #ABS cases ABS
736                   |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
737                     normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
738                     >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
739                     >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
740                     [1,3: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
741                     |2,4: @le_n
742                     ]
743                   ]
744                 ]
745               ]
746             |2,4: / by I/
747             ]
748           |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded]
749           ]
750         ]
751       ]
752     |1: #pi cases pi normalize nodelta
753      [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:
754        [1,2,3,6,7,24,25: #x #y
755        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
756        #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
757        cases (le_to_or_lt_eq … Hi) -Hi #Hi
758        [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:
759          cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
760          [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:
761            <(proj2 ?? (pair_destruct ?????? Heq2))
762            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
763            [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:
764              >(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)
765              [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:
766                @(Hold Hadded i (le_S_to_le … Hi))
767              |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:
768                @bitvector_of_nat_abs
769                [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:
770                  @lt_to_not_eq @Hi
771                |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:
772                  @(transitive_lt ??? Hi)
773                ]
774                @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
775                @le_S_S <plus_n_Sm @le_S @le_plus_n_r
776              ]
777            |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:
778              @bitvector_of_nat_abs
779              [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:
780                @lt_to_not_eq @le_S @Hi
781              |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:
782                @(transitive_lt … Hi) @le_S_to_le
783              ]
784              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
785              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
786            ]
787          |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:
788            >Hi >(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,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
790              >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @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,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
794              @bitvector_of_nat_abs
795              [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:
796                @lt_to_not_eq @le_n
797              |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:
798                @le_S_to_le
799              ]
800              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
801                @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
802            ]
803          ]
804        |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:
805          >Hi >lookup_insert_hit
806          (* USE fst p = lookup |prefix| *)
807          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
808          <(Hold Hadded (|prefix|) (le_n (|prefix|)))
809          (* USE: sigma_compact (from old_sigma) *)
810          lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
811          [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:
812            >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
813          |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:
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,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
817              normalize nodelta #_ #ABS cases ABS
818            |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:
819              lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
820              cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
821              [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:
822                normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
823              |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:
824                normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
825                normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
826                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
827                >prf >p1 >Hins >nth_append_second
828                [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:
829                  @(le_n (|prefix|))
830                |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:
831                  <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
832                  #H >H @plus_left_monotone @instruction_size_irrelevant @nmk #H @H
833                ]
834              ]
835            ]
836          ]
837        ]
838      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Hold #Hadded
839        #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
840        -Hi #Hi
841        [1,3,5,7,9,11,13,15,17: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
842          [1,3,5,7,9,11,13,15,17:
843            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
844            [1,3,5,7,9,11,13,15,17:
845              >(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)
846              [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_to_le … Hi))
847                >commutative_plus in Hadded; @plus_zero_zero
848              |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
849                [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
850                |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi)
851                ]
852                @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
853                >append_length @le_plus_n_r
854              ]
855            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
856              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
857              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) @le_S_to_le
858              ]
859              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
860              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
861            ]
862          |2,4,6,8,10,12,14,16,18: >Hi
863            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
864            [1,3,5,7,9,11,13,15,17: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
865              [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
866              (* USE: fst p = lookup |prefix| *)
867              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
868            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
869              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
870              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
871              ]
872              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
873              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
874            ]
875          ]
876        |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
877          elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
878          [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt
879            <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max / by I/
880          |2,4,6,8,10,12,14,16,18: #H (* USE: fst p = lookup |prefix| *)
881            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
882            <(Hold ? (|prefix|) (le_n (|prefix|)))
883            [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
884              >(jump_length_equal_max … H)
885              [1,3,5,7,9,11,13,15,17: (* USE: sigma_compact_unsafe (from old_sigma) *)
886                lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
887                [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
888                |2,4,6,8,10,12,14,16,18: lapply Holdeq
889                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
890                  cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
891                  [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #ABS cases ABS
892                  |2,4,6,8,10,12,14,16,18: normalize nodelta
893                    lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
894                    cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
895                    [1,3,5,7,9,11,13,15,17: #_ #x cases x -x #pc #j normalize nodelta
896                      #_ #_ #ABS cases ABS
897                    |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x
898                      #pc #j #EQ
899                      normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
900                      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
901                      >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
902                      [1,3,5,7,9,11,13,15,17: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
903                      |2,4,6,8,10,12,14,16,18: @le_n
904                      ]
905                    ]
906                  ]
907                ]
908              |2,4,6,8,10,12,14,16,18: / by I/
909              ]
910            |2,4,6,8,10,12,14,16,18: @plus_zero_zero
911              [2,4,6,8,10,12,14,16,18: >commutative_plus @Hadded]
912            ]
913          ]
914        ]
915      ]
916    ]*)
917qed.
918
919lemma jump_expansion_step7:
920(*
921 program :
922  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
923 labels :
924  (Σlm:label_map
925   .(∀l:identifier ASMTag
926     .occurs_exactly_once ASMTag pseudo_instruction l program
927      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
928       =address_of_word_labels_code_mem program l))
929 old_sigma :
930  (Σpolicy:ppc_pc_map
931   .not_jump_default program policy
932    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
933                 〈O,short_jump〉)
934     =O
935    ∧\fst  policy
936     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
937                  (\snd  policy) 〈O,short_jump〉)
938    ∧sigma_compact_unsafe program labels policy
939    ∧\fst  policy≤ 2 \sup 16 )*)
940 ∀prefix : list (option Identifier×pseudo_instruction).(*
941 x : (option Identifier×pseudo_instruction)
942 tl : (list (option Identifier×pseudo_instruction))
943 prf : (program=prefix@[x]@tl)
944 acc :
945  (Σx0:ℕ×ppc_pc_map
946   .(let 〈added,policy〉 ≝x0 in 
947     not_jump_default prefix policy
948     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
949                  〈O,short_jump〉)
950      =O
951     ∧\fst  policy
952      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
953                   (\snd  policy) 〈O,short_jump〉)
954     ∧jump_increase prefix old_sigma policy
955     ∧sigma_compact_unsafe prefix labels policy
956     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
957     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
958     ∧out_of_program_none prefix policy
959     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
960                  (\snd  policy) 〈O,short_jump〉)
961      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
962                   (\snd  old_sigma) 〈O,short_jump〉)
963       +added
964     ∧sigma_safe prefix labels added old_sigma policy))
965 inc_added : ℕ
966 inc_pc_sigma : ppc_pc_map
967 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
968 ∀label : option Identifier.
969 ∀instr : pseudo_instruction.(*
970 p1 : (x≃〈label,instr〉)
971 add_instr ≝
972  match instr
973   in pseudo_instruction
974   return λ_:pseudo_instruction.(option jump_length)
975   with 
976  [Instruction (i:(preinstruction Identifier))⇒
977   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
978   (|prefix|) i
979  |Comment (_:String)⇒None jump_length
980  |Cost (_:costlabel)⇒None jump_length
981  |Jmp (j:Identifier)⇒
982   Some jump_length
983   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
984  |Call (c:Identifier)⇒
985   Some jump_length
986   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
987  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
988 inc_pc : ℕ
989 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
990 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
991 old_pc : ℕ
992 old_length : jump_length
993 Holdeq :
994  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
995   〈O,short_jump〉
996   =〈old_pc,old_length〉)
997 Hpolicy :
998  (not_jump_default prefix 〈inc_pc,inc_sigma〉
999   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
1000                〈O,short_jump〉)
1001    =O
1002   ∧inc_pc
1003    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
1004                 〈O,short_jump〉)
1005   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
1006   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
1007   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
1008   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
1009   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
1010   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
1011                〈O,short_jump〉)
1012    =old_pc+inc_added
1013   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)
1014 added : ℕ*)
1015 ∀policy : ppc_pc_map.(*
1016 new_length : jump_length
1017 isize : ℕ
1018 Heq1 :
1019  (match 
1020   match instr
1021    in pseudo_instruction
1022    return λ_:pseudo_instruction.(option jump_length)
1023    with 
1024   [Instruction (i:(preinstruction Identifier))⇒
1025    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1026    (|prefix|) i
1027   |Comment (_:String)⇒None jump_length
1028   |Cost (_:costlabel)⇒None jump_length
1029   |Jmp (j:Identifier)⇒
1030    Some jump_length
1031    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1032   |Call (c:Identifier)⇒
1033    Some jump_length
1034    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1035   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
1036    in option
1037    return λ_0:(option jump_length).(jump_length×ℕ)
1038    with 
1039   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
1040   |Some (pl:jump_length)⇒
1041    〈max_length old_length pl,
1042    instruction_size_jmplen (max_length old_length pl) instr〉]
1043   =〈new_length,isize〉)
1044 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
1045 prefix_ok : (|prefix|< 2 \sup 16 )
1046 Heq2a :
1047  (match 
1048   match instr
1049    in pseudo_instruction
1050    return λ_0:pseudo_instruction.(option jump_length)
1051    with 
1052   [Instruction (i:(preinstruction Identifier))⇒
1053    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1054    (|prefix|) i
1055   |Comment (_0:String)⇒None jump_length
1056   |Cost (_0:costlabel)⇒None jump_length
1057   |Jmp (j:Identifier)⇒
1058    Some jump_length
1059    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1060   |Call (c:Identifier)⇒
1061    Some jump_length
1062    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1063   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
1064    in option
1065    return λ_0:(option jump_length).ℕ
1066    with 
1067   [None⇒inc_added
1068   |Some (x0:jump_length)⇒
1069    inc_added+(isize-instruction_size_jmplen old_length instr)]
1070   =added)
1071 Heq2b :
1072  (〈inc_pc+isize,
1073   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
1074   〈inc_pc+isize,
1075   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
1076               (\snd  old_sigma) 〈O,short_jump〉)〉
1077   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1078    〈inc_pc,new_length〉 inc_sigma)〉
1079   =policy)
1080*)
1081 out_of_program_none (prefix@[〈label,instr〉]) policy.
1082cases daemon (*
1083    #i #Hi2 >append_length <commutative_plus @conj
1084    [ (* → *) #Hi normalize in Hi;
1085      cases instr in Heq2; normalize nodelta
1086      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
1087      [1,3,5,7,9,11: >lookup_opt_insert_miss
1088        [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *)
1089          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2))
1090          @le_S_to_le @Hi
1091        |2,4,6,8,10,12: @bitvector_of_nat_abs
1092          [1,4,7,10,13,16: @Hi2
1093          |2,5,8,11,14,17: @(transitive_lt … Hi2)
1094          |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
1095          ] @le_S_to_le @Hi
1096        ]
1097      |2,4,6,8,10,12: @bitvector_of_nat_abs
1098        [1,4,7,10,13,16: @Hi2
1099        |2,5,8,11,14,17: @(transitive_lt … Hi2)
1100        |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
1101        ] @Hi
1102      ]
1103    | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
1104      elim (decidable_lt i (|prefix|))
1105      [ #Hi
1106        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
1107        #Hl2 (* USE[pass]: out_of_program_none ← *)
1108        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2)
1109        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
1110      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
1111        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
1112          [ / by /
1113          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
1114          ]
1115        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
1116          >X >eq_bv_refl #H normalize in H; destruct (H)
1117        ]
1118      ]
1119    ]*)
1120qed.
1121
1122lemma jump_expansion_step8:
1123(*
1124 program :
1125  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
1126 labels :
1127  (Σlm:label_map
1128   .(∀l:identifier ASMTag
1129     .occurs_exactly_once ASMTag pseudo_instruction l program
1130      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
1131       =address_of_word_labels_code_mem program l))*)
1132 ∀old_sigma : ppc_pc_map.(*
1133  (Σpolicy:ppc_pc_map
1134   .not_jump_default program policy
1135    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
1136                 〈O,short_jump〉)
1137     =O
1138    ∧\fst  policy
1139     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
1140                  (\snd  policy) 〈O,short_jump〉)
1141    ∧sigma_compact_unsafe program labels policy
1142    ∧\fst  policy≤ 2 \sup 16 )*)
1143 ∀prefix : list (option Identifier×pseudo_instruction).(*
1144 x : (option Identifier×pseudo_instruction)
1145 tl : (list (option Identifier×pseudo_instruction))
1146 prf : (program=prefix@[x]@tl)
1147 acc :
1148  (Σx0:ℕ×ppc_pc_map
1149   .(let 〈added,policy〉 ≝x0 in 
1150     not_jump_default prefix policy
1151     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
1152                  〈O,short_jump〉)
1153      =O
1154     ∧\fst  policy
1155      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1156                   (\snd  policy) 〈O,short_jump〉)
1157     ∧jump_increase prefix old_sigma policy
1158     ∧sigma_compact_unsafe prefix labels policy
1159     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
1160     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
1161     ∧out_of_program_none prefix policy
1162     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1163                  (\snd  policy) 〈O,short_jump〉)
1164      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1165                   (\snd  old_sigma) 〈O,short_jump〉)
1166       +added
1167     ∧sigma_safe prefix labels added old_sigma policy))
1168 inc_added : ℕ
1169 inc_pc_sigma : ppc_pc_map
1170 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
1171 ∀label : option Identifier.
1172 ∀instr : pseudo_instruction.(*
1173 p1 : (x≃〈label,instr〉)
1174 add_instr ≝
1175  match instr
1176   in pseudo_instruction
1177   return λ_:pseudo_instruction.(option jump_length)
1178   with 
1179  [Instruction (i:(preinstruction Identifier))⇒
1180   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1181   (|prefix|) i
1182  |Comment (_:String)⇒None jump_length
1183  |Cost (_:costlabel)⇒None jump_length
1184  |Jmp (j:Identifier)⇒
1185   Some jump_length
1186   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1187  |Call (c:Identifier)⇒
1188   Some jump_length
1189   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1190  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
1191 inc_pc : ℕ
1192 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
1193 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
1194 old_pc : ℕ
1195 old_length : jump_length
1196 Holdeq :
1197  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
1198   〈O,short_jump〉
1199   =〈old_pc,old_length〉)
1200 Hpolicy :
1201  (not_jump_default prefix 〈inc_pc,inc_sigma〉
1202   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
1203                〈O,short_jump〉)
1204    =O
1205   ∧inc_pc
1206    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
1207                 〈O,short_jump〉)
1208   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
1209   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
1210   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
1211   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
1212   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
1213   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
1214                〈O,short_jump〉)
1215    =old_pc+inc_added
1216   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
1217 ∀added : ℕ.
1218 ∀policy : ppc_pc_map.(*
1219 new_length : jump_length
1220 isize : ℕ
1221 Heq1 :
1222  (match 
1223   match instr
1224    in pseudo_instruction
1225    return λ_:pseudo_instruction.(option jump_length)
1226    with 
1227   [Instruction (i:(preinstruction Identifier))⇒
1228    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1229    (|prefix|) i
1230   |Comment (_:String)⇒None jump_length
1231   |Cost (_:costlabel)⇒None jump_length
1232   |Jmp (j:Identifier)⇒
1233    Some jump_length
1234    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1235   |Call (c:Identifier)⇒
1236    Some jump_length
1237    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1238   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
1239    in option
1240    return λ_0:(option jump_length).(jump_length×ℕ)
1241    with 
1242   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
1243   |Some (pl:jump_length)⇒
1244    〈max_length old_length pl,
1245    instruction_size_jmplen (max_length old_length pl) instr〉]
1246   =〈new_length,isize〉)
1247 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
1248 prefix_ok : (|prefix|< 2 \sup 16 )
1249 Heq2a :
1250  (match 
1251   match instr
1252    in pseudo_instruction
1253    return λ_0:pseudo_instruction.(option jump_length)
1254    with 
1255   [Instruction (i:(preinstruction Identifier))⇒
1256    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1257    (|prefix|) i
1258   |Comment (_0:String)⇒None jump_length
1259   |Cost (_0:costlabel)⇒None jump_length
1260   |Jmp (j:Identifier)⇒
1261    Some jump_length
1262    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1263   |Call (c:Identifier)⇒
1264    Some jump_length
1265    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1266   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
1267    in option
1268    return λ_0:(option jump_length).ℕ
1269    with 
1270   [None⇒inc_added
1271   |Some (x0:jump_length)⇒
1272    inc_added+(isize-instruction_size_jmplen old_length instr)]
1273   =added)
1274 Heq2b :
1275  (〈inc_pc+isize,
1276   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
1277   〈inc_pc+isize,
1278   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
1279               (\snd  old_sigma) 〈O,short_jump〉)〉
1280   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1281    〈inc_pc,new_length〉 inc_sigma)〉
1282   =policy)
1283*)
1284   \fst  (lookup (ℕ×jump_length) 16
1285              (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd  policy)
1286              〈O,short_jump〉)
1287  =\fst  (lookup (ℕ×jump_length) 16
1288               (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd  old_sigma)
1289               〈O,short_jump〉)
1290   +added.
1291cases daemon(*
1292    <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O
1293    >lookup_insert_hit
1294    <(proj1 ?? (pair_destruct ?????? Heq2)) cases instr in p1 Heq1;
1295    [2,3,6: #x [3: #y] normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
1296      (* USE: sigma_compact_unsafe (from old_sigma) *)
1297      lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
1298      [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
1299      |2,4,6: lapply Holdeq -Holdeq
1300        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
1301        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
1302        [1,3,5: normalize nodelta #_ #_ #abs cases abs
1303        |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
1304          cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
1305          [1,3,5: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
1306          |2,4,6: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
1307            #H (* USE: fst p = lookup |prefix| *)
1308            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
1309            (* USE[pass]: lookup p = lookup old_sigma + added *)
1310            >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
1311            -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
1312            >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
1313            [1,3,5: <minus_n_n >p1 whd in match (nth ????); >associative_plus
1314              >(associative_plus pc) @plus_left_monotone >commutative_plus
1315              @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
1316            |2,4,6: @le_n
1317            ]
1318          ]
1319        ]
1320      ]
1321    |4,5: #x normalize nodelta #p1 #Heq1
1322      (* USE: sigma_compact_unsafe (from old_sigma) *)
1323      lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
1324      [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
1325      |2,4: lapply Holdeq -Holdeq
1326        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
1327        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
1328        [1,3: normalize nodelta #_ #_ #abs cases abs
1329        |2,4: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
1330          cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
1331          [1,3: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
1332          |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
1333            #H (* USE: fst p = lookup |prefix| *)
1334            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
1335            (* USE[pass]: lookup p = lookup old_sigma + added *)
1336            >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
1337            -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
1338            >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
1339            >(associative_plus pc) @plus_left_monotone >assoc_plus1
1340            >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
1341            [1,3: >(proj2 ?? (pair_destruct ?????? EQ)) >prf >nth_append_second
1342              [1,3: <minus_n_n whd in match (nth ????); >p1 >commutative_plus
1343                @minus_plus_m_m
1344              |2,4: @le_n
1345              ]
1346            |2,4: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max @I
1347            ]
1348          ]
1349        ]
1350      ]
1351    |1: #pi cases pi
1352      [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:
1353        [1,2,3,6,7,24,25: #x #y
1354        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
1355        normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
1356        (* USE: sigma_compact_unsafe (from old_sigma) *)
1357        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
1358        [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:
1359          >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
1360        |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:
1361          lapply Holdeq -Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
1362          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
1363          [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:
1364            normalize nodelta #_ #_ #abs cases abs
1365          |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:
1366            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
1367            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
1368            [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:
1369              normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
1370            |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:
1371              #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
1372              #H (* USE: fst p = lookup |prefix| *)
1373              >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
1374              (* USE[pass]: lookup p = lookup old_sigma + added *)
1375              >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
1376              -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
1377              >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
1378              [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:
1379                <minus_n_n >p1 whd in match (nth ????); >associative_plus
1380                >(associative_plus pc) @plus_left_monotone >commutative_plus
1381                @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
1382              |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:
1383                @le_n
1384              ]
1385            ]
1386          ]
1387        ]
1388      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta #p1 #Heq1
1389      (* USE: sigma_compact_unsafe (from old_sigma) *)
1390        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
1391        [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
1392        |2,4,6,8,10,12,14,16,18: lapply Holdeq -Holdeq
1393          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
1394          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
1395          [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs
1396          |2,4,6,8,10,12,14,16,18: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
1397            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
1398            [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #x cases x -x #Spc #Sj
1399              normalize nodelta #_ #_ #abs cases abs
1400            |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j
1401              #Holdeq #EQ normalize nodelta #H (* USE: fst p = lookup |prefix| *)
1402              >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
1403              (* USE[pass]: lookup p = lookup old_sigma + added *)
1404              >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
1405              -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
1406              >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
1407              >(associative_plus pc) @plus_left_monotone >assoc_plus1
1408              >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
1409              [1,3,5,7,9,11,13,15,17: >(proj2 ?? (pair_destruct ?????? EQ)) >prf
1410                >nth_append_second
1411                [1,3,5,7,9,11,13,15,17: <minus_n_n whd in match (nth ????); >p1
1412                  >commutative_plus @minus_plus_m_m
1413                |2,4,6,8,10,12,14,16,18: @le_n
1414                ]
1415              |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq1))
1416                @jump_length_le_max @I
1417              ]
1418            ]
1419          ]
1420        ]
1421      ]
1422    ] *)
1423qed.
1424
1425lemma jump_expansion_step9:
1426(*
1427 program :
1428  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
1429 ∀labels : label_map.(*
1430  (Σlm:label_map
1431   .(∀l:identifier ASMTag
1432     .occurs_exactly_once ASMTag pseudo_instruction l program
1433      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
1434       =address_of_word_labels_code_mem program l))*)
1435 ∀old_sigma : ppc_pc_map.(*
1436  (Σpolicy:ppc_pc_map
1437   .not_jump_default program policy
1438    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
1439                 〈O,short_jump〉)
1440     =O
1441    ∧\fst  policy
1442     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
1443                  (\snd  policy) 〈O,short_jump〉)
1444    ∧sigma_compact_unsafe program labels policy
1445    ∧\fst  policy≤ 2 \sup 16 )*)
1446 ∀prefix : list (option Identifier×pseudo_instruction).(*
1447 x : (option Identifier×pseudo_instruction)
1448 tl : (list (option Identifier×pseudo_instruction))
1449 prf : (program=prefix@[x]@tl)
1450 acc :
1451  (Σx0:ℕ×ppc_pc_map
1452   .(let 〈added,policy〉 ≝x0 in 
1453     not_jump_default prefix policy
1454     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
1455                  〈O,short_jump〉)
1456      =O
1457     ∧\fst  policy
1458      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1459                   (\snd  policy) 〈O,short_jump〉)
1460     ∧jump_increase prefix old_sigma policy
1461     ∧sigma_compact_unsafe prefix labels policy
1462     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
1463     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
1464     ∧out_of_program_none prefix policy
1465     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1466                  (\snd  policy) 〈O,short_jump〉)
1467      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1468                   (\snd  old_sigma) 〈O,short_jump〉)
1469       +added
1470     ∧sigma_safe prefix labels added old_sigma policy))
1471 inc_added : ℕ
1472 inc_pc_sigma : ppc_pc_map
1473 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
1474 ∀label : option Identifier.
1475 ∀instr : pseudo_instruction.(*
1476 p1 : (x≃〈label,instr〉)
1477 add_instr ≝
1478  match instr
1479   in pseudo_instruction
1480   return λ_:pseudo_instruction.(option jump_length)
1481   with 
1482  [Instruction (i:(preinstruction Identifier))⇒
1483   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1484   (|prefix|) i
1485  |Comment (_:String)⇒None jump_length
1486  |Cost (_:costlabel)⇒None jump_length
1487  |Jmp (j:Identifier)⇒
1488   Some jump_length
1489   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1490  |Call (c:Identifier)⇒
1491   Some jump_length
1492   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1493  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
1494 inc_pc : ℕ
1495 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
1496 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
1497 old_pc : ℕ
1498 old_length : jump_length
1499 Holdeq :
1500  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
1501   〈O,short_jump〉
1502   =〈old_pc,old_length〉)
1503 Hpolicy :
1504  (not_jump_default prefix 〈inc_pc,inc_sigma〉
1505   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
1506                〈O,short_jump〉)
1507    =O
1508   ∧inc_pc
1509    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
1510                 〈O,short_jump〉)
1511   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
1512   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
1513   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
1514   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
1515   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
1516   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
1517                〈O,short_jump〉)
1518    =old_pc+inc_added
1519   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
1520 ∀added : ℕ.
1521 ∀policy : ppc_pc_map.(*
1522 new_length : jump_length
1523 isize : ℕ
1524 Heq1 :
1525  (match 
1526   match instr
1527    in pseudo_instruction
1528    return λ_:pseudo_instruction.(option jump_length)
1529    with 
1530   [Instruction (i:(preinstruction Identifier))⇒
1531    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1532    (|prefix|) i
1533   |Comment (_:String)⇒None jump_length
1534   |Cost (_:costlabel)⇒None jump_length
1535   |Jmp (j:Identifier)⇒
1536    Some jump_length
1537    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1538   |Call (c:Identifier)⇒
1539    Some jump_length
1540    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1541   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
1542    in option
1543    return λ_0:(option jump_length).(jump_length×ℕ)
1544    with 
1545   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
1546   |Some (pl:jump_length)⇒
1547    〈max_length old_length pl,
1548    instruction_size_jmplen (max_length old_length pl) instr〉]
1549   =〈new_length,isize〉)
1550 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
1551 prefix_ok : (|prefix|< 2 \sup 16 )
1552 Heq2a :
1553  (match 
1554   match instr
1555    in pseudo_instruction
1556    return λ_0:pseudo_instruction.(option jump_length)
1557    with 
1558   [Instruction (i:(preinstruction Identifier))⇒
1559    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
1560    (|prefix|) i
1561   |Comment (_0:String)⇒None jump_length
1562   |Cost (_0:costlabel)⇒None jump_length
1563   |Jmp (j:Identifier)⇒
1564    Some jump_length
1565    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1566   |Call (c:Identifier)⇒
1567    Some jump_length
1568    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1569   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
1570    in option
1571    return λ_0:(option jump_length).ℕ
1572    with 
1573   [None⇒inc_added
1574   |Some (x0:jump_length)⇒
1575    inc_added+(isize-instruction_size_jmplen old_length instr)]
1576   =added)
1577 Heq2b :
1578  (〈inc_pc+isize,
1579   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
1580   〈inc_pc+isize,
1581   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
1582               (\snd  old_sigma) 〈O,short_jump〉)〉
1583   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
1584    〈inc_pc,new_length〉 inc_sigma)〉
1585   =policy)
1586*)
1587 sigma_safe (prefix@[〈label,instr〉]) labels added old_sigma policy.
1588cases daemon(*
1589    #i >append_length >commutative_plus #Hi normalize in Hi;
1590    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
1591    [ >nth_append_first [2: @Hi]
1592      <Heq2b >lookup_insert_miss
1593      [ >lookup_insert_miss
1594        [ >lookup_insert_miss
1595          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
1596            [ >lookup_insert_miss
1597              [ (* USE[pass]: sigma_safe *)
1598                lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
1599                cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
1600                #pc #j normalize nodelta
1601                cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
1602                #Spc #Sj normalize nodelta
1603                cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
1604                #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj
1605                lapply (refl ? (leb (lookup_def … labels dest 0) (S (|prefix|))))
1606                cases (leb (lookup_def … labels dest 0) (S (|prefix|))) in ⊢ (???% → %); #H
1607                [ cases (le_to_or_lt_eq … (leb_true_to_le … H)) -H #H
1608                  [ >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
1609                    >lookup_insert_miss
1610                    [ cases (le_to_or_lt_eq … (le_S_S_to_le … H)) -H #H
1611                      [ >lookup_insert_miss
1612                        [ #H2 @H2
1613                        | @bitvector_of_nat_abs
1614                          [3: @lt_to_not_eq @H
1615                          |1: @(transitive_lt ??? H)
1616                          ]
1617                          @prefix_ok
1618                        ]
1619                      | >H >lookup_insert_hit
1620                        (* USE: inc_pc = lookup |prefix| *)
1621                        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1622                        #H2 @H2
1623                      ]
1624                    | @bitvector_of_nat_abs
1625                      [3: @lt_to_not_eq @H
1626                      |1: @(transitive_lt ??? H)
1627                      ]
1628                      @prefix_ok1
1629                    ]
1630                  | >H >lookup_insert_hit normalize nodelta
1631                    >(not_le_to_leb_false … (lt_to_not_le ?? (le_S_S ?? (le_n (|prefix|)))))
1632                    normalize nodelta
1633                    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1634                    #H2 >(proj2 ?? (proj1 ?? Hpolicy))
1635                  ]
1636                |
1637                       
1638                       
1639                       
1640                [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
1641                  [1,4,7: cases (decidable_le (lookup_def … labels dest 0) (S (|prefix|))) #H
1642                    [1,3,5: >(le_to_leb_true … H) normalize nodelta cases (le_to_or_lt_eq … H) -H #H
1643                      [1,3,5: >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
1644                        >lookup_insert_miss
1645                        [2,4,6: @bitvector_of_nat_abs
1646                          [3,6,9: @lt_to_not_eq @H
1647                          |1,4,7: @(transitive_lt ??? H)
1648                          ]
1649                          @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
1650                          @le_S_S >append_length <plus_n_Sm @le_S_S @le_plus_n_r
1651                        ]
1652                        cases (le_to_or_lt_eq … H) -H #H
1653                        [1,3,5: >lookup_insert_miss
1654                          [1,3,5: #H @H
1655                          |2,4,6: @bitvector_of_nat_abs
1656                            [3,6,9: @lt_to_not_eq @(le_S_S_to_le … H)
1657                            |1,4,7: @(transitive_lt ??? (le_S_S_to_le … H))
1658                            ]
1659                            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
1660                            >append_length @le_S_S @le_plus_n_r
1661                          ]
1662                        |2,4,6: >(injective_S … H) >lookup_insert_hit
1663                          (* USE: blerp *)
1664                          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1665                          #H @H
1666                        ]
1667                      |2,4,6: >H >lookup_insert_hit >(not_le_to_leb_false)
1668                        [2,4,6: @le_to_not_lt @le_n]
1669                        normalize nodelta
1670                        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
1671                        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
1672                         lapply (refl ? (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
1673                          cases (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
1674                          [1,3,5: normalize nodelta #_ #abs cases abs
1675                          |2,4,6: #x cases x -x #ppc #pj normalize nodelta #PEQ
1676                            lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
1677                            cases (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
1678                            [1,3,5: normalize nodelta #_ #abs cases abs
1679                            |2,4,6: #x cases x -x #Sppc #Spj normalize nodelta #SPEQ #Pcompact
1680                              >(lookup_opt_lookup_hit … SPEQ 〈0,short_jump〉)
1681                              >(lookup_opt_lookup_hit … PEQ 〈0,short_jump〉) in Holdeq;
1682                              #H >Pcompact >(proj1 ?? (pair_destruct ?????? H))
1683                              >commutative_plus >assoc_plus1 <(proj2 ?? (proj1 ?? Hpolicy))
1684                              <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1685                              >prf >nth_append_second
1686                              [1,3,5: <minus_n_n whd in match (nth ????); >p1
1687                                cases daemon (* to be lemmatized *)
1688                              |2,4,6: @le_n
1689                              ]
1690                            ]
1691                          ]
1692                        ]
1693                      |2,4,6: >(not_le_to_leb_false … H)
1694                        >not_le_to_leb_false
1695                        [2,4,6: @lt_to_not_le @le_S_to_le @not_le_to_lt @H
1696                        |1,3,5: normalize nodelta #H @H
1697                        ]
1698                      ]
1699                    |2,5,8: cases daemon (* like previous case *)
1700                    |3,6,9: cases daemon (* like previous case *)
1701                    ]
1702                  |4,5: #x normalize nodelta cases daemon (* blerp *)
1703                  |1: cases daemon (* blerp *)
1704                  ]
1705               
1706                               
1707                         
1708
1709   (*(\fst  (short_jump_cond (bitvector_of_nat 16 Spc)
1710              (bitvector_of_nat 16
1711               (inc_pc
1712                +instruction_size_jmplen
1713                 (max_length old_length
1714                  (select_jump_length labels old_sigma inc_pc_sigma inc_added
1715                   (|prefix|) xx)) (Jmp xx))))
1716  =true                   *)
1717                       
1718                 
1719  ]       
1720              [ >lookup_insert_miss
1721                [ (* USE[pass]: sigma_safe *)
1722                  lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
1723                  cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
1724                  #pc #j normalize nodelta
1725                  cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
1726                  #Spc #Sj normalize nodelta
1727                  cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
1728                  #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
1729                  [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
1730                    [1,4,7: *)
1731qed.
1732
1733(* One step in the search for a jump expansion fixpoint. *)
1734definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.
1735  S (|l|) < 2^16 ∧ is_well_labelled_p l).
1736  ∀labels:(Σlm:label_map.∀l.
1737    occurs_exactly_once ?? l program →
1738    bitvector_of_nat ? (lookup_def … lm l 0) =
1739    address_of_word_labels_code_mem program l).
1740  ∀old_policy:(Σpolicy:ppc_pc_map.
1741    (* out_of_program_none program policy *)
1742    And (And (And (And (not_jump_default program policy)
1743    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
1744    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
1745    (sigma_compact_unsafe program labels policy))
1746    (\fst policy ≤ 2^16)).
1747  (Σx:bool × (option ppc_pc_map).
1748    let 〈no_ch,y〉 ≝ x in
1749    match y with
1750    [ None ⇒ nec_plus_ultra program old_policy
1751    | Some p ⇒ And (And (And (And (And (And (And
1752       (not_jump_default program p)
1753       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
1754       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
1755       (jump_increase program old_policy p))
1756       (sigma_compact_unsafe program labels p))
1757       (sigma_jump_equal program old_policy p → no_ch = true))
1758       (no_ch = true → sigma_pc_equal program old_policy p))
1759       (\fst p ≤ 2^16)
1760    ])
1761    ≝
1762  λprogram.λlabels.λold_sigma.
1763  let 〈final_added, final_policy〉 ≝
1764    pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
1765    (λprefix.Σx:ℕ × ppc_pc_map.
1766      let 〈added,policy〉 ≝ x in
1767      And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
1768      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
1769      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
1770      (jump_increase prefix old_sigma policy))
1771      (sigma_compact_unsafe prefix labels policy))
1772      (sigma_jump_equal prefix old_sigma policy → added = 0))
1773      (added = 0 → sigma_pc_equal prefix old_sigma policy))
1774      (out_of_program_none prefix policy))
1775      (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) =
1776       \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added))
1777      (sigma_safe prefix labels added old_sigma policy))
1778    program
1779    (λprefix.λx.λtl.λprf.λacc.
1780      let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
1781      let 〈label,instr〉 ≝ x in
1782      (* Now, we must add the current ppc and its pc translation.
1783       * Three possibilities:
1784       *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
1785       *   - Instruction is a backward jump; we can use the sigma we're constructing,
1786       *     since it will already know the translation of its destination;
1787       *   - Instruction is a forward jump; we must use the old sigma (the new sigma
1788       *     does not know the translation yet), but compensate for the jumps we
1789       *     have lengthened.
1790       *)
1791      let add_instr ≝ match instr with
1792      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
1793      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
1794      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
1795      | _             ⇒ None ?
1796      ] in
1797      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
1798      let old_length ≝
1799        \snd (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
1800      let old_size ≝ instruction_size_jmplen old_length instr in
1801      let 〈new_length, isize〉 ≝ match add_instr with
1802      [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
1803      | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
1804      ] in
1805      let new_added ≝ match add_instr with
1806      [ None   ⇒ inc_added
1807      | Some x ⇒ plus inc_added (minus isize old_size)
1808      ] in
1809      let old_Slength ≝
1810        \snd (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
1811      let updated_sigma ≝
1812        (* we add the new PC to the next position and the new jump length to this one *)
1813        bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, old_Slength〉
1814        (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
1815      〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
1816    ) 〈0, 〈0,
1817      bvt_insert …
1818        (bitvector_of_nat ? 0)
1819        〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
1820        (Stub ??)〉〉
1821    ) in
1822    if gtb (\fst final_policy) 2^16 then
1823      〈eqb final_added 0, None ?〉
1824    else
1825      〈eqb final_added 0, Some ? final_policy〉.
1826[ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
1827  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
1828  (* USE: inc_pc = fst of policy (from fold) *)
1829  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1;
1830  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
1831  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
1832  #Hsig #Hge
1833  (* USE: added = 0 → policy_pc_equal (from fold) *)
1834  lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (|program|) (le_n (|program|)))
1835  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
1836    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
1837    inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
1838    [ #Hj
1839      (* USE: policy_increase (from fold) *)
1840      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
1841      lapply (Habs i Hi ?) [ >Hj %]
1842      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
1843      #opc #oj
1844      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉)
1845      #pc #j normalize nodelta #Heq >Heq cases j
1846      [1,2: #abs cases abs #abs2 try (cases abs2) @refl
1847      |3: #_ @refl
1848      ]
1849    | #Hnj
1850      (* USE: not_jump_default (from fold and old_sigma) *)
1851      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?)
1852      [2: >Hnj %]
1853      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try %
1854      >Hnj %
1855    ]
1856  | #abs >abs in Hsig; #Hsig
1857    @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
1858  ]
1859| normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
1860  >H2 in H; normalize nodelta -H2 -x #H @conj
1861  [ @conj [ @conj
1862  [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy,
1863     * jump_increase, sigma_compact_unsafe (from fold) *)
1864    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
1865  | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *)
1866    @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2
1867  ]
1868  | (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *)
1869     #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
1870  ]
1871  | @not_lt_to_le @ltb_false_to_not_lt @p1
1872  ]
1873|4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
1874  #inc_pc #inc_sigma #Hips
1875  inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
1876  #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
1877  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
1878  #Heq1 #Heq2
1879 cut (S (|prefix|) < 2^16)
1880 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length
1881   <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1
1882 cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok
1883 cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
1884  % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
1885  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
1886   * commented out for full proofs, but this needs a lot of memory and time *)
1887  [ (* not_jump_default *)
1888    @(jump_expansion_step1 … Heq1 Heq2b) try assumption
1889    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
1890  | (* 0 ↦ 0 *)
1891    @(jump_expansion_step2 … Heq2b) try assumption
1892    [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
1893    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ]
1894  | (* inc_pc = fst of policy *)
1895    <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
1896  | (* jump_increase *)
1897    @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq
1898      … Heq1 prefix_ok1 prefix_ok Heq2b)
1899    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
1900    cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
1901  | (* sigma_compact_unsafe *)
1902    @(jump_expansion_step4 … Heq1 … Heq2b) try assumption
1903    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1904    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))
1905    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
1906  | (* policy_jump_equal → added = 0 *)
1907    @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption
1908    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
1909    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1910  | (* added = 0 → policy_pc_equal *) cases daemon (*
1911    @(jump_expansion_step6 … Heq1 … Heq2b) try assumption
1912    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
1913    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
1914    *)
1915  | (* out_of_program_none *) cases daemon(*
1916    @jump_expansion_step7 try assumption
1917    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))))
1918    *)
1919  | (* lookup p = lookup old_sigma + added *) cases daemon(*
1920    @jump_expansion_step8 try assumption
1921    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))   
1922    @(proj2 ?? (proj1 ?? Hpolicy)) *)
1923  | (* sigma_safe *) cases daemon (*
1924    @jump_expansion_step9 try assumption
1925    @(proj2 ?? Hpolicy) *)
1926  ]     
1927| normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
1928  [ #i cases i
1929    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1930    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
1931    ]
1932  | >lookup_insert_hit @refl
1933  | >lookup_insert_hit @refl
1934  | #i #Hi <(le_n_O_to_eq … Hi)
1935    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
1936    #a #b normalize nodelta %2 @refl
1937  | #i cases i
1938    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1939    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1940    ]
1941  | #_ %
1942  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
1943    (* USE: 0 ↦ 0 (from old_sigma) *)
1944    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
1945  | #i cases i
1946    [ #Hi2 @conj
1947      [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
1948      | >lookup_opt_insert_hit #H destruct (H)
1949      ]
1950    | -i #i #Hi2 @conj
1951      [ #Hi >lookup_opt_insert_miss
1952        [ / by refl/
1953        | @bitvector_of_nat_abs
1954          [ @Hi2
1955          | / by /
1956          | @sym_neq @lt_to_not_eq / by /
1957          ]
1958        ]
1959      | #_ @le_S_S @le_O_n
1960      ]
1961    ]
1962  | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *)
1963    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O %
1964  | #i cases i
1965    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1966    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1967    ]
1968  ]
1969]
1970qed.
Note: See TracBrowser for help on using the repository browser.