source: src/ASM/ASMCosts.ma @ 1904

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

Problem with proof fixed by noting that problem is actually irrelevant

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