Context Navigation

ASMCosts.ma @ 3003

Last change on this file since 3003 was 2999, checked in by sacerdot, 8 years ago
code_memory added to labelled_object_code to avoid recomputing it every time. This gives a major speed up in the semantics of the extracted code.
File size: 36.3 KB

Line
1	include "ASM/Interpret.ma".
2
3	definition ASMRegisterRets: list [[ acc_a; direct; registr ]] ≝
4	[ DIRECT (bitvector_of_nat 8 82); (* DPL *)
5	DIRECT (bitvector_of_nat 8 83); (* DPH *)
6	REGISTER [[ false; false; false ]]; (* Register00 *)
7	REGISTER [[ false; false; true ]] ]. (* Register01 *)
8	% qed.
9
10	definition as_result_of_finaladdr: ∀T:Type[0]. ∀cm:T. PreStatus … cm → Word → option int ≝
11	λT,cm,st,finaladdr.
12	if eq_bv ? (program_counter ?? st) finaladdr then
13	let vals ≝
14	map [[acc_a;direct;registr]] ? (get_arg_8 ?? st false) (ASMRegisterRets⌈list ? ↦ ?⌉) in
15	let dummy ≝ zero ? in
16	let first_byte ≝ λl. match l with [ nil ⇒ 〈dummy,[]〉 \| cons hd tl ⇒ 〈hd,tl〉] in
17	let 〈b1,tl1〉 ≝ first_byte vals in
18	let 〈b2,tl2〉 ≝ first_byte tl1 in
19	let 〈b3,tl3〉 ≝ first_byte tl2 in
20	let 〈b4,tl4〉 ≝ first_byte tl3 in
21	Some ? (b4 @@ b3 @@ b2 @@ b1)
22	else
23	None ?.
24	[ @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % \| % ]
25	qed.
26
27	definition OC_as_call_ident:
28	∀prog:labelled_object_code.∀cm. (Σs:Status cm. OC_classify … s = cl_call) → ident
29	≝
30	λprog,cm,s0.
31	let pc ≝ program_counter ?? (execute_1' cm s0) in
32	match lookup_opt ?? pc (symboltable prog) with
33	[ None ⇒ ⊥ \| Some id ⇒ id ].
34	cases daemon (CSC: we need a specification of the symboltable for this )
35	qed.
36
37	definition OC_abstract_status: labelled_object_code → abstract_status ≝
38	λprog.
39	mk_abstract_status
40	(Status (cm prog))
41	(λs1,s2. execute_1 … s1 = s2)
42	word_deqset
43	(program_counter …)
44	(OC_classify …)
45	(λpc.lookup_opt … pc (costlabels prog))
46	(next_instruction_properly_relates_program_counters …)
47	(λst. as_result_of_finaladdr … st (final_pc prog))
48	(OC_as_call_ident prog …)
49	?.
50	* #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
51	try (#x #y #abs) try (#x #abs) try #abs destruct
52	qed.
53
54	definition trace_any_label_length ≝
55	λprog: labelled_object_code.
56	λtrace_ends_flag: trace_ends_with_ret.
57	λstart_status: Status (cm prog).
58	λfinal_status: Status (cm prog).
59	λthe_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
60	as_trace_any_label_length' … the_trace.
61
62	let rec all_program_counter_list
63	(n: nat)
64	on n ≝
65	match n with
66	[ O ⇒ [ ]
67	\| S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n')
68	].
69
70	lemma all_program_counter_list_bound_eq:
71	∀bound: nat.
72	\|all_program_counter_list bound\| = bound.
73	#bound elim bound try %
74	#bound' #inductive_hypothesis normalize
75	>inductive_hypothesis %
76	qed.
77
78	lemma mem_all_program_counter_list_lt_bound:
79	∀bound: nat.
80	∀bound_proof: bound ≤ 2^16.
81	∀e: Word.
82	memb word_deqset e (all_program_counter_list bound) = true →
83	nat_of_bitvector … e < bound.
84	#bound elim bound
85	[1:
86	#bound_proof #e
87	normalize #absurd destruct(absurd)
88	\|2:
89	#bound' #inductive_hypothesis
90	#bound_proof #e
91	change with (if eq_bv ??? then ? else ? = ? → ?)
92	@eq_bv_elim
93	[1:
94	#eq_assm
95	normalize nodelta destruct #_
96	>nat_of_bitvector_bitvector_of_nat_inverse try assumption
97	normalize %
98	\|2:
99	#neq_assm normalize nodelta
100	#memb_assm %2 @inductive_hypothesis
101	try assumption
102	@(transitive_le bound' (S bound'))
103	try assumption %2 %
104	]
105	]
106	qed.
107
108	lemma lt_bound_mem_all_program_counter_list:
109	∀bound: nat.
110	∀bound_proof: bound ≤ 2^16.
111	∀e: Word.
112	nat_of_bitvector … e < bound →
113	memb word_deqset e (all_program_counter_list bound) = true.
114	#bound elim bound
115	[1:
116	#bound_proof #e normalize
117	#absurd cases (lt_to_not_zero … absurd)
118	\|2:
119	#bound' #inductive_hypothesis
120	#bound_proof #e
121	change with (? → if eq_bv ??? then ? else ? = ?)
122	#assm
123	cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?)
124	[1:
125	#e_lt_assm
126	@eq_bv_elim
127	[1:
128	#eq_assm normalize nodelta %
129	\|2:
130	#neq_assm normalize nodelta
131	@inductive_hypothesis try assumption
132	@(transitive_le bound' (S bound')) try assumption
133	%2 %
134	]
135	\|2:
136	#relevant >eq_eq_bv normalize nodelta try %
137	destruct >bitvector_of_nat_inverse_nat_of_bitvector %
138	\|3:
139	normalize in assm;
140	@le_S_S_to_le assumption
141	]
142	]
143	qed.
144
145	include alias "arithmetics/nat.ma".
146
147	lemma execute_1_and_program_counter_after_other_in_lockstep00:
148	∀code_memory: BitVectorTrie Byte 16.
149	∀start_status: Status code_memory.
150	let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
151	ASM_classify0 instruction = cl_other →
152	program_counter ? ? (execute_1 … start_status) =
153	program_counter_after_other pc instruction.
154	#code_memory #start_status
155	whd in match execute_1; normalize nodelta
156	cases (execute_1' code_memory start_status) #the_status; * #_
157	cases (fetch ? ?); * #instruction #pc #ticks
158	#classify_assm #classify_assm0 @classify_assm assumption
159	qed.
160
161	lemma execute_1_and_program_counter_after_other_in_lockstep0:
162	∀code_memory: BitVectorTrie Byte 16.
163	∀start_status: Status code_memory.
164	OC_classify … start_status = cl_other →
165	let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
166	program_counter ? ? (execute_1 … start_status) =
167	program_counter_after_other pc instruction.
168	#code_memory #start_status #classify_assm
169	whd in match execute_1; normalize nodelta
170	cases (execute_1' code_memory start_status) #the_status
171	* #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
172	cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
173	#classify_assm #classify_assm' @classify_assm' assumption
174	qed.
175
176	lemma execute_1_and_program_counter_after_other_in_lockstep:
177	∀prog: labelled_object_code.
178	∀start_status: Status (cm prog).
179	as_classifier (OC_abstract_status prog) start_status cl_other →
180	let 〈instruction, pc, ticks〉 ≝ fetch (cm prog) (program_counter … start_status) in
181	program_counter ? ? (execute_1 … start_status) =
182	program_counter_after_other pc instruction.
183	#prog #start_status #classify_assm
184	change with (ASM_classify0 ? = ?) in classify_assm;
185	destruct (classify_assm)
186	@execute_1_and_program_counter_after_other_in_lockstep0 assumption.
187	qed.
188
189	lemma sublist_tal_pc_list_all_program_counter_list:
190	∀prog: labelled_object_code.
191	∀start, final: Status (cm prog).
192	∀trace_ends_flag.
193	∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
194	sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
195	#prog #start #final #trace_ends_flag #the_trace
196	whd in match (sublist ???); #pc #memb_assm
197	@lt_bound_mem_all_program_counter_list try %
198	@nat_of_bitvector_lt_bound
199	qed.
200
201	corollary tal_pc_list_length_leq_total_program_size:
202	∀prog: labelled_object_code.
203	∀start, final: Status (cm prog).
204	∀trace_ends_flag.
205	∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
206	∀unrepeating_witness: tal_unrepeating … the_trace.
207	\|tal_pc_list … the_trace\| ≤ 2^16.
208	#prog #start #final #trace_ends_flag #the_trace #unrepeating_witness
209	<(all_program_counter_list_bound_eq (2^16))
210	@sublist_length
211	[1:
212	@tal_unrepeating_uniqueb
213	assumption
214	\|2:
215	@sublist_tal_pc_list_all_program_counter_list
216	assumption
217	]
218	qed.
219
220	let rec compute_paid_trace_any_label
221	(prog: labelled_object_code) (trace_ends_flag: trace_ends_with_ret)
222	(start_status: Status (cm prog))
223	(final_status: Status (cm prog))
224	(the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
225	on the_trace: nat ≝
226	match the_trace with
227	[ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
228	\| tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
229	\| tal_base_call pre_fun_call start_fun_call final _ _ _ _ _ ⇒ current_instruction_cost … pre_fun_call
230	\| tal_base_tailcall pre_fun_call start_fun_call final _ _ _ ⇒ current_instruction_cost … pre_fun_call
231	\| tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
232	_ _ _ call_trace _ final_trace ⇒
233	let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
234	let final_trace_cost ≝ compute_paid_trace_any_label prog end_flag … final_trace in
235	current_instruction_cost + final_trace_cost
236	\| tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
237	let current_instruction_cost ≝ current_instruction_cost … status_pre in
238	let tail_trace_cost ≝
239	compute_paid_trace_any_label prog end_flag
240	status_init status_end tail_trace
241	in
242	current_instruction_cost + tail_trace_cost
243	].
244
245	definition compute_paid_trace_label_label ≝
246	λprog: labelled_object_code.
247	λtrace_ends_flag: trace_ends_with_ret.
248	λstart_status: Status (cm prog).
249	λfinal_status: Status (cm prog).
250	λthe_trace: (trace_label_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
251	match the_trace with
252	[ tll_base ends_flag initial final given_trace labelled_proof ⇒
253	compute_paid_trace_any_label … given_trace
254	].
255
256	lemma trace_compute_paid_trace_cl_other:
257	∀prog : labelled_object_code.
258	∀program_counter' : Word.
259	∀program_size' : ℕ.
260	∀ticks : ℕ.
261	∀instruction : instruction.
262	∀program_counter'' : Word.
263	∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
264	let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
265	∀start_status : (Status (cm prog)).
266	∀final_status : (Status (cm prog)).
267	∀trace_ends_flag : trace_ends_with_ret.
268	∀the_trace : (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
269	∀program_counter_refl : (program_counter' = program_counter … start_status).
270	∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
271	∀classify_assm: ASM_classify0 instruction = cl_other.
272	∀pi1 : ℕ.
273	(if match lookup_opt costlabel 16 program_counter''' (costlabels prog) with
274	[None ⇒ true
275	\|Some _ ⇒ false
276	]
277	then
278	∀start_status0:Status (cm prog).
279	∀final_status0:Status (cm prog).
280	∀trace_ends_flag0:trace_ends_with_ret.
281	∀the_trace0:trace_any_label (OC_abstract_status prog) trace_ends_flag0 start_status0 final_status0.
282	trace_any_label_length … the_trace0 ≤ program_size' →
283	program_counter''' = program_counter … start_status0 →
284	pi1
285	=compute_paid_trace_any_label … the_trace0
286	else (pi1=O) )
287	→ ticks+pi1
288	=compute_paid_trace_any_label … the_trace.
289	#prog #program_counter' #program_size' #ticks #instruction
290	#program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace
291	#program_counter_refl #size_invariant #classify_assm #recursive_block_cost
292	#recursive_assm
293	@(trace_any_label_inv_ind … the_trace)
294	[2:
295	#start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
296	#start_status_refl #final_status_refl #the_trace_assm destruct @⊥
297	\|3:
298	#status_pre_fun_call #status_start_fun_call #status_final #execute_assm
299	#classifier_assm #after_return_assm #trace_label_return #costed_assm
300	#ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
301	destruct @⊥
302	\|4:
303	#status_pre_fun_call #status_start_fun_call #status_final #execute_assm
304	#classifier_assm #trace_label_return
305	#ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
306	destruct @⊥
307	\|5:
308	#end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
309	#status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
310	#costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
311	#final_status_refl #the_trace_refl destruct @⊥
312	\|6:
313	#end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
314	#classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
315	#the_trace_refl
316	destruct
317	whd in match (trace_any_label_length … (tal_step_default …));
318	whd in match (compute_paid_trace_any_label … (tal_step_default …));
319	whd in costed_assm:(?%);
320	generalize in match costed_assm;
321	generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog)));
322	whd in match (as_label ??);
323	generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog))
324	in ⊢ (??%? → % → ?);
325	#lookup_assm cases lookup_assm
326	[1:
327	#None_lookup_opt_assm normalize nodelta #_
328	generalize in match recursive_assm;
329	lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
330	<FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
331	#None_lookup_opt_assm <None_lookup_opt_assm
332	normalize nodelta #new_recursive_assm
333	cases(new_recursive_assm (execute_1 ? status_pre) status_end
334	end_flag trace_any_label ? ?) try (>rewrite_assm %)
335	whd in match (current_instruction_cost … status_pre);
336	cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre)))
337	[1,3:
338	<FETCH %
339	\|2:
340	#ticks_refl_assm
341	>ticks_refl_assm %
342	\|4:
343	#ticks_refl_assm
344	change with (S ? ≤ S ?) in size_invariant;
345	lapply (le_S_S_to_le … size_invariant) #assm
346	assumption
347	]
348	\|2:
349	#costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm
350	#absurd
351	cases (not_Some_neq_None_to_False ?? absurd)
352	]
353	\|1:
354	#status_start #status_final #execute_assm #classifier_assm #costed_assm
355	#trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
356	destruct
357	whd in match (trace_any_label_length … (tal_base_not_return …));
358	whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
359	whd in costed_assm;
360	generalize in match costed_assm;
361	generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) ?));
362	whd in match (as_label ??);
363	generalize in match (lookup_opt … (program_counter … (execute_1 … status_start)) (costlabels prog))
364	in ⊢ (??%? → % → ?);
365	#lookup_assm cases lookup_assm
366	[1:
367	#None_lookup_opt_assm
368	#absurd @⊥ cases absurd -absurd #absurd @absurd %
369	\|2:
370	#costlabel #Some_lookup_opt_assm normalize nodelta #ignore
371	generalize in match recursive_assm;
372	cases classifier_assm -classifier_assm #classifier_assm
373	[2:
374	lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
375	<FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
376	#Some_lookup_opt_assm <Some_lookup_opt_assm
377	normalize nodelta #new_recursive_assm >new_recursive_assm
378	cut(ticks = \snd (fetch (cm prog) (program_counter … status_start)))
379	[1:
380	<FETCH %
381	\|2:
382	#ticks_refl_assm >ticks_refl_assm
383	<plus_n_O %
384	]
385	\|1:
386	(* JHM: wicked failure because Some prevent previous unfolding of OC_classify here *)
387	@⊥
388	(* *** (* previously: unnecessary case analysis on instruction *)
389	change with ((Some ? (ASM_classify0 ?) = ?) → ?);
390	whd in match (current_instruction code_memory' status_start);
391	<FETCH generalize in match classify_assm;
392	cases instruction
393	[8:
394	#preinstruction normalize nodelta
395	whd in match ASM_classify0; normalize nodelta
396	#contradiction >contradiction #absurd destruct(absurd)
397	]
398	try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
399	try(#addr normalize nodelta #ignore #absurd destruct(absurd))
400	normalize in ignore; destruct(ignore)
401	*** *)
402	]
403	]
404	]
405	change with (ASM_classify0 ? = ?) in classifier_assm;
406	whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
407	whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
408	<FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
409	qed.
410
411	lemma trace_compute_paid_trace_cl_jump:
412	∀prog: labelled_object_code.
413	∀program_counter': Word.
414	∀first_time_around: bool.
415	∀program_size': ℕ.
416	∀ticks: ℕ.
417	∀instruction: instruction.
418	∀program_counter'': Word.
419	∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch (cm prog) program_counter'.
420	∀start_status: (Status (cm prog)).
421	∀final_status: (Status (cm prog)).
422	∀trace_ends_flag: trace_ends_with_ret.
423	∀the_trace: (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
424	∀program_counter_refl: (program_counter' = program_counter … start_status).
425	∀classify_assm: ASM_classify0 instruction = cl_jump.
426	ticks
427	=compute_paid_trace_any_label … the_trace.
428	#prog #program_counter' #first_time_around
429	#program_size' #ticks #instruction #program_counter'' #FETCH
430	#start_status #final_status
431	#trace_ends_flag #the_trace #program_counter_refl #classify_assm
432	@(trace_any_label_inv_ind … the_trace)
433	[6:
434	#end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
435	#classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
436	#the_trace_refl destruct @⊥
437	\|1:
438	#status_start #status_final #execute_assm #classifier_assm #costed_assm
439	#trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
440	destruct
441	whd in match (trace_any_label_length … (tal_base_not_return …));
442	whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
443	<FETCH %
444	\|2:
445	#start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
446	#start_status_refl #final_status_refl #the_trace_assm destruct @⊥
447	\|3:
448	#status_pre_fun_call #status_start_fun_call #status_final #execute_assm
449	#classifier_assm #after_return_assm #trace_label_return #costed_assm
450	#ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
451	destruct @⊥
452	\|4:
453	#status_pre_fun_call #status_start_fun_call #status_final #execute_assm
454	#classifier_assm #trace_label_return
455	#ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
456	destruct @⊥
457	\|5:
458	#end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
459	#status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
460	#costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
461	#final_status_refl #the_trace_refl destruct @⊥
462	]
463	change with (ASM_classify0 ? = ?) in classifier_assm;
464	whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
465	whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
466	<FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
467	qed.
468
469	lemma trace_compute_paid_trace_cl_call:
470	∀prog: labelled_object_code.
471	∀program_counter' : Word.
472	∀program_size' : ℕ.
473	∀ticks : ℕ.
474	∀instruction : instruction.
475	∀program_counter'' : Word.
476	∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
477	∀start_status : (Status (cm prog)).
478	∀final_status : (Status (cm prog)).
479	∀trace_ends_flag : trace_ends_with_ret.
480	∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
481	∀program_counter_refl : (program_counter' = program_counter … start_status).
482	∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
483	∀classify_assm: ASM_classify0 instruction = cl_call.
484	(∀pi1:ℕ
485	.if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with
486	[None ⇒ true \| Some _ ⇒ false]
487	then (∀start_status0:Status (cm prog)
488	.∀final_status0:Status (cm prog)
489	.∀trace_ends_flag0:trace_ends_with_ret
490	.∀the_trace0:trace_any_label
491	(OC_abstract_status prog)
492	trace_ends_flag0 start_status0 final_status0.
493	trace_any_label_length … the_trace0
494	≤ program_size' →
495	program_counter''
496	=program_counter … start_status0
497	→ pi1
498	=compute_paid_trace_any_label … the_trace0)
499	else (pi1=O)
500	→ ticks+pi1
501	=compute_paid_trace_any_label … the_trace).
502	#prog #program_counter' #program_size'
503	#ticks #instruction #program_counter'' #FETCH
504	#start_status #final_status #trace_ends_flag
505	#the_trace #program_counter_refl #size_invariant #classify_assm
506	#recursive_block_cost #recursive_assm
507	@(trace_any_label_inv_ind … the_trace)
508	[6:
509	#end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
510	#classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
511	#the_trace_refl destruct @⊥
512	\|1:
513	#status_start #status_final #execute_assm #classifier_assm #costed_assm
514	#trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
515	destruct @⊥
516	\|2:
517	#start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
518	#start_status_refl #final_status_refl #the_trace_assm destruct @⊥
519	\|3:
520	#status_pre_fun_call #status_start_fun_call #status_final #execute_assm
521	#classifier_assm #after_return_assm #trace_label_return #costed_assm
522	#ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
523	destruct
524	whd in match (trace_any_label_length … (tal_base_call …));
525	whd in match (compute_paid_trace_any_label … (tal_base_call …));
526	whd in costed_assm;
527	generalize in match costed_assm;
528	generalize in match (refl … (lookup_opt … (program_counter … status_final) (costlabels prog)));
529	whd in match (as_label ??);
530	generalize in match (lookup_opt … (program_counter … status_final) ?)
531	in ⊢ (??%? → % → ?);
532	#lookup_assm cases lookup_assm
533	[1:
534	#None_lookup_opt normalize nodelta #absurd cases absurd
535	-absurd #absurd @⊥ @absurd %
536	\|2:
537	#costlabel #Some_lookup_opt normalize nodelta #ignore
538	generalize in match recursive_assm;
539	cut(program_counter'' = (program_counter … status_final))
540	[1:
541	generalize in match after_return_assm;
542	whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
543	\|2:
544	#program_counter_assm >program_counter_assm <Some_lookup_opt
545	normalize nodelta #new_recursive_assm >new_recursive_assm
546	cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre_fun_call)))
547	[1:
548	<FETCH %
549	\|2:
550	#ticks_refl_assm >ticks_refl_assm
551	<plus_n_O %
552	]
553	]
554	]
555	\|4:
556	#status_pre_fun_call #status_start_fun_call #status_final #execute_assm
557	#classifier_assm #trace_label_return
558	#ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
559	destruct @⊥
560	\|5:
561	#end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
562	#status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
563	#costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
564	#final_status_refl #the_trace_refl
565	generalize in match execute_assm; destruct #execute_assm
566	whd in match (trace_any_label_length … (tal_step_call …));
567	whd in match (compute_paid_trace_any_label … (tal_step_call …));
568	whd in costed_assm:(?%);
569	generalize in match costed_assm;
570	generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) (costlabels ?)));
571	whd in match (as_label ??);
572	generalize in match (lookup_opt … (program_counter … status_after_fun_call) (costlabels prog))
573	in ⊢ (??%? → % → ?);
574	#lookup_assm cases lookup_assm
575	[1:
576	#None_lookup_opt_assm normalize nodelta #ignore
577	generalize in match recursive_assm;
578	cut(program_counter'' = program_counter … status_after_fun_call)
579	[1:
580	generalize in match after_return_assm;
581	whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
582	\|2:
583	#program_counter_refl >program_counter_refl <None_lookup_opt_assm
584	normalize nodelta #new_recursive_assm
585	cases (new_recursive_assm … trace_any_label ? ?)
586	[1:
587	@plus_right_monotone whd in ⊢ (???%); <FETCH %
588	\|2:
589	@le_S_S_to_le @size_invariant
590	\|3:
591	%
592	]
593	]
594	\|2:
595	#cost_label #Some_lookup_opt_assm #absurd
596	cases (not_Some_neq_None_to_False ?? absurd)
597	]
598	]
599	try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
600	try (change with (ASM_classify0 ? = ?) in classifier_assm;)
601	whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
602	whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
603	<FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
604	#absurd destruct(absurd)
605	qed.
606
607	lemma trace_compute_paid_trace_cl_return:
608	∀prog: labelled_object_code.
609	∀program_counter' : Word.
610	∀program_size' : ℕ.
611	∀ticks : ℕ.
612	∀instruction : instruction.
613	∀program_counter'' : Word.
614	∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
615	∀start_status : (Status (cm prog)).
616	∀final_status : (Status (cm prog)).
617	∀trace_ends_flag : trace_ends_with_ret.
618	∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
619	∀program_counter_refl : (program_counter' = program_counter … start_status).
620	∀classify_assm: ASM_classify0 instruction = cl_return.
621	ticks
622	=compute_paid_trace_any_label … the_trace.
623	#prog #program_counter' #program_size'
624	#ticks #instruction #program_counter'' #FETCH
625	#start_status #final_status #trace_ends_flag
626	#the_trace #program_counter_refl #classify_assm
627	@(trace_any_label_inv_ind … the_trace)
628	[1:
629	#start_status' #final_status' #execute_assm #classifier_assm #costed_assm
630	#trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
631	destruct @⊥
632	\|2:
633	#start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
634	#start_status_refl #final_status_refl #the_trace_refl destruct
635	whd in match (trace_any_label_length … (tal_base_return …));
636	whd in match (compute_paid_trace_any_label … (tal_base_return …));
637	<FETCH %
638	\|3:
639	#status_pre_fun_call #status_start_fun_call #status_final #execute_assm
640	#classifier_assm #after_return_assm #trace_label_return #costed_assm
641	#trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
642	destruct @⊥
643	\|4:
644	#status_pre_fun_call #status_start_fun_call #status_final #execute_assm
645	#classifier_assm
646	destruct @⊥
647	change with (ASM_classify0 ? = ?) in classifier_assm;
648	cases (current_instruction ??) in classifier_assm;
649	[7: #preinstruction cases preinstruction ]
650	try(#addr1 #addr2 #absurd normalize in absurd; destruct(absurd))
651	try(#addr #absurd normalize in absurd; destruct(absurd))
652	#absurd normalize in absurd; destruct(absurd)
653	\|5:
654	#end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
655	#status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
656	#costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
657	#final_status_refl #the_trace_refl
658	destruct @⊥
659	\|6:
660	#end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
661	#classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
662	#final_status_refl #the_trace_refl destruct @⊥
663	]
664	try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
665	try (change with (ASM_classify0 ? = ?) in classifier_assm;)
666	whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
667	whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
668	<FETCH in classifier_assm; >classify_assm
669	#absurd try (destruct(absurd))
670	cases absurd
671	#absurd destruct(absurd)
672	qed.
673
674	lemma trace_any_label_length_leq_0_to_False:
675	∀prog: labelled_object_code.
676	∀trace_ends_flag: trace_ends_with_ret.
677	∀start_status: Status (cm prog).
678	∀final_status: Status (cm prog).
679	∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
680	trace_any_label_length … the_trace ≤ 0 → False.
681	#prog #trace_ends_flag #start_status #final_status #the_trace
682	cases the_trace /2 by absurd/
683	qed.
684
685	let rec block_cost'
686	(prog: labelled_object_code) (program_counter': Word)
687	(program_size: nat)
688	(first_time_around: bool)
689	on program_size:
690	Σcost_of_block: nat.
691	if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true \| _ ⇒ first_time_around ]) then
692	∀start_status,final_status: Status (cm prog).
693	∀trace_ends_flag.
694	∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
695	trace_any_label_length … the_trace ≤ program_size →
696	program_counter' = program_counter … start_status →
697	cost_of_block = compute_paid_trace_any_label … the_trace
698	else
699	(cost_of_block = 0) ≝
700	match program_size return λx. x = program_size → ? with
701	[ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
702	\| S program_size' ⇒ λstep_case.
703	let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (cm prog) program_counter' in
704	let to_continue ≝
705	match lookup_opt … program_counter' (costlabels prog) with
706	[ None ⇒ true
707	\| Some _ ⇒ first_time_around
708	]
709	in
710	((if to_continue then
711	pi1 … (match instruction return λx. x = instruction → ? with
712	[ RealInstruction real_instruction ⇒ λreal_instruction_refl.
713	match real_instruction return λx. x = real_instruction →
714	Σcost_of_block: nat.
715	∀start_status,final_status: Status (cm prog).
716	∀trace_ends_flag.
717	∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
718	trace_any_label_length … the_trace ≤ S program_size' →
719	program_counter' = program_counter … start_status →
720	cost_of_block = compute_paid_trace_any_label … the_trace with
721	[ RET ⇒ λinstr. ticks
722	\| RETI ⇒ λinstr. ticks
723	\| JC relative ⇒ λinstr. ticks
724	\| JNC relative ⇒ λinstr. ticks
725	\| JB bit_addr relative ⇒ λinstr. ticks
726	\| JNB bit_addr relative ⇒ λinstr. ticks
727	\| JBC bit_addr relative ⇒ λinstr. ticks
728	\| JZ relative ⇒ λinstr. ticks
729	\| JNZ relative ⇒ λinstr. ticks
730	\| CJNE src_trgt relative ⇒ λinstr. ticks
731	\| DJNZ src_trgt relative ⇒ λinstr. ticks
732	\| JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
733	ticks + block_cost' prog program_counter'' program_size' false
734	\| _ ⇒ λinstr.
735	ticks + block_cost' prog program_counter'' program_size' false
736	] (refl …)
737	\| ACALL addr ⇒ λinstr.
738	ticks + block_cost' prog program_counter'' program_size' false
739	\| AJMP addr ⇒ λinstr.
740	let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
741	ticks + block_cost' prog jump_target program_size' false
742	\| LCALL addr ⇒ λinstr.
743	ticks + block_cost' prog program_counter'' program_size' false
744	\| LJMP addr ⇒ λinstr.
745	let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
746	ticks + block_cost' prog jump_target program_size' false
747	\| SJMP addr ⇒ λinstr.
748	let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
749	ticks + block_cost' prog jump_target program_size' false
750	\| MOVC src trgt ⇒ λinstr.
751	ticks + block_cost' prog program_counter'' program_size' false
752	] (refl …))
753	else
754	0)
755	: Σcost_of_block: nat.
756	match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true \| _ ⇒ first_time_around ]) with
757	[ true ⇒
758	∀start_status: Status (cm prog).
759	∀final_status: Status (cm prog).
760	∀trace_ends_flag.
761	∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
762	trace_any_label_length … the_trace ≤ S program_size' →
763	program_counter' = program_counter … start_status →
764	cost_of_block = compute_paid_trace_any_label … the_trace
765	\| false ⇒
766	(cost_of_block = 0)
767	])
768	] (refl …).
769	[2:
770	change with (if to_continue then ? else (? = 0))
771	>p in ⊢ (match % return ? with [ _ ⇒ ? \| _ ⇒ ? ]); normalize nodelta
772	@pi2
773	\|1:
774	destruct
775	cases (lookup_opt ????) normalize nodelta
776	[1:
777	#start_status #final_status #trace_ends_flag #the_trace
778	#absurd
779	cases (trace_any_label_length_leq_0_to_False … absurd)
780	\|2:
781	#cost cases first_time_around normalize nodelta try %
782	#start_status #final_status #trace_ends_flag #the_trace #absurd
783	cases (trace_any_label_length_leq_0_to_False … absurd)
784	]
785	\|3:
786	change with (if to_continue then ? else (0 = 0))
787	>p normalize nodelta %
788	\|6,7:
789	#start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
790	@(trace_compute_paid_trace_cl_return … program_size' … FETCH … the_trace program_counter_refl)
791	destruct %
792	\|4,46,47:
793	#start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
794	cases(block_cost' ???) -block_cost'
795	@(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant)
796	destruct %
797	\|43,44,45: (* XXX: unconditional jumps *)
798	#start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
799	cases (block_cost' ???) -block_cost'
800	lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)
801	whd in match (program_counter_after_other ??); normalize nodelta destruct
802	whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
803	\|25,26,27,28,29,30,31,32,33:
804	#start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
805	@(trace_compute_paid_trace_cl_jump prog … first_time_around program_size' … FETCH … the_trace program_counter_refl)
806	destruct %
807	\|4,33:
808	\|*:
809	#start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
810	cases(block_cost' ???) -block_cost'
811	lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)
812	destruct #assm @assm %
813	]
814	qed.
815
816	definition block_cost:
817	∀prog: labelled_object_code.
818	∀program_counter': Word.
819	Σcost_of_block: nat.
820	∀start_status: Status (cm prog).
821	∀final_status: Status (cm prog).
822	∀trace_ends_flag.
823	∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
824	∀unrepeating_witness: tal_unrepeating … the_trace.
825	program_counter' = program_counter … start_status →
826	cost_of_block = compute_paid_trace_any_label … the_trace.
827	#prog #program_counter
828	cases(block_cost' prog program_counter (2^16) true)
829	#cost_of_block #block_cost_hyp
830	%{cost_of_block}
831	cases(lookup_opt … (costlabels prog)) in block_cost_hyp;
832	[2: #cost_label] normalize nodelta
833	#hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness
834	@hyp @tal_pc_list_length_leq_total_program_size try assumption
835	qed.

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

Download in other formats:

Original Format