source: src/ASM/Policy.ma @ 2222

Last change on this file since 2222 was 2211, checked in by boender, 7 years ago
  • finished proof of sigma specification
  • added some stuff to Util, as usual
File size: 49.1 KB
Line 
1include "ASM/PolicyStep.ma".
2
3include alias "basics/lists/list.ma".
4include alias "arithmetics/nat.ma".
5include alias "basics/logic.ma".
6
7let rec jump_expansion_internal (program: Σl:list labelled_instruction.
8  lt (S (|l|)) 2^16 ∧ is_well_labelled_p l) (n: ℕ)
9  on n:(Σx:bool × (option ppc_pc_map).
10    let 〈no_ch,pol〉 ≝ x in
11    match pol with
12    [ None ⇒ True
13    | Some x ⇒
14      And (And (And (And
15        (not_jump_default program x)
16        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0))
17        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
18        (sigma_compact_unsafe program (create_label_map program) x))
19        (\fst x ≤ 2^16)
20    ]) ≝
21 let labels ≝ create_label_map program in
22  match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with
23  [ O   ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉
24  | S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
25          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
26          [ None    ⇒ λp2.〈false,None ?〉
27          | Some op ⇒ λp2.if no_ch
28            then pi1 ?? (jump_expansion_internal program m)
29            else pi1 ?? (jump_expansion_step program labels «op,?»)
30          ] (refl … z)
31  ] (refl … n).
32[ normalize nodelta cases (jump_expansion_start program (create_label_map program))
33  #x cases x -x
34  [ #H / by I/
35  | #sigma normalize nodelta #H @conj [ @conj
36    [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
37    | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
38    ]
39    | @(proj2 ?? H)
40    ]
41  ]
42| / by I/
43| cases no_ch in p1; #p1
44  [ @(pi2 ?? (jump_expansion_internal program m))
45  | cases (jump_expansion_step program (create_label_map program) «op,?»)
46    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
47    [ #_ / by I/
48    | #j2 #H2 @conj [ @conj
49      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
50      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
51      ]
52      | @(proj2 ?? H2)
53      ]
54    ]
55  ]
56| cases (jump_expansion_internal program m) in p1;
57  #p cases p -p #p #r cases r normalize nodelta
58  [ #_ >p2 #ABS destruct (ABS)
59  | #map >p2 normalize nodelta
60    #H #eq destruct (eq) @H
61  ]
62]
63qed.
64
65 
66lemma pe_int_refl: ∀program.reflexive ? (sigma_jump_equal program).
67#program whd #x whd #n #Hn
68cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉)
69#y #z normalize nodelta @refl
70qed.
71
72lemma pe_int_sym: ∀program.symmetric ? (sigma_jump_equal program).
73#program whd #x #y #Hxy whd #n #Hn
74lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
75#x1 #x2
76cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉)
77#y1 #y2 normalize nodelta //
78qed.
79 
80lemma pe_int_trans: ∀program.transitive ? (sigma_jump_equal program).
81#program whd #x #y #z whd in match (sigma_jump_equal ???); whd in match (sigma_jump_equal ?y ?);
82whd in match (sigma_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
83lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
84#x1 #x2
85cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) #y1 #y2
86cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,short_jump〉) #z1 #z2
87normalize nodelta //
88qed.
89
90definition policy_equal_opt ≝
91  λprogram:list labelled_instruction.λp1,p2:option ppc_pc_map.
92  match p1 with
93  [ Some x1 ⇒ match p2 with
94              [ Some x2 ⇒ sigma_jump_equal program x1 x2
95              | _       ⇒ False
96              ]
97  | None    ⇒ p2 = None ?
98  ].
99
100lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program).
101#program whd #x whd cases x
102[ //
103| #y @pe_int_refl
104]
105qed.
106
107lemma pe_sym: ∀program.symmetric ? (policy_equal_opt program).
108#program whd #x #y #Hxy whd cases y in Hxy;
109[ cases x
110  [ //
111  | #x' #H @⊥ @(absurd ? H) /2 by nmk/
112  ]
113| #y' cases x
114  [ #H @⊥ @(absurd ? H) whd in match (policy_equal_opt ???); @nmk #H destruct (H)
115  | #x' #H @pe_int_sym @H
116  ]
117]
118qed.
119
120lemma pe_trans: ∀program.transitive ? (policy_equal_opt program).
121#program whd #x #y #z cases x
122[ #Hxy #Hyz >Hxy in Hyz; //
123| #x' cases y
124  [ #H @⊥ @(absurd ? H) /2 by nmk/
125  | #y' cases z
126    [ #_ #H @⊥ @(absurd ? H) /2 by nmk/
127    | #z' @pe_int_trans
128    ]
129  ]
130]
131qed.
132
133definition step_none: ∀program.∀n.
134  (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? →
135  ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?.
136#program #n lapply (refl ? (jump_expansion_internal program n))
137 cases (jump_expansion_internal program n) in ⊢ (???% → %);
138 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
139[ <plus_n_O >Heqj @Hj
140| #k' -k <plus_n_Sm
141  lapply (refl ? (jump_expansion_internal program (n+k')))
142  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → %);
143  #x2 cases x2 -x2 #c2 #p2 normalize nodelta #H #Heqj2
144  cases p2 in H Heqj2;
145  [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
146    >Heqj2 normalize nodelta @refl
147  | #x #H #Heqj2 #abs destruct (abs)
148  ]
149]
150qed.
151
152lemma jump_pc_equal: ∀program.∀n.
153  match \snd (jump_expansion_internal program n) with
154  [ None   ⇒ True
155  | Some p1 ⇒ match \snd (jump_expansion_internal program (S n)) with
156    [ None ⇒ True
157    | Some p2 ⇒ sigma_jump_equal program p1 p2 → sigma_pc_equal program p1 p2
158    ]
159  ].
160 #program #n lapply (refl ? (jump_expansion_internal program n))
161 cases (jump_expansion_internal program n) in ⊢ (???% → %); #x cases x -x
162 #Nno_ch #No cases No
163 [ normalize nodelta #HN #NEQ @I
164 | #Npol normalize nodelta #HN #NEQ lapply (refl ? (jump_expansion_internal program (S n)))
165   cases (jump_expansion_internal program (S n)) in ⊢ (???% → %); #x cases x -x
166   #Sno_ch #So cases So
167   [ normalize nodelta #HS #SEQ @I
168   | #Spol normalize nodelta #HS #SEQ #Hj
169     whd in match (jump_expansion_internal program (S n)) in SEQ; (*80s*)
170     >NEQ in SEQ; normalize nodelta cases Nno_ch in HN;
171     [ #HN normalize nodelta #SEQ >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? SEQ))))
172       / by /
173     | #HN normalize nodelta cases (jump_expansion_step program (create_label_map program) «Npol,?»)     
174       #x cases x -x #Stno_ch #Stno_o normalize nodelta cases Stno_o
175       [ normalize nodelta #_ #H destruct (H)
176       | #Stno_p normalize nodelta #HSt #STeq
177         <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? STeq)))) in Hj; #Hj
178         @(proj2 ?? (proj1 ?? HSt)) @(proj2 ?? (proj1 ?? (proj1 ?? HSt))) @Hj
179       ]
180     ]
181   ]
182 ]
183qed.
184       
185
186lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
187  ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n)))
188   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
189  policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
190    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
191#program #n #Heq
192cases daemon (* XXX *)
193qed.
194
195lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.
196  S (|l|) < 2^16 ∧ is_well_labelled_p l).∀n:ℕ.
197  policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
198   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
199  ∀k.k ≥ n → policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
200   (\snd (pi1 … (jump_expansion_internal program k))).
201#program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
202lapply Heq -Heq; lapply n -n; elim z -z;
203[ #n #Heq <plus_n_O @pe_refl
204| #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z);
205  @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n)))))
206  [ @Heq
207  | @Hind @pe_step @Heq
208  ]
209]
210qed.
211
212(* this number monotonically increases over iterations, maximum 2*|program| *)
213let rec measure_int (program: list labelled_instruction) (policy: ppc_pc_map) (acc: ℕ)
214 on program: ℕ ≝
215 match program with
216 [ nil      ⇒ acc
217 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) with
218   [ long_jump   ⇒ measure_int t policy (acc + 2)
219   | absolute_jump ⇒ measure_int t policy (acc + 1)
220   | _           ⇒ measure_int t policy acc
221   ]
222 ].
223
224lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
225 measure_int program policy (x+d) = measure_int program policy x + d.
226#program #policy #x #d generalize in match x; -x elim d
227[ //
228| -d; #d #Hind elim program
229  [ / by refl/
230  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
231    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
232    [ normalize nodelta @Hd
233    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
234      @Hd
235    ]
236  ]
237]
238qed.
239
240lemma measure_le: ∀program.∀policy.
241  measure_int program policy 0 ≤ 2*|program|.
242#program #policy elim program
243[ normalize @le_n
244| #h #t #Hind whd in match (measure_int ???);
245  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
246  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
247  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
248    @le_plus [1,3: @Hind |2,4: / by le_n/ ]
249  ]
250]
251qed.
252
253(* uses the second part of policy_increase *)
254lemma measure_incr_or_equal: ∀program:(Σl:list labelled_instruction.
255  S (|l|) <2^16 ∧ is_well_labelled_p l).
256  ∀policy:Σp:ppc_pc_map.
257    (*out_of_program_none program p ∧*)
258    not_jump_default program p ∧
259    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
260    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
261    sigma_compact_unsafe program (create_label_map program) p ∧
262    \fst p ≤ 2^16.
263  ∀l.|l| ≤ |program| → ∀acc:ℕ.
264  match \snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy)) with
265  [ None   ⇒ True
266  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
267  ].
268#program #policy #l elim l -l;
269[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
270| #h #t #Hind #Hp #acc
271  lapply (refl ? (jump_expansion_step program (create_label_map program) policy))
272  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r
273  [ / by I/
274  | #x normalize nodelta #Hx #Hjeq
275    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) (le_S_to_le … Hp))
276    whd in match (measure_int ???); whd in match (measure_int ? x ?);
277    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
278    #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,short_jump〉)
279    #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2
280    [1,4,5,7,8,9: #H cases H
281    |2,3,6: #_ normalize nodelta
282      [1,2: @(transitive_le ? (measure_int t x acc))
283      |3: @(transitive_le ? (measure_int t x (acc+1)))
284      ]
285      [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
286      >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
287    |11,12,13,15,16,17: #H destruct (H)
288    |10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
289    ]
290  ]
291]
292qed.
293
294lemma measure_full: ∀program.∀policy.
295  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
296  is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) →
297  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.
298#program #policy elim program in ⊢ (% → ∀i.% → ? → %);
299[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
300| #h #t #Hind #Hm #i #Hi #Hj
301  cases (le_to_or_lt_eq … Hi) -Hi
302  [ #Hi @Hind
303    [ whd in match (measure_int ???) in Hm;
304      cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
305      normalize nodelta
306      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
307      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
308        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
309      | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/
310      ]
311    | @(le_S_S_to_le … Hi)
312    | @Hj
313    ]
314  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
315    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
316    normalize nodelta
317    [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/
318    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
319      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
320    | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/
321    ]
322  ]
323]
324qed.
325
326(* uses second part of policy_increase *)
327lemma measure_special: ∀program:(Σl:list labelled_instruction.
328    (S (|l|)) < 2^16 ∧ is_well_labelled_p l).
329  ∀policy:Σp:ppc_pc_map.
330    not_jump_default program p ∧
331    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
332    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
333    sigma_compact_unsafe program (create_label_map program) p ∧
334    \fst p ≤ 2^16.
335  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
336  [ None ⇒ True
337  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
338#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy)))
339cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %);
340#p cases p -p #ch #pol normalize nodelta cases pol
341[ / by I/
342| #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|))
343  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
344      measure_int x policy 0 = measure_int x p 0 →
345      sigma_jump_equal x policy p) ?? (pi1 ?? program))
346 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n
347 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le …  Hi)) -Hi #Hi
348   [ @Hind
349     [ @(transitive_le … Hp) / by /
350     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
351       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
352       #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc;
353       #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
354       #y1 #y2 #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
355       cases x2 cases y2 normalize nodelta
356       [1: / by /
357       |2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
358         lapply (measure_incr_or_equal program policy t ? 0)
359         [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
360       |4,7,8: #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
361       |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
362         #_ #H @(injective_plus_r … H)
363       |6: >measure_plus >measure_plus
364         change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
365         #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
366         lapply (measure_incr_or_equal program policy t ? 0)
367         [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
368       |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
369         #_ #H @(injective_plus_r … H)
370       ]
371     | @Hi
372     ]
373   | >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
374     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
375     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
376     #x1 #x2
377     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2
378     normalize nodelta cases x2 cases y2 normalize nodelta
379     [1,5,9: #_ #_ @refl
380     |4,7,8: #_ #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
381     |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
382       lapply (measure_incr_or_equal program policy t ? 0)
383       [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
384     |6: >measure_plus >measure_plus
385        change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
386        #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
387        lapply (measure_incr_or_equal program policy t ? 0)
388        [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
389     ]
390   ]
391 ]
392qed.
393
394lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.
395  S (|l|) < 2^16 ∧ is_well_labelled_p l.
396  match jump_expansion_start program (create_label_map program) with
397  [ None ⇒ True
398  | Some p ⇒ |l| ≤ |program| → measure_int l p 0 = 0
399  ].
400 #l #program lapply (refl ? (jump_expansion_start program (create_label_map program)))
401 cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); #p #Hp #EQ
402 cases p in Hp EQ;
403 [ / by I/
404 | #pl normalize nodelta #Hpl #EQ elim l
405   [ / by refl/
406   | #h #t #Hind #Hp whd in match (measure_int ???);
407     elim (proj2 ?? (proj1 ?? Hpl) (|t|) (le_S_to_le … Hp))
408     #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind
409     @(transitive_le … Hp) @le_n_Sn
410   ]
411 ]
412qed.
413
414(* the actual computation of the fixpoint *)
415definition je_fixpoint: ∀program:(Σl:list labelled_instruction.
416  S (|l|) < 2^16 ∧ is_well_labelled_p l).
417  Σp:option ppc_pc_map.
418    match p with
419      [ None ⇒ True
420      | Some pol ⇒ And (And (And
421          (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
422          (\fst pol = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd pol) 〈0,short_jump〉)))
423          (sigma_compact program (create_label_map program) pol))
424          (\fst pol ≤ 2^16)
425      ].
426#program @(\snd (jump_expansion_internal program (S (2*|program|))))
427cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
428   (\snd (pi1 ?? (jump_expansion_internal program k)))
429   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
430[ #Hex cases Hex -Hex #k #Hk
431  lapply (refl ? (jump_expansion_internal program (S (2*|program|))))
432  cases (jump_expansion_internal ? (S (2*|program|))) in ⊢ (???% → %);
433  #x cases x -x #Gno_ch #Go cases Go normalize nodelta
434  [ #H #Heq / by I/
435  | -Go #Gp #HGp #Geq
436    cut (policy_equal_opt program (\snd (jump_expansion_internal program (2*|program|)))
437      (\snd (jump_expansion_internal program (S (2*|program|)))))
438    [ @(pe_trans … (equal_remains_equal program k (proj2 ?? Hk) (S (2*|program|)) (le_S … (le_S_to_le … (proj1 ?? Hk)))))
439      @pe_sym @equal_remains_equal [ @(proj2 ?? Hk) | @(le_S_to_le … (proj1 ?? Hk)) ]
440    | >Geq lapply (refl ? (jump_expansion_internal program (2*|program|)))
441      cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
442      #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
443      [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS)
444      | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq
445        @conj [ @conj [ @conj
446        [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
447        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
448        ]
449        | @(equal_compact_unsafe_compact ?? Fp)
450          [ lapply (jump_pc_equal program (2*|program|))
451            >Feq >Geq normalize nodelta #H @H @Heq
452          | cases daemon (* true, but have to add this to properties *)
453          | @(proj2 ?? (proj1 ?? HGp))
454          ]
455        ]
456        | @(proj2 ?? HGp)
457        ]
458      ]
459    ]
460  ]
461| #Hnex lapply (not_exists_forall … Hnex) -Hnex #Hfa
462  lapply (refl ? (jump_expansion_internal program (2*|program|)))
463  cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
464  #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
465  [ (* None *)
466     #HF #Feq lapply (step_none program (2*|program|) ? 1) >Feq / by /
467    <plus_n_Sm <plus_n_O #H >H -H normalize nodelta / by I/
468  | -Fo #Fp #HFp #Feq lapply (measure_full program Fp ?)
469    [ @le_to_le_to_eq
470      [ @measure_le
471      | cut (∀x:ℕ.x ≤ 2*|program| →
472         ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
473          x ≤ measure_int program p 0))
474        [ #x elim x
475          [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program)))
476            cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %);
477             #z cases z -z normalize nodelta
478             [ #H #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #n #Hn
479               @(absurd … (step_none program 0 ? n))
480               [ whd in match (jump_expansion_internal ??); >Heqn @refl
481               | <Hn >Feq @nmk #H destruct (H)
482               ]
483             | #Zp #HZp #Zeq @(ex_intro ?? Zp) @conj
484               [ whd in match (jump_expansion_internal ??); >Zeq @refl
485               | @le_O_n
486               ]
487             ]
488          | -x #x #Hind #Hx
489            lapply (refl ? (jump_expansion_internal program (S x)))
490            cases (jump_expansion_internal program (S x)) in ⊢ (???% → %);
491            #z cases z -z #Sno_ch #So cases So -So
492            [ #HSp #Seq normalize nodelta @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
493              @(absurd … (step_none program (S x) ? k))
494              [ >Seq @refl
495              | <Hk >Feq @nmk #H destruct (H)
496              ]
497            | #Sp #HSp #Seq @(ex_intro ?? Sp) @conj
498              [ @refl
499              | elim (Hind (transitive_le … (le_n_Sn x) Hx))
500                #pol #Hpol @(le_to_lt_to_lt … (proj2 ?? Hpol))
501                lapply (proj1 ?? Hpol) -Hpol
502                lapply (refl ? (jump_expansion_internal program x))
503                cases (jump_expansion_internal program x) in ⊢ (???% → %);
504                #z cases z -z #Xno_ch #Xo cases Xo
505                [ #HXp #Xeq #abs destruct (abs)
506                | normalize nodelta #Xp #HXp #Xeq #H <(Some_eq ??? H) -H -pol
507                  lapply (Hfa x Hx) >Xeq >Seq whd in match policy_equal_opt;
508                  normalize nodelta #Hpe
509                  lapply (measure_incr_or_equal program Xp program (le_n (|program|)) 0)
510                  [ @HXp
511                  | lapply (Hfa x Hx) >Xeq >Seq
512                    lapply (measure_special program «Xp,?»)
513                    [ @HXp
514                    | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*)
515                      >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq
516                      [ normalize nodelta #EQ
517                        >(proj2 ?? (pair_destruct ?????? (pi1_eq ???? EQ)))
518                        #_ #abs @⊥ @(absurd ?? abs) / by /
519                      | normalize nodelta cases (jump_expansion_step ???);
520                        #z cases z -z #stch #sto cases sto   
521                        [ normalize nodelta #_ #ABS destruct (ABS)
522                        | -sto #stp normalize nodelta #Hstp #steq
523                          >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? steq))))
524                          #Hms #Hneq #glerp elim (le_to_or_lt_eq … glerp)
525                          [ / by /
526                          | #glorp @⊥ @(absurd ?? Hneq) @Hms @glorp
527                          ]
528                        ]
529                      ]
530                    ]
531                  ]
532                ]
533              ]
534            ]
535          ]
536        | #H elim (H (2*|program|) (le_n ?)) #plp >Feq #Hplp
537          >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp)
538        ]
539      ]
540    | #Hfull lapply (refl ? (jump_expansion_internal program (S (2*|program|))))
541      cases (jump_expansion_internal program (S (2*|program|))) in ⊢ (???% → %);
542      #z cases z -z #Gch #Go cases Go normalize nodelta
543      [ #HGp #Geq @I
544      | -Go #Gp normalize nodelta #HGp #Geq @conj [ @conj [ @conj
545        [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
546        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
547        ]
548        | @(equal_compact_unsafe_compact ?? Fp)
549          [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
550            #H @H #i #Hi
551            cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
552            [ #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
553              >Feq in Geq; normalize nodelta cases Fno_ch
554              [ normalize nodelta #Heq
555                >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) %
556              | normalize nodelta cases (jump_expansion_step program (create_label_map program) «Fp,?»)
557                #x cases x -x #stch #sto normalize nodelta cases sto
558                [ normalize nodelta #_ #X destruct (X)
559                | -sto #stp normalize nodelta #Hst #Heq
560                   <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq))))
561                   lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi))
562                   lapply (Hfull i Hi Hj)
563                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
564                   #fp #fj #Hfj >Hfj normalize nodelta
565                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
566                   #stp #stj cases stj normalize nodelta
567                   [1,2: #H cases H #H2 cases H2 destruct (H2)
568                   |3: #_ @refl
569                   ]
570                 ]
571               ]
572             | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi Hj)
573                >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl
574              ]
575            | cases daemon (* true, but have to add to properties in some way *)
576            | @(proj2 ?? (proj1 ?? HGp))
577            ]
578          ]
579          | @(proj2 ?? HGp)
580          ]
581        ]
582      ]
583    ]
584  | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
585    #x cases x -x #nch #npol normalize nodelta #Hnpol
586    #x cases x -x #Sch #Spol normalize nodelta #HSpol
587    cases npol in Hnpol; cases Spol in HSpol;
588    [ #Hnpol #HSpol %1 //
589    |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
590      #H destruct (H)
591    |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
592        cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
593        #x1 #x2
594        cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
595        #y1 #y2 normalize nodelta
596        @dec_eq_jump_length
597    ]
598  ]
599qed.
600
601include alias "arithmetics/nat.ma".
602include alias "basics/logic.ma".
603
604lemma pc_increases: ∀i,j:ℕ.∀program.∀pol:Σp:ppc_pc_map.
605  And (And (And
606    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)
607    (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
608    (sigma_compact program (create_label_map program) p))
609    (\fst p ≤ 2^16).i ≤ j → j ≤ |program| →
610  \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 i) (\snd pol) 〈0,short_jump〉) ≤
611  \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 j) (\snd pol) 〈0,short_jump〉).
612 #i #j #program #pol #H elim (le_to_eq_plus … H) #n #Hn >Hn -Hn -j elim n
613 [ <plus_n_O #_ @le_n
614 | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H)))
615   lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (i+n) H)
616   lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)))
617   cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %);
618   [ normalize nodelta #_ #abs cases abs
619   | #x cases x -x #pc #jl #EQ normalize nodelta
620     lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)))
621     cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %);
622     [ normalize nodelta #_ #abs cases abs
623     | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp
624       >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
625       >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r
626     ]
627   ]
628 ]
629qed.
630 
631(* The glue between Policy and Assembly. *)
632(*CSC: modified to really use the specification in Assembly.ma.*)
633definition jump_expansion':
634∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
635 option (Σsigma_policy:(Word → Word) × (Word → bool).
636   let 〈sigma,policy〉≝ sigma_policy in
637   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy)
638   ≝
639 λprogram.
640  let f: option ppc_pc_map ≝ je_fixpoint (\snd program) in
641  match f return λx.f = x → ? with
642  [ None ⇒ λp.None ?
643  | Some x ⇒ λp.Some ?
644      «〈(λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
645          bitvector_of_nat 16 pc),
646         (λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
647          jmpeqb jl long_jump)〉,?»
648  ] (refl ? f).
649normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta
650lapply (pi2 ?? (je_fixpoint (\snd program))) >p normalize nodelta cases x
651#fpc #fpol #Hfpol
652@conj
653[ lapply (proj1 ?? (proj1 ?? (proj1 ?? Hfpol))) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
654  #x #y #Hx normalize nodelta >Hx / by refl/
655| #ppc #ppc_ok normalize nodelta @conj
656  [ lapply ((proj2 ?? (proj1 ?? Hfpol)) (nat_of_bitvector ? ppc) ppc_ok)
657    >bitvector_of_nat_inverse_nat_of_bitvector
658    lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
659    [ #Hl normalize nodelta #abs cases abs
660    | #x cases x -x #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm
661      >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
662      lapply (refl ? (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol))
663      cases (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol) in ⊢ (???% → %);
664      [ #Hl normalize nodelta #abs cases abs
665      | #x cases x -x #Spc #Sjl #SHl normalize nodelta #Hcompact
666        >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
667        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
668        >add_bitvector_of_nat_plus >Hcompact whd in match instruction_size;
669        normalize nodelta whd in match assembly_1_pseudoinstruction;
670        normalize nodelta whd in match expand_pseudo_instruction;
671        normalize nodelta whd in match fetch_pseudo_instruction;
672        normalize nodelta
673        lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok))
674        cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %);
675        #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉)
676        >Hli normalize nodelta cases instr
677        [2,3,6: #x [3: #y] normalize nodelta %
678        |4,5: #x normalize nodelta
679          >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
680          whd in match create_label_map; normalize nodelta
681          >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
682          cases (bvt_lookup … (bitvector_of_nat ?
683           (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
684          #lpc #ljl normalize nodelta @refl
685        |1: #pi cases pi
686          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
687            [1,2,3,6,7,24,25: #x #y
688            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
689            normalize nodelta %
690          |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
691            whd in match expand_relative_jump; normalize nodelta
692            whd in match expand_relative_jump_internal; normalize nodelta
693            >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
694            whd in match create_label_map; normalize nodelta
695            >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
696            cases (bvt_lookup … (bitvector_of_nat ?
697             (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
698            #lpc #ljl normalize nodelta %
699          ]
700        ]
701      ]
702    ]
703  | (* Basic proof scheme:
704       - ppc < |snd program|, hence our instruction is in the program
705       - either we are the last non-zero-size instruction, in which case we are
706         either smaller than 2^16 (because the entire program is), or we are exactly
707         2^16 and something weird happens
708       - or we are not, in which case we are definitely smaller than 2^16 (by transitivity
709         through the next non-zero instruction)
710    *)
711    elim (le_to_or_lt_eq … (proj2 ?? Hfpol)) #Hfpc
712    [ %1 @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol)))
713      lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
714      >bitvector_of_nat_inverse_nat_of_bitvector
715      lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
716      [ normalize nodelta #_ #abs cases abs
717      | #x cases x -x #pc #jl #EQ normalize nodelta
718        lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol))
719        cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
720        [ normalize nodelta #_ #abs cases abs
721        | #x cases x -x #Spc #Sjl #SEQ normalize nodelta whd in match instruction_size;
722          normalize nodelta whd in match assembly_1_pseudoinstruction;
723          normalize nodelta whd in match expand_pseudo_instruction;
724          normalize nodelta whd in match fetch_pseudo_instruction;
725          normalize nodelta
726          lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok))
727          cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %);
728          #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉)
729          >Hli normalize nodelta cases instr
730          [2,3,6: #x [3: #y] normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
731            normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
732            [1,3,5: <H
733              lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
734              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X
735            |2,4,6: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
736              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
737              #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
738            ]
739          |4,5: #x normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
740            normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
741            [1,3: <add_bitvector_of_nat_Sm in SEQ;
742              >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ
743              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta
744              cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
745              #lpc #ljl normalize nodelta #H <H
746              lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
747              <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector
748              >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2
749            |2,4: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
750              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
751              #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
752            ]
753          |1: #pi cases pi
754            [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
755              [1,2,3,6,7,24,25: #x #y
756              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
757              normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
758              normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
759              [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
760                <H lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
761                >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X
762              |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
763                lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
764                >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
765                #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
766              ]
767            |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x]
768              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
769              normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
770              [1,3,5,7,9,11,13,15,17: <add_bitvector_of_nat_Sm in SEQ;
771                >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ
772                whd in match expand_relative_jump; normalize nodelta
773                whd in match expand_relative_jump_internal; normalize nodelta
774                >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta
775                cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
776                #lpc #ljl normalize nodelta #H <H
777                lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
778                <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector
779                >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2
780              |2,4,6,8,10,12,14,16,18:
781                lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
782                >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
783                #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
784              ]
785            ]
786          ]
787        ]
788      ]
789    | (* the program is of length 2^16 and ppc is followed by only zero-size instructions
790       * until the end of the program *)
791      elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)))
792      [ lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
793        >bitvector_of_nat_inverse_nat_of_bitvector
794        lapply (refl ? (lookup_opt … ppc fpol))
795        cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
796        [ #_ normalize nodelta #abs cases abs
797        | #x cases x -x #pc #jl #EQ normalize nodelta
798          lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol))
799          cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
800          [ #_ normalize nodelta #abs cases abs
801          | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hc
802            >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hpc normalize nodelta
803            >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
804            >nat_of_bitvector_bitvector_of_nat_inverse
805            [2: <Hfpc >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @Hpc ]
806            elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
807            [ <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
808              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc %1
809              >Hc in HSpc;
810              whd in match create_label_map;
811              whd in match fetch_pseudo_instruction; normalize nodelta
812              >(nth_safe_nth … 〈None ?, Comment []〉)
813              cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
814              #lbl #ins normalize nodelta
815              whd in match instruction_size;
816              whd in match assembly_1_pseudoinstruction;
817              whd in match expand_pseudo_instruction; normalize nodelta
818              <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector
819              >add_commutative #SEQ cases ins
820              [2,3,6: #x [3: #y] normalize nodelta #H @H
821              |4,5: #x normalize nodelta
822                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
823                >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
824                cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
825                #lpc #ljl normalize nodelta #H @H
826              |1: #pi cases pi
827                [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
828                  [1,2,3,6,7,24,25: #x #y
829                  |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
830                  normalize nodelta #H @H
831                |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
832                  whd in match expand_relative_jump;
833                  whd in match expand_relative_jump_internal; normalize nodelta
834                  >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
835                  >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
836                  cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
837                  #lpc #ljl normalize nodelta #H @H
838                ]
839              ]
840            | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
841              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj
842              [ #ppc' #ppc_ok' #Hppc'
843                (* S ppc < ppc' < |\snd program| *)
844                (* lookup S ppc = 2^16 *)
845                (* lookup |\snd program| = 2^16 *)
846                (* lookup ppc' = 2^16 → instruction size = 0 *)
847                lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc') ppc_ok')
848                >bitvector_of_nat_inverse_nat_of_bitvector
849                lapply (refl ? (lookup_opt … ppc' fpol))
850                cases (lookup_opt … ppc' fpol) in ⊢ (???% → %);
851                [ normalize nodelta #_ #abs cases abs
852                | normalize nodelta #x cases x -x #xpc #xjl #XEQ normalize nodelta
853                  lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol))
854                  cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol) in ⊢ (???% → %);
855                  [ normalize nodelta #_ #abs cases abs
856                  | normalize nodelta #x cases x -x #Sxpc #Sxjl #SXEQ normalize nodelta
857                    #Hpcompact
858                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
859                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1
860                    lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
861                    <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2
862                    lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1
863                    >bitvector_of_nat_inverse_nat_of_bitvector
864                    >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
865                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
866                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1
867                    lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
868                    <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2
869                    lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2
870                    >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc
871                    >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H
872                    @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
873                    normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)
874                    cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;
875                    #lbl #ins normalize nodelta
876                    whd in match instruction_size;
877                    whd in match assembly_1_pseudoinstruction;
878                    whd in match expand_pseudo_instruction; normalize nodelta
879                    <add_bitvector_of_nat_Sm in SXEQ; >bitvector_of_nat_inverse_nat_of_bitvector
880                    >add_commutative #SXEQ cases ins
881                    [2,3,6: #x [3: #y] normalize nodelta #H @(sym_eq ??? H)
882                    |4,5: #x normalize nodelta
883                      >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉)
884                      >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉)
885                      cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
886                      #lpc #ljl normalize nodelta #H @(sym_eq ??? H)
887                    |1: #pi cases pi
888                      [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
889                        [1,2,3,6,7,24,25: #x #y
890                        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta
891                          #H @(sym_eq ??? H)
892                      |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
893                        whd in match expand_relative_jump;
894                        whd in match expand_relative_jump_internal; normalize nodelta
895                        >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉)
896                        >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉)
897                        cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
898                        #lpc #ljl normalize nodelta #H @(sym_eq ??? H)
899                      ]
900                    ]
901                  ]
902                ]
903              | >Hc in Hspc;
904                whd in match create_label_map;
905                whd in match fetch_pseudo_instruction; normalize nodelta
906                >(nth_safe_nth … 〈None ?, Comment []〉)
907                cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
908                 #lbl #ins normalize nodelta
909                whd in match instruction_size;
910                whd in match assembly_1_pseudoinstruction;
911                whd in match expand_pseudo_instruction; normalize nodelta
912                <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector
913                >add_commutative #SEQ cases ins
914                [2,3,6: #x [3: #y] normalize nodelta #H @H
915                |4,5: #x normalize nodelta
916                  >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
917                  >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
918                  cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
919                  #lpc #ljl normalize nodelta #H @H
920                |1: #pi cases pi
921                  [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
922                    [1,2,3,6,7,24,25: #x #y
923                    |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta
924                    #H @H
925                  |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
926                    whd in match expand_relative_jump;
927                    whd in match expand_relative_jump_internal; normalize nodelta
928                    >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
929                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
930                    cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
931                    #lpc #ljl normalize nodelta #H @H
932                  ]
933                ]
934              ]
935            ]
936          ]
937        ]
938      | >bitvector_of_nat_inverse_nat_of_bitvector
939        <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
940        cases (lookup … ppc fpol 〈0,short_jump〉) #pc #jl normalize nodelta #Hpc %1 >Hpc
941        >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?));
942        <plus_O_n whd in match instruction_size; normalize nodelta
943        lapply (refl ? (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?))
944        [5: cases (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?) in ⊢ (???% → %);
945          #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
946          #Hli >Hli
947          lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?)
948          [5: >Hass / by /
949          ]
950        ]
951      ]
952    ]
953  ]
954]
955qed.
Note: See TracBrowser for help on using the repository browser.