source: src/ASM/ASMCosts.ma @ 1902

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

Reverted needless changes to StructuredTraces?

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