Changeset 1597 for src/ASM/ASMCosts.ma
 Timestamp:
 Dec 12, 2011, 9:51:21 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1591 r1597 90 90 (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b. 91 91 // 92 qed. 92 qed. 93 93 94 94 axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o: 95 95 ∀m, n, o: nat. 96 96 m  n ≤ m  S o → S m  n ≤ m  o. 97 (* XXX: ^^^ false without some preconditions *) 98 99 axiom m_leq_n_to_m_eq_n_or_m_lt_n: 100 ∀n, m: nat. 101 m ≤ n → m = n ∨ m < n. 97 102 98 103 lemma strengthened_invariant: … … 112 117 >new_program_counter_from_fetch 113 118 lapply (sig2 ? ? (fetch code_memory program_counter)) #assm 119 cases daemon 120 qed. 114 121 115 116 122 (* XXX: use memoisation here in the future *) 117 123 let rec block_cost … … 123 129 let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in 124 130 Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return)) 125 on program_size: total_program_size  nat_of_bitvector … program_counter <program_size → nat ≝126 match program_size return λprogram_size: nat. total_program_size  nat_of_bitvector … program_counter <program_size → nat with127 [ O ⇒ λ absurd. ⊥131 on program_size: total_program_size  nat_of_bitvector … program_counter ≤ program_size → nat ≝ 132 match program_size return λprogram_size: nat. total_program_size  nat_of_bitvector … program_counter ≤ program_size → nat with 133 [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *) 128 134  S program_size ⇒ λrecursive_case. 129 135 let ticks ≝ \snd (fetch … code_memory program_counter) in … … 132 138 match lookup_opt … newpc cost_labels return λx: option costlabel. nat with 133 139 [ None ⇒ 134 let classify ≝ ASM_classify0 instr in 135 match classify return λx. ∀classify_refl: x = classify. nat with 136 [ cl_jump ⇒ λclassify_refl. ticks 137  cl_call ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 138  cl_return ⇒ λclassify_refl. ticks 139  cl_other ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 140 ] (refl … classify) 140 match ASM_classify0 instr with 141 [ cl_jump ⇒ ticks 142  cl_call ⇒ ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 143  cl_return ⇒ ticks 144  cl_other ⇒ ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 145 ] 141 146  Some _ ⇒ ticks 142 147 ] 143 148 ]. 149 [1,3: 150 lapply(sig2 ? ? (fetch code_memory program_counter)) 151 change with ( 152 nat_of_bitvector … newpc 153 ) in ⊢ (??% → ?); 154 155 156 144 157 [1: 145 158 cases(lt_to_not_zero … absurd) … … 147 160 cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc) 148 161 [1,3: 149 @fetch_pc_lt_new_pc (* XXX: now @sig2 from fetch's russell type *) 150 lapply(transitive_lt 151 (nat_of_bitvector 16 pc) 152 initial_program_size 153 (size Byte 16 mem) ? ?) 154 [1,2,4,5: 155 assumption 156 3,6: 157 #assm assumption 158 ] 162 normalize nodelta in match newpc; 163 lapply(sig2 ? ? (fetch code_memory program_counter)) 164 [*: #assm assumption ] 159 165 2,4: 160 change with ( 161 S (nat_of_bitvector … 16 pc) ≤ nat_of_bitvector … newpc 162 ) in ⊢ (% → ?); 163 #first_le_assm 166 #first_lt_assm 167 ] 168 169 170 3,5: 171 lapply(sig2 164 172 normalize in recursive_case; 165 173 change with ( 166 S ( initial_program_size  nat_of_bitvector … newpc) ≤ program_size)174 S (total_program_size  nat_of_bitvector … newpc) ≤ program_size) 167 175 lapply (le_S_S_to_le … recursive_case) 168 176 change with (
Note: See TracChangeset
for help on using the changeset viewer.