source: src/ASM/ASMCosts.ma @ 1642

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

finished big proof in all but two cases

File size: 32.2 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
94let rec fetch_program_counter_n
95  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
96    on n: option Word ≝
97  match n with
98  [ O ⇒ Some … program_counter
99  | S n ⇒
100    match fetch_program_counter_n n code_memory program_counter with
101    [ None ⇒ None …
102    | Some tail_pc ⇒
103      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
104        if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
105          Some … program_counter
106        else
107          None Word (* XXX: overflow! *)
108    ]
109  ].
110   
111definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
112  λcode_memory: BitVectorTrie Byte 16.
113  λprogram_size: nat.
114  λprogram_counter: Word.
115    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
116        nat_of_bitvector 16 program_counter < program_size.
117
118axiom full_add_zero:
119  ∀n: nat.
120  ∀b: BitVector n.
121    \snd (full_add n (zero …) b false) = b.
122
123lemma half_add_zero:
124  ∀n: nat.
125  ∀b: BitVector n.
126    \snd (half_add n (zero …) b) = b.
127  #n #b
128  cases b
129  [1:
130    %
131  |2:
132    #n' #hd #tl
133    cases hd
134    whd in match half_add; normalize nodelta
135    >full_add_zero %
136  ]
137qed.
138   
139definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
140  λcode_memory: BitVectorTrie Byte 16.
141  λtotal_program_size: nat.
142  ∀program_counter: Word.
143  ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
144  let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
145    match instruction with
146    [ RealInstruction instr ⇒
147      match instr with
148      [ RET                    ⇒ True
149      | JC   relative          ⇒ True (* XXX: see below *)
150      | JNC  relative          ⇒ True (* XXX: see below *)
151      | JB   bit_addr relative ⇒ True
152      | JNB  bit_addr relative ⇒ True
153      | JBC  bit_addr relative ⇒ True
154      | JZ   relative          ⇒ True
155      | JNZ  relative          ⇒ True
156      | CJNE src_trgt relative ⇒ True
157      | DJNZ src_trgt relative ⇒ True
158      | _                      ⇒
159        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
160          nat_of_bitvector … program_counter' < total_program_size
161      ]
162    | LCALL addr         ⇒
163      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
164      [ ADDR16 addr ⇒ λaddr16: True.
165          reachable_program_counter code_memory total_program_size addr ∧
166            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
167              nat_of_bitvector … program_counter' < total_program_size
168      | _ ⇒ λother: False. ⊥
169      ] (subaddressing_modein … addr)
170    | ACALL addr         ⇒
171      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
172      [ ADDR11 addr ⇒ λaddr11: True.
173        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
174        let 〈thr, eig〉 ≝ split … 3 8 addr in
175        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
176        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
177          reachable_program_counter code_memory total_program_size new_program_counter ∧
178            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
179              nat_of_bitvector … program_counter' < total_program_size
180      | _ ⇒ λother: False. ⊥
181      ] (subaddressing_modein … addr)
182    | AJMP  addr         ⇒
183      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
184      [ ADDR11 addr ⇒ λaddr11: True.
185        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
186        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
187        let bit ≝ get_index' … O ? nl in
188        let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
189        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
190        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
191          reachable_program_counter code_memory total_program_size new_program_counter
192      | _ ⇒ λother: False. ⊥
193      ] (subaddressing_modein … addr)
194    | LJMP  addr         ⇒
195      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
196      [ ADDR16 addr ⇒ λaddr16: True.
197          reachable_program_counter code_memory total_program_size addr
198      | _ ⇒ λother: False. ⊥
199      ] (subaddressing_modein … addr)
200    | SJMP  addr     ⇒
201      match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
202      [ RELATIVE addr ⇒ λrelative: True.
203        let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in
204          reachable_program_counter code_memory total_program_size new_program_counter
205      | _ ⇒ λother: False. ⊥
206      ] (subaddressing_modein … addr)
207    | JMP   addr     ⇒ True (* XXX: JMP is used for fptrs and unconstrained *)
208    | MOVC  src trgt ⇒
209        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
210          nat_of_bitvector … program_counter' < total_program_size
211    ].
212  cases other
213qed.
214
215lemma is_in_tail_to_is_in_cons_hd_tl:
216  ∀n: nat.
217  ∀the_vect: Vector addressing_mode_tag n.
218  ∀h: addressing_mode_tag.
219  ∀element: addressing_mode.
220    is_in n the_vect element → is_in (S n) (h:::the_vect) element.
221  #n #the_vect #h #element #assm
222  normalize cases (is_a h element) normalize nodelta
223  //
224qed.
225
226lemma is_in_subvector_is_in_supervector:
227  ∀m, n: nat.
228  ∀subvector: Vector addressing_mode_tag m.
229  ∀supervector: Vector addressing_mode_tag n.
230  ∀element: addressing_mode.
231    subvector_with … eq_a subvector supervector →
232      is_in m subvector element → is_in n supervector element.
233  #m #n #subvector #supervector #element
234  elim subvector
235  [1:
236    #subvector_proof #is_in_proof
237    normalize in is_in_proof; cases is_in_proof
238  |2:
239    #n' #addressing_mode_tag #tail #ind_hyp #subvector_proof #is_in_proof
240    @ind_hyp
241    cases daemon (* XXX *)
242  ]
243qed.
244
245let rec member_addressing_mode_tag
246  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
247    on v: Prop ≝
248  match v with
249  [ VEmpty ⇒ False
250  | VCons n' hd tl ⇒
251      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
252  ].
253 
254let rec subaddressing_mode_elim_type
255  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
256    (Q: addressing_mode → T → Prop)
257      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
258      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
259      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
260      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
261      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
262      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
263      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
264      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
265      (p_dptr:                               is_in m fixed_v DPTR              → T)
266      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
267      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
268      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
269      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
270      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
271      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
272      (p_carry:                              is_in m fixed_v CARRY             → T)
273      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
274      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
275      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
276        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
277      on v: Prop ≝
278  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
279  [ VEmpty         ⇒ λm_refl. λv_refl.
280      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
281        Q addr (
282        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
283        [ ADDR11 x          ⇒ p_addr11 x
284        | ADDR16 x          ⇒ p_addr16 x
285        | DIRECT x          ⇒ p_direct x
286        | INDIRECT x        ⇒ p_indirect x
287        | EXT_INDIRECT x    ⇒ p_ext_indirect x
288        | ACC_A             ⇒ p_acc_a
289        | REGISTER x        ⇒ p_register x
290        | ACC_B             ⇒ p_acc_b
291        | DPTR              ⇒ p_dptr
292        | DATA x            ⇒ p_data x
293        | DATA16 x          ⇒ p_data16 x
294        | ACC_DPTR          ⇒ p_acc_dptr
295        | ACC_PC            ⇒ p_acc_pc
296        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
297        | INDIRECT_DPTR     ⇒ p_indirect_dptr
298        | CARRY             ⇒ p_carry
299        | BIT_ADDR x        ⇒ p_bit_addr x
300        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
301        | RELATIVE x        ⇒ p_relative x
302        ] p)
303  | VCons n' hd tl ⇒ λm_refl. λv_refl.
304    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
305      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
306        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
307          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
308            p_bit_addr p_n_bit_addr p_relative n' tl ?
309    in
310    match hd return λa: addressing_mode_tag. a = hd → ? with
311    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
312    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
313    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
314    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
315    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
316    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
317    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
318    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
319    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
320    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
321    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
322    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
323    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
324    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
325    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
326    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
327    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
328    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
329    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
330    ] (refl … hd)
331  ] (refl … n) (refl_jmeq … v).
332  [20:
333    generalize in match proof; destruct
334    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
335    cases (mem … eq_a m fixed_v hd) normalize nodelta
336    [1:
337      whd in match (subvector_with … eq_a tl fixed_v);
338      #assm assumption
339    |2:
340      normalize in ⊢ (% → ?);
341      #absurd cases absurd
342    ]
343  ]
344  @(is_in_subvector_is_in_supervector n m v fixed_v … proof)
345  destruct @I
346qed.
347
348axiom subaddressing_mode_elim':
349  ∀T: Type[2].
350  ∀m: nat.
351  ∀fixed_v: Vector addressing_mode_tag m.
352  ∀Q: addressing_mode → T → Prop.
353  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
354  ∀n: nat.
355  ∀v: Vector addressing_mode_tag n.
356  ∀proof.
357    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
358      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
359(*  #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
360  elim v
361  [ #proof normalize
362   
363qed. *)
364
365(*
366lemma subaddressing_mode_elim:
367  ∀T:Type[2].
368  ∀P1: Word11 → T.
369  ∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T.
370  ∀addr: addressing_mode.
371  ∀p: is_in 1 [[ addr11 ]] addr.
372  ∀Q: addressing_mode → T → Prop.
373    (∀w. Q (ADDR11 w) (P1 w)) →
374      Q addr (
375        match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with 
376        [ ADDR11 (x:Word11) ⇒ λH:True. P1 x
377        | ADDR16 _ ⇒ λH:False. P2 H
378        | DIRECT _ ⇒ λH:False. P3 H
379        | INDIRECT _ ⇒ λH:False. P4 H
380        | EXT_INDIRECT _ ⇒ λH:False. P5 H
381        | ACC_A ⇒ λH:False. P6 H
382        | REGISTER _ ⇒ λH:False. P7 H
383        | ACC_B ⇒ λH:False. P8 H
384        | DPTR ⇒ λH:False. P9 H
385        | DATA _ ⇒ λH:False. P10 H
386        | DATA16 _ ⇒ λH:False. P11 H
387        | ACC_DPTR ⇒ λH:False. P12 H
388        | ACC_PC ⇒ λH:False. P13 H
389        | EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
390        | INDIRECT_DPTR ⇒ λH:False. P15 H
391        | CARRY ⇒ λH:False. P16 H
392        | BIT_ADDR _ ⇒ λH:False. P17 H
393        | N_BIT_ADDR _ ⇒ λH:False. P18 H   
394        | RELATIVE _ ⇒ λH:False. P19 H
395        ] p).
396  #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
397  #P14 #P15 #P16 #P17 #P18 #P19
398  * try #x1 try #x2 try #x3 try #x4
399  try (@⊥ assumption) normalize @x4
400qed. *)
401
402include alias "arithmetics/nat.ma".
403
404lemma lt_n_o_to_plus_m_n_lt_plus_m_o:
405  ∀m, n, o: nat.
406    n < o → m + n < m + o.
407  #m #n #o #assm /2 by monotonic_le_plus_r/
408qed.
409
410(*
411axiom blah:
412  ∀instruction: instruction.
413  ∀program_counter': Word.
414  ∀ticks, n: nat.
415  ∀code_memory: BitVectorTrie Byte 16.
416    〈instruction,program_counter',ticks〉 = fetch code_memory (fetch_program_counter_n n code_memory (zero 16)) →
417       program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
418*)   
419
420let rec block_cost
421  (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
422    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
423      (reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter)
424        (good_program_witness: good_program code_memory total_program_size)
425          on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
426  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with
427  [ O ⇒ λbase_case. ⊥
428  | S program_size' ⇒ λrecursive_case.
429    let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
430      match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with
431      [ None   ⇒
432        match instruction return λx. x = instruction → ? with
433        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
434          match real_instruction return λx. x = real_instruction → ? with
435          [ RET                    ⇒ λinstr. ticks
436          | JC   relative          ⇒ λinstr. ticks
437          | JNC  relative          ⇒ λinstr. ticks
438          | JB   bit_addr relative ⇒ λinstr. ticks
439          | JNB  bit_addr relative ⇒ λinstr. ticks
440          | JBC  bit_addr relative ⇒ λinstr. ticks
441          | JZ   relative          ⇒ λinstr. ticks
442          | JNZ  relative          ⇒ λinstr. ticks
443          | CJNE src_trgt relative ⇒ λinstr. ticks
444          | DJNZ src_trgt relative ⇒ λinstr. ticks
445          | _                      ⇒ λinstr.
446              ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
447          ] (refl … real_instruction)
448        | ACALL addr     ⇒ λinstr.
449            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
450        | AJMP  addr     ⇒ λinstr. ticks
451        | LCALL addr     ⇒ λinstr.
452            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
453        | LJMP  addr     ⇒ λinstr. ticks
454        | SJMP  addr     ⇒ λinstr. ticks
455        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
456            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
457        | MOVC  src trgt ⇒ λinstr.
458            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
459        ] (refl … instruction)
460      | Some _ ⇒ ticks
461      ]
462  ].
463  [1:
464    cases reachable_program_counter_witness #_ #hyp
465    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
466    @(le_to_lt_to_lt … base_case hyp)
467  |2:
468    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
469    lapply(good_program_witness program_counter reachable_program_counter_witness)
470      <FETCH normalize nodelta <instr normalize nodelta
471    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #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 * * * * #n'
475    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
476    @(transitive_le
477      total_program_size
478      ((S program_size') + nat_of_bitvector … program_counter)
479      (program_size' + nat_of_bitvector … program_counter') recursive_case)
480    normalize in match (S program_size' + nat_of_bitvector … program_counter);
481    >plus_n_Sm
482    @monotonic_le_plus_r
483    change with (
484      nat_of_bitvector … program_counter <
485        nat_of_bitvector … program_counter')
486    assumption
487  |3:
488    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
489    lapply(good_program_witness program_counter reachable_program_counter_witness)
490      <FETCH normalize nodelta <instr normalize nodelta
491    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
492    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
493    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
494    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
495    #_ #_ #program_counter_lt' #program_counter_lt_tps'
496    %
497    [1:
498      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
499      <FETCH normalize nodelta whd in match ltb; normalize nodelta
500      >(le_to_leb_true … program_counter_lt') %
501    |2:
502      assumption
503    ]
504  |4:
505    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
506    lapply(good_program_witness program_counter reachable_program_counter_witness)
507      <FETCH normalize nodelta <instr normalize nodelta
508    @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
509    * * * * #n'
510    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
511    @(transitive_le
512      total_program_size
513      ((S program_size') + nat_of_bitvector … program_counter)
514      (program_size' + nat_of_bitvector … program_counter') recursive_case)
515    normalize in match (S program_size' + nat_of_bitvector … program_counter);
516    >plus_n_Sm
517    @monotonic_le_plus_r
518    change with (
519      nat_of_bitvector … program_counter <
520        nat_of_bitvector … program_counter')
521    assumption
522  |5:
523    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
524    lapply(good_program_witness program_counter reachable_program_counter_witness)
525      <FETCH normalize nodelta <instr normalize nodelta
526    @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
527    * * * * #n'
528    #_ #_ #program_counter_lt' #program_counter_lt_tps'
529    %
530    [1:
531      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
532      <FETCH normalize nodelta whd in match ltb; normalize nodelta
533      >(le_to_leb_true … program_counter_lt') %
534    |2:
535      assumption
536    ]
537  |6:
538    cases daemon (* XXX *)
539  |7:
540    cases daemon (* XXX *)
541  |8:
542    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
543    lapply(good_program_witness program_counter reachable_program_counter_witness)
544    <FETCH normalize nodelta <instr normalize nodelta
545    try(<real_instruction_refl <instr normalize nodelta) *
546    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
547    @(transitive_le
548      total_program_size
549      ((S program_size') + nat_of_bitvector … program_counter)
550      (program_size' + nat_of_bitvector … program_counter') recursive_case)
551    normalize in match (S program_size' + nat_of_bitvector … program_counter);
552    >plus_n_Sm
553    @monotonic_le_plus_r
554    change with (
555      nat_of_bitvector … program_counter <
556        nat_of_bitvector … program_counter')
557    assumption
558  |9:
559    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
560    lapply(good_program_witness program_counter reachable_program_counter_witness)
561      <FETCH normalize nodelta <instr normalize nodelta *
562    #program_counter_lt' #program_counter_lt_tps' %
563    [1:
564      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
565      <FETCH normalize nodelta whd in match ltb; normalize nodelta
566      >(le_to_leb_true … program_counter_lt') %
567    |2:
568      assumption
569    ]
570  |11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,
571    55,57,59,61,63:
572    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
573    lapply(good_program_witness program_counter reachable_program_counter_witness)
574      <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
575    #program_counter_lt' #program_counter_lt_tps' %
576    [1:
577      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
578      <FETCH normalize nodelta whd in match ltb; normalize nodelta
579      >(le_to_leb_true … program_counter_lt') %
580    |2:
581      assumption
582    ]
583  |10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
584    54,56,58,60,62:
585    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
586    lapply(good_program_witness program_counter reachable_program_counter_witness)
587    <FETCH normalize nodelta
588    <real_instruction_refl <instr normalize nodelta *
589    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
590    @(transitive_le
591      total_program_size
592      ((S program_size') + nat_of_bitvector … program_counter)
593      (program_size' + nat_of_bitvector … program_counter') recursive_case)
594    normalize in match (S program_size' + nat_of_bitvector … program_counter);
595    >plus_n_Sm
596    @monotonic_le_plus_r
597    change with (
598      nat_of_bitvector … program_counter <
599        nat_of_bitvector … program_counter')
600    assumption
601  ]
602qed.
603   
604   
605   
606   
607   
608   
609   
610  [1: (* ACALL *)
611    generalize in match good_program_witness;
612    whd in match good_program; normalize nodelta
613    cases FETCH normalize nodelta
614    cases instr normalize nodelta
615    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
616    cases (split … 8 8 program_counter) #pc_bu #pc_bl normalize nodelta
617    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
618    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
619    #assm cases assm #ignore
620    whd in match good_program_counter; normalize nodelta * #n * *
621    #program_counter_eq #program_counter_lt_total_program_size
622    #fetch_n_leq_program_counter
623    @(transitive_le
624      total_program_size
625      ((S program_size') + nat_of_bitvector … program_counter)
626      (program_size' + nat_of_bitvector … program_counter') recursive_case)
627    normalize in match (S program_size' + nat_of_bitvector … program_counter);
628    >plus_n_Sm
629    @monotonic_le_plus_r
630    change with (
631      nat_of_bitvector … program_counter <
632        nat_of_bitvector … program_counter')
633    >program_counter_eq in FETCH; #hyp
634    >(blah … hyp)
635    <program_counter_eq assumption
636  |2:
637    generalize in match good_program_witness;
638    whd in match good_program; normalize nodelta
639    cases FETCH normalize nodelta
640    cases instr normalize nodelta
641    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
642    cases (split … 8 8 program_counter) #pc_bu #pc_bl normalize nodelta
643    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
644    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
645    #assm cases assm #ignore
646    whd in match good_program_counter; normalize nodelta * #n * *
647    #program_counter_eq #program_counter_lt_total_program_size
648    #fetch_n_leq_program_counter
649
650    whd in match good_program; normalize nodelta
651    @pair_elim #lft #rgt normalize nodelta #fetch_hyp
652    @pair_elim #instruction #program
653  |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
654   54,56,58,60,62:
655  |3: (* LCALL *)
656    generalize in match good_program_witness;
657    whd in match good_program; normalize nodelta
658    cases FETCH normalize nodelta
659    cases instr normalize nodelta
660    @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
661    * #irrelevant
662    whd in match good_program_counter; normalize nodelta * #n * *
663    #program_counter_eq #program_counter_lt_total_program_size
664    #fetch_n_leq_program_counter
665    @(transitive_le
666      total_program_size
667      ((S program_size') + nat_of_bitvector … program_counter)
668      (program_size' + nat_of_bitvector … program_counter') recursive_case)
669    normalize in match (S program_size' + nat_of_bitvector … program_counter);
670    >plus_n_Sm
671    @monotonic_le_plus_r
672    change with (
673      nat_of_bitvector … program_counter <
674        nat_of_bitvector … program_counter')
675    >program_counter_eq in FETCH; #hyp
676    >(blah … hyp)
677    <program_counter_eq assumption
678  |5,7: (* JMP and MOVC *)
679    generalize in match good_program_witness;
680    whd in match good_program; normalize nodelta
681    cases FETCH normalize nodelta
682    cases instr normalize nodelta
683  |9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,
684   49,51,53,55,57,59,61,63: (* ADD and similar non-branching instructions *)
685    generalize in match good_program_witness;
686    whd in match good_program; normalize nodelta
687    cases FETCH normalize nodelta
688    <real_instruction_refl <instr normalize nodelta
689  ]
690    whd in match good_program_counter; normalize nodelta * #n * *
691    #program_counter_eq #program_counter_lt_total_program_size
692    #fetch_n_leq_program_counter
693    @(transitive_le
694      total_program_size
695      (S program_size' + nat_of_bitvector … program_counter)
696      (program_size' + nat_of_bitvector … program_counter')
697      recursive_case)
698    normalize in match (S program_size' + nat_of_bitvector … program_counter);
699    >plus_n_Sm
700    @monotonic_le_plus_r
701    change with (
702      nat_of_bitvector … program_counter <
703        nat_of_bitvector … program_counter')
704    >program_counter_eq in FETCH; #hyp
705    >(blah … hyp)
706    <program_counter_eq assumption
707qed.
708       
709(* XXX: use memoisation here in the future *)
710let rec block_cost
711  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
712    (program_counter: Word) (program_size: nat) (total_program_size: nat)
713      (size_invariant: total_program_size ≤ code_memory_size)
714        (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
715          on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
716  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
717  [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *)
718  | S program_size ⇒ λrecursive_case.
719    let 〈instr, newpc, ticks〉 ≝ fetch … code_memory program_counter in
720      match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
721      [ None ⇒
722          let classify ≝ ASM_classify0 instr in
723          match classify return λx. classify = x → ? with
724          [ cl_jump ⇒ λclassify_refl. ticks
725          | cl_call ⇒ λclassify_refl. (* ite here *)
726              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
727          | cl_return ⇒ λclassify_refl. ticks
728          | cl_other ⇒ λclassify_refl. (* ite here *)
729              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
730          ] (refl … classify)
731        | Some _ ⇒ ticks
732      ]
733  ].
734
735let rec traverse_code_internal
736  (program: list Byte) (mem: BitVectorTrie Byte 16)
737    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
738      on program: identifier_map CostTag nat ≝
739 let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
740 match program with
741 [ nil ⇒ empty_map …
742 | cons hd tl ⇒
743   match lookup_opt … pc cost_labels with
744   [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
745   | Some lbl ⇒
746     let cost ≝ block_cost mem cost_labels pc program_size in
747     let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
748       add … cost_mapping lbl cost ]].
749
750definition traverse_code ≝
751  λprogram: list Byte.
752  λmem: BitVectorTrie Byte 16.
753  λcost_labels.
754  λprogram_size: nat.
755    traverse_code_internal program mem cost_labels (zero …) program_size.
756
757definition compute_costs ≝
758  λprogram: list Byte.
759  λcost_labels: BitVectorTrie costlabel 16.
760  λhas_main: bool.
761  let program_size ≝ |program| + 1 in
762  let memory ≝ load_code_memory program in
763   traverse_code program memory cost_labels program_size.
Note: See TracBrowser for help on using the repository browser.