source: src/ASM/PolicyStep.ma @ 3003

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

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