Context Navigation

Policy.ma @ 2141

Last change on this file since 2141 was 2141, checked in by boender, 7 years ago
committed working version
File size: 29.3 KB

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

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format