root/src/ASM/ASMCosts.ma @ 1927

Revision 1927, 66.0 KB (checked in by mulligan, 13 months ago)

Reduced complexity of good_program predicate, ported to new notion of as_label, reintroduced some deleted code from common/StructuredTraces.ma.
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5include "common/StructuredTraces.ma".
6
7(* XXX: alternative approach:
8 * R : Word → Prop
9 * TPS ≝ |R|
10 * GP : ∀a. R(a) → R(next(a))
11 *)
12
13let rec fetch_program_counter_n
14  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
15    on n: option Word ≝
16  match n with
17  [ O ⇒ Some … program_counter
18  | S n ⇒
19    match fetch_program_counter_n n code_memory program_counter with
20    [ None ⇒ None …
21    | Some tail_pc ⇒
22      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
23        if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
24          Some … program_counter
25        else
26          None Word (* XXX: overflow! *)
27    ]
28  ].
29   
30definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
31  λcode_memory: BitVectorTrie Byte 16.
32  λprogram_size: nat.
33  λprogram_counter: Word.
34    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
35        nat_of_bitvector 16 program_counter < program_size.
36   
37definition well_labelling: BitVectorTrie costlabel 16 → Prop ≝
38  λcost_labels.
39    injective … (λx. lookup_opt … x cost_labels).
40   
41definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
42  λcode_memory: BitVectorTrie Byte 16.
43  λtotal_program_size: nat.
44  ∀program_counter: Word.
45  ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
46  let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
47    match instruction with
48    [ RealInstruction instr ⇒
49      match instr with
50      [ RET                    ⇒ True
51      | JC   relative          ⇒ True (* XXX: see below *)
52      | JNC  relative          ⇒ True (* XXX: see below *)
53      | JB   bit_addr relative ⇒ True
54      | JNB  bit_addr relative ⇒ True
55      | JBC  bit_addr relative ⇒ True
56      | JZ   relative          ⇒ True
57      | JNZ  relative          ⇒ True
58      | CJNE src_trgt relative ⇒ True
59      | DJNZ src_trgt relative ⇒ True
60      | _                      ⇒
61        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
62          nat_of_bitvector … program_counter' < total_program_size
63      ]
64    | LCALL addr         ⇒
65      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
66        nat_of_bitvector … program_counter' < total_program_size
67      (*match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
68      [ ADDR16 addr ⇒ λaddr16: True.
69          reachable_program_counter code_memory total_program_size addr ∧
70            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
71              nat_of_bitvector … program_counter' < total_program_size
72      | _ ⇒ λother: False. ⊥
73      ] (subaddressing_modein … addr) *)
74    | ACALL addr         ⇒
75      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
76        nat_of_bitvector … program_counter' < total_program_size
77      (* match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
78      [ ADDR11 addr ⇒ λaddr11: True.
79        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
80        let 〈thr, eig〉 ≝ split … 3 8 addr in
81        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
82        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
83          reachable_program_counter code_memory total_program_size new_program_counter ∧
84            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
85              nat_of_bitvector … program_counter' < total_program_size
86      | _ ⇒ λother: False. ⊥
87      ] (subaddressing_modein … addr) *)
88    | AJMP  addr         ⇒
89      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
90        reachable_program_counter code_memory total_program_size jump_target
91    | LJMP  addr         ⇒
92      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
93        reachable_program_counter code_memory total_program_size jump_target
94    | SJMP  addr     ⇒
95      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
96        reachable_program_counter code_memory total_program_size jump_target
97    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
98      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
99        nat_of_bitvector … program_counter' < total_program_size
100    | MOVC  src trgt ⇒
101        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
102          nat_of_bitvector … program_counter' < total_program_size
103    ].
104(*  cases other
105qed. *)
106
107definition current_instruction_label ≝
108  λcode_memory.
109  λcost_labels: BitVectorTrie costlabel 16.
110  λs: Status code_memory.
111  let pc ≝ program_counter … code_memory s in
112    lookup_opt … pc cost_labels.
113
114definition next_instruction_properly_relates_program_counters ≝
115  λcode_memory.
116  λbefore: Status code_memory.
117  λafter : Status code_memory.
118    let program_counter_before ≝ program_counter ? code_memory before in
119    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
120      program_counter ? code_memory after = program_counter_after.
121
122lemma eq_bv_true_to_refl:
123  ∀n: nat.
124  ∀x: BitVector n.
125  ∀y: BitVector n.
126    eq_bv n x y = true → x = y.
127  #n #x #y
128  cases daemon (* XXX: !!! *)
129qed.
130
131lemma refl_to_eq_bv_true:
132  ∀n: nat.
133  ∀x: BitVector n.
134  ∀y: BitVector n.
135    x = y → eq_bv n x y = true.
136  #n #x #y #refl destruct /2/
137qed.
138
139corollary refl_iff_eq_bv_true:
140  ∀n: nat.
141  ∀x: BitVector n.
142  ∀y: BitVector n.
143    eq_bv n x y = true ↔ x = y.
144  #n #x #y whd in match iff; normalize nodelta
145  @conj /2/
146qed.
147
148definition word_deqset: DeqSet ≝
149  mk_DeqSet Word (eq_bv 16) ?.
150  @refl_iff_eq_bv_true
151qed.
152
153definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
154  λcode_memory.
155  λcost_labels.
156    mk_abstract_status
157      (Status code_memory)
158      (λs,s'. (execute_1 … s) = s')
159      word_deqset
160      (program_counter …)
161      (λs,class. ASM_classify … s = class)
162      (current_instruction_label code_memory cost_labels)
163      (next_instruction_properly_relates_program_counters code_memory)
164      ?.
165  cases daemon (* XXX: is final predicate *)
166qed.
167
168let rec trace_any_label_length
169  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
170    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
171      (final_status: Status code_memory)
172      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
173        on the_trace: nat ≝
174  match the_trace with
175  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
176  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 0
177  | tal_base_return the_status _ _ _ ⇒ 0
178  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
179      let tail_length ≝ trace_any_label_length … final_trace in
180      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
181        pc_difference + tail_length
182  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
183      let tail_length ≝ trace_any_label_length … tail_trace in
184      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
185        pc_difference + tail_length       
186  ].
187
188definition trace_any_label_length' ≝
189  λcode_memory: BitVectorTrie Byte 16.
190  λcost_labels: BitVectorTrie costlabel 16.
191  λtrace_ends_flag: trace_ends_with_ret.
192  λstart_status: Status code_memory.
193  λfinal_status: Status code_memory.
194  λthe_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status.
195    as_trace_any_label_length' … the_trace.
196
197let rec all_program_counter_list
198  (n: nat)
199    on n ≝
200  match n with
201  [ O ⇒ [ ]
202  | S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n')
203  ].
204
205lemma all_program_counter_list_bound_eq:
206  ∀bound: nat.
207    |all_program_counter_list bound| = bound.
208  #bound elim bound try %
209  #bound' #inductive_hypothesis normalize
210  >inductive_hypothesis %
211qed.
212
213axiom nat_of_bitvector_bitvector_of_nat_inverse:
214  ∀n: nat.
215  ∀b: nat.
216    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
217
218axiom bitvector_of_nat_inverse_nat_of_bitvector:
219  ∀n: nat.
220  ∀b: BitVector n.
221    bitvector_of_nat n (nat_of_bitvector n b) = b.
222
223lemma mem_all_program_counter_list_lt_bound:
224  ∀bound: nat.
225  ∀bound_proof: bound ≤ 2^16.
226  ∀e: Word.
227    memb word_deqset e (all_program_counter_list bound) = true →
228      nat_of_bitvector … e < bound.
229  #bound elim bound
230  [1:
231    #bound_proof #e
232    normalize #absurd destruct(absurd)
233  |2:
234    #bound' #inductive_hypothesis
235    #bound_proof #e
236    change with (if eq_bv ??? then ? else ? = ? → ?)
237    @eq_bv_elim
238    [1:
239      #eq_assm
240      normalize nodelta destruct #_
241      >nat_of_bitvector_bitvector_of_nat_inverse try assumption
242      normalize %
243    |2:
244      #neq_assm normalize nodelta
245      #memb_assm %2 @inductive_hypothesis
246      try assumption
247      @(transitive_le bound' (S bound'))
248      try assumption %2 %
249    ]
250  ]
251qed.
252
253lemma lt_bound_mem_all_program_counter_list:
254  ∀bound: nat.
255  ∀bound_proof: bound ≤ 2^16.
256  ∀e: Word.
257    nat_of_bitvector … e < bound →
258      memb word_deqset e (all_program_counter_list bound) = true.
259  #bound elim bound
260  [1:
261    #bound_proof #e normalize
262    #absurd cases (lt_to_not_zero … absurd)
263  |2:
264    #bound' #inductive_hypothesis
265    #bound_proof #e
266    change with (? → if eq_bv ??? then ? else ? = ?)
267    #assm
268    cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?)
269    [1:
270      #e_lt_assm
271      @eq_bv_elim
272      [1:
273        #eq_assm normalize nodelta %
274      |2:
275        #neq_assm normalize nodelta
276        @inductive_hypothesis try assumption
277        @(transitive_le bound' (S bound')) try assumption
278        %2 %
279      ]
280    |2:
281      #relevant >eq_eq_bv normalize nodelta try %
282      destruct >bitvector_of_nat_inverse_nat_of_bitvector %
283    |3:
284      normalize in assm;
285      @le_S_S_to_le assumption
286    ]
287  ]
288qed.
289
290include alias "arithmetics/nat.ma".
291
292lemma fetch_program_counter_n_Sn:
293  ∀instruction: instruction.
294  ∀program_counter, program_counter': Word.
295  ∀ticks, n: nat.
296  ∀code_memory: BitVectorTrie Byte 16.
297    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
298      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
299        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
300          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
301  #instruction #program_counter #program_counter' #ticks #n #code_memory
302  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
303  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
304  <fetch_program_counter_n_hyp normalize nodelta
305  <fetch_hyp normalize nodelta
306  change with (
307    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
308  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
309  >(le_to_leb_true … lt_hyp) %
310qed.
311
312(* XXX: indexing bug *)
313lemma execute_1_and_program_counter_after_other_in_lockstep:
314  ∀code_memory: BitVectorTrie Byte 16.
315  ∀start_status: Status code_memory.
316    ASM_classify code_memory start_status = cl_other →
317      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
318        program_counter ? ? (execute_1 … start_status) =
319          program_counter_after_other pc instruction.
320  #code_memory #start_status #classify_assm
321  whd in match execute_1; normalize nodelta
322  cases (execute_1' code_memory start_status) #the_status
323  * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
324  cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
325  #classify_assm #classify_assm' @classify_assm' assumption
326qed-.
327
328let rec tal_pc_list_lt_total_program_size
329  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
330    (total_program_size: nat) (total_program_size_invariant: total_program_size ≤ 2^16)
331      (good_program_witness: good_program code_memory total_program_size)
332        (start: Status code_memory) (final: Status code_memory) (trace_ends_flag: trace_ends_with_ret)
333          (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final)
334            (pc: as_pc (ASM_abstract_status code_memory cost_labels))
335              on the_trace:
336  reachable_program_counter code_memory total_program_size (program_counter … start) →
337    memb word_deqset pc (tal_pc_list (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace) = true →
338      nat_of_bitvector 16 pc<total_program_size ≝
339  match the_trace with
340  [ tal_base_not_return the_status _ _ _ _ ⇒ ?
341  | tal_base_return the_status _ _ _ ⇒ ?
342  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ ?
343  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
344     _ classifier after_return call_trace _ final_trace ⇒ ?
345  | tal_step_default end_flag status_pre status_init status_end execute tail_trace classifier _ ⇒ ?
346  ].
347  #reachable_program_counter_witness
348  whd in ⊢ (??%? → ?); @(bool_inv_ind … (pc==as_pc_of (ASM_abstract_status code_memory cost_labels) ?))
349  normalize nodelta #eq_assm cases reachable_program_counter_witness
350  [1,3,5,7,9:
351    >(eq_bv_eq … eq_assm) #_ #relevant #_
352    assumption
353  |2,4,6:
354    #_ #_ #absurd
355    normalize in absurd; destruct(absurd)
356  |8:
357    #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption
358    whd in after_return;
359    lapply after_return
360    @pair_elim * normalize nodelta #instruction #pc' #ticks
361    #fetch_eq #pc_assm' >pc_assm'
362    lapply (good_program_witness ? reachable_program_counter_witness)
363    whd in classifier; whd in classifier:(??%?);
364    whd in match (current_instruction ??) in classifier;
365    whd in match current_instruction0 in classifier;
366    >fetch_eq in classifier;
367    normalize nodelta cases instruction
368    normalize nodelta -tal_pc_list_lt_total_program_size
369    [8:
370      #preinstruction elim preinstruction
371      normalize in match (? = cl_call);
372    ]
373    try (#assm1 #assm2 #absurd destruct(absurd) @I)
374    try (#assm1 #absurd destruct(absurd) @I)
375    try (#absurd destruct(absurd) @I)
376    (* [1:
377      #addr #_
378      @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ]
379      #w
380      @pair_elim #lft #rgt @pair_elim #lft' #rgt' @pair_elim #lft'' #rgt''
381      #_ #_ #_ * * #_
382    |2:
383      #addr #_
384      @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ]
385      #w * * #_
386    |3:
387      #addr #_ *
388    ] *)
389    #_ #_ * #relevant #pc_tps_assm'
390    whd cases reachable_program_counter_witness * #n
391    #Some_assm #_ % try assumption
392    %{(S n)}
393    @(fetch_program_counter_n_Sn … Some_assm (sym_eq … fetch_eq))
394    assumption
395  |10:
396    #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption -tal_pc_list_lt_total_program_size
397    lapply (execute_1_and_program_counter_after_other_in_lockstep … status_pre classifier)
398    @pair_elim * #instruction #pc #ticks normalize nodelta
399    #fetch_eq whd in match program_counter_after_other; normalize nodelta
400    lapply (good_program_witness … reachable_program_counter_witness)
401    whd in classifier; whd in classifier:(??%?);
402    whd in match (current_instruction ??) in classifier;
403    whd in match current_instruction0 in classifier;
404    >fetch_eq in classifier; normalize nodelta cases instruction
405    normalize nodelta
406    [8:
407      #preinstruction elim preinstruction
408      normalize in match (? = cl_other);
409    ]
410    try (#assm1 #assm2 #absurd destruct(absurd) @I)
411    try (#assm1 #absurd destruct(absurd) @I)
412    try (#absurd destruct(absurd) @I) normalize nodelta
413    [27,28,29:
414      #addr #_ #reachable
415      #program_counter_execute_1_refl
416      whd in execute; <execute
417      >program_counter_execute_1_refl assumption
418    |*:
419      try (#assm1 #assm2 #_ * #relevant #pc_lt_assm)
420      try (#assm1 #_ * #relevant #pc_lt_assm)
421      try (#_ * #relevant #pc_lt_assm) #pc_refl
422      cases reachable_program_counter_witness * #n
423      #Some_assm #tps_lt_assm
424      whd in match reachable_program_counter; normalize nodelta %
425      try %{(S n)}
426      whd in execute; <execute
427      try (@(fetch_program_counter_n_Sn instruction ?? ticks ?? Some_assm ?) >execute >fetch_eq <pc_refl >execute try %)
428      <pc_refl in relevant; <execute #assm
429      >pc_refl >pc_refl in assm; #assm assumption
430    ]
431  ]
432qed.
433
434lemma sublist_tal_pc_list_all_program_counter_list:
435  ∀code_memory: BitVectorTrie Byte 16.
436  ∀cost_labels: BitVectorTrie costlabel 16.
437  ∀total_program_size: nat.
438  ∀total_program_size_invariant: total_program_size ≤ 2^16.
439  ∀good_program_witness: good_program code_memory total_program_size.
440  ∀start, final: Status code_memory.
441  ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size
442    (program_counter (BitVectorTrie Byte 16) code_memory start).
443  ∀trace_ends_flag.
444  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
445    sublist ? (tal_pc_list … the_trace) (all_program_counter_list total_program_size).
446  #code_memory #cost_labels #total_program_size #total_program_size_invariant
447  #good_program_witness #start #final #reachable_program_counter_witness
448  #trace_ends_flag #the_trace
449  whd in match (sublist ???); #pc #memb_assm
450  @lt_bound_mem_all_program_counter_list
451  try assumption destruct
452  lapply memb_assm -memb_assm
453  @tal_pc_list_lt_total_program_size
454  assumption
455qed.
456
457corollary tal_pc_list_length_leq_total_program_size:
458  ∀code_memory: BitVectorTrie Byte 16.
459  ∀cost_labels: BitVectorTrie costlabel 16.
460  ∀total_program_size: nat.
461  ∀total_program_size_invariant: total_program_size ≤ 2^16.
462  ∀good_program_witness: good_program code_memory total_program_size.
463  ∀start, final: Status code_memory.
464  ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size
465    (program_counter (BitVectorTrie Byte 16) code_memory start).
466  ∀trace_ends_flag.
467  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
468  ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace.
469    |tal_pc_list … the_trace| ≤ total_program_size.
470  #code_memory #cost_labels #total_program_size #total_program_size_invariant
471  #good_program_witness #start #final #reachable_program_counter_witness
472  #trace_ends_flag #the_trace #unrepeating_witness
473  <(all_program_counter_list_bound_eq total_program_size)
474  @sublist_length
475  [1:
476    @tal_unrepeating_uniqueb
477    assumption
478  |2:
479    @sublist_tal_pc_list_all_program_counter_list
480    assumption
481  ]
482qed.
483
484let rec compute_paid_trace_any_label
485  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
486    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
487      (final_status: Status code_memory)
488        (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
489       on the_trace: nat ≝
490  match the_trace with
491  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
492  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
493  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ current_instruction_cost … pre_fun_call
494  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
495     _ _ _ call_trace _ final_trace ⇒
496      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
497      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
498        current_instruction_cost + final_trace_cost
499  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
500      let current_instruction_cost ≝ current_instruction_cost … status_pre in
501      let tail_trace_cost ≝
502       compute_paid_trace_any_label … cost_labels end_flag
503        status_init status_end tail_trace
504      in
505        current_instruction_cost + tail_trace_cost
506  ].
507
508definition compute_paid_trace_label_label ≝
509  λcode_memory: BitVectorTrie Byte 16.
510  λcost_labels: BitVectorTrie costlabel 16.
511  λtrace_ends_flag: trace_ends_with_ret.
512  λstart_status: Status code_memory.
513  λfinal_status: Status code_memory.
514  λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
515  match the_trace with
516  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
517      compute_paid_trace_any_label … given_trace
518  ].
519
520include alias "arithmetics/nat.ma".
521include alias "basics/logic.ma".
522
523lemma plus_right_monotone:
524  ∀m, n, o: nat.
525    m = n → m + o = n + o.
526  #m #n #o #refl >refl %
527qed.
528
529lemma plus_left_monotone:
530  ∀m, n, o: nat.
531    m = n → o + m = o + n.
532  #m #n #o #refl destruct %
533qed.
534
535lemma minus_plus_cancel:
536  ∀m, n : nat.
537  ∀proof: n ≤ m.
538    (m - n) + n = m.
539  #m #n #proof /2 by plus_minus/
540qed.
541
542lemma reachable_program_counter_to_0_lt_total_program_size:
543  ∀code_memory: BitVectorTrie Byte 16.
544  ∀program_counter: Word.
545  ∀total_program_size: nat.
546    reachable_program_counter code_memory total_program_size program_counter →
547      0 < total_program_size.
548  #code_memory #program_counter #total_program_size
549  whd in match reachable_program_counter; normalize nodelta * * #some_n
550  #_ cases (nat_of_bitvector 16 program_counter)
551  [1:
552    #assm assumption
553  |2:
554    #new_pc @ltn_to_ltO
555  ]
556qed.
557
558lemma not_Some_neq_None_to_False:
559  ∀a: Type[0].
560  ∀e: a.
561    ¬ (Some a e ≠ None a) → False.
562  #a #e #absurd cases absurd -absurd
563  #absurd @absurd @nmk -absurd
564  #absurd destruct(absurd)
565qed.
566
567lemma trace_compute_paid_trace_cl_other:
568  ∀code_memory' : (BitVectorTrie Byte 16).
569  ∀program_counter' : Word.
570  ∀total_program_size : ℕ.
571  ∀cost_labels : (BitVectorTrie costlabel 16).
572  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
573  ∀good_program_witness : (good_program code_memory' total_program_size).
574  ∀program_size' : ℕ.
575  ∀ticks : ℕ.
576  ∀instruction : instruction.
577  ∀program_counter'' : Word.
578  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
579  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
580  ∀start_status : (Status code_memory').
581  ∀final_status : (Status code_memory').
582  ∀trace_ends_flag : trace_ends_with_ret.
583  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
584  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
585  ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
586  ∀classify_assm: ASM_classify0 instruction = cl_other.
587  ∀pi1 : ℕ.
588   (if match lookup_opt costlabel 16 program_counter''' cost_labels with 
589         [None ⇒ true
590         |Some _ ⇒ false
591         ] 
592    then
593      ∀start_status0:Status code_memory'.
594      ∀final_status0:Status code_memory'.
595      ∀trace_ends_flag0:trace_ends_with_ret.
596      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
597        trace_any_label_length' code_memory' cost_labels trace_ends_flag0
598          start_status0 final_status0 the_trace0 ≤ program_size' →
599        program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
600                  pi1
601                    =compute_paid_trace_any_label code_memory' cost_labels
602                     trace_ends_flag0 start_status0 final_status0 the_trace0
603    else (pi1=O) )
604   → ticks+pi1
605     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
606      start_status final_status the_trace.
607  #code_memory' #program_counter' #total_program_size #cost_labels
608  #reachable_program_counter_witness #good_program_witness
609  #program_size' #ticks #instruction #program_counter'' #FETCH
610  #start_status #final_status
611  #trace_ends_flag #the_trace #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
612  #recursive_assm
613  @(trace_any_label_inv_ind … the_trace)
614    [5:
615      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
616      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
617      #the_trace_refl
618      destruct
619      whd in match (trace_any_label_length … (tal_step_default …));
620      whd in match (compute_paid_trace_any_label … (tal_step_default …));
621      whd in costed_assm:(?%);
622      generalize in match costed_assm;
623      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
624      whd in match (as_label ??);
625      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
626        in ⊢ (??%? → % → ?);
627      #lookup_assm cases lookup_assm
628      [1:
629        #None_lookup_opt_assm normalize nodelta #_
630        generalize in match recursive_assm;
631        lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
632        <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
633        #None_lookup_opt_assm <None_lookup_opt_assm
634        normalize nodelta #new_recursive_assm
635        cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
636          end_flag trace_any_label ? ?) try %
637        whd in match (current_instruction_cost … status_pre);
638        cut(ticks = \snd (fetch code_memory'
639           (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
640        [1,3,5:
641          <FETCH %
642        |2:
643          #ticks_refl_assm
644          >ticks_refl_assm %
645        |4:
646          #ticks_refl_assm
647          change with (S ? ≤ S ?) in size_invariant;
648          lapply (le_S_S_to_le … size_invariant) #assm
649          assumption
650        |6:
651          #ticks_refl_assm
652          <rewrite_assm %
653        ]
654      |2:
655        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm
656        #absurd
657        cases (not_Some_neq_None_to_False ?? absurd)
658      ]
659    |1:
660      #status_start #status_final #execute_assm #classifier_assm #costed_assm
661      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
662      destruct
663      whd in match (trace_any_label_length … (tal_base_not_return …));
664      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
665      whd in costed_assm;
666      generalize in match costed_assm;
667      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
668      whd in match (as_label ??);
669      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
670        in ⊢ (??%? → % → ?);
671      #lookup_assm cases lookup_assm
672      [1:
673        #None_lookup_opt_assm
674        #absurd @⊥ cases absurd -absurd #absurd @absurd %
675      |2:
676        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
677        generalize in match recursive_assm;
678        cases classifier_assm
679        [1:
680          whd in ⊢ (% → ?);
681          whd in ⊢ (??%? → ?);
682          whd in match (current_instruction code_memory' status_start);
683          <FETCH generalize in match classify_assm;
684          cases instruction
685          [8:
686            #preinstruction normalize nodelta
687            whd in match ASM_classify0; normalize nodelta
688            #contradiction >contradiction #absurd destruct(absurd)
689          ]
690          try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
691          try(#addr normalize nodelta #ignore #absurd destruct(absurd))
692          normalize in ignore; destruct(ignore)
693        |2:
694          -classifier_assm #classifier_assm
695          lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
696          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
697          #Some_lookup_opt_assm <Some_lookup_opt_assm
698          normalize nodelta #new_recursive_assm >new_recursive_assm
699          cut(ticks = \snd (fetch code_memory'
700             (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
701          [1:
702            <FETCH %
703          |2:
704            #ticks_refl_assm >ticks_refl_assm
705            <plus_n_O %
706          ]
707        ]
708      ]
709    |2:
710      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
711      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
712    |3:
713      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
714      #classifier_assm #after_return_assm #trace_label_return #costed_assm
715      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
716      destruct @⊥
717    |4:
718      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
719      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
720      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
721      #final_status_refl #the_trace_refl destruct @⊥
722    ]
723  change with (ASM_classify0 ? = ?) in classifier_assm;
724  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
725  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
726  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
727qed.
728
729lemma trace_compute_paid_trace_cl_jump:
730  ∀code_memory': BitVectorTrie Byte 16.
731  ∀program_counter': Word.
732  ∀total_program_size: ℕ.
733  ∀cost_labels: BitVectorTrie costlabel 16.
734  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
735  ∀good_program_witness: good_program code_memory' total_program_size.
736  ∀first_time_around: bool.
737  ∀program_size': ℕ.
738  ∀ticks: ℕ.
739  ∀instruction: instruction.
740  ∀program_counter'': Word.
741  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
742  ∀start_status: (Status code_memory').
743  ∀final_status: (Status code_memory').
744  ∀trace_ends_flag: trace_ends_with_ret.
745  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
746  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
747  ∀classify_assm: ASM_classify0 instruction = cl_jump.
748    ticks
749     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
750      start_status final_status the_trace.
751  #code_memory' #program_counter' #total_program_size #cost_labels
752  #reachable_program_counter_witness #good_program_witness #first_time_around
753  #program_size' #ticks #instruction #program_counter'' #FETCH
754  #start_status #final_status
755  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
756  @(trace_any_label_inv_ind … the_trace)
757  [5:
758    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
759    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
760    #the_trace_refl destruct @⊥
761  |1:
762    #status_start #status_final #execute_assm #classifier_assm #costed_assm
763    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
764    destruct
765    whd in match (trace_any_label_length … (tal_base_not_return …));
766    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
767    <FETCH %
768  |2:
769    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
770    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
771  |3:
772    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
773    #classifier_assm #after_return_assm #trace_label_return #costed_assm
774    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
775    destruct @⊥
776  |4:
777    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
778    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
779    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
780    #final_status_refl #the_trace_refl destruct @⊥
781  ]
782  change with (ASM_classify0 ? = ?) in classifier_assm;
783  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
784  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
785  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
786qed.
787
788lemma trace_compute_paid_trace_cl_call:
789  ∀code_memory' : (BitVectorTrie Byte 16).
790  ∀program_counter' : Word.
791  ∀total_program_size : ℕ.
792  ∀cost_labels : (BitVectorTrie costlabel 16).
793  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
794  ∀good_program_witness : (good_program code_memory' total_program_size).
795  ∀program_size' : ℕ.
796  ∀ticks : ℕ.
797  ∀instruction : instruction.
798  ∀program_counter'' : Word.
799  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
800  ∀start_status : (Status code_memory').
801  ∀final_status : (Status code_memory').
802  ∀trace_ends_flag : trace_ends_with_ret.
803  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
804  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
805  ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
806  ∀classify_assm: ASM_classify0 instruction = cl_call.
807  (∀pi1:ℕ
808  .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
809      [None ⇒ true | Some _ ⇒ false] 
810   then (∀start_status0:Status code_memory'
811             .∀final_status0:Status code_memory'
812              .∀trace_ends_flag0:trace_ends_with_ret
813               .∀the_trace0:trace_any_label
814                                        (ASM_abstract_status code_memory' cost_labels)
815                                        trace_ends_flag0 start_status0 final_status0.
816                trace_any_label_length' code_memory' cost_labels trace_ends_flag0
817                  start_status0 final_status0 the_trace0
818                   ≤ program_size' →
819                program_counter''
820                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
821                 → pi1
822                   =compute_paid_trace_any_label code_memory' cost_labels
823                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
824   else (pi1=O) 
825   → ticks+pi1
826     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
827      start_status final_status the_trace).
828  #code_memory' #program_counter' #total_program_size #cost_labels
829  #reachable_program_counter_witness #good_program_witness #program_size'
830  #ticks #instruction #program_counter'' #FETCH
831  #start_status #final_status #trace_ends_flag
832  #the_trace #program_counter_refl #size_invariant #classify_assm
833  #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    whd in match (as_label ??);
857    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
858      in ⊢ (??%? → % → ?);
859    #lookup_assm cases lookup_assm
860    [1:
861      #None_lookup_opt normalize nodelta #absurd cases absurd
862      -absurd #absurd @⊥ @absurd %
863    |2:
864      #costlabel #Some_lookup_opt normalize nodelta #ignore
865      generalize in match recursive_assm;
866      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
867      [1:
868        generalize in match after_return_assm;
869        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
870      |2:
871        #program_counter_assm >program_counter_assm <Some_lookup_opt
872        normalize nodelta #new_recursive_assm >new_recursive_assm
873        cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
874        [1:
875          <FETCH %
876        |2:
877          #ticks_refl_assm >ticks_refl_assm
878          <plus_n_O %
879        ]
880      ]
881    ]
882  |4:
883    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
884    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
885    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
886    #final_status_refl #the_trace_refl
887    generalize in match execute_assm; destruct #execute_assm
888    whd in match (trace_any_label_length … (tal_step_call …));
889    whd in match (compute_paid_trace_any_label … (tal_step_call …));
890    whd in costed_assm:(?%);
891    generalize in match costed_assm;
892    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
893    whd in match (as_label ??);
894    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
895      in ⊢ (??%? → % → ?);
896    #lookup_assm cases lookup_assm
897    [1:
898      #None_lookup_opt_assm normalize nodelta #ignore
899      generalize in match recursive_assm;
900      cut(program_counter'' = program_counter … status_after_fun_call)
901      [1:
902        generalize in match after_return_assm;
903        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
904      |2:
905        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
906        normalize nodelta #new_recursive_assm
907        cases (new_recursive_assm … trace_any_label ? ?)
908        [1:
909          @plus_right_monotone whd in ⊢ (???%); <FETCH %
910        |2:
911          @le_S_S_to_le @size_invariant
912        |3:
913          %
914        ]
915      ]
916    |2:
917      #cost_label #Some_lookup_opt_assm #absurd
918      cases (not_Some_neq_None_to_False ?? absurd)
919    ]
920  ]
921  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
922  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
923  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
924  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
925  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
926  #absurd destruct(absurd)
927qed.
928
929lemma trace_compute_paid_trace_cl_return:
930  ∀code_memory' : (BitVectorTrie Byte 16).
931  ∀program_counter' : Word.
932  ∀total_program_size : ℕ.
933  ∀cost_labels : (BitVectorTrie costlabel 16).
934  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
935  ∀good_program_witness : (good_program code_memory' total_program_size).
936  ∀program_size' : ℕ.
937  ∀ticks : ℕ.
938  ∀instruction : instruction.
939  ∀program_counter'' : Word.
940  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
941  ∀start_status : (Status code_memory').
942  ∀final_status : (Status code_memory').
943  ∀trace_ends_flag : trace_ends_with_ret.
944  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
945  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
946  ∀classify_assm: ASM_classify0 instruction = cl_return.
947    ticks
948     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
949      start_status final_status the_trace.
950  #code_memory' #program_counter' #total_program_size #cost_labels
951  #reachable_program_counter_witness #good_program_witness #program_size'
952  #ticks #instruction #program_counter'' #FETCH
953  #start_status #final_status #trace_ends_flag
954  #the_trace #program_counter_refl #classify_assm
955  @(trace_any_label_inv_ind … the_trace)
956  [1:
957    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
958    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
959    destruct @⊥
960  |2:
961    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
962    #start_status_refl #final_status_refl #the_trace_refl destruct
963    whd in match (trace_any_label_length … (tal_base_return …));
964    whd in match (compute_paid_trace_any_label … (tal_base_return …));
965    <FETCH %
966  |3:
967    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
968    #classifier_assm #after_return_assm #trace_label_return #costed_assm
969    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
970    destruct @⊥
971  |4:
972    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
973    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
974    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
975    #final_status_refl #the_trace_refl
976    destruct @⊥
977  |5:
978    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
979    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
980    #final_status_refl #the_trace_refl destruct @⊥
981  ]
982  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
983  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
984  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
985  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
986  <FETCH in classifier_assm; >classify_assm
987  #absurd try (destruct(absurd))
988  cases absurd
989  #absurd destruct(absurd)
990qed.
991
992lemma trace_any_label_length_leq_0_to_False:
993  ∀code_memory: BitVectorTrie Byte 16.
994  ∀cost_labels: BitVectorTrie costlabel 16.
995  ∀trace_ends_flag: trace_ends_with_ret.
996  ∀start_status: Status code_memory.
997  ∀final_status: Status code_memory.
998  ∀the_trace.
999  trace_any_label_length' code_memory cost_labels trace_ends_flag start_status
1000    final_status the_trace ≤ 0 → False.
1001  #code_memory #cost_labels #trace_ends_flag #start_status #final_status
1002  #the_trace
1003  cases the_trace /2/
1004qed.
1005     
1006let rec block_cost'
1007  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
1008    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
1009      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
1010        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
1011          on program_size:
1012          Σcost_of_block: nat.
1013          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
1014            ∀start_status: Status code_memory'.
1015            ∀final_status: Status code_memory'.
1016            ∀trace_ends_flag.
1017            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1018              trace_any_label_length' … the_trace ≤ program_size →
1019              program_counter' = program_counter … start_status →
1020                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
1021          else
1022            (cost_of_block = 0) ≝
1023  match program_size return λx. x = program_size → ? with
1024  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
1025  | S program_size' ⇒ λstep_case.
1026    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
1027    let to_continue ≝
1028      match lookup_opt … program_counter' cost_labels with
1029      [ None ⇒ true
1030      | Some _ ⇒ first_time_around
1031      ]
1032    in
1033      ((if to_continue then
1034       pi1 … (match instruction return λx. x = instruction → ? with
1035        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
1036          match real_instruction return λx. x = real_instruction →
1037          Σcost_of_block: nat.
1038            ∀start_status: Status code_memory'.
1039            ∀final_status: Status code_memory'.
1040            ∀trace_ends_flag.
1041            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
1042              trace_any_label_length' … the_trace ≤ S program_size' →
1043              program_counter' = program_counter … start_status →
1044                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
1045          [ RET                    ⇒ λinstr. ticks
1046          | RETI                   ⇒ λinstr. ticks
1047          | JC   relative          ⇒ λinstr. ticks
1048          | JNC  relative          ⇒ λinstr. ticks
1049          | JB   bit_addr relative ⇒ λinstr. ticks
1050          | JNB  bit_addr relative ⇒ λinstr. ticks
1051          | JBC  bit_addr relative ⇒ λinstr. ticks
1052          | JZ   relative          ⇒ λinstr. ticks
1053          | JNZ  relative          ⇒ λinstr. ticks
1054          | CJNE src_trgt relative ⇒ λinstr. ticks
1055          | DJNZ src_trgt relative ⇒ λinstr. ticks
1056          | _                      ⇒ λinstr.
1057              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
1058          ] (refl …)
1059        | ACALL addr     ⇒ λinstr.
1060            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
1061        | AJMP  addr     ⇒ λinstr.
1062          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
1063            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
1064        | LCALL addr     ⇒ λinstr.
1065            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
1066        | LJMP  addr     ⇒ λinstr.
1067          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
1068            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
1069        | SJMP  addr     ⇒ λinstr.
1070          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
1071            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
1072        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
1073            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
1074        | MOVC  src trgt ⇒ λinstr.
1075            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
1076        ] (refl …))
1077      else
1078        0)
1079      : Σcost_of_block: nat.
1080          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
1081          [ true ⇒
1082            ∀start_status: Status code_memory'.
1083            ∀final_status: Status code_memory'.
1084            ∀trace_ends_flag.
1085            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1086              trace_any_label_length' … the_trace ≤ S program_size' →
1087              program_counter' = program_counter … start_status →
1088                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
1089          | false ⇒
1090            (cost_of_block = 0)
1091          ])
1092  ] (refl …).
1093  [2:
1094    change with (if to_continue then ? else (? = 0))
1095    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
1096    @pi2
1097  |1:
1098    destruct
1099    cases (lookup_opt ????) normalize nodelta
1100    [1:
1101      #start_status #final_status #trace_ends_flag #the_trace
1102      #absurd
1103      cases (trace_any_label_length_leq_0_to_False … absurd)
1104    |2:
1105      #cost cases first_time_around normalize nodelta try %
1106      #start_status #final_status #trace_ends_flag #the_trace #absurd
1107      cases (trace_any_label_length_leq_0_to_False … absurd)
1108    ]
1109  |3:
1110    change with (if to_continue then ? else (0 = 0))
1111    >p normalize nodelta %
1112  |6,7:
1113    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1114    @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl)
1115    destruct %
1116  |69,77,79:
1117    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1118    cases(block_cost' ????????) -block_cost'
1119    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
1120    destruct %
1121  |4,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,51,53,55,57,59,61,63,65,
1122    67:
1123    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1124    cases(block_cost' ????????) -block_cost'
1125    lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)     
1126    destruct #assm @assm %
1127  |42,43,44,45,46,47,48,49,50:
1128    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1129    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … FETCH … the_trace program_counter_refl)
1130    destruct %
1131  |71,73,75: (* XXX: unconditional jumps *)
1132    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1133    cases (block_cost' ????????) -block_cost'
1134    lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
1135    whd in match (program_counter_after_other ??); normalize nodelta destruct
1136    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
1137  ]
1138  -block_cost'
1139  [29,30,31: (* XXX: unconditional jumps *)
1140    normalize nodelta
1141    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1142    lapply (good_program_witness program_counter' reachable_program_counter_witness)
1143    <FETCH normalize nodelta <instr normalize nodelta #assm assumption
1144  |*:
1145    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1146    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1147    <FETCH normalize nodelta destruct normalize nodelta
1148    * #program_counter_lt' #program_counter_lt_tps'
1149    % try assumption
1150    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1151    <FETCH normalize nodelta whd in match ltb; normalize nodelta
1152    >(le_to_leb_true … program_counter_lt') %
1153  ]
1154qed.
1155
1156definition block_cost:
1157    ∀code_memory': BitVectorTrie Byte 16.
1158    ∀program_counter': Word.
1159    ∀total_program_size: nat.
1160    ∀total_program_size_invariant: total_program_size ≤ 2^16.
1161    ∀cost_labels: BitVectorTrie costlabel 16.
1162    ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
1163    ∀good_program_witness: good_program code_memory' total_program_size.
1164      Σcost_of_block: nat.
1165        ∀start_status: Status code_memory'.
1166        ∀final_status: Status code_memory'.
1167        ∀trace_ends_flag.
1168        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1169        ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size (program_counter (BitVectorTrie Byte 16) code_memory' start_status).
1170        ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status the_trace.
1171          program_counter' = program_counter … start_status →
1172            cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
1173  λcode_memory: BitVectorTrie Byte 16.
1174  λprogram_counter: Word.
1175  λtotal_program_size: nat.
1176  λtotal_program_size_invariant: total_program_size ≤ 2^16.
1177  λcost_labels: BitVectorTrie costlabel 16.
1178  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
1179  λgood_program_witness: good_program code_memory total_program_size. ?.
1180  cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
1181    reachable_program_counter_witness good_program_witness true)
1182  #cost_of_block #block_cost_hyp
1183  %{cost_of_block}
1184  cases(lookup_opt … cost_labels) in block_cost_hyp;
1185  [2: #cost_label] normalize nodelta
1186  #hyp #start_status #final_status #trace_ends_flag #the_trace
1187  #reachable_program_counter_witness #unrepeating_witness
1188  @hyp @tal_pc_list_length_leq_total_program_size try assumption
1189qed.
1190
1191(* XXX: to be moved into common/Identifiers.ma *)
1192lemma lookup_present_add_hit:
1193  ∀tag, A, map, k, v, k_pres.
1194    lookup_present tag A (add … map k v) k k_pres = v.
1195  #tag #a #map #k #v #k_pres
1196  lapply (lookup_lookup_present … (add … map k v) … k_pres)
1197  >lookup_add_hit #Some_assm destruct(Some_assm)
1198  <e0 %
1199qed.
1200
1201lemma lookup_present_add_miss:
1202  ∀tag, A, map, k, k', v, k_pres', k_pres''.
1203    k' ≠ k →
1204      lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
1205  #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
1206  lapply (lookup_lookup_present … (add … map k v) ? k_pres')
1207  >lookup_add_miss try assumption
1208  #Some_assm
1209  lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
1210  lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
1211qed.
1212
1213(* XXX: to be moved into basics/types.ma *)
1214lemma not_None_to_Some:
1215  ∀A: Type[0].
1216  ∀o: option A.
1217    o ≠ None A → ∃v: A. o = Some A v.
1218  #A #o cases o
1219  [1:
1220    #absurd cases absurd #absurd' cases (absurd' (refl …))
1221  |2:
1222    #v' #ignore /2/
1223  ]
1224qed.
1225
1226lemma present_add_present:
1227  ∀tag, a, map, k, k', v.
1228    k' ≠ k →
1229      present tag a (add tag a map k v) k' →
1230        present tag a map k'.
1231  #tag #a #map #k #k' #v #neq_hyp #present_hyp
1232  whd in match present; normalize nodelta
1233  whd in match present in present_hyp; normalize nodelta in present_hyp;
1234  cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
1235  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
1236  [1:
1237    * #k_eq_hyp @⊥ /2/
1238  |2:
1239    #Some_eq_hyp' /2/
1240  ]
1241qed.
1242
1243lemma present_add_hit:
1244  ∀tag, a, map, k, v.
1245    present tag a (add tag a map k v) k.
1246  #tag #a #map #k #v
1247  whd >lookup_add_hit
1248  % #absurd destruct
1249qed.
1250
1251lemma present_add_miss:
1252  ∀tag, a, map, k, k', v.
1253    k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
1254  #tag #a #map #k #k' #v #neq_assm #present_assm
1255  whd >lookup_add_miss assumption
1256qed.
1257
1258lemma lt_to_le_to_le:
1259  ∀n, m, p: nat.
1260    n < m → m ≤ p → n ≤ p.
1261  #n #m #p #H #H1
1262  elim H
1263  [1:
1264    @(transitive_le n m p) /2/
1265  |2:
1266    /2/
1267  ]
1268qed.
1269
1270lemma eqb_decidable:
1271  ∀l, r: nat.
1272    (eqb l r = true) ∨ (eqb l r = false).
1273  #l #r //
1274qed.
1275
1276lemma r_Sr_and_l_r_to_Sl_r:
1277  ∀r, l: nat.
1278    (∃r': nat. r = S r' ∧ l = r') → S l = r.
1279  #r #l #exists_hyp
1280  cases exists_hyp #r'
1281  #and_hyp cases and_hyp
1282  #left_hyp #right_hyp
1283  destruct %
1284qed.
1285
1286lemma eqb_Sn_to_exists_n':
1287  ∀m, n: nat.
1288    eqb (S m) n = true → ∃n': nat. n = S n'.
1289  #m #n
1290  cases n
1291  [1:
1292    normalize #absurd
1293    destruct(absurd)
1294  |2:
1295    #n' #_ %{n'} %
1296  ]
1297qed.
1298
1299lemma eqb_true_to_eqb_S_S_true:
1300  ∀m, n: nat.
1301    eqb m n = true → eqb (S m) (S n) = true.
1302  #m #n normalize #assm assumption
1303qed.
1304
1305lemma eqb_S_S_true_to_eqb_true:
1306  ∀m, n: nat.
1307    eqb (S m) (S n) = true → eqb m n = true.
1308  #m #n normalize #assm assumption
1309qed.
1310
1311lemma eqb_true_to_refl:
1312  ∀l, r: nat.
1313    eqb l r = true → l = r.
1314  #l
1315  elim l
1316  [1:
1317    #r cases r
1318    [1:
1319      #_ %
1320    |2:
1321      #l' normalize
1322      #absurd destruct(absurd)
1323    ]
1324  |2:
1325    #l' #inductive_hypothesis #r
1326    #eqb_refl @r_Sr_and_l_r_to_Sl_r
1327    %{(pred r)} @conj
1328    [1:
1329      cases (eqb_Sn_to_exists_n' … eqb_refl)
1330      #r' #S_assm >S_assm %
1331    |2:
1332      cases (eqb_Sn_to_exists_n' … eqb_refl)
1333      #r' #refl_assm destruct normalize
1334      @inductive_hypothesis
1335      normalize in eqb_refl; assumption
1336    ]
1337  ]
1338qed.
1339
1340lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
1341  ∀r, l: nat.
1342    r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
1343  #r #l #disj_hyp
1344  cases disj_hyp
1345  [1:
1346    #r_O_refl destruct @nmk
1347    #absurd destruct(absurd)
1348  |2:
1349    #exists_hyp cases exists_hyp #r'
1350    #conj_hyp cases conj_hyp #left_conj #right_conj
1351    destruct @nmk #S_S_refl_hyp
1352    elim right_conj #hyp @hyp //
1353  ]
1354qed.
1355
1356lemma neq_l_r_to_neq_Sl_Sr:
1357  ∀l, r: nat.
1358    l ≠ r → S l ≠ S r.
1359  #l #r #l_neq_r_assm
1360  @nmk #Sl_Sr_assm cases l_neq_r_assm
1361  #assm @assm //
1362qed.
1363
1364lemma eqb_false_to_not_refl:
1365  ∀l, r: nat.
1366    eqb l r = false → l ≠ r.
1367  #l
1368  elim l
1369  [1:
1370    #r cases r
1371    [1:
1372      normalize #absurd destruct(absurd)
1373    |2:
1374      #r' #_ @nmk
1375      #absurd destruct(absurd)
1376    ]
1377  |2:
1378    #l' #inductive_hypothesis #r
1379    cases r
1380    [1:
1381      #eqb_false_assm
1382      @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
1383      @or_introl %
1384    |2:
1385      #r' #eqb_false_assm
1386      @neq_l_r_to_neq_Sl_Sr
1387      @inductive_hypothesis
1388      assumption
1389    ]
1390  ]
1391qed.
1392
1393lemma le_to_lt_or_eq:
1394  ∀m, n: nat.
1395    m ≤ n → m = n ∨ m < n.
1396  #m #n #le_hyp
1397  cases le_hyp
1398  [1:
1399    @or_introl %
1400  |2:
1401    #m' #le_hyp'
1402    @or_intror
1403    normalize
1404    @le_S_S assumption
1405  ]
1406qed.
1407
1408lemma le_neq_to_lt:
1409  ∀m, n: nat.
1410    m ≤ n → m ≠ n → m < n.
1411  #m #n #le_hyp #neq_hyp
1412  cases neq_hyp
1413  #eq_absurd_hyp
1414  generalize in match (le_to_lt_or_eq m n le_hyp);
1415  #disj_assm cases disj_assm
1416  [1:
1417    #absurd cases (eq_absurd_hyp absurd)
1418  |2:
1419    #assm assumption
1420  ]
1421qed.
1422
1423inverter nat_jmdiscr for nat.
1424
1425lemma plus_lt_to_lt:
1426  ∀m, n, o: nat.
1427    m + n < o → m < o.
1428  #m #n #o
1429  elim n
1430  [1:
1431    <(plus_n_O m) in ⊢ (% → ?);
1432    #assumption assumption
1433  |2:
1434    #n' #inductive_hypothesis
1435    <(plus_n_Sm m n') in ⊢ (% → ?);
1436    #assm @inductive_hypothesis
1437    normalize in assm; normalize
1438    /2 by lt_S_to_lt/
1439  ]
1440qed.
1441
1442include "arithmetics/div_and_mod.ma".
1443
1444lemma n_plus_1_n_to_False:
1445  ∀n: nat.
1446    n + 1 = n → False.
1447  #n elim n
1448  [1:
1449    normalize #absurd destruct(absurd)
1450  |2:
1451    #n' #inductive_hypothesis normalize
1452    #absurd @inductive_hypothesis /2/
1453  ]
1454qed.
1455
1456lemma one_two_times_n_to_False:
1457  ∀n: nat.
1458    1=2*n→False.
1459  #n cases n
1460  [1:
1461    normalize #absurd destruct(absurd)
1462  |2:
1463    #n' normalize #absurd
1464    lapply (injective_S … absurd) -absurd #absurd
1465    /2/
1466  ]
1467qed.
1468
1469let rec odd_p
1470  (n: nat)
1471    on n ≝
1472  match n with
1473  [ O ⇒ False
1474  | S n' ⇒ even_p n'
1475  ]
1476and even_p
1477  (n: nat)
1478    on n ≝
1479  match n with
1480  [ O ⇒ True
1481  | S n' ⇒ odd_p n'
1482  ].
1483
1484let rec n_even_p_to_n_plus_2_even_p
1485  (n: nat)
1486    on n: even_p n → even_p (n + 2) ≝
1487  match n with
1488  [ O ⇒ ?
1489  | S n' ⇒ ?
1490  ]
1491and n_odd_p_to_n_plus_2_odd_p
1492  (n: nat)
1493    on n: odd_p n → odd_p (n + 2) ≝
1494  match n with
1495  [ O ⇒ ?
1496  | S n' ⇒ ?
1497  ].
1498  [1,3:
1499    normalize #assm assumption
1500  |2:
1501    normalize @n_odd_p_to_n_plus_2_odd_p
1502  |4:
1503    normalize @n_even_p_to_n_plus_2_even_p
1504  ]
1505qed.
1506
1507let rec two_times_n_even_p
1508  (n: nat)
1509    on n: even_p (2 * n) ≝
1510  match n with
1511  [ O ⇒ ?
1512  | S n' ⇒ ?
1513  ]
1514and two_times_n_plus_one_odd_p
1515  (n: nat)
1516    on n: odd_p ((2 * n) + 1) ≝
1517  match n with
1518  [ O ⇒ ?
1519  | S n' ⇒ ?
1520  ].
1521  [1,3:
1522    normalize @I
1523  |2:
1524    normalize
1525    >plus_n_Sm
1526    <(associative_plus n' n' 1)
1527    >(plus_n_O (n' + n'))
1528    cut(n' + n' + 0 + 1 = 2 * n' + 1)
1529    [1:
1530      //
1531    |2:
1532      #refl_assm >refl_assm
1533      @two_times_n_plus_one_odd_p     
1534    ]
1535  |4:
1536    normalize
1537    >plus_n_Sm
1538    cut(n' + (n' + 1) + 1 = (2 * n') + 2)
1539    [1:
1540      normalize /2/
1541    |2:
1542      #refl_assm >refl_assm
1543      @n_even_p_to_n_plus_2_even_p
1544      @two_times_n_even_p
1545    ]
1546  ]
1547qed.
1548
1549let rec even_p_to_not_odd_p
1550  (n: nat)
1551    on n: even_p n → ¬ odd_p n ≝
1552  match n with
1553  [ O ⇒ ?
1554  | S n' ⇒ ?
1555  ]
1556and odd_p_to_not_even_p
1557  (n: nat)
1558    on n: odd_p n → ¬ even_p n ≝
1559  match n with
1560  [ O ⇒ ?
1561  | S n' ⇒ ?
1562  ].
1563  [1:
1564    normalize #_
1565    @nmk #assm assumption
1566  |3:
1567    normalize #absurd
1568    cases absurd
1569  |2:
1570    normalize
1571    @odd_p_to_not_even_p
1572  |4:
1573    normalize
1574    @even_p_to_not_odd_p
1575  ]
1576qed.
1577
1578lemma even_p_odd_p_cases:
1579  ∀n: nat.
1580    even_p n ∨ odd_p n.
1581  #n elim n
1582  [1:
1583    normalize @or_introl @I
1584  |2:
1585    #n' #inductive_hypothesis
1586    normalize
1587    cases inductive_hypothesis
1588    #assm
1589    try (@or_introl assumption)
1590    try (@or_intror assumption)
1591  ]
1592qed.
1593
1594lemma two_times_n_plus_one_refl_two_times_n_to_False:
1595  ∀m, n: nat.
1596    2 * m + 1 = 2 * n → False.
1597  #m #n
1598  #assm
1599  cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
1600  [1:
1601    >assm
1602    @conj
1603    @two_times_n_even_p
1604  |2:
1605    * #_ #absurd
1606    cases (even_p_to_not_odd_p … absurd)
1607    #assm @assm
1608    @two_times_n_plus_one_odd_p
1609  ]
1610qed.
1611
1612lemma nat_of_bitvector_aux_injective:
1613  ∀n: nat.
1614  ∀l, r: BitVector n.
1615  ∀acc_l, acc_r: nat.
1616    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
1617      acc_l = acc_r ∧ l ≃ r.
1618  #n #l
1619  elim l #r
1620  [1:
1621    #acc_l #acc_r normalize
1622    >(BitVector_O r) normalize /2/
1623  |2:
1624    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
1625    normalize normalize in inductive_hypothesis;
1626    cases (BitVector_Sn … r)
1627    #r_hd * #r_tl #r_refl destruct normalize
1628    cases hd cases r_hd normalize
1629    [1:
1630      #relevant
1631      cases (inductive_hypothesis … relevant)
1632      #acc_assm #tl_assm destruct % //
1633      lapply (injective_plus_l ? ? ? acc_assm)
1634      -acc_assm #acc_assm
1635      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1636      lapply (injective_times_r ? ? ? ? acc_assm) /2/
1637    |4:
1638      #relevant
1639      cases (inductive_hypothesis … relevant)
1640      #acc_assm #tl_assm destruct % //
1641      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1642      lapply(injective_times_r ? ? ? ? acc_assm) /2/
1643    |2:
1644      #relevant 
1645      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
1646        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
1647      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
1648      [1:
1649        #eqb_true_assm
1650        lapply (eqb_true_to_refl … eqb_true_assm)
1651        #refl_assm
1652        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1653      |2:
1654        #eqb_false_assm
1655        lapply (eqb_false_to_not_refl … eqb_false_assm)
1656        #not_refl_assm cases not_refl_assm #absurd_assm
1657        cases (inductive_hypothesis … relevant) #absurd
1658        cases (absurd_assm absurd)
1659      ]
1660    |3:
1661      #relevant 
1662      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
1663        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
1664      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
1665      [1:
1666        #eqb_true_assm
1667        lapply (eqb_true_to_refl … eqb_true_assm)
1668        #refl_assm
1669        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
1670        -refl_assm #refl_assm
1671        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1672      |2:
1673        #eqb_false_assm
1674        lapply (eqb_false_to_not_refl … eqb_false_assm)
1675        #not_refl_assm cases not_refl_assm #absurd_assm
1676        cases (inductive_hypothesis … relevant) #absurd
1677        cases (absurd_assm absurd)
1678      ]
1679    ]
1680  ]
1681qed.
1682
1683lemma nat_of_bitvector_destruct:
1684  ∀n: nat.
1685  ∀l_hd, r_hd: bool.
1686  ∀l_tl, r_tl: BitVector n.
1687    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
1688      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
1689  #n #l_hd #r_hd #l_tl #r_tl
1690  normalize
1691  cases l_hd cases r_hd
1692  normalize
1693  [4:
1694    /2/
1695  |1:
1696    #relevant
1697    cases (nat_of_bitvector_aux_injective … relevant)
1698    #_ #l_r_tl_refl destruct /2/
1699  |2,3:
1700    #relevant
1701    cases (nat_of_bitvector_aux_injective … relevant)
1702    #absurd destruct(absurd)
1703  ]
1704qed.
1705
1706lemma BitVector_cons_injective:
1707  ∀n: nat.
1708  ∀l_hd, r_hd: bool.
1709  ∀l_tl, r_tl: BitVector n.
1710    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
1711  #l #l_hd #r_hd #l_tl #r_tl
1712  #l_refl #r_refl destruct %
1713qed.
1714
1715lemma refl_nat_of_bitvector_to_refl:
1716  ∀n: nat.
1717  ∀l, r: BitVector n.
1718    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
1719  #n
1720  elim n
1721  [1:
1722    #l #r
1723    >(BitVector_O l)
1724    >(BitVector_O r)
1725    #_ %
1726  |2:
1727    #n' #inductive_hypothesis #l #r
1728    lapply (BitVector_Sn ? l) #l_hypothesis
1729    lapply (BitVector_Sn ? r) #r_hypothesis
1730    cases l_hypothesis #l_hd #l_tail_hypothesis
1731    cases r_hypothesis #r_hd #r_tail_hypothesis
1732    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
1733    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
1734    destruct #cons_refl
1735    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
1736    #hd_refl #tl_refl
1737    @BitVector_cons_injective try assumption
1738    @inductive_hypothesis assumption
1739  ]
1740qed.
Note: See TracBrowser for help on using the browser.