source: src/ASM/ASMCosts.ma @ 1709

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

Changes to the execution of the MOVC instruction

File size: 69.9 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 well_labelling: BitVectorTrie costlabel 16 → Prop ≝
32  λcost_labels.
33    injective … (λx. lookup_opt … x cost_labels).
34   
35definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
36  λcode_memory: BitVectorTrie Byte 16.
37  λtotal_program_size: nat.
38  ∀program_counter: Word.
39  ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
40  let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
41    match instruction with
42    [ RealInstruction instr ⇒
43      match instr with
44      [ RET                    ⇒ True
45      | JC   relative          ⇒ True (* XXX: see below *)
46      | JNC  relative          ⇒ True (* XXX: see below *)
47      | JB   bit_addr relative ⇒ True
48      | JNB  bit_addr relative ⇒ True
49      | JBC  bit_addr relative ⇒ True
50      | JZ   relative          ⇒ True
51      | JNZ  relative          ⇒ True
52      | CJNE src_trgt relative ⇒ True
53      | DJNZ src_trgt relative ⇒ True
54      | _                      ⇒
55        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
56          nat_of_bitvector … program_counter' < total_program_size
57      ]
58    | LCALL addr         ⇒
59      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
60      [ ADDR16 addr ⇒ λaddr16: True.
61          reachable_program_counter code_memory total_program_size addr ∧
62            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
63              nat_of_bitvector … program_counter' < total_program_size
64      | _ ⇒ λother: False. ⊥
65      ] (subaddressing_modein … addr)
66    | ACALL addr         ⇒
67      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
68      [ ADDR11 addr ⇒ λaddr11: True.
69        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
70        let 〈thr, eig〉 ≝ split … 3 8 addr in
71        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
72        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
73          reachable_program_counter code_memory total_program_size new_program_counter ∧
74            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
75              nat_of_bitvector … program_counter' < total_program_size
76      | _ ⇒ λother: False. ⊥
77      ] (subaddressing_modein … addr)
78    | AJMP  addr         ⇒
79      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
80      [ ADDR11 addr ⇒ λaddr11: True.
81        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
82        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
83        let bit ≝ get_index' … O ? nl in
84        let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
85        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
86        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
87          reachable_program_counter code_memory total_program_size new_program_counter
88      | _ ⇒ λother: False. ⊥
89      ] (subaddressing_modein … addr)
90    | LJMP  addr         ⇒
91      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
92      [ ADDR16 addr ⇒ λaddr16: True.
93          reachable_program_counter code_memory total_program_size addr
94      | _ ⇒ λother: False. ⊥
95      ] (subaddressing_modein … addr)
96    | SJMP  addr     ⇒
97      match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
98      [ RELATIVE addr ⇒ λrelative: True.
99        let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in
100          reachable_program_counter code_memory total_program_size new_program_counter
101      | _ ⇒ λother: False. ⊥
102      ] (subaddressing_modein … addr)
103    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
104      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
105        nat_of_bitvector … program_counter' < total_program_size
106    | MOVC  src trgt ⇒
107        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
108          nat_of_bitvector … program_counter' < total_program_size
109    ].
110  cases other
111qed.
112       
113lemma is_a_decidable:
114  ∀hd.
115  ∀element.
116    is_a hd element = true ∨ is_a hd element = false.
117  #hd #element //
118qed.
119
120lemma mem_decidable:
121  ∀n: nat.
122  ∀v: Vector addressing_mode_tag n.
123  ∀element: addressing_mode_tag.
124    mem … eq_a n v element = true ∨
125      mem … eq_a … v element = false.
126  #n #v #element //
127qed.
128
129lemma eq_a_elim:
130  ∀tag.
131  ∀hd.
132  ∀P: bool → Prop.
133    (tag = hd → P (true)) →
134      (tag ≠ hd → P (false)) →
135        P (eq_a tag hd).
136  #tag #hd #P
137  cases tag
138  cases hd
139  #true_hyp #false_hyp
140  try @false_hyp
141  try @true_hyp
142  try %
143  #absurd destruct(absurd)
144qed.
145 
146lemma is_a_true_to_is_in:
147  ∀n: nat.
148  ∀x: addressing_mode.
149  ∀tag: addressing_mode_tag.
150  ∀supervector: Vector addressing_mode_tag n.
151  mem addressing_mode_tag eq_a n supervector tag →
152    is_a tag x = true →
153      is_in … supervector x.
154  #n #x #tag #supervector
155  elim supervector
156  [1:
157    #absurd cases absurd
158  |2:
159    #n' #hd #tl #inductive_hypothesis
160    whd in match (mem … eq_a (S n') (hd:::tl) tag);
161    @eq_a_elim normalize nodelta
162    [1:
163      #tag_hd_eq #irrelevant
164      whd in match (is_in (S n') (hd:::tl) x);
165      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
166      @I
167    |2:
168      #tag_hd_neq
169      whd in match (is_in (S n') (hd:::tl) x);
170      change with (
171        mem … eq_a n' tl tag)
172          in match (fold_right … n' ? false tl);
173      #mem_hyp #is_a_hyp
174      cases(is_a hd x)
175      [1:
176        normalize nodelta //
177      |2:
178        normalize nodelta
179        @inductive_hypothesis assumption
180      ]
181    ]
182  ]
183qed.
184
185lemma is_in_subvector_is_in_supervector:
186  ∀m, n: nat.
187  ∀subvector: Vector addressing_mode_tag m.
188  ∀supervector: Vector addressing_mode_tag n.
189  ∀element: addressing_mode.
190    subvector_with … eq_a subvector supervector →
191      is_in m subvector element → is_in n supervector element.
192  #m #n #subvector #supervector #element
193  elim subvector
194  [1:
195    #subvector_with_proof #is_in_proof
196    cases is_in_proof
197  |2:
198    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
199    whd in match (is_in … (hd':::tl') element);
200    cases (is_a_decidable hd' element)
201    [1:
202      #is_a_true >is_a_true
203      #irrelevant
204      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
205      @(is_a_true_to_is_in … is_a_true)
206      lapply(subvector_with_proof)
207      cases(mem … eq_a n supervector hd') //
208    |2:
209      #is_a_false >is_a_false normalize nodelta
210      #assm
211      @inductive_hypothesis
212      [1:
213        generalize in match subvector_with_proof;
214        whd in match (subvector_with … eq_a (hd':::tl') supervector);
215        cases(mem_decidable n supervector hd')
216        [1:
217          #mem_true >mem_true normalize nodelta
218          #assm assumption
219        |2:
220          #mem_false >mem_false #absurd
221          cases absurd
222        ]
223      |2:
224        assumption
225      ]
226    ]
227  ]
228qed.
229
230let rec member_addressing_mode_tag
231  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
232    on v: Prop ≝
233  match v with
234  [ VEmpty ⇒ False
235  | VCons n' hd tl ⇒
236      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
237  ].
238 
239let rec subaddressing_mode_elim_type
240  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
241    (Q: addressing_mode → T → Prop)
242      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
243      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
244      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
245      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
246      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
247      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
248      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
249      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
250      (p_dptr:                               is_in m fixed_v DPTR              → T)
251      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
252      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
253      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
254      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
255      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
256      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
257      (p_carry:                              is_in m fixed_v CARRY             → T)
258      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
259      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
260      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
261        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
262      on v: Prop ≝
263  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
264  [ VEmpty         ⇒ λm_refl. λv_refl.
265      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
266        Q addr (
267        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
268        [ ADDR11 x          ⇒ p_addr11 x
269        | ADDR16 x          ⇒ p_addr16 x
270        | DIRECT x          ⇒ p_direct x
271        | INDIRECT x        ⇒ p_indirect x
272        | EXT_INDIRECT x    ⇒ p_ext_indirect x
273        | ACC_A             ⇒ p_acc_a
274        | REGISTER x        ⇒ p_register x
275        | ACC_B             ⇒ p_acc_b
276        | DPTR              ⇒ p_dptr
277        | DATA x            ⇒ p_data x
278        | DATA16 x          ⇒ p_data16 x
279        | ACC_DPTR          ⇒ p_acc_dptr
280        | ACC_PC            ⇒ p_acc_pc
281        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
282        | INDIRECT_DPTR     ⇒ p_indirect_dptr
283        | CARRY             ⇒ p_carry
284        | BIT_ADDR x        ⇒ p_bit_addr x
285        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
286        | RELATIVE x        ⇒ p_relative x
287        ] p)
288  | VCons n' hd tl ⇒ λm_refl. λv_refl.
289    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
290      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
291        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
292          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
293            p_bit_addr p_n_bit_addr p_relative n' tl ?
294    in
295    match hd return λa: addressing_mode_tag. a = hd → ? with
296    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
297    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
298    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
299    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
300    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
301    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
302    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
303    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
304    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
305    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
306    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
307    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
308    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
309    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
310    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
311    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
312    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
313    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
314    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
315    ] (refl … hd)
316  ] (refl … n) (refl_jmeq … v).
317  [20:
318    generalize in match proof; destruct
319    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
320    cases (mem … eq_a m fixed_v hd) normalize nodelta
321    [1:
322      whd in match (subvector_with … eq_a tl fixed_v);
323      #assm assumption
324    |2:
325      normalize in ⊢ (% → ?);
326      #absurd cases absurd
327    ]
328  ]
329  @(is_in_subvector_is_in_supervector … proof)
330  destruct @I
331qed.
332
333(* XXX: todo *)
334lemma subaddressing_mode_elim':
335  ∀T: Type[2].
336  ∀n: nat.
337  ∀o: nat.
338  ∀Q: addressing_mode → T → Prop.
339  ∀fixed_v: Vector addressing_mode_tag (n + o).
340  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
341  ∀v1: Vector addressing_mode_tag n.
342  ∀v2: Vector addressing_mode_tag o.
343  ∀fixed_v_proof: fixed_v = v1 @@ v2.
344  ∀subaddressing_mode_proof.
345    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
346      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
347  #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
348  #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof
349  cases daemon
350qed.
351
352(* XXX: todo *)
353axiom subaddressing_mode_elim:
354  ∀T: Type[2].
355  ∀m: nat.
356  ∀n: nat.
357  ∀Q: addressing_mode → T → Prop.
358  ∀fixed_v: Vector addressing_mode_tag m.
359  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
360  ∀v: Vector addressing_mode_tag n.
361  ∀proof.
362    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
363      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
364
365definition current_instruction_is_labelled ≝
366  λcode_memory.
367  λcost_labels: BitVectorTrie costlabel 16.
368  λs: Status code_memory.
369  let pc ≝ program_counter … code_memory s in
370    match lookup_opt … pc cost_labels with
371    [ None ⇒ False
372    | _    ⇒ True
373    ].
374
375definition next_instruction_properly_relates_program_counters ≝
376  λcode_memory.
377  λbefore: Status code_memory.
378  λafter : Status code_memory.
379  let size ≝ current_instruction_cost code_memory before in
380  let pc_before ≝ program_counter … code_memory before in
381  let pc_after ≝ program_counter … code_memory after in
382  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
383    sum = pc_after.
384
385definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
386  λcode_memory.
387  λcost_labels.
388    mk_abstract_status
389      (Status code_memory)
390      (λs,s'. (execute_1 … s) = s')
391      (λs,class. ASM_classify … s = class)
392      (current_instruction_is_labelled … cost_labels)
393      (next_instruction_properly_relates_program_counters code_memory).
394
395let rec trace_any_label_length
396  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
397    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
398      (final_status: Status code_memory)
399      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
400        on the_trace: nat ≝
401  match the_trace with
402  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
403  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 0
404  | tal_base_return the_status _ _ _ ⇒ 0
405  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
406      let tail_length ≝ trace_any_label_length … final_trace in
407      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
408        pc_difference + tail_length
409  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
410      let tail_length ≝ trace_any_label_length … tail_trace in
411      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
412        pc_difference + tail_length       
413  ].
414
415let rec compute_paid_trace_any_label
416  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
417    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
418      (final_status: Status code_memory)
419        (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
420       on the_trace: nat ≝
421  match the_trace with
422  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
423  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
424  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call
425  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
426     _ _ _ call_trace _ final_trace ⇒
427      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
428      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
429        current_instruction_cost + final_trace_cost
430  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
431      let current_instruction_cost ≝ current_instruction_cost … status_pre in
432      let tail_trace_cost ≝
433       compute_paid_trace_any_label … cost_labels end_flag
434        status_init status_end tail_trace
435      in
436        current_instruction_cost + tail_trace_cost
437  ].
438
439definition compute_paid_trace_label_label ≝
440  λcode_memory: BitVectorTrie Byte 16.
441  λcost_labels: BitVectorTrie costlabel 16.
442  λtrace_ends_flag: trace_ends_with_ret.
443  λstart_status: Status code_memory.
444  λfinal_status: Status code_memory.
445  λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
446  match the_trace with
447  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
448      compute_paid_trace_any_label … given_trace
449  ].
450
451include alias "arithmetics/nat.ma".
452include alias "basics/logic.ma".
453
454lemma plus_right_monotone:
455  ∀m, n, o: nat.
456    m = n → m + o = n + o.
457  #m #n #o #refl >refl %
458qed.
459
460lemma minus_plus_cancel:
461  ∀m, n : nat.
462  ∀proof: n ≤ m.
463    (m - n) + n = m.
464  #m #n #proof /2 by plus_minus/
465qed.
466
467(* XXX: indexing bug *)
468lemma fetch_twice_fetch_execute_1:
469  ∀code_memory: BitVectorTrie Byte 16.
470  ∀start_status: Status code_memory.
471    ASM_classify code_memory start_status = cl_other →
472    \snd (\fst (fetch code_memory (program_counter … start_status))) =
473      program_counter … (execute_1 … start_status).
474  #code_memory #start_status #classify_assm
475  whd in match execute_1; normalize nodelta
476  whd in match execute_1'; normalize nodelta
477  whd in match execute_1_0; normalize nodelta
478  generalize in match (refl … (fetch code_memory
479    (program_counter (BitVectorTrie Byte 16) code_memory start_status)));
480  cases (fetch code_memory
481    (program_counter (BitVectorTrie Byte 16) code_memory start_status)) in ⊢ (??%? → ?);
482  #instr_pc #ticks #fetch_rewrite <fetch_rewrite
483  cases
484qed-.
485
486lemma reachable_program_counter_to_0_lt_total_program_size:
487  ∀code_memory: BitVectorTrie Byte 16.
488  ∀program_counter: Word.
489  ∀total_program_size: nat.
490    reachable_program_counter code_memory total_program_size program_counter →
491      0 < total_program_size.
492  #code_memory #program_counter #total_program_size
493  whd in match reachable_program_counter; normalize nodelta * * #some_n
494  #_ cases (nat_of_bitvector 16 program_counter)
495  [1:
496    #assm assumption
497  |2:
498    #new_pc @ltn_to_ltO
499  ]
500qed.
501
502lemma trace_compute_paid_trace_cl_other:
503  ∀code_memory' : (BitVectorTrie Byte 16).
504  ∀program_counter' : Word.
505  ∀total_program_size : ℕ.
506  ∀cost_labels : (BitVectorTrie costlabel 16).
507  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
508  ∀good_program_witness : (good_program code_memory' total_program_size).
509  ∀program_size' : ℕ.
510  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
511  ∀ticks : ℕ.
512  ∀instruction : instruction.
513  ∀program_counter'' : Word.
514  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
515  ∀start_status : (Status code_memory').
516  ∀final_status : (Status code_memory').
517  ∀trace_ends_flag : trace_ends_with_ret.
518  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
519  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
520  ∀classify_assm: ASM_classify0 instruction = cl_other.
521  ∀pi1 : ℕ.
522   (if match lookup_opt costlabel 16 program_counter'' cost_labels with 
523         [None ⇒ true
524         |Some _ ⇒ false
525         ] 
526    then
527      ∀start_status0:Status code_memory'.
528      ∀final_status0:Status code_memory'.
529      ∀trace_ends_flag0:trace_ends_with_ret.
530      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
531        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
532        (∃n:ℕ
533                    .trace_any_label_length code_memory' cost_labels
534                     trace_ends_flag0 start_status0 final_status0 the_trace0
535                     +S n
536                     =total_program_size)
537                   ∧pi1
538                    =compute_paid_trace_any_label code_memory' cost_labels
539                     trace_ends_flag0 start_status0 final_status0 the_trace0
540    else (pi1=O) )
541   →(∃n:ℕ
542     .trace_any_label_length code_memory' cost_labels trace_ends_flag
543      start_status final_status the_trace
544      +S n
545      =total_program_size)
546    ∧ticks+pi1
547     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
548      start_status final_status the_trace.
549  #code_memory' #program_counter' #total_program_size #cost_labels
550  #reachable_program_counter_witness #good_program_witness
551  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
552  #start_status #final_status
553  #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
554  #recursive_assm
555  @(trace_any_label_inv_ind … the_trace)
556    [5:
557      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
558      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
559      #the_trace_refl
560      destruct
561      whd in match (trace_any_label_length … (tal_step_default …));
562      whd in match (compute_paid_trace_any_label … (tal_step_default …));
563      whd in costed_assm:(?%);
564      generalize in match costed_assm;
565      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
566      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
567        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
568      #lookup_assm cases lookup_assm
569      [1:
570        #None_lookup_opt_assm normalize nodelta #ignore
571        generalize in match recursive_assm;
572        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
573        [1:
574          <fetch_twice_fetch_execute_1 <FETCH %
575        |2:
576          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
577          normalize nodelta #new_recursive_assm
578          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
579            end_flag trace_any_label ?) [2: % ]
580          #exists_assm #recursive_block_cost_assm %
581          [1:
582            cases exists_assm #exists_n #total_program_size_refl
583            <total_program_size_refl
584            %{(exists_n - current_instruction_cost … status_pre)}
585            (* XXX: Christ knows what's going on with the rewrite tactic here? *)
586            cases daemon
587          |2:
588            >recursive_block_cost_assm
589            whd in match (current_instruction_cost … status_pre);
590            cut(ticks = \snd (fetch code_memory'
591               (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
592            [1:
593              <FETCH %
594            |2:
595              #ticks_refl_assm >ticks_refl_assm %
596            ]
597          ]
598        ]
599      |2:
600        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
601        #absurd cases absurd #absurd cases(absurd I)
602      ]
603    |1:
604      #status_start #status_final #execute_assm #classifier_assm #costed_assm
605      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
606      destruct
607      whd in match (trace_any_label_length … (tal_base_not_return …));
608      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
609      whd in costed_assm;
610      generalize in match costed_assm;
611      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
612      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
613        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
614      #lookup_assm cases lookup_assm
615      [1:
616        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
617        #absurd cases absurd
618      |2:
619        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
620        generalize in match recursive_assm;
621        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
622        [1:
623          <fetch_twice_fetch_execute_1 <FETCH %
624        |2:
625          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
626          normalize nodelta #new_recursive_assm >new_recursive_assm %
627          [1:
628            %{(pred total_program_size)} whd in ⊢ (??%?);
629            @S_pred
630            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
631          |2:
632            cut(ticks = \snd (fetch code_memory'
633               (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
634            [1:
635              <FETCH %
636            |2:
637              #ticks_refl_assm >ticks_refl_assm
638              <plus_n_O %
639            ]
640          ]
641        ]
642      ]
643    |2:
644      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
645      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
646    |3:
647      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
648      #classifier_assm #after_return_assm #trace_label_return #costed_assm
649      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
650      destruct @⊥
651    |4:
652      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
653      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
654      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
655      #final_status_refl #the_trace_refl destruct @⊥
656    ]
657  change with (ASM_classify0 ? = ?) in classifier_assm;
658  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
659  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
660  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
661qed.
662
663lemma trace_compute_paid_trace_cl_jump:
664  ∀code_memory': BitVectorTrie Byte 16.
665  ∀program_counter': Word.
666  ∀total_program_size: ℕ.
667  ∀cost_labels: BitVectorTrie costlabel 16.
668  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
669  ∀good_program_witness: good_program code_memory' total_program_size.
670  ∀first_time_around: bool.
671  ∀program_size': ℕ.
672  ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'.
673  ∀ticks: ℕ.
674  ∀instruction: instruction.
675  ∀program_counter'': Word.
676  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
677  ∀start_status: (Status code_memory').
678  ∀final_status: (Status code_memory').
679  ∀trace_ends_flag: trace_ends_with_ret.
680  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
681  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
682  ∀classify_assm: ASM_classify0 instruction = cl_jump.
683   (∃n:ℕ
684     .trace_any_label_length code_memory' cost_labels trace_ends_flag
685      start_status final_status the_trace
686      +S n
687      =total_program_size)
688    ∧ticks
689     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
690      start_status final_status the_trace.
691  #code_memory' #program_counter' #total_program_size #cost_labels
692  #reachable_program_counter_witness #good_program_witness #first_time_around
693  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
694  #start_status #final_status
695  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
696  @(trace_any_label_inv_ind … the_trace)
697  [5:
698    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
699    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
700    #the_trace_refl destruct @⊥
701  |1:
702    #status_start #status_final #execute_assm #classifier_assm #costed_assm
703    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
704    destruct
705    whd in match (trace_any_label_length … (tal_base_not_return …));
706    whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); %
707    [1:
708      %{(pred total_program_size)} whd in ⊢ (??%?);
709      @S_pred
710      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
711    |2:
712      <FETCH %
713    ]
714  |2:
715    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
716    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
717  |3:
718    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
719    #classifier_assm #after_return_assm #trace_label_return #costed_assm
720    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
721    destruct @⊥
722  |4:
723    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
724    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
725    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
726    #final_status_refl #the_trace_refl destruct @⊥
727  ]
728  change with (ASM_classify0 ? = ?) in classifier_assm;
729  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
730  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
731  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
732qed.
733
734lemma trace_compute_paid_trace_cl_call:
735  ∀code_memory' : (BitVectorTrie Byte 16).
736  ∀program_counter' : Word.
737  ∀total_program_size : ℕ.
738  ∀cost_labels : (BitVectorTrie costlabel 16).
739  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
740  ∀good_program_witness : (good_program code_memory' total_program_size).
741  ∀program_size' : ℕ.
742  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
743  ∀ticks : ℕ.
744  ∀instruction : instruction.
745  ∀program_counter'' : Word.
746  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
747  ∀start_status : (Status code_memory').
748  ∀final_status : (Status code_memory').
749  ∀trace_ends_flag : trace_ends_with_ret.
750  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
751  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
752  ∀classify_assm: ASM_classify0 instruction = cl_call.
753  (∀pi1:ℕ
754  .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
755      [None ⇒ true | Some _ ⇒ false] 
756   then (∀start_status0:Status code_memory'
757             .∀final_status0:Status code_memory'
758              .∀trace_ends_flag0:trace_ends_with_ret
759               .∀the_trace0:trace_any_label
760                                        (ASM_abstract_status code_memory' cost_labels)
761                                        trace_ends_flag0 start_status0 final_status0
762                .program_counter''
763                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
764                 →(∃n:ℕ
765                   .trace_any_label_length code_memory' cost_labels trace_ends_flag0
766                    start_status0 final_status0 the_trace0
767                    +S n
768                    =total_program_size)
769                  ∧pi1
770                   =compute_paid_trace_any_label code_memory' cost_labels
771                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
772   else (pi1=O) 
773   →(∃n:ℕ
774     .trace_any_label_length code_memory' cost_labels trace_ends_flag
775      start_status final_status the_trace
776      +S n
777      =total_program_size)
778    ∧ticks+pi1
779     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
780      start_status final_status the_trace).
781  #code_memory' #program_counter' #total_program_size #cost_labels
782  #reachable_program_counter_witness #good_program_witness #program_size'
783  #recursive_case #ticks #instruction #program_counter'' #FETCH
784  #start_status #final_status #trace_ends_flag
785  #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
786  @(trace_any_label_inv_ind … the_trace)
787  [5:
788    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
789    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
790    #the_trace_refl destruct @⊥
791  |1:
792    #status_start #status_final #execute_assm #classifier_assm #costed_assm
793    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
794    destruct @⊥
795  |2:
796    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
797    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
798  |3:
799    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
800    #classifier_assm #after_return_assm #trace_label_return #costed_assm
801    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
802    destruct
803    whd in match (trace_any_label_length … (tal_base_call …));
804    whd in match (compute_paid_trace_any_label … (tal_base_call …));
805    whd in costed_assm;
806    generalize in match costed_assm;
807    generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
808    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
809      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
810    #lookup_assm cases lookup_assm
811    [1:
812      #None_lookup_opt normalize nodelta #absurd cases absurd
813    |2:
814      #costlabel #Some_lookup_opt normalize nodelta #ignore
815      generalize in match recursive_assm;
816      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
817      [1:
818        whd in after_return_assm; <after_return_assm; (* XXX: here *)
819        cases daemon
820      |2:
821        #program_counter_assm >program_counter_assm <Some_lookup_opt
822        normalize nodelta #new_recursive_assm >new_recursive_assm %
823        [1:
824          %{(pred total_program_size)} whd in ⊢ (??%?);
825          @S_pred
826          @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
827        |2:
828          cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
829          [1:
830            <FETCH %
831          |2:
832            #ticks_refl_assm >ticks_refl_assm
833            <plus_n_O %
834          ]
835        ]
836      ]
837    ]
838  |4:
839    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
840    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
841    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
842    #final_status_refl #the_trace_refl destruct
843    whd in match (trace_any_label_length … (tal_step_call …));
844    whd in match (compute_paid_trace_any_label … (tal_step_call …));
845    whd in costed_assm:(?%);
846    generalize in match costed_assm;
847    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
848    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
849      in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
850    #lookup_assm cases lookup_assm
851    [1:
852      #None_lookup_opt_assm normalize nodelta #ignore
853      generalize in match recursive_assm;
854      cut(program_counter'' = program_counter … status_after_fun_call)
855      [1:
856        cases daemon
857      |2:
858        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
859        normalize nodelta #new_recursive_assm %
860        cases (new_recursive_assm … trace_any_label ?)
861        [1,3:
862          #exists_assm #recursive_block_cost_assm
863          [2:
864            >recursive_block_cost_assm
865            @plus_right_monotone
866            whd in ⊢ (???%); <FETCH %
867          |1:
868            (*
869            cases exists_assm #recursive_n #new_exists_assm
870            <new_exists_assm
871           
872            %
873            [1:
874              @(recursive_n - current_instruction_cost … status_pre_fun_call)
875            |2:
876             
877              cut(current_instruction_cost … status_pre_fun_call =
878                (nat_of_bitvector 16
879  (program_counter (BitVectorTrie Byte 16) code_memory' status_after_fun_call)
880  -nat_of_bitvector 16
881   (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
882              [1:
883              |2:
884                #eq_assm <eq_assm -eq_assm -new_exists_assm -recursive_block_cost_assm
885                <plus_n_Sm <plus_n_Sm @eq_f
886                >associative_plus in ⊢ (??%?); >commutative_plus in ⊢ (??%?);
887                >associative_plus @eq_f
888                <plus_minus_m_m [1: % ]
889              ]
890            ] *)
891            cases daemon
892          ]
893        |2,4:
894          %
895        ]
896      ]
897    |2:
898      #cost_label #Some_lookup_opt_assm normalize nodelta #absurd
899      cases absurd #absurd cases (absurd I)
900    ]
901  ]
902  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
903  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
904  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
905  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
906  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
907  #absurd destruct(absurd)
908qed.
909
910let rec block_cost'
911  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
912    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
913      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
914        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
915          on program_size:
916          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
917          Σcost_of_block: nat.
918          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
919            ∀start_status: Status code_memory'.
920            ∀final_status: Status code_memory'.
921            ∀trace_ends_flag.
922            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
923              program_counter' = program_counter … start_status →
924                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
925                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
926          else
927            (cost_of_block = 0) ≝
928  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
929  [ O ⇒ λbase_case. ⊥
930  | S program_size' ⇒ λrecursive_case.
931    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
932    let to_continue ≝
933      match lookup_opt … program_counter' cost_labels with
934      [ None ⇒ true
935      | Some _ ⇒ first_time_around
936      ]
937    in
938      ((if to_continue then
939       pi1 … (match instruction return λx. x = instruction → ? with
940        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
941          match real_instruction return λx. x = real_instruction →
942          Σcost_of_block: nat.
943            ∀start_status: Status code_memory'.
944            ∀final_status: Status code_memory'.
945            ∀trace_ends_flag.
946            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
947              program_counter' = program_counter … start_status →
948                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
949                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
950          [ RET                    ⇒ λinstr. ticks
951          | JC   relative          ⇒ λinstr. ticks
952          | JNC  relative          ⇒ λinstr. ticks
953          | JB   bit_addr relative ⇒ λinstr. ticks
954          | JNB  bit_addr relative ⇒ λinstr. ticks
955          | JBC  bit_addr relative ⇒ λinstr. ticks
956          | JZ   relative          ⇒ λinstr. ticks
957          | JNZ  relative          ⇒ λinstr. ticks
958          | CJNE src_trgt relative ⇒ λinstr. ticks
959          | DJNZ src_trgt relative ⇒ λinstr. ticks
960          | _                      ⇒ λinstr.
961         
962              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
963          ] (refl …)
964        | ACALL addr     ⇒ λinstr.
965            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
966        | AJMP  addr     ⇒ λinstr. ticks
967        | LCALL addr     ⇒ λinstr.
968            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
969        | LJMP  addr     ⇒ λinstr. ticks
970        | SJMP  addr     ⇒ λinstr. ticks
971        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
972            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
973        | MOVC  src trgt ⇒ λinstr.
974            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
975        ] (refl …))
976      else
977        0)
978      : Σcost_of_block: nat.
979          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
980          [ true ⇒
981            ∀start_status: Status code_memory'.
982            ∀final_status: Status code_memory'.
983            ∀trace_ends_flag.
984            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
985              program_counter' = program_counter … start_status →
986                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
987                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
988          | false ⇒
989            (cost_of_block = 0)
990          ])
991  ].
992  cases daemon (*
993  [1:
994    cases reachable_program_counter_witness #_ #hyp
995    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
996    @(le_to_lt_to_lt … base_case hyp)
997  |2:
998    change with (if to_continue then ? else (? = 0))
999    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
1000    @pi2
1001  |3:
1002    change with (if to_continue then ? else (0 = 0))
1003    >p normalize nodelta %
1004  |98,104,107:
1005    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1006    cases(block_cost' ?????????) -block_cost'
1007    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
1008    destruct %
1009  |4,7,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
1010   92,95:
1011    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1012    cases(block_cost' ?????????) -block_cost'
1013    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
1014    destruct %
1015  |62,63,64,65,66,67,68,69,101,102,103:
1016    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1017    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
1018    destruct %
1019  |96,99:
1020    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1021    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1022    <FETCH normalize nodelta <instr normalize nodelta *
1023    #program_counter_lt' #program_counter_lt_tps' %
1024    [1,3:
1025      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1026      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1027      >(le_to_leb_true … program_counter_lt') %
1028    |2,4:
1029      assumption
1030    ]
1031  |105:
1032    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1033    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1034    <FETCH normalize nodelta <instr normalize nodelta
1035    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1036    * * * * #n'
1037    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1038    %
1039    [1:
1040      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1041      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1042      >(le_to_leb_true … program_counter_lt') %
1043    |2:
1044      assumption
1045    ]
1046  |106:
1047    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1048    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1049    <FETCH normalize nodelta <instr normalize nodelta
1050    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1051    * * * * #n'
1052    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1053    @(transitive_le
1054      total_program_size
1055      ((S program_size') + nat_of_bitvector … program_counter')
1056      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1057    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1058    >plus_n_Sm
1059    @monotonic_le_plus_r
1060    change with (
1061      nat_of_bitvector … program_counter' <
1062        nat_of_bitvector … program_counter'')
1063    assumption
1064  |108:
1065    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1066    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1067    <FETCH normalize nodelta <instr normalize nodelta
1068    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1069    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1070    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1071    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1072    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1073    %
1074    [1:
1075      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1076      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1077      >(le_to_leb_true … program_counter_lt') %
1078    |2:
1079      assumption
1080    ]
1081  |109:
1082    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1083    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1084    <FETCH normalize nodelta <instr normalize nodelta
1085    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1086    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1087    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1088    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1089    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1090    @(transitive_le
1091      total_program_size
1092      ((S program_size') + nat_of_bitvector … program_counter')
1093      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1094    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1095    >plus_n_Sm
1096    @monotonic_le_plus_r
1097    change with (
1098      nat_of_bitvector … program_counter' <
1099        nat_of_bitvector … program_counter'')
1100    assumption
1101  |5,8,12,14,15,18,20,21,24,27,30,33,36,39,42,45,48,51,54,57,60,72,75,
1102   78,81,84,87,90,93:
1103    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1104    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1105    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1106    #program_counter_lt' #program_counter_lt_tps' %
1107    try assumption
1108    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1109    <FETCH normalize nodelta whd in match ltb; normalize nodelta
1110    >(le_to_leb_true … program_counter_lt') %
1111  |6,9,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,73,76,79,82,85,88,91,
1112   94:
1113    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1114    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1115    <FETCH normalize nodelta
1116    <real_instruction_refl <instr normalize nodelta *
1117    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1118    @(transitive_le
1119      total_program_size
1120      ((S program_size') + nat_of_bitvector … program_counter')
1121      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1122    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1123    >plus_n_Sm
1124    @monotonic_le_plus_r
1125    change with (
1126      nat_of_bitvector … program_counter' <
1127        nat_of_bitvector … program_counter'')
1128    assumption
1129  |10:
1130    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1131    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
1132      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
1133    [1:
1134      #recursive_block_cost #recursive_assm
1135      @(trace_any_label_inv_ind … the_trace)
1136      [1:
1137        #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
1138        #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1139        destruct @⊥
1140      |2:
1141        #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
1142        #start_status_refl #final_status_refl #the_trace_refl destruct
1143        whd in match (trace_any_label_length … (tal_base_return …));
1144        whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
1145        [1:
1146          %{(pred total_program_size)} whd in ⊢ (??%?);
1147          @S_pred
1148          @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
1149        |2:
1150          <FETCH %
1151        ]
1152      |3:
1153        #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
1154        #classifier_assm #after_return_assm #trace_label_return #costed_assm
1155        #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1156        destruct @⊥
1157      |4:
1158        #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1159        #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
1160        #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
1161        #final_status_refl #the_trace_refl
1162        destruct @⊥
1163      |5:
1164        #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
1165        #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
1166        #final_status_refl #the_trace_refl destruct @⊥
1167      ]
1168      try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
1169      try (change with (ASM_classify0 ? = ?) in classifier_assm;)
1170      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1171      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1172      <FETCH in classifier_assm;
1173      try(whd in ⊢ ((??%?) → ?); #absurd destruct(absurd))
1174      whd in ⊢ (?(??%?)(??%?) → ?); #absurd
1175      cases absurd #absurd destruct(absurd)
1176    |2:
1177      cases daemon (* XXX: ??? *)
1178    ]
1179  |62,63,64,65,66,67,68,69,70,101,102,103:
1180    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1181    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
1182      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
1183    try (@(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl …) destruct %)
1184    cases daemon (* XXX: ???, same as above case *)
1185  |96,99:
1186    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1187    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1188    <FETCH normalize nodelta <instr normalize nodelta *
1189    #program_counter_lt' #program_counter_lt_tps' %
1190    [1,3:
1191      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1192      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1193      >(le_to_leb_true … program_counter_lt') %
1194    |2,4:
1195      assumption
1196    ]
1197  |98,104,107:
1198    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1199    cases(block_cost' ?????????) -block_cost'
1200    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness first_time_around … recursive_case … FETCH … the_trace program_counter_refl …)
1201    destruct %
1202  |105:
1203    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1204    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1205    <FETCH normalize nodelta <instr normalize nodelta
1206    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1207    * * * * #n'
1208    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1209    %
1210    [1:
1211      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1212      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1213      >(le_to_leb_true … program_counter_lt') %
1214    |2:
1215      assumption
1216    ]
1217  |106:
1218    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1219    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1220    <FETCH normalize nodelta <instr normalize nodelta
1221    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1222    * * * * #n'
1223    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1224    @(transitive_le
1225      total_program_size
1226      ((S program_size') + nat_of_bitvector … program_counter')
1227      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1228    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1229    >plus_n_Sm
1230    @monotonic_le_plus_r
1231    change with (
1232      nat_of_bitvector … program_counter' <
1233        nat_of_bitvector … program_counter'')
1234    assumption
1235  |108:
1236    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1237    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1238    <FETCH normalize nodelta <instr normalize nodelta
1239    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1240    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1241    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1242    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1243    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1244    %
1245    [1:
1246      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1247      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1248      >(le_to_leb_true … program_counter_lt') %
1249    |2:
1250      assumption
1251    ]
1252  |109:
1253    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1254    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1255    <FETCH normalize nodelta <instr normalize nodelta
1256    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1257    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1258    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1259    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1260    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1261    @(transitive_le
1262      total_program_size
1263      ((S program_size') + nat_of_bitvector … program_counter')
1264      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1265    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1266    >plus_n_Sm
1267    @monotonic_le_plus_r
1268    change with (
1269      nat_of_bitvector … program_counter' <
1270        nat_of_bitvector … program_counter'')
1271    assumption
1272  |97,100:
1273    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1274    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1275    <FETCH normalize nodelta <instr normalize nodelta
1276    try(<real_instruction_refl <instr normalize nodelta) *
1277    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1278    @(transitive_le
1279      total_program_size
1280      ((S program_size') + nat_of_bitvector … program_counter')
1281      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1282    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1283    >plus_n_Sm
1284    @monotonic_le_plus_r
1285    change with (
1286      nat_of_bitvector … program_counter' <
1287        nat_of_bitvector … program_counter'')
1288    assumption
1289  ] *)
1290qed.
1291
1292(*
1293  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
1294    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
1295      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
1296        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
1297          on program_size:
1298          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
1299          Σcost_of_block: nat.
1300          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
1301            ∀start_status: Status code_memory'.
1302            ∀final_status: Status code_memory'.
1303            ∀trace_ends_flag.
1304            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1305              program_counter' = program_counter … start_status →
1306                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1307                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
1308          else
1309            (cost_of_block = 0)
1310*)
1311
1312definition block_cost:
1313    ∀code_memory': BitVectorTrie Byte 16.
1314    ∀program_counter': Word.
1315    ∀total_program_size: nat.
1316    ∀cost_labels: BitVectorTrie costlabel 16.
1317    ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
1318    ∀good_program_witness: good_program code_memory' total_program_size.
1319      Σcost_of_block: nat.
1320        ∀start_status: Status code_memory'.
1321        ∀final_status: Status code_memory'.
1322        ∀trace_ends_flag.
1323        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1324          program_counter' = program_counter … start_status →
1325            (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1326              cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
1327  λcode_memory: BitVectorTrie Byte 16.
1328  λprogram_counter: Word.
1329  λtotal_program_size: nat.
1330  λcost_labels: BitVectorTrie costlabel 16.
1331  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
1332  λgood_program_witness: good_program code_memory total_program_size. ?.
1333  cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
1334    reachable_program_counter_witness good_program_witness true ?)
1335  [1:
1336    #cost_of_block #block_cost_hyp
1337    %{cost_of_block}
1338    cases(lookup_opt … cost_labels) in block_cost_hyp;
1339    [2: #cost_label] normalize nodelta
1340    #hyp assumption
1341  |2:
1342    @le_plus_n_r
1343  ]
1344qed.
1345
1346lemma fetch_program_counter_n_Sn:
1347  ∀instruction: instruction.
1348  ∀program_counter, program_counter': Word.
1349  ∀ticks, n: nat.
1350  ∀code_memory: BitVectorTrie Byte 16.
1351    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
1352      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
1353        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
1354          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
1355  #instruction #program_counter #program_counter' #ticks #n #code_memory
1356  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
1357  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
1358  <fetch_program_counter_n_hyp normalize nodelta
1359  <fetch_hyp normalize nodelta
1360  change with (
1361    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
1362  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
1363  >(le_to_leb_true … lt_hyp) %
1364qed.
1365
1366(* XXX: to be moved into common/Identifiers.ma *)
1367lemma lookup_present_add_hit:
1368  ∀tag, A, map, k, v, k_pres.
1369    lookup_present tag A (add … map k v) k k_pres = v.
1370  #tag #a #map #k #v #k_pres
1371  lapply (lookup_lookup_present … (add … map k v) … k_pres)
1372  >lookup_add_hit #Some_assm destruct(Some_assm)
1373  <e0 %
1374qed.
1375
1376lemma lookup_present_add_miss:
1377  ∀tag, A, map, k, k', v, k_pres', k_pres''.
1378    k' ≠ k →
1379      lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
1380  #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
1381  lapply (lookup_lookup_present … (add … map k v) ? k_pres')
1382  >lookup_add_miss try assumption
1383  #Some_assm
1384  lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
1385  lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
1386qed.
1387
1388(* XXX: to be moved into basics/types.ma *)
1389lemma not_None_to_Some:
1390  ∀A: Type[0].
1391  ∀o: option A.
1392    o ≠ None A → ∃v: A. o = Some A v.
1393  #A #o cases o
1394  [1:
1395    #absurd cases absurd #absurd' cases (absurd' (refl …))
1396  |2:
1397    #v' #ignore /2/
1398  ]
1399qed.
1400
1401lemma present_add_present:
1402  ∀tag, a, map, k, k', v.
1403    k' ≠ k →
1404      present tag a (add tag a map k v) k' →
1405        present tag a map k'.
1406  #tag #a #map #k #k' #v #neq_hyp #present_hyp
1407  whd in match present; normalize nodelta
1408  whd in match present in present_hyp; normalize nodelta in present_hyp;
1409  cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
1410  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
1411  [1:
1412    * #k_eq_hyp @⊥ /2/
1413  |2:
1414    #Some_eq_hyp' /2/
1415  ]
1416qed.
1417
1418lemma present_add_hit:
1419  ∀tag, a, map, k, v.
1420    present tag a (add tag a map k v) k.
1421  #tag #a #map #k #v
1422  whd >lookup_add_hit
1423  % #absurd destruct
1424qed.
1425
1426lemma present_add_miss:
1427  ∀tag, a, map, k, k', v.
1428    k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
1429  #tag #a #map #k #k' #v #neq_assm #present_assm
1430  whd >lookup_add_miss assumption
1431qed.
1432
1433let rec traverse_code_internal
1434  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
1435    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
1436      (reachable_program_counter_witness:
1437          ∀lbl: costlabel.
1438          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1439            reachable_program_counter code_memory fixed_program_size program_counter)
1440        (good_program_witness: good_program code_memory fixed_program_size)
1441        on program_size:
1442          Σcost_map: identifier_map CostTag nat.
1443            (∀pc,k. nat_of_bitvector … program_counter < nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
1444            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
1445              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
1446                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
1447  match program_size with
1448  [ O ⇒ empty_map …
1449  | S program_size' ⇒ pi1 …
1450 
1451    (let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in
1452    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size' ? good_program_witness in
1453    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
1454    [ None ⇒ λlookup_refl. pi1 … cost_mapping
1455    | Some lbl ⇒ λlookup_refl.
1456      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
1457        add … cost_mapping lbl cost
1458    ] (refl … (lookup_opt … program_counter cost_labels)))
1459  ].
1460  [2:
1461    @pi2
1462  |4:
1463    @(reachable_program_counter_witness lbl)
1464    assumption
1465  |3:
1466    assumption
1467  |1:
1468    %
1469    [1:
1470      #pc #k #absurd1 #absurd2
1471      @⊥ lapply(lt_to_not_le … absurd1) #absurd
1472      cases absurd #absurd @absurd
1473      @(transitive_le … absurd2) @le_S @le_n
1474    |2:
1475      #k #k_pres
1476      @⊥ normalize in k_pres; /2/
1477    ]
1478  |5:
1479    %
1480    [2:
1481      #k #k_pres
1482      @(eq_identifier_elim … k lbl)
1483      [1:
1484        #eq_assm %{program_counter} #lookup_opt_assm
1485        %{(reachable_program_counter_witness …)} try assumption
1486        >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
1487      |2:
1488        #neq_assm
1489        cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
1490        cases ind_hyp #_ #relevant cases (relevant k ?)
1491        [2:
1492          @(present_add_present … present_assm) assumption
1493        |1:
1494          #program_counter' #ind_hyp' %{program_counter'}
1495          #relevant cases (ind_hyp' relevant) #reachable_witness'
1496          #ind_hyp'' %{reachable_witness'} >ind_hyp''
1497          @sym_eq @lookup_present_add_miss assumption
1498        ]
1499      ]
1500    |1:
1501      #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
1502      [1:
1503        #eq_assm >eq_assm
1504        cases cost_mapping #cost_mapping' * #ind_hyp #_
1505        @present_add_hit
1506      |2:
1507        #neq_assm @present_add_miss try assumption
1508        cases cost_mapping #cost_mapping' * #ind_hyp #_
1509        cases daemon (* XXX: !!! *)
1510      ]
1511    ]
1512  |6:
1513  ]
1514qed.
1515
1516definition traverse_code:
1517  ∀code_memory: BitVectorTrie Byte 16.
1518  ∀cost_labels: BitVectorTrie costlabel 16.
1519  ∀program_size: nat.
1520  ∀reachable_program_counter_witness:
1521    ∀lbl: costlabel.
1522    ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1523      reachable_program_counter code_memory program_size program_counter.
1524  ∀good_program_witness: good_program code_memory program_size.
1525    Σcost_map: identifier_map CostTag nat.
1526      (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
1527        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
1528          pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
1529  λcode_memory: BitVectorTrie Byte 16.
1530  λcost_labels: BitVectorTrie costlabel 16.
1531  λprogram_size: nat.
1532  λreachable_program_counter_witness:
1533          ∀lbl: costlabel.
1534          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1535            reachable_program_counter code_memory program_size program_counter.
1536  λgood_program_witness: good_program code_memory program_size.
1537    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
1538 
1539definition compute_costs ≝
1540  λprogram: list Byte.
1541  λcost_labels: BitVectorTrie costlabel 16.
1542  λreachable_program_witness.
1543  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
1544    let program_size ≝ |program| + 1 in
1545    let code_memory ≝ load_code_memory program in
1546      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
1547  @good_program_witness
1548qed.
Note: See TracBrowser for help on using the repository browser.