source: src/ASM/Policy.ma @ 2141

Last change on this file since 2141 was 2141, checked in by boender, 7 years ago
  • committed working version
File size: 29.3 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 (And
15        (out_of_program_none program x)
16        (not_jump_default program x))
17        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0))
18        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
19        (\fst x < 2^16))
20        (no_ch = true → sigma_compact program (create_label_map program) x)
21    ]) ≝
22 let labels ≝ create_label_map program in
23  match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with
24  [ O   ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉
25  | S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
26          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
27          [ None    ⇒ λp2.〈false,None ?〉
28          | Some op ⇒ λp2.if no_ch
29            then pi1 ?? (jump_expansion_internal program m)
30            else pi1 ?? (jump_expansion_step program labels «op,?»)
31          ] (refl … z)
32  ] (refl … n).
33[ normalize nodelta cases (jump_expansion_start program (create_label_map program))
34  #x cases x -x
35  [ #H / by I/
36  | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj
37    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
38    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
39    ]
40    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
41    ]
42    | @(proj2 ?? H)
43    ]
44    | #H destruct (H)
45    ]
46  ]
47| / by I/
48| cases no_ch in p1; #p1
49  [ @(pi2 ?? (jump_expansion_internal program m))
50  | cases (jump_expansion_step program (create_label_map program) «op,?»)
51    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
52    [ #_ / by I/
53    | #j2 #H2 @conj [ @conj [ @conj [ @conj
54      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
55      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
56      ]
57      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
58      ]     
59      | @(proj2 ?? H2)
60      ]
61      | #Ht @(equal_compact_unsafe_compact ?? op)
62        [ @(proj2 ?? (proj1 ?? (proj1 ?? H2))) @Ht
63        | cases daemon (* add to invvariants *)
64        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
65        ]
66      ]
67    ]
68  ]
69| cases (jump_expansion_internal program m) in p1;
70  #p cases p -p #p #r cases r normalize nodelta
71  [ #_ >p2 #ABS destruct (ABS)
72  | #map >p2 normalize nodelta
73    #H #eq destruct (eq) cases daemon (* change order *)
74  ]
75]
76qed.
77
78lemma pe_int_refl: ∀program.reflexive ? (sigma_jump_equal program).
79#program whd #x whd #n #Hn
80cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉)
81#y #z normalize nodelta @refl
82qed.
83
84lemma pe_int_sym: ∀program.symmetric ? (sigma_jump_equal program).
85#program whd #x #y #Hxy whd #n #Hn
86lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
87#x1 #x2
88cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉)
89#y1 #y2 normalize nodelta //
90qed.
91 
92lemma pe_int_trans: ∀program.transitive ? (sigma_jump_equal program).
93#program whd #x #y #z whd in match (sigma_jump_equal ???); whd in match (sigma_jump_equal ?y ?);
94whd in match (sigma_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
95lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
96#x1 #x2
97cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) #y1 #y2
98cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,short_jump〉) #z1 #z2
99normalize nodelta //
100qed.
101
102definition policy_equal_opt ≝
103  λprogram:list labelled_instruction.λp1,p2:option ppc_pc_map.
104  match p1 with
105  [ Some x1 ⇒ match p2 with
106              [ Some x2 ⇒ sigma_jump_equal program x1 x2
107              | _       ⇒ False
108              ]
109  | None    ⇒ p2 = None ?
110  ].
111
112lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program).
113#program whd #x whd cases x
114[ //
115| #y @pe_int_refl
116]
117qed.
118
119lemma pe_sym: ∀program.symmetric ? (policy_equal_opt program).
120#program whd #x #y #Hxy whd cases y in Hxy;
121[ cases x
122  [ //
123  | #x' #H @⊥ @(absurd ? H) /2 by nmk/
124  ]
125| #y' cases x
126  [ #H @⊥ @(absurd ? H) whd in match (policy_equal_opt ???); @nmk #H destruct (H)
127  | #x' #H @pe_int_sym @H
128  ]
129]
130qed.
131
132lemma pe_trans: ∀program.transitive ? (policy_equal_opt program).
133#program whd #x #y #z cases x
134[ #Hxy #Hyz >Hxy in Hyz; //
135| #x' cases y
136  [ #H @⊥ @(absurd ? H) /2 by nmk/
137  | #y' cases z
138    [ #_ #H @⊥ @(absurd ? H) /2 by nmk/
139    | #z' @pe_int_trans
140    ]
141  ]
142]
143qed.
144
145definition step_none: ∀program.∀n.
146  (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? →
147  ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?.
148#program #n lapply (refl ? (jump_expansion_internal program n))
149 cases (jump_expansion_internal program n) in ⊢ (???% → %);
150 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
151[ <plus_n_O >Heqj @Hj
152| #k' -k <plus_n_Sm
153  lapply (refl ? (jump_expansion_internal program (n+k')))
154  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → %);
155  #x2 cases x2 -x2 #c2 #p2 normalize nodelta #H #Heqj2
156  cases p2 in H Heqj2;
157  [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
158    >Heqj2 normalize nodelta @refl
159  | #x #H #Heqj2 #abs destruct (abs)
160  ]
161]
162qed.
163
164lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
165  ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n)))
166   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
167  policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
168    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
169#program #n #Heq
170cases daemon (* XXX *)
171qed.
172
173lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.
174  S (|l|) < 2^16 ∧ is_well_labelled_p l).∀n:ℕ.
175  policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
176   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
177  ∀k.k ≥ n → policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
178   (\snd (pi1 … (jump_expansion_internal program k))).
179#program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
180lapply Heq -Heq; lapply n -n; elim z -z;
181[ #n #Heq <plus_n_O @pe_refl
182| #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z);
183  @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n)))))
184  [ @Heq
185  | @Hind @pe_step @Heq
186  ]
187]
188qed.
189
190(* this number monotonically increases over iterations, maximum 2*|program| *)
191let rec measure_int (program: list labelled_instruction) (policy: ppc_pc_map) (acc: ℕ)
192 on program: ℕ ≝
193 match program with
194 [ nil      ⇒ acc
195 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) with
196   [ long_jump   ⇒ measure_int t policy (acc + 2)
197   | absolute_jump ⇒ measure_int t policy (acc + 1)
198   | _           ⇒ measure_int t policy acc
199   ]
200 ].
201
202lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
203 measure_int program policy (x+d) = measure_int program policy x + d.
204#program #policy #x #d generalize in match x; -x elim d
205[ //
206| -d; #d #Hind elim program
207  [ / by refl/
208  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
209    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
210    [ normalize nodelta @Hd
211    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
212      @Hd
213    ]
214  ]
215]
216qed.
217
218lemma measure_le: ∀program.∀policy.
219  measure_int program policy 0 ≤ 2*|program|.
220#program #policy elim program
221[ normalize @le_n
222| #h #t #Hind whd in match (measure_int ???);
223  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
224  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
225  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
226    @le_plus [1,3: @Hind |2,4: / by le_n/ ]
227  ]
228]
229qed.
230
231(* uses the second part of policy_increase *)
232lemma measure_incr_or_equal: ∀program:(Σl:list labelled_instruction.
233  S (|l|) <2^16 ∧ is_well_labelled_p l).
234  ∀policy:Σp:ppc_pc_map.
235    (*out_of_program_none program p ∧*)
236    not_jump_default program p ∧
237    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
238    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
239    sigma_compact_unsafe program (create_label_map program) p ∧
240    \fst p < 2^16.
241  ∀l.|l| ≤ |program| → ∀acc:ℕ.
242  match \snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy)) with
243  [ None   ⇒ True
244  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
245  ].
246#program #policy #l elim l -l;
247[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
248| #h #t #Hind #Hp #acc
249  lapply (refl ? (jump_expansion_step program (create_label_map program) policy))
250  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r
251  [ / by I/
252  | #x normalize nodelta #Hx #Hjeq
253    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) (le_S_to_le … Hp))
254    whd in match (measure_int ???); whd in match (measure_int ? x ?);
255    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
256    #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,short_jump〉)
257    #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2
258    [1,4,5,7,8,9: #H cases H
259    |2,3,6: #_ normalize nodelta
260      [1,2: @(transitive_le ? (measure_int t x acc))
261      |3: @(transitive_le ? (measure_int t x (acc+1)))
262      ]
263      [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
264      >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
265    |11,12,13,15,16,17: #H destruct (H)
266    |10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
267    ]
268  ]
269]
270qed.
271
272lemma measure_full: ∀program.∀policy.
273  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
274  is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) →
275  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.
276#program #policy elim program in ⊢ (% → ∀i.% → ? → %);
277[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
278| #h #t #Hind #Hm #i #Hi #Hj
279  cases (le_to_or_lt_eq … Hi) -Hi
280  [ #Hi @Hind
281    [ whd in match (measure_int ???) in Hm;
282      cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
283      normalize nodelta
284      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
285      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
286        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
287      | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/
288      ]
289    | @(le_S_S_to_le … Hi)
290    | @Hj
291    ]
292  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
293    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
294    normalize nodelta
295    [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/
296    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
297      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
298    | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/
299    ]
300  ]
301]
302qed.
303
304(* uses second part of policy_increase *)
305lemma measure_special: ∀program:(Σl:list labelled_instruction.
306    (S (|l|)) < 2^16 ∧ is_well_labelled_p l).
307  ∀policy:Σp:ppc_pc_map.
308    not_jump_default program p ∧
309    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
310    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
311    sigma_compact_unsafe program (create_label_map program) p ∧
312    \fst p < 2^16.
313  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
314  [ None ⇒ True
315  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
316#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy)))
317cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %);
318#p cases p -p #ch #pol normalize nodelta cases pol
319[ / by I/
320| #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|))
321  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
322      measure_int x policy 0 = measure_int x p 0 →
323      sigma_jump_equal x policy p) ?? (pi1 ?? program))
324 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n
325 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le …  Hi)) -Hi #Hi
326   [ @Hind
327     [ @(transitive_le … Hp) / by /
328     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
329       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
330       #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc;
331       #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
332       #y1 #y2 #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
333       cases x2 cases y2 normalize nodelta
334       [1: / by /
335       |2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
336         lapply (measure_incr_or_equal program policy t ? 0)
337         [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
338       |4,7,8: #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
339       |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
340         #_ #H @(injective_plus_r … H)
341       |6: >measure_plus >measure_plus
342         change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
343         #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
344         lapply (measure_incr_or_equal program policy t ? 0)
345         [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
346       |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
347         #_ #H @(injective_plus_r … H)
348       ]
349     | @Hi
350     ]
351   | >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
352     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
353     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
354     #x1 #x2
355     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2
356     normalize nodelta cases x2 cases y2 normalize nodelta
357     [1,5,9: #_ #_ @refl
358     |4,7,8: #_ #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
359     |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
360       lapply (measure_incr_or_equal program policy t ? 0)
361       [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
362     |6: >measure_plus >measure_plus
363        change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
364        #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
365        lapply (measure_incr_or_equal program policy t ? 0)
366        [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
367     ]
368   ]
369 ]
370qed.
371
372lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.
373  S (|l|) < 2^16 ∧ is_well_labelled_p l.
374  match jump_expansion_start program (create_label_map program) with
375  [ None ⇒ True
376  | Some p ⇒ |l| ≤ |program| → measure_int l p 0 = 0
377  ].
378 #l #program lapply (refl ? (jump_expansion_start program (create_label_map program)))
379 cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); #p #Hp #EQ
380 cases p in Hp EQ;
381 [ / by I/
382 | #pl normalize nodelta #Hpl #EQ elim l
383   [ / by refl/
384   | #h #t #Hind #Hp whd in match (measure_int ???);
385     elim (proj2 ?? (proj1 ?? Hpl) (|t|) (le_S_to_le … Hp))
386     #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind
387     @(transitive_le … Hp) @le_n_Sn
388   ]
389 ]
390qed.
391
392(* the actual computation of the fixpoint *)
393definition je_fixpoint: ∀program:(Σl:list labelled_instruction.
394  S (|l|) < 2^16 ∧ is_well_labelled_p l).
395  Σp:option ppc_pc_map.
396    match p with
397      [ None ⇒ True
398      | Some pol ⇒ And (And (out_of_program_none program pol)
399      (sigma_compact program (create_label_map program) pol))
400      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
401      ].
402#program @(\snd (jump_expansion_internal program (S (2*|program|))))
403cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
404   (\snd (pi1 ?? (jump_expansion_internal program k)))
405   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
406[ #Hex cases Hex -Hex #k #Hk
407  lapply (refl ? (jump_expansion_internal program (S (2*|program|))))
408  cases (jump_expansion_internal ? (S (2*|program|))) in ⊢ (???% → %);
409  #x cases x -x #Gno_ch #Go cases Go normalize nodelta
410  [ #H #Heq / by I/
411  | -Go #Gp #HGp #Geq
412    cut (policy_equal_opt program (\snd (jump_expansion_internal program (2*|program|)))
413      (\snd (jump_expansion_internal program (S (2*|program|)))))
414    [ @(pe_trans … (equal_remains_equal program k (proj2 ?? Hk) (S (2*|program|)) (le_S … (le_S_to_le … (proj1 ?? Hk)))))
415      @pe_sym @equal_remains_equal [ @(proj2 ?? Hk) | @(le_S_to_le … (proj1 ?? Hk)) ]
416    | >Geq lapply (refl ? (jump_expansion_internal program (2*|program|)))
417      cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
418      #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
419      [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS)
420      | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq
421        @conj [ @conj
422        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))
423        | @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*)
424          >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq
425          [ destruct (Geq) / by /
426          | cases (jump_expansion_step program (create_label_map (pi1 ?? program)) «Fp,?») in Geq;
427            #x cases x -x #Sch #So normalize nodelta cases So
428            [ normalize nodelta #_ #ABS destruct (ABS)
429            | -So normalize nodelta #Sp #HSp #Seq <(proj1 ?? (pair_destruct ?????? (pi1_eq ???? Seq)))
430              cases Sch in HSp Seq; #HSp #Seq
431              [ @refl
432              | normalize nodelta in Seq; @(proj2 ?? (proj1 ?? HSp))
433                >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Seq))))
434                @Heq
435              ]
436            ]
437          ]
438        ]
439        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
440        ]
441      ]
442    ]
443  ]
444| #Hnex lapply (not_exists_forall … Hnex) -Hnex #Hfa
445  lapply (refl ? (jump_expansion_internal program (2*|program|)))
446  cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
447  #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
448  [ (* None *)
449     #HF #Feq lapply (step_none program (2*|program|) ? 1) >Feq / by /
450    <plus_n_Sm <plus_n_O #H >H -H normalize nodelta / by I/
451  | -Fo #Fp #HFp #Feq lapply (measure_full program Fp ?)
452    [ @le_to_le_to_eq
453      [ @measure_le
454      | cut (∀x:ℕ.x ≤ 2*|program| →
455         ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
456          x ≤ measure_int program p 0))
457        [ #x elim x
458          [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program)))
459            cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %);
460             #z cases z -z normalize nodelta
461             [ #H #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #n #Hn
462               @(absurd … (step_none program 0 ? n))
463               [ whd in match (jump_expansion_internal ??); >Heqn @refl
464               | <Hn >Feq @nmk #H destruct (H)
465               ]
466             | #Zp #HZp #Zeq @(ex_intro ?? Zp) @conj
467               [ whd in match (jump_expansion_internal ??); >Zeq @refl
468               | @le_O_n
469               ]
470             ]
471          | -x #x #Hind #Hx
472            lapply (refl ? (jump_expansion_internal program (S x)))
473            cases (jump_expansion_internal program (S x)) in ⊢ (???% → %);
474            #z cases z -z #Sno_ch #So cases So -So
475            [ #HSp #Seq normalize nodelta @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
476              @(absurd … (step_none program (S x) ? k))
477              [ >Seq @refl
478              | <Hk >Feq @nmk #H destruct (H)
479              ]
480            | #Sp #HSp #Seq @(ex_intro ?? Sp) @conj
481              [ @refl
482              | elim (Hind (transitive_le … (le_n_Sn x) Hx))
483                #pol #Hpol @(le_to_lt_to_lt … (proj2 ?? Hpol))
484                lapply (proj1 ?? Hpol) -Hpol
485                lapply (refl ? (jump_expansion_internal program x))
486                cases (jump_expansion_internal program x) in ⊢ (???% → %);
487                #z cases z -z #Xno_ch #Xo cases Xo
488                [ #HXp #Xeq #abs destruct (abs)
489                | normalize nodelta #Xp #HXp #Xeq #H <(Some_eq ??? H) -H -pol
490                  lapply (Hfa x Hx) >Xeq >Seq whd in match policy_equal_opt;
491                  normalize nodelta #Hpe
492                  lapply (measure_incr_or_equal program Xp program (le_n (|program|)) 0)
493                  [ cases daemon (* reorder *)
494                  | lapply (Hfa x Hx) >Xeq >Seq
495                    lapply (measure_special program «Xp,?»)
496                    [ cases daemon (* reorder *)
497                    | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*)
498                      >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq
499                      [ normalize nodelta #EQ
500                        >(proj2 ?? (pair_destruct ?????? (pi1_eq ???? EQ)))
501                        #_ #abs @⊥ @(absurd ?? abs) / by /
502                      | normalize nodelta cases (jump_expansion_step ???);
503                        #z cases z -z #stch #sto cases sto   
504                        [ normalize nodelta #_ #ABS destruct (ABS)
505                        | -sto #stp normalize nodelta #Hstp #steq
506                          >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? steq))))
507                          #Hms #Hneq #glerp elim (le_to_or_lt_eq … glerp)
508                          [ / by /
509                          | #glorp @⊥ @(absurd ?? Hneq) @Hms @glorp
510                          ]
511                        ]
512                      ]
513                    ]
514                  ]
515                ]
516              ]
517            ]
518          ]
519        | #H elim (H (2*|program|) (le_n ?)) #plp >Feq #Hplp
520          >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp)
521        ]
522      ]
523    | #Hfull
524      whd in match (jump_expansion_internal program (S (2*|program|))); (*65s*)
525      >Feq normalize nodelta cases Fno_ch in HFp Feq; #HFp #Feq
526      normalize nodelta
527      [ @conj [ @conj
528        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))))
529        | @((proj2 ?? HFp) (refl ? true)) ]
530        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
531        ]
532      | cases (jump_expansion_step ???); #z cases z -z #stch #sto cases sto
533        [ #_ / by I/
534        | -sto #stp normalize nodelta #Hstp @conj [ @conj
535          [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))))
536          | @(equal_compact_unsafe_compact ?? Fp)
537            [ @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) @(proj2 ?? (proj1 ?? Hstp))
538              #i #Hi
539              cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
540              [ #Hj
541                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))) i (le_S_to_le … Hi))
542                lapply (Hfull i Hi Hj)
543                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
544                #fp #fj #Hfj >Hfj normalize nodelta
545                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
546                #stp #stj cases stj normalize nodelta
547                [1,2: #H cases H #H2 cases H2 destruct (H2)
548                |3: #_ @refl
549                ]
550              | #Hj >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj)
551                >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl
552              ]
553            | cases daemon 
554            | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))
555            ]
556          ]
557        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))) ]
558        ]
559      ]
560    ]
561  ]
562| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
563  #x cases x -x #nch #npol normalize nodelta #Hnpol
564  #x cases x -x #Sch #Spol normalize nodelta #HSpol
565  cases npol in Hnpol; cases Spol in HSpol;
566  [ #Hnpol #HSpol %1 //
567  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
568    #H destruct (H)
569  |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
570      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
571      #x1 #x2
572      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
573      #y1 #y2 normalize nodelta
574      @dec_eq_jump_length
575  ]
576]
577qed.
578
579include alias "arithmetics/nat.ma".
580include alias "basics/logic.ma".
581
582(* The glue between Policy and Assembly. *)
583(*CSC: modified to really use the specification in Assembly.ma.*)
584definition jump_expansion':
585∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16).
586 option (Σsigma_policy:(Word → Word) × (Word → bool).
587   let 〈sigma,policy〉≝ sigma_policy in
588   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy)
589   ≝
590 λprogram.
591  let f: option ppc_pc_map ≝ je_fixpoint (\snd program) in
592  match f return λx.f = x → ? with
593  [ None ⇒ λp.None ?
594  | Some x ⇒ λp.Some ?
595      «〈(λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
596          bitvector_of_nat 16 pc),
597         (λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
598          jmpeqb jl long_jump)〉,?»
599  ] (refl ? f).
600normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta
601lapply (pi2 ?? (je_fixpoint (\snd program))) >p normalize nodelta cases x
602#fpc #fpol #Hfpol
603@conj
604[ lapply (proj2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
605  #x #y #Hx normalize nodelta >Hx / by refl/
606| #ppc #ppc_ok @conj
607  [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok)
608    >bitvector_of_nat_inverse_nat_of_bitvector
609    lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
610    [ normalize nodelta #_ #abs cases abs
611    | #x cases x -x #x1 #y1 normalize nodelta #Hl_ppc
612      >(plus_n_O (nat_of_bitvector 16 ppc)) >plus_n_Sm <add_bitvector_of_nat_plus
613      >bitvector_of_nat_inverse_nat_of_bitvector
614      lapply (refl ? (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol))
615      cases (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol) in ⊢ (???% → %);
616      [ normalize nodelta #_ #abs cases abs
617      | #x cases x -x #x2 #y2 normalize nodelta #Hl_Sppc
618        #Hcompact >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉)
619        >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
620        >add_bitvector_of_nat_plus whd in match (fetch_pseudo_instruction ???);
621        >(nth_safe_nth … 〈None ?, Comment []〉)
622        >Hcompact <plus_n_O
623        cases (nth (nat_of_bitvector ? ppc) ? (\snd program) ?) #a #b normalize nodelta
624        whd in match instruction_size; normalize nodelta
625        whd in match assembly_1_pseudoinstruction; normalize nodelta
626        whd in match expand_pseudo_instruction; normalize nodelta
627        cases b
628        [2,3,6: #p [3: #q] normalize nodelta @refl
629        |4,5: #p normalize nodelta
630          >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta
631          >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
632          whd in match (create_label_map ?);
633          cases (lookup ?? (bitvector_of_nat ?
634          (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉)
635          #z1 #z2 normalize nodelta @refl
636        |1: #pi cases pi
637          [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:
638            [1,2,3,6,7,24,25: #p #q
639            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #p]
640            normalize nodelta @refl
641          |9,10,11,12,13,14,15,16,17: [1,2,6,7: #p |3,4,5,8,9: #q #p] normalize nodelta
642            whd in match expand_relative_jump; normalize nodelta
643            whd in match expand_relative_jump_internal; normalize nodelta
644            >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta
645            >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
646            whd in match (create_label_map ?);
647            cases (lookup ?? (bitvector_of_nat ?
648            (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉)
649            #z1 #z2 normalize nodelta @refl
650          ]
651        ]
652      ]
653    ]
654  | cases daemon (* XXX remains to be done *)
655  ]
656]
657qed.           
Note: See TracBrowser for help on using the repository browser.