Context Navigation

Policy.ma @ 2034

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

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

Download in other formats:

Original Format