source: src/ASM/ASMCosts.ma @ 1639

Last change on this file since 1639 was 1639, checked in by mulligan, 8 years ago

changes from today

File size: 27.0 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 → nat → Word → Prop ≝
95  λcode_memory: BitVectorTrie Byte 16.
96  λprogram_size: nat.
97  λprogram_counter: Word.
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
104axiom half_add_zero:
105  ∀n: nat.
106  ∀b: BitVector n.
107    \snd (half_add n (zero …) b) = b.
108
109lemma fetch_program_counter_n_half_add:
110  ∀n: nat.
111  ∀code_memory: BitVectorTrie Byte 16.
112    fetch_program_counter_n (S n) code_memory (zero …) =
113      let program_counter ≝ fetch_program_counter_n n code_memory (zero …) in
114      let 〈instr, new_program_counter, cost〉 ≝ fetch code_memory program_counter in
115        \snd (half_add … program_counter new_program_counter).
116  #n #code_memory elim n
117  [1:
118    whd in match (fetch_program_counter_n 1 code_memory (zero …));
119    normalize in match (fetch_program_counter_n 0 code_memory (zero …));
120    change with (
121      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory (zero …) in
122        program_counter
123    ) in ⊢ (??%?);
124    cases (fetch code_memory (zero …)) #instr #program_counter normalize nodelta
125    generalize in match instr; #instr
126    cases instr #instr #program_counter normalize nodelta
127    >half_add_zero %
128  |2:
129    #n' #ind_hyp
130    whd in match (fetch_program_counter_n (S (S n')) code_memory (zero …));
131    >ind_hyp (* XXX: things start going wrong here!
132    generalize in match (let (program_counter:Word) ≝
133                  fetch_program_counter_n n' code_memory (zero 16) in 
134           let 〈eta40050,cost〉 ≝fetch code_memory program_counter in 
135           let 〈instr,new_program_counter〉 ≝eta40050 in 
136           \snd  (half_add 16 program_counter new_program_counter));
137    #B normalize nodelta
138    cases (fetch code_memory B) #instr_program_counter #cost normalize nodelta
139    cases instr_program_counter #instr #program_counter normalize nodelta *)
140    cases daemon
141  ]
142qed.
143   
144definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝
145  λcode_memory: BitVectorTrie Byte 16.
146  λprogram_counter: Word.
147  λtotal_program_size: nat.
148  let 〈instruction, program_counter, ticks〉 ≝ fetch code_memory program_counter in
149    match instruction with
150    [ RealInstruction instr ⇒
151      match instr with
152      [ RET                    ⇒ True
153      | JC   relative          ⇒ True (* XXX: see below *)
154      | JNC  relative          ⇒ True (* XXX: see below *)
155      | JB   bit_addr relative ⇒ True
156      | JNB  bit_addr relative ⇒ True
157      | JBC  bit_addr relative ⇒ True
158      | JZ   relative          ⇒ True
159      | JNZ  relative          ⇒ True
160      | CJNE src_trgt relative ⇒ True
161      | DJNZ src_trgt relative ⇒ True
162      | _                      ⇒
163          good_program_counter code_memory total_program_size program_counter
164      ]
165    | LCALL addr         ⇒
166      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
167      [ ADDR16 addr ⇒ λaddr16: True.
168          good_program_counter code_memory total_program_size addr ∧
169            good_program_counter code_memory total_program_size program_counter
170      | _ ⇒ λother: False. ⊥
171      ] (subaddressing_modein … addr)
172    | ACALL addr         ⇒
173      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
174      [ ADDR11 addr ⇒ λaddr11: True.
175        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
176        let 〈thr, eig〉 ≝ split … 3 8 addr in
177        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
178        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
179          good_program_counter code_memory total_program_size new_program_counter ∧
180            good_program_counter code_memory total_program_size program_counter
181      | _ ⇒ λother: False. ⊥
182      ] (subaddressing_modein … addr)
183    | AJMP  addr         ⇒
184      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
185      [ ADDR11 addr ⇒ λaddr11: True.
186        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
187        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
188        let bit ≝ get_index' … O ? nl in
189        let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
190        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
191        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
192          (good_program_counter code_memory total_program_size new_program_counter) ∧
193            (good_program_counter code_memory total_program_size program_counter)
194      | _ ⇒ λother: False. ⊥
195      ] (subaddressing_modein … addr)
196    | LJMP  addr         ⇒
197      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
198      [ ADDR16 addr ⇒ λaddr16: True.
199          good_program_counter code_memory total_program_size addr ∧
200            good_program_counter code_memory total_program_size program_counter
201      | _ ⇒ λother: False. ⊥
202      ] (subaddressing_modein … addr)
203    | SJMP  addr     ⇒
204      match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
205      [ RELATIVE addr ⇒ λrelative: True.
206        let 〈carry, new_program_counter〉 ≝ half_add … program_counter (sign_extension addr) in
207          good_program_counter code_memory total_program_size new_program_counter ∧
208            good_program_counter code_memory total_program_size program_counter
209      | _ ⇒ λother: False. ⊥
210      ] (subaddressing_modein … addr)
211    | JMP   addr     ⇒ True (* XXX: should recurse here, but dptr in JMP ... *)
212    | MOVC  src trgt ⇒
213        good_program_counter code_memory total_program_size program_counter
214    ].
215  cases other
216qed.
217
218lemma is_in_tail_to_is_in_cons_hd_tl:
219  ∀n: nat.
220  ∀the_vect: Vector addressing_mode_tag n.
221  ∀h: addressing_mode_tag.
222  ∀element: addressing_mode.
223    is_in n the_vect element → is_in (S n) (h:::the_vect) element.
224  #n #the_vect #h #element #assm
225  normalize cases (is_a h element) normalize nodelta
226  //
227qed.
228
229axiom is_in_subvector_is_in_supervector:
230  ∀m, n: nat.
231  ∀subvector: Vector addressing_mode_tag m.
232  ∀supervector: Vector addressing_mode_tag n.
233  ∀element: addressing_mode.
234    subvector_with … eq_a subvector supervector →
235      is_in m subvector element → is_in n supervector element.
236
237let rec member_addressing_mode_tag
238  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
239    on v: Prop ≝
240  match v with
241  [ VEmpty ⇒ False
242  | VCons n' hd tl ⇒
243      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
244  ].
245 
246let rec subaddressing_mode_elim_type
247  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
248    (Q: addressing_mode → T → Prop)
249      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
250      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
251      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
252      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
253      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
254      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
255      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
256      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
257      (p_dptr:                               is_in m fixed_v DPTR              → T)
258      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
259      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
260      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
261      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
262      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
263      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
264      (p_carry:                              is_in m fixed_v CARRY             → T)
265      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
266      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
267      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
268        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
269      on v: Prop ≝
270  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
271  [ VEmpty         ⇒ λm_refl. λv_refl.
272      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
273        Q addr (
274        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
275        [ ADDR11 x          ⇒ p_addr11 x
276        | ADDR16 x          ⇒ p_addr16 x
277        | DIRECT x          ⇒ p_direct x
278        | INDIRECT x        ⇒ p_indirect x
279        | EXT_INDIRECT x    ⇒ p_ext_indirect x
280        | ACC_A             ⇒ p_acc_a
281        | REGISTER x        ⇒ p_register x
282        | ACC_B             ⇒ p_acc_b
283        | DPTR              ⇒ p_dptr
284        | DATA x            ⇒ p_data x
285        | DATA16 x          ⇒ p_data16 x
286        | ACC_DPTR          ⇒ p_acc_dptr
287        | ACC_PC            ⇒ p_acc_pc
288        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
289        | INDIRECT_DPTR     ⇒ p_indirect_dptr
290        | CARRY             ⇒ p_carry
291        | BIT_ADDR x        ⇒ p_bit_addr x
292        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
293        | RELATIVE x        ⇒ p_relative x
294        ] p)
295  | VCons n' hd tl ⇒ λm_refl. λv_refl.
296    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
297      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
298        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
299          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
300            p_bit_addr p_n_bit_addr p_relative n' tl ?
301    in
302    match hd return λa: addressing_mode_tag. a = hd → ? with
303    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
304    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
305    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
306    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
307    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
308    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
309    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
310    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
311    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
312    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
313    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
314    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
315    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
316    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
317    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
318    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
319    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
320    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
321    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
322    ] (refl … hd)
323  ] (refl … n) (refl_jmeq … v).
324  [20:
325    generalize in match proof; destruct
326    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
327    cases (mem … eq_a m fixed_v hd) normalize nodelta
328    [1:
329      whd in match (subvector_with … eq_a tl fixed_v);
330      #assm assumption
331    |2:
332      normalize in ⊢ (% → ?);
333      #absurd cases absurd
334    ]
335  ]
336  @(is_in_subvector_is_in_supervector n m v fixed_v … proof)
337  destruct @I
338qed.
339
340axiom subaddressing_mode_elim':
341  ∀T: Type[2].
342  ∀m: nat.
343  ∀fixed_v: Vector addressing_mode_tag m.
344  ∀Q: addressing_mode → T → Prop.
345  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
346  ∀n: nat.
347  ∀v: Vector addressing_mode_tag n.
348  ∀proof.
349    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
350      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
351(*  #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
352  elim v
353  [ #proof normalize
354   
355qed. *)
356
357(*
358lemma subaddressing_mode_elim:
359  ∀T:Type[2].
360  ∀P1: Word11 → T.
361  ∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T.
362  ∀addr: addressing_mode.
363  ∀p: is_in 1 [[ addr11 ]] addr.
364  ∀Q: addressing_mode → T → Prop.
365    (∀w. Q (ADDR11 w) (P1 w)) →
366      Q addr (
367        match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with 
368        [ ADDR11 (x:Word11) ⇒ λH:True. P1 x
369        | ADDR16 _ ⇒ λH:False. P2 H
370        | DIRECT _ ⇒ λH:False. P3 H
371        | INDIRECT _ ⇒ λH:False. P4 H
372        | EXT_INDIRECT _ ⇒ λH:False. P5 H
373        | ACC_A ⇒ λH:False. P6 H
374        | REGISTER _ ⇒ λH:False. P7 H
375        | ACC_B ⇒ λH:False. P8 H
376        | DPTR ⇒ λH:False. P9 H
377        | DATA _ ⇒ λH:False. P10 H
378        | DATA16 _ ⇒ λH:False. P11 H
379        | ACC_DPTR ⇒ λH:False. P12 H
380        | ACC_PC ⇒ λH:False. P13 H
381        | EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
382        | INDIRECT_DPTR ⇒ λH:False. P15 H
383        | CARRY ⇒ λH:False. P16 H
384        | BIT_ADDR _ ⇒ λH:False. P17 H
385        | N_BIT_ADDR _ ⇒ λH:False. P18 H   
386        | RELATIVE _ ⇒ λH:False. P19 H
387        ] p).
388  #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
389  #P14 #P15 #P16 #P17 #P18 #P19
390  * try #x1 try #x2 try #x3 try #x4
391  try (@⊥ assumption) normalize @x4
392qed. *)
393
394include alias "arithmetics/nat.ma".
395
396lemma lt_n_o_to_plus_m_n_lt_plus_m_o:
397  ∀m, n, o: nat.
398    n < o → m + n < m + o.
399  #m #n #o #assm /2 by monotonic_le_plus_r/
400qed.
401
402axiom fetch_program_counter_n_technical:
403  ∀n: nat.
404  ∀code_memory: BitVectorTrie Byte 16.
405  ∀program_counter, program_counter': Word.
406  program_counter' = fetch_program_counter_n (S n) code_memory (zero …) →
407    program_counter' = \snd (\fst (fetch code_memory program_counter)) →
408      program_counter = fetch_program_counter_n n code_memory (zero …).
409   
410let rec block_cost
411  (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
412    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
413      (good_program_witness: good_program code_memory program_counter total_program_size)
414        on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
415  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with
416  [ O ⇒ λbase_case. 0
417  | S program_size' ⇒ λrecursive_case.
418    let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
419      match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with
420      [ None   ⇒
421        match instruction return λx. x = instruction → ? with
422        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
423          match real_instruction return λx. x = real_instruction → ? with
424          [ RET                    ⇒ λinstr. ticks
425          | JC   relative          ⇒ λinstr. ticks
426          | JNC  relative          ⇒ λinstr. ticks
427          | JB   bit_addr relative ⇒ λinstr. ticks
428          | JNB  bit_addr relative ⇒ λinstr. ticks
429          | JBC  bit_addr relative ⇒ λinstr. ticks
430          | JZ   relative          ⇒ λinstr. ticks
431          | JNZ  relative          ⇒ λinstr. ticks
432          | CJNE src_trgt relative ⇒ λinstr. ticks
433          | DJNZ src_trgt relative ⇒ λinstr. ticks
434          | _                      ⇒ λinstr.
435              ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
436          ] (refl … real_instruction)
437        | ACALL addr     ⇒ λinstr.
438            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
439        | AJMP  addr     ⇒ λinstr. ticks
440        | LCALL addr     ⇒ λinstr.
441            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
442        | LJMP  addr     ⇒ λinstr. ticks
443        | SJMP  addr     ⇒ λinstr. ticks
444        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
445            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
446        | MOVC  src trgt ⇒ λinstr.
447            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
448        ] (refl … instruction)
449      | Some _ ⇒ ticks
450      ]
451  ].
452  [1: (* ACALL *)
453    generalize in match good_program_witness;
454    whd in match good_program; normalize nodelta
455    cases FETCH normalize nodelta
456    cases instr normalize nodelta
457    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #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 n code_memory program_counter program_counter')
475    /2 by pair_destruct_2/
476  |2:
477    generalize in match good_program_witness;
478    whd in match good_program in ⊢ (? → %); normalize nodelta
479    cases FETCH normalize nodelta
480    cases instr normalize nodelta
481    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
482    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
483    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
484    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
485    * #ignore #good_program_counter_assm
486    cases (fetch code_memory program_counter') #instruction_program_counter #cost normalize nodelta
487    cases instruction_program_counter #instruction #program_counter normalize nodelta
488    cases instruction
489    [1:
490      #addr11 normalize nodelta
491      cases addr11 #addressing_mode
492      cases addressing_mode
493      try (#assm #proof normalize in proof; cases proof)
494      try (#proof normalize in proof; cases proof)
495      normalize nodelta
496  |3: (* LCALL *)
497    generalize in match good_program_witness;
498    whd in match good_program; normalize nodelta
499    cases FETCH normalize nodelta
500    cases instr normalize nodelta
501    @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
502    #assm cases assm #ignore
503    whd in match good_program_counter; normalize nodelta * #n * *
504    #program_counter_eq' #program_counter_lt_total_program_size
505    #fetch_n_leq_program_counter'
506    @(transitive_le
507      total_program_size
508      ((S program_size') + nat_of_bitvector … program_counter)
509      (program_size' + nat_of_bitvector … program_counter') recursive_case)
510    whd in ⊢ (?%?);
511    change with (
512      program_size' + (nat_of_bitvector … program_counter) <
513        program_size' + (nat_of_bitvector … program_counter'))
514    @lt_n_o_to_plus_m_n_lt_plus_m_o
515    >(fetch_program_counter_n_technical n code_memory program_counter program_counter')
516    /2 by pair_destruct_2/
517  |5: (* JMP *)
518    generalize in match good_program_witness;
519    whd in match good_program; normalize nodelta
520    cases FETCH normalize nodelta
521    cases instr normalize nodelta
522    cases daemon (* XXX ??? *)
523  |7: (* MOVC *)
524    generalize in match good_program_witness;
525    whd in match good_program; normalize nodelta
526    cases FETCH normalize nodelta
527    cases instr normalize nodelta
528    cases daemon (* XXX ??? *)
529  |9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,
530   49,51,53,55,57,59,61,63: (* ADD and similar non-branching instructions *)
531    generalize in match good_program_witness;
532    whd in match good_program; normalize nodelta
533    cases FETCH normalize nodelta
534    cases real_instruction_refl
535    cases instr normalize nodelta
536    whd in match good_program_counter; normalize nodelta
537    * #the_n * *
538    #program_counter_fetch_program_counter_n' #program_counter_lt_total_program_size'
539    #fetch_program_n_lt_program_counter'
540    @(transitive_le
541      total_program_size
542      (S program_size' + nat_of_bitvector … program_counter)
543      (program_size' + nat_of_bitvector … program_counter')
544      recursive_case)
545    normalize in match (S program_size' + nat_of_bitvector … program_counter);
546    >plus_n_Sm
547    @monotonic_le_plus_r
548    change with (
549      nat_of_bitvector … program_counter <
550        nat_of_bitvector … program_counter')
551    generalize in match (
552      fetch_program_counter_n_technical the_n code_memory
553        program_counter program_counter' program_counter_fetch_program_counter_n');
554    #hyp >hyp
555    >program_counter_fetch_program_counter_n'
556  ]
557qed.
558     
559     
560     
561     
562     
563     
564     
565     
566     
567(* XXX: use memoisation here in the future *)
568let rec block_cost
569  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
570    (program_counter: Word) (program_size: nat) (total_program_size: nat)
571      (size_invariant: total_program_size ≤ code_memory_size)
572        (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
573          on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
574  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
575  [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *)
576  | S program_size ⇒ λrecursive_case.
577    let 〈instr, newpc, ticks〉 ≝ fetch … code_memory program_counter in
578      match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
579      [ None ⇒
580          let classify ≝ ASM_classify0 instr in
581          match classify return λx. classify = x → ? with
582          [ cl_jump ⇒ λclassify_refl. ticks
583          | cl_call ⇒ λclassify_refl. (* ite here *)
584              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
585          | cl_return ⇒ λclassify_refl. ticks
586          | cl_other ⇒ λclassify_refl. (* ite here *)
587              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
588          ] (refl … classify)
589        | Some _ ⇒ ticks
590      ]
591  ].
592
593let rec traverse_code_internal
594  (program: list Byte) (mem: BitVectorTrie Byte 16)
595    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
596      on program: identifier_map CostTag nat ≝
597 let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
598 match program with
599 [ nil ⇒ empty_map …
600 | cons hd tl ⇒
601   match lookup_opt … pc cost_labels with
602   [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
603   | Some lbl ⇒
604     let cost ≝ block_cost mem cost_labels pc program_size in
605     let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
606       add … cost_mapping lbl cost ]].
607
608definition traverse_code ≝
609  λprogram: list Byte.
610  λmem: BitVectorTrie Byte 16.
611  λcost_labels.
612  λprogram_size: nat.
613    traverse_code_internal program mem cost_labels (zero …) program_size.
614
615definition compute_costs ≝
616  λprogram: list Byte.
617  λcost_labels: BitVectorTrie costlabel 16.
618  λhas_main: bool.
619  let program_size ≝ |program| + 1 in
620  let memory ≝ load_code_memory program in
621   traverse_code program memory cost_labels program_size.
Note: See TracBrowser for help on using the repository browser.