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. let rec traverse_code_internal (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) (program_counter: Word) (fixed_program_size: nat) (program_size: nat) (reachable_program_counter_witness: ∀lbl: costlabel. ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → reachable_program_counter code_memory fixed_program_size program_counter) (good_program_witness: good_program code_memory fixed_program_size) (program_size_invariant: nat_of_bitvector … program_counter + program_size = fixed_program_size) (fixed_program_size_limit: fixed_program_size < 2^16 + 1) on program_size: Σcost_map: identifier_map CostTag nat. (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧ (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ match program_size return λx. x = program_size → Σcost_map: ?. ? with [ O ⇒ λprogram_size_refl. empty_map … | S program_size' ⇒ λprogram_size_refl. pi1 … (let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in let 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' fixed_program_size program_size' ? good_program_witness ? fixed_program_size_limit in match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧ (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) with [ None ⇒ λlookup_refl. pi1 … cost_mapping | Some lbl ⇒ λlookup_refl. let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in add … cost_mapping lbl cost ] (refl … (lookup_opt … program_counter cost_labels))) ] (refl … program_size). cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter))) [1,3,5,7,9,11,13: |14: cases daemon (* XXX: russell error here i think *) |2: #_ % [1: #pc #k #absurd1 #absurd2 @⊥ lapply(lt_to_not_le … absurd2) * #absurd @absurd assumption |2: #k #k_pres @⊥ normalize in k_pres; /2/ ] |4: #S_assm cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter)) [1: new_program_counter_assm' eq_assm cases cost_mapping #cost_mapping' * #ind_hyp #_ @present_add_hit |2: #neq_assm @present_add_miss try assumption cases cost_mapping #cost_mapping' * #ind_hyp #_ @(ind_hyp … lookup_opt_assm) [1: generalize in match (eqb_decidable (nat_of_bitvector … program_counter) (nat_of_bitvector … pc)); #hyp cases hyp [1: #relevant generalize in match (eqb_true_to_refl … relevant); #rewrite_assm plus_n_Sm in ⊢ (% → ?); cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)) [1: new_program_counter_assm' >S_assm #relevant assumption ] ] ] |2: #k #k_pres @(eq_identifier_elim … k lbl) [1: #eq_assm %{program_counter} #lookup_opt_assm %{(reachable_program_counter_witness …)} try assumption >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % |2: #neq_assm cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm cases ind_hyp #_ #relevant cases (relevant k ?) [2: @(present_add_present … present_assm) assumption |1: #program_counter' #ind_hyp' %{program_counter'} #relevant cases (ind_hyp' relevant) #reachable_witness' #ind_hyp'' %{reachable_witness'} >ind_hyp'' @sym_eq @lookup_present_add_miss assumption ] ] ] |12: #S_assm % [1: #pc #k #H1 #H2 #lookup_opt_assm whd >lookup_opt_assm |2: ] ] |5: % [2: #k #k_pres @(eq_identifier_elim … k lbl) [1: #eq_assm %{program_counter} #lookup_opt_assm %{(reachable_program_counter_witness …)} try assumption >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % |2: #neq_assm cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm cases ind_hyp #_ #relevant cases (relevant k ?) [2: @(present_add_present … present_assm) assumption |1: #program_counter' #ind_hyp' %{program_counter'} #relevant cases (ind_hyp' relevant) #reachable_witness' #ind_hyp'' %{reachable_witness'} >ind_hyp'' @sym_eq @lookup_present_add_miss assumption ] ] |1: #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl) [1: #eq_assm >eq_assm cases cost_mapping #cost_mapping' * #ind_hyp #_ @present_add_hit |2: #neq_assm @present_add_miss try assumption cases cost_mapping #cost_mapping' * #ind_hyp #_ @(ind_hyp … lookup_opt_assm) [1: generalize in match (eqb_decidable (nat_of_bitvector … program_counter) (nat_of_bitvector … pc)); #hyp cases hyp [1: #relevant generalize in match (eqb_true_to_refl … relevant); #rewrite_assm plus_n_Sm in ⊢ (% → ?); cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)) [1: new_program_counter_assm' cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter))) [1: (* XXX: todo *) |2: #S_program_counter_assm >S_program_counter_assm #relevant plus_n_Sm in ⊢ (% → ?); eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % |2: #neq_assm cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm cases ind_hyp #_ #relevant cases (relevant k ?) [2: @(present_add_present … present_assm) assumption |1: #program_counter' #ind_hyp' %{program_counter'} #relevant cases (ind_hyp' relevant) #reachable_witness' #ind_hyp'' %{reachable_witness'} >ind_hyp'' @sym_eq @lookup_present_add_miss assumption ] ] |1: #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl) [1: #eq_assm >eq_assm cases cost_mapping #cost_mapping' * #ind_hyp #_ @present_add_hit |2: #neq_assm @present_add_miss try assumption cases cost_mapping #cost_mapping' * #ind_hyp #_ cases daemon (* XXX: !!! *) ] ] |6: ] qed. definition traverse_code: ∀code_memory: BitVectorTrie Byte 16. ∀cost_labels: BitVectorTrie costlabel 16. ∀program_size: nat. ∀reachable_program_counter_witness: ∀lbl: costlabel. ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → reachable_program_counter code_memory program_size program_counter. ∀good_program_witness: good_program code_memory program_size. Σcost_map: identifier_map CostTag nat. (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → ∃reachable_witness: reachable_program_counter code_memory program_size pc. pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ λcode_memory: BitVectorTrie Byte 16. λcost_labels: BitVectorTrie costlabel 16. λprogram_size: nat. λreachable_program_counter_witness: ∀lbl: costlabel. ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → reachable_program_counter code_memory program_size program_counter. λgood_program_witness: good_program code_memory program_size. traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness. definition compute_costs ≝ λprogram: list Byte. λcost_labels: BitVectorTrie costlabel 16. λreachable_program_witness. λgood_program_witness: good_program (load_code_memory program) (|program| + 1). let program_size ≝ |program| + 1 in let code_memory ≝ load_code_memory program in traverse_code code_memory cost_labels program_size reachable_program_witness ?. @good_program_witness qed.