source: src/ASM/Policy.ma @ 2101

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