source: src/ASM/Policy.ma @ 2152

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