Context Navigation

ASMCosts.ma @ 2475

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

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

Download in other formats:

Original Format