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. |
---|