include "ASM/ASM.ma". include "ASM/Arithmetic.ma". include "ASM/Fetch.ma". include "ASM/Interpret.ma". include "common/StructuredTraces.ma". let rec fetch_program_counter_n (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word) on n: option Word ≝ match n with [ O ⇒ Some … program_counter | S n ⇒ match fetch_program_counter_n n code_memory program_counter with [ None ⇒ None … | Some tail_pc ⇒ let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then Some … program_counter else None Word (* XXX: overflow! *) ] ]. definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝ λcode_memory: BitVectorTrie Byte 16. λprogram_size: nat. λprogram_counter: Word. (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧ nat_of_bitvector 16 program_counter < program_size. definition well_labelling: BitVectorTrie costlabel 16 → Prop ≝ λcost_labels. injective … (λx. lookup_opt … x cost_labels). definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝ λcode_memory: BitVectorTrie Byte 16. λtotal_program_size: nat. ∀program_counter: Word. ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in match instruction with [ RealInstruction instr ⇒ match instr with [ RET ⇒ True | JC relative ⇒ True (* XXX: see below *) | JNC relative ⇒ True (* XXX: see below *) | JB bit_addr relative ⇒ True | JNB bit_addr relative ⇒ True | JBC bit_addr relative ⇒ True | JZ relative ⇒ True | JNZ relative ⇒ True | CJNE src_trgt relative ⇒ True | DJNZ src_trgt relative ⇒ True | _ ⇒ nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ nat_of_bitvector … program_counter' < total_program_size ] | LCALL addr ⇒ match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with [ ADDR16 addr ⇒ λaddr16: True. reachable_program_counter code_memory total_program_size addr ∧ nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ nat_of_bitvector … program_counter' < total_program_size | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) | ACALL addr ⇒ match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with [ ADDR11 addr ⇒ λaddr11: True. let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in let 〈thr, eig〉 ≝ split … 3 8 addr in let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in reachable_program_counter code_memory total_program_size new_program_counter ∧ nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ nat_of_bitvector … program_counter' < total_program_size | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) | AJMP addr ⇒ match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with [ ADDR11 addr ⇒ λaddr11: True. let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in let 〈nu, nl〉 ≝ split … 4 4 pc_bu in let bit ≝ get_index' … O ? nl in let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in reachable_program_counter code_memory total_program_size new_program_counter | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) | LJMP addr ⇒ match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with [ ADDR16 addr ⇒ λaddr16: True. reachable_program_counter code_memory total_program_size addr | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) | SJMP addr ⇒ match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with [ RELATIVE addr ⇒ λrelative: True. let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in reachable_program_counter code_memory total_program_size new_program_counter | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) | JMP addr ⇒ (* XXX: JMP is used for fptrs and unconstrained *) nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ nat_of_bitvector … program_counter' < total_program_size | MOVC src trgt ⇒ nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ nat_of_bitvector … program_counter' < total_program_size ]. cases other qed. lemma is_a_decidable: ∀hd. ∀element. is_a hd element = true ∨ is_a hd element = false. #hd #element // qed. lemma mem_decidable: ∀n: nat. ∀v: Vector addressing_mode_tag n. ∀element: addressing_mode_tag. mem … eq_a n v element = true ∨ mem … eq_a … v element = false. #n #v #element // qed. lemma eq_a_elim: ∀tag. ∀hd. ∀P: bool → Prop. (tag = hd → P (true)) → (tag ≠ hd → P (false)) → P (eq_a tag hd). #tag #hd #P cases tag cases hd #true_hyp #false_hyp try @false_hyp try @true_hyp try % #absurd destruct(absurd) qed. lemma is_a_true_to_is_in: ∀n: nat. ∀x: addressing_mode. ∀tag: addressing_mode_tag. ∀supervector: Vector addressing_mode_tag n. mem addressing_mode_tag eq_a n supervector tag → is_a tag x = true → is_in … supervector x. #n #x #tag #supervector elim supervector [1: #absurd cases absurd |2: #n' #hd #tl #inductive_hypothesis whd in match (mem … eq_a (S n') (hd:::tl) tag); @eq_a_elim normalize nodelta [1: #tag_hd_eq #irrelevant whd in match (is_in (S n') (hd:::tl) x); is_a_hyp normalize nodelta @I |2: #tag_hd_neq whd in match (is_in (S n') (hd:::tl) x); change with ( mem … eq_a n' tl tag) in match (fold_right … n' ? false tl); #mem_hyp #is_a_hyp cases(is_a hd x) [1: normalize nodelta // |2: normalize nodelta @inductive_hypothesis assumption ] ] ] qed. lemma is_in_subvector_is_in_supervector: ∀m, n: nat. ∀subvector: Vector addressing_mode_tag m. ∀supervector: Vector addressing_mode_tag n. ∀element: addressing_mode. subvector_with … eq_a subvector supervector → is_in m subvector element → is_in n supervector element. #m #n #subvector #supervector #element elim subvector [1: #subvector_with_proof #is_in_proof cases is_in_proof |2: #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof whd in match (is_in … (hd':::tl') element); cases (is_a_decidable hd' element) [1: #is_a_true >is_a_true #irrelevant whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof; @(is_a_true_to_is_in … is_a_true) lapply(subvector_with_proof) cases(mem … eq_a n supervector hd') // |2: #is_a_false >is_a_false normalize nodelta #assm @inductive_hypothesis [1: generalize in match subvector_with_proof; whd in match (subvector_with … eq_a (hd':::tl') supervector); cases(mem_decidable n supervector hd') [1: #mem_true >mem_true normalize nodelta #assm assumption |2: #mem_false >mem_false #absurd cases absurd ] |2: assumption ] ] ] qed. let rec member_addressing_mode_tag (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) on v: Prop ≝ match v with [ VEmpty ⇒ False | VCons n' hd tl ⇒ bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a ]. let rec subaddressing_mode_elim_type (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m) (Q: addressing_mode → T → Prop) (p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T) (p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T) (p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T) (p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T) (p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T) (p_acc_a: is_in m fixed_v ACC_A → T) (p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T) (p_acc_b: is_in m fixed_v ACC_B → T) (p_dptr: is_in m fixed_v DPTR → T) (p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T) (p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T) (p_acc_dptr: is_in m fixed_v ACC_DPTR → T) (p_acc_pc: is_in m fixed_v ACC_PC → T) (p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T) (p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T) (p_carry: is_in m fixed_v CARRY → T) (p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T) (p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T) (p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T) (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v) on v: Prop ≝ match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with [ VEmpty ⇒ λm_refl. λv_refl. ∀addr: addressing_mode. ∀p: is_in m fixed_v addr. Q addr ( match addr return λx: addressing_mode. is_in … fixed_v x → T with  [ ADDR11 x ⇒ p_addr11 x | ADDR16 x ⇒ p_addr16 x | DIRECT x ⇒ p_direct x | INDIRECT x ⇒ p_indirect x | EXT_INDIRECT x ⇒ p_ext_indirect x | ACC_A ⇒ p_acc_a | REGISTER x ⇒ p_register x | ACC_B ⇒ p_acc_b | DPTR ⇒ p_dptr | DATA x ⇒ p_data x | DATA16 x ⇒ p_data16 x | ACC_DPTR ⇒ p_acc_dptr | ACC_PC ⇒ p_acc_pc | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr | INDIRECT_DPTR ⇒ p_indirect_dptr | CARRY ⇒ p_carry | BIT_ADDR x ⇒ p_bit_addr x | N_BIT_ADDR x ⇒ p_n_bit_addr x | RELATIVE x ⇒ p_relative x ] p) | VCons n' hd tl ⇒ λm_refl. λv_refl. let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11 p_addr16 p_direct p_indirect p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr p_relative n' tl ? in match hd return λa: addressing_mode_tag. a = hd → ? with [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call | addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call | direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call | indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call | ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call | acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call | registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call | acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call | dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call | data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call | data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call | acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call | acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call | indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call | carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call | bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call | n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call | relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call ] (refl … hd) ] (refl … n) (refl_jmeq … v). [20: generalize in match proof; destruct whd in match (subvector_with … eq_a (hd:::tl) fixed_v); cases (mem … eq_a m fixed_v hd) normalize nodelta [1: whd in match (subvector_with … eq_a tl fixed_v); #assm assumption |2: normalize in ⊢ (% → ?); #absurd cases absurd ] ] @(is_in_subvector_is_in_supervector … proof) destruct @I qed. (* XXX: todo *) lemma subaddressing_mode_elim': ∀T: Type[2]. ∀n: nat. ∀o: nat. ∀Q: addressing_mode → T → Prop. ∀fixed_v: Vector addressing_mode_tag (n + o). ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. ∀v1: Vector addressing_mode_tag n. ∀v2: Vector addressing_mode_tag o. ∀fixed_v_proof: fixed_v = v1 @@ v2. ∀subaddressing_mode_proof. subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof. #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof cases daemon qed. (* XXX: todo *) axiom subaddressing_mode_elim: ∀T: Type[2]. ∀m: nat. ∀n: nat. ∀Q: addressing_mode → T → Prop. ∀fixed_v: Vector addressing_mode_tag m. ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. ∀v: Vector addressing_mode_tag n. ∀proof. subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof. definition current_instruction_is_labelled ≝ λcode_memory. λcost_labels: BitVectorTrie costlabel 16. λs: Status code_memory. let pc ≝ program_counter … code_memory s in match lookup_opt … pc cost_labels with [ None ⇒ False | _ ⇒ True ]. definition next_instruction_properly_relates_program_counters ≝ λcode_memory. λbefore: Status code_memory. λafter : Status code_memory. let size ≝ current_instruction_cost code_memory before in let pc_before ≝ program_counter … code_memory before in let pc_after ≝ program_counter … code_memory after in let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in sum = pc_after. definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝ λcode_memory. λcost_labels. mk_abstract_status (Status code_memory) (λs,s'. (execute_1 … s) = s') (λs,class. ASM_classify … s = class) (current_instruction_is_labelled … cost_labels) (next_instruction_properly_relates_program_counters code_memory). let rec trace_any_label_length (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory) (final_status: Status code_memory) (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status) on the_trace: nat ≝ match the_trace with [ tal_base_not_return the_status _ _ _ _ ⇒ 0 | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 0 | tal_base_return the_status _ _ _ ⇒ 0 | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒ let tail_length ≝ trace_any_label_length … final_trace in let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in pc_difference + tail_length | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ let tail_length ≝ trace_any_label_length … tail_trace in let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in pc_difference + tail_length ]. let rec compute_paid_trace_any_label (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory) (final_status: Status code_memory) (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status) on the_trace: nat ≝ match the_trace with [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒ let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in current_instruction_cost + final_trace_cost | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ let current_instruction_cost ≝ current_instruction_cost … status_pre in let tail_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag status_init status_end tail_trace in current_instruction_cost + tail_trace_cost ]. definition compute_paid_trace_label_label ≝ λcode_memory: BitVectorTrie Byte 16. λcost_labels: BitVectorTrie costlabel 16. λtrace_ends_flag: trace_ends_with_ret. λstart_status: Status code_memory. λfinal_status: Status code_memory. λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. match the_trace with [ tll_base ends_flag initial final given_trace labelled_proof ⇒ compute_paid_trace_any_label … given_trace ]. include alias "arithmetics/nat.ma". include alias "basics/logic.ma". lemma plus_right_monotone: ∀m, n, o: nat. m = n → m + o = n + o. #m #n #o #refl >refl % qed. lemma minus_plus_cancel: ∀m, n : nat. ∀proof: n ≤ m. (m - n) + n = m. #m #n #proof /2 by plus_minus/ qed. (* XXX: indexing bug *) lemma fetch_twice_fetch_execute_1: ∀code_memory: BitVectorTrie Byte 16. ∀start_status: Status code_memory. ASM_classify code_memory start_status = cl_other → \snd (\fst (fetch code_memory (program_counter … start_status))) = program_counter … (execute_1 … start_status). #code_memory #start_status #classify_assm whd in match execute_1; normalize nodelta cases (execute_1' code_memory start_status) #the_status * #_ #classify_assm' @classify_assm' assumption qed-. lemma reachable_program_counter_to_0_lt_total_program_size: ∀code_memory: BitVectorTrie Byte 16. ∀program_counter: Word. ∀total_program_size: nat. reachable_program_counter code_memory total_program_size program_counter → 0 < total_program_size. #code_memory #program_counter #total_program_size whd in match reachable_program_counter; normalize nodelta * * #some_n #_ cases (nat_of_bitvector 16 program_counter) [1: #assm assumption |2: #new_pc @ltn_to_ltO ] qed. lemma trace_compute_paid_trace_cl_other: ∀code_memory' : (BitVectorTrie Byte 16). ∀program_counter' : Word. ∀total_program_size : ℕ. ∀cost_labels : (BitVectorTrie costlabel 16). ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter'). ∀good_program_witness : (good_program code_memory' total_program_size). ∀program_size' : ℕ. ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter'). ∀ticks : ℕ. ∀instruction : instruction. ∀program_counter'' : Word. ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). ∀start_status : (Status code_memory'). ∀final_status : (Status code_memory'). ∀trace_ends_flag : trace_ends_with_ret. ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). ∀classify_assm: ASM_classify0 instruction = cl_other. ∀pi1 : ℕ. (if match lookup_opt costlabel 16 program_counter'' cost_labels with  [None ⇒ true |Some _ ⇒ false ]  then ∀start_status0:Status code_memory'. ∀final_status0:Status code_memory'. ∀trace_ends_flag0:trace_ends_with_ret. ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0. program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 → (∃n:ℕ .trace_any_label_length code_memory' cost_labels trace_ends_flag0 start_status0 final_status0 the_trace0 +S n =total_program_size) ∧pi1 =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag0 start_status0 final_status0 the_trace0 else (pi1=O) ) →(∃n:ℕ .trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace +S n =total_program_size) ∧ticks+pi1 =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace. #code_memory' #program_counter' #total_program_size #cost_labels #reachable_program_counter_witness #good_program_witness #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm @(trace_any_label_inv_ind … the_trace) [5: #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl #the_trace_refl destruct whd in match (trace_any_label_length … (tal_step_default …)); whd in match (compute_paid_trace_any_label … (tal_step_default …)); whd in costed_assm:(?%); generalize in match costed_assm; generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)); generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels) in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?); #lookup_assm cases lookup_assm [1: #None_lookup_opt_assm normalize nodelta #ignore generalize in match recursive_assm; cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre))) [1: classifier_assm % ] |2: #program_counter_assm >program_counter_assm recursive_block_cost_assm whd in match (current_instruction_cost … status_pre); cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre))) [1: ticks_refl_assm % ] ] ] |2: #costlabel #Some_lookup_opt_assm None_lookup_opt_assm #absurd cases absurd |2: #costlabel #Some_lookup_opt_assm normalize nodelta #ignore generalize in match recursive_assm; cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start))) [1: contradiction #absurd destruct(absurd) ] try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd)) try(#addr normalize nodelta #ignore #absurd destruct(absurd)) normalize in ignore; destruct(ignore) |2: #classifier_assm' >classifier_assm' % ] ] |2: #program_counter_assm >program_counter_assm new_recursive_assm % [1: %{(pred total_program_size)} whd in ⊢ (??%?); @S_pred @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) |2: cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_start))) [1: ticks_refl_assm classify_assm #absurd destruct(absurd) qed. lemma trace_compute_paid_trace_cl_jump: ∀code_memory': BitVectorTrie Byte 16. ∀program_counter': Word. ∀total_program_size: ℕ. ∀cost_labels: BitVectorTrie costlabel 16. ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'. ∀good_program_witness: good_program code_memory' total_program_size. ∀first_time_around: bool. ∀program_size': ℕ. ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'. ∀ticks: ℕ. ∀instruction: instruction. ∀program_counter'': Word. ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'. ∀start_status: (Status code_memory'). ∀final_status: (Status code_memory'). ∀trace_ends_flag: trace_ends_with_ret. ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). ∀classify_assm: ASM_classify0 instruction = cl_jump. (∃n:ℕ .trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace +S n =total_program_size) ∧ticks =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace. #code_memory' #program_counter' #total_program_size #cost_labels #reachable_program_counter_witness #good_program_witness #first_time_around #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl #classify_assm @(trace_any_label_inv_ind … the_trace) [5: #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl #the_trace_refl destruct @⊥ |1: #status_start #status_final #execute_assm #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct whd in match (trace_any_label_length … (tal_base_not_return …)); whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); % [1: %{(pred total_program_size)} whd in ⊢ (??%?); @S_pred @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) |2: classify_assm #absurd destruct(absurd) qed. lemma trace_compute_paid_trace_cl_call: ∀code_memory' : (BitVectorTrie Byte 16). ∀program_counter' : Word. ∀total_program_size : ℕ. ∀cost_labels : (BitVectorTrie costlabel 16). ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter'). ∀good_program_witness : (good_program code_memory' total_program_size). ∀program_size' : ℕ. ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter'). ∀ticks : ℕ. ∀instruction : instruction. ∀program_counter'' : Word. ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). ∀start_status : (Status code_memory'). ∀final_status : (Status code_memory'). ∀trace_ends_flag : trace_ends_with_ret. ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). ∀classify_assm: ASM_classify0 instruction = cl_call. (∀pi1:ℕ .if match lookup_opt costlabel 16 program_counter'' cost_labels with  [None ⇒ true | Some _ ⇒ false]  then (∀start_status0:Status code_memory' .∀final_status0:Status code_memory' .∀trace_ends_flag0:trace_ends_with_ret .∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0 .program_counter'' =program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →(∃n:ℕ .trace_any_label_length code_memory' cost_labels trace_ends_flag0 start_status0 final_status0 the_trace0 +S n =total_program_size) ∧pi1 =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag0 start_status0 final_status0 the_trace0)  else (pi1=O)  →(∃n:ℕ .trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace +S n =total_program_size) ∧ticks+pi1 =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace). #code_memory' #program_counter' #total_program_size #cost_labels #reachable_program_counter_witness #good_program_witness #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm @(trace_any_label_inv_ind … the_trace) [5: #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl #the_trace_refl destruct @⊥ |1: #status_start #status_final #execute_assm #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct @⊥ |2: #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |3: #status_pre_fun_call #status_start_fun_call #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return #costed_assm #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct whd in match (trace_any_label_length … (tal_base_call …)); whd in match (compute_paid_trace_any_label … (tal_base_call …)); whd in costed_assm; generalize in match costed_assm; generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels)); generalize in match (lookup_opt … (program_counter … status_final) cost_labels) in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?); #lookup_assm cases lookup_assm [1: #None_lookup_opt normalize nodelta #absurd cases absurd |2: #costlabel #Some_lookup_opt normalize nodelta #ignore generalize in match recursive_assm; cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final)) [1: whd in after_return_assm; program_counter_assm new_recursive_assm % [1: %{(pred total_program_size)} whd in ⊢ (??%?); @S_pred @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) |2: cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call))) [1: ticks_refl_assm program_counter_refl recursive_block_cost_assm @plus_right_monotone whd in ⊢ (???%); associative_plus in ⊢ (??%?); >commutative_plus in ⊢ (??%?); >associative_plus @eq_f classify_assm #absurd destruct(absurd) cases absurd #absurd destruct(absurd) qed. lemma trace_compute_paid_trace_cl_return: ∀code_memory' : (BitVectorTrie Byte 16). ∀program_counter' : Word. ∀total_program_size : ℕ. ∀cost_labels : (BitVectorTrie costlabel 16). ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter'). ∀good_program_witness : (good_program code_memory' total_program_size). ∀program_size' : ℕ. ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter'). ∀ticks : ℕ. ∀instruction : instruction. ∀program_counter'' : Word. ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). ∀start_status : (Status code_memory'). ∀final_status : (Status code_memory'). ∀trace_ends_flag : trace_ends_with_ret. ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). ∀classify_assm: ASM_classify0 instruction = cl_return. (∃n:ℕ .trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace +S n =total_program_size) ∧ticks =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace. #code_memory' #program_counter' #total_program_size #cost_labels #reachable_program_counter_witness #good_program_witness #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl #classify_assm @(trace_any_label_inv_ind … the_trace) [1: #start_status' #final_status' #execute_assm #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct @⊥ |2: #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct whd in match (trace_any_label_length … (tal_base_return …)); whd in match (compute_paid_trace_any_label … (tal_base_return …)); % [1: %{(pred total_program_size)} whd in ⊢ (??%?); @S_pred @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) |2: classify_assm #absurd try (destruct(absurd)) cases absurd #absurd destruct(absurd) qed. let rec block_cost' (code_memory': BitVectorTrie Byte 16) (program_counter': Word) (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16) (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter') (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool) on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter' → Σcost_of_block: nat. if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then ∀start_status: Status code_memory'. ∀final_status: Status code_memory'. ∀trace_ends_flag. ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. program_counter' = program_counter … start_status → (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace else (cost_of_block = 0) ≝ match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with [ O ⇒ λbase_case. ⊥ | S program_size' ⇒ λrecursive_case. let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in let to_continue ≝ match lookup_opt … program_counter' cost_labels with [ None ⇒ true | Some _ ⇒ first_time_around ] in ((if to_continue then pi1 … (match instruction return λx. x = instruction → ? with [ RealInstruction real_instruction ⇒ λreal_instruction_refl. match real_instruction return λx. x = real_instruction → Σcost_of_block: nat. ∀start_status: Status code_memory'. ∀final_status: Status code_memory'. ∀trace_ends_flag. ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status. program_counter' = program_counter … start_status → (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with [ RET ⇒ λinstr. ticks | RETI ⇒ λinstr. ticks | JC relative ⇒ λinstr. ticks | JNC relative ⇒ λinstr. ticks | JB bit_addr relative ⇒ λinstr. ticks | JNB bit_addr relative ⇒ λinstr. ticks | JBC bit_addr relative ⇒ λinstr. ticks | JZ relative ⇒ λinstr. ticks | JNZ relative ⇒ λinstr. ticks | CJNE src_trgt relative ⇒ λinstr. ticks | DJNZ src_trgt relative ⇒ λinstr. ticks | _ ⇒ λinstr. ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? ] (refl …) | ACALL addr ⇒ λinstr. ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? | AJMP addr ⇒ λinstr. ticks | LCALL addr ⇒ λinstr. ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? | LJMP addr ⇒ λinstr. ticks | SJMP addr ⇒ λinstr. ticks | JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *) ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? | MOVC src trgt ⇒ λinstr. ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? ] (refl …)) else 0) : Σcost_of_block: nat. match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with [ true ⇒ ∀start_status: Status code_memory'. ∀final_status: Status code_memory'. ∀trace_ends_flag. ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. program_counter' = program_counter … start_status → (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace | false ⇒ (cost_of_block = 0) ]) ]. [1: cases reachable_program_counter_witness #_ #hyp @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …)) @(le_to_lt_to_lt … base_case hyp) |2: change with (if to_continue then ? else (? = 0)) >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta @pi2 |3: change with (if to_continue then ? else (0 = 0)) >p normalize nodelta % |7,8: #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) destruct % |96,102,105: #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl cases(block_cost' ?????????) -block_cost' @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl) destruct % |4,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,69,72,75,78,81,84,87, 90,93: #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl cases(block_cost' ?????????) -block_cost' @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) destruct % |60,61,62,63,64,65,66,67,68,69,99,101,100,102: #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) destruct % |103: cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp lapply(good_program_witness program_counter' reachable_program_counter_witness) (le_to_leb_true … program_counter_lt') % |2: assumption ] |104: cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp lapply(good_program_witness program_counter' reachable_program_counter_witness) plus_n_Sm @monotonic_le_plus_r change with ( nat_of_bitvector … program_counter' < nat_of_bitvector … program_counter'') assumption |106: cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp lapply(good_program_witness program_counter' reachable_program_counter_witness) (le_to_leb_true … program_counter_lt') % |2: assumption ] |107: cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp lapply(good_program_witness program_counter' reachable_program_counter_witness) plus_n_Sm @monotonic_le_plus_r change with ( nat_of_bitvector … program_counter' < nat_of_bitvector … program_counter'') assumption |94,97: cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp lapply(good_program_witness program_counter' reachable_program_counter_witness) (le_to_leb_true … program_counter_lt') % |2,4: assumption ] |5,10,12,13,16,18,19,22,25,28,31,34,37,40,43,46,49,52,55,58,70,73, 76,79,82,85,88,91: cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp lapply(good_program_witness program_counter' reachable_program_counter_witness) (le_to_leb_true … program_counter_lt') % (* XXX: got to here *) |6,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89, 92: cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp lapply(good_program_witness program_counter' reachable_program_counter_witness) plus_n_Sm @monotonic_le_plus_r change with ( nat_of_bitvector … program_counter' < nat_of_bitvector … program_counter'') assumption |95,98: cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp lapply(good_program_witness program_counter' reachable_program_counter_witness) plus_n_Sm @monotonic_le_plus_r change with ( nat_of_bitvector … program_counter' < nat_of_bitvector … program_counter'') assumption ] qed. definition block_cost: ∀code_memory': BitVectorTrie Byte 16. ∀program_counter': Word. ∀total_program_size: nat. ∀cost_labels: BitVectorTrie costlabel 16. ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'. ∀good_program_witness: good_program code_memory' total_program_size. Σcost_of_block: nat. ∀start_status: Status code_memory'. ∀final_status: Status code_memory'. ∀trace_ends_flag. ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. program_counter' = program_counter … start_status → (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝ λcode_memory: BitVectorTrie Byte 16. λprogram_counter: Word. λtotal_program_size: nat. λcost_labels: BitVectorTrie costlabel 16. λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. λgood_program_witness: good_program code_memory total_program_size. ?. cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels reachable_program_counter_witness good_program_witness true ?) [1: #cost_of_block #block_cost_hyp %{cost_of_block} cases(lookup_opt … cost_labels) in block_cost_hyp; [2: #cost_label] normalize nodelta #hyp assumption |2: @le_plus_n_r ] qed. lemma fetch_program_counter_n_Sn: ∀instruction: instruction. ∀program_counter, program_counter': Word. ∀ticks, n: nat. ∀code_memory: BitVectorTrie Byte 16. Some … program_counter = fetch_program_counter_n n code_memory (zero 16) → 〈instruction,program_counter',ticks〉 = fetch code_memory program_counter → nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' → Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …). #instruction #program_counter #program_counter' #ticks #n #code_memory #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp whd in match (fetch_program_counter_n (S n) code_memory (zero …)); (le_to_leb_true … lt_hyp) % qed. (* XXX: to be moved into common/Identifiers.ma *) lemma lookup_present_add_hit: ∀tag, A, map, k, v, k_pres. lookup_present tag A (add … map k v) k k_pres = v. #tag #a #map #k #v #k_pres lapply (lookup_lookup_present … (add … map k v) … k_pres) >lookup_add_hit #Some_assm destruct(Some_assm) lookup_add_miss try assumption #Some_assm lapply (lookup_lookup_present … map k') >Some_assm #Some_assm' lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption qed. (* XXX: to be moved into basics/types.ma *) lemma not_None_to_Some: ∀A: Type[0]. ∀o: option A. o ≠ None A → ∃v: A. o = Some A v. #A #o cases o [1: #absurd cases absurd #absurd' cases (absurd' (refl …)) |2: #v' #ignore /2/ ] qed. lemma present_add_present: ∀tag, a, map, k, k', v. k' ≠ k → present tag a (add tag a map k v) k' → present tag a map k'. #tag #a #map #k #k' #v #neq_hyp #present_hyp whd in match present; normalize nodelta whd in match present in present_hyp; normalize nodelta in present_hyp; cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp lapply (lookup_add_cases tag ?????? Some_eq_hyp) * [1: * #k_eq_hyp @⊥ /2/ |2: #Some_eq_hyp' /2/ ] qed. lemma present_add_hit: ∀tag, a, map, k, v. present tag a (add tag a map k v) k. #tag #a #map #k #v whd >lookup_add_hit % #absurd destruct qed. lemma present_add_miss: ∀tag, a, map, k, k', v. k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'. #tag #a #map #k #k' #v #neq_assm #present_assm whd >lookup_add_miss assumption qed. lemma lt_to_le_to_le: ∀n, m, p: nat. n < m → m ≤ p → n ≤ p. #n #m #p #H #H1 elim H [1: @(transitive_le n m p) /2/ |2: /2/ ] qed. lemma eqb_decidable: ∀l, r: nat. (eqb l r = true) ∨ (eqb l r = false). #l #r // qed. lemma r_Sr_and_l_r_to_Sl_r: ∀r, l: nat. (∃r': nat. r = S r' ∧ l = r') → S l = r. #r #l #exists_hyp cases exists_hyp #r' #and_hyp cases and_hyp #left_hyp #right_hyp destruct % qed. lemma eqb_Sn_to_exists_n': ∀m, n: nat. eqb (S m) n = true → ∃n': nat. n = S n'. #m #n cases n [1: normalize #absurd destruct(absurd) |2: #n' #_ %{n'} % ] qed. lemma eqb_true_to_eqb_S_S_true: ∀m, n: nat. eqb m n = true → eqb (S m) (S n) = true. #m #n normalize #assm assumption qed. lemma eqb_S_S_true_to_eqb_true: ∀m, n: nat. eqb (S m) (S n) = true → eqb m n = true. #m #n normalize #assm assumption qed. lemma eqb_true_to_refl: ∀l, r: nat. eqb l r = true → l = r. #l elim l [1: #r cases r [1: #_ % |2: #l' normalize #absurd destruct(absurd) ] |2: #l' #inductive_hypothesis #r #eqb_refl @r_Sr_and_l_r_to_Sl_r %{(pred r)} @conj [1: cases (eqb_Sn_to_exists_n' … eqb_refl) #r' #S_assm >S_assm % |2: cases (eqb_Sn_to_exists_n' … eqb_refl) #r' #refl_assm destruct normalize @inductive_hypothesis normalize in eqb_refl; assumption ] ] qed. lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r: ∀r, l: nat. r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r. #r #l #disj_hyp cases disj_hyp [1: #r_O_refl destruct @nmk #absurd destruct(absurd) |2: #exists_hyp cases exists_hyp #r' #conj_hyp cases conj_hyp #left_conj #right_conj destruct @nmk #S_S_refl_hyp elim right_conj #hyp @hyp // ] qed. lemma neq_l_r_to_neq_Sl_Sr: ∀l, r: nat. l ≠ r → S l ≠ S r. #l #r #l_neq_r_assm @nmk #Sl_Sr_assm cases l_neq_r_assm #assm @assm // qed. lemma eqb_false_to_not_refl: ∀l, r: nat. eqb l r = false → l ≠ r. #l elim l [1: #r cases r [1: normalize #absurd destruct(absurd) |2: #r' #_ @nmk #absurd destruct(absurd) ] |2: #l' #inductive_hypothesis #r cases r [1: #eqb_false_assm @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r @or_introl % |2: #r' #eqb_false_assm @neq_l_r_to_neq_Sl_Sr @inductive_hypothesis assumption ] ] qed. lemma le_to_lt_or_eq: ∀m, n: nat. m ≤ n → m = n ∨ m < n. #m #n #le_hyp cases le_hyp [1: @or_introl % |2: #m' #le_hyp' @or_intror normalize @le_S_S assumption ] qed. lemma le_neq_to_lt: ∀m, n: nat. m ≤ n → m ≠ n → m < n. #m #n #le_hyp #neq_hyp cases neq_hyp #eq_absurd_hyp generalize in match (le_to_lt_or_eq m n le_hyp); #disj_assm cases disj_assm [1: #absurd cases (eq_absurd_hyp absurd) |2: #assm assumption ] qed. inverter nat_jmdiscr for nat. (* XXX: this is false in the general case. For instance, if n = 0 then the base case requires us prove 1 = 0, as it is the carry bit that holds the result of the addition. *) axiom succ_nat_of_bitvector_half_add_1: ∀n: nat. ∀bv: BitVector n. ∀power_proof: nat_of_bitvector … bv < 2^n - 1. S (nat_of_bitvector … bv) = nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)). lemma plus_lt_to_lt: ∀m, n, o: nat. m + n < o → m < o. #m #n #o elim n [1: <(plus_n_O m) in ⊢ (% → ?); #assumption assumption |2: #n' #inductive_hypothesis <(plus_n_Sm m n') in ⊢ (% → ?); #assm @inductive_hypothesis normalize in assm; normalize /2 by lt_S_to_lt/ ] qed. include "arithmetics/div_and_mod.ma". lemma n_plus_1_n_to_False: ∀n: nat. n + 1 = n → False. #n elim n [1: normalize #absurd destruct(absurd) |2: #n' #inductive_hypothesis normalize #absurd @inductive_hypothesis /2/ ] qed. lemma one_two_times_n_to_False: ∀n: nat. 1=2*n→False. #n cases n [1: normalize #absurd destruct(absurd) |2: #n' normalize #absurd lapply (injective_S … absurd) -absurd #absurd /2/ ] qed. lemma generalized_nat_cases: ∀n: nat. n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m). #n cases n [1: @or_introl @or_introl % |2: #n' cases n' [1: @or_introl @or_intror % |2: #n'' @or_intror %{n''} % ] ] qed. let rec odd_p (n: nat) on n ≝ match n with [ O ⇒ False | S n' ⇒ even_p n' ] and even_p (n: nat) on n ≝ match n with [ O ⇒ True | S n' ⇒ odd_p n' ]. let rec n_even_p_to_n_plus_2_even_p (n: nat) on n: even_p n → even_p (n + 2) ≝ match n with [ O ⇒ ? | S n' ⇒ ? ] and n_odd_p_to_n_plus_2_odd_p (n: nat) on n: odd_p n → odd_p (n + 2) ≝ match n with [ O ⇒ ? | S n' ⇒ ? ]. [1,3: normalize #assm assumption |2: normalize @n_odd_p_to_n_plus_2_odd_p |4: normalize @n_even_p_to_n_plus_2_even_p ] qed. let rec two_times_n_even_p (n: nat) on n: even_p (2 * n) ≝ match n with [ O ⇒ ? | S n' ⇒ ? ] and two_times_n_plus_one_odd_p (n: nat) on n: odd_p ((2 * n) + 1) ≝ match n with [ O ⇒ ? | S n' ⇒ ? ]. [1,3: normalize @I |2: normalize >plus_n_Sm <(associative_plus n' n' 1) >(plus_n_O (n' + n')) cut(n' + n' + 0 + 1 = 2 * n' + 1) [1: // |2: #refl_assm >refl_assm @two_times_n_plus_one_odd_p ] |4: normalize >plus_n_Sm cut(n' + (n' + 1) + 1 = (2 * n') + 2) [1: normalize /2/ |2: #refl_assm >refl_assm @n_even_p_to_n_plus_2_even_p @two_times_n_even_p ] ] qed. let rec even_p_to_not_odd_p (n: nat) on n: even_p n → ¬ odd_p n ≝ match n with [ O ⇒ ? | S n' ⇒ ? ] and odd_p_to_not_even_p (n: nat) on n: odd_p n → ¬ even_p n ≝ match n with [ O ⇒ ? | S n' ⇒ ? ]. [1: normalize #_ @nmk #assm assumption |3: normalize #absurd cases absurd |2: normalize @odd_p_to_not_even_p |4: normalize @even_p_to_not_odd_p ] qed. lemma even_p_odd_p_cases: ∀n: nat. even_p n ∨ odd_p n. #n elim n [1: normalize @or_introl @I |2: #n' #inductive_hypothesis normalize cases inductive_hypothesis #assm try (@or_introl assumption) try (@or_intror assumption) ] qed. lemma two_times_n_plus_one_refl_two_times_n_to_False: ∀m, n: nat. 2 * m + 1 = 2 * n → False. #m #n #assm cut (even_p (2 * n) ∧ even_p ((2 * m) + 1)) [1: >assm @conj @two_times_n_even_p |2: * #_ #absurd cases (even_p_to_not_odd_p … absurd) #assm @assm @two_times_n_plus_one_odd_p ] qed. lemma nat_of_bitvector_aux_injective: ∀n: nat. ∀l, r: BitVector n. ∀acc_l, acc_r: nat. nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r → acc_l = acc_r ∧ l ≃ r. #n #l elim l #r [1: #acc_l #acc_r normalize >(BitVector_O r) normalize /2/ |2: #hd #tl #inductive_hypothesis #r #acc_l #acc_r normalize normalize in inductive_hypothesis; cases (BitVector_Sn … r) #r_hd * #r_tl #r_refl destruct normalize cases hd cases r_hd normalize [1: #relevant cases (inductive_hypothesis … relevant) #acc_assm #tl_assm destruct % // lapply (injective_plus_l ? ? ? acc_assm) -acc_assm #acc_assm change with (2 * acc_l = 2 * acc_r) in acc_assm; lapply (injective_times_r ? ? ? ? acc_assm) /2/ |4: #relevant cases (inductive_hypothesis … relevant) #acc_assm #tl_assm destruct % // change with (2 * acc_l = 2 * acc_r) in acc_assm; lapply(injective_times_r ? ? ? ? acc_assm) /2/ |2: #relevant change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) = (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant; cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r)) [1: #eqb_true_assm lapply (eqb_true_to_refl … eqb_true_assm) #refl_assm cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm) |2: #eqb_false_assm lapply (eqb_false_to_not_refl … eqb_false_assm) #not_refl_assm cases not_refl_assm #absurd_assm cases (inductive_hypothesis … relevant) #absurd cases (absurd_assm absurd) ] |3: #relevant change with ((nat_of_bitvector_aux r (2 * acc_l) tl) = (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant; cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1)) [1: #eqb_true_assm lapply (eqb_true_to_refl … eqb_true_assm) #refl_assm lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm) -refl_assm #refl_assm cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm) |2: #eqb_false_assm lapply (eqb_false_to_not_refl … eqb_false_assm) #not_refl_assm cases not_refl_assm #absurd_assm cases (inductive_hypothesis … relevant) #absurd cases (absurd_assm absurd) ] ] ] qed. lemma nat_of_bitvector_destruct: ∀n: nat. ∀l_hd, r_hd: bool. ∀l_tl, r_tl: BitVector n. nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) → l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl. #n #l_hd #r_hd #l_tl #r_tl normalize cases l_hd cases r_hd normalize [4: /2/ |1: #relevant cases (nat_of_bitvector_aux_injective … relevant) #_ #l_r_tl_refl destruct /2/ |2,3: #relevant cases (nat_of_bitvector_aux_injective … relevant) #absurd destruct(absurd) ] qed. lemma BitVector_cons_injective: ∀n: nat. ∀l_hd, r_hd: bool. ∀l_tl, r_tl: BitVector n. l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl. #l #l_hd #r_hd #l_tl #r_tl #l_refl #r_refl destruct % qed. lemma refl_nat_of_bitvector_to_refl: ∀n: nat. ∀l, r: BitVector n. nat_of_bitvector n l = nat_of_bitvector n r → l = r. #n elim n [1: #l #r >(BitVector_O l) >(BitVector_O r) #_ % |2: #n' #inductive_hypothesis #l #r lapply (BitVector_Sn ? l) #l_hypothesis lapply (BitVector_Sn ? r) #r_hypothesis cases l_hypothesis #l_hd #l_tail_hypothesis cases r_hypothesis #r_hd #r_tail_hypothesis cases l_tail_hypothesis #l_tl #l_hd_tl_refl cases r_tail_hypothesis #r_tl #r_hd_tl_refl destruct #cons_refl cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl) #hd_refl #tl_refl @BitVector_cons_injective try assumption @inductive_hypothesis assumption ] qed.