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