Changeset 1544 for src/ASM/CostsProof.ma
 Timestamp:
 Nov 23, 2011, 6:01:15 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1534 r1544 2 2 include "ASM/WellLabeled.ma". 3 3 include "ASM/Status.ma". 4 5 definition is_jump_p ≝ 6 λs. 7 match s with 8 [ AJMP _ ⇒ True 9  LJMP _ ⇒ True 10  SJMP _ ⇒ True 11  JMP _ ⇒ False 12  RealInstruction ri ⇒ 13 match ri with 14 [ JZ _ ⇒ True 15  JNZ _ ⇒ True 16  JC _ ⇒ True 17  JNC _ ⇒ True 18  JB _ _ ⇒ True 19  JNB _ _ ⇒ True 20  JBC _ _ ⇒ True 21  CJNE _ _ ⇒ True 22  DJNZ _ _ ⇒ True 23  _ ⇒ False 24 ] 25  _ ⇒ False 26 ]. 4 include "common/StructuredTraces.ma". 5 6 definition current_instruction ≝ 7 λs: Status. 8 let pc ≝ program_counter … s in 9 \fst (\fst (fetch … (code_memory … s) pc)). 10 11 definition ASM_classify: Status → status_class ≝ 12 λs. 13 match current_instruction s with 14 [ RealInstruction pre ⇒ 15 match pre with 16 [ RET ⇒ cl_return 17  JZ _ ⇒ cl_jump 18  JNZ _ ⇒ cl_jump 19  JC _ ⇒ cl_jump 20  JNC _ ⇒ cl_jump 21  JB _ _ ⇒ cl_jump 22  JNB _ _ ⇒ cl_jump 23  JBC _ _ ⇒ cl_jump 24  CJNE _ _ ⇒ cl_jump 25  DJNZ _ _ ⇒ cl_jump 26  _ ⇒ cl_other 27 ] 28  ACALL _ ⇒ cl_call 29  LCALL _ ⇒ cl_call 30  JMP _ ⇒ cl_call 31  AJMP _ ⇒ cl_jump 32  LJMP _ ⇒ cl_jump 33  SJMP _ ⇒ cl_jump 34  _ ⇒ cl_other 35 ]. 36 37 definition current_instruction_is_labelled ≝ 38 λcost_labels: BitVectorTrie Byte 16. 39 λs: Status. 40 let pc ≝ program_counter … s in 41 match lookup_opt … pc cost_labels with 42 [ None ⇒ False 43  _ ⇒ True 44 ]. 45 46 definition current_instruction_cost ≝ 47 λs: Status. \snd (fetch (code_memory … s) (program_counter … s)). 48 49 definition next_instruction_properly_relates_program_counters ≝ 50 λbefore: Status. 51 λafter : Status. 52 let size ≝ current_instruction_cost before in 53 let pc_before ≝ program_counter … before in 54 let pc_after ≝ program_counter … after in 55 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in 56 sum = pc_after. 57 58 definition ASM_abstract_status: BitVectorTrie Byte 16 → abstract_status ≝ 59 λcost_labels. 60 mk_abstract_status 61 Status 62 (λs,s'. eject … (execute_1 s) = s') 63 (λs,class. ASM_classify s = class) 64 (current_instruction_is_labelled cost_labels) 65 next_instruction_properly_relates_program_counters. 66 67 (* 68 definition next_instruction_is_labelled ≝ 69 λcost_labels: BitVectorTrie Byte 16. 70 λs: Status. 71 let pc ≝ program_counter … (execute_1 s) in 72 match lookup_opt … pc cost_labels with 73 [ None ⇒ False 74  _ ⇒ True 75 ]. 76 77 definition current_instruction_cost ≝ 78 λs: Status. \snd (fetch (code_memory … s) (program_counter … s)). 27 79 28 80 definition is_call_p ≝ … … 52 104  _ ⇒ True 53 105 ]. 54 55 definition current_instruction_cost ≝56 λs: Status.57 \snd (fetch (code_memory … s) (program_counter … s)).58 106 59 107 definition next_instruction_properly_relates_program_counters ≝ … … 142 190 ¬ (current_instruction_is_labelled cost_labels status_init) → 143 191 trace_label_label_pre cost_labels end_flag status_pre status_end. 144 145 (* XXX: to do later 192 *) 193 194 (* XXX: not us 146 195 definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ …. 147 196 … … 157 206 158 207 let rec compute_max_trace_label_label_cost 159 (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret) 208 (cost_labels: BitVectorTrie Byte 16) 209 (trace_ends_flag: trace_ends_with_ret) 160 210 (start_status: Status) (final_status: Status) 161 (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)162 on the_trace: nat ≝211 (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag 212 start_status final_status) on the_trace: nat ≝ 163 213 match the_trace with 164 214 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ 165 compute_max_trace_label_label_pre_cost … given_trace 166 ] 167 and compute_max_trace_label_label_pre_cost 168 (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret) 169 (start_status: Status) (final_status: Status) 170 (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status) 171 on the_trace: nat ≝ 215 compute_max_trace_any_label_cost … given_trace 216 ] 217 and compute_max_trace_any_label_cost 218 (cost_labels: BitVectorTrie Byte 16) 219 (trace_ends_flag: trace_ends_with_ret) 220 (start_status: Status) (final_status: Status) 221 (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status) 222 on the_trace: nat ≝ 172 223 match the_trace with 173 [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒ 174 current_instruction_cost the_status 175  tllp_base_return the_status is_return ⇒ current_instruction_cost the_status 176  tllp_base_jump the_status is_jump is_cost ⇒ 177 current_instruction_cost the_status 178  tllp_step_call end_flag pre_fun_call after_fun_call final is_call 179 next_intruction_coherence call_trace final_trace ⇒ 224 [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status 225  tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status 226  tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final 227 _ _ _ call_trace final_trace ⇒ 180 228 let current_instruction_cost ≝ current_instruction_cost pre_fun_call in 181 let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels… call_trace in182 let final_trace_cost ≝ compute_max_trace_ label_label_pre_cost cost_labels end_flag after_fun_call finalfinal_trace in229 let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in 230 let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in 183 231 call_trace_cost + current_instruction_cost + final_trace_cost 184  tllp_step_default end_flag status_pre status_end tail_trace is_not_call 185 is_not_jump is_not_ret is_not_labelled ⇒ 232  tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 186 233 let current_instruction_cost ≝ current_instruction_cost status_pre in 187 let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in 234 let tail_trace_cost ≝ 235 compute_max_trace_any_label_cost cost_labels end_flag 236 status_init status_end tail_trace 237 in 188 238 current_instruction_cost + tail_trace_cost 189 239 ] 190 240 and compute_max_trace_label_return_cost 191 (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status) 192 (the_trace: trace_label_return cost_labels start_status final_status) 241 (cost_labels: BitVectorTrie Byte 16) 242 (start_status: Status) (final_status: Status) 243 (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status) 193 244 on the_trace: nat ≝ 194 245 match the_trace with … … 200 251 ]. 201 252 253 (* To be moved *) 202 254 lemma pred_minus_1: 203 255 ∀m, n: nat. … … 225 277 ∀m: nat. 226 278 S m = m + 1. 227 #m 228 elim m 229 [ % 230  #m' #ind_hyp 231 normalize 232 <ind_hyp 233 % 234 ] 235 qed. 279 // 280 qed. 281 282 include alias "arithmetics/nat.ma". 236 283 237 284 lemma minus_m_n_minus_minus_plus_1: … … 239 286 ∀proof: n < m. 240 287 m  n = (m  n  1) + 1. 241 #m 242 elim m 243 [ #n #proof 244 cases(lt_to_not_zero … proof) 245  #m' #ind_hyp #n 246 normalize 247 cases n 248 [ normalize // 249  #n' #proof normalize 250 <ind_hyp 251 [ % 252  @le_S_S_to_le 253 assumption 254 ] 255 ] 256 ] 257 qed. 258 259 include alias "arithmetics/nat.ma". 288 /3 by lt_plus_to_minus_r, plus_minus/ 289 qed. 260 290 261 291 lemma plus_minus_rearrangement_1: 262 292 ∀m, n, o: nat. 263 ∀proof_n_m: n <m.264 ∀proof_m_o: m <o.293 ∀proof_n_m: n ≤ m. 294 ∀proof_m_o: m ≤ o. 265 295 (m  n) + (o  m) = o  n. 266 #m #n #o 267 elim m 268 [1: #proof_n_m 269 cases(lt_to_not_zero … proof_n_m) 270 2: #m' #ind_hyp 271 #proof_n_m' #proof_m_o 272 >minus_Sn_m 273 [2: normalize in proof_n_m'; 274 @le_S_S_to_le 275 assumption 276 1: >eq_minus_S_pred 277 >pred_minus_1 278 [1: >(succ_m_plus_one (m'  n)) 279 >(associative_plus (m'  n) 1 (o  m'  1)) 280 <commutative_plus in match (1 + (o  m'  1)); 281 <(minus_m_n_minus_minus_plus_1 o m') in match (o  m'  1 + 1); 282 [1: >ind_hyp 283 [1: % 284 2: normalize 285 normalize in proof_m_o; 286 @le_S_S_to_le 287 @(le_S ? ? proof_m_o) 288 3: cases daemon (* XXX: problem here *) 289 ] 290 2: normalize in proof_m_o; 291 normalize 292 @le_S_S_to_le 293 @(le_S (S (S m')) o proof_m_o) 294 ] 295 2: normalize 296 normalize in proof_m_o; 297 @le_S_S_to_le 298 @(le_S (S (S m')) o proof_m_o) 299 ] 300 ] 301 ] 302 qed. 303 304 axiom plus_minus_rearrangement_2: 305 ∀m, n, o: nat. 296 #m #n #o #H1 #H2 297 lapply (minus_to_plus … H1 (refl …)) #K1 >K1 298 lapply (minus_to_plus … H2 (refl …)) #K2 >K2 299 /2 by plus_minus/ 300 qed. 301 302 lemma plus_minus_rearrangement_2: 303 ∀m, n, o: nat. n ≤ m → o ≤ n → 306 304 (m  n) + (n  o) = m  o. 307 308 example set_program_counter_ignores_clock: 309 ∀s: Status. 310 ∀pc: Word. 311 clock … (set_program_counter … s pc) = clock … s. 312 #s #pc % 313 qed. 314 315 example set_low_internal_ram_ignores_clock: 316 ∀s: Status. 317 ∀ram: BitVectorTrie Byte 7. 318 clock … (set_low_internal_ram … s ram) = clock … s. 319 #s #ram % 320 qed. 321 322 example set_8051_sfr_ignores_clock: 323 ∀s: Status. 324 ∀sfr: SFR8051. 325 ∀v: Byte. 326 clock … (set_8051_sfr ? s sfr v) = clock … s. 327 #s #sfr #v % 328 qed. 329 330 example clock_set_clock: 331 ∀s: Status. 332 ∀v. 333 clock … (set_clock … s v) = v. 334 #s #v % 335 qed. 336 337 example write_at_stack_pointer_ignores_clock: 338 ∀s: Status. 339 ∀sp: Byte. 340 clock … (write_at_stack_pointer … s sp) = clock … s. 341 #s #sp 342 change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp); with ( 343 let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in 344 ?); 345 normalize nodelta; 346 cases(split bool 4 4 (get_8051_sfr (BitVectorTrie Byte 16) s SFR_SP)) 347 #nu #nl normalize nodelta; 348 cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3))) 349 [ normalize nodelta; % 350  normalize nodelta; % 351 ] 352 qed. 353 354 example status_execution_progresses_processor_clock: 355 ∀s: Status. 356 clock … s ≤ clock … (execute 1 s). 357 #s 358 change in match (execute 1 s) with (execute_1 s); 359 change in match (execute_1 s) with ( 360 let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s) 361 (program_counter (BitVectorTrie Byte 16) s) 362 in 363 execute_1_0 s instr_pc_ticks); 364 normalize nodelta; 365 whd in match (execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s) 366 (program_counter (BitVectorTrie Byte 16) s))); 367 normalize nodelta; 368 cases (fetch (code_memory (BitVectorTrie Byte 16) s) 369 (program_counter (BitVectorTrie Byte 16) s)) 370 #instruction_pc #ticks 371 normalize nodelta; 372 cases instruction_pc 373 #instruction #pc 374 cases instruction 375 [1: 376 #addr11 cases addr11 #addressing_mode 377 normalize nodelta; cases addressing_mode 378 normalize nodelta; 379 [1,2,3,4,8,9,15,16,17,19: 380 #assm whd in ⊢ (% → ?) 381 #absurd cases(absurd) 382 5,6,7,10,11,12,13,14: 383 whd in ⊢ (% → ?) 384 #absurd cases(absurd) 385 18: 386 #addr11 #irrelevant 387 normalize nodelta; 388 >set_program_counter_ignores_clock 389 normalize nodelta; 390 >set_program_counter_ignores_clock 391 >write_at_stack_pointer_ignores_clock 392 >set_8051_sfr_ignores_clock 393 >write_at_stack_pointer_ignores_clock 394 >set_8051_sfr_ignores_clock 395 >clock_set_clock // 396 ] 397 2: 398 #addr16 cases addr16 #addressing_mode 399 normalize nodelta; cases addressing_mode 400 normalize nodelta; 401 [1,2,3,4,8,9,15,16,17,18: 402 #assm whd in ⊢ (% → ?) 403 #absurd cases(absurd) 404 5,6,7,10,11,12,13,14: 405 whd in ⊢ (% → ?) 406 #absurd cases(absurd) 407 19: 408 #addr16 #irrelevant 409 normalize nodelta; 410 >set_program_counter_ignores_clock 411 >write_at_stack_pointer_ignores_clock 412 >set_8051_sfr_ignores_clock 413 >write_at_stack_pointer_ignores_clock 414 >set_8051_sfr_ignores_clock 415 >clock_set_clock 416 >set_program_counter_ignores_clock // 417 ] 418 3: #addr11 cases addr11 #addressing_mode 419 normalize nodelta; cases addressing_mode 420 normalize nodelta; 421 [1,2,3,4,8,9,15,16,17,19: 422 #assm whd in ⊢ (% → ?) 423 #absurd cases(absurd) 424 5,6,7,10,11,12,13,14: 425 whd in ⊢ (% → ?) 426 #absurd cases(absurd) 427 18: 428 #word11 #irrelevant 429 normalize nodelta; 430 >set_program_counter_ignores_clock 431 >clock_set_clock 432 >set_program_counter_ignores_clock // 433 ] 434 4: #addr16 cases addr16 #addressing_mode 435 normalize nodelta; cases addressing_mode 436 normalize nodelta; 437 [1,2,3,4,8,9,15,16,17,18: 438 #assm whd in ⊢ (% → ?) 439 #absurd cases(absurd) 440 5,6,7,10,11,12,13,14: 441 whd in ⊢ (% → ?) 442 #absurd cases(absurd) 443 19: 444 #word #irrelevant 445 normalize nodelta; 446 >set_program_counter_ignores_clock 447 >clock_set_clock 448 >set_program_counter_ignores_clock // 449 ] 450 5: #relative cases relative #addressing_mode 451 normalize nodelta; cases addressing_mode 452 normalize nodelta; 453 [1,2,3,4,8,9,15,16,18,19: 454 #assm whd in ⊢ (% → ?) 455 #absurd cases(absurd) 456 5,6,7,10,11,12,13,14: 457 whd in ⊢ (% → ?) 458 #absurd cases(absurd) 459 17: 460 #byte #irrelevant 461 normalize nodelta; 462 >set_program_counter_ignores_clock 463 >set_program_counter_ignores_clock 464 >clock_set_clock // 465 ] 466 6: #indirect_dptr cases indirect_dptr #addressing_mode 467 normalize nodelta; cases addressing_mode 468 normalize nodelta; 469 [1,2,3,4,8,9,15,16,17,18,19: 470 #assm whd in ⊢ (% → ?) 471 #absurd cases(absurd) 472 5,6,7,10,11,12,14: 473 whd in ⊢ (% → ?) 474 #absurd cases(absurd) 475 13: 476 #irrelevant 477 normalize nodelta; 478 >set_program_counter_ignores_clock 479 >set_program_counter_ignores_clock 480 >clock_set_clock // 481 ] 482 8: cases daemon (* XXX: my god *) 483 7: #acc_a cases acc_a #addressing_mode 484 normalize nodelta; cases addressing_mode 485 normalize nodelta; 486 [1,2,3,4,8,9,15,16,17,18,19: 487 #assm whd in ⊢ (% → ?) 488 #absurd cases(absurd) 489 6,7,10,11,12,13,14: 490 whd in ⊢ (% → ?) 491 #absurd cases(absurd) 492 5: 493 #irrelevant #acc_dptr_acc_pc 494 normalize nodelta; 495 cases daemon (* XXX: my god *) 496 ] 497 ] 305 /2 by plus_minus_rearrangement_1/ 498 306 qed. 499 307 … … 502 310 current_instruction_cost s = clock … (execute 1 s)  clock … s. 503 311 #s 504 change in match (execute 1 s) with (execute_1 s);505 change in match (execute_1 s)with (312 change with (execute_1 s) in match (eject … (execute 1 s)); 313 change with ( 506 314 let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s) 507 315 (program_counter (BitVectorTrie Byte 16) s) 508 316 in 509 execute_1_0 s instr_pc_ticks);510 change in ⊢ (??%?)with (511 \snd (fetch (code_memory … s) (program_counter … s))) ;317 eject … (execute_1_0 s instr_pc_ticks)) in match (eject … (execute_1 s)); 318 change with ( 319 \snd (fetch (code_memory … s) (program_counter … s))) in ⊢ (??%?); 512 320 normalize nodelta; 513 321 whd in match (
Note: See TracChangeset
for help on using the changeset viewer.