source: src/ASM/ASMCosts.ma @ 1894

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

Closed a hole in the proof by deriving a contradiction using even_p and odd_p

File size: 90.1 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  cases (execute_1' code_memory start_status) #the_status
477  * #_ #classify_assm' @classify_assm' assumption
478qed-.
479
480lemma reachable_program_counter_to_0_lt_total_program_size:
481  ∀code_memory: BitVectorTrie Byte 16.
482  ∀program_counter: Word.
483  ∀total_program_size: nat.
484    reachable_program_counter code_memory total_program_size program_counter →
485      0 < total_program_size.
486  #code_memory #program_counter #total_program_size
487  whd in match reachable_program_counter; normalize nodelta * * #some_n
488  #_ cases (nat_of_bitvector 16 program_counter)
489  [1:
490    #assm assumption
491  |2:
492    #new_pc @ltn_to_ltO
493  ]
494qed.
495
496lemma trace_compute_paid_trace_cl_other:
497  ∀code_memory' : (BitVectorTrie Byte 16).
498  ∀program_counter' : Word.
499  ∀total_program_size : ℕ.
500  ∀cost_labels : (BitVectorTrie costlabel 16).
501  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
502  ∀good_program_witness : (good_program code_memory' total_program_size).
503  ∀program_size' : ℕ.
504  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
505  ∀ticks : ℕ.
506  ∀instruction : instruction.
507  ∀program_counter'' : Word.
508  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
509  ∀start_status : (Status code_memory').
510  ∀final_status : (Status code_memory').
511  ∀trace_ends_flag : trace_ends_with_ret.
512  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
513  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
514  ∀classify_assm: ASM_classify0 instruction = cl_other.
515  ∀pi1 : ℕ.
516   (if match lookup_opt costlabel 16 program_counter'' cost_labels with 
517         [None ⇒ true
518         |Some _ ⇒ false
519         ] 
520    then
521      ∀start_status0:Status code_memory'.
522      ∀final_status0:Status code_memory'.
523      ∀trace_ends_flag0:trace_ends_with_ret.
524      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
525        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
526        (∃n:ℕ
527                    .trace_any_label_length code_memory' cost_labels
528                     trace_ends_flag0 start_status0 final_status0 the_trace0
529                     +S n
530                     =total_program_size)
531                   ∧pi1
532                    =compute_paid_trace_any_label code_memory' cost_labels
533                     trace_ends_flag0 start_status0 final_status0 the_trace0
534    else (pi1=O) )
535   →(∃n:ℕ
536     .trace_any_label_length code_memory' cost_labels trace_ends_flag
537      start_status final_status the_trace
538      +S n
539      =total_program_size)
540    ∧ticks+pi1
541     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
542      start_status final_status the_trace.
543  #code_memory' #program_counter' #total_program_size #cost_labels
544  #reachable_program_counter_witness #good_program_witness
545  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
546  #start_status #final_status
547  #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
548  #recursive_assm
549  @(trace_any_label_inv_ind … the_trace)
550    [5:
551      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
552      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
553      #the_trace_refl
554      destruct
555      whd in match (trace_any_label_length … (tal_step_default …));
556      whd in match (compute_paid_trace_any_label … (tal_step_default …));
557      whd in costed_assm:(?%);
558      generalize in match costed_assm;
559      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
560      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
561        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
562      #lookup_assm cases lookup_assm
563      [1:
564        #None_lookup_opt_assm normalize nodelta #ignore
565        generalize in match recursive_assm;
566        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
567        [1:
568          <fetch_twice_fetch_execute_1
569          [1:
570            <FETCH %
571          |2:
572            >classifier_assm %
573          ]
574        |2:
575          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
576          normalize nodelta #new_recursive_assm
577          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
578            end_flag trace_any_label ?) [2: % ]
579          #exists_assm #recursive_block_cost_assm %
580          [1:
581            cases exists_assm #exists_n #total_program_size_refl
582            <total_program_size_refl
583            %{(exists_n - current_instruction_cost … status_pre)}
584            (* XXX: Christ knows what's going on with the rewrite tactic here? *)
585            cases daemon
586          |2:
587            >recursive_block_cost_assm
588            whd in match (current_instruction_cost … status_pre);
589            cut(ticks = \snd (fetch code_memory'
590               (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
591            [1:
592              <FETCH %
593            |2:
594              #ticks_refl_assm >ticks_refl_assm %
595            ]
596          ]
597        ]
598      |2:
599        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
600        #absurd cases absurd #absurd cases(absurd I)
601      ]
602    |1:
603      #status_start #status_final #execute_assm #classifier_assm #costed_assm
604      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
605      destruct
606      whd in match (trace_any_label_length … (tal_base_not_return …));
607      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
608      whd in costed_assm;
609      generalize in match costed_assm;
610      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
611      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
612        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
613      #lookup_assm cases lookup_assm
614      [1:
615        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
616        #absurd cases absurd
617      |2:
618        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
619        generalize in match recursive_assm;
620        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
621        [1:
622          <fetch_twice_fetch_execute_1
623          [1:
624            <FETCH %
625          |2:
626            cases classifier_assm
627            [1:
628              whd in ⊢ (% → ?);
629              whd in ⊢ (??%? → ?);
630              whd in match (current_instruction code_memory' status_start);
631              <FETCH generalize in match classify_assm;
632              cases instruction
633              [8:
634                #preinstruction normalize nodelta
635                whd in match ASM_classify0; normalize nodelta
636                #contradiction >contradiction #absurd destruct(absurd)
637              ]
638              try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
639              try(#addr normalize nodelta #ignore #absurd destruct(absurd))
640              normalize in ignore; destruct(ignore)
641            |2:
642              #classifier_assm' >classifier_assm' %
643            ]
644          ]
645        |2:
646          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
647          normalize nodelta #new_recursive_assm >new_recursive_assm %
648          [1:
649            %{(pred total_program_size)} whd in ⊢ (??%?);
650            @S_pred
651            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
652          |2:
653            cut(ticks = \snd (fetch code_memory'
654               (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
655            [1:
656              <FETCH %
657            |2:
658              #ticks_refl_assm >ticks_refl_assm
659              <plus_n_O %
660            ]
661          ]
662        ]
663      ]
664    |2:
665      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
666      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
667    |3:
668      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
669      #classifier_assm #after_return_assm #trace_label_return #costed_assm
670      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
671      destruct @⊥
672    |4:
673      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
674      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
675      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
676      #final_status_refl #the_trace_refl destruct @⊥
677    ]
678  change with (ASM_classify0 ? = ?) in classifier_assm;
679  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
680  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
681  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
682qed.
683
684lemma trace_compute_paid_trace_cl_jump:
685  ∀code_memory': BitVectorTrie Byte 16.
686  ∀program_counter': Word.
687  ∀total_program_size: ℕ.
688  ∀cost_labels: BitVectorTrie costlabel 16.
689  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
690  ∀good_program_witness: good_program code_memory' total_program_size.
691  ∀first_time_around: bool.
692  ∀program_size': ℕ.
693  ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'.
694  ∀ticks: ℕ.
695  ∀instruction: instruction.
696  ∀program_counter'': Word.
697  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
698  ∀start_status: (Status code_memory').
699  ∀final_status: (Status code_memory').
700  ∀trace_ends_flag: trace_ends_with_ret.
701  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
702  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
703  ∀classify_assm: ASM_classify0 instruction = cl_jump.
704   (∃n:ℕ
705     .trace_any_label_length code_memory' cost_labels trace_ends_flag
706      start_status final_status the_trace
707      +S n
708      =total_program_size)
709    ∧ticks
710     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
711      start_status final_status the_trace.
712  #code_memory' #program_counter' #total_program_size #cost_labels
713  #reachable_program_counter_witness #good_program_witness #first_time_around
714  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
715  #start_status #final_status
716  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
717  @(trace_any_label_inv_ind … the_trace)
718  [5:
719    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
720    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
721    #the_trace_refl destruct @⊥
722  |1:
723    #status_start #status_final #execute_assm #classifier_assm #costed_assm
724    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
725    destruct
726    whd in match (trace_any_label_length … (tal_base_not_return …));
727    whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); %
728    [1:
729      %{(pred total_program_size)} whd in ⊢ (??%?);
730      @S_pred
731      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
732    |2:
733      <FETCH %
734    ]
735  |2:
736    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
737    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
738  |3:
739    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
740    #classifier_assm #after_return_assm #trace_label_return #costed_assm
741    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
742    destruct @⊥
743  |4:
744    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
745    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
746    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
747    #final_status_refl #the_trace_refl destruct @⊥
748  ]
749  change with (ASM_classify0 ? = ?) in classifier_assm;
750  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
751  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
752  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
753qed.
754
755lemma trace_compute_paid_trace_cl_call:
756  ∀code_memory' : (BitVectorTrie Byte 16).
757  ∀program_counter' : Word.
758  ∀total_program_size : ℕ.
759  ∀cost_labels : (BitVectorTrie costlabel 16).
760  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
761  ∀good_program_witness : (good_program code_memory' total_program_size).
762  ∀program_size' : ℕ.
763  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
764  ∀ticks : ℕ.
765  ∀instruction : instruction.
766  ∀program_counter'' : Word.
767  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
768  ∀start_status : (Status code_memory').
769  ∀final_status : (Status code_memory').
770  ∀trace_ends_flag : trace_ends_with_ret.
771  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
772  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
773  ∀classify_assm: ASM_classify0 instruction = cl_call.
774  (∀pi1:ℕ
775  .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
776      [None ⇒ true | Some _ ⇒ false] 
777   then (∀start_status0:Status code_memory'
778             .∀final_status0:Status code_memory'
779              .∀trace_ends_flag0:trace_ends_with_ret
780               .∀the_trace0:trace_any_label
781                                        (ASM_abstract_status code_memory' cost_labels)
782                                        trace_ends_flag0 start_status0 final_status0
783                .program_counter''
784                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
785                 →(∃n:ℕ
786                   .trace_any_label_length code_memory' cost_labels trace_ends_flag0
787                    start_status0 final_status0 the_trace0
788                    +S n
789                    =total_program_size)
790                  ∧pi1
791                   =compute_paid_trace_any_label code_memory' cost_labels
792                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
793   else (pi1=O) 
794   →(∃n:ℕ
795     .trace_any_label_length code_memory' cost_labels trace_ends_flag
796      start_status final_status the_trace
797      +S n
798      =total_program_size)
799    ∧ticks+pi1
800     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
801      start_status final_status the_trace).
802  #code_memory' #program_counter' #total_program_size #cost_labels
803  #reachable_program_counter_witness #good_program_witness #program_size'
804  #recursive_case #ticks #instruction #program_counter'' #FETCH
805  #start_status #final_status #trace_ends_flag
806  #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
807  @(trace_any_label_inv_ind … the_trace)
808  [5:
809    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
810    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
811    #the_trace_refl destruct @⊥
812  |1:
813    #status_start #status_final #execute_assm #classifier_assm #costed_assm
814    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
815    destruct @⊥
816  |2:
817    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
818    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
819  |3:
820    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
821    #classifier_assm #after_return_assm #trace_label_return #costed_assm
822    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
823    destruct
824    whd in match (trace_any_label_length … (tal_base_call …));
825    whd in match (compute_paid_trace_any_label … (tal_base_call …));
826    whd in costed_assm;
827    generalize in match costed_assm;
828    generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
829    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
830      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
831    #lookup_assm cases lookup_assm
832    [1:
833      #None_lookup_opt normalize nodelta #absurd cases absurd
834    |2:
835      #costlabel #Some_lookup_opt normalize nodelta #ignore
836      generalize in match recursive_assm;
837      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
838      [1:
839        whd in after_return_assm; <after_return_assm; (* XXX: here *)
840        cases daemon
841      |2:
842        #program_counter_assm >program_counter_assm <Some_lookup_opt
843        normalize nodelta #new_recursive_assm >new_recursive_assm %
844        [1:
845          %{(pred total_program_size)} whd in ⊢ (??%?);
846          @S_pred
847          @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
848        |2:
849          cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
850          [1:
851            <FETCH %
852          |2:
853            #ticks_refl_assm >ticks_refl_assm
854            <plus_n_O %
855          ]
856        ]
857      ]
858    ]
859  |4:
860    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
861    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
862    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
863    #final_status_refl #the_trace_refl destruct
864    whd in match (trace_any_label_length … (tal_step_call …));
865    whd in match (compute_paid_trace_any_label … (tal_step_call …));
866    whd in costed_assm:(?%);
867    generalize in match costed_assm;
868    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
869    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
870      in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
871    #lookup_assm cases lookup_assm
872    [1:
873      #None_lookup_opt_assm normalize nodelta #ignore
874      generalize in match recursive_assm;
875      cut(program_counter'' = program_counter … status_after_fun_call)
876      [1:
877        cases daemon
878      |2:
879        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
880        normalize nodelta #new_recursive_assm %
881        cases (new_recursive_assm … trace_any_label ?)
882        [1,3:
883          #exists_assm #recursive_block_cost_assm
884          [2:
885            >recursive_block_cost_assm
886            @plus_right_monotone
887            whd in ⊢ (???%); <FETCH %
888          |1:
889            (*
890            cases exists_assm #recursive_n #new_exists_assm
891            <new_exists_assm
892           
893            %
894            [1:
895              @(recursive_n - current_instruction_cost … status_pre_fun_call)
896            |2:
897             
898              cut(current_instruction_cost … status_pre_fun_call =
899                (nat_of_bitvector 16
900  (program_counter (BitVectorTrie Byte 16) code_memory' status_after_fun_call)
901  -nat_of_bitvector 16
902   (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
903              [1:
904              |2:
905                #eq_assm <eq_assm -eq_assm -new_exists_assm -recursive_block_cost_assm
906                <plus_n_Sm <plus_n_Sm @eq_f
907                >associative_plus in ⊢ (??%?); >commutative_plus in ⊢ (??%?);
908                >associative_plus @eq_f
909                <plus_minus_m_m [1: % ]
910              ]
911            ] *)
912            cases daemon
913          ]
914        |2,4:
915          %
916        ]
917      ]
918    |2:
919      #cost_label #Some_lookup_opt_assm normalize nodelta #absurd
920      cases absurd #absurd cases (absurd I)
921    ]
922  ]
923  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
924  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
925  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
926  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
927  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
928  #absurd destruct(absurd)
929qed.
930
931lemma trace_compute_paid_trace_cl_return:
932  ∀code_memory' : (BitVectorTrie Byte 16).
933  ∀program_counter' : Word.
934  ∀total_program_size : ℕ.
935  ∀cost_labels : (BitVectorTrie costlabel 16).
936  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
937  ∀good_program_witness : (good_program code_memory' total_program_size).
938  ∀program_size' : ℕ.
939  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
940  ∀ticks : ℕ.
941  ∀instruction : instruction.
942  ∀program_counter'' : Word.
943  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
944  ∀start_status : (Status code_memory').
945  ∀final_status : (Status code_memory').
946  ∀trace_ends_flag : trace_ends_with_ret.
947  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
948  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
949  ∀classify_assm: ASM_classify0 instruction = cl_return.
950    (∃n:ℕ
951     .trace_any_label_length code_memory' cost_labels trace_ends_flag
952      start_status final_status the_trace
953      +S n
954      =total_program_size)
955    ∧ticks
956     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
957      start_status final_status the_trace.
958  #code_memory' #program_counter' #total_program_size #cost_labels
959  #reachable_program_counter_witness #good_program_witness #program_size'
960  #recursive_case #ticks #instruction #program_counter'' #FETCH
961  #start_status #final_status #trace_ends_flag
962  #the_trace #program_counter_refl #classify_assm
963  @(trace_any_label_inv_ind … the_trace)
964  [1:
965    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
966    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
967    destruct @⊥
968  |2:
969    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
970    #start_status_refl #final_status_refl #the_trace_refl destruct
971    whd in match (trace_any_label_length … (tal_base_return …));
972    whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
973    [1:
974      %{(pred total_program_size)} whd in ⊢ (??%?);
975      @S_pred
976      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
977    |2:
978      <FETCH %
979    ]
980  |3:
981    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
982    #classifier_assm #after_return_assm #trace_label_return #costed_assm
983    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
984    destruct @⊥
985  |4:
986    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
987    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
988    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
989    #final_status_refl #the_trace_refl
990    destruct @⊥
991  |5:
992    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
993    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
994    #final_status_refl #the_trace_refl destruct @⊥
995  ]
996  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
997  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
998  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
999  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1000  <FETCH in classifier_assm; >classify_assm
1001  #absurd try (destruct(absurd))
1002  cases absurd
1003  #absurd destruct(absurd)
1004qed.
1005     
1006     
1007let rec block_cost'
1008  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
1009    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
1010      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
1011        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
1012          on program_size:
1013          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
1014          Σcost_of_block: nat.
1015          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
1016            ∀start_status: Status code_memory'.
1017            ∀final_status: Status code_memory'.
1018            ∀trace_ends_flag.
1019            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1020              program_counter' = program_counter … start_status →
1021                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1022                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
1023          else
1024            (cost_of_block = 0) ≝
1025  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
1026  [ O ⇒ λbase_case. ⊥
1027  | S program_size' ⇒ λrecursive_case.
1028    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
1029    let to_continue ≝
1030      match lookup_opt … program_counter' cost_labels with
1031      [ None ⇒ true
1032      | Some _ ⇒ first_time_around
1033      ]
1034    in
1035      ((if to_continue then
1036       pi1 … (match instruction return λx. x = instruction → ? with
1037        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
1038          match real_instruction return λx. x = real_instruction →
1039          Σcost_of_block: nat.
1040            ∀start_status: Status code_memory'.
1041            ∀final_status: Status code_memory'.
1042            ∀trace_ends_flag.
1043            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
1044              program_counter' = program_counter … start_status →
1045                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1046                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
1047          [ RET                    ⇒ λinstr. ticks
1048          | RETI                   ⇒ λinstr. ticks
1049          | JC   relative          ⇒ λinstr. ticks
1050          | JNC  relative          ⇒ λinstr. ticks
1051          | JB   bit_addr relative ⇒ λinstr. ticks
1052          | JNB  bit_addr relative ⇒ λinstr. ticks
1053          | JBC  bit_addr relative ⇒ λinstr. ticks
1054          | JZ   relative          ⇒ λinstr. ticks
1055          | JNZ  relative          ⇒ λinstr. ticks
1056          | CJNE src_trgt relative ⇒ λinstr. ticks
1057          | DJNZ src_trgt relative ⇒ λinstr. ticks
1058          | _                      ⇒ λinstr.
1059         
1060              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1061          ] (refl …)
1062        | ACALL addr     ⇒ λinstr.
1063            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1064        | AJMP  addr     ⇒ λinstr. ticks
1065        | LCALL addr     ⇒ λinstr.
1066            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1067        | LJMP  addr     ⇒ λinstr. ticks
1068        | SJMP  addr     ⇒ λinstr. ticks
1069        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
1070            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1071        | MOVC  src trgt ⇒ λinstr.
1072            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1073        ] (refl …))
1074      else
1075        0)
1076      : Σcost_of_block: nat.
1077          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
1078          [ true ⇒
1079            ∀start_status: Status code_memory'.
1080            ∀final_status: Status code_memory'.
1081            ∀trace_ends_flag.
1082            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1083              program_counter' = program_counter … start_status →
1084                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1085                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
1086          | false ⇒
1087            (cost_of_block = 0)
1088          ])
1089  ].
1090  [1:
1091    cases reachable_program_counter_witness #_ #hyp
1092    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
1093    @(le_to_lt_to_lt … base_case hyp)
1094  |2:
1095    change with (if to_continue then ? else (? = 0))
1096    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
1097    @pi2
1098  |3:
1099    change with (if to_continue then ? else (0 = 0))
1100    >p normalize nodelta %
1101  |7,8:
1102    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1103    @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
1104    destruct %
1105  |96,102,105:
1106    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1107    cases(block_cost' ?????????) -block_cost'
1108    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
1109    destruct %
1110  |4,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,69,72,75,78,81,84,87,
1111   90,93:
1112    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1113    cases(block_cost' ?????????) -block_cost'
1114    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
1115    destruct %
1116  |60,61,62,63,64,65,66,67,68,69,99,101,100,102:
1117    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1118    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
1119    destruct %
1120  |103:
1121    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1122    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1123    <FETCH normalize nodelta <instr normalize nodelta
1124    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1125    * * * * #n'
1126    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1127    %
1128    [1:
1129      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1130      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1131      >(le_to_leb_true … program_counter_lt') %
1132    |2:
1133      assumption
1134    ]
1135  |104:
1136    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1137    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1138    <FETCH normalize nodelta <instr normalize nodelta
1139    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1140    * * * * #n'
1141    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1142    @(transitive_le
1143      total_program_size
1144      ((S program_size') + nat_of_bitvector … program_counter')
1145      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1146    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1147    >plus_n_Sm
1148    @monotonic_le_plus_r
1149    change with (
1150      nat_of_bitvector … program_counter' <
1151        nat_of_bitvector … program_counter'')
1152    assumption
1153  |106:
1154    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1155    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1156    <FETCH normalize nodelta <instr normalize nodelta
1157    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1158    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1159    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1160    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1161    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1162    %
1163    [1:
1164      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1165      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1166      >(le_to_leb_true … program_counter_lt') %
1167    |2:
1168      assumption
1169    ]
1170  |107:
1171    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1172    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1173    <FETCH normalize nodelta <instr normalize nodelta
1174    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1175    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1176    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1177    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1178    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1179    @(transitive_le
1180      total_program_size
1181      ((S program_size') + nat_of_bitvector … program_counter')
1182      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1183    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1184    >plus_n_Sm
1185    @monotonic_le_plus_r
1186    change with (
1187      nat_of_bitvector … program_counter' <
1188        nat_of_bitvector … program_counter'')
1189    assumption
1190  |94,97:
1191    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1192    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1193    <FETCH normalize nodelta <instr normalize nodelta *
1194    #program_counter_lt' #program_counter_lt_tps' %
1195    [1,3:
1196      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1197      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1198      >(le_to_leb_true … program_counter_lt') %
1199    |2,4:
1200      assumption
1201    ]
1202  |5,10,12,13,16,18,19,22,25,28,31,34,37,40,43,46,49,52,55,58,70,73,
1203   76,79,82,85,88,91:
1204    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1205    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1206    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1207    #program_counter_lt' #program_counter_lt_tps' %
1208    try assumption
1209    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1210    <FETCH normalize nodelta whd in match ltb; normalize nodelta
1211    >(le_to_leb_true … program_counter_lt') %
1212    (* XXX: got to here *)
1213  |6,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
1214   92:
1215    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1216    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1217    <FETCH normalize nodelta
1218    <real_instruction_refl <instr normalize nodelta *
1219    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1220    @(transitive_le
1221      total_program_size
1222      ((S program_size') + nat_of_bitvector … program_counter')
1223      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1224    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1225    >plus_n_Sm
1226    @monotonic_le_plus_r
1227    change with (
1228      nat_of_bitvector … program_counter' <
1229        nat_of_bitvector … program_counter'')
1230    assumption
1231  |95,98:
1232    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1233    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1234    <FETCH normalize nodelta <instr normalize nodelta
1235    try(<real_instruction_refl <instr normalize nodelta) *
1236    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1237    @(transitive_le
1238      total_program_size
1239      ((S program_size') + nat_of_bitvector … program_counter')
1240      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1241    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1242    >plus_n_Sm
1243    @monotonic_le_plus_r
1244    change with (
1245      nat_of_bitvector … program_counter' <
1246        nat_of_bitvector … program_counter'')
1247    assumption
1248  ]
1249qed.
1250
1251definition block_cost:
1252    ∀code_memory': BitVectorTrie Byte 16.
1253    ∀program_counter': Word.
1254    ∀total_program_size: nat.
1255    ∀cost_labels: BitVectorTrie costlabel 16.
1256    ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
1257    ∀good_program_witness: good_program code_memory' total_program_size.
1258      Σcost_of_block: nat.
1259        ∀start_status: Status code_memory'.
1260        ∀final_status: Status code_memory'.
1261        ∀trace_ends_flag.
1262        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1263          program_counter' = program_counter … start_status →
1264            (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1265              cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
1266  λcode_memory: BitVectorTrie Byte 16.
1267  λprogram_counter: Word.
1268  λtotal_program_size: nat.
1269  λcost_labels: BitVectorTrie costlabel 16.
1270  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
1271  λgood_program_witness: good_program code_memory total_program_size. ?.
1272  cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
1273    reachable_program_counter_witness good_program_witness true ?)
1274  [1:
1275    #cost_of_block #block_cost_hyp
1276    %{cost_of_block}
1277    cases(lookup_opt … cost_labels) in block_cost_hyp;
1278    [2: #cost_label] normalize nodelta
1279    #hyp assumption
1280  |2:
1281    @le_plus_n_r
1282  ]
1283qed.
1284
1285lemma fetch_program_counter_n_Sn:
1286  ∀instruction: instruction.
1287  ∀program_counter, program_counter': Word.
1288  ∀ticks, n: nat.
1289  ∀code_memory: BitVectorTrie Byte 16.
1290    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
1291      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
1292        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
1293          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
1294  #instruction #program_counter #program_counter' #ticks #n #code_memory
1295  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
1296  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
1297  <fetch_program_counter_n_hyp normalize nodelta
1298  <fetch_hyp normalize nodelta
1299  change with (
1300    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
1301  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
1302  >(le_to_leb_true … lt_hyp) %
1303qed.
1304
1305(* XXX: to be moved into common/Identifiers.ma *)
1306lemma lookup_present_add_hit:
1307  ∀tag, A, map, k, v, k_pres.
1308    lookup_present tag A (add … map k v) k k_pres = v.
1309  #tag #a #map #k #v #k_pres
1310  lapply (lookup_lookup_present … (add … map k v) … k_pres)
1311  >lookup_add_hit #Some_assm destruct(Some_assm)
1312  <e0 %
1313qed.
1314
1315lemma lookup_present_add_miss:
1316  ∀tag, A, map, k, k', v, k_pres', k_pres''.
1317    k' ≠ k →
1318      lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
1319  #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
1320  lapply (lookup_lookup_present … (add … map k v) ? k_pres')
1321  >lookup_add_miss try assumption
1322  #Some_assm
1323  lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
1324  lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
1325qed.
1326
1327(* XXX: to be moved into basics/types.ma *)
1328lemma not_None_to_Some:
1329  ∀A: Type[0].
1330  ∀o: option A.
1331    o ≠ None A → ∃v: A. o = Some A v.
1332  #A #o cases o
1333  [1:
1334    #absurd cases absurd #absurd' cases (absurd' (refl …))
1335  |2:
1336    #v' #ignore /2/
1337  ]
1338qed.
1339
1340lemma present_add_present:
1341  ∀tag, a, map, k, k', v.
1342    k' ≠ k →
1343      present tag a (add tag a map k v) k' →
1344        present tag a map k'.
1345  #tag #a #map #k #k' #v #neq_hyp #present_hyp
1346  whd in match present; normalize nodelta
1347  whd in match present in present_hyp; normalize nodelta in present_hyp;
1348  cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
1349  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
1350  [1:
1351    * #k_eq_hyp @⊥ /2/
1352  |2:
1353    #Some_eq_hyp' /2/
1354  ]
1355qed.
1356
1357lemma present_add_hit:
1358  ∀tag, a, map, k, v.
1359    present tag a (add tag a map k v) k.
1360  #tag #a #map #k #v
1361  whd >lookup_add_hit
1362  % #absurd destruct
1363qed.
1364
1365lemma present_add_miss:
1366  ∀tag, a, map, k, k', v.
1367    k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
1368  #tag #a #map #k #k' #v #neq_assm #present_assm
1369  whd >lookup_add_miss assumption
1370qed.
1371
1372lemma lt_to_le_to_le:
1373  ∀n, m, p: nat.
1374    n < m → m ≤ p → n ≤ p.
1375  #n #m #p #H #H1
1376  elim H
1377  [1:
1378    @(transitive_le n m p) /2/
1379  |2:
1380    /2/
1381  ]
1382qed.
1383
1384lemma eqb_decidable:
1385  ∀l, r: nat.
1386    (eqb l r = true) ∨ (eqb l r = false).
1387  #l #r //
1388qed.
1389
1390lemma r_Sr_and_l_r_to_Sl_r:
1391  ∀r, l: nat.
1392    (∃r': nat. r = S r' ∧ l = r') → S l = r.
1393  #r #l #exists_hyp
1394  cases exists_hyp #r'
1395  #and_hyp cases and_hyp
1396  #left_hyp #right_hyp
1397  destruct %
1398qed.
1399
1400lemma eqb_Sn_to_exists_n':
1401  ∀m, n: nat.
1402    eqb (S m) n = true → ∃n': nat. n = S n'.
1403  #m #n
1404  cases n
1405  [1:
1406    normalize #absurd
1407    destruct(absurd)
1408  |2:
1409    #n' #_ %{n'} %
1410  ]
1411qed.
1412
1413lemma eqb_true_to_eqb_S_S_true:
1414  ∀m, n: nat.
1415    eqb m n = true → eqb (S m) (S n) = true.
1416  #m #n normalize #assm assumption
1417qed.
1418
1419lemma eqb_S_S_true_to_eqb_true:
1420  ∀m, n: nat.
1421    eqb (S m) (S n) = true → eqb m n = true.
1422  #m #n normalize #assm assumption
1423qed.
1424
1425lemma eqb_true_to_refl:
1426  ∀l, r: nat.
1427    eqb l r = true → l = r.
1428  #l
1429  elim l
1430  [1:
1431    #r cases r
1432    [1:
1433      #_ %
1434    |2:
1435      #l' normalize
1436      #absurd destruct(absurd)
1437    ]
1438  |2:
1439    #l' #inductive_hypothesis #r
1440    #eqb_refl @r_Sr_and_l_r_to_Sl_r
1441    %{(pred r)} @conj
1442    [1:
1443      cases (eqb_Sn_to_exists_n' … eqb_refl)
1444      #r' #S_assm >S_assm %
1445    |2:
1446      cases (eqb_Sn_to_exists_n' … eqb_refl)
1447      #r' #refl_assm destruct normalize
1448      @inductive_hypothesis
1449      normalize in eqb_refl; assumption
1450    ]
1451  ]
1452qed.
1453
1454lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
1455  ∀r, l: nat.
1456    r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
1457  #r #l #disj_hyp
1458  cases disj_hyp
1459  [1:
1460    #r_O_refl destruct @nmk
1461    #absurd destruct(absurd)
1462  |2:
1463    #exists_hyp cases exists_hyp #r'
1464    #conj_hyp cases conj_hyp #left_conj #right_conj
1465    destruct @nmk #S_S_refl_hyp
1466    elim right_conj #hyp @hyp //
1467  ]
1468qed.
1469
1470lemma neq_l_r_to_neq_Sl_Sr:
1471  ∀l, r: nat.
1472    l ≠ r → S l ≠ S r.
1473  #l #r #l_neq_r_assm
1474  @nmk #Sl_Sr_assm cases l_neq_r_assm
1475  #assm @assm //
1476qed.
1477
1478lemma eqb_false_to_not_refl:
1479  ∀l, r: nat.
1480    eqb l r = false → l ≠ r.
1481  #l
1482  elim l
1483  [1:
1484    #r cases r
1485    [1:
1486      normalize #absurd destruct(absurd)
1487    |2:
1488      #r' #_ @nmk
1489      #absurd destruct(absurd)
1490    ]
1491  |2:
1492    #l' #inductive_hypothesis #r
1493    cases r
1494    [1:
1495      #eqb_false_assm
1496      @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
1497      @or_introl %
1498    |2:
1499      #r' #eqb_false_assm
1500      @neq_l_r_to_neq_Sl_Sr
1501      @inductive_hypothesis
1502      assumption
1503    ]
1504  ]
1505qed.
1506
1507lemma le_to_lt_or_eq:
1508  ∀m, n: nat.
1509    m ≤ n → m = n ∨ m < n.
1510  #m #n #le_hyp
1511  cases le_hyp
1512  [1:
1513    @or_introl %
1514  |2:
1515    #m' #le_hyp'
1516    @or_intror
1517    normalize
1518    @le_S_S assumption
1519  ]
1520qed.
1521
1522lemma le_neq_to_lt:
1523  ∀m, n: nat.
1524    m ≤ n → m ≠ n → m < n.
1525  #m #n #le_hyp #neq_hyp
1526  cases neq_hyp
1527  #eq_absurd_hyp
1528  generalize in match (le_to_lt_or_eq m n le_hyp);
1529  #disj_assm cases disj_assm
1530  [1:
1531    #absurd cases (eq_absurd_hyp absurd)
1532  |2:
1533    #assm assumption
1534  ]
1535qed.
1536
1537inverter nat_jmdiscr for nat.
1538
1539(* XXX: this is false in the general case.  For instance, if n = 0 then the
1540        base case requires us prove 1 = 0, as it is the carry bit that holds
1541        the result of the addition. *)
1542axiom succ_nat_of_bitvector_half_add_1:
1543  ∀n: nat.
1544  ∀bv: BitVector n.
1545  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
1546    S (nat_of_bitvector … bv) = nat_of_bitvector …
1547      (\snd (half_add n (bitvector_of_nat … 1) bv)).
1548
1549lemma plus_lt_to_lt:
1550  ∀m, n, o: nat.
1551    m + n < o → m < o.
1552  #m #n #o
1553  elim n
1554  [1:
1555    <(plus_n_O m) in ⊢ (% → ?);
1556    #assumption assumption
1557  |2:
1558    #n' #inductive_hypothesis
1559    <(plus_n_Sm m n') in ⊢ (% → ?);
1560    #assm @inductive_hypothesis
1561    normalize in assm; normalize
1562    /2 by lt_S_to_lt/
1563  ]
1564qed.
1565
1566definition nat_of_bool:
1567    bool → nat ≝
1568  λb: bool.
1569  match b with
1570  [ true ⇒ 1
1571  | false ⇒ 0
1572  ].
1573
1574axiom nat_of_bitvector_aux_accum:
1575  ∀m: nat.
1576  ∀v: BitVector m.
1577  ∀acc: nat.
1578    ∃n: nat.
1579      nat_of_bitvector_aux m acc v = n + nat_of_bitvector m v.
1580
1581axiom nat_of_bitvector_plus:
1582  ∀n: nat.
1583  ∀tl: BitVector n.
1584  ∀hd: bool.
1585    nat_of_bitvector (S n) (hd:::tl) = (2 ^ n) * nat_of_bool hd + nat_of_bitvector n tl.
1586
1587axiom mult_refl_to_refl_lor_refl:
1588  ∀m, m', n, n': nat.
1589    m * m' = n * n' → (m = n ∧ m' = n') ∨ (m = n' ∧ n = m').
1590
1591(*
1592lemma BitVector_inv_ind_2:
1593  ∀n: nat.
1594  ∀left: Vector bool n.
1595  ∀right: Vector bool n.
1596  ∀P: (∀m: nat. Vector bool m → Vector bool m → Prop).
1597    (n ≃ O → left ≃ VEmpty bool → right ≃ VEmpty bool → (P 0 [[ ]] [[ ]])) →
1598    (∀m: nat.
1599     ∀hd, hd': bool.
1600     ∀tl, tl': Vector bool m.
1601       (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') →
1602       (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) →
1603    P n left right.
1604  #n #left
1605  elim left
1606  [1:
1607    #right #P #base #step
1608    >(BitVector_O right)
1609    @base
1610    try %
1611    >(BitVector_O right) %
1612  |2:
1613    #n' #hd #tl #inductive_hypothesis #right #P #base #step
1614    cases (BitVector_Sn … right)
1615    #hd' #right_tail_exists_assm
1616    cases right_tail_exists_assm #right_tl #right_tl_refl
1617    destruct @step try %
1618    #n_refl' #left_refl #right_refl destruct
1619    @inductive_hypothesis
1620*)
1621
1622include "arithmetics/div_and_mod.ma".
1623
1624lemma n_plus_1_n_to_False:
1625  ∀n: nat.
1626    n + 1 = n → False.
1627  #n elim n
1628  [1:
1629    normalize #absurd destruct(absurd)
1630  |2:
1631    #n' #inductive_hypothesis normalize
1632    #absurd @inductive_hypothesis /2/
1633  ]
1634qed.
1635
1636lemma one_two_times_n_to_False:
1637  ∀n: nat.
1638    1=2*n→False.
1639  #n cases n
1640  [1:
1641    normalize #absurd destruct(absurd)
1642  |2:
1643    #n' normalize #absurd
1644    lapply (injective_S … absurd) -absurd #absurd
1645    /2/
1646  ]
1647qed.
1648
1649lemma generalized_nat_cases:
1650  ∀n: nat.
1651    n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m).
1652  #n
1653  cases n
1654  [1:
1655    @or_introl @or_introl %
1656  |2:
1657    #n' cases n'
1658    [1:
1659      @or_introl @or_intror %
1660    |2:
1661      #n'' @or_intror %{n''} %
1662    ]
1663  ]
1664qed.
1665
1666let rec odd_p
1667  (n: nat)
1668    on n ≝
1669  match n with
1670  [ O ⇒ False
1671  | S n' ⇒ even_p n'
1672  ]
1673and even_p
1674  (n: nat)
1675    on n ≝
1676  match n with
1677  [ O ⇒ True
1678  | S n' ⇒ odd_p n'
1679  ].
1680
1681let rec n_even_p_to_n_plus_2_even_p
1682  (n: nat)
1683    on n: even_p n → even_p (n + 2) ≝
1684  match n with
1685  [ O ⇒ ?
1686  | S n' ⇒ ?
1687  ]
1688and n_odd_p_to_n_plus_2_odd_p
1689  (n: nat)
1690    on n: odd_p n → odd_p (n + 2) ≝
1691  match n with
1692  [ O ⇒ ?
1693  | S n' ⇒ ?
1694  ].
1695  [1,3:
1696    normalize #assm assumption
1697  |2:
1698    normalize @n_odd_p_to_n_plus_2_odd_p
1699  |4:
1700    normalize @n_even_p_to_n_plus_2_even_p
1701  ]
1702qed.
1703
1704let rec two_times_n_even_p
1705  (n: nat)
1706    on n: even_p (2 * n) ≝
1707  match n with
1708  [ O ⇒ ?
1709  | S n' ⇒ ?
1710  ]
1711and two_times_n_plus_one_odd_p
1712  (n: nat)
1713    on n: odd_p ((2 * n) + 1) ≝
1714  match n with
1715  [ O ⇒ ?
1716  | S n' ⇒ ?
1717  ].
1718  [1,3:
1719    normalize @I
1720  |2:
1721    normalize
1722    >plus_n_Sm
1723    <(associative_plus n' n' 1)
1724    >(plus_n_O (n' + n'))
1725    cut(n' + n' + 0 + 1 = 2 * n' + 1)
1726    [1:
1727      //
1728    |2:
1729      #refl_assm >refl_assm
1730      @two_times_n_plus_one_odd_p     
1731    ]
1732  |4:
1733    normalize
1734    >plus_n_Sm
1735    cut(n' + (n' + 1) + 1 = (2 * n') + 2)
1736    [1:
1737      normalize /2/
1738    |2:
1739      #refl_assm >refl_assm
1740      @n_even_p_to_n_plus_2_even_p
1741      @two_times_n_even_p
1742    ]
1743  ]
1744qed.
1745
1746let rec even_p_to_not_odd_p
1747  (n: nat)
1748    on n: even_p n → ¬ odd_p n ≝
1749  match n with
1750  [ O ⇒ ?
1751  | S n' ⇒ ?
1752  ]
1753and odd_p_to_not_even_p
1754  (n: nat)
1755    on n: odd_p n → ¬ even_p n ≝
1756  match n with
1757  [ O ⇒ ?
1758  | S n' ⇒ ?
1759  ].
1760  [1:
1761    normalize #_
1762    @nmk #assm assumption
1763  |3:
1764    normalize #absurd
1765    cases absurd
1766  |2:
1767    normalize
1768    @odd_p_to_not_even_p
1769  |4:
1770    normalize
1771    @even_p_to_not_odd_p
1772  ]
1773qed.
1774
1775lemma even_p_odd_p_cases:
1776  ∀n: nat.
1777    even_p n ∨ odd_p n.
1778  #n elim n
1779  [1:
1780    normalize @or_introl @I
1781  |2:
1782    #n' #inductive_hypothesis
1783    normalize
1784    cases inductive_hypothesis
1785    #assm
1786    try (@or_introl assumption)
1787    try (@or_intror assumption)
1788  ]
1789qed.
1790
1791lemma two_times_n_plus_one_refl_two_times_n_to_False:
1792  ∀m, n: nat.
1793    2 * m + 1 = 2 * n → False.
1794  #m #n
1795  #assm
1796  cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
1797  [1:
1798    >assm
1799    @conj
1800    @two_times_n_even_p
1801  |2:
1802    * #_ #absurd
1803    cases (even_p_to_not_odd_p … absurd)
1804    #assm @assm
1805    @two_times_n_plus_one_odd_p
1806  ]
1807qed.
1808
1809(*
1810lemma two_times_m_plus_one_refl_2_times_n_to_m_refl_0_land_n_refl_1:
1811  ∀m, n: nat.
1812    2 * m + 1 = 2 * n → m = 0 ∧ n = 1.
1813(*
1814  #m #n
1815  lapply (generalized_nat_cases m)
1816  lapply (generalized_nat_cases n)
1817  #n_assms #m_assms
1818  cases n_assms
1819  [1:
1820    #left_n_assms
1821    cases left_n_assms #n_O_refl destruct
1822    normalize cases m normalize
1823    [1,3:
1824      #absurd destruct(absurd)
1825    |2,4:
1826      #m' normalize
1827      <plus_n_Sm <plus_n_Sm #absurd
1828      destruct(absurd)
1829    ]
1830  |2:
1831    #right_n_assms
1832    cases m_assms
1833    [1:
1834      #left_m_assms
1835      cases left_m_assms
1836      [1:
1837        #m_0_refl destruct normalize
1838        cases n
1839        [1:
1840          normalize
1841          #absurd destruct(absurd)
1842        |2:
1843          #n' normalize
1844          <plus_n_Sm #absurd
1845          destruct(absurd)
1846        ]
1847      |2:
1848        #m_1_refl destruct normalize
1849        cases n
1850        [1:
1851          normalize #absurd destruct(absurd)
1852        |2:
1853          #n' <plus_n_Sm #assm
1854          lapply (injective_S … assm)
1855          -assm #assm lapply (injective_S … assm)
1856          cases n'
1857          [1:
1858            normalize #absurd destruct(absurd)
1859          |2:
1860            #n'' normalize <plus_n_Sm #absurd destruct(absurd)
1861          ]
1862        ]
1863      ]
1864    |2:
1865      #right_m_assms cases right_n_assms cases right_m_assms
1866      #n' #n_assm #m' #m_assm destruct normalize
1867      <plus_n_Sm <plus_n_Sm <plus_n_Sm <plus_n_O <plus_n_O <plus_n_O <plus_n_Sm
1868      <plus_n_Sm #assm destruct(assm)
1869    ]
1870  ]
1871 
1872  #relevant_m
1873  cases relevant_m
1874  -relevant_m
1875  [1:
1876    lapply(generalized_nat_cases n)
1877    #relevant_n
1878    cases relevant_n
1879    -relevant_n
1880    [1:
1881      #relevant_n cases relevant_n
1882      #n_assm #relevant_m cases relevant_m
1883      #m_assm destruct normalize
1884      #absurd destruct(absurd)
1885    |2:
1886      #relevant_m cases relevant_m
1887*)
1888  cases daemon
1889qed.
1890*)
1891
1892lemma nat_of_bitvector_aux_injective:
1893  ∀n: nat.
1894  ∀l, r: BitVector n.
1895  ∀acc_l, acc_r: nat.
1896    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
1897      acc_l = acc_r ∧ l ≃ r.
1898  #n #l
1899  elim l #r
1900  [1:
1901    #acc_l #acc_r normalize
1902    >(BitVector_O r) normalize /2/
1903  |2:
1904    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
1905    normalize normalize in inductive_hypothesis;
1906    cases (BitVector_Sn … r)
1907    #r_hd * #r_tl #r_refl destruct normalize
1908    cases hd cases r_hd normalize
1909    [1:
1910      #relevant
1911      cases (inductive_hypothesis … relevant)
1912      #acc_assm #tl_assm destruct % //
1913      lapply (injective_plus_l ? ? ? acc_assm)
1914      -acc_assm #acc_assm
1915      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1916      lapply (injective_times_r ? ? ? ? acc_assm) /2/
1917    |4:
1918      #relevant
1919      cases (inductive_hypothesis … relevant)
1920      #acc_assm #tl_assm destruct % //
1921      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1922      lapply(injective_times_r ? ? ? ? acc_assm) /2/
1923    |2:
1924      #relevant 
1925      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
1926        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
1927      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
1928      [1:
1929        #eqb_true_assm
1930        lapply (eqb_true_to_refl … eqb_true_assm)
1931        #refl_assm
1932        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1933      |2:
1934        #eqb_false_assm
1935        lapply (eqb_false_to_not_refl … eqb_false_assm)
1936        #not_refl_assm cases not_refl_assm #absurd_assm
1937        cases (inductive_hypothesis … relevant) #absurd
1938        cases (absurd_assm absurd)
1939      ]
1940    |3:
1941      #relevant 
1942      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
1943        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
1944      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
1945      [1:
1946        #eqb_true_assm
1947        lapply (eqb_true_to_refl … eqb_true_assm)
1948        #refl_assm
1949        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
1950        -refl_assm #refl_assm
1951        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1952      |2:
1953        #eqb_false_assm
1954        lapply (eqb_false_to_not_refl … eqb_false_assm)
1955        #not_refl_assm cases not_refl_assm #absurd_assm
1956        cases (inductive_hypothesis … relevant) #absurd
1957        cases (absurd_assm absurd)
1958      ]
1959    ]
1960  ]
1961qed.
1962
1963lemma nat_of_bitvector_destruct:
1964  ∀n: nat.
1965  ∀l_hd, r_hd: bool.
1966  ∀l_tl, r_tl: BitVector n.
1967    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
1968      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
1969  #n #l_hd #r_hd #l_tl #r_tl
1970  normalize
1971  cases l_hd cases r_hd
1972  normalize
1973  [4:
1974    /2/
1975  |1:
1976    #relevant
1977    cases (nat_of_bitvector_aux_injective … relevant)
1978    #_ #l_r_tl_refl destruct /2/
1979  |2,3:
1980    #relevant
1981    cases (nat_of_bitvector_aux_injective … relevant)
1982    #absurd destruct(absurd)
1983  ]
1984qed.
1985
1986lemma BitVector_cons_injective:
1987  ∀n: nat.
1988  ∀l_hd, r_hd: bool.
1989  ∀l_tl, r_tl: BitVector n.
1990    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
1991  #l #l_hd #r_hd #l_tl #r_tl
1992  #l_refl #r_refl destruct %
1993qed.
1994
1995lemma refl_nat_of_bitvector_to_refl:
1996  ∀n: nat.
1997  ∀l, r: BitVector n.
1998    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
1999  #n
2000  elim n
2001  [1:
2002    #l #r
2003    >(BitVector_O l)
2004    >(BitVector_O r)
2005    #_ %
2006  |2:
2007    #n' #inductive_hypothesis #l #r
2008    lapply (BitVector_Sn ? l) #l_hypothesis
2009    lapply (BitVector_Sn ? r) #r_hypothesis
2010    cases l_hypothesis #l_hd #l_tail_hypothesis
2011    cases r_hypothesis #r_hd #r_tail_hypothesis
2012    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
2013    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
2014    destruct #cons_refl
2015    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
2016    #hd_refl #tl_refl
2017    @BitVector_cons_injective try assumption
2018    @inductive_hypothesis assumption
2019  ]
2020qed.
2021
2022let rec traverse_code_internal
2023  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
2024    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
2025      (reachable_program_counter_witness:
2026          ∀lbl: costlabel.
2027          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
2028            reachable_program_counter code_memory fixed_program_size program_counter)
2029        (good_program_witness: good_program code_memory fixed_program_size)
2030        (program_size_invariant: nat_of_bitvector … program_counter + program_size = fixed_program_size)
2031        (fixed_program_size_limit: fixed_program_size < 2^16 - 1)
2032        on program_size:
2033          Σcost_map: identifier_map CostTag nat.
2034            (∀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) ∧
2035            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
2036              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
2037                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
2038  match program_size return λx. x = program_size → Σcost_map: ?. ? with
2039  [ O ⇒ λprogram_size_refl. empty_map …
2040  | S program_size' ⇒ λprogram_size_refl. pi1 …
2041    (let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
2042    let 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
2043    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' fixed_program_size program_size' ? good_program_witness ? fixed_program_size_limit in
2044    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. (∀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) ∧
2045            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
2046              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
2047                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) with
2048    [ None ⇒ λlookup_refl. pi1 … cost_mapping
2049    | Some lbl ⇒ λlookup_refl.
2050      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
2051        add … cost_mapping lbl cost
2052    ] (refl … (lookup_opt … program_counter cost_labels)))
2053  ] (refl … program_size).
2054  cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
2055  [1:
2056    destruct
2057    @succ_nat_of_bitvector_half_add_1
2058    <plus_n_O in fixed_program_size_limit;
2059    #assumption assumption
2060  |3,5,7,9,11,13:
2061    destruct
2062    @succ_nat_of_bitvector_half_add_1
2063    @(plus_lt_to_lt ? (S program_size') (2^16 - 1))
2064    assumption
2065  |14:
2066    cases daemon (* XXX: russell error here i think *)
2067  |2:
2068    #_ %
2069    [1:
2070      #pc #k #absurd1 #absurd2
2071      @⊥ lapply(lt_to_not_le … absurd2) *
2072      #absurd @absurd assumption
2073    |2:
2074      #k #k_pres
2075      @⊥ normalize in k_pres; /2/
2076    ]
2077  |4:
2078    #S_assm
2079    cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
2080    [1:
2081      <NEW_PC' %
2082    |2:
2083      #new_program_counter_assm' >new_program_counter_assm'
2084      <program_size_invariant <program_size_refl
2085      <S_assm normalize <plus_n_Sm %
2086    ]
2087  |6:
2088    #_ assumption
2089  |8:
2090    #_ @(reachable_program_counter_witness lbl)
2091    assumption
2092  |10:
2093    #S_assm %
2094    [1:
2095      #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
2096      [1:
2097        #eq_assm >eq_assm
2098        cases cost_mapping #cost_mapping' * #ind_hyp #_
2099        @present_add_hit
2100      |2:
2101        #neq_assm @present_add_miss try assumption
2102        cases cost_mapping #cost_mapping' * #ind_hyp #_
2103        @(ind_hyp … lookup_opt_assm)
2104        [1:
2105          generalize in match (eqb_decidable (nat_of_bitvector … program_counter)
2106            (nat_of_bitvector … pc));
2107          #hyp cases hyp
2108          [1:
2109            #eqb_assm generalize in match (eqb_true_to_refl … eqb_assm);
2110            #eqb_refl_assm
2111            -eqb_assm -hyp -ind_hyp -H1 -H2
2112            lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
2113            #program_counter_refl_assm -eqb_refl_assm
2114            <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
2115            #Some_assm destruct(Some_assm)
2116            cases neq_assm #absurd_assm
2117            cases (absurd_assm (refl … k))
2118          |2:
2119            #eqb_assm generalize in match (eqb_false_to_not_refl … eqb_assm);
2120            #eqb_refl_assm
2121            -eqb_assm -hyp -ind_hyp -H1 -H2 -cost_mapping -traverse_code_internal
2122            <NEW_PC' in S_assm; #relevant <relevant -relevant
2123            cases daemon (* XXX: ??? *)
2124          ]
2125        |2:
2126          generalize in match H2; <program_size_refl whd in ⊢ (??% → ?);
2127          >plus_n_Sm in ⊢ (% → ?);
2128          cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
2129          [1:
2130            <NEW_PC' %
2131          |2:
2132            #new_program_counter_assm' >new_program_counter_assm'
2133            >S_assm #relevant assumption
2134          ]
2135        ]
2136      ]
2137    |2:
2138      #k #k_pres
2139      @(eq_identifier_elim … k lbl)
2140      [1:
2141        #eq_assm %{program_counter} #lookup_opt_assm
2142        %{(reachable_program_counter_witness …)} try assumption
2143        >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
2144      |2:
2145        #neq_assm
2146        cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
2147        cases ind_hyp #_ #relevant cases (relevant k ?)
2148        [2:
2149          @(present_add_present … present_assm) assumption
2150        |1:
2151          #program_counter' #ind_hyp' %{program_counter'}
2152          #relevant cases (ind_hyp' relevant) #reachable_witness'
2153          #ind_hyp'' %{reachable_witness'} >ind_hyp''
2154          @sym_eq @lookup_present_add_miss assumption
2155        ]
2156      ]
2157    ]
2158  |12:
2159    #S_assm %
2160    [1:
2161      #pc #k #H1 #H2 #lookup_opt_assm
2162      whd
2163    |2:
2164      #k #k_pres
2165    ]
2166  ]
2167   
2168  |5:
2169    %
2170    [2:
2171      #k #k_pres
2172      @(eq_identifier_elim … k lbl)
2173      [1:
2174        #eq_assm %{program_counter} #lookup_opt_assm
2175        %{(reachable_program_counter_witness …)} try assumption
2176        >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
2177      |2:
2178        #neq_assm
2179        cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
2180        cases ind_hyp #_ #relevant cases (relevant k ?)
2181        [2:
2182          @(present_add_present … present_assm) assumption
2183        |1:
2184          #program_counter' #ind_hyp' %{program_counter'}
2185          #relevant cases (ind_hyp' relevant) #reachable_witness'
2186          #ind_hyp'' %{reachable_witness'} >ind_hyp''
2187          @sym_eq @lookup_present_add_miss assumption
2188        ]
2189      ]
2190    |1:
2191      #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
2192      [1:
2193        #eq_assm >eq_assm
2194        cases cost_mapping #cost_mapping' * #ind_hyp #_
2195        @present_add_hit
2196      |2:
2197        #neq_assm @present_add_miss try assumption
2198        cases cost_mapping #cost_mapping' * #ind_hyp #_
2199        @(ind_hyp … lookup_opt_assm)
2200        [1:
2201          generalize in match (eqb_decidable (nat_of_bitvector … program_counter)
2202            (nat_of_bitvector … pc));
2203          #hyp cases hyp
2204          [1:
2205            #relevant
2206            generalize in match (eqb_true_to_refl … relevant);
2207            #rewrite_assm <rewrite_assm
2208          |2:
2209            #relevant
2210            generalize in match (eqb_false_to_not_refl … relevant);
2211            #rewrite_assm
2212            @⊥
2213            cases rewrite_assm #relevant @relevant -relevant
2214            -rewrite_assm -relevant -hyp
2215          ]
2216          (* XXX: case analysis over pc = new_program_counter' *)
2217        |2:
2218          generalize in match H2; whd in ⊢ (??% → ?);
2219          >plus_n_Sm in ⊢ (% → ?);
2220          cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
2221          [1:
2222            <NEW_PC' %
2223          |2:
2224            #new_program_counter_assm' >new_program_counter_assm'
2225            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
2226            [1:
2227              (* XXX: todo *)
2228            |2:
2229              #S_program_counter_assm >S_program_counter_assm
2230              #relevant <program_size_refl in relevant;
2231              change with (
2232                nat_of_bitvector 16 pc < S (program_size'+nat_of_bitvector 16 program_counter)
2233              ) in ⊢ (% → ?);
2234              >plus_n_Sm in ⊢ (% → ?);
2235              <S_program_counter_assm
2236              #relevant assumption
2237            ]
2238          ]
2239        ]
2240      ]
2241    ]
2242  |6:
2243  ]
2244qed.
2245
2246
2247
2248let rec traverse_code_internal
2249  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
2250    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
2251      (label_map_correctness_:
2252          ∀lbl: costlabel.
2253          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
2254            reachable_program_counter code_memory fixed_program_size program_counter)
2255        (good_program_witness: good_program code_memory fixed_program_size)
2256        on program_size:
2257          fixed_program_size < nat_of_bitvector … program_counter + program_size →
2258          Σcost_map: identifier_map CostTag nat.
2259            (∀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) ∧
2260            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
2261              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
2262                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
2263  match program_size return λx. fixed_program_size < nat_of_bitvector … program_counter + x → Σx: ?. ? with
2264  [ O ⇒ λabsrd. ⊥
2265  | S program_size' ⇒ λstep_case.
2266    (let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in
2267      if ltb (nat_of_bitvector … new_program_counter) fixed_program_size then
2268        let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size' ? good_program_witness ? in
2269        match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
2270        [ None ⇒ λlookup_refl. pi1 … cost_mapping
2271        | Some lbl ⇒ λlookup_refl.
2272          let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
2273            add … cost_mapping lbl cost
2274        ] (refl … (lookup_opt … program_counter cost_labels))
2275      else
2276        (empty_map ? ?))
2277  ].
2278  [2:
2279    @pi2
2280  |6:
2281    @(reachable_program_counter_witness lbl)
2282    assumption
2283  |8:
2284    assumption
2285  |3:
2286  (*
2287    %
2288    [1:
2289      #pc #k #absurd1 #absurd2
2290      @⊥ lapply(lt_to_not_le … absurd1) #absurd
2291      cases absurd #absurd @absurd
2292      @(lt_to_le_to_le … absurd2)
2293      @(transitive_le)
2294    |2:
2295      #k #k_pres
2296      @⊥ normalize in k_pres; /2/
2297    ] *)
2298  |1:
2299    generalize in match (reachable_program_counter_to_0_lt_total_program_size code_memory program_counter fixed_program_size);
2300    #reachable_program_counter_assm
2301    letin dummy_cost_label ≝ (an_identifier CostTag one)
2302    lapply (reachable_program_counter_witness dummy_cost_label program_counter)
2303    normalize in absurd;
2304  |5:
2305    %
2306    [2:
2307      #k #k_pres
2308      @(eq_identifier_elim … k lbl)
2309      [1:
2310        #eq_assm %{program_counter} #lookup_opt_assm
2311        %{(reachable_program_counter_witness …)} try assumption
2312        >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
2313      |2:
2314        #neq_assm
2315        cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
2316        cases ind_hyp #_ #relevant cases (relevant k ?)
2317        [2:
2318          @(present_add_present … present_assm) assumption
2319        |1:
2320          #program_counter' #ind_hyp' %{program_counter'}
2321          #relevant cases (ind_hyp' relevant) #reachable_witness'
2322          #ind_hyp'' %{reachable_witness'} >ind_hyp''
2323          @sym_eq @lookup_present_add_miss assumption
2324        ]
2325      ]
2326    |1:
2327      #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
2328      [1:
2329        #eq_assm >eq_assm
2330        cases cost_mapping #cost_mapping' * #ind_hyp #_
2331        @present_add_hit
2332      |2:
2333        #neq_assm @present_add_miss try assumption
2334        cases cost_mapping #cost_mapping' * #ind_hyp #_
2335        cases daemon (* XXX: !!! *)
2336      ]
2337    ]
2338  |6:
2339  ]
2340qed.
2341
2342definition traverse_code:
2343  ∀code_memory: BitVectorTrie Byte 16.
2344  ∀cost_labels: BitVectorTrie costlabel 16.
2345  ∀program_size: nat.
2346  ∀reachable_program_counter_witness:
2347    ∀lbl: costlabel.
2348    ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
2349      reachable_program_counter code_memory program_size program_counter.
2350  ∀good_program_witness: good_program code_memory program_size.
2351    Σcost_map: identifier_map CostTag nat.
2352      (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
2353        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
2354          pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
2355  λcode_memory: BitVectorTrie Byte 16.
2356  λcost_labels: BitVectorTrie costlabel 16.
2357  λprogram_size: nat.
2358  λreachable_program_counter_witness:
2359          ∀lbl: costlabel.
2360          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
2361            reachable_program_counter code_memory program_size program_counter.
2362  λgood_program_witness: good_program code_memory program_size.
2363    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
2364 
2365definition compute_costs ≝
2366  λprogram: list Byte.
2367  λcost_labels: BitVectorTrie costlabel 16.
2368  λreachable_program_witness.
2369  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
2370    let program_size ≝ |program| + 1 in
2371    let code_memory ≝ load_code_memory program in
2372      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
2373  @good_program_witness
2374qed.
Note: See TracBrowser for help on using the repository browser.