Changeset 1575
 Timestamp:
 Nov 29, 2011, 2:21:39 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1573 r1575 249 249 qed. 250 250 251 lemmacurrent_instruction_cost_non_zero:251 axiom current_instruction_cost_non_zero: 252 252 ∀s: Status. 253 253 current_instruction_cost s > 0. 254 #s255 cases s256 #code_memory #hi_ram #lo_ram #x_ram #pc #sfr_8051 #sfr_8052 #p1_latch257 #p2_latch #clock258 change with (\snd (fetch ? ?)) in ⊢ (?%?);259 change with (fetch0 ? ?) in match (fetch ? ?);260 change with (261 let 〈pc,v〉 ≝ next code_memory pc in262 let 〈b,v0〉 ≝head bool 7 v in263 ?) in match (fetch0 ? ?);264 normalize nodelta;265 266 cases(fetch (code_memory … s) (program_counter … s))267 #instruction_pc268 cases(instruction_pc)269 #instruction #pc270 cases(instruction)271 [ #addr11272 254 273 255 lemma le_monotonic_plus: 274 256 ∀m, n, o: nat. 275 257 m ≤ n → m + o ≤ n + o. 276 #m #n #o #hyp 277 elim o 278 [ // 279  #o' #ind_hyp 280 <plus_n_Sm <plus_n_Sm 281 @le_S_S 282 assumption 283 ] 258 #m #n #o #hyp /2/ 284 259 qed. 285 260 … … 296 271 ∀m, n, o. 297 272 m  n = o → o > 0 → n ≤ m. 273 (* #m #n #o #eq_hyp <eq_hyp in ⊢ (% → ?); 274 normalize in ⊢ (% → ?); 275 >le_monot *) 298 276 299 277 let rec compute_max_trace_label_label_cost_is_ok 
src/ASM/Interpret.ma
r1573 r1575 170 170 ∀s:PreStatus M. 171 171 Σs': PreStatus M. 172 Or (clock … s'  clock … s = \fst ticks) 173 (clock … s'  clock … s = \snd ticks) 172 And 173 (Or (clock … s'  clock … s = \fst ticks) 174 (clock … s'  clock … s = \snd ticks)) 175 (clock … s ≤ clock … s') 174 176 ≝ 175 177 λticks. … … 180 182 let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in 181 183 let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in 182 match instr return λx. Σs': PreStatus M. Or (clock … s'  clock … s = \fst ticks) 183 (clock … s'  clock … s = \snd ticks) with 184 match instr return λx. 185 Σs': PreStatus M. 186 And 187 (Or (clock … s'  clock … s = \fst ticks) 188 (clock … s'  clock … s = \snd ticks)) 189 (clock … s ≤ clock … s') with 184 190 [ ADD addr1 addr2 ⇒ 185 191 let s ≝ add_ticks1 s in … … 267 273 (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → 268 274 Σs': PreStatus M. 269 Or (clock … s'  clock … s = \fst ticks) 270 (clock … s'  clock … s = \snd ticks) 275 And 276 (Or (clock … s'  clock … s = \fst ticks) 277 (clock … s'  clock … s = \snd ticks)) 278 (clock … s ≤ clock … s') 271 279 with 272 280 [ ACC_A ⇒ λacc_a: True. … … 341 349 s 342 350  CLR addr ⇒ 343 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. Or (clock … s'  clock … s = \fst ticks) (clock … s'  clock … s = \snd ticks) with 351 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → 352 Σs': PreStatus M. 353 And 354 (Or (clock … s'  clock … s = \fst ticks) 355 (clock … s'  clock … s = \snd ticks)) 356 (clock … s ≤ clock … s') with 344 357 [ ACC_A ⇒ λacc_a: True. 345 358 let s ≝ add_ticks1 s in … … 354 367 ] (subaddressing_modein … addr) 355 368  CPL addr ⇒ 356 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. Or (clock … s'  clock … s = \fst ticks) (clock … s'  clock … s = \snd ticks) with 369 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → 370 Σs': PreStatus M. 371 And 372 (Or (clock … s'  clock … s = \fst ticks) 373 (clock … s'  clock … s = \snd ticks)) 374 (clock … s ≤ clock … s') with 357 375 [ ACC_A ⇒ λacc_a: True. 358 376 let s ≝ add_ticks1 s in … … 408 426 set_8051_sfr ? s SFR_ACC_A new_acc 409 427  PUSH addr ⇒ 410 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus M. Or (clock … s'  clock … s = \fst ticks) (clock … s'  clock … s = \snd ticks) with 428 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → 429 Σs': PreStatus M. 430 And 431 (Or (clock … s'  clock … s = \fst ticks) 432 (clock … s'  clock … s = \snd ticks)) 433 (clock … s ≤ clock … s') with 411 434 [ DIRECT d ⇒ λdirect: True. 412 435 let s ≝ add_ticks1 s in … … 593 616 ) (*66s*) 594 617 try @le_n 595 [ /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ // 596 *: cases daemon ] 597 (* 598 [2,6,10: normalize @I 599 1,5: /by/ (* 81 seconds *) 600 9: 601 normalize nodelta <set_flags_ignores_clock >set_arg_8_ignores_clock 602 >clock_set_clock // 603 23: 604 normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock 605 >set_8051_sfr_ignores_clock >clock_set_clock // 606 21,24: 607 normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock 608 >clock_set_clock // 609 25,26,28: 610 normalize nodelta // 611 30,32,35: 612 normalize nodelta // 613 13,14,15,16,18: 614 normalize nodelta >set_arg_8_ignores_clock >clock_set_clock // 615 17: 616 normalize nodelta >set_8051_sfr_ignores_clock >clock_set_clock // 617 3,4,7,8,11,12,19,20,33,36: cases daemon 618 27,29,31,34,37: 619 normalize nodelta >set_program_counter_ignores_clock >clock_set_clock // 620 22: 621 normalize nodelta <set_flags_ignores_clock >clock_set_clock // 622 [9: (* normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock 623 >clock_set_clock // *) (* segfault now *) 624 32,34: cases l #either normalize nodelta cases either 625 #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock 626 >clock_set_clock // 627 36,48: cases addr #either normalize nodelta cases either 628 #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock 629 >clock_set_clock // (* XXX: change addr to l *) 630 44: cases l2 #either normalize nodelta 631 [2: cases either #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock 632 >clock_set_clock // 633 1: cases either #addr cases addr #addr1 #addr2 normalize nodelta 634 >set_arg_8_ignores_clock >clock_set_clock // 635 ] (* XXX: change l2 to l *) 636 5: cases (sub_8_with_carry (get_arg_8 M s1 true addr) (bitvector_of_nat 8 1) false) 637 #result #flags normalize nodelta >set_arg_8_ignores_clock >clock_set_clock // 638 37: cases addr 639 20,21,30,31: (* XXX: segfault here *) 640 1,2,3: /by/ (*41s*) 641 4,6,7,8,10,11,12,13,14,15: /by/ (*6s*) 642 16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*9s*) 643 33,35,39,41,43,54,55,56: /by/ (*6s*) 644 57,58,59,60,61: <set_args_8_ignores_clock /by/ (*0.5s ??*) 645 (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *) 646 *:cases daemon] *) 618 [ /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ /2 by or_introl/ 619  /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ // 620 *: cases daemon (* XXX: easy? *) ] 647 621 qed. 648 622 … … 663 637 qed. 664 638 665 definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat. Σs': Status. clock … s'  clock … s = \snd current ≝ 639 definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat. 640 Σs': Status. And (clock … s'  clock … s = \snd current) (clock … s ≤ clock … s') ≝ 666 641 λs0,instr_pc_ticks. 667 642 let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in 668 643 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 669 644 let s ≝ set_program_counter ? s0 pc in 670 match instr return λ_. Statuswith671 [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?645 match instr return λ_. Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 646 [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ? 672 647 (λx. λs. 673 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ?with648 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 674 649 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r)) 675 650  _ ⇒ λabsd. ⊥ 676 651 ] (subaddressing_modein … x)) instr s) 677  ACALL addr⇒652  MOVC addr1 addr2 ⇒ 678 653 let s ≝ set_clock ? s (ticks + clock ? s) in 679 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 680 [ ADDR11 a ⇒ λaddr11: True. 681 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 682 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 683 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 684 let s ≝ write_at_stack_pointer ? s pc_bl in 685 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 686 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 687 let s ≝ write_at_stack_pointer ? s pc_bu in 688 let 〈thr, eig〉 ≝ split ? 3 8 a in 689 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 690 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 691 set_program_counter ? s new_addr 692  _ ⇒ λother: False. ⊥ 693 ] (subaddressing_modein … addr) 694  LCALL addr ⇒ 695 let s ≝ set_clock ? s (ticks + clock ? s) in 696 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 697 [ ADDR16 a ⇒ λaddr16: True. 698 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 699 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 700 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 701 let s ≝ write_at_stack_pointer ? s pc_bl in 702 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 703 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 704 let s ≝ write_at_stack_pointer ? s pc_bu in 705 set_program_counter ? s a 706  _ ⇒ λother: False. ⊥ 707 ] (subaddressing_modein … addr) 708  MOVC addr1 addr2 ⇒ 709 let s ≝ set_clock ? s (ticks + clock ? s) in 710 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 654 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → 655 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 711 656 [ ACC_DPTR ⇒ λacc_dptr: True. 712 657 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in … … 726 671  _ ⇒ λother: False. ⊥ 727 672 ] (subaddressing_modein … addr2) 728 673  JMP _ ⇒ (* DPM: always indirect_dptr *) 729 674 let s ≝ set_clock ? s (ticks + clock ? s) in 730 675 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in … … 733 678 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in 734 679 set_program_counter ? s new_pc 735 680  LJMP addr ⇒ 736 681 let s ≝ set_clock ? s (ticks + clock ? s) in 737 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 682 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → 683 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 738 684 [ ADDR16 a ⇒ λaddr16: True. 739 685 set_program_counter ? s a 740 686  _ ⇒ λother: False. ⊥ 741 687 ] (subaddressing_modein … addr) 742 688  SJMP addr ⇒ 743 689 let s ≝ set_clock ? s (ticks + clock ? s) in 744 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 690 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → 691 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 745 692 [ RELATIVE r ⇒ λrelative: True. 746 693 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in … … 748 695  _ ⇒ λother: False. ⊥ 749 696 ] (subaddressing_modein … addr) 750 697  AJMP addr ⇒ 751 698 let s ≝ set_clock ? s (ticks + clock ? s) in 752 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 699 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → 700 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 753 701 [ ADDR11 a ⇒ λaddr11: True. 754 702 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in … … 761 709  _ ⇒ λother: False. ⊥ 762 710 ] (subaddressing_modein … addr) 711  ACALL addr ⇒ 712 let s ≝ set_clock ? s (ticks + clock ? s) in 713 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → 714 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 715 [ ADDR11 a ⇒ λaddr11: True. 716 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 717 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 718 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 719 let s ≝ write_at_stack_pointer ? s pc_bl in 720 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 721 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 722 let s ≝ write_at_stack_pointer ? s pc_bu in 723 let 〈thr, eig〉 ≝ split ? 3 8 a in 724 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 725 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 726 set_program_counter ? s new_addr 727  _ ⇒ λother: False. ⊥ 728 ] (subaddressing_modein … addr) 729  LCALL addr ⇒ 730 let s ≝ set_clock ? s (ticks + clock ? s) in 731 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → 732 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 733 [ ADDR16 a ⇒ λaddr16: True. 734 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 735 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 736 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 737 let s ≝ write_at_stack_pointer ? s pc_bl in 738 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 739 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 740 let s ≝ write_at_stack_pointer ? s pc_bu in 741 set_program_counter ? s a 742  _ ⇒ λother: False. ⊥ 743 ] (subaddressing_modein … addr) 763 744 ]. (*10s*) 745 cases daemon (* XXX: problem with russell here *) 746 (* 764 747 [*:try assumption] 765 748 [1,2,3,4,5,7: @sig2 (*7s*) … … 781 764 >set_program_counter_ignores_clock >clock_set_clock 782 765 >set_program_counter_ignores_clock 783 cut (∀n,m. n+mm = n) [1,3:#n #m /by/ *: #H @H]] 766 cut (∀n,m. n+mm = n) [1,3:#n #m /by/ *: #H @H]] *) 784 767 qed. 785 768 … … 788 771 \snd (fetch (code_memory … s) (program_counter … s)). 789 772 790 definition execute_1: ∀s:Status. Σs':Status. clock … s'  clock … s = current_instruction_cost s ≝ 773 definition execute_1: ∀s:Status. 774 Σs':Status. And (clock … s'  clock … s = current_instruction_cost s) (clock … s ≤ clock … s') ≝ 791 775 λs: Status. 792 776 let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
Note: See TracChangeset
for help on using the changeset viewer.