Context Navigation

ASMCosts.ma @ 2226

Last change on this file since 2226 was 1964, checked in by tranquil, 9 years ago
introduced as_label_of_cost and adapted accordingly. Equality of cost mapping sums
File size: 35.4 KB

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

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

Download in other formats:

Original Format