Context Navigation

Policy.ma @ 2317

Last change on this file since 2317 was 2317, checked in by boender, 8 years ago
small changes to make things compile
File size: 35.6 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
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	]
64	qed.
65
66
67	lemma pe_int_refl: ∀program.reflexive ? (sigma_jump_equal program).
68	#program whd #x whd #n #Hn
69	cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉)
70	#y #z normalize nodelta @refl
71	qed.
72
73	lemma pe_int_sym: ∀program.symmetric ? (sigma_jump_equal program).
74	#program whd #x #y #Hxy whd #n #Hn
75	lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
76	#x1 #x2
77	cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉)
78	#y1 #y2 normalize nodelta //
79	qed.
80
81	lemma 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 ?);
83	whd in match (sigma_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
84	lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
85	#x1 #x2
86	cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) #y1 #y2
87	cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,short_jump〉) #z1 #z2
88	normalize nodelta //
89	qed.
90
91	definition 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
101	lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program).
102	#program whd #x whd cases x try % #y @pe_int_refl
103	qed.
104
105	lemma 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	]
116	qed.
117
118	lemma 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	]
129	qed.
130
131	definition 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	]
148	qed.
149
150	lemma 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	]
181	qed.
182
183	lemma 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	]
211	qed.
212
213	lemma 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;
220	lapply 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	]
228	qed.
229
230	(* this number monotonically increases over iterations, maximum 2\|program\| )
231	let 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
242	lemma 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	]
256	qed.
257
258	lemma 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	]
269	qed.
270
271	(* uses the second part of policy_increase *)
272	lemma 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	]
310	qed.
311
312	lemma measure_full: ∀program.∀policy.
313	measure_int program policy 0 = 2*\|program\| → ∀i.i<\|program\| →
314	is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) →
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 /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	\| @(le_S_S_to_le … Hi)
330	\| @Hj
331	]
332	\| #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
333	cases (\snd (bvt_lookup … (bitvector_of_nat ? (\|t\|)) (\snd policy) 〈0,short_jump〉)) in Hm;
334	normalize nodelta
335	[ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/
336	\| >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
337	<(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
338	\| >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/
339	]
340	]
341	]
342	qed.
343
344	(* uses second part of policy_increase *)
345	lemma measure_special: ∀program:(Σl:list labelled_instruction.
346	(S (\|l\|)) < 2^16 ∧ is_well_labelled_p l).
347	∀policy:Σp:ppc_pc_map.
348	not_jump_default program p ∧
349	\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
350	\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (\|program\|)) (\snd p) 〈0,short_jump〉) ∧
351	sigma_compact_unsafe program (pi1 … (create_label_map program)) p ∧
352	\fst p ≤ 2^16.
353	match (\snd (pi1 ?? (jump_expansion_step program (pi1 … (create_label_map program)) policy))) with
354	[ None ⇒ True
355	\| Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
356	[2: #l #_ %]
357	#program #policy inversion (jump_expansion_step ???)
358	#p cases p -p #ch #pol normalize nodelta cases pol
359	[ / by I/
360	\| #p normalize nodelta #Hpol #eqpol lapply (le_n (\|program\|))
361	@(list_ind ? (λx.\|x\| ≤ \|pi1 ?? program\| →
362	measure_int x policy 0 = measure_int x p 0 →
363	sigma_jump_equal x policy p) ?? (pi1 ?? program))
364	[ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n
365	\| #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
366	[ @Hind
367	[ @(transitive_le … Hp) / by /
368	\| whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
369	lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (\|t\|) (le_S_to_le … Hp))
370	#Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) ? 〈0,short_jump〉) in Hm Hinc;
371	#x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) ? 〈0,short_jump〉);
372	#y1 #y2 #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
373	cases x2 cases y2 normalize nodelta
374	[1: / by /
375	\|2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
376	lapply (measure_incr_or_equal program policy t ? 0)
377	[1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
378	\|4,7,8: #H elim H #H2 [1,3,5: cases H2 \|2,4,6: destruct (H2) ]
379	\|5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
380	#_ #H @(injective_plus_r … H)
381	\|6: >measure_plus >measure_plus
382	change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
383	#_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
384	lapply (measure_incr_or_equal program policy t ? 0)
385	[ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
386	\|9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
387	#_ #H @(injective_plus_r … H)
388	]
389	\| @Hi
390	]
391	\| >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
392	lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (\|t\|) (le_S_to_le … Hp))
393	cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) ? 〈0,short_jump〉) in Hm;
394	#x1 #x2
395	cases (bvt_lookup ?? (bitvector_of_nat ? (\|t\|)) ? 〈0,short_jump〉); #y1 #y2
396	normalize nodelta cases x2 cases y2 normalize nodelta
397	[1,5,9: #_ #_ @refl
398	\|4,7,8: #_ #H elim H #H2 [1,3,5: cases H2 \|2,4,6: destruct (H2) ]
399	\|2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
400	lapply (measure_incr_or_equal program policy t ? 0)
401	[1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
402	\|6: >measure_plus >measure_plus
403	change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
404	#H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
405	lapply (measure_incr_or_equal program policy t ? 0)
406	[ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
407	]
408	]
409	]
410	qed.
411
412	lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.
413	S (\|l\|) < 2^16 ∧ is_well_labelled_p l.
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 ?? 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.
434	S (\|l\|) < 2^16 ∧ is_well_labelled_p l).
435	Σp:option ppc_pc_map.
436	match p with
437	[ None ⇒ True
438	\| Some pol ⇒ And (And (And
439	(\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
440	(\fst pol = \fst (bvt_lookup … (bitvector_of_nat ? (\|program\|)) (\snd pol) 〈0,short_jump〉)))
441	(sigma_compact program (pi1 … (create_label_map program)) pol))
442	(\fst pol ≤ 2^16)
443	].
444	#program @(\snd (jump_expansion_internal program (S (2*\|program\|))))
445	cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
446	(\snd (pi1 ?? (jump_expansion_internal program k)))
447	(\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*\|program\|))
448	[ #Hex cases Hex -Hex #k #Hk
449	inversion (jump_expansion_internal ??)
450	#x cases x -x #Gno_ch #Go cases Go normalize nodelta
451	[ #H #Heq / by I/
452	\| -Go #Gp #HGp #Geq
453	cut (policy_equal_opt program (\snd (jump_expansion_internal program (2*\|program\|)))
454	(\snd (jump_expansion_internal program (S (2*\|program\|)))))
455	[ @(pe_trans … (equal_remains_equal program k (proj2 ?? Hk) (S (2*\|program\|)) (le_S … (le_S_to_le … (proj1 ?? Hk)))))
456	@pe_sym @equal_remains_equal [ @(proj2 ?? Hk) \| @(le_S_to_le … (proj1 ?? Hk)) ]
457	\| >Geq lapply (refl ? (jump_expansion_internal program (2*\|program\|)))
458	cases (jump_expansion_internal program (2*\|program\|)) in ⊢ (???% → %);
459	#x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
460	[ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS)
461	\| -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq
462	@conj [ @conj [ @conj
463	[ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
464	\| @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
465	]
466	\| @(equal_compact_unsafe_compact ? Fp)
467	[ lapply (jump_pc_equal program (2*\|program\|))
468	>Feq >Geq normalize nodelta #H @H @Heq
469	\| @Heq
470	\| cases daemon (* true, but have to add this to properties *)
471	\| cases daemon
472	\| @(proj2 ?? (proj1 ?? HGp))
473	]
474	]
475	\| @(proj2 ?? HGp)
476	]
477	]
478	]
479	]
480	\| #Hnex lapply (not_exists_forall … Hnex) -Hnex #Hfa
481	lapply (refl ? (jump_expansion_internal program (2*\|program\|)))
482	cases (jump_expansion_internal program (2*\|program\|)) in ⊢ (???% → %);
483	#x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
484	[ (* None *)
485	#HF #Feq lapply (step_none program (2*\|program\|) ? 1) >Feq / by /
486	<plus_n_Sm <plus_n_O #H >H -H normalize nodelta / by I/
487	\| -Fo #Fp #HFp #Feq lapply (measure_full program Fp ?)
488	[ @le_to_le_to_eq
489	[ @measure_le
490	\| cut (∀x:ℕ.x ≤ 2*\|program\| →
491	∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
492	x ≤ measure_int program p 0))
493	[ #x elim x
494	[ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program)))
495	cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %);
496	#z cases z -z normalize nodelta
497	[ #H #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #n #Hn
498	@(absurd … (step_none program 0 ? n))
499	[ whd in match (jump_expansion_internal ??); >Heqn @refl
500	\| <Hn >Feq @nmk #H destruct (H)
501	]
502	\| #Zp #HZp #Zeq @(ex_intro ?? Zp) @conj
503	[ whd in match (jump_expansion_internal ??); >Zeq @refl
504	\| @le_O_n
505	]
506	]
507	\| -x #x #Hind #Hx
508	lapply (refl ? (jump_expansion_internal program (S x)))
509	cases (jump_expansion_internal program (S x)) in ⊢ (???% → %);
510	#z cases z -z #Sno_ch #So cases So -So
511	[ #HSp #Seq normalize nodelta @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
512	@(absurd … (step_none program (S x) ? k))
513	[ >Seq @refl
514	\| <Hk >Feq @nmk #H destruct (H)
515	]
516	\| #Sp #HSp #Seq @(ex_intro ?? Sp) @conj
517	[ @refl
518	\| elim (Hind (transitive_le … (le_n_Sn x) Hx))
519	#pol #Hpol @(le_to_lt_to_lt … (proj2 ?? Hpol))
520	lapply (proj1 ?? Hpol) -Hpol
521	lapply (refl ? (jump_expansion_internal program x))
522	cases (jump_expansion_internal program x) in ⊢ (???% → %);
523	#z cases z -z #Xno_ch #Xo cases Xo
524	[ #HXp #Xeq #abs destruct (abs)
525	\| normalize nodelta #Xp #HXp #Xeq #H <(Some_eq ??? H) -H -pol
526	lapply (Hfa x Hx) >Xeq >Seq whd in match policy_equal_opt;
527	normalize nodelta #Hpe
528	lapply (measure_incr_or_equal program Xp program (le_n (\|program\|)) 0)
529	[ @HXp
530	\| lapply (Hfa x Hx) >Xeq >Seq
531	lapply (measure_special program «Xp,?»)
532	[ @HXp
533	\| lapply Seq whd in match (jump_expansion_internal program (S x)); (340s)
534	>Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq
535	[ normalize nodelta #EQ
536	>(proj2 ?? (pair_destruct ?????? (pi1_eq ???? EQ)))
537	#_ #abs @⊥ @(absurd ?? abs) / by /
538	\| normalize nodelta cases (jump_expansion_step ???);
539	#z cases z -z #stch #sto cases sto
540	[ normalize nodelta #_ #ABS destruct (ABS)
541	\| -sto #stp normalize nodelta #Hstp #steq
542	>(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? steq))))
543	#Hms #Hneq #glerp elim (le_to_or_lt_eq … glerp)
544	[ / by /
545	\| #glorp @⊥ @(absurd ?? Hneq) @Hms @glorp
546	]
547	]
548	]
549	]
550	]
551	]
552	]
553	]
554	]
555	\| #H elim (H (2*\|program\|) (le_n ?)) #plp >Feq #Hplp
556	>(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp)
557	]
558	]
559	\| #Hfull lapply (refl ? (jump_expansion_internal program (S (2*\|program\|))))
560	cases (jump_expansion_internal program (S (2*\|program\|))) in ⊢ (???% → %);
561	#z cases z -z #Gch #Go cases Go normalize nodelta
562	[ #HGp #Geq @I
563	\| -Go #Gp normalize nodelta #HGp #Geq @conj [ @conj [ @conj
564	[ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
565	\| @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
566	]
567	\| @(equal_compact_unsafe_compact ? Fp)
568	[1,2:
569	[1: lapply (jump_pc_equal program (2*(\|program\|))) >Feq >Geq normalize nodelta
570	#H @H ]
571	#i #Hi
572	inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
573	[1,3: #Hj whd in match (jump_expansion_internal program (S (2\|program\|))) in Geq; (85s*)
574	>Feq in Geq; normalize nodelta cases Fno_ch
575	[1,3: normalize nodelta #Heq
576	>(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) %
577	\|2,4: normalize nodelta cases (jump_expansion_step ???)
578	#x cases x -x #stch #sto normalize nodelta cases sto
579	[1,3: normalize nodelta #_ #X destruct (X)
580	\|2,4: -sto #stp normalize nodelta #Hst #Heq
581	<(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq))))
582	lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi))
583	lapply (Hfull i Hi ?) [1,3: >Hj %]
584	cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
585	#fp #fj #Hfj >Hfj normalize nodelta
586	cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
587	#stp #stj cases stj normalize nodelta
588	[1,2,4,5: #H cases H #H2 cases H2 destruct (H2)
589	\|3,6: #_ @refl
590	]
591	]
592	]
593	\|2,4: #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2,4:>Hj %]
594	>(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2,4:>Hj] %
595	]
596	\| cases daemon (* true, but have to add to properties in some way *)
597	\| cases daemon
598	\| @(proj2 ?? (proj1 ?? HGp))
599	]
600	]
601	\| @(proj2 ?? HGp)
602	]
603	]
604	]
605	]
606	\| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
607	#x cases x -x #nch #npol normalize nodelta #Hnpol
608	#x cases x -x #Sch #Spol normalize nodelta #HSpol
609	cases npol in Hnpol; cases Spol in HSpol;
610	[ #Hnpol #HSpol %1 //
611	\|2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
612	#H destruct (H)
613	\|4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
614	cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
615	#x1 #x2
616	cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
617	#y1 #y2 normalize nodelta
618	@dec_eq_jump_length
619	]
620	]
621	qed.
622
623	include alias "arithmetics/nat.ma".
624	include alias "basics/logic.ma".
625
626	lemma pc_increases: ∀i,j:ℕ.∀program.∀pol:Σp:ppc_pc_map.
627	And (And (And
628	(\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)
629	(\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (\|program\|)) (\snd p) 〈0,short_jump〉)))
630	(sigma_compact program (create_label_map program) p))
631	(\fst p ≤ 2^16).i ≤ j → j ≤ \|program\| →
632	\fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 i) (\snd pol) 〈0,short_jump〉) ≤
633	\fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 j) (\snd pol) 〈0,short_jump〉).
634	#i #j #program #pol #H elim (le_to_eq_plus … H) #n #Hn >Hn -Hn -j elim n
635	[ <plus_n_O #_ @le_n
636	\| -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H)))
637	lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (i+n) H)
638	lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)))
639	cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %);
640	[ normalize nodelta #_ #abs cases abs
641	\| #x cases x -x #pc #jl #EQ normalize nodelta
642	lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)))
643	cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %);
644	[ normalize nodelta #_ #abs cases abs
645	\| #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp
646	>(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
647	>(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r
648	]
649	]
650	]
651	qed.
652
653	(* The glue between Policy and Assembly. *)
654	definition jump_expansion':
655	∀program:preamble × (Σl:list labelled_instruction.S (\|l\|) < 2^16 ∧ is_well_labelled_p l).
656	option (Σsigma_policy:(Word → Word) × (Word → bool).
657	let 〈sigma,policy〉≝ sigma_policy in
658	sigma_policy_specification 〈\fst program,\snd program〉 sigma policy)
659	≝
660	λprogram.
661	let f: option ppc_pc_map ≝ je_fixpoint (\snd program) in
662	match f return λx.f = x → ? with
663	[ None ⇒ λp.None ?
664	\| Some x ⇒ λp.Some ?
665	«〈(λppc.let pc ≝ \fst (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in
666	bitvector_of_nat 16 pc),
667	(λppc.let jl ≝ \snd (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in
668	jmpeqb jl long_jump)〉,?»
669	] (refl ? f).
670	normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta
671	lapply (pi2 ?? (je_fixpoint (\snd program))) >p normalize nodelta cases x
672	#fpc #fpol #Hfpol cases Hfpol ** #Hfpol1 #Hfpol2 #Hfpol3 #Hfpol4
673	@conj
674	[ >Hfpol1 %
675	\| #ppc #ppc_ok normalize nodelta
676	>(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) =
677	\snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment []〉))
678	[2: whd in match fetch_pseudo_instruction; normalize nodelta
679	>(nth_safe_nth … 〈None ?, Comment []〉)
680	cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
681	#lbl #ins % ]
682	lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok) >bitvector_of_nat_inverse_nat_of_bitvector
683	inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ]
684	* #pc #jl #Hl normalize nodelta
685	inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ]
686	* #Spc #Sjl #SHL lapply SHL
687	<add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
688	#SHl normalize nodelta #Hcompact
689	@conj
690	[ >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉)
691	>(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
692	>add_bitvector_of_nat_plus >Hcompact %
693	\| (* Basic proof scheme:
694	- ppc < \|snd program\|, hence our instruction is in the program
695	- either we are the last non-zero-size instruction, in which case we are
696	either smaller than 2^16 (because the entire program is), or we are exactly
697	2^16 and something weird happens
698	- or we are not, in which case we are definitely smaller than 2^16 (by transitivity
699	through the next non-zero instruction)
700	*)
701	elim (le_to_or_lt_eq … Hfpol4) #Hfpc
702	[ %1 @(le_to_lt_to_lt … Hfpc) >Hfpol2
703	>(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
704	>nat_of_bitvector_bitvector_of_nat_inverse
705	[2: lapply (pc_increases (nat_of_bitvector 16 ppc) (\|\snd program\|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
706	>bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
707	#H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @H ]
708	lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (\|\snd program\|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
709	>(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >Hcompact #X @X
710	\| (* the program is of length 2^16 and ppc is followed by only zero-size instructions
711	* until the end of the program *)
712	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 ?)))
713	[ >bitvector_of_nat_inverse_nat_of_bitvector
714	>(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc normalize nodelta
715	>nat_of_bitvector_bitvector_of_nat_inverse
716	[2: <Hfpc >Hfpol2 @Hpc ]
717	elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (\|\snd program\|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
718	<Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) #HSpc
719	[ %1 >Hcompact in HSpc; #X @X
720	\| %2 @conj
721	[2: >Hcompact in HSpc; #X @X
722	\| #ppc' #ppc_ok' #Hppc'
723	(* S ppc < ppc' < \|\snd program\| *)
724	(* lookup S ppc = 2^16 *)
725	(* lookup \|\snd program\| = 2^16 *)
726	(* lookup ppc' = 2^16 → instruction size = 0 *)
727	lapply (Hfpol3 (nat_of_bitvector ? ppc') ppc_ok')
728	>bitvector_of_nat_inverse_nat_of_bitvector
729	inversion (lookup_opt ????) normalize nodelta
730	[ #_ #abs cases abs
731	\| * #xpc #xjl #XEQ normalize nodelta
732	inversion (lookup_opt ????) normalize nodelta
733	[ #_ #abs cases abs
734	\| * #Sxpc #Sxjl #SXEQ normalize nodelta
735	#Hpcompact
736	lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
737	>(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
738	lapply (pc_increases (nat_of_bitvector ? ppc') (\|\snd program\|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
739	<Hfpol2 >Hfpc #Hle2
740	lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1
741	>bitvector_of_nat_inverse_nat_of_bitvector
742	>(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
743	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')
744	>(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
745	lapply (pc_increases (S (nat_of_bitvector ? ppc')) (\|\snd program\|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
746	<Hfpol2 >Hfpc #Hle2
747	lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2
748	>(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc
749	>Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H
750	@(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
751	normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)
752	cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;
753	#lbl #ins normalize nodelta #X @sym_eq @X
754	]
755	]
756	]
757	]
758	\| >bitvector_of_nat_inverse_nat_of_bitvector
759	<Hfpol2 >Hfpc >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc
760	%1 >Hpc
761	>bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?));
762	<plus_O_n whd in match instruction_size; normalize nodelta
763	inversion (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?)
764	#len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
765	#Hli >Hli
766	lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?)
767	[5: >Hass / by / ]
768	]
769	]
770	]
771	]
772	qed.

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

Download in other formats:

Original Format