source: src/ASM/ASMCosts.ma @ 1901

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

Slight changes to StructuredTraces?: should not change too much

File size: 72.5 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5include "common/StructuredTraces.ma".
6
7let rec fetch_program_counter_n
8  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
9    on n: option Word ≝
10  match n with
11  [ O ⇒ Some … program_counter
12  | S n ⇒
13    match fetch_program_counter_n n code_memory program_counter with
14    [ None ⇒ None …
15    | Some tail_pc ⇒
16      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
17        if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
18          Some … program_counter
19        else
20          None Word (* XXX: overflow! *)
21    ]
22  ].
23   
24definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
25  λcode_memory: BitVectorTrie Byte 16.
26  λprogram_size: nat.
27  λprogram_counter: Word.
28    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
29        nat_of_bitvector 16 program_counter < program_size.
30   
31definition 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 program_counters_properly_related:
386    ∀code_memory: BitVectorTrie Byte 16. Status code_memory → Status code_memory → Prop ≝
387  λcode_memory: BitVectorTrie Byte 16.
388  λbefore: Status code_memory.
389  λafter: Status code_memory.
390    let program_counter_before ≝ program_counter ? code_memory before in
391    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
392      program_counter ? code_memory after = program_counter_after.
393
394definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
395  λcode_memory.
396  λcost_labels.
397    mk_abstract_status
398      (Status code_memory)
399      (λs,s'. (execute_1 … s) = s')
400      (λs,class. ASM_classify … s = class)
401      (current_instruction_is_labelled … cost_labels)
402      (next_instruction_properly_relates_program_counters code_memory)
403      (program_counters_properly_related code_memory).
404
405let rec trace_any_label_length
406  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
407    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
408      (final_status: Status code_memory)
409      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
410        on the_trace: nat ≝
411  match the_trace with
412  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
413  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace _ ⇒ 0
414  | tal_base_return the_status _ _ _ ⇒ 0
415  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ _ call_trace _ final_trace ⇒
416      let tail_length ≝ trace_any_label_length … final_trace in
417      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
418        pc_difference + tail_length
419  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
420      let tail_length ≝ trace_any_label_length … tail_trace in
421      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
422        pc_difference + tail_length       
423  ].
424
425let rec compute_paid_trace_any_label
426  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
427    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
428      (final_status: Status code_memory)
429        (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
430       on the_trace: nat ≝
431  match the_trace with
432  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
433  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
434  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call
435  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
436     _ _ _ _ call_trace _ final_trace ⇒
437      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
438      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
439        current_instruction_cost + final_trace_cost
440  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
441      let current_instruction_cost ≝ current_instruction_cost … status_pre in
442      let tail_trace_cost ≝
443       compute_paid_trace_any_label … cost_labels end_flag
444        status_init status_end tail_trace
445      in
446        current_instruction_cost + tail_trace_cost
447  ].
448
449definition compute_paid_trace_label_label ≝
450  λcode_memory: BitVectorTrie Byte 16.
451  λcost_labels: BitVectorTrie costlabel 16.
452  λtrace_ends_flag: trace_ends_with_ret.
453  λstart_status: Status code_memory.
454  λfinal_status: Status code_memory.
455  λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
456  match the_trace with
457  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
458      compute_paid_trace_any_label … given_trace
459  ].
460
461include alias "arithmetics/nat.ma".
462include alias "basics/logic.ma".
463
464lemma plus_right_monotone:
465  ∀m, n, o: nat.
466    m = n → m + o = n + o.
467  #m #n #o #refl >refl %
468qed.
469
470lemma plus_left_monotone:
471  ∀m, n, o: nat.
472    m = n → o + m = o + n.
473  #m #n #o #refl destruct %
474qed.
475
476lemma minus_plus_cancel:
477  ∀m, n : nat.
478  ∀proof: n ≤ m.
479    (m - n) + n = m.
480  #m #n #proof /2 by plus_minus/
481qed.
482
483(* XXX: indexing bug *)
484lemma fetch_twice_fetch_execute_1:
485  ∀code_memory: BitVectorTrie Byte 16.
486  ∀start_status: Status code_memory.
487    ASM_classify code_memory start_status = cl_other →
488    \snd (\fst (fetch code_memory (program_counter … start_status))) =
489      program_counter … (execute_1 … start_status).
490  #code_memory #start_status #classify_assm
491  whd in match execute_1; normalize nodelta
492  cases (execute_1' code_memory start_status) #the_status
493  * #_ #classify_assm' @classify_assm' assumption
494qed-.
495
496lemma reachable_program_counter_to_0_lt_total_program_size:
497  ∀code_memory: BitVectorTrie Byte 16.
498  ∀program_counter: Word.
499  ∀total_program_size: nat.
500    reachable_program_counter code_memory total_program_size program_counter →
501      0 < total_program_size.
502  #code_memory #program_counter #total_program_size
503  whd in match reachable_program_counter; normalize nodelta * * #some_n
504  #_ cases (nat_of_bitvector 16 program_counter)
505  [1:
506    #assm assumption
507  |2:
508    #new_pc @ltn_to_ltO
509  ]
510qed.
511
512lemma trace_compute_paid_trace_cl_other:
513  ∀code_memory' : (BitVectorTrie Byte 16).
514  ∀program_counter' : Word.
515  ∀total_program_size : ℕ.
516  ∀cost_labels : (BitVectorTrie costlabel 16).
517  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
518  ∀good_program_witness : (good_program code_memory' total_program_size).
519  ∀program_size' : ℕ.
520  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
521  ∀ticks : ℕ.
522  ∀instruction : instruction.
523  ∀program_counter'' : Word.
524  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
525  ∀start_status : (Status code_memory').
526  ∀final_status : (Status code_memory').
527  ∀trace_ends_flag : trace_ends_with_ret.
528  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
529  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
530  ∀classify_assm: ASM_classify0 instruction = cl_other.
531  ∀pi1 : ℕ.
532   (if match lookup_opt costlabel 16 program_counter'' cost_labels with 
533         [None ⇒ true
534         |Some _ ⇒ false
535         ] 
536    then
537      ∀start_status0:Status code_memory'.
538      ∀final_status0:Status code_memory'.
539      ∀trace_ends_flag0:trace_ends_with_ret.
540      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
541        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
542        (∃n:ℕ.
543            trace_any_label_length code_memory' cost_labels
544              trace_ends_flag0 start_status0 final_status0 the_trace0
545                + S n
546                  = total_program_size) ∧
547                  pi1
548                    =compute_paid_trace_any_label code_memory' cost_labels
549                     trace_ends_flag0 start_status0 final_status0 the_trace0
550    else (pi1=O) )
551   →(∃n:ℕ.
552     trace_any_label_length code_memory' cost_labels trace_ends_flag
553      start_status final_status the_trace
554      +S n
555      =total_program_size)
556    ∧ticks+pi1
557     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
558      start_status final_status the_trace.
559  #code_memory' #program_counter' #total_program_size #cost_labels
560  #reachable_program_counter_witness #good_program_witness
561  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
562  #start_status #final_status
563  #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
564  #recursive_assm
565  @(trace_any_label_inv_ind … the_trace)
566    [5:
567      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
568      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
569      #the_trace_refl
570      destruct
571      whd in match (trace_any_label_length … (tal_step_default …));
572      whd in match (compute_paid_trace_any_label … (tal_step_default …));
573      whd in costed_assm:(?%);
574      generalize in match costed_assm;
575      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
576      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
577        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
578      #lookup_assm cases lookup_assm
579      [1:
580        #None_lookup_opt_assm normalize nodelta #ignore
581        generalize in match recursive_assm;
582        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
583        [1:
584          <fetch_twice_fetch_execute_1
585          [1:
586            <FETCH %
587          |2:
588            >classifier_assm %
589          ]
590        |2:
591          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
592          normalize nodelta #new_recursive_assm
593          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
594            end_flag trace_any_label ?) try %
595          #exists_assm #recursive_block_cost_assm %
596          [1:
597            cases exists_assm #exists_n #total_program_size_refl
598            <total_program_size_refl
599            %{(exists_n - (nat_of_bitvector 16
600                (program_counter (BitVectorTrie Byte 16) code_memory'
601                  (execute_1 code_memory' status_pre))
602                - nat_of_bitvector 16
603                  (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))}
604            <plus_n_Sm <plus_n_Sm @eq_f >commutative_plus
605            cases daemon
606          |2:
607            >recursive_block_cost_assm
608            whd in match (current_instruction_cost … status_pre);
609            cut(ticks = \snd (fetch code_memory'
610               (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
611            [1:
612              <FETCH %
613            |2:
614              #ticks_refl_assm >ticks_refl_assm %
615            ]
616          ]
617        ]
618      |2:
619        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
620        #absurd cases absurd #absurd cases(absurd I)
621      ]
622    |1:
623      #status_start #status_final #execute_assm #classifier_assm #costed_assm
624      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
625      destruct
626      whd in match (trace_any_label_length … (tal_base_not_return …));
627      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
628      whd in costed_assm;
629      generalize in match costed_assm;
630      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
631      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
632        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
633      #lookup_assm cases lookup_assm
634      [1:
635        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
636        #absurd cases absurd
637      |2:
638        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
639        generalize in match recursive_assm;
640        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
641        [1:
642          <fetch_twice_fetch_execute_1
643          [1:
644            <FETCH %
645          |2:
646            cases classifier_assm
647            [1:
648              whd in ⊢ (% → ?);
649              whd in ⊢ (??%? → ?);
650              whd in match (current_instruction code_memory' status_start);
651              <FETCH generalize in match classify_assm;
652              cases instruction
653              [8:
654                #preinstruction normalize nodelta
655                whd in match ASM_classify0; normalize nodelta
656                #contradiction >contradiction #absurd destruct(absurd)
657              ]
658              try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
659              try(#addr normalize nodelta #ignore #absurd destruct(absurd))
660              normalize in ignore; destruct(ignore)
661            |2:
662              #classifier_assm' >classifier_assm' %
663            ]
664          ]
665        |2:
666          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
667          normalize nodelta #new_recursive_assm >new_recursive_assm %
668          [1:
669            %{(pred total_program_size)} whd in ⊢ (??%?);
670            @S_pred
671            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
672          |2:
673            cut(ticks = \snd (fetch code_memory'
674               (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
675            [1:
676              <FETCH %
677            |2:
678              #ticks_refl_assm >ticks_refl_assm
679              <plus_n_O %
680            ]
681          ]
682        ]
683      ]
684    |2:
685      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
686      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
687    |3:
688      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
689      #classifier_assm #after_return_assm #trace_label_return #costed_assm
690      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
691      destruct @⊥
692    |4:
693      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
694      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
695      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
696      #final_status_refl #the_trace_refl destruct @⊥
697    ]
698  change with (ASM_classify0 ? = ?) in classifier_assm;
699  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
700  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
701  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
702qed.
703
704lemma trace_compute_paid_trace_cl_jump:
705  ∀code_memory': BitVectorTrie Byte 16.
706  ∀program_counter': Word.
707  ∀total_program_size: ℕ.
708  ∀cost_labels: BitVectorTrie costlabel 16.
709  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
710  ∀good_program_witness: good_program code_memory' total_program_size.
711  ∀first_time_around: bool.
712  ∀program_size': ℕ.
713  ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'.
714  ∀ticks: ℕ.
715  ∀instruction: instruction.
716  ∀program_counter'': Word.
717  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
718  ∀start_status: (Status code_memory').
719  ∀final_status: (Status code_memory').
720  ∀trace_ends_flag: trace_ends_with_ret.
721  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
722  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
723  ∀classify_assm: ASM_classify0 instruction = cl_jump.
724   (∃n:ℕ
725     .trace_any_label_length code_memory' cost_labels trace_ends_flag
726      start_status final_status the_trace
727      +S n
728      =total_program_size)
729    ∧ticks
730     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
731      start_status final_status the_trace.
732  #code_memory' #program_counter' #total_program_size #cost_labels
733  #reachable_program_counter_witness #good_program_witness #first_time_around
734  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
735  #start_status #final_status
736  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
737  @(trace_any_label_inv_ind … the_trace)
738  [5:
739    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
740    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
741    #the_trace_refl destruct @⊥
742  |1:
743    #status_start #status_final #execute_assm #classifier_assm #costed_assm
744    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
745    destruct
746    whd in match (trace_any_label_length … (tal_base_not_return …));
747    whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); %
748    [1:
749      %{(pred total_program_size)} whd in ⊢ (??%?);
750      @S_pred
751      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
752    |2:
753      <FETCH %
754    ]
755  |2:
756    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
757    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
758  |3:
759    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
760    #classifier_assm #after_return_assm #trace_label_return #costed_assm
761    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
762    destruct @⊥
763  |4:
764    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
765    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
766    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
767    #final_status_refl #the_trace_refl destruct @⊥
768  ]
769  change with (ASM_classify0 ? = ?) in classifier_assm;
770  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
771  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
772  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
773qed.
774
775lemma trace_compute_paid_trace_cl_call:
776  ∀code_memory' : (BitVectorTrie Byte 16).
777  ∀program_counter' : Word.
778  ∀total_program_size : ℕ.
779  ∀cost_labels : (BitVectorTrie costlabel 16).
780  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
781  ∀good_program_witness : (good_program code_memory' total_program_size).
782  ∀program_size' : ℕ.
783  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
784  ∀ticks : ℕ.
785  ∀instruction : instruction.
786  ∀program_counter'' : Word.
787  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
788  ∀start_status : (Status code_memory').
789  ∀final_status : (Status code_memory').
790  ∀trace_ends_flag : trace_ends_with_ret.
791  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
792  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
793  ∀classify_assm: ASM_classify0 instruction = cl_call.
794  (∀pi1:ℕ
795  .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
796      [None ⇒ true | Some _ ⇒ false] 
797   then (∀start_status0:Status code_memory'
798             .∀final_status0:Status code_memory'
799              .∀trace_ends_flag0:trace_ends_with_ret
800               .∀the_trace0:trace_any_label
801                                        (ASM_abstract_status code_memory' cost_labels)
802                                        trace_ends_flag0 start_status0 final_status0
803                .program_counter''
804                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
805                 →(∃n:ℕ
806                   .trace_any_label_length code_memory' cost_labels trace_ends_flag0
807                    start_status0 final_status0 the_trace0
808                    +S n
809                    =total_program_size)
810                  ∧pi1
811                   =compute_paid_trace_any_label code_memory' cost_labels
812                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
813   else (pi1=O) 
814   →(∃n:ℕ
815     .trace_any_label_length code_memory' cost_labels trace_ends_flag
816      start_status final_status the_trace
817      +S n
818      =total_program_size)
819    ∧ticks+pi1
820     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
821      start_status final_status the_trace).
822  #code_memory' #program_counter' #total_program_size #cost_labels
823  #reachable_program_counter_witness #good_program_witness #program_size'
824  #recursive_case #ticks #instruction #program_counter'' #FETCH
825  #start_status #final_status #trace_ends_flag
826  #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
827  @(trace_any_label_inv_ind … the_trace)
828  [5:
829    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
830    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
831    #the_trace_refl destruct @⊥
832  |1:
833    #status_start #status_final #execute_assm #classifier_assm #costed_assm
834    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
835    destruct @⊥
836  |2:
837    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
838    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
839  |3:
840    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
841    #classifier_assm #after_return_assm #trace_label_return #costed_assm
842    #program_counters_properly_related_assm #ends_flag_refl #start_status_refl
843    #final_status_refl #the_trace_refl
844    destruct
845    whd in match (trace_any_label_length … (tal_base_call …));
846    whd in match (compute_paid_trace_any_label … (tal_base_call …));
847    whd in costed_assm;
848    generalize in match costed_assm;
849    generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
850    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
851      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
852    #lookup_assm cases lookup_assm
853    [1:
854      #None_lookup_opt normalize nodelta #absurd cases absurd
855    |2:
856      #costlabel #Some_lookup_opt normalize nodelta #ignore
857      generalize in match recursive_assm;
858      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
859      [1:
860        generalize in match program_counters_properly_related_assm;
861        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
862      |2:
863        #program_counter_assm >program_counter_assm <Some_lookup_opt
864        normalize nodelta #new_recursive_assm >new_recursive_assm %
865        [1:
866          %{(pred total_program_size)} whd in ⊢ (??%?);
867          @S_pred
868          @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
869        |2:
870          cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
871          [1:
872            <FETCH %
873          |2:
874            #ticks_refl_assm >ticks_refl_assm
875            <plus_n_O %
876          ]
877        ]
878      ]
879    ]
880  |4:
881    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
882    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
883    #costed_assm #program_counters_properly_related_assm #trace_any_label
884    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
885    generalize in match execute_assm; destruct #execute_assm
886    whd in match (trace_any_label_length … (tal_step_call …));
887    whd in match (compute_paid_trace_any_label … (tal_step_call …));
888    whd in costed_assm:(?%);
889    generalize in match costed_assm;
890    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
891    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
892      in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
893    #lookup_assm cases lookup_assm
894    [1:
895      #None_lookup_opt_assm normalize nodelta #ignore
896      generalize in match recursive_assm;
897      cut(program_counter'' = program_counter … status_after_fun_call)
898      [1:
899        generalize in match program_counters_properly_related_assm;
900        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
901      |2:
902        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
903        normalize nodelta #new_recursive_assm %
904        cases (new_recursive_assm … trace_any_label ?)
905        [1,3:
906          #exists_assm #recursive_block_cost_assm
907          [2:
908            >recursive_block_cost_assm
909            @plus_right_monotone
910            whd in ⊢ (???%); <FETCH %
911          |1:
912            cases exists_assm #exists_n #trace_total_program_size_assm
913            generalize in match execute_assm; destruct #execute_assm
914            %{(exists_n - ((nat_of_bitvector … (program_counter … status_after_fun_call)
915                - nat_of_bitvector … (program_counter … status_pre_fun_call))))}
916            >commutative_plus in ⊢ (??(?%?)?);
917            <plus_n_Sm <plus_n_Sm @eq_f >associative_plus in ⊢ (??%?);
918            @plus_left_monotone @sym_eq <commutative_plus in ⊢ (???%);
919            @plus_minus_m_m
920            cases daemon (* XXX: !!! *)
921          ]
922        |2,4:
923          %
924        ]
925      ]
926    |2:
927      #cost_label #Some_lookup_opt_assm normalize nodelta #absurd
928      cases absurd #absurd cases (absurd I)
929    ]
930  ]
931  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
932  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
933  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
934  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
935  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
936  #absurd destruct(absurd)
937qed.
938
939lemma trace_compute_paid_trace_cl_return:
940  ∀code_memory' : (BitVectorTrie Byte 16).
941  ∀program_counter' : Word.
942  ∀total_program_size : ℕ.
943  ∀cost_labels : (BitVectorTrie costlabel 16).
944  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
945  ∀good_program_witness : (good_program code_memory' total_program_size).
946  ∀program_size' : ℕ.
947  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
948  ∀ticks : ℕ.
949  ∀instruction : instruction.
950  ∀program_counter'' : Word.
951  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
952  ∀start_status : (Status code_memory').
953  ∀final_status : (Status code_memory').
954  ∀trace_ends_flag : trace_ends_with_ret.
955  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
956  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
957  ∀classify_assm: ASM_classify0 instruction = cl_return.
958    (∃n:ℕ
959     .trace_any_label_length code_memory' cost_labels trace_ends_flag
960      start_status final_status the_trace
961      +S n
962      =total_program_size)
963    ∧ticks
964     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
965      start_status final_status the_trace.
966  #code_memory' #program_counter' #total_program_size #cost_labels
967  #reachable_program_counter_witness #good_program_witness #program_size'
968  #recursive_case #ticks #instruction #program_counter'' #FETCH
969  #start_status #final_status #trace_ends_flag
970  #the_trace #program_counter_refl #classify_assm
971  @(trace_any_label_inv_ind … the_trace)
972  [1:
973    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
974    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
975    destruct @⊥
976  |2:
977    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
978    #start_status_refl #final_status_refl #the_trace_refl destruct
979    whd in match (trace_any_label_length … (tal_base_return …));
980    whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
981    [1:
982      %{(pred total_program_size)} whd in ⊢ (??%?);
983      @S_pred
984      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
985    |2:
986      <FETCH %
987    ]
988  |3:
989    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
990    #classifier_assm #after_return_assm #trace_label_return #costed_assm
991    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
992    destruct @⊥
993  |4:
994    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
995    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
996    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
997    #final_status_refl #the_trace_refl
998    destruct @⊥
999  |5:
1000    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
1001    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
1002    #final_status_refl #the_trace_refl destruct @⊥
1003  ]
1004  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
1005  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
1006  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1007  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1008  <FETCH in classifier_assm; >classify_assm
1009  #absurd try (destruct(absurd))
1010  cases absurd
1011  #absurd destruct(absurd)
1012qed.
1013     
1014let rec block_cost'
1015  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
1016    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
1017      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
1018        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
1019          on program_size:
1020          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
1021          Σcost_of_block: nat.
1022          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
1023            ∀start_status: Status code_memory'.
1024            ∀final_status: Status code_memory'.
1025            ∀trace_ends_flag.
1026            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1027              program_counter' = program_counter … start_status →
1028                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1029                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
1030          else
1031            (cost_of_block = 0) ≝
1032  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
1033  [ O ⇒ λbase_case. ⊥
1034  | S program_size' ⇒ λrecursive_case.
1035    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
1036    let to_continue ≝
1037      match lookup_opt … program_counter' cost_labels with
1038      [ None ⇒ true
1039      | Some _ ⇒ first_time_around
1040      ]
1041    in
1042      ((if to_continue then
1043       pi1 … (match instruction return λx. x = instruction → ? with
1044        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
1045          match real_instruction return λx. x = real_instruction →
1046          Σcost_of_block: nat.
1047            ∀start_status: Status code_memory'.
1048            ∀final_status: Status code_memory'.
1049            ∀trace_ends_flag.
1050            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
1051              program_counter' = program_counter … start_status →
1052                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1053                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
1054          [ RET                    ⇒ λinstr. ticks
1055          | RETI                   ⇒ λinstr. ticks
1056          | JC   relative          ⇒ λinstr. ticks
1057          | JNC  relative          ⇒ λinstr. ticks
1058          | JB   bit_addr relative ⇒ λinstr. ticks
1059          | JNB  bit_addr relative ⇒ λinstr. ticks
1060          | JBC  bit_addr relative ⇒ λinstr. ticks
1061          | JZ   relative          ⇒ λinstr. ticks
1062          | JNZ  relative          ⇒ λinstr. ticks
1063          | CJNE src_trgt relative ⇒ λinstr. ticks
1064          | DJNZ src_trgt relative ⇒ λinstr. ticks
1065          | _                      ⇒ λinstr.
1066         
1067              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1068          ] (refl …)
1069        | ACALL addr     ⇒ λinstr.
1070            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1071        | AJMP  addr     ⇒ λinstr. ticks
1072        | LCALL addr     ⇒ λinstr.
1073            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1074        | LJMP  addr     ⇒ λinstr. ticks
1075        | SJMP  addr     ⇒ λinstr. ticks
1076        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
1077            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1078        | MOVC  src trgt ⇒ λinstr.
1079            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
1080        ] (refl …))
1081      else
1082        0)
1083      : Σcost_of_block: nat.
1084          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
1085          [ true ⇒
1086            ∀start_status: Status code_memory'.
1087            ∀final_status: Status code_memory'.
1088            ∀trace_ends_flag.
1089            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1090              program_counter' = program_counter … start_status →
1091                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1092                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
1093          | false ⇒
1094            (cost_of_block = 0)
1095          ])
1096  ].
1097  [1:
1098    cases reachable_program_counter_witness #_ #hyp
1099    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
1100    @(le_to_lt_to_lt … base_case hyp)
1101  |2:
1102    change with (if to_continue then ? else (? = 0))
1103    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
1104    @pi2
1105  |3:
1106    change with (if to_continue then ? else (0 = 0))
1107    >p normalize nodelta %
1108  |7,8:
1109    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1110    @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
1111    destruct %
1112  |96,102,105:
1113    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1114    cases(block_cost' ?????????) -block_cost'
1115    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
1116    destruct %
1117  |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,
1118   90,93:
1119    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1120    cases(block_cost' ?????????) -block_cost'
1121    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
1122    destruct %
1123  |60,61,62,63,64,65,66,67,68,69,99,101,100,102:
1124    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1125    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
1126    destruct %
1127  |103:
1128    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1129    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1130    <FETCH normalize nodelta <instr normalize nodelta
1131    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1132    * * * * #n'
1133    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1134    %
1135    [1:
1136      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1137      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1138      >(le_to_leb_true … program_counter_lt') %
1139    |2:
1140      assumption
1141    ]
1142  |104:
1143    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1144    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1145    <FETCH normalize nodelta <instr normalize nodelta
1146    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1147    * * * * #n'
1148    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1149    @(transitive_le
1150      total_program_size
1151      ((S program_size') + nat_of_bitvector … program_counter')
1152      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1153    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1154    >plus_n_Sm
1155    @monotonic_le_plus_r
1156    change with (
1157      nat_of_bitvector … program_counter' <
1158        nat_of_bitvector … program_counter'')
1159    assumption
1160  |106:
1161    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1162    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1163    <FETCH normalize nodelta <instr normalize nodelta
1164    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1165    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1166    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1167    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1168    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1169    %
1170    [1:
1171      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1172      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1173      >(le_to_leb_true … program_counter_lt') %
1174    |2:
1175      assumption
1176    ]
1177  |107:
1178    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1179    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1180    <FETCH normalize nodelta <instr normalize nodelta
1181    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1182    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1183    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1184    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1185    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1186    @(transitive_le
1187      total_program_size
1188      ((S program_size') + nat_of_bitvector … program_counter')
1189      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1190    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1191    >plus_n_Sm
1192    @monotonic_le_plus_r
1193    change with (
1194      nat_of_bitvector … program_counter' <
1195        nat_of_bitvector … program_counter'')
1196    assumption
1197  |94,97:
1198    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1199    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1200    <FETCH normalize nodelta <instr normalize nodelta *
1201    #program_counter_lt' #program_counter_lt_tps' %
1202    [1,3:
1203      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1204      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1205      >(le_to_leb_true … program_counter_lt') %
1206    |2,4:
1207      assumption
1208    ]
1209  |5,10,12,13,16,18,19,22,25,28,31,34,37,40,43,46,49,52,55,58,70,73,
1210   76,79,82,85,88,91:
1211    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1212    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1213    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1214    #program_counter_lt' #program_counter_lt_tps' %
1215    try assumption
1216    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1217    <FETCH normalize nodelta whd in match ltb; normalize nodelta
1218    >(le_to_leb_true … program_counter_lt') %
1219  |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,
1220   92:
1221    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1222    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1223    <FETCH normalize nodelta
1224    <real_instruction_refl <instr normalize nodelta *
1225    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1226    @(transitive_le
1227      total_program_size
1228      ((S program_size') + nat_of_bitvector … program_counter')
1229      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1230    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1231    >plus_n_Sm
1232    @monotonic_le_plus_r
1233    change with (
1234      nat_of_bitvector … program_counter' <
1235        nat_of_bitvector … program_counter'')
1236    assumption
1237  |95,98:
1238    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1239    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1240    <FETCH normalize nodelta <instr normalize nodelta
1241    try(<real_instruction_refl <instr normalize nodelta) *
1242    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1243    @(transitive_le
1244      total_program_size
1245      ((S program_size') + nat_of_bitvector … program_counter')
1246      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1247    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1248    >plus_n_Sm
1249    @monotonic_le_plus_r
1250    change with (
1251      nat_of_bitvector … program_counter' <
1252        nat_of_bitvector … program_counter'')
1253    assumption
1254  ]
1255qed.
1256
1257definition block_cost:
1258    ∀code_memory': BitVectorTrie Byte 16.
1259    ∀program_counter': Word.
1260    ∀total_program_size: nat.
1261    ∀cost_labels: BitVectorTrie costlabel 16.
1262    ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
1263    ∀good_program_witness: good_program code_memory' total_program_size.
1264      Σcost_of_block: nat.
1265        ∀start_status: Status code_memory'.
1266        ∀final_status: Status code_memory'.
1267        ∀trace_ends_flag.
1268        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1269          program_counter' = program_counter … start_status →
1270            (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1271              cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
1272  λcode_memory: BitVectorTrie Byte 16.
1273  λprogram_counter: Word.
1274  λtotal_program_size: nat.
1275  λcost_labels: BitVectorTrie costlabel 16.
1276  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
1277  λgood_program_witness: good_program code_memory total_program_size. ?.
1278  cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
1279    reachable_program_counter_witness good_program_witness true ?)
1280  [1:
1281    #cost_of_block #block_cost_hyp
1282    %{cost_of_block}
1283    cases(lookup_opt … cost_labels) in block_cost_hyp;
1284    [2: #cost_label] normalize nodelta
1285    #hyp assumption
1286  |2:
1287    @le_plus_n_r
1288  ]
1289qed.
1290
1291lemma fetch_program_counter_n_Sn:
1292  ∀instruction: instruction.
1293  ∀program_counter, program_counter': Word.
1294  ∀ticks, n: nat.
1295  ∀code_memory: BitVectorTrie Byte 16.
1296    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
1297      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
1298        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
1299          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
1300  #instruction #program_counter #program_counter' #ticks #n #code_memory
1301  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
1302  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
1303  <fetch_program_counter_n_hyp normalize nodelta
1304  <fetch_hyp normalize nodelta
1305  change with (
1306    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
1307  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
1308  >(le_to_leb_true … lt_hyp) %
1309qed.
1310
1311(* XXX: to be moved into common/Identifiers.ma *)
1312lemma lookup_present_add_hit:
1313  ∀tag, A, map, k, v, k_pres.
1314    lookup_present tag A (add … map k v) k k_pres = v.
1315  #tag #a #map #k #v #k_pres
1316  lapply (lookup_lookup_present … (add … map k v) … k_pres)
1317  >lookup_add_hit #Some_assm destruct(Some_assm)
1318  <e0 %
1319qed.
1320
1321lemma lookup_present_add_miss:
1322  ∀tag, A, map, k, k', v, k_pres', k_pres''.
1323    k' ≠ k →
1324      lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
1325  #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
1326  lapply (lookup_lookup_present … (add … map k v) ? k_pres')
1327  >lookup_add_miss try assumption
1328  #Some_assm
1329  lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
1330  lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
1331qed.
1332
1333(* XXX: to be moved into basics/types.ma *)
1334lemma not_None_to_Some:
1335  ∀A: Type[0].
1336  ∀o: option A.
1337    o ≠ None A → ∃v: A. o = Some A v.
1338  #A #o cases o
1339  [1:
1340    #absurd cases absurd #absurd' cases (absurd' (refl …))
1341  |2:
1342    #v' #ignore /2/
1343  ]
1344qed.
1345
1346lemma present_add_present:
1347  ∀tag, a, map, k, k', v.
1348    k' ≠ k →
1349      present tag a (add tag a map k v) k' →
1350        present tag a map k'.
1351  #tag #a #map #k #k' #v #neq_hyp #present_hyp
1352  whd in match present; normalize nodelta
1353  whd in match present in present_hyp; normalize nodelta in present_hyp;
1354  cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
1355  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
1356  [1:
1357    * #k_eq_hyp @⊥ /2/
1358  |2:
1359    #Some_eq_hyp' /2/
1360  ]
1361qed.
1362
1363lemma present_add_hit:
1364  ∀tag, a, map, k, v.
1365    present tag a (add tag a map k v) k.
1366  #tag #a #map #k #v
1367  whd >lookup_add_hit
1368  % #absurd destruct
1369qed.
1370
1371lemma present_add_miss:
1372  ∀tag, a, map, k, k', v.
1373    k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
1374  #tag #a #map #k #k' #v #neq_assm #present_assm
1375  whd >lookup_add_miss assumption
1376qed.
1377
1378lemma lt_to_le_to_le:
1379  ∀n, m, p: nat.
1380    n < m → m ≤ p → n ≤ p.
1381  #n #m #p #H #H1
1382  elim H
1383  [1:
1384    @(transitive_le n m p) /2/
1385  |2:
1386    /2/
1387  ]
1388qed.
1389
1390lemma eqb_decidable:
1391  ∀l, r: nat.
1392    (eqb l r = true) ∨ (eqb l r = false).
1393  #l #r //
1394qed.
1395
1396lemma r_Sr_and_l_r_to_Sl_r:
1397  ∀r, l: nat.
1398    (∃r': nat. r = S r' ∧ l = r') → S l = r.
1399  #r #l #exists_hyp
1400  cases exists_hyp #r'
1401  #and_hyp cases and_hyp
1402  #left_hyp #right_hyp
1403  destruct %
1404qed.
1405
1406lemma eqb_Sn_to_exists_n':
1407  ∀m, n: nat.
1408    eqb (S m) n = true → ∃n': nat. n = S n'.
1409  #m #n
1410  cases n
1411  [1:
1412    normalize #absurd
1413    destruct(absurd)
1414  |2:
1415    #n' #_ %{n'} %
1416  ]
1417qed.
1418
1419lemma eqb_true_to_eqb_S_S_true:
1420  ∀m, n: nat.
1421    eqb m n = true → eqb (S m) (S n) = true.
1422  #m #n normalize #assm assumption
1423qed.
1424
1425lemma eqb_S_S_true_to_eqb_true:
1426  ∀m, n: nat.
1427    eqb (S m) (S n) = true → eqb m n = true.
1428  #m #n normalize #assm assumption
1429qed.
1430
1431lemma eqb_true_to_refl:
1432  ∀l, r: nat.
1433    eqb l r = true → l = r.
1434  #l
1435  elim l
1436  [1:
1437    #r cases r
1438    [1:
1439      #_ %
1440    |2:
1441      #l' normalize
1442      #absurd destruct(absurd)
1443    ]
1444  |2:
1445    #l' #inductive_hypothesis #r
1446    #eqb_refl @r_Sr_and_l_r_to_Sl_r
1447    %{(pred r)} @conj
1448    [1:
1449      cases (eqb_Sn_to_exists_n' … eqb_refl)
1450      #r' #S_assm >S_assm %
1451    |2:
1452      cases (eqb_Sn_to_exists_n' … eqb_refl)
1453      #r' #refl_assm destruct normalize
1454      @inductive_hypothesis
1455      normalize in eqb_refl; assumption
1456    ]
1457  ]
1458qed.
1459
1460lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
1461  ∀r, l: nat.
1462    r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
1463  #r #l #disj_hyp
1464  cases disj_hyp
1465  [1:
1466    #r_O_refl destruct @nmk
1467    #absurd destruct(absurd)
1468  |2:
1469    #exists_hyp cases exists_hyp #r'
1470    #conj_hyp cases conj_hyp #left_conj #right_conj
1471    destruct @nmk #S_S_refl_hyp
1472    elim right_conj #hyp @hyp //
1473  ]
1474qed.
1475
1476lemma neq_l_r_to_neq_Sl_Sr:
1477  ∀l, r: nat.
1478    l ≠ r → S l ≠ S r.
1479  #l #r #l_neq_r_assm
1480  @nmk #Sl_Sr_assm cases l_neq_r_assm
1481  #assm @assm //
1482qed.
1483
1484lemma eqb_false_to_not_refl:
1485  ∀l, r: nat.
1486    eqb l r = false → l ≠ r.
1487  #l
1488  elim l
1489  [1:
1490    #r cases r
1491    [1:
1492      normalize #absurd destruct(absurd)
1493    |2:
1494      #r' #_ @nmk
1495      #absurd destruct(absurd)
1496    ]
1497  |2:
1498    #l' #inductive_hypothesis #r
1499    cases r
1500    [1:
1501      #eqb_false_assm
1502      @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
1503      @or_introl %
1504    |2:
1505      #r' #eqb_false_assm
1506      @neq_l_r_to_neq_Sl_Sr
1507      @inductive_hypothesis
1508      assumption
1509    ]
1510  ]
1511qed.
1512
1513lemma le_to_lt_or_eq:
1514  ∀m, n: nat.
1515    m ≤ n → m = n ∨ m < n.
1516  #m #n #le_hyp
1517  cases le_hyp
1518  [1:
1519    @or_introl %
1520  |2:
1521    #m' #le_hyp'
1522    @or_intror
1523    normalize
1524    @le_S_S assumption
1525  ]
1526qed.
1527
1528lemma le_neq_to_lt:
1529  ∀m, n: nat.
1530    m ≤ n → m ≠ n → m < n.
1531  #m #n #le_hyp #neq_hyp
1532  cases neq_hyp
1533  #eq_absurd_hyp
1534  generalize in match (le_to_lt_or_eq m n le_hyp);
1535  #disj_assm cases disj_assm
1536  [1:
1537    #absurd cases (eq_absurd_hyp absurd)
1538  |2:
1539    #assm assumption
1540  ]
1541qed.
1542
1543inverter nat_jmdiscr for nat.
1544
1545(* XXX: this is false in the general case.  For instance, if n = 0 then the
1546        base case requires us prove 1 = 0, as it is the carry bit that holds
1547        the result of the addition. *)
1548axiom succ_nat_of_bitvector_half_add_1:
1549  ∀n: nat.
1550  ∀bv: BitVector n.
1551  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
1552    S (nat_of_bitvector … bv) = nat_of_bitvector …
1553      (\snd (half_add n (bitvector_of_nat … 1) bv)).
1554
1555lemma plus_lt_to_lt:
1556  ∀m, n, o: nat.
1557    m + n < o → m < o.
1558  #m #n #o
1559  elim n
1560  [1:
1561    <(plus_n_O m) in ⊢ (% → ?);
1562    #assumption assumption
1563  |2:
1564    #n' #inductive_hypothesis
1565    <(plus_n_Sm m n') in ⊢ (% → ?);
1566    #assm @inductive_hypothesis
1567    normalize in assm; normalize
1568    /2 by lt_S_to_lt/
1569  ]
1570qed.
1571
1572include "arithmetics/div_and_mod.ma".
1573
1574lemma n_plus_1_n_to_False:
1575  ∀n: nat.
1576    n + 1 = n → False.
1577  #n elim n
1578  [1:
1579    normalize #absurd destruct(absurd)
1580  |2:
1581    #n' #inductive_hypothesis normalize
1582    #absurd @inductive_hypothesis /2/
1583  ]
1584qed.
1585
1586lemma one_two_times_n_to_False:
1587  ∀n: nat.
1588    1=2*n→False.
1589  #n cases n
1590  [1:
1591    normalize #absurd destruct(absurd)
1592  |2:
1593    #n' normalize #absurd
1594    lapply (injective_S … absurd) -absurd #absurd
1595    /2/
1596  ]
1597qed.
1598
1599lemma generalized_nat_cases:
1600  ∀n: nat.
1601    n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m).
1602  #n
1603  cases n
1604  [1:
1605    @or_introl @or_introl %
1606  |2:
1607    #n' cases n'
1608    [1:
1609      @or_introl @or_intror %
1610    |2:
1611      #n'' @or_intror %{n''} %
1612    ]
1613  ]
1614qed.
1615
1616let rec odd_p
1617  (n: nat)
1618    on n ≝
1619  match n with
1620  [ O ⇒ False
1621  | S n' ⇒ even_p n'
1622  ]
1623and even_p
1624  (n: nat)
1625    on n ≝
1626  match n with
1627  [ O ⇒ True
1628  | S n' ⇒ odd_p n'
1629  ].
1630
1631let rec n_even_p_to_n_plus_2_even_p
1632  (n: nat)
1633    on n: even_p n → even_p (n + 2) ≝
1634  match n with
1635  [ O ⇒ ?
1636  | S n' ⇒ ?
1637  ]
1638and n_odd_p_to_n_plus_2_odd_p
1639  (n: nat)
1640    on n: odd_p n → odd_p (n + 2) ≝
1641  match n with
1642  [ O ⇒ ?
1643  | S n' ⇒ ?
1644  ].trace_any_label_length
1645  [1,3:
1646    normalize #assm assumption
1647  |2:
1648    normalize @n_odd_p_to_n_plus_2_odd_p
1649  |4:
1650    normalize @n_even_p_to_n_plus_2_even_p
1651  ]
1652qed.
1653
1654let rec two_times_n_even_p
1655  (n: nat)
1656    on n: even_p (2 * n) ≝
1657  match n with
1658  [ O ⇒ ?
1659  | S n' ⇒ ?
1660  ]
1661and two_times_n_plus_one_odd_p
1662  (n: nat)
1663    on n: odd_p ((2 * n) + 1) ≝
1664  match n with
1665  [ O ⇒ ?
1666  | S n' ⇒ ?
1667  ].
1668  [1,3:
1669    normalize @I
1670  |2:
1671    normalize
1672    >plus_n_Sm
1673    <(associative_plus n' n' 1)
1674    >(plus_n_O (n' + n'))
1675    cut(n' + n' + 0 + 1 = 2 * n' + 1)
1676    [1:
1677      //
1678    |2:
1679      #refl_assm >refl_assm
1680      @two_times_n_plus_one_odd_p     
1681    ]
1682  |4:
1683    normalize
1684    >plus_n_Sm
1685    cut(n' + (n' + 1) + 1 = (2 * n') + 2)
1686    [1:
1687      normalize /2/
1688    |2:
1689      #refl_assm >refl_assm
1690      @n_even_p_to_n_plus_2_even_p
1691      @two_times_n_even_p
1692    ]
1693  ]
1694qed.
1695
1696let rec even_p_to_not_odd_p
1697  (n: nat)
1698    on n: even_p n → ¬ odd_p n ≝
1699  match n with
1700  [ O ⇒ ?
1701  | S n' ⇒ ?
1702  ]
1703and odd_p_to_not_even_p
1704  (n: nat)
1705    on n: odd_p n → ¬ even_p n ≝
1706  match n with
1707  [ O ⇒ ?
1708  | S n' ⇒ ?
1709  ].
1710  [1:
1711    normalize #_
1712    @nmk #assm assumption
1713  |3:
1714    normalize #absurd
1715    cases absurd
1716  |2:
1717    normalize
1718    @odd_p_to_not_even_p
1719  |4:
1720    normalize
1721    @even_p_to_not_odd_p
1722  ]
1723qed.
1724
1725lemma even_p_odd_p_cases:
1726  ∀n: nat.
1727    even_p n ∨ odd_p n.
1728  #n elim n
1729  [1:
1730    normalize @or_introl @I
1731  |2:
1732    #n' #inductive_hypothesis
1733    normalize
1734    cases inductive_hypothesis
1735    #assm
1736    try (@or_introl assumption)
1737    try (@or_intror assumption)
1738  ]
1739qed.
1740
1741lemma two_times_n_plus_one_refl_two_times_n_to_False:
1742  ∀m, n: nat.
1743    2 * m + 1 = 2 * n → False.
1744  #m #n
1745  #assm
1746  cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
1747  [1:
1748    >assm
1749    @conj
1750    @two_times_n_even_p
1751  |2:
1752    * #_ #absurd
1753    cases (even_p_to_not_odd_p … absurd)
1754    #assm @assm
1755    @two_times_n_plus_one_odd_p
1756  ]
1757qed.
1758
1759lemma nat_of_bitvector_aux_injective:
1760  ∀n: nat.
1761  ∀l, r: BitVector n.
1762  ∀acc_l, acc_r: nat.
1763    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
1764      acc_l = acc_r ∧ l ≃ r.
1765  #n #l
1766  elim l #r
1767  [1:
1768    #acc_l #acc_r normalize
1769    >(BitVector_O r) normalize /2/
1770  |2:
1771    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
1772    normalize normalize in inductive_hypothesis;
1773    cases (BitVector_Sn … r)
1774    #r_hd * #r_tl #r_refl destruct normalize
1775    cases hd cases r_hd normalize
1776    [1:
1777      #relevant
1778      cases (inductive_hypothesis … relevant)
1779      #acc_assm #tl_assm destruct % //
1780      lapply (injective_plus_l ? ? ? acc_assm)
1781      -acc_assm #acc_assm
1782      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1783      lapply (injective_times_r ? ? ? ? acc_assm) /2/
1784    |4:
1785      #relevant
1786      cases (inductive_hypothesis … relevant)
1787      #acc_assm #tl_assm destruct % //
1788      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1789      lapply(injective_times_r ? ? ? ? acc_assm) /2/
1790    |2:
1791      #relevant 
1792      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
1793        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
1794      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
1795      [1:
1796        #eqb_true_assm
1797        lapply (eqb_true_to_refl … eqb_true_assm)
1798        #refl_assm
1799        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1800      |2:
1801        #eqb_false_assm
1802        lapply (eqb_false_to_not_refl … eqb_false_assm)
1803        #not_refl_assm cases not_refl_assm #absurd_assm
1804        cases (inductive_hypothesis … relevant) #absurd
1805        cases (absurd_assm absurd)
1806      ]
1807    |3:
1808      #relevant 
1809      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
1810        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
1811      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
1812      [1:
1813        #eqb_true_assm
1814        lapply (eqb_true_to_refl … eqb_true_assm)
1815        #refl_assm
1816        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
1817        -refl_assm #refl_assm
1818        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1819      |2:
1820        #eqb_false_assm
1821        lapply (eqb_false_to_not_refl … eqb_false_assm)
1822        #not_refl_assm cases not_refl_assm #absurd_assm
1823        cases (inductive_hypothesis … relevant) #absurd
1824        cases (absurd_assm absurd)
1825      ]
1826    ]
1827  ]
1828qed.
1829
1830lemma nat_of_bitvector_destruct:
1831  ∀n: nat.
1832  ∀l_hd, r_hd: bool.
1833  ∀l_tl, r_tl: BitVector n.
1834    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
1835      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
1836  #n #l_hd #r_hd #l_tl #r_tl
1837  normalize
1838  cases l_hd cases r_hd
1839  normalize
1840  [4:
1841    /2/
1842  |1:
1843    #relevant
1844    cases (nat_of_bitvector_aux_injective … relevant)
1845    #_ #l_r_tl_refl destruct /2/
1846  |2,3:
1847    #relevant
1848    cases (nat_of_bitvector_aux_injective … relevant)
1849    #absurd destruct(absurd)
1850  ]
1851qed.
1852
1853lemma BitVector_cons_injective:
1854  ∀n: nat.
1855  ∀l_hd, r_hd: bool.
1856  ∀l_tl, r_tl: BitVector n.
1857    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
1858  #l #l_hd #r_hd #l_tl #r_tl
1859  #l_refl #r_refl destruct %
1860qed.
1861
1862lemma refl_nat_of_bitvector_to_refl:
1863  ∀n: nat.
1864  ∀l, r: BitVector n.
1865    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
1866  #n
1867  elim n
1868  [1:
1869    #l #r
1870    >(BitVector_O l)
1871    >(BitVector_O r)
1872    #_ %
1873  |2:
1874    #n' #inductive_hypothesis #l #r
1875    lapply (BitVector_Sn ? l) #l_hypothesis
1876    lapply (BitVector_Sn ? r) #r_hypothesis
1877    cases l_hypothesis #l_hd #l_tail_hypothesis
1878    cases r_hypothesis #r_hd #r_tail_hypothesis
1879    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
1880    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
1881    destruct #cons_refl
1882    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
1883    #hd_refl #tl_refl
1884    @BitVector_cons_injective try assumption
1885    @inductive_hypothesis assumption
1886  ]
1887qed.
Note: See TracBrowser for help on using the repository browser.