Changeset 1621 for src/ASM/ASMCosts.ma
 Timestamp:
 Dec 15, 2011, 10:22:59 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1606 r1621 91 91 // 92 92 qed. 93 94 axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o: 95 ∀m, n, o: nat. 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. 102 103 lemma strengthened_invariant: 104 ∀code_memory: BitVectorTrie Byte 16. 105 ∀total_program_size: nat. 106 ∀new_program_counter: Word. 107 ∀program_counter: Word. 108 total_program_size ≤ code_memory_size → 109 let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in 110 Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) → 111 new_program_counter = \snd (\fst (fetch … code_memory program_counter)) → 112 nat_of_bitvector … program_counter ≤ total_program_size → 113 nat_of_bitvector … new_program_counter ≤ total_program_size. 114 #code_memory #total_program_size #new_program_counter #program_counter 115 #relation_total_program_code_memory_size #end_instruction_is_ok 116 #new_program_counter_from_fetch #program_counter_within_program 117 >new_program_counter_from_fetch 118 lapply (fetch code_memory program_counter) #assm 119 cases daemon 93 94 definition good_program_counter: BitVectorTrie Byte 16 → Word → nat → Prop ≝ 95 λcode_memory: BitVectorTrie Byte 16. 96 λprogram_counter: Word. 97 λprogram_size: nat. 98 ∃n: nat. 99 let tail_program_counter ≝ fetch_program_counter_n n code_memory (zero 16) in 100 program_counter = fetch_program_counter_n (S n) code_memory (zero 16) ∧ 101 nat_of_bitvector 16 program_counter ≤ program_size ∧ 102 nat_of_bitvector 16 tail_program_counter ≤ nat_of_bitvector 16 program_counter. 103 104 definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝ 105 λcode_memory: BitVectorTrie Byte 16. 106 λprogram_counter: Word. 107 λtotal_program_size: nat. 108 let 〈instruction, program_counter, ticks〉 ≝ fetch code_memory program_counter in 109 match instruction with 110 [ RealInstruction instr ⇒ 111 match instr with 112 [ RET ⇒ True 113  JC relative ⇒ True (* XXX: see below *) 114  JNC relative ⇒ True (* XXX: see below *) 115  JB bit_addr relative ⇒ True 116  JNB bit_addr relative ⇒ True 117  JBC bit_addr relative ⇒ True 118  JZ relative ⇒ True 119  JNZ relative ⇒ True 120  CJNE src_trgt relative ⇒ True 121  DJNZ src_trgt relative ⇒ True 122  _ ⇒ 123 good_program_counter code_memory program_counter total_program_size 124 ] 125  LCALL addr ⇒ 126 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with 127 [ ADDR16 addr ⇒ λaddr16: True. 128 good_program_counter code_memory addr total_program_size ∧ 129 good_program_counter code_memory program_counter total_program_size 130  _ ⇒ λother: False. ⊥ 131 ] (subaddressing_modein … addr) 132  ACALL addr ⇒ 133 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with 134 [ ADDR11 addr ⇒ λaddr11: True. 135 let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in 136 let 〈thr, eig〉 ≝ split … 3 8 addr in 137 let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in 138 let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in 139 good_program_counter code_memory new_program_counter total_program_size ∧ 140 good_program_counter code_memory program_counter total_program_size 141  _ ⇒ λother: False. ⊥ 142 ] (subaddressing_modein … addr) 143  AJMP addr ⇒ 144 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with 145 [ ADDR11 addr ⇒ λaddr11: True. 146 let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in 147 let 〈nu, nl〉 ≝ split … 4 4 pc_bu in 148 let bit ≝ get_index' … O ? nl in 149 let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in 150 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 151 let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in 152 (good_program_counter code_memory new_program_counter total_program_size) ∧ 153 (good_program_counter code_memory program_counter total_program_size) 154  _ ⇒ λother: False. ⊥ 155 ] (subaddressing_modein … addr) 156  LJMP addr ⇒ 157 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with 158 [ ADDR16 addr ⇒ λaddr16: True. 159 good_program_counter code_memory addr total_program_size ∧ 160 good_program_counter code_memory program_counter total_program_size 161  _ ⇒ λother: False. ⊥ 162 ] (subaddressing_modein … addr) 163  SJMP addr ⇒ 164 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with 165 [ RELATIVE addr ⇒ λrelative: True. 166 let 〈carry, new_program_counter〉 ≝ half_add … program_counter (sign_extension addr) in 167 good_program_counter code_memory new_program_counter total_program_size ∧ 168 good_program_counter code_memory program_counter total_program_size 169  _ ⇒ λother: False. ⊥ 170 ] (subaddressing_modein … addr) 171  JMP addr ⇒ True (* XXX: should recurse here, but dptr in JMP ... *) 172  MOVC src trgt ⇒ 173 good_program_counter code_memory program_counter total_program_size 174 ]. 175 cases other 120 176 qed. 121 177 178 axiom dubious: 179 ∀m, n, o, p: nat. 180 1 ≤ p → n ≤ m → m  n ≤ S o → m  (n + p) ≤ o. 181 182 lemma subaddressing_mod_elim: 183 ∀T:Type[2]. 184 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19,addr,p. 185 ∀Q: addressing_mode → T → Prop. 186 (∀w. Q (ADDR11 w) (P1 w)) → 187 Q addr (match addr 188 in addressing_mode 189 return λx:addressing_mode.(is_in 1 [[addr11]] x→T) 190 with 191 [ADDR11 (x:Word11) ⇒ λH:True. P1 x 192 ADDR16 _ ⇒ λH:False. P2 H 193 DIRECT _ ⇒ λH:False. P3 H 194 INDIRECT _ ⇒ λH:False. P4 H 195 EXT_INDIRECT _ ⇒ λH:False. P5 H 196 ACC_A ⇒ λH:False. P6 H 197 REGISTER _ ⇒ λH:False. P7 H 198 ACC_B ⇒ λH:False. P8 H 199 DPTR ⇒ λH:False. P9 H 200 DATA _ ⇒ λH:False. P10 H 201 DATA16 _ ⇒ λH:False. P11 H 202 ACC_DPTR ⇒ λH:False. P12 H 203 ACC_PC ⇒ λH:False. P13 H 204 EXT_INDIRECT_DPTR ⇒ λH:False. P14 H 205 INDIRECT_DPTR ⇒ λH:False. P15 H 206 CARRY ⇒ λH:False. P16 H 207 BIT_ADDR _ ⇒ λH:False. P17 H 208 N_BIT_ADDR _ ⇒ λH:False. P18 H 209 RELATIVE _ ⇒ λH:False. P19 H 210 ] p). 211 #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13 212 #P14 #P15 #P16 #P17 #P18 #P19 213 * try #x1 try #x2 try #x3 try #x4 214 try (@⊥ assumption) normalize @x4 215 qed. 216 217 let rec block_cost 218 (code_memory: BitVectorTrie Byte 16) (program_counter: Word) 219 (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16) 220 (good_program_witness: good_program code_memory program_counter total_program_size) 221 on program_size: total_program_size  nat_of_bitvector … program_counter ≤ program_size → nat ≝ 222 match program_size return λprogram_size: nat. total_program_size  nat_of_bitvector … program_counter ≤ program_size → nat with 223 [ O ⇒ λbase_case. 0 224  S program_size' ⇒ λrecursive_case. 225 let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in 226 match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with 227 [ None ⇒ 228 match instruction return λx. x = instruction → ? with 229 [ RealInstruction instruction ⇒ λreal_instruction. 230 match instruction return λx. x = instruction → ? with 231 [ RET ⇒ λret. ticks 232  JC relative ⇒ λjc. ticks 233  JNC relative ⇒ λjnc. ticks 234  JB bit_addr relative ⇒ λjb. ticks 235  JNB bit_addr relative ⇒ λjnb. ticks 236  JBC bit_addr relative ⇒ λjbc. ticks 237  JZ relative ⇒ λjz. ticks 238  JNZ relative ⇒ λjnz. ticks 239  CJNE src_trgt relative ⇒ λcjne. ticks 240  DJNZ src_trgt relative ⇒ λdjnz. ticks 241  _ ⇒ λalt. 242 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 243 ] (refl … instruction) 244  ACALL addr ⇒ λacall. 245 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 246  AJMP addr ⇒ λajmp. ticks 247  LCALL addr ⇒ λlcall. 248 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 249  LJMP addr ⇒ λljmp. ticks 250  SJMP addr ⇒ λsjmp. ticks 251  JMP addr ⇒ λjmp. (* XXX: actually a call due to use with fptrs *) 252 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 253  MOVC src trgt ⇒ λmovc. 254 ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ? 255 ] (refl … instruction) 256  Some _ ⇒ ticks 257 ] 258 ]. 259 [1: block_cost eta62747 program_size 260 generalize in match good_program_witness; 261 whd in match good_program; normalize nodelta 262 cases FETCH normalize nodelta 263 cases acall normalize nodelta 264 @(subaddressing_mod_elim Prop ??????????????????? addr 265 (subaddressing_modein ? [[addr11]] addr) 266 (λ_.λP. P → total_program_sizenat_of_bitvector 16 program_counter'≤program_size')) 267 268 cases addr #subaddressing_mode cases subaddressing_mode 269 try (#assm #absurd normalize in absurd; cases absurd) 270 try (#absurd normalize in absurd; cases absurd) 271 normalize nodelta 272 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 273 cases (split … 3 8 assm) #thr #eig normalize nodelta 274 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta 275 #assm cases assm #ignore 276 whd in match good_program_counter; normalize nodelta * #n * * 277 #program_counter_eq' #program_counter_lt_total_program_size 278 #fetch_n_leq_program_counter' 279 lapply(dubious total_program_size (nat_of_bitvector … program_counter') 280 program_size' ? ? ? ?) 281 [2: assumption ] 282 [2: 283 (* generalize in match good_program_witness; *) 284 whd in match good_program; normalize nodelta 285 cases FETCH normalize nodelta 286 cases (fetch code_memory program_counter') #instruction_program_counter' #ticks' normalize nodelta 287 cases instruction_program_counter' #instruction' #program_counter'' normalize nodelta 288 cases acall normalize nodelta 289 cases addr #subaddressing_mode cases subaddressing_mode 290 try (#assm #absurd normalize in absurd; cases absurd) 291 try (#absurd normalize in absurd; cases absurd) 292 normalize nodelta 293 cases instruction' 294 try (#assm normalize nodelta) 295 [7: 296 #irrelevant 297 whd in match good_program_counter; normalize nodelta 298 299 300 301 302 303 304 305 306 122 307 (* XXX: use memoisation here in the future *) 123 308 let rec block_cost … … 126 311 (size_invariant: total_program_size ≤ code_memory_size) 127 312 (pc_invariant: nat_of_bitvector … program_counter < total_program_size) 128 (final_instr_invariant: 129 let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in 130 Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return)) 131 on program_size: total_program_size  nat_of_bitvector … program_counter ≤ program_size → nat ≝ 313 on program_size: total_program_size  nat_of_bitvector … program_counter ≤ program_size → nat ≝ 132 314 match program_size return λprogram_size: nat. total_program_size  nat_of_bitvector … program_counter ≤ program_size → nat with 133 315 [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *) 134 316  S program_size ⇒ λrecursive_case. 135 let ticks ≝ \snd (fetch … code_memory program_counter) in 136 let instr ≝ \fst (\fst (fetch … code_memory program_counter)) in 137 let newpc ≝ \snd (\fst (fetch … code_memory program_counter)) in 138 match lookup_opt … newpc cost_labels return λx: option costlabel. nat with 139 [ None ⇒ 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 ] 146  Some _ ⇒ ticks 147 ] 317 let 〈instr, newpc, ticks〉 ≝ fetch … code_memory program_counter in 318 match lookup_opt … newpc cost_labels return λx: option costlabel. nat with 319 [ None ⇒ 320 let classify ≝ ASM_classify0 instr in 321 match classify return λx. classify = x → ? with 322 [ cl_jump ⇒ λclassify_refl. ticks 323  cl_call ⇒ λclassify_refl. (* ite here *) 324 ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 325  cl_return ⇒ λclassify_refl. ticks 326  cl_other ⇒ λclassify_refl. (* ite here *) 327 ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) 328 ] (refl … classify) 329  Some _ ⇒ ticks 330 ] 148 331 ]. 149 [1,3:150 lapply(sig2 ? ? (fetch code_memory program_counter))151 change with (152 nat_of_bitvector … newpc153 ) in ⊢ (??% → ?);154 155 156 157 [1:158 cases(lt_to_not_zero … absurd)159 2,4:160 cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc)161 [1,3:162 normalize nodelta in match newpc;163 lapply(sig2 ? ? (fetch code_memory program_counter))164 [*: #assm assumption ]165 2,4:166 #first_lt_assm167 ]168 169 170 3,5:171 lapply(sig2172 normalize in recursive_case;173 change with (174 S (total_program_size  nat_of_bitvector … newpc) ≤ program_size)175 lapply (le_S_S_to_le … recursive_case)176 change with (177 initial_program_size  (nat_of_bitvector … pc) ≤ program_size178 ) in ⊢ (% → ?);179 #second_le_assm180 @(transitive_le181 (S (initial_program_sizenat_of_bitvector 16 newpc))182 (initial_program_sizenat_of_bitvector_aux 16 O pc)183 program_size ? second_le_assm)184 change with (185 initial_program_size  nat_of_bitvector … pc186 ) in ⊢ (??%);187 lapply (minus_Sn_m (nat_of_bitvector … newpc) initial_program_size)188 #assm <assm in ⊢ (?%?);189 [1,3:190 @minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o191 @monotonic_le_minus_r192 assumption193 2,4:194 @(strengthened_invariant mem initial_program_size newpc pc size_invariant final_instr_invariant)195 [1,3:196 %197 2,4:198 assumption199 ]200 ]201 ]202 3,5:203 ]204 qed.205 332 206 333 let rec traverse_code_internal
Note: See TracChangeset
for help on using the changeset viewer.