Changeset 1547 for src/ASM/Interpret.ma
 Timestamp:
 Nov 23, 2011, 11:08:42 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1541 r1547 126 126 qed. 127 127 128 lemma set_arg s_8_ignores_clock:128 lemma set_arg_8_ignores_clock: 129 129 ∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2). 130 130 #M #s #f1 #f2 cases (set_arg_8 M s f1 f2) … … 132 132 qed. 133 133 134 exampleset_program_counter_ignores_clock:134 lemma set_program_counter_ignores_clock: 135 135 ∀M: Type[0]. 136 136 ∀s: PreStatus M. … … 140 140 qed. 141 141 142 exampleset_low_internal_ram_ignores_clock:142 lemma set_low_internal_ram_ignores_clock: 143 143 ∀M: Type[0]. 144 144 ∀s: PreStatus M. … … 148 148 qed. 149 149 150 exampleset_8051_sfr_ignores_clock:150 lemma set_8051_sfr_ignores_clock: 151 151 ∀M: Type[0]. 152 152 ∀s: PreStatus M. … … 156 156 #M #s #sfr #v % 157 157 qed. 158 159 axiom set_arg_8_ignores_clock:160 ∀M: Type[0].161 ∀s: PreStatus M.162 ∀arg.163 ∀val.164 clock M (set_arg_8 … s arg val) = clock … s.165 158 166 exampleclock_set_clock:159 lemma clock_set_clock: 167 160 ∀M: Type[0]. 168 161 ∀s: PreStatus M. … … 172 165 qed. 173 166 174 lemma tech_clocks_le:175 ∀M,s.∀t:Σs'. clock M s ≤ clock M s'. clock … s ≤ clock … t.176 #M #s * //177 qed.178 179 167 definition execute_1_preinstruction: 180 168 ∀ticks: nat × nat. 181 169 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → 182 ∀s:PreStatus M. Σs': PreStatus M. clock M s ≤ clock … s' ≝ 170 ∀s:PreStatus M. 171 Σs': PreStatus M. 172 Or (clock … s'  clock … s = \fst ticks) 173 (clock … s'  clock … s = \snd ticks) 174 ≝ 183 175 λticks. 184 176 λA, M: Type[0]. … … 188 180 let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in 189 181 let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in 190 match instr return λx. Σs': PreStatus M. clock … s ≤ clock … s' with 182 match instr return λx. Σs': PreStatus M. Or (clock … s'  clock … s = \fst ticks) 183 (clock … s'  clock … s = \snd ticks) with 191 184 [ ADD addr1 addr2 ⇒ 192 185 let s ≝ add_ticks1 s in … … 269 262 ] 270 263  INC addr ⇒ 271 match addr return λx. bool_to_Prop (is_in … [[ acc_a; 272 registr; 273 direct; 274 indirect; 275 dptr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with 264 match addr 265 return 266 λx. bool_to_Prop 267 (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → 268 Σs': PreStatus M. 269 Or (clock … s'  clock … s = \fst ticks) 270 (clock … s'  clock … s = \snd ticks) 271 with 276 272 [ ACC_A ⇒ λacc_a: True. 277 273 let s' ≝ add_ticks1 s in … … 345 341 s 346 342  CLR addr ⇒ 347 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s'with343 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 348 344 [ ACC_A ⇒ λacc_a: True. 349 345 let s ≝ add_ticks1 s in … … 358 354 ] (subaddressing_modein … addr) 359 355  CPL addr ⇒ 360 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s'with356 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 361 357 [ ACC_A ⇒ λacc_a: True. 362 358 let s ≝ add_ticks1 s in … … 412 408 set_8051_sfr ? s SFR_ACC_A new_acc 413 409  PUSH addr ⇒ 414 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus M. clock … s ≤ clock … s'with410 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 415 411 [ DIRECT d ⇒ λdirect: True. 416 412 let s ≝ add_ticks1 s in … … 589 585 let s ≝ add_ticks2 s in 590 586 s 591 ]. cases daemon (* 592 (*14s*) 593 (* try assumption (*20s*) 587 ]. (*15s*) 588 try assumption (*20s*) 594 589 try % (*6s*) 595 590 try ( 596 591 @ (execute_1_technical … (subaddressing_modein …)) 597 592 @ I 598 ) (*34s*) *) 599 try assumption 593 ) (*66s*) 600 594 try @le_n 595 [ /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ // 596 *: cases daemon ] 597 (* 601 598 [2,6,10: normalize @I 602 599 1,5: /by/ (* 81 seconds *) … … 666 663 qed. 667 664 668 definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s'≝665 definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat. Σs': Status. clock … s'  clock … s = \snd current ≝ 669 666 λs0,instr_pc_ticks. 670 667 let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in 671 668 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 672 669 let s ≝ set_program_counter ? s0 pc in 673 match instr return λ_. Σs': Status. clock … s0 ≤ clock … s'with674 [ RealInstruction instr ⇒ e xecute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?670 match instr return λ_.Status with 671 [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ? 675 672 (λx. λs. 676 673 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with 677 674 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r)) 678 675  _ ⇒ λabsd. ⊥ 679 ] (subaddressing_modein … x)) instr s 676 ] (subaddressing_modein … x)) instr s) 680 677  ACALL addr ⇒ 681 678 let s ≝ set_clock ? s (ticks + clock ? s) in 682 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s 0 ≤ clock … s'with679 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 683 680 [ ADDR11 a ⇒ λaddr11: True. 684 681 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in … … 697 694  LCALL addr ⇒ 698 695 let s ≝ set_clock ? s (ticks + clock ? s) in 699 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s 0 ≤ clock … s'with696 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 700 697 [ ADDR16 a ⇒ λaddr16: True. 701 698 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in … … 711 708  MOVC addr1 addr2 ⇒ 712 709 let s ≝ set_clock ? s (ticks + clock ? s) in 713 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s 0 ≤ clock … s'with710 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 714 711 [ ACC_DPTR ⇒ λacc_dptr: True. 715 712 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in … … 738 735  LJMP addr ⇒ 739 736 let s ≝ set_clock ? s (ticks + clock ? s) in 740 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s 0 ≤ clock … s'with737 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 741 738 [ ADDR16 a ⇒ λaddr16: True. 742 739 set_program_counter ? s a … … 745 742  SJMP addr ⇒ 746 743 let s ≝ set_clock ? s (ticks + clock ? s) in 747 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s 0 ≤ clock … s'with744 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 748 745 [ RELATIVE r ⇒ λrelative: True. 749 746 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in … … 753 750  AJMP addr ⇒ 754 751 let s ≝ set_clock ? s (ticks + clock ? s) in 755 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s 0 ≤ clock … s'with752 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s'  clock … s0 = ticks with 756 753 [ ADDR11 a ⇒ λaddr11: True. 757 754 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in … … 764 761  _ ⇒ λother: False. ⊥ 765 762 ] (subaddressing_modein … addr) 766 ]. 767 try assumption 768 [1,2: >set_program_counter_ignores_clock normalize nodelta 763 ]. (*10s*) 764 [*:try assumption] 765 [1,2,3,4,5,7: @sig2 (*7s*) 766 8: cases (execute_1_preinstruction ??????) #a * #H @H] 767 [2,3: >set_program_counter_ignores_clock normalize nodelta 769 768 >write_at_stack_pointer_ignores_clock 770 769 >set_8051_sfr_ignores_clock 771 770 >write_at_stack_pointer_ignores_clock 772 >set_8051_sfr_ignores_clock 773 change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/ 774 3,4,5,6: >set_program_counter_ignores_clock normalize nodelta 775 change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/ 776 7,8: >set_8051_sfr_ignores_clock normalize nodelta change with (? ≤ ?+?) 777 >set_program_counter_ignores_clock /by/] 778 qed. 779 780 definition execute_1: ∀s:Status. Σs':Status. clock … s ≤ clock … s' ≝ 771 >set_8051_sfr_ignores_clock >clock_set_clock 772 >set_program_counter_ignores_clock 773 cut (∀n,m. n+mm = n) [1,3:#n #m /by/ *: #H @H] (*Andrea: ???*) 774 1,4,5,6: >set_program_counter_ignores_clock normalize nodelta 775 >clock_set_clock >set_program_counter_ignores_clock 776 cut (∀n,m. n+mm = n) [1,3,5,7:#n #m /by/ *: #H @H] (*Andrea: ???*) 777 7: >set_8051_sfr_ignores_clock normalize nodelta 778 >clock_set_clock >set_program_counter_ignores_clock 779 cut (∀n,m. n+mm = n) [1,3:#n #m /by/ *: #H @H] 780 8: >set_8051_sfr_ignores_clock normalize nodelta 781 >set_program_counter_ignores_clock >clock_set_clock 782 >set_program_counter_ignores_clock 783 cut (∀n,m. n+mm = n) [1,3:#n #m /by/ *: #H @H]] 784 qed. 785 786 definition current_instruction_cost ≝ 787 λs: Status. \snd (fetch (code_memory … s) (program_counter … s)). 788 789 definition execute_1: ∀s:Status. Σs':Status. clock … s'  clock … s = current_instruction_cost s ≝ 781 790 λs: Status. 782 791 let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
Note: See TracChangeset
for help on using the changeset viewer.