source: src/ASM/ASMCosts.ma @ 1648

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

new version of utilities/monad.ma with typecheck command comented out

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