source: src/ASM/ASMCosts.ma @ 1624

Last change on this file since 1624 was 1624, checked in by mulligan, 9 years ago

commit for claudio

File size: 24.4 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5include "common/StructuredTraces.ma".
6
7definition current_instruction0 ≝
8  λmem,pc. \fst (\fst (fetch … mem pc)).
9
10definition current_instruction ≝
11 λs:Status. current_instruction0 (code_memory … s) (program_counter … s).
12
13definition 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
39definition ASM_classify: Status → status_class ≝
40 λs.ASM_classify0 (current_instruction s).
41
42definition 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
51definition 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
61definition 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
70definition 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 *)
80definition 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  //
92qed.
93   
94definition 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
104definition 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
176qed.
177
178lemma 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  //
187qed.
188
189let rec member_addressing_mode_tag
190  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
191    on v: Prop ≝
192  match v with
193  [ VEmpty ⇒ False
194  | VCons n' hd tl ⇒
195      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
196  ].
197 
198let rec subaddressing_mode_elim_type
199  (T: Type[2]) (n: nat) (v: Vector addressing_mode_tag n)
200    (Q: addressing_mode → T → Prop)
201      on v:
202    (∀w: Word11.      is_in n v (ADDR11 w)        → T) →
203    (∀w: Word.        is_in n v (ADDR16 w)        → T) →
204    (∀w: Byte.        is_in n v (DIRECT w)        → T) →
205    (∀w: Bit.         is_in n v (INDIRECT w)      → T) →
206    (∀w: Bit.         is_in n v (EXT_INDIRECT w)  → T) →
207    (                 is_in n v ACC_A             → T) →
208    (∀w: BitVector 3. is_in n v (REGISTER w)      → T) →
209    (                 is_in n v ACC_B             → T) →
210    (                 is_in n v DPTR              → T) →
211    (∀w: Byte.        is_in n v (DATA w)          → T) →
212    (∀w: Word.        is_in n v (DATA16 w)        → T) →
213    (                 is_in n v ACC_DPTR          → T) →
214    (                 is_in n v ACC_PC            → T) →
215    (                 is_in n v EXT_INDIRECT_DPTR → T) →
216    (                 is_in n v INDIRECT_DPTR     → T) →
217    (                 is_in n v CARRY             → T) →
218    (∀w: Byte.        is_in n v (BIT_ADDR w)      → T) →
219    (∀w: Byte.        is_in n v (N_BIT_ADDR w)    → T) →
220    (∀w: Byte.        is_in n v (RELATIVE w)      → T) → Prop ≝
221  match v return λm: nat. λv': Vector addressing_mode_tag m. m = n → v ≃ v' → ? with
222  [ VEmpty         ⇒ λm_refl. λv_refl.
223    λp_addr11. λp_addr16. λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a.
224    λp_register. λp_acc_b. λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc.
225    λp_ext_indirect_dptr. λp_indirect_dptr. λp_carry. λp_bit_addr.
226    λp_n_bit_addr. λp_relative.
227      ∀addr. ∀p: is_in … v addr.
228        Q addr (
229        match addr return λx: addressing_mode. is_in … v x → T with 
230        [ ADDR11 x          ⇒ p_addr11 x
231        | ADDR16 x          ⇒ p_addr16 x
232        | DIRECT x          ⇒ p_direct x
233        | INDIRECT x        ⇒ p_indirect x
234        | EXT_INDIRECT x    ⇒ p_ext_indirect x
235        | ACC_A             ⇒ p_acc_a
236        | REGISTER x        ⇒ p_register x
237        | ACC_B             ⇒ p_acc_b
238        | DPTR              ⇒ p_dptr
239        | DATA x            ⇒ p_data x
240        | DATA16 x          ⇒ p_data16 x
241        | ACC_DPTR          ⇒ p_acc_dptr
242        | ACC_PC            ⇒ p_acc_pc
243        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
244        | INDIRECT_DPTR     ⇒ p_indirect_dptr
245        | CARRY             ⇒ p_carry
246        | BIT_ADDR x        ⇒ p_bit_addr x
247        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
248        | RELATIVE x        ⇒ p_relative x
249        ] p)
250  | VCons n' hd tl ⇒ λm_refl. λv_refl.
251    λp_addr11. λp_addr16: (∀w: Word. is_in n v (ADDR16 w)            → T).
252    λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. λp_register. λp_acc_b.
253    λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. λp_ext_indirect_dptr.
254    λp_indirect_dptr. λp_carry. λp_bit_addr. λp_n_bit_addr. λp_relative.
255    let tail_call ≝ subaddressing_mode_elim_type T n' tl Q (? p_addr11)
256      (? p_addr16) (? p_direct) (? p_indirect) (? p_ext_indirect) (? p_acc_a)
257        (? p_register) (? p_acc_b) (? p_dptr) (? p_data) (? p_data16) (? p_acc_dptr)
258          (? p_acc_pc) (? p_ext_indirect_dptr) (? p_indirect_dptr) (? p_carry)
259            (? p_bit_addr) (? p_n_bit_addr) (? p_relative)
260    in
261    match hd return λa: addressing_mode_tag. a = hd → ? with
262    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
263    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
264    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
265    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
266    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
267    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
268    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
269    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
270    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
271    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
272    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
273    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
274    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
275    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
276    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
277    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
278    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
279    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
280    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
281    ] (refl … hd)
282  ] (refl … n) (refl_jmeq … v).
283  try (#_ #w1 try #w2)
284  [20:
285    destruct @p_addr11 try assumption
286    @is_in_tail_to_is_in_cons_hd_tl assumption
287  |21:
288    destruct @p_addr16 try assumption
289    @is_in_tail_to_is_in_cons_hd_tl assumption
290  |22:
291    destruct @p_direct try assumption
292    @is_in_tail_to_is_in_cons_hd_tl assumption
293  |23:
294    destruct @p_indirect try assumption
295    @is_in_tail_to_is_in_cons_hd_tl assumption
296  |24:
297    destruct @p_ext_indirect try assumption
298    @is_in_tail_to_is_in_cons_hd_tl assumption
299  |25:
300    destruct @p_acc_a try assumption
301    @is_in_tail_to_is_in_cons_hd_tl assumption
302  |26:
303    destruct @p_register try assumption
304    @is_in_tail_to_is_in_cons_hd_tl assumption
305  |27:
306    destruct @p_acc_b try assumption
307    @is_in_tail_to_is_in_cons_hd_tl assumption
308  |28:
309    destruct @p_dptr try assumption
310    @is_in_tail_to_is_in_cons_hd_tl assumption
311  |29:
312    destruct @p_data try assumption
313    @is_in_tail_to_is_in_cons_hd_tl assumption
314  |30:
315    destruct @p_data16 try assumption
316    @is_in_tail_to_is_in_cons_hd_tl assumption
317  |31:
318    destruct @p_acc_dptr try assumption
319    @is_in_tail_to_is_in_cons_hd_tl assumption
320  |32:
321    destruct @p_acc_pc try assumption
322    @is_in_tail_to_is_in_cons_hd_tl assumption
323  |33:
324    destruct @p_ext_indirect_dptr try assumption
325    @is_in_tail_to_is_in_cons_hd_tl assumption
326  |34:
327    destruct @p_indirect_dptr try assumption
328    @is_in_tail_to_is_in_cons_hd_tl assumption
329  |35:
330    destruct @p_carry try assumption
331    @is_in_tail_to_is_in_cons_hd_tl assumption
332  |36:
333    destruct @p_bit_addr try assumption
334    @is_in_tail_to_is_in_cons_hd_tl assumption
335  |37:
336    destruct @p_n_bit_addr try assumption
337    @is_in_tail_to_is_in_cons_hd_tl assumption
338  |38:
339    destruct @p_relative try assumption
340    @is_in_tail_to_is_in_cons_hd_tl assumption
341  |*:
342    -tail_call destruct @I
343 ]
344qed.
345
346axiom subaddressing_mode_elim:
347  ∀T: Type[2].
348  ∀n: nat.
349  ∀v: Vector addressing_mode_tag n.
350  ∀Q: addressing_mode → T → Prop.
351  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
352    subaddressing_mode_elim_type T n v Q P1 P2 P3 P4 P5 P6 P7
353      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19.
354
355(*
356lemma subaddressing_mode_elim:
357  ∀T:Type[2].
358  ∀P1: Word11 → T.
359  ∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T.
360  ∀addr: addressing_mode.
361  ∀p: is_in 1 [[ addr11 ]] addr.
362  ∀Q: addressing_mode → T → Prop.
363    (∀w. Q (ADDR11 w) (P1 w)) →
364      Q addr (
365        match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with 
366        [ ADDR11 (x:Word11) ⇒ λH:True. P1 x
367        | ADDR16 _ ⇒ λH:False. P2 H
368        | DIRECT _ ⇒ λH:False. P3 H
369        | INDIRECT _ ⇒ λH:False. P4 H
370        | EXT_INDIRECT _ ⇒ λH:False. P5 H
371        | ACC_A ⇒ λH:False. P6 H
372        | REGISTER _ ⇒ λH:False. P7 H
373        | ACC_B ⇒ λH:False. P8 H
374        | DPTR ⇒ λH:False. P9 H
375        | DATA _ ⇒ λH:False. P10 H
376        | DATA16 _ ⇒ λH:False. P11 H
377        | ACC_DPTR ⇒ λH:False. P12 H
378        | ACC_PC ⇒ λH:False. P13 H
379        | EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
380        | INDIRECT_DPTR ⇒ λH:False. P15 H
381        | CARRY ⇒ λH:False. P16 H
382        | BIT_ADDR _ ⇒ λH:False. P17 H
383        | N_BIT_ADDR _ ⇒ λH:False. P18 H   
384        | RELATIVE _ ⇒ λH:False. P19 H
385        ] p).
386  #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
387  #P14 #P15 #P16 #P17 #P18 #P19
388  * try #x1 try #x2 try #x3 try #x4
389  try (@⊥ assumption) normalize @x4
390qed. *)
391
392include alias "arithmetics/nat.ma".
393
394lemma lt_n_o_to_plus_m_n_lt_plus_m_o:
395  ∀m, n, o: nat.
396    n < o → m + n < m + o.
397  #m #n #o #assm /2 by monotonic_le_plus_r/
398qed.
399
400axiom fetch_program_counter_n_technical:
401  ∀code_memory: BitVectorTrie Byte 16.
402  ∀program_counter, program_counter': Word.
403  ∀instruction: instruction.
404  ∀ticks, n: nat.
405  program_counter' = \snd (\fst (fetch code_memory program_counter)) →
406    program_counter' = fetch_program_counter_n (S n) code_memory (zero …) →
407      program_counter = fetch_program_counter_n n code_memory (zero …).
408   
409let rec block_cost
410  (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
411    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
412      (good_program_witness: good_program code_memory program_counter total_program_size)
413        on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
414  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with
415  [ O ⇒ λbase_case. 0
416  | S program_size' ⇒ λrecursive_case.
417    let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
418      match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with
419      [ None   ⇒
420        match instruction return λx. x = instruction → ? with
421        [ RealInstruction instruction ⇒ λreal_instruction.
422          match instruction return λx. x = instruction → ? with
423          [ RET                    ⇒ λinstr. ticks
424          | JC   relative          ⇒ λinstr. ticks
425          | JNC  relative          ⇒ λinstr. ticks
426          | JB   bit_addr relative ⇒ λinstr. ticks
427          | JNB  bit_addr relative ⇒ λinstr. ticks
428          | JBC  bit_addr relative ⇒ λinstr. ticks
429          | JZ   relative          ⇒ λinstr. ticks
430          | JNZ  relative          ⇒ λinstr. ticks
431          | CJNE src_trgt relative ⇒ λinstr. ticks
432          | DJNZ src_trgt relative ⇒ λinstr. ticks
433          | _                      ⇒ λinstr.
434              ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
435          ] (refl … instruction)
436        | ACALL addr     ⇒ λinstr.
437            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
438        | AJMP  addr     ⇒ λinstr. ticks
439        | LCALL addr     ⇒ λinstr.
440            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
441        | LJMP  addr     ⇒ λinstr. ticks
442        | SJMP  addr     ⇒ λinstr. ticks
443        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
444            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
445        | MOVC  src trgt ⇒ λinstr.
446            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
447        ] (refl … instruction)
448      | Some _ ⇒ ticks
449      ]
450  ].
451  [1:
452    generalize in match good_program_witness;
453    whd in match good_program; normalize nodelta
454    cases FETCH normalize nodelta
455    cases instr normalize nodelta
456    @(subaddressing_mode_elim Prop 1 [[ addr11 ]]) try //
457    [2: normalize // #new_addr
458    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
459    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
460    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
461    #assm cases assm #ignore
462    whd in match good_program_counter; normalize nodelta * #n * *
463    #program_counter_eq' #program_counter_lt_total_program_size
464    #fetch_n_leq_program_counter'
465    @(transitive_le
466      total_program_size
467      ((S program_size') + nat_of_bitvector … program_counter)
468      (program_size' + nat_of_bitvector … program_counter') recursive_case)
469    whd in ⊢ (?%?);
470    change with (
471      program_size' + (nat_of_bitvector … program_counter) <
472        program_size' + (nat_of_bitvector … program_counter'))
473    @lt_n_o_to_plus_m_n_lt_plus_m_o
474    >(fetch_program_counter_n_technical code_memory program_counter
475      program_counter' instruction ticks n)
476    /2 by pair_destruct_2/
477  |3,5,7,9,11:
478    (* XXX etc. need the subaddressing_mode_elim generalizing *)
479  |2:
480    generalize in match good_program_witness;
481    whd in match (good_program code_memory program_counter total_program_size);
482    cases FETCH normalize nodelta
483    cases instr normalize nodelta
484    @subaddressing_mode_elim #new_addr
485    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
486    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
487    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
488    #assm cases assm #ignore #good_program_counter
489    whd in match (good_program code_memory program_counter' total_program_size);
490    cases(fetch code_memory program_counter') #instruction_program_counter'' #ticks''
491    cases(instruction_program_counter'') #instruction'' #program_counter'' normalize nodelta
492   
493  [2:
494    (* generalize in match good_program_witness; *)
495    whd in match good_program; normalize nodelta
496    cases FETCH normalize nodelta
497    cases (fetch code_memory program_counter') #instruction_program_counter' #ticks' normalize nodelta
498    cases instruction_program_counter' #instruction' #program_counter'' normalize nodelta
499    cases acall normalize nodelta
500    cases addr #subaddressing_mode cases subaddressing_mode
501    try (#assm #absurd normalize in absurd; cases absurd)
502    try (#absurd normalize in absurd; cases absurd)
503    normalize nodelta
504    cases instruction'
505    try (#assm normalize nodelta)
506    [7:
507      #irrelevant
508      whd in match good_program_counter; normalize nodelta
509     
510     
511     
512     
513     
514     
515     
516     
517     
518(* XXX: use memoisation here in the future *)
519let rec block_cost
520  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
521    (program_counter: Word) (program_size: nat) (total_program_size: nat)
522      (size_invariant: total_program_size ≤ code_memory_size)
523        (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
524          on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
525  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
526  [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *)
527  | S program_size ⇒ λrecursive_case.
528    let 〈instr, newpc, ticks〉 ≝ fetch … code_memory program_counter in
529      match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
530      [ None ⇒
531          let classify ≝ ASM_classify0 instr in
532          match classify return λx. classify = x → ? with
533          [ cl_jump ⇒ λclassify_refl. ticks
534          | cl_call ⇒ λclassify_refl. (* ite here *)
535              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
536          | cl_return ⇒ λclassify_refl. ticks
537          | cl_other ⇒ λclassify_refl. (* ite here *)
538              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
539          ] (refl … classify)
540        | Some _ ⇒ ticks
541      ]
542  ].
543
544let rec traverse_code_internal
545  (program: list Byte) (mem: BitVectorTrie Byte 16)
546    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
547      on program: identifier_map CostTag nat ≝
548 let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
549 match program with
550 [ nil ⇒ empty_map …
551 | cons hd tl ⇒
552   match lookup_opt … pc cost_labels with
553   [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
554   | Some lbl ⇒
555     let cost ≝ block_cost mem cost_labels pc program_size in
556     let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
557       add … cost_mapping lbl cost ]].
558
559definition traverse_code ≝
560  λprogram: list Byte.
561  λmem: BitVectorTrie Byte 16.
562  λcost_labels.
563  λprogram_size: nat.
564    traverse_code_internal program mem cost_labels (zero …) program_size.
565
566definition compute_costs ≝
567  λprogram: list Byte.
568  λcost_labels: BitVectorTrie costlabel 16.
569  λhas_main: bool.
570  let program_size ≝ |program| + 1 in
571  let memory ≝ load_code_memory program in
572   traverse_code program memory cost_labels program_size.
Note: See TracBrowser for help on using the repository browser.