root/src/ASM/ASMCosts.ma @ 1924

Revision 1924, 67.5 KB (checked in by mulligan, 13 months ago)

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