source: src/ASM/Policy.ma @ 2714

Last change on this file since 2714 was 2700, checked in by sacerdot, 7 years ago
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
File size: 35.6 KB
Line 
1include "ASM/PolicyStep.ma".
2
3include alias "basics/lists/list.ma".
4include alias "arithmetics/nat.ma".
5include alias "basics/logic.ma".
6
7let rec jump_expansion_internal (program: Σl:list labelled_instruction.
8  lt (S (|l|)) 2^16 ∧ is_well_labelled_p l) (n: ℕ)
9  on n:(Σx:bool × (option ppc_pc_map).
10    let 〈no_ch,pol〉 ≝ x in
11    match pol with
12    [ None ⇒ True
13    | Some x ⇒
14      And (And (And (And
15        (not_jump_default program x)
16        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0))
17        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
18        (sigma_compact_unsafe program (create_label_map program) x))
19        (\fst x ≤ 2^16)
20    ]) ≝
21 let labels ≝ create_label_map program in
22  match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with
23  [ O   ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉
24  | S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
25          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
26          [ None    ⇒ λp2.〈false,None ?〉
27          | Some op ⇒ λp2.if no_ch
28            then pi1 ?? (jump_expansion_internal program m)
29            else pi1 ?? (jump_expansion_step program (pi1 ?? labels) «op,?»)
30          ] (refl … z)
31  ] (refl … n).
32[5: #l #_ %
33| normalize nodelta cases (jump_expansion_start program (create_label_map program))
34  #x cases x -x
35  [ #H %
36  | #sigma normalize nodelta #H @conj [ @conj
37    [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
38    | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
39    ]
40    | @(proj2 ?? H)
41    ]
42  ]
43| %
44| cases no_ch in p1; #p1
45  [ @(pi2 ?? (jump_expansion_internal program m))
46  | cases (jump_expansion_step ???)
47    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
48    [ #_ %
49    | #j2 #H2 @conj [ @conj
50      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
51      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
52      ]
53      | @(proj2 ?? H2)
54      ]
55    ]
56  ]
57| cases (jump_expansion_internal program m) in p1;
58  #p cases p -p #p #r cases r normalize nodelta
59  [ #_ >p2 #ABS destruct (ABS)
60  | #map >p2 normalize nodelta
61    #H #eq destruct (eq) @H
62  ]
63]
64qed.
65
66 
67lemma pe_int_refl: ∀program.reflexive ? (sigma_jump_equal program).
68#program whd #x whd #n #Hn
69cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉)
70#y #z normalize nodelta @refl
71qed.
72
73lemma pe_int_sym: ∀program.symmetric ? (sigma_jump_equal program).
74#program whd #x #y #Hxy whd #n #Hn
75lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
76#x1 #x2
77cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉)
78#y1 #y2 normalize nodelta //
79qed.
80 
81lemma pe_int_trans: ∀program.transitive ? (sigma_jump_equal program).
82#program whd #x #y #z whd in match (sigma_jump_equal ???); whd in match (sigma_jump_equal ?y ?);
83whd in match (sigma_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
84lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
85#x1 #x2
86cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) #y1 #y2
87cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,short_jump〉) #z1 #z2
88normalize nodelta //
89qed.
90
91definition policy_equal_opt ≝
92  λprogram:list labelled_instruction.λp1,p2:option ppc_pc_map.
93  match p1 with
94  [ Some x1 ⇒ match p2 with
95              [ Some x2 ⇒ sigma_jump_equal program x1 x2
96              | _       ⇒ False
97              ]
98  | None    ⇒ p2 = None ?
99  ].
100
101lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program).
102#program whd #x whd cases x try % #y @pe_int_refl
103qed.
104
105lemma pe_sym: ∀program.symmetric ? (policy_equal_opt program).
106#program whd #x #y #Hxy whd cases y in Hxy;
107[ cases x
108  [ #_ %
109  | #x' #H @⊥ @(absurd ? H) /2 by nmk/
110  ]
111| #y' cases x
112  [ #H @⊥ @(absurd ? H) whd in match (policy_equal_opt ???); @nmk #H destruct (H)
113  | #x' #H @pe_int_sym @H
114  ]
115]
116qed.
117
118lemma pe_trans: ∀program.transitive ? (policy_equal_opt program).
119#program whd #x #y #z cases x
120[ #Hxy #Hyz >Hxy in Hyz; //
121| #x' cases y
122  [ #H @⊥ @(absurd ? H) /2 by nmk/
123  | #y' cases z
124    [ #_ #H @⊥ @(absurd ? H) /2 by nmk/
125    | #z' @pe_int_trans
126    ]
127  ]
128]
129qed.
130
131definition step_none: ∀program.∀n.
132  (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? →
133  ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?.
134#program #n lapply (refl ? (jump_expansion_internal program n))
135 cases (jump_expansion_internal program n) in ⊢ (???% → %);
136 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
137[ <plus_n_O >Heqj @Hj
138| #k' -k <plus_n_Sm
139  lapply (refl ? (jump_expansion_internal program (n+k')))
140  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → %);
141  #x2 cases x2 -x2 #c2 #p2 normalize nodelta #H #Heqj2
142  cases p2 in H Heqj2;
143  [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
144    >Heqj2 normalize nodelta @refl
145  | #x #H #Heqj2 #abs destruct (abs)
146  ]
147]
148qed.
149
150lemma jump_pc_equal: ∀program.∀n.
151  match \snd (jump_expansion_internal program n) with
152  [ None   ⇒ True
153  | Some p1 ⇒ match \snd (jump_expansion_internal program (S n)) with
154    [ None ⇒ True
155    | Some p2 ⇒ sigma_jump_equal program p1 p2 → sigma_pc_equal program p1 p2
156    ]
157  ].
158 #program #n lapply (refl ? (jump_expansion_internal program n))
159 cases (jump_expansion_internal program n) in ⊢ (???% → %); #x cases x -x
160 #Nno_ch #No cases No
161 [ normalize nodelta #HN #NEQ @I
162 | #Npol normalize nodelta #HN #NEQ lapply (refl ? (jump_expansion_internal program (S n)))
163   cases (jump_expansion_internal program (S n)) in ⊢ (???% → %); #x cases x -x
164   #Sno_ch #So cases So
165   [ normalize nodelta #HS #SEQ @I
166   | #Spol normalize nodelta #HS #SEQ #Hj
167     whd in match (jump_expansion_internal program (S n)) in SEQ; (*80s*)
168     >NEQ in SEQ; normalize nodelta cases Nno_ch in HN;
169     [ #HN normalize nodelta #SEQ >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? SEQ))))
170       / by /
171     | #HN normalize nodelta cases (jump_expansion_step ???)     
172       #x cases x -x #Stno_ch #Stno_o normalize nodelta cases Stno_o
173       [ normalize nodelta #_ #H destruct (H)
174       | #Stno_p normalize nodelta #HSt #STeq
175         <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? STeq)))) in Hj; #Hj
176         @(proj2 ?? (proj1 ?? HSt)) @(proj2 ?? (proj1 ?? (proj1 ?? HSt))) @Hj
177       ]
178     ]
179   ]
180 ]
181qed.     
182
183lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
184  ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n)))
185   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
186  policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
187    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
188#program #n #Heq inversion (jump_expansion_internal program n) #x cases x -x
189 #no_ch #pol cases pol normalize nodelta
190 [ #H #Hj lapply (step_none program n) >Hj #Hn lapply (Hn (refl ??) 1) <plus_n_Sm <plus_n_O
191   #HSeq >HSeq lapply (Hn (refl ??) 2) <plus_n_Sm <plus_n_Sm <plus_n_O #HSSeq >HSSeq / by /
192 | -pol #pol #Hpol #Hn >Hn in Heq; whd in match (policy_equal_opt ???);
193   lapply (refl ? (jump_expansion_internal program (S n)))
194   whd in match (jump_expansion_internal program (S n)) in ⊢ (???% → ?); >Hn
195   normalize nodelta inversion no_ch #Hno_ch normalize nodelta #Seq >Seq
196   [ #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
197     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
198     normalize nodelta #Teq >Teq @pe_refl
199   | #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
200     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
201     normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq ⊢ ?; (*320s*)
202     #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol
203     [ normalize nodelta #HSn #Heq #Seq cases Heq
204     | -Spol #Spol normalize nodelta cases Sno_ch normalize nodelta #HSn #Heq #Seq
205       [ @pe_refl
206       | cases daemon
207       ]
208     ]
209   ]
210 ]
211qed.
212
213lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.
214  S (|l|) < 2^16 ∧ is_well_labelled_p l).∀n:ℕ.
215  policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
216   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
217  ∀k.k ≥ n → policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
218   (\snd (pi1 … (jump_expansion_internal program k))).
219#program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
220lapply Heq -Heq; lapply n -n; elim z -z;
221[ #n #Heq <plus_n_O @pe_refl
222| #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z);
223  @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n)))))
224  [ @Heq
225  | @Hind @pe_step @Heq
226  ]
227]
228qed.
229
230(* this number monotonically increases over iterations, maximum 2*|program| *)
231let rec measure_int (program: list labelled_instruction) (policy: ppc_pc_map) (acc: ℕ)
232 on program: ℕ ≝
233 match program with
234 [ nil      ⇒ acc
235 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) with
236   [ long_jump   ⇒ measure_int t policy (acc + 2)
237   | absolute_jump ⇒ measure_int t policy (acc + 1)
238   | _           ⇒ measure_int t policy acc
239   ]
240 ].
241
242lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
243 measure_int program policy (x+d) = measure_int program policy x + d.
244#program #policy #x #d generalize in match x; -x elim d
245[ //
246| -d; #d #Hind elim program
247  [ / by refl/
248  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
249    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
250    [ normalize nodelta @Hd
251    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
252      @Hd
253    ]
254  ]
255]
256qed.
257
258lemma measure_le: ∀program.∀policy.
259  measure_int program policy 0 ≤ 2*|program|.
260#program #policy elim program
261[ normalize @le_n
262| #h #t #Hind whd in match (measure_int ???);
263  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
264  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
265  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
266    @le_plus [1,3: @Hind |2,4: / by le_n/ ]
267  ]
268]
269qed.
270
271(* uses the second part of policy_increase *)
272lemma measure_incr_or_equal: ∀program:(Σl:list labelled_instruction.
273  S (|l|) <2^16 ∧ is_well_labelled_p l).
274  ∀policy:Σp:ppc_pc_map.
275    (*out_of_program_none program p ∧*)
276    not_jump_default program p ∧
277    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
278    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
279    sigma_compact_unsafe program (pi1 … (create_label_map program)) p ∧
280    \fst p ≤ 2^16.
281  ∀l.|l| ≤ |program| → ∀acc:ℕ.
282  match \snd (pi1 ?? (jump_expansion_step program (pi1 … (create_label_map program)) policy)) with
283  [ None   ⇒ True
284  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
285  ].
286[2: #l #_ %]
287#program #policy #l elim l -l;
288[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
289| #h #t #Hind #Hp #acc
290  inversion (jump_expansion_step ???) #pi1 cases pi1 -pi1 #c #r cases r
291  [ / by I/
292  | #x normalize nodelta #Hx #Hjeq
293    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) (le_S_to_le … Hp))
294    whd in match (measure_int ???); whd in match (measure_int ? x ?);
295    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
296    #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,short_jump〉)
297    #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2
298    [1,4,5,7,8,9: #H cases H
299    |2,3,6: #_ normalize nodelta
300      [1,2: @(transitive_le ? (measure_int t x acc))
301      |3: @(transitive_le ? (measure_int t x (acc+1)))
302      ]
303      [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
304      >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
305    |11,12,13,15,16,17: #H destruct (H)
306    |10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
307    ]
308  ]
309]
310qed.
311
312lemma measure_full: ∀program.∀policy.
313  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
314  is_jump (\snd (nth i ? program 〈None ?,Comment EmptyString〉)) →
315  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.
316#program #policy elim program in ⊢ (% → ∀i.% → ? → %);
317[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
318| #h #t #Hind #Hm #i #Hi #Hj
319  cases (le_to_or_lt_eq … Hi) -Hi
320  [ #Hi @Hind
321    [ 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      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le
325        @monotonic_lt_times_r [/2/] %
326      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
327        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
328      | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/
329      ]
330    | @(le_S_S_to_le … Hi)
331    | @Hj
332    ]
333  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
334    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
335    normalize nodelta
336    [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le
337      @monotonic_lt_times_r try % /2/
338    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
339      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
340    | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/
341    ]
342  ]
343]
344qed.
345
346(* uses second part of policy_increase *)
347lemma measure_special: ∀program:(Σl:list labelled_instruction.
348    (S (|l|)) < 2^16 ∧ is_well_labelled_p l).
349  ∀policy:Σp:ppc_pc_map.
350    not_jump_default program p ∧
351    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
352    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
353    sigma_compact_unsafe program (pi1 … (create_label_map program)) p ∧
354    \fst p ≤ 2^16.
355  match (\snd (pi1 ?? (jump_expansion_step program (pi1 … (create_label_map program)) policy))) with
356  [ None ⇒ True
357  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
358[2: #l #_ %]
359#program #policy inversion (jump_expansion_step ???)
360#p cases p -p #ch #pol normalize nodelta cases pol
361[ / by I/
362| #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|))
363  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
364      measure_int x policy 0 = measure_int x p 0 →
365      sigma_jump_equal x policy p) ?? (pi1 ?? program))
366 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n
367 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le …  Hi)) -Hi #Hi
368   [ @Hind
369     [ @(transitive_le … Hp) / by /
370     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
371       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
372       #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc;
373       #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
374       #y1 #y2 #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
375       cases x2 cases y2 normalize nodelta
376       [1: / by /
377       |2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
378         lapply (measure_incr_or_equal program policy t ? 0)
379         [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
380       |4,7,8: #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
381       |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
382         #_ #H @(injective_plus_r … H)
383       |6: >measure_plus >measure_plus
384         change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
385         #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
386         lapply (measure_incr_or_equal program policy t ? 0)
387         [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
388       |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
389         #_ #H @(injective_plus_r … H)
390       ]
391     | @Hi
392     ]
393   | >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
394     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
395     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
396     #x1 #x2
397     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2
398     normalize nodelta cases x2 cases y2 normalize nodelta
399     [1,5,9: #_ #_ @refl
400     |4,7,8: #_ #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
401     |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
402       lapply (measure_incr_or_equal program policy t ? 0)
403       [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
404     |6: >measure_plus >measure_plus
405        change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
406        #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
407        lapply (measure_incr_or_equal program policy t ? 0)
408        [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
409     ]
410   ]
411 ]
412qed.
413
414lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.
415  S (|l|) < 2^16 ∧ is_well_labelled_p l.
416  match jump_expansion_start program (create_label_map program) with
417  [ None ⇒ True
418  | Some p ⇒ |l| ≤ |program| → measure_int l p 0 = 0
419  ].
420 #l #program lapply (refl ? (jump_expansion_start program (create_label_map program)))
421 cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); #p #Hp #EQ
422 cases p in Hp EQ;
423 [ / by I/
424 | #pl normalize nodelta #Hpl #EQ elim l
425   [ / by refl/
426   | #h #t #Hind #Hp whd in match (measure_int ???);
427     elim (proj2 ?? (proj1 ?? Hpl) (|t|) (le_S_to_le … Hp))
428     #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind
429     @(transitive_le … Hp) @le_n_Sn
430   ]
431 ]
432qed.
433
434(* the actual computation of the fixpoint *)
435definition je_fixpoint: ∀program:(Σl:list labelled_instruction.
436  S (|l|) < 2^16 ∧ is_well_labelled_p l).
437  Σp:option ppc_pc_map.
438    match p with
439      [ None ⇒ True
440      | Some pol ⇒ And (And (And
441          (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
442          (\fst pol = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd pol) 〈0,short_jump〉)))
443          (sigma_compact program (pi1 … (create_label_map program)) pol))
444          (\fst pol ≤ 2^16)
445      ].
446#program @(\snd (jump_expansion_internal program (S (2*|program|))))
447cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
448   (\snd (pi1 ?? (jump_expansion_internal program k)))
449   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
450[ #Hex cases Hex -Hex #k #Hk
451  inversion (jump_expansion_internal ??)
452  #x cases x -x #Gno_ch #Go cases Go normalize nodelta
453  [ #H #Heq / by I/
454  | -Go #Gp #HGp #Geq
455    cut (policy_equal_opt program (\snd (jump_expansion_internal program (2*|program|)))
456      (\snd (jump_expansion_internal program (S (2*|program|)))))
457    [ @(pe_trans … (equal_remains_equal program k (proj2 ?? Hk) (S (2*|program|)) (le_S … (le_S_to_le … (proj1 ?? Hk)))))
458      @pe_sym @equal_remains_equal [ @(proj2 ?? Hk) | @(le_S_to_le … (proj1 ?? Hk)) ]
459    | >Geq lapply (refl ? (jump_expansion_internal program (2*|program|)))
460      cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
461      #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
462      [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS)
463      | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq
464        @conj [ @conj [ @conj
465        [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
466        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
467        ]
468        | @(equal_compact_unsafe_compact ? Fp)
469          [ lapply (jump_pc_equal program (2*|program|))
470            >Feq >Geq normalize nodelta #H @H @Heq
471          | @Heq
472          | cases daemon (* true, but have to add this to properties *)
473          | cases daemon
474          | @(proj2 ?? (proj1 ?? HGp))
475          ]
476        ]
477        | @(proj2 ?? HGp)
478        ]
479      ]
480    ]
481  ]
482| #Hnex lapply (not_exists_forall … Hnex) -Hnex #Hfa
483  lapply (refl ? (jump_expansion_internal program (2*|program|)))
484  cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
485  #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
486  [ (* None *)
487     #HF #Feq lapply (step_none program (2*|program|) ? 1) >Feq / by /
488    <plus_n_Sm <plus_n_O #H >H -H normalize nodelta / by I/
489  | -Fo #Fp #HFp #Feq lapply (measure_full program Fp ?)
490    [ @le_to_le_to_eq
491      [ @measure_le
492      | cut (∀x:ℕ.x ≤ 2*|program| →
493         ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
494          x ≤ measure_int program p 0))
495        [ #x elim x
496          [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program)))
497            cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %);
498             #z cases z -z normalize nodelta
499             [ #H #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #n #Hn
500               @(absurd … (step_none program 0 ? n))
501               [ whd in match (jump_expansion_internal ??); >Heqn @refl
502               | <Hn >Feq @nmk #H destruct (H)
503               ]
504             | #Zp #HZp #Zeq @(ex_intro ?? Zp) @conj
505               [ whd in match (jump_expansion_internal ??); >Zeq @refl
506               | @le_O_n
507               ]
508             ]
509          | -x #x #Hind #Hx
510            lapply (refl ? (jump_expansion_internal program (S x)))
511            cases (jump_expansion_internal program (S x)) in ⊢ (???% → %);
512            #z cases z -z #Sno_ch #So cases So -So
513            [ #HSp #Seq normalize nodelta @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
514              @(absurd … (step_none program (S x) ? k))
515              [ >Seq @refl
516              | <Hk >Feq @nmk #H destruct (H)
517              ]
518            | #Sp #HSp #Seq @(ex_intro ?? Sp) @conj
519              [ @refl
520              | elim (Hind (transitive_le … (le_n_Sn x) Hx))
521                #pol #Hpol @(le_to_lt_to_lt … (proj2 ?? Hpol))
522                lapply (proj1 ?? Hpol) -Hpol
523                lapply (refl ? (jump_expansion_internal program x))
524                cases (jump_expansion_internal program x) in ⊢ (???% → %);
525                #z cases z -z #Xno_ch #Xo cases Xo
526                [ #HXp #Xeq #abs destruct (abs)
527                | normalize nodelta #Xp #HXp #Xeq #H <(Some_eq ??? H) -H -pol
528                  lapply (Hfa x Hx) >Xeq >Seq whd in match policy_equal_opt;
529                  normalize nodelta #Hpe
530                  lapply (measure_incr_or_equal program Xp program (le_n (|program|)) 0)
531                  [ @HXp
532                  | lapply (Hfa x Hx) >Xeq >Seq
533                    lapply (measure_special program «Xp,?»)
534                    [ @HXp
535                    | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*)
536                      >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq
537                      [ normalize nodelta #EQ
538                        >(proj2 ?? (pair_destruct ?????? (pi1_eq ???? EQ)))
539                        #_ #abs @⊥ @(absurd ?? abs) / by /
540                      | normalize nodelta cases (jump_expansion_step ???);
541                        #z cases z -z #stch #sto cases sto   
542                        [ normalize nodelta #_ #ABS destruct (ABS)
543                        | -sto #stp normalize nodelta #Hstp #steq
544                          >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? steq))))
545                          #Hms #Hneq #glerp elim (le_to_or_lt_eq … glerp)
546                          [ / by /
547                          | #glorp @⊥ @(absurd ?? Hneq) @Hms @glorp
548                          ]
549                        ]
550                      ]
551                    ]
552                  ]
553                ]
554              ]
555            ]
556          ]
557        | #H elim (H (2*|program|) (le_n ?)) #plp >Feq #Hplp
558          >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp)
559        ]
560      ]
561    | #Hfull lapply (refl ? (jump_expansion_internal program (S (2*|program|))))
562      cases (jump_expansion_internal program (S (2*|program|))) in ⊢ (???% → %);
563      #z cases z -z #Gch #Go cases Go normalize nodelta
564      [ #HGp #Geq @I
565      | -Go #Gp normalize nodelta #HGp #Geq @conj [ @conj [ @conj
566        [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
567        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
568        ]
569        | @(equal_compact_unsafe_compact ? Fp)
570          [1,2:
571            [1: lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
572            #H @H ]
573            #i #Hi
574            inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)))
575            [1,3: #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
576              >Feq in Geq; normalize nodelta cases Fno_ch
577              [1,3: normalize nodelta #Heq
578                >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) %
579              |2,4: normalize nodelta cases (jump_expansion_step ???)
580                #x cases x -x #stch #sto normalize nodelta cases sto
581                [1,3: normalize nodelta #_ #X destruct (X)
582                |2,4: -sto #stp normalize nodelta #Hst #Heq
583                   <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq))))
584                   lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi))
585                   lapply (Hfull i Hi ?) [1,3: >Hj %]
586                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
587                   #fp #fj #Hfj >Hfj normalize nodelta
588                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
589                   #stp #stj cases stj normalize nodelta
590                   [1,2,4,5: #H cases H #H2 cases H2 destruct (H2)
591                   |3,6: #_ @refl
592                   ]
593                ]
594              ]
595            |2,4: #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2,4:>Hj %]
596              >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2,4:>Hj] %
597            ]
598          | cases daemon (* true, but have to add to properties in some way *)
599          | cases daemon
600          | @(proj2 ?? (proj1 ?? HGp))
601          ]
602        ]
603        | @(proj2 ?? HGp)
604        ]
605      ]
606    ]
607  ]
608| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
609  #x cases x -x #nch #npol normalize nodelta #Hnpol
610  #x cases x -x #Sch #Spol normalize nodelta #HSpol
611  cases npol in Hnpol; cases Spol in HSpol;
612  [ #Hnpol #HSpol %1 //
613  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
614    #H destruct (H)
615  |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
616      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
617      #x1 #x2
618      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
619      #y1 #y2 normalize nodelta
620      @dec_eq_jump_length
621  ]
622]
623qed.
624
625include alias "arithmetics/nat.ma".
626include alias "basics/logic.ma".
627
628lemma pc_increases: ∀i,j:ℕ.∀program.∀pol:Σp:ppc_pc_map.
629  And (And (And
630    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)
631    (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
632    (sigma_compact program (create_label_map program) p))
633    (\fst p ≤ 2^16).i ≤ j → j ≤ |program| →
634  \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 i) (\snd pol) 〈0,short_jump〉) ≤
635  \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 j) (\snd pol) 〈0,short_jump〉).
636 #i #j #program #pol #H elim (le_to_eq_plus … H) #n #Hn >Hn -Hn -j elim n
637 [ <plus_n_O #_ @le_n
638 | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H)))
639   lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.zero 16) (i+n) H)
640   lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)))
641   cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %);
642   [ normalize nodelta #_ #abs cases abs
643   | #x cases x -x #pc #jl #EQ normalize nodelta
644     lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)))
645     cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %);
646     [ normalize nodelta #_ #abs cases abs
647     | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp
648       >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
649       >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r
650     ]
651   ]
652 ]
653qed.
654 
655(* The glue between Policy and Assembly. *)
656definition jump_expansion':
657∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
658 option (Σsigma_policy:(Word → Word) × (Word → bool).
659   let 〈sigma,policy〉≝ sigma_policy in
660   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy)
661   ≝
662 λprogram.
663  let f: option ppc_pc_map ≝ je_fixpoint (\snd program) in
664  match f return λx.f = x → ? with
665  [ None ⇒ λp.None ?
666  | Some x ⇒ λp.Some ?
667      «〈(λppc.let pc ≝ \fst (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in
668          bitvector_of_nat 16 pc),
669         (λppc.let jl ≝ \snd (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in
670          jmpeqb jl long_jump)〉,?»
671  ] (refl ? f).
672normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta
673lapply (pi2 ?? (je_fixpoint (\snd program))) >p normalize nodelta cases x
674#fpc #fpol #Hfpol cases Hfpol ** #Hfpol1 #Hfpol2 #Hfpol3 #Hfpol4
675@conj
676[ >Hfpol1 %
677| #ppc #ppc_ok normalize nodelta
678  >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) =
679       \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment EmptyString〉))
680  [2: whd in match fetch_pseudo_instruction; normalize nodelta
681   >(nth_safe_nth … 〈None ?, Comment EmptyString〉)
682   cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment EmptyString〉)
683   #lbl #ins % ]
684  lapply (Hfpol3 ? (nat_of_bitvector ? ppc) ppc_ok)
685  [2: >bitvector_of_nat_inverse_nat_of_bitvector
686  inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ]
687  * #pc #jl #Hl normalize nodelta
688  inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ]
689  * #Spc #Sjl #SHL lapply SHL
690  <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
691  #SHl normalize nodelta #Hcompact
692  @conj
693  [ >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉)
694    >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
695    >add_bitvector_of_nat_plus >Hcompact %
696  | (* Basic proof scheme:
697       - ppc < |snd program|, hence our instruction is in the program
698       - either we are the last non-zero-size instruction, in which case we are
699         either smaller than 2^16 (because the entire program is), or we are exactly
700         2^16 and something weird happens
701       - or we are not, in which case we are definitely smaller than 2^16 (by transitivity
702         through the next non-zero instruction)
703    *)
704    elim (le_to_or_lt_eq … Hfpol4) #Hfpc
705    [ %1 @(le_to_lt_to_lt … Hfpc) >Hfpol2
706      >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
707      >nat_of_bitvector_bitvector_of_nat_inverse
708      [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
709          >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
710          #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @H ]
711      lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
712      >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >Hcompact #X @X
713    | (* the program is of length 2^16 and ppc is followed by only zero-size instructions
714       * until the end of the program *)
715      elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)))
716      [ >bitvector_of_nat_inverse_nat_of_bitvector
717        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc normalize nodelta
718        >nat_of_bitvector_bitvector_of_nat_inverse
719        [2: <Hfpc >Hfpol2 @Hpc ]
720        elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
721        <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) #HSpc
722        [ %1 >Hcompact in HSpc; #X @X
723        | %2 @conj
724          [2: >Hcompact in HSpc; #X @X
725          | #ppc' #ppc_ok' #Hppc'
726            (* S ppc < ppc' < |\snd program| *)
727            (* lookup S ppc = 2^16 *)
728            (* lookup |\snd program| = 2^16 *)
729            (* lookup ppc' = 2^16 → instruction size = 0 *)
730            lapply (Hfpol3 ? (nat_of_bitvector ? ppc') ppc_ok')
731            [2: >bitvector_of_nat_inverse_nat_of_bitvector
732            inversion (lookup_opt ????) normalize nodelta
733            [ #_ #abs cases abs
734            | * #xpc #xjl #XEQ normalize nodelta
735              inversion (lookup_opt ????) normalize nodelta
736              [ #_ #abs cases abs
737              | * #Sxpc #Sxjl #SXEQ normalize nodelta
738                #Hpcompact
739                lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
740                >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
741                lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
742                <Hfpol2 >Hfpc #Hle2
743                lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1
744                >bitvector_of_nat_inverse_nat_of_bitvector
745                >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
746                lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
747                >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
748                lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
749                <Hfpol2 >Hfpc #Hle2
750                lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2
751                >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc
752                >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H
753                @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
754                normalize nodelta >(nth_safe_nth … 〈None ?, Comment EmptyString〉)
755                cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment EmptyString〉) in H;
756                #lbl #ins normalize nodelta #X @sym_eq @X
757              ]
758            ] ]
759          ]
760        ]
761      | >bitvector_of_nat_inverse_nat_of_bitvector
762        <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc
763        %1 >Hpc
764        >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?));
765        <plus_O_n whd in match instruction_size; normalize nodelta
766        inversion (assembly_1_pseudoinstruction ??? ppc ??)
767        #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
768        #Hli >Hli
769        lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc ??)
770        [6: >Hass / by / ]
771      ]
772    ]
773  ] ]
774]
775qed.
Note: See TracBrowser for help on using the repository browser.