source: src/ASM/Policy.ma @ 2055

Last change on this file since 2055 was 2055, checked in by sacerdot, 7 years ago

Warning: this commit adds an hypothesis that breaks all of assembly stuff.

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