include "ASM/ASMCosts.ma". include alias "arithmetics/nat.ma". include alias "basics/logic.ma". (* Also extracts an equality proof (useful when not using Russell). *) notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)" with precedence 10 for @{ match \$t return λx.∀\${ident E}: x = \$t. \$ty with [ mk_Prod \${ident x} \${ident y} ⇒ λ\${ident E}.\$s ] (refl ? \$t) }. (* lemma test: ∀c: nat × nat. Σx: nat. ∃y: nat. c = 〈x, y〉 ≝ λc: nat × nat. let 〈left, right〉 as T return Σx: ?. ? ≝ c in left. *) notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)" with precedence 10 for @{ match \$t return λx.∀\${ident E}: x = \$t. Σz: ?. ? with [ mk_Prod \${ident x} \${ident y} ⇒ λ\${ident E}.\$s ] (refl ? \$t) }. (* notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" with precedence 10 for @{ match \$t return λx.x = \$t → ? with [ mk_Prod \${fresh xy} \${ident z} ⇒ match \${fresh xy} return λx. ? = \$t → ? with [ mk_Prod \${ident x} \${ident y} ⇒ λ\${ident E}.\$s ] ] (refl ? \$t) }. *) notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" with precedence 10 for @{ match \$t return λx.∀\${fresh w}:x = \$t. Σq: ?. ? with [ mk_Prod \${fresh xy} \${ident z} ⇒ match \${fresh xy} return λx.∀\${ident E}:? = \$t. Σu: ?. ? with [ mk_Prod \${ident x} \${ident y} ⇒ λ\${ident E}.\$s ] ] (refl ? \$t) }. notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)" with precedence 10 for @{ match \$t return λx.∀\${fresh w}:x = \$t. Σq: ?. ? with [ mk_Prod \${fresh xy} \${ident z} ⇒ match \${fresh xy} return λx.∀\${ident E}:? = \$t. \$ty with [ mk_Prod \${ident x} \${ident y} ⇒ λ\${ident E}.\$s ] ] (refl ? \$t) }. lemma succ_nat_of_bitvector_aux_half_add_1: ∀n: nat. ∀bv: BitVector n. ∀buffer: nat. ∀power_proof: nat_of_bitvector … bv < 2^n - 1. S (nat_of_bitvector_aux n buffer bv) = nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)). #n #bv elim bv [1: #buffer normalize #absurd cases (lt_to_not_zero … absurd) |2: #n' #hd #tl #inductive_hypothesis #buffer cases daemon ] qed. lemma 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)). #n #bv elim bv [1: normalize #absurd cases (lt_to_not_zero … absurd) |2: #n' #hd #tl #inductive_hypothesis cases daemon ] 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: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size) (fixed_program_size_limit: fixed_program_size ≤ 2^16) 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 CostTag nat | S program_size' ⇒ λprogram_size_refl. deplet 〈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: ?. ? 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). [5: assumption |4: @(reachable_program_counter_witness lbl) @lookup_refl |3: cases program_size_invariant [1: #destruct_assm @⊥ -traverse_code_internal destruct |2: #program_size_invariant' % [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 #_ inversion program_size' [1: #program_size_refl_0 -traverse_code_internal destruct @⊥ cases neq_assm #assm @assm cut (Some … k = Some … lbl → k = lbl) (* XXX: lemma *) [1: #Some_assm destruct(Some_assm) % |2: #Some_assm @Some_assm lookup_refl >(?:pc=program_counter) [1: % |2: @refl_nat_of_bitvector_to_refl @le_to_le_to_eq try assumption change with (? ≤ ?) in H2; @le_S_S_to_le assumption ] ] |2: #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter))) [1: destruct @succ_nat_of_bitvector_half_add_1 @le_plus_to_minus_r @(transitive_le … fixed_program_size_limit) change with (S ? ≤ ?) >plus_n_Sm @monotonic_le_plus_r @le_S_S @le_S_S @le_O_n |2: #S_assm @(ind_hyp … lookup_opt_assm) [1: @(eqb_elim (nat_of_bitvector … program_counter) (nat_of_bitvector … pc)) [1: #eqb_refl_assm -ind_hyp -H1 -H2 lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm) #program_counter_refl_assm -eqb_refl_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} % [1: >eq_assm >lookup_refl % |2: %{(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'} % [1: cases ind_hyp' #assm #_ assumption |2: cases ind_hyp' #lookup_opt_assm * #reachable_witness' #ind_hyp'' %{reachable_witness'} >ind_hyp'' @sym_eq @lookup_present_add_miss assumption ] ] ] ] ] |1: % [1: #pc #k #absurd1 #absurd2 @⊥ lapply(lt_to_not_le … absurd2) * #absurd @absurd assumption |2: #k #k_pres @⊥ normalize in k_pres; /2/ ] |2: cases cost_mapping -traverse_code_internal #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 % [1: #pc #k #H1 #H2 cases program_size_invariant [1: #destruct_assm @⊥ destruct |2: -program_size_invariant #program_size_invariant inversion program_size' [1: #program_size_refl_0 destruct #lookup_opt_Some_assm >(?:pc = program_counter) in lookup_opt_Some_assm; [1: #absurd plus_n_Sm @monotonic_le_plus_r @le_S_S @le_S_S @le_O_n |2: #Sn_refl_assm >Sn_refl_assm plus_n_Sm @monotonic_le_plus_r @le_S_S @le_S_S @le_O_n |2: #S_assm change with (S (S n' + ?) ≤ ?) >plus_n_Sm @monotonic_le_plus_r >S_assm program_size_refl_Sn plus_n_Sm @monotonic_le_plus_r @le_S_S @le_S_S @le_O_n |2: #S_assm cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter)) [1: new_program_counter_assm' cases program_size_invariant [1: #destruct_assm destruct |2: #program_size_invariant (cost_labels_injective … lookup_opt_assm lookup_opt_assm') %{reachable_witness} assumption ] ] qed. definition compute_costs ≝ λprogram: list Byte. λcost_labels: BitVectorTrie costlabel 16. λcost_labels_injective: ∀pc, pc',l. lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → pc = pc'. λreachable_program_witness. λgood_program_witness: good_program (load_code_memory program) (|program|). λprogram_size_limit: |program| ≤ 2^16. let program_size ≝ |program| in let code_memory ≝ load_code_memory program in traverse_code code_memory cost_labels cost_labels_injective program_size program_size_limit reachable_program_witness good_program_witness.