Changeset 1511
 Timestamp:
 Nov 16, 2011, 5:35:24 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1509 r1511 55 55 definition current_instruction_cost ≝ 56 56 λs: Status. 57 let 〈ignore, ignore, cost〉 ≝ fetch (code_memory … s) (program_counter … s) in 58 cost. 57 \snd (fetch (code_memory … s) (program_counter … s)). 59 58 60 59 definition next_instruction_properly_relates_program_counters ≝ … … 64 63 let pc_before ≝ program_counter … before in 65 64 let pc_after ≝ program_counter … after in 66 let 〈carry, sum〉 ≝ half_add … pc_before (bitvector_of_nat … size) in65 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in 67 66 sum = pc_after. 68 67 … … 70 69 λs: Status. 71 70 let pc ≝ program_counter … s in 72 let 〈instruction, new_pc, cost〉 ≝ fetch … (code_memory … s) pc in 73 instruction. 71 \fst (\fst (fetch … (code_memory … s) pc)). 74 72 75 73 definition current_instruction_is_labelled ≝ … … 302 300 qed. 303 301 304 lemma status_execution_progresses_processor_clock: 302 example set_program_counter_ignores_clock: 303 ∀s: Status. 304 ∀pc: Word. 305 clock … (set_program_counter … s pc) = clock … s. 306 #s #pc % 307 qed. 308 309 example set_low_internal_ram_ignores_clock: 310 ∀s: Status. 311 ∀ram: BitVectorTrie Byte 7. 312 clock … (set_low_internal_ram … s ram) = clock … s. 313 #s #ram % 314 qed. 315 316 example set_8051_sfr_ignores_clock: 317 ∀s: Status. 318 ∀sfr: SFR8051. 319 ∀v: Byte. 320 clock … (set_8051_sfr ? s sfr v) = clock … s. 321 #s #sfr #v % 322 qed. 323 324 example clock_set_clock: 325 ∀s: Status. 326 ∀v. 327 clock … (set_clock … s v) = v. 328 #s #v % 329 qed. 330 331 example write_at_stack_pointer_ignores_clock: 332 ∀s: Status. 333 ∀sp: Byte. 334 clock … (write_at_stack_pointer … s sp) = clock … s. 335 #s #sp 336 change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp) with ( 337 let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in 338 ?); 339 normalize nodelta; 340 cases(split bool 4 4 (get_8051_sfr (BitVectorTrie Byte 16) s SFR_SP)) 341 #nu #nl normalize nodelta; 342 cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3))) 343 [ normalize nodelta; % 344  normalize nodelta; % 345 ] 346 qed. 347 348 example status_execution_progresses_processor_clock: 305 349 ∀s: Status. 306 350 clock … s ≤ clock … (execute 1 s). 307 #status 308 cases status 309 #ignore1 #ignore2 #ignore3 #ignore4 #ignore5 #ignore6 #ignore7 #ignore8 310 #ignore9 #clock 311 351 #s 352 change in match (execute 1 s) with (execute_1 s); 353 change in match (execute_1 s) with ( 354 let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s) 355 (program_counter (BitVectorTrie Byte 16) s) 356 in 357 execute_1_0 s instr_pc_ticks); 358 normalize nodelta; 359 whd in match (execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s) 360 (program_counter (BitVectorTrie Byte 16) s))); 361 normalize nodelta; 362 cases (fetch (code_memory (BitVectorTrie Byte 16) s) 363 (program_counter (BitVectorTrie Byte 16) s)) 364 #instruction_pc #ticks 365 normalize nodelta; 366 cases instruction_pc 367 #instruction #pc 368 cases instruction 369 [1: 370 #addr11 cases addr11 #addressing_mode 371 normalize nodelta; cases addressing_mode 372 normalize nodelta; 373 [1,2,3,4,8,9,15,16,17,19: 374 #assm whd in ⊢ (% → ?) 375 #absurd cases(absurd) 376 5,6,7,10,11,12,13,14: 377 whd in ⊢ (% → ?) 378 #absurd cases(absurd) 379 18: 380 #addr11 #irrelevant 381 normalize nodelta; 382 >set_program_counter_ignores_clock 383 normalize nodelta; 384 >set_program_counter_ignores_clock 385 >write_at_stack_pointer_ignores_clock 386 >set_8051_sfr_ignores_clock 387 >write_at_stack_pointer_ignores_clock 388 >set_8051_sfr_ignores_clock 389 >clock_set_clock // 390 ] 391 2: 392 #addr16 cases addr16 #addressing_mode 393 normalize nodelta; cases addressing_mode 394 normalize nodelta; 395 [1,2,3,4,8,9,15,16,17,18: 396 #assm whd in ⊢ (% → ?) 397 #absurd cases(absurd) 398 5,6,7,10,11,12,13,14: 399 whd in ⊢ (% → ?) 400 #absurd cases(absurd) 401 19: 402 #addr16 #irrelevant 403 normalize nodelta; 404 >set_program_counter_ignores_clock 405 >write_at_stack_pointer_ignores_clock 406 >set_8051_sfr_ignores_clock 407 >write_at_stack_pointer_ignores_clock 408 >set_8051_sfr_ignores_clock 409 >clock_set_clock 410 >set_program_counter_ignores_clock // 411 ] 412 3: #addr11 cases addr11 #addressing_mode 413 normalize nodelta; cases addressing_mode 414 normalize nodelta; 415 [1,2,3,4,8,9,15,16,17,19: 416 #assm whd in ⊢ (% → ?) 417 #absurd cases(absurd) 418 5,6,7,10,11,12,13,14: 419 whd in ⊢ (% → ?) 420 #absurd cases(absurd) 421 18: 422 #word11 #irrelevant 423 normalize nodelta; 424 >set_program_counter_ignores_clock 425 >clock_set_clock 426 >set_program_counter_ignores_clock // 427 ] 428 4: #addr16 cases addr16 #addressing_mode 429 normalize nodelta; cases addressing_mode 430 normalize nodelta; 431 [1,2,3,4,8,9,15,16,17,18: 432 #assm whd in ⊢ (% → ?) 433 #absurd cases(absurd) 434 5,6,7,10,11,12,13,14: 435 whd in ⊢ (% → ?) 436 #absurd cases(absurd) 437 19: 438 #word #irrelevant 439 normalize nodelta; 440 >set_program_counter_ignores_clock 441 >clock_set_clock 442 >set_program_counter_ignores_clock // 443 ] 444 5: #relative cases relative #addressing_mode 445 normalize nodelta; cases addressing_mode 446 normalize nodelta; 447 [1,2,3,4,8,9,15,16,18,19: 448 #assm whd in ⊢ (% → ?) 449 #absurd cases(absurd) 450 5,6,7,10,11,12,13,14: 451 whd in ⊢ (% → ?) 452 #absurd cases(absurd) 453 17: 454 #byte #irrelevant 455 normalize nodelta; 456 >set_program_counter_ignores_clock 457 >set_program_counter_ignores_clock 458 >clock_set_clock // 459 ] 460 6: #indirect_dptr cases indirect_dptr #addressing_mode 461 normalize nodelta; cases addressing_mode 462 normalize nodelta; 463 464 465 lemma current_instruction_cost_is_ok: 466 ∀s: Status. 467 current_instruction_cost s = clock … (execute 1 s)  clock … s. 468 #s 469 change in match (execute 1 s) with (execute_1 s); 470 change in match (execute_1 s) with ( 471 let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s) 472 (program_counter (BitVectorTrie Byte 16) s) 473 in 474 execute_1_0 s instr_pc_ticks); 475 change in ⊢ (??%?) with ( 476 \snd (fetch (code_memory … s) (program_counter … s))); 477 normalize nodelta; 312 478 313 479 let rec compute_max_trace_label_label_cost_is_ok … … 348 514 2: cases the_trace 349 515 [1: #the_status #not_return #not_jump #not_cost 516 change in ⊢ (??%?) with (current_instruction_cost the_status); 517 @current_instruction_cost_is_ok 350 518 2: #the_status #is_return 519 change in ⊢ (??%?) with (current_instruction_cost the_status); 520 @current_instruction_cost_is_ok 351 521 3: #the_status #is_jump #is_cost 522 change in ⊢ (??%?) with (current_instruction_cost the_status); 523 @current_instruction_cost_is_ok 352 524 4: #end_flag #pre_fun_call #after_fun_call #final #is_call 353 #next_intruction_coherence #call_trace #final_trace 525 #next_instruction_coherence #call_trace #final_trace 526 change in ⊢ (??%?) with ( 527 let current_instruction_cost ≝ current_instruction_cost pre_fun_call in 528 let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in 529 let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in 530 call_trace_cost + current_instruction_cost + final_trace_cost) 531 normalize nodelta; 532 >current_instruction_cost_is_ok 533 >compute_max_trace_label_return_cost_is_ok 534 >compute_max_trace_label_label_pre_cost_is_ok 535 generalize in match next_instruction_coherence; 536 change in ⊢ (% → ?) with ( 537 let size ≝ current_instruction_cost pre_fun_call in 538 let pc_before ≝ program_counter … pre_fun_call in 539 let pc_after ≝ program_counter … after_fun_call in 540 let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in 541 sum = pc_after) 542 normalize nodelta; 543 >(plus_minus_rearrangement 544 (clock (BitVectorTrie Byte 16) after_fun_call) 545 (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)) 546 (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?); 354 547 5: #end_flag #status_pre #status_end #tail_trace #is_not_call 355 548 #is_not_jump #is_not_ret #is_not_labelled 356 @current_instruction_cost 549 change in ⊢ (??%?) with ( 550 let current_instruction_cost ≝ current_instruction_cost status_pre in 551 let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in 552 current_instruction_cost + tail_trace_cost) 553 normalize nodelta; 554 >compute_max_trace_label_label_pre_cost_is_ok 555 >current_instruction_cost_is_ok 357 556 ] 358 557 ] 
src/ASM/Interpret.ma
r1494 r1511 545 545 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 546 546 [ ADDR11 a ⇒ λaddr11: True. 547 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in547 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 548 548 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 549 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 549 let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in 550 let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in 550 551 let s ≝ write_at_stack_pointer ? s pc_bl in 551 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in552 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 552 553 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 553 554 let s ≝ write_at_stack_pointer ? s pc_bu in 554 let 〈thr, eig〉 ≝ split ? 3 8 a in 555 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 555 let thr ≝ \fst (split ? 3 8 a) in 556 let eig ≝ \snd (split ? 3 8 a) in 557 let fiv ≝ \fst (split ? 5 3 pc_bu) in 558 let thr' ≝ \snd (split ? 5 3 pc_bu) in 556 559 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 557 560 set_program_counter ? s new_addr … … 562 565 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 563 566 [ ADDR16 a ⇒ λaddr16: True. 564 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in567 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 565 568 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 566 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 569 let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in 570 let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in 567 571 let s ≝ write_at_stack_pointer ? s pc_bl in 568 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in572 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 569 573 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 570 574 let s ≝ write_at_stack_pointer ? s pc_bu in … … 596 600 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 597 601 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 598 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptrin599 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addrin602 let jmp_addr ≝ \snd (half_add ? big_acc dptr) in 603 let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr) in 600 604 set_program_counter ? s new_pc 601 605  LJMP addr ⇒ … … 610 614 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 611 615 [ RELATIVE r ⇒ λrelative: True. 612 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in616 let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in 613 617 set_program_counter ? s new_pc 614 618  _ ⇒ λother: False. ⊥ … … 618 622 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 619 623 [ ADDR11 a ⇒ λaddr11: True. 620 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 621 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 624 let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in 625 let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in 626 let nu ≝ \fst (split ? 4 4 pc_bu) in 627 let nl ≝ \snd (split ? 4 4 pc_bu) in 622 628 let bit ≝ get_index' ? O ? nl in 623 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 629 let relevant1 ≝ \fst (split ? 3 8 a) in 630 let relevant2 ≝ \snd (split ? 3 8 a) in 624 631 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 625 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addrin632 let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in 626 633 set_program_counter ? s new_pc 627 634  _ ⇒ λother: False. ⊥
Note: See TracChangeset
for help on using the changeset viewer.