source: src/ASM/ASMCosts.ma @ 1921

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

Horror proof mostly finished (compiles all way until end of CostsProof?.ma).

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