source: src/ASM/PolicyStep.ma @ 2316

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