source: src/ASM/PolicyStep.ma @ 3341

Last change on this file since 3341 was 3097, checked in by sacerdot, 7 years ago

Performance improvement in policy computation.

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