Context Navigation

ASMCosts.ma @ 1625

Last change on this file since 1625 was 1625, checked in by mulligan, 9 years ago
before christmas
File size: 24.5 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 current_instruction0 ≝
8	λmem,pc. \fst (\fst (fetch … mem pc)).
9
10	definition current_instruction ≝
11	λs:Status. current_instruction0 (code_memory … s) (program_counter … s).
12
13	definition ASM_classify0: instruction → status_class ≝
14	λi.
15	match i with
16	[ RealInstruction pre ⇒
17	match pre with
18	[ RET ⇒ cl_return
19	\| JZ _ ⇒ cl_jump
20	\| JNZ _ ⇒ cl_jump
21	\| JC _ ⇒ cl_jump
22	\| JNC _ ⇒ cl_jump
23	\| JB _ _ ⇒ cl_jump
24	\| JNB _ _ ⇒ cl_jump
25	\| JBC _ _ ⇒ cl_jump
26	\| CJNE _ _ ⇒ cl_jump
27	\| DJNZ _ _ ⇒ cl_jump
28	\| _ ⇒ cl_other
29	]
30	\| ACALL _ ⇒ cl_call
31	\| LCALL _ ⇒ cl_call
32	\| JMP _ ⇒ cl_call
33	\| AJMP _ ⇒ cl_jump
34	\| LJMP _ ⇒ cl_jump
35	\| SJMP _ ⇒ cl_jump
36	\| _ ⇒ cl_other
37	].
38
39	definition ASM_classify: Status → status_class ≝
40	λs.ASM_classify0 (current_instruction s).
41
42	definition current_instruction_is_labelled ≝
43	λcost_labels: BitVectorTrie costlabel 16.
44	λs: Status.
45	let pc ≝ program_counter … s in
46	match lookup_opt … pc cost_labels with
47	[ None ⇒ False
48	\| _ ⇒ True
49	].
50
51	definition label_of_current_instruction:
52	BitVectorTrie costlabel 16 → Status → list costlabel
53	≝
54	λcost_labels,s.
55	let pc ≝ program_counter … s in
56	match lookup_opt … pc cost_labels with
57	[ None ⇒ []
58	\| Some l ⇒ [l]
59	].
60
61	definition next_instruction_properly_relates_program_counters ≝
62	λbefore: Status.
63	λafter : Status.
64	let size ≝ current_instruction_cost before in
65	let pc_before ≝ program_counter … before in
66	let pc_after ≝ program_counter … after in
67	let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
68	sum = pc_after.
69
70	definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
71	λcost_labels.
72	mk_abstract_status
73	Status
74	(λs,s'. (execute_1 s) = s')
75	(λs,class. ASM_classify s = class)
76	(current_instruction_is_labelled cost_labels)
77	next_instruction_properly_relates_program_counters.
78
79	(* To be moved in ASM/arithmetic.ma *)
80	definition addr16_of_addr11: Word → Word11 → Word ≝
81	λpc: Word.
82	λa: Word11.
83	let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
84	let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
85	let 〈b123, b〉 ≝ split … 3 8 a in
86	let b1 ≝ get_index_v … b123 0 ? in
87	let b2 ≝ get_index_v … b123 1 ? in
88	let b3 ≝ get_index_v … b123 2 ? in
89	let p5 ≝ get_index_v … n2 0 ? in
90	(n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
91	//
92	qed.
93
94	definition good_program_counter: BitVectorTrie Byte 16 → Word → nat → Prop ≝
95	λcode_memory: BitVectorTrie Byte 16.
96	λprogram_counter: Word.
97	λprogram_size: nat.
98	∃n: nat.
99	let tail_program_counter ≝ fetch_program_counter_n n code_memory (zero 16) in
100	program_counter = fetch_program_counter_n (S n) code_memory (zero 16) ∧
101	nat_of_bitvector 16 program_counter ≤ program_size ∧
102	nat_of_bitvector 16 tail_program_counter < nat_of_bitvector 16 program_counter.
103
104	definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝
105	λcode_memory: BitVectorTrie Byte 16.
106	λprogram_counter: Word.
107	λtotal_program_size: nat.
108	let 〈instruction, program_counter, ticks〉 ≝ fetch code_memory program_counter in
109	match instruction with
110	[ RealInstruction instr ⇒
111	match instr with
112	[ RET ⇒ True
113	\| JC relative ⇒ True (* XXX: see below *)
114	\| JNC relative ⇒ True (* XXX: see below *)
115	\| JB bit_addr relative ⇒ True
116	\| JNB bit_addr relative ⇒ True
117	\| JBC bit_addr relative ⇒ True
118	\| JZ relative ⇒ True
119	\| JNZ relative ⇒ True
120	\| CJNE src_trgt relative ⇒ True
121	\| DJNZ src_trgt relative ⇒ True
122	\| _ ⇒
123	good_program_counter code_memory program_counter total_program_size
124	]
125	\| LCALL addr ⇒
126	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
127	[ ADDR16 addr ⇒ λaddr16: True.
128	good_program_counter code_memory addr total_program_size ∧
129	good_program_counter code_memory program_counter total_program_size
130	\| _ ⇒ λother: False. ⊥
131	] (subaddressing_modein … addr)
132	\| ACALL addr ⇒
133	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
134	[ ADDR11 addr ⇒ λaddr11: True.
135	let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
136	let 〈thr, eig〉 ≝ split … 3 8 addr in
137	let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
138	let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
139	good_program_counter code_memory new_program_counter total_program_size ∧
140	good_program_counter code_memory program_counter total_program_size
141	\| _ ⇒ λother: False. ⊥
142	] (subaddressing_modein … addr)
143	\| AJMP addr ⇒
144	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
145	[ ADDR11 addr ⇒ λaddr11: True.
146	let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
147	let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
148	let bit ≝ get_index' … O ? nl in
149	let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
150	let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
151	let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
152	(good_program_counter code_memory new_program_counter total_program_size) ∧
153	(good_program_counter code_memory program_counter total_program_size)
154	\| _ ⇒ λother: False. ⊥
155	] (subaddressing_modein … addr)
156	\| LJMP addr ⇒
157	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
158	[ ADDR16 addr ⇒ λaddr16: True.
159	good_program_counter code_memory addr total_program_size ∧
160	good_program_counter code_memory program_counter total_program_size
161	\| _ ⇒ λother: False. ⊥
162	] (subaddressing_modein … addr)
163	\| SJMP addr ⇒
164	match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
165	[ RELATIVE addr ⇒ λrelative: True.
166	let 〈carry, new_program_counter〉 ≝ half_add … program_counter (sign_extension addr) in
167	good_program_counter code_memory new_program_counter total_program_size ∧
168	good_program_counter code_memory program_counter total_program_size
169	\| _ ⇒ λother: False. ⊥
170	] (subaddressing_modein … addr)
171	\| JMP addr ⇒ True (* XXX: should recurse here, but dptr in JMP ... *)
172	\| MOVC src trgt ⇒
173	good_program_counter code_memory program_counter total_program_size
174	].
175	cases other
176	qed.
177
178	lemma is_in_tail_to_is_in_cons_hd_tl:
179	∀n: nat.
180	∀the_vect: Vector addressing_mode_tag n.
181	∀h: addressing_mode_tag.
182	∀element: addressing_mode.
183	is_in n the_vect element → is_in (S n) (h:::the_vect) element.
184	#n #the_vect #h #element #assm
185	normalize cases (is_a h element) normalize nodelta
186	//
187	qed.
188
189	axiom is_in_subvector_is_in_supervector:
190	∀m, n: nat.
191	∀subvector: Vector addressing_mode_tag m.
192	∀supervector: Vector addressing_mode_tag n.
193	∀element: addressing_mode.
194	subvector_with … eq_a subvector supervector →
195	is_in m subvector element → is_in n supervector element.
196
197	let rec member_addressing_mode_tag
198	(n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
199	on v: Prop ≝
200	match v with
201	[ VEmpty ⇒ False
202	\| VCons n' hd tl ⇒
203	bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
204	].
205
206	let rec subaddressing_mode_elim_type
207	(T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
208	(Q: addressing_mode → T → Prop)
209	(p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T)
210	(p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T)
211	(p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T)
212	(p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T)
213	(p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T)
214	(p_acc_a: is_in m fixed_v ACC_A → T)
215	(p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T)
216	(p_acc_b: is_in m fixed_v ACC_B → T)
217	(p_dptr: is_in m fixed_v DPTR → T)
218	(p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T)
219	(p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T)
220	(p_acc_dptr: is_in m fixed_v ACC_DPTR → T)
221	(p_acc_pc: is_in m fixed_v ACC_PC → T)
222	(p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T)
223	(p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T)
224	(p_carry: is_in m fixed_v CARRY → T)
225	(p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T)
226	(p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T)
227	(p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T)
228	(n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
229	on v: Prop ≝
230	match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
231	[ VEmpty ⇒ λm_refl. λv_refl.
232	∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
233	Q addr (
234	match addr return λx: addressing_mode. is_in … fixed_v x → T with
235	[ ADDR11 x ⇒ p_addr11 x
236	\| ADDR16 x ⇒ p_addr16 x
237	\| DIRECT x ⇒ p_direct x
238	\| INDIRECT x ⇒ p_indirect x
239	\| EXT_INDIRECT x ⇒ p_ext_indirect x
240	\| ACC_A ⇒ p_acc_a
241	\| REGISTER x ⇒ p_register x
242	\| ACC_B ⇒ p_acc_b
243	\| DPTR ⇒ p_dptr
244	\| DATA x ⇒ p_data x
245	\| DATA16 x ⇒ p_data16 x
246	\| ACC_DPTR ⇒ p_acc_dptr
247	\| ACC_PC ⇒ p_acc_pc
248	\| EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
249	\| INDIRECT_DPTR ⇒ p_indirect_dptr
250	\| CARRY ⇒ p_carry
251	\| BIT_ADDR x ⇒ p_bit_addr x
252	\| N_BIT_ADDR x ⇒ p_n_bit_addr x
253	\| RELATIVE x ⇒ p_relative x
254	] p)
255	\| VCons n' hd tl ⇒ λm_refl. λv_refl.
256	let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
257	p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
258	p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
259	p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
260	p_bit_addr p_n_bit_addr p_relative n' tl ?
261	in
262	match hd return λa: addressing_mode_tag. a = hd → ? with
263	[ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
264	\| addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
265	\| direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
266	\| indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
267	\| ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
268	\| acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
269	\| registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
270	\| acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
271	\| dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
272	\| data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
273	\| data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
274	\| acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
275	\| acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
276	\| ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
277	\| indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
278	\| carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
279	\| bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
280	\| n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
281	\| relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
282	] (refl … hd)
283	] (refl … n) (refl_jmeq … v).
284	[20:
285	generalize in match proof; destruct
286	whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
287	cases (mem … eq_a m fixed_v hd) normalize nodelta
288	[1:
289	whd in match (subvector_with … eq_a tl fixed_v);
290	#assm assumption
291	\|2:
292	normalize in ⊢ (% → ?);
293	#absurd cases absurd
294	]
295	]
296	@(is_in_subvector_is_in_supervector n m v fixed_v … proof)
297	destruct @I
298	qed.
299
300	lemma subaddressing_mode_elim':
301	∀T: Type[2].
302	∀m: nat.
303	∀fixed_v: Vector addressing_mode_tag m.
304	∀Q: addressing_mode → T → Prop.
305	∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
306	∀n: nat.
307
308	∀v: Vector addressing_mode_tag n.
309	∀proof.
310	subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
311	P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
312	#T #m #fixed_v #Q #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #n #v
313	elim v
314	[ #proof normalize
315
316	qed.
317
318	(*
319	lemma subaddressing_mode_elim:
320	∀T:Type[2].
321	∀P1: Word11 → T.
322	∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T.
323	∀addr: addressing_mode.
324	∀p: is_in 1 [[ addr11 ]] addr.
325	∀Q: addressing_mode → T → Prop.
326	(∀w. Q (ADDR11 w) (P1 w)) →
327	Q addr (
328	match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with
329	[ ADDR11 (x:Word11) ⇒ λH:True. P1 x
330	\| ADDR16 _ ⇒ λH:False. P2 H
331	\| DIRECT _ ⇒ λH:False. P3 H
332	\| INDIRECT _ ⇒ λH:False. P4 H
333	\| EXT_INDIRECT _ ⇒ λH:False. P5 H
334	\| ACC_A ⇒ λH:False. P6 H
335	\| REGISTER _ ⇒ λH:False. P7 H
336	\| ACC_B ⇒ λH:False. P8 H
337	\| DPTR ⇒ λH:False. P9 H
338	\| DATA _ ⇒ λH:False. P10 H
339	\| DATA16 _ ⇒ λH:False. P11 H
340	\| ACC_DPTR ⇒ λH:False. P12 H
341	\| ACC_PC ⇒ λH:False. P13 H
342	\| EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
343	\| INDIRECT_DPTR ⇒ λH:False. P15 H
344	\| CARRY ⇒ λH:False. P16 H
345	\| BIT_ADDR _ ⇒ λH:False. P17 H
346	\| N_BIT_ADDR _ ⇒ λH:False. P18 H
347	\| RELATIVE _ ⇒ λH:False. P19 H
348	] p).
349	#T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
350	#P14 #P15 #P16 #P17 #P18 #P19
351	* try #x1 try #x2 try #x3 try #x4
352	try (@⊥ assumption) normalize @x4
353	qed. *)
354
355	include alias "arithmetics/nat.ma".
356
357	lemma lt_n_o_to_plus_m_n_lt_plus_m_o:
358	∀m, n, o: nat.
359	n < o → m + n < m + o.
360	#m #n #o #assm /2 by monotonic_le_plus_r/
361	qed.
362
363	axiom fetch_program_counter_n_technical:
364	∀code_memory: BitVectorTrie Byte 16.
365	∀program_counter, program_counter': Word.
366	∀instruction: instruction.
367	∀ticks, n: nat.
368	program_counter' = \snd (\fst (fetch code_memory program_counter)) →
369	program_counter' = fetch_program_counter_n (S n) code_memory (zero …) →
370	program_counter = fetch_program_counter_n n code_memory (zero …).
371
372	let rec block_cost
373	(code_memory: BitVectorTrie Byte 16) (program_counter: Word)
374	(program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
375	(good_program_witness: good_program code_memory program_counter total_program_size)
376	on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
377	match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with
378	[ O ⇒ λbase_case. 0
379	\| S program_size' ⇒ λrecursive_case.
380	let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
381	match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with
382	[ None ⇒
383	match instruction return λx. x = instruction → ? with
384	[ RealInstruction instruction ⇒ λreal_instruction.
385	match instruction return λx. x = instruction → ? with
386	[ RET ⇒ λinstr. ticks
387	\| JC relative ⇒ λinstr. ticks
388	\| JNC relative ⇒ λinstr. ticks
389	\| JB bit_addr relative ⇒ λinstr. ticks
390	\| JNB bit_addr relative ⇒ λinstr. ticks
391	\| JBC bit_addr relative ⇒ λinstr. ticks
392	\| JZ relative ⇒ λinstr. ticks
393	\| JNZ relative ⇒ λinstr. ticks
394	\| CJNE src_trgt relative ⇒ λinstr. ticks
395	\| DJNZ src_trgt relative ⇒ λinstr. ticks
396	\| _ ⇒ λinstr.
397	ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
398	] (refl … instruction)
399	\| ACALL addr ⇒ λinstr.
400	ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
401	\| AJMP addr ⇒ λinstr. ticks
402	\| LCALL addr ⇒ λinstr.
403	ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
404	\| LJMP addr ⇒ λinstr. ticks
405	\| SJMP addr ⇒ λinstr. ticks
406	\| JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
407	ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
408	\| MOVC src trgt ⇒ λinstr.
409	ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
410	] (refl … instruction)
411	\| Some _ ⇒ ticks
412	]
413	].
414	[1:
415	generalize in match good_program_witness;
416	whd in match good_program; normalize nodelta
417	cases FETCH normalize nodelta
418	cases instr normalize nodelta
419	@(subaddressing_mode_elim … [[ addr11 ]]) #new_addr
420	cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
421	cases (split … 3 8 new_addr) #thr #eig normalize nodelta
422	cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
423	#assm cases assm #ignore
424	whd in match good_program_counter; normalize nodelta * #n * *
425	#program_counter_eq' #program_counter_lt_total_program_size
426	#fetch_n_leq_program_counter'
427	@(transitive_le
428	total_program_size
429	((S program_size') + nat_of_bitvector … program_counter)
430	(program_size' + nat_of_bitvector … program_counter') recursive_case)
431	whd in ⊢ (?%?);
432	change with (
433	program_size' + (nat_of_bitvector … program_counter) <
434	program_size' + (nat_of_bitvector … program_counter'))
435	@lt_n_o_to_plus_m_n_lt_plus_m_o
436	>(fetch_program_counter_n_technical code_memory program_counter
437	program_counter' instruction ticks n)
438	/2 by pair_destruct_2/
439	\|7:
440	generalize in match good_program_witness;
441	whd in match good_program; normalize nodelta
442	cases FETCH normalize nodelta
443	cases instr normalize nodelta
444	@(subaddressing_mode_elim … [[ acc_dptr; acc_pc ]]) #new_addr
445	cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
446	cases (split … 3 8 new_addr) #thr #eig normalize nodelta
447	cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
448	#assm cases assm #ignore
449	whd in match good_program_counter; normalize nodelta * #n * *
450	#program_counter_eq' #program_counter_lt_total_program_size
451	#fetch_n_leq_program_counter'
452	@(transitive_le
453	total_program_size
454	((S program_size') + nat_of_bitvector … program_counter)
455	(program_size' + nat_of_bitvector … program_counter') recursive_case)
456	whd in ⊢ (?%?);
457	change with (
458	program_size' + (nat_of_bitvector … program_counter) <
459	program_size' + (nat_of_bitvector … program_counter'))
460	@lt_n_o_to_plus_m_n_lt_plus_m_o
461	>(fetch_program_counter_n_technical code_memory program_counter
462	program_counter' instruction ticks n)
463	/2 by pair_destruct_2/
464	\|3,5,7,9,11:
465	(* XXX etc. need the subaddressing_mode_elim generalizing *)
466	\|2:
467	generalize in match good_program_witness;
468	whd in match (good_program code_memory program_counter total_program_size);
469	cases FETCH normalize nodelta
470	cases instr normalize nodelta
471	@subaddressing_mode_elim #new_addr
472	cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
473	cases (split … 3 8 new_addr) #thr #eig normalize nodelta
474	cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
475	#assm cases assm #ignore #good_program_counter
476	whd in match (good_program code_memory program_counter' total_program_size);
477	cases(fetch code_memory program_counter') #instruction_program_counter'' #ticks''
478	cases(instruction_program_counter'') #instruction'' #program_counter'' normalize nodelta
479
480	[2:
481	(* generalize in match good_program_witness; *)
482	whd in match good_program; normalize nodelta
483	cases FETCH normalize nodelta
484	cases (fetch code_memory program_counter') #instruction_program_counter' #ticks' normalize nodelta
485	cases instruction_program_counter' #instruction' #program_counter'' normalize nodelta
486	cases acall normalize nodelta
487	cases addr #subaddressing_mode cases subaddressing_mode
488	try (#assm #absurd normalize in absurd; cases absurd)
489	try (#absurd normalize in absurd; cases absurd)
490	normalize nodelta
491	cases instruction'
492	try (#assm normalize nodelta)
493	[7:
494	#irrelevant
495	whd in match good_program_counter; normalize nodelta
496
497
498
499
500
501
502
503
504
505	(* XXX: use memoisation here in the future *)
506	let rec block_cost
507	(code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
508	(program_counter: Word) (program_size: nat) (total_program_size: nat)
509	(size_invariant: total_program_size ≤ code_memory_size)
510	(pc_invariant: nat_of_bitvector … program_counter < total_program_size)
511	on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
512	match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
513	[ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *)
514	\| S program_size ⇒ λrecursive_case.
515	let 〈instr, newpc, ticks〉 ≝ fetch … code_memory program_counter in
516	match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
517	[ None ⇒
518	let classify ≝ ASM_classify0 instr in
519	match classify return λx. classify = x → ? with
520	[ cl_jump ⇒ λclassify_refl. ticks
521	\| cl_call ⇒ λclassify_refl. (* ite here *)
522	ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
523	\| cl_return ⇒ λclassify_refl. ticks
524	\| cl_other ⇒ λclassify_refl. (* ite here *)
525	ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
526	] (refl … classify)
527	\| Some _ ⇒ ticks
528	]
529	].
530
531	let rec traverse_code_internal
532	(program: list Byte) (mem: BitVectorTrie Byte 16)
533	(cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
534	on program: identifier_map CostTag nat ≝
535	let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
536	match program with
537	[ nil ⇒ empty_map …
538	\| cons hd tl ⇒
539	match lookup_opt … pc cost_labels with
540	[ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
541	\| Some lbl ⇒
542	let cost ≝ block_cost mem cost_labels pc program_size in
543	let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
544	add … cost_mapping lbl cost ]].
545
546	definition traverse_code ≝
547	λprogram: list Byte.
548	λmem: BitVectorTrie Byte 16.
549	λcost_labels.
550	λprogram_size: nat.
551	traverse_code_internal program mem cost_labels (zero …) program_size.
552
553	definition compute_costs ≝
554	λprogram: list Byte.
555	λcost_labels: BitVectorTrie costlabel 16.
556	λhas_main: bool.
557	let program_size ≝ \|program\| + 1 in
558	let memory ≝ load_code_memory program in
559	traverse_code program memory cost_labels program_size.

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

Download in other formats:

Original Format