source: src/ASM/Policy.ma @ 2059

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