source: src/ASM/ASMCosts.ma @ 1663

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

old cases working again, work on new ones

File size: 46.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 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_a_decidable:
110  ∀hd.
111  ∀element.
112    is_a hd element = true ∨ is_a hd element = false.
113  #hd #element //
114qed.
115
116lemma mem_decidable:
117  ∀n: nat.
118  ∀v: Vector addressing_mode_tag n.
119  ∀element: addressing_mode_tag.
120    mem … eq_a n v element = true ∨
121      mem … eq_a … v element = false.
122  #n #v #element //
123qed.
124
125lemma eq_a_elim:
126  ∀tag.
127  ∀hd.
128  ∀P: bool → Prop.
129    (tag = hd → P (true)) →
130      (tag ≠ hd → P (false)) →
131        P (eq_a tag hd).
132  #tag #hd #P
133  cases tag
134  cases hd
135  #true_hyp #false_hyp
136  try @false_hyp
137  try @true_hyp
138  try %
139  #absurd destruct(absurd)
140qed.
141 
142lemma is_a_true_to_is_in:
143  ∀n: nat.
144  ∀x: addressing_mode.
145  ∀tag: addressing_mode_tag.
146  ∀supervector: Vector addressing_mode_tag n.
147  mem addressing_mode_tag eq_a n supervector tag →
148    is_a tag x = true →
149      is_in … supervector x.
150  #n #x #tag #supervector
151  elim supervector
152  [1:
153    #absurd cases absurd
154  |2:
155    #n' #hd #tl #inductive_hypothesis
156    whd in match (mem … eq_a (S n') (hd:::tl) tag);
157    @eq_a_elim normalize nodelta
158    [1:
159      #tag_hd_eq #irrelevant
160      whd in match (is_in (S n') (hd:::tl) x);
161      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
162      @I
163    |2:
164      #tag_hd_neq
165      whd in match (is_in (S n') (hd:::tl) x);
166      change with (
167        mem … eq_a n' tl tag)
168          in match (fold_right … n' ? false tl);
169      #mem_hyp #is_a_hyp
170      cases(is_a hd x)
171      [1:
172        normalize nodelta //
173      |2:
174        normalize nodelta
175        @inductive_hypothesis assumption
176      ]
177    ]
178  ]
179qed.
180
181lemma is_in_subvector_is_in_supervector:
182  ∀m, n: nat.
183  ∀subvector: Vector addressing_mode_tag m.
184  ∀supervector: Vector addressing_mode_tag n.
185  ∀element: addressing_mode.
186    subvector_with … eq_a subvector supervector →
187      is_in m subvector element → is_in n supervector element.
188  #m #n #subvector #supervector #element
189  elim subvector
190  [1:
191    #subvector_with_proof #is_in_proof
192    cases is_in_proof
193  |2:
194    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
195    whd in match (is_in … (hd':::tl') element);
196    cases (is_a_decidable hd' element)
197    [1:
198      #is_a_true >is_a_true
199      #irrelevant
200      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
201      @(is_a_true_to_is_in … is_a_true)
202      lapply(subvector_with_proof)
203      cases(mem … eq_a n supervector hd') //
204    |2:
205      #is_a_false >is_a_false normalize nodelta
206      #assm
207      @inductive_hypothesis
208      [1:
209        generalize in match subvector_with_proof;
210        whd in match (subvector_with … eq_a (hd':::tl') supervector);
211        cases(mem_decidable n supervector hd')
212        [1:
213          #mem_true >mem_true normalize nodelta
214          #assm assumption
215        |2:
216          #mem_false >mem_false #absurd
217          cases absurd
218        ]
219      |2:
220        assumption
221      ]
222    ]
223  ]
224qed.
225
226let rec member_addressing_mode_tag
227  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
228    on v: Prop ≝
229  match v with
230  [ VEmpty ⇒ False
231  | VCons n' hd tl ⇒
232      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
233  ].
234 
235let rec subaddressing_mode_elim_type
236  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
237    (Q: addressing_mode → T → Prop)
238      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
239      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
240      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
241      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
242      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
243      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
244      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
245      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
246      (p_dptr:                               is_in m fixed_v DPTR              → T)
247      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
248      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
249      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
250      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
251      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
252      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
253      (p_carry:                              is_in m fixed_v CARRY             → T)
254      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
255      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
256      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
257        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
258      on v: Prop ≝
259  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
260  [ VEmpty         ⇒ λm_refl. λv_refl.
261      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
262        Q addr (
263        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
264        [ ADDR11 x          ⇒ p_addr11 x
265        | ADDR16 x          ⇒ p_addr16 x
266        | DIRECT x          ⇒ p_direct x
267        | INDIRECT x        ⇒ p_indirect x
268        | EXT_INDIRECT x    ⇒ p_ext_indirect x
269        | ACC_A             ⇒ p_acc_a
270        | REGISTER x        ⇒ p_register x
271        | ACC_B             ⇒ p_acc_b
272        | DPTR              ⇒ p_dptr
273        | DATA x            ⇒ p_data x
274        | DATA16 x          ⇒ p_data16 x
275        | ACC_DPTR          ⇒ p_acc_dptr
276        | ACC_PC            ⇒ p_acc_pc
277        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
278        | INDIRECT_DPTR     ⇒ p_indirect_dptr
279        | CARRY             ⇒ p_carry
280        | BIT_ADDR x        ⇒ p_bit_addr x
281        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
282        | RELATIVE x        ⇒ p_relative x
283        ] p)
284  | VCons n' hd tl ⇒ λm_refl. λv_refl.
285    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
286      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
287        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
288          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
289            p_bit_addr p_n_bit_addr p_relative n' tl ?
290    in
291    match hd return λa: addressing_mode_tag. a = hd → ? with
292    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
293    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
294    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
295    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
296    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
297    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
298    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
299    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
300    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
301    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
302    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
303    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
304    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
305    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
306    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
307    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
308    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
309    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
310    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
311    ] (refl … hd)
312  ] (refl … n) (refl_jmeq … v).
313  [20:
314    generalize in match proof; destruct
315    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
316    cases (mem … eq_a m fixed_v hd) normalize nodelta
317    [1:
318      whd in match (subvector_with … eq_a tl fixed_v);
319      #assm assumption
320    |2:
321      normalize in ⊢ (% → ?);
322      #absurd cases absurd
323    ]
324  ]
325  @(is_in_subvector_is_in_supervector … proof)
326  destruct @I
327qed.
328
329lemma subaddressing_mode_elim':
330  ∀T: Type[2].
331  ∀n: nat.
332  ∀o: nat.
333  ∀Q: addressing_mode → T → Prop.
334  ∀fixed_v: Vector addressing_mode_tag (n + o).
335  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
336  ∀v1: Vector addressing_mode_tag n.
337  ∀v2: Vector addressing_mode_tag o.
338  ∀fixed_v_proof: fixed_v = v1 @@ v2.
339  ∀subaddressing_mode_proof.
340    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
341      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
342  #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
343  #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof
344  cases daemon
345qed.
346
347axiom subaddressing_mode_elim:
348  ∀T: Type[2].
349  ∀m: nat.
350  ∀n: nat.
351  ∀Q: addressing_mode → T → Prop.
352  ∀fixed_v: Vector addressing_mode_tag m.
353  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
354  ∀v: Vector addressing_mode_tag n.
355  ∀proof.
356    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
357      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
358
359definition current_instruction0 ≝
360  λcode_memory: BitVectorTrie Byte 16.
361  λprogram_counter: Word.
362    \fst (\fst (fetch … code_memory program_counter)).
363
364definition current_instruction ≝
365  λs: Status.
366    current_instruction0 (code_memory … s) (program_counter … s).
367
368definition ASM_classify0: instruction → status_class ≝
369  λi: instruction.
370  match i with
371   [ RealInstruction pre ⇒
372     match pre with
373      [ RET ⇒ cl_return
374      | JZ _ ⇒ cl_jump
375      | JNZ _ ⇒ cl_jump
376      | JC _ ⇒ cl_jump
377      | JNC _ ⇒ cl_jump
378      | JB _ _ ⇒ cl_jump
379      | JNB _ _ ⇒ cl_jump
380      | JBC _ _ ⇒ cl_jump
381      | CJNE _ _ ⇒ cl_jump
382      | DJNZ _ _ ⇒ cl_jump
383      | _ ⇒ cl_other
384      ]
385   | ACALL _ ⇒ cl_call
386   | LCALL _ ⇒ cl_call
387   | JMP _ ⇒ cl_call
388   | AJMP _ ⇒ cl_jump
389   | LJMP _ ⇒ cl_jump
390   | SJMP _ ⇒ cl_jump
391   | _ ⇒ cl_other
392   ].
393
394definition ASM_classify: Status → status_class ≝
395  λs: Status.
396    ASM_classify0 (current_instruction s).
397
398definition current_instruction_is_labelled ≝
399  λcost_labels: BitVectorTrie costlabel 16.
400  λs: Status.
401  let pc ≝ program_counter … s in
402    match lookup_opt … pc cost_labels with
403    [ None ⇒ False
404    | _    ⇒ True
405    ].
406
407definition next_instruction_properly_relates_program_counters ≝
408  λbefore: Status.
409  λafter : Status.
410  let size ≝ current_instruction_cost before in
411  let pc_before ≝ program_counter … before in
412  let pc_after ≝ program_counter … after in
413  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
414    sum = pc_after.
415
416definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
417 λcost_labels.
418  mk_abstract_status
419   Status
420   (λs,s'. (execute_1 s) = s')
421   (λs,class. ASM_classify s = class)
422   (current_instruction_is_labelled cost_labels)
423   next_instruction_properly_relates_program_counters.
424
425let rec trace_any_label_length
426  (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
427    (start_status: Status) (final_status: Status)
428      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
429        on the_trace: nat ≝
430  match the_trace with
431  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
432  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 0
433  | tal_base_return the_status _ _ _ ⇒ 0
434  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
435      let tail_length ≝ trace_any_label_length … final_trace in
436      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
437        pc_difference + tail_length
438  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
439      let tail_length ≝ trace_any_label_length … tail_trace in
440      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
441        pc_difference + tail_length       
442  ].
443
444let rec compute_paid_trace_any_label
445  (cost_labels: BitVectorTrie costlabel 16)
446  (trace_ends_flag: trace_ends_with_ret)
447   (start_status: Status) (final_status: Status)
448     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
449       on the_trace: nat ≝
450  match the_trace with
451  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
452  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
453  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost pre_fun_call
454  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
455     _ _ _ call_trace _ final_trace ⇒
456      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
457      let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
458        current_instruction_cost + final_trace_cost
459  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
460      let current_instruction_cost ≝ current_instruction_cost status_pre in
461      let tail_trace_cost ≝
462       compute_paid_trace_any_label cost_labels end_flag
463        status_init status_end tail_trace
464      in
465        current_instruction_cost + tail_trace_cost
466  ].
467
468definition compute_paid_trace_label_label ≝
469 λcost_labels: BitVectorTrie costlabel 16.
470  λtrace_ends_flag: trace_ends_with_ret.
471   λstart_status: Status.
472    λfinal_status: Status.
473     λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
474      start_status final_status.
475  match the_trace with
476  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
477      compute_paid_trace_any_label … given_trace
478  ].
479
480include alias "arithmetics/nat.ma".
481include alias "basics/logic.ma".
482
483lemma plus_right_monotone:
484  ∀m, n, o: nat.
485    m = n → m + o = n + o.
486  #m #n #o #refl >refl %
487qed.
488
489let rec block_cost'
490  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
491    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
492      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
493        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
494          on program_size:
495          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
496          Σcost_of_block: nat.
497            ∀start_status: Status.
498            ∀final_status: Status.
499            ∀trace_ends_flag.
500            ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
501              code_memory' = code_memory … start_status →
502                program_counter' = program_counter … start_status →
503                    (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
504                      cost_of_block = compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝
505  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
506  [ O ⇒ λbase_case. ⊥
507  | S program_size' ⇒ λrecursive_case.
508    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
509    let to_continue ≝
510      match lookup_opt … program_counter'' cost_labels with
511      [ None ⇒ true
512      | Some _ ⇒ first_time_around
513      ]
514    in
515      if to_continue then
516        match instruction return λx. x = instruction → ? with
517        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
518          match real_instruction return λx. x = real_instruction →
519          Σcost_of_block: nat.
520            ∀start_status: Status.
521            ∀final_status: Status.
522            ∀trace_ends_flag.
523            ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
524              code_memory' = code_memory … start_status →
525                program_counter' = program_counter … start_status →
526                    (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
527                      cost_of_block = compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace with
528          [ RET                    ⇒ λinstr. ticks
529          | JC   relative          ⇒ λinstr. ticks
530          | JNC  relative          ⇒ λinstr. ticks
531          | JB   bit_addr relative ⇒ λinstr. ticks
532          | JNB  bit_addr relative ⇒ λinstr. ticks
533          | JBC  bit_addr relative ⇒ λinstr. ticks
534          | JZ   relative          ⇒ λinstr. ticks
535          | JNZ  relative          ⇒ λinstr. ticks
536          | CJNE src_trgt relative ⇒ λinstr. ticks
537          | DJNZ src_trgt relative ⇒ λinstr. ticks
538          | _                      ⇒ λinstr.
539              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
540          ] (refl …)
541        | ACALL addr     ⇒ λinstr.
542            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
543        | AJMP  addr     ⇒ λinstr. ticks
544        | LCALL addr     ⇒ λinstr.
545            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
546        | LJMP  addr     ⇒ λinstr. ticks
547        | SJMP  addr     ⇒ λinstr. ticks
548        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
549            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
550        | MOVC  src trgt ⇒ λinstr.
551            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
552        ] (refl …)
553      else
554        (0 : (Σn: nat. ?))
555  ].
556  [1:
557    cases reachable_program_counter_witness #_ #hyp
558    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
559    @(le_to_lt_to_lt … base_case hyp)
560  |4:
561    #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
562    cases(block_cost' ?????????) -block_cost'
563    #recursive_block_cost #recursive_assm
564    @(trace_any_label_inv_ind … the_trace)
565    [1:
566      #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
567      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct
568      cases classifier_assm
569      whd in match (as_classifier ???);
570      whd in ⊢ (??%? → ?);
571      whd in match current_instruction; normalize nodelta
572      whd in match current_instruction0; normalize nodelta
573      #absurd @⊥ <FETCH in absurd; normalize nodelta
574      #absurd destruct(absurd)
575    |2:
576      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
577      #start_status_refl #final_status_refl #the_trace_assm destruct
578      whd in classifier_assm;
579      whd in classifier_assm:(??%?);
580      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
581      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
582      @⊥ <FETCH in classifier_assm; normalize nodelta
583      #absurd destruct(absurd)
584    |3:
585      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
586      #classifier_assm #after_return_assm #trace_label_return #costed_assm
587      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
588      destruct
589      cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
590        (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
591          (execute_1 status_pre_fun_call) status_final
592          (refl Status (execute_1 status_pre_fun_call)) classifier_assm
593          after_return_assm trace_label_return costed_assm) ? ?)
594      [2: %
595      |3:
596      |1:
597      ]
598    |4:
599      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
600      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
601      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
602      #final_status_refl #the_trace_refl destruct
603      whd in match (compute_paid_trace_any_label … (tal_step_call …));
604      whd in match (trace_any_label_length … (tal_step_call …));
605      cases(recursive_assm status_after_fun_call status_final end_flag trace_any_label ? ?)
606      [1:
607        * #recursive_n #recursive_trace_total #recursive_block_cost_assm
608        >recursive_block_cost_assm <recursive_trace_total %
609        [1:
610          %
611          [1:
612          |2:
613            >commutative_plus in ⊢ (??%?);
614            >commutative_plus in ⊢ (???%);
615          ]
616        |2:
617          @plus_right_monotone
618          whd in match (current_instruction_cost status_pre_fun_call);
619          <FETCH %
620        ]
621      |2:
622      |3:
623      ]
624    |5:
625      #end_flag #status_pre #status_init #status_end #execute_assm #the_trace'
626      #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
627      #final_status_refl #trace_refl
628      generalize in match the_trace; destruct #the_trace
629      whd in classifier_assm;
630      whd in classifier_assm:(??%?);
631      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
632      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
633      @⊥ <FETCH in classifier_assm; normalize nodelta
634      #absurd destruct(absurd)
635    ]
636  |7,8,9,10,13,16,19,22,25,28,31,34,37,40,41,42,43,44,45,46,47,48,49,52,55,58,61,
637    64,67,70,73,76,79,82,85,88,91,94,97,100,101,104,108,107:
638    cases daemon (* XXX: massive terms *)
639  |2:
640    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
641    lapply(good_program_witness program_counter' reachable_program_counter_witness)
642    <FETCH normalize nodelta <instr normalize nodelta
643    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
644    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
645    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
646    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
647    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
648    @(transitive_le
649      total_program_size
650      ((S program_size') + nat_of_bitvector … program_counter')
651      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
652    normalize in match (S program_size' + nat_of_bitvector … program_counter');
653    >plus_n_Sm
654    @monotonic_le_plus_r
655    change with (
656      nat_of_bitvector … program_counter' <
657        nat_of_bitvector … program_counter'')
658    assumption
659  |3:
660    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
661    lapply(good_program_witness program_counter' reachable_program_counter_witness)
662    <FETCH normalize nodelta <instr normalize nodelta
663    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
664    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
665    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
666    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
667    #_ #_ #program_counter_lt' #program_counter_lt_tps'
668    %
669    [1:
670      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
671      <FETCH normalize nodelta whd in match ltb; normalize nodelta
672      >(le_to_leb_true … program_counter_lt') %
673    |2:
674      assumption
675    ]
676  |5:
677    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
678    lapply(good_program_witness program_counter' reachable_program_counter_witness)
679      <FETCH normalize nodelta <instr normalize nodelta
680    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
681    * * * * #n'
682    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
683    @(transitive_le
684      total_program_size
685      ((S program_size') + nat_of_bitvector … program_counter')
686      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
687    normalize in match (S program_size' + nat_of_bitvector … program_counter');
688    >plus_n_Sm
689    @monotonic_le_plus_r
690    change with (
691      nat_of_bitvector … program_counter' <
692        nat_of_bitvector … program_counter'')
693    assumption
694  |6:
695    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
696    lapply(good_program_witness program_counter' reachable_program_counter_witness)
697      <FETCH normalize nodelta <instr normalize nodelta
698    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
699    * * * * #n'
700    #_ #_ #program_counter_lt' #program_counter_lt_tps'
701    %
702    [1:
703      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
704      <FETCH normalize nodelta whd in match ltb; normalize nodelta
705      >(le_to_leb_true … program_counter_lt') %
706    |2:
707      assumption
708    ]
709  |11,14: (* JMP and MOVC *)
710    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
711    lapply(good_program_witness program_counter' reachable_program_counter_witness)
712    <FETCH normalize nodelta <instr normalize nodelta
713    try(<real_instruction_refl <instr normalize nodelta) *
714    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
715    @(transitive_le
716      total_program_size
717      ((S program_size') + nat_of_bitvector … program_counter')
718      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
719    normalize in match (S program_size' + nat_of_bitvector … program_counter');
720    >plus_n_Sm
721    @monotonic_le_plus_r
722    change with (
723      nat_of_bitvector … program_counter' <
724        nat_of_bitvector … program_counter'')
725    assumption
726  |12,15:
727    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
728    lapply(good_program_witness program_counter' reachable_program_counter_witness)
729    <FETCH normalize nodelta <instr normalize nodelta *
730    #program_counter_lt' #program_counter_lt_tps' %
731    [1,3:
732      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
733      <FETCH normalize nodelta whd in match ltb; normalize nodelta
734      >(le_to_leb_true … program_counter_lt') %
735    |2,4:
736      assumption
737    ]
738  |17,20,23,26,29,32,35,38,50,53,56,59,62,65,68,71,74,77,80,83,86,89,92,95,98,
739   102,105:
740    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
741    lapply(good_program_witness program_counter' reachable_program_counter_witness)
742    <FETCH normalize nodelta
743    <real_instruction_refl <instr normalize nodelta *
744    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
745    @(transitive_le
746      total_program_size
747      ((S program_size') + nat_of_bitvector … program_counter')
748      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
749    normalize in match (S program_size' + nat_of_bitvector … program_counter');
750    >plus_n_Sm
751    @monotonic_le_plus_r
752    change with (
753      nat_of_bitvector … program_counter' <
754        nat_of_bitvector … program_counter'')
755    assumption
756  |18,21,24,27,30,33,36,39,51,54,57,60,63,66,69,72,75,78,
757    81,84,87,90,93,96,99,103,106:
758    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
759    lapply(good_program_witness program_counter' reachable_program_counter_witness)
760    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
761    #program_counter_lt' #program_counter_lt_tps' %
762    try assumption
763    [*:
764      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
765      <FETCH normalize nodelta whd in match ltb; normalize nodelta
766      >(le_to_leb_true … program_counter_lt') %
767    ]
768  [1:
769    #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
770    cases(block_cost' ?????? ?? ?) -block_cost'
771    #recursive_block_cost #recursive_assm
772    @(trace_any_label_inv_ind … the_trace)
773    [1:
774      #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
775      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct
776      cases classifier_assm
777      whd in match (as_classifier ? ? ?);
778      whd in ⊢ (??%? → ?);
779      whd in match current_instruction; normalize nodelta
780      whd in match current_instruction0; normalize nodelta
781      #absurd @⊥ >p1 in absurd; normalize nodelta
782      #absurd destruct(absurd)
783    |2:
784      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
785      #start_status_refl #final_status_refl #the_trace_assm destruct
786      whd in classifier_assm;
787      whd in classifier_assm:(??%?);
788      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
789      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
790      @⊥
791      >p1 in classifier_assm; normalize nodelta
792      #absurd destruct(absurd)
793    |3:
794      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
795      #classifier_assm #after_return_assm #trace_label_return #costed_assm
796      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
797      destruct
798      cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
799        (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
800          (execute_1 status_pre_fun_call) status_final
801          (refl Status (execute_1 status_pre_fun_call)) classifier_assm
802          after_return_assm trace_label_return costed_assm) ? ?)
803      [2: %
804      |3:
805      |1:
806      ]
807    |4:
808      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
809      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
810      #costed_assm #trace_any_label #trace_ends_refl #start_status_refl #final_status_refl
811      #the_trace_refl destruct whd in ⊢ (??(???%)); whd in match (trace_any_label_length … (tal_step_call … trace_any_label));
812    |5:
813      #end_flag #status_pre #status_init #status_end #execute_assm #the_trace
814      #classifier_assm #costed_assm #ends_flag_refl #start_status_refl #final_status_refl
815      #the_trace_refl -the_trace_refl destruct
816      whd in classifier_assm;
817      whd in classifier_assm:(??%?);
818      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
819      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
820      @⊥ >p1 in classifier_assm; normalize nodelta
821      #absurd destruct(absurd)
822    ]
823  [1:
824    #start_status #final_status #trace_ends_flag #the_trace
825    #code_memory_refl #program_counter_refl
826    cases(block_cost' ?????? ?? ?) -block_cost'
827    #recursive_block_cost #recursive_assm
828    @(trace_any_label_inv_ind … the_trace)
829    [1:
830      #start_status' #final_status' #execute_assm #not_return_assm
831      #costed_assm #trace_ends_flag_assm #start_status_assm #final_status_assm
832      #the_trace_assm
833      cases daemon (* XXX: bug in notion of traces here *)
834    |2:
835
836    |3:
837      cases daemon (* XXX *)
838    |4:
839    ]
840  |108:
841    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
842    lapply(good_program_witness program_counter' reachable_program_counter_witness)
843    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
844    #program_counter_lt' #program_counter_lt_tps' %
845    try assumption
846    [*:
847      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
848      <FETCH normalize nodelta whd in match ltb; normalize nodelta
849      >(le_to_leb_true … program_counter_lt') %
850    ]
851  [1:
852    cases reachable_program_counter_witness #_ #hyp
853    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
854    @(le_to_lt_to_lt … base_case hyp)
855  |2:
856    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
857    lapply(good_program_witness program_counter reachable_program_counter_witness)
858      <FETCH normalize nodelta <instr normalize nodelta
859    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
860    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
861    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
862    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
863    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
864    @(transitive_le
865      total_program_size
866      ((S program_size') + nat_of_bitvector … program_counter)
867      (program_size' + nat_of_bitvector … program_counter') recursive_case)
868    normalize in match (S program_size' + nat_of_bitvector … program_counter);
869    >plus_n_Sm
870    @monotonic_le_plus_r
871    change with (
872      nat_of_bitvector … program_counter <
873        nat_of_bitvector … program_counter')
874    assumption
875  |3:
876    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
877    lapply(good_program_witness program_counter reachable_program_counter_witness)
878      <FETCH normalize nodelta <instr normalize nodelta
879    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
880    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
881    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
882    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
883    #_ #_ #program_counter_lt' #program_counter_lt_tps'
884    %
885    [1:
886      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
887      <FETCH normalize nodelta whd in match ltb; normalize nodelta
888      >(le_to_leb_true … program_counter_lt') %
889    |2:
890      assumption
891    ]
892  |4:
893    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
894    lapply(good_program_witness program_counter reachable_program_counter_witness)
895      <FETCH normalize nodelta <instr normalize nodelta
896    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
897    * * * * #n'
898    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
899    @(transitive_le
900      total_program_size
901      ((S program_size') + nat_of_bitvector … program_counter)
902      (program_size' + nat_of_bitvector … program_counter') recursive_case)
903    normalize in match (S program_size' + nat_of_bitvector … program_counter);
904    >plus_n_Sm
905    @monotonic_le_plus_r
906    change with (
907      nat_of_bitvector … program_counter <
908        nat_of_bitvector … program_counter')
909    assumption
910  |5:
911    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
912    lapply(good_program_witness program_counter reachable_program_counter_witness)
913      <FETCH normalize nodelta <instr normalize nodelta
914    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
915    * * * * #n'
916    #_ #_ #program_counter_lt' #program_counter_lt_tps'
917    %
918    [1:
919      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
920      <FETCH normalize nodelta whd in match ltb; normalize nodelta
921      >(le_to_leb_true … program_counter_lt') %
922    |2:
923      assumption
924    ]
925  |6,8: (* JMP and MOVC *)
926    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
927    lapply(good_program_witness program_counter reachable_program_counter_witness)
928    <FETCH normalize nodelta <instr normalize nodelta
929    try(<real_instruction_refl <instr normalize nodelta) *
930    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
931    @(transitive_le
932      total_program_size
933      ((S program_size') + nat_of_bitvector … program_counter)
934      (program_size' + nat_of_bitvector … program_counter') recursive_case)
935    normalize in match (S program_size' + nat_of_bitvector … program_counter);
936    >plus_n_Sm
937    @monotonic_le_plus_r
938    change with (
939      nat_of_bitvector … program_counter <
940        nat_of_bitvector … program_counter')
941    assumption
942  |7,9:
943    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
944    lapply(good_program_witness program_counter reachable_program_counter_witness)
945    <FETCH normalize nodelta <instr normalize nodelta *
946    #program_counter_lt' #program_counter_lt_tps' %
947    [1,3:
948      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
949      <FETCH normalize nodelta whd in match ltb; normalize nodelta
950      >(le_to_leb_true … program_counter_lt') %
951    |2,4:
952      assumption
953    ]
954  |11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,
955    55,57,59,61,63:
956    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
957    lapply(good_program_witness program_counter reachable_program_counter_witness)
958    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
959    #program_counter_lt' #program_counter_lt_tps' %
960    try assumption
961    [*:
962      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
963      <FETCH normalize nodelta whd in match ltb; normalize nodelta
964      >(le_to_leb_true … program_counter_lt') %
965    ]
966  |10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
967    54,56,58,60,62:
968    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
969    lapply(good_program_witness program_counter reachable_program_counter_witness)
970    <FETCH normalize nodelta
971    <real_instruction_refl <instr normalize nodelta *
972    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
973    @(transitive_le
974      total_program_size
975      ((S program_size') + nat_of_bitvector … program_counter)
976      (program_size' + nat_of_bitvector … program_counter') recursive_case)
977    normalize in match (S program_size' + nat_of_bitvector … program_counter);
978    >plus_n_Sm
979    @monotonic_le_plus_r
980    change with (
981      nat_of_bitvector … program_counter <
982        nat_of_bitvector … program_counter')
983    assumption
984  ]
985qed.
986
987definition block_cost ≝
988  λcode_memory: BitVectorTrie Byte 16.
989  λprogram_counter: Word.
990  λtotal_program_size: nat.
991  λcost_labels: BitVectorTrie costlabel 16.
992  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
993  λgood_program_witness: good_program code_memory total_program_size.
994    block_cost' code_memory program_counter total_program_size total_program_size cost_labels
995      reachable_program_counter_witness good_program_witness true ?.
996  @le_plus_n_r
997qed.
998
999lemma fetch_program_counter_n_Sn:
1000  ∀instruction: instruction.
1001  ∀program_counter, program_counter': Word.
1002  ∀ticks, n: nat.
1003  ∀code_memory: BitVectorTrie Byte 16.
1004    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
1005      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
1006        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
1007          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
1008  #instruction #program_counter #program_counter' #ticks #n #code_memory
1009  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
1010  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
1011  <fetch_program_counter_n_hyp normalize nodelta
1012  <fetch_hyp normalize nodelta
1013  change with (
1014    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
1015  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
1016  >(le_to_leb_true … lt_hyp) %
1017qed.
1018
1019let rec traverse_code_internal
1020  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
1021    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
1022      (reachable_program_counter_witness:
1023          ∀lbl: costlabel.
1024          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1025            reachable_program_counter code_memory fixed_program_size program_counter)
1026        (good_program_witness: good_program code_memory fixed_program_size)
1027        on program_size: identifier_map CostTag nat ≝
1028  match program_size with
1029  [ O ⇒ empty_map …
1030  | S program_size ⇒
1031    let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
1032    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in
1033    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → ? with
1034    [ None ⇒ λlookup_refl. cost_mapping
1035    | Some lbl ⇒ λlookup_refl.
1036      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
1037        add … cost_mapping lbl cost
1038    ] (refl … (lookup_opt … program_counter cost_labels))
1039  ].
1040  [1:
1041    @(reachable_program_counter_witness lbl)
1042    assumption
1043  |2:
1044    assumption
1045  ]
1046qed.
1047
1048definition traverse_code ≝
1049  λcode_memory: BitVectorTrie Byte 16.
1050  λcost_labels: BitVectorTrie costlabel 16.
1051  λprogram_size: nat.
1052  λreachable_program_counter_witness:
1053          ∀lbl: costlabel.
1054          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1055            reachable_program_counter code_memory program_size program_counter.
1056  λgood_program_witness: good_program code_memory program_size.
1057    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
1058 
1059definition compute_costs ≝
1060  λprogram: list Byte.
1061  λcost_labels: BitVectorTrie costlabel 16.
1062  λreachable_program_witness.
1063  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
1064    let program_size ≝ |program| + 1 in
1065    let code_memory ≝ load_code_memory program in
1066      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
1067  @good_program_witness
1068qed.
Note: See TracBrowser for help on using the repository browser.