Changeset 1588 for src/ASM/Interpret.ma
 Timestamp:
 Dec 6, 2011, 11:21:37 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1587 r1588 18 18 cases b 19 19 normalize 20 //21 20 # K 21 try % 22 22 cases (eq_true_false K) 23 23 qed. … … 126 126 qed. 127 127 128 lemma set_arg_8_ignores_clock:129 ∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2).130 #M #s #f1 #f2 cases (set_arg_8 M s f1 f2)131 #a #E >E //132 qed.133 134 128 lemma set_program_counter_ignores_clock: 135 129 ∀M: Type[0]. … … 163 157 clock … (set_8051_sfr ? s sfr v) = clock … s. 164 158 #M #s #sfr #v % 165 qed.166 167 lemma set_arg_1_ignores_clock:168 ∀m: Type[0].169 ∀s: PreStatus m.170 ∀addr: [[bit_addr; carry]].171 ∀bit: Bit.172 clock … (set_arg_1 m s addr bit) = clock … s.173 #m #s #addr #bit174 whd in match set_arg_1; normalize nodelta175 cases addr #subaddressing_mode176 cases subaddressing_mode177 try #assm1 try #assm2178 try (normalize in assm2; cases assm2)179 try (normalize in assm1; cases assm1)180 normalize nodelta181 cases (split bool 4 4 (get_8051_sfr m s SFR_PSW))182 #nu #nl normalize nodelta183 [ @set_8051_sfr_ignores_clock184  cases(split … 1 3 nu)185 #ignore #three_bits normalize nodelta186 cases(get_index_v … 4 nu 0 ?)187 normalize nodelta188 [ <set_bit_addressable_sfr_ignores_clock  >set_low_internal_ram_ignores_clock ] %189 ]190 qed.191 192 lemma set_arg_16_ignores_clock:193 ∀m: Type[0].194 ∀s: PreStatus m.195 ∀w: Word.196 ∀addr: [[dptr]].197 clock … (set_arg_16 m s w addr) = clock … s.198 #m #s #w #addr199 whd in match set_arg_16; normalize nodelta200 cases addr #subaddressing_modein201 cases subaddressing_modein202 try #assm1 try #assm2203 try (normalize in assm2; cases assm2)204 try (normalize in assm1; cases assm1)205 normalize nodelta206 cases (split … 8 8 w) #bu #bl normalize nodelta207 >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock %208 159 qed. 209 160 … … 228 179 qed. 229 180 230 definition execute_1_preinstruction :181 definition execute_1_preinstruction': 231 182 ∀ticks: nat × nat. 232 183 ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a → … … 279 230 let 〈addr1, addr2〉 ≝ l' in 280 231 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 281 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)232 set_arg_8 ? s addr1 and_val 282 233  inr r ⇒ 283 234 let 〈addr1, addr2〉 ≝ r in 284 235 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 285 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)236 set_arg_8 ? s addr1 and_val 286 237 ] 287 238  inr r ⇒ 288 239 let 〈addr1, addr2〉 ≝ r in 289 240 let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in 290 eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s and_val (None ?) (get_ov_flag ? s))241 set_flags ? s and_val (None ?) (get_ov_flag ? s) 291 242 ] 292 243  ORL addr ⇒ … … 294 245 match addr with 295 246 [ inl l ⇒ 296 match l return λ_. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s)with247 match l with 297 248 [ inl l' ⇒ 298 249 let 〈addr1, addr2〉 ≝ l' in 299 250 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 300 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)251 set_arg_8 ? s addr1 or_val 301 252  inr r ⇒ 302 253 let 〈addr1, addr2〉 ≝ r in 303 254 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 304 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)255 set_arg_8 ? s addr1 or_val 305 256 ] 306 257  inr r ⇒ 307 258 let 〈addr1, addr2〉 ≝ r in 308 259 let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in 309 eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s or_val (None ?) (get_ov_flag ? s))260 set_flags ? s or_val (None ?) (get_ov_flag ? s) 310 261 ] 311 262  XRL addr ⇒ … … 315 266 let 〈addr1, addr2〉 ≝ l' in 316 267 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 317 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)268 set_arg_8 ? s addr1 xor_val 318 269  inr r ⇒ 319 270 let 〈addr1, addr2〉 ≝ r in 320 271 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 321 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)272 set_arg_8 ? s addr1 xor_val 322 273 ] 323 274  INC addr ⇒ … … 326 277 let s' ≝ add_ticks1 s in 327 278 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in 328 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' ACC_A result)279 set_arg_8 ? s' ACC_A result 329 280  REGISTER r ⇒ λregister: True. 330 281 let s' ≝ add_ticks1 s in 331 282 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in 332 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (REGISTER r) result)283 set_arg_8 ? s' (REGISTER r) result 333 284  DIRECT d ⇒ λdirect: True. 334 285 let s' ≝ add_ticks1 s in 335 286 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in 336 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (DIRECT d) result)287 set_arg_8 ? s' (DIRECT d) result 337 288  INDIRECT i ⇒ λindirect: True. 338 289 let s' ≝ add_ticks1 s in 339 290 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 340 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (INDIRECT i) result)291 set_arg_8 ? s' (INDIRECT i) result 341 292  DPTR ⇒ λdptr: True. 342 293 let s' ≝ add_ticks1 s in … … 344 295 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in 345 296 let s ≝ set_8051_sfr ? s' SFR_DPL bl in 346 eject (PreStatus m) (λx. clock … s' = clock … x) (set_8051_sfr ? s' SFR_DPH bu)297 set_8051_sfr ? s' SFR_DPH bu 347 298  _ ⇒ λother: False. ⊥ 348 299 ] (subaddressing_modein … addr) … … 353 304 let s ≝ add_ticks1 s in 354 305 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in 355 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr result)306 set_arg_8 ? s addr result 356 307  MUL addr1 addr2 ⇒ 357 308 let s ≝ add_ticks1 s in … … 397 348 [ ACC_A ⇒ λacc_a: True. 398 349 let s ≝ add_ticks1 s in 399 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s ACC_A (zero 8))350 set_arg_8 ? s ACC_A (zero 8) 400 351  CARRY ⇒ λcarry: True. 401 352 let s ≝ add_ticks1 s in 402 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY false)353 set_arg_1 ? s CARRY false 403 354  BIT_ADDR b ⇒ λbit_addr: True. 404 355 let s ≝ add_ticks1 s in 405 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) false)356 set_arg_1 ? s (BIT_ADDR b) false 406 357  _ ⇒ λother: False. ⊥ 407 358 ] (subaddressing_modein … addr) … … 412 363 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 413 364 let new_acc ≝ negation_bv ? old_acc in 414 eject (PreStatus m) (λx. clock … s = clock … x) (set_8051_sfr ? s SFR_ACC_A new_acc)365 set_8051_sfr ? s SFR_ACC_A new_acc 415 366  CARRY ⇒ λcarry: True. 416 367 let s ≝ add_ticks1 s in 417 368 let old_cy_flag ≝ get_arg_1 ? s CARRY true in 418 369 let new_cy_flag ≝ ¬old_cy_flag in 419 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY new_cy_flag)370 set_arg_1 ? s CARRY new_cy_flag 420 371  BIT_ADDR b ⇒ λbit_addr: True. 421 372 let s ≝ add_ticks1 s in 422 373 let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in 423 374 let new_bit ≝ ¬old_bit in 424 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) new_bit)375 set_arg_1 ? s (BIT_ADDR b) new_bit 425 376  _ ⇒ λother: False. ? 426 377 ] (subaddressing_modein … addr) … … 480 431 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 481 432 let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in 482 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr2 old_acc)433 set_arg_8 ? s addr2 old_acc 483 434  XCHD addr1 addr2 ⇒ 484 435 let s ≝ add_ticks1 s in … … 515 466 [ inl l ⇒ 516 467 let 〈addr1, addr2〉 ≝ l in 517 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))468 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 518 469  inr r ⇒ 519 470 let 〈addr1, addr2〉 ≝ r in 520 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))471 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 521 472 ] 522 473  MOV addr ⇒ … … 533 484 [ inl l'''' ⇒ 534 485 let 〈addr1, addr2〉 ≝ l'''' in 535 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))486 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 536 487  inr r'''' ⇒ 537 488 let 〈addr1, addr2〉 ≝ r'''' in 538 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))489 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 539 490 ] 540 491  inr r''' ⇒ 541 492 let 〈addr1, addr2〉 ≝ r''' in 542 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))493 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 543 494 ] 544 495  inr r'' ⇒ 545 496 let 〈addr1, addr2〉 ≝ r'' in 546 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_16 ? s (get_arg_16 ? s addr2) addr1)497 set_arg_16 ? s (get_arg_16 ? s addr2) addr1 547 498 ] 548 499  inr r ⇒ 549 500 let 〈addr1, addr2〉 ≝ r in 550 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))501 set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false) 551 502 ] 552 503  inr r ⇒ 553 504 let 〈addr1, addr2〉 ≝ r in 554 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))505 set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false) 555 506 ] 556 507  JC addr ⇒ … … 638 589 let s ≝ add_ticks2 s in 639 590 s 640 ]. (*15s*) (*591 ]. (*15s*) 641 592 try (cases(other)) 642 593 try assumption (*20s*) 643 try % (*6s*)594 try (% @False) (*6s*) (* Bug exploited here to implement solve :*) 644 595 try ( 645 596 @ (execute_1_technical … (subaddressing_modein …)) 646 597 @ I 647 598 ) (*66s*) 648 try (<set_arg_8_ignores_clock normalize nodelta /demod/ %) 649 try (/demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ %) 650 try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock /demod/ %) 651 try (normalize nodelta <set_flags_ignores_clock /demod/ %) 652 try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus) 653 try (/demod/ normalize nodelta >clock_set_clock @commutative_plus) 654 try (/demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock @commutative_plus) 655 try (/demod/ normalize nodelta >clock_set_clock <set_arg_8_ignores_clock @commutative_plus) 656 try (/demod/ normalize nodelta >set_arg_1_ignores_clock >clock_set_clock @commutative_plus) 657 try (normalize nodelta >clock_set_clock >set_arg_1_ignores_clock >clock_set_clock %) 658 try (normalize nodelta <set_arg_8_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %) 659 try (normalize nodelta >set_arg_1_ignores_clock >clock_set_clock %) 660 try (normalize nodelta >clock_set_clock >set_arg_16_ignores_clock >clock_set_clock %) 661 try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %) *) (* XXX: for convenience *) 662 cases daemon 599 normalize nodelta /2 by or_introl, or_intror/ (*35s*) 600 qed. 601 602 definition execute_1_preinstruction: 603 ∀ticks: nat × nat. 604 ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a → 605 PreStatus m → PreStatus m ≝ execute_1_preinstruction'. 606 607 lemma execute_1_preinstruction_ok: 608 ∀ticks,a,m,f,i,s. 609 clock ? (execute_1_preinstruction ticks a m f i s) = \fst ticks + clock … s ∨ 610 clock ? (execute_1_preinstruction ticks a m f i s) = \snd ticks + clock … s. 611 #ticks #a #m #f #i #s whd in match execute_1_preinstruction; normalize nodelta @sig2 663 612 qed. 664 613 … … 669 618 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 670 619 let s ≝ set_program_counter ? s0 pc in 671 match instr return λ_. Σs': Status. clock … s' = ticks + clock … s0with672 [ RealInstruction instr ⇒ e ject … (execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?620 match instr return λ_.Status with 621 [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ? 673 622 (λx. λs. 674 623 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 675 624 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r)) 676 625  _ ⇒ λabsd. ⊥ 677 ] (subaddressing_modein … x)) instr s )626 ] (subaddressing_modein … x)) instr s 678 627  MOVC addr1 addr2 ⇒ 679 628 let s ≝ set_clock ? s (ticks + clock ? s) in … … 763 712 ] (subaddressing_modein … addr) 764 713 ]. (*10s*) 765 try (cases(other))766 [2: normalize nodelta767 >set_program_counter_ignores_clock768 >write_at_stack_pointer_ignores_clock769 >set_8051_sfr_ignores_clock770 >write_at_stack_pointer_ignores_clock771 >set_8051_sfr_ignores_clock >clock_set_clock772 >set_program_counter_ignores_clock %773 *: cases daemon774 ]775 (*776 714 [*:try assumption] 777 [1,2,3,4,5,7: @sig2 (*7s*) 778 8: cases (execute_1_preinstruction ??????) #a * #H @H] 779 [2,3: >set_program_counter_ignores_clock normalize nodelta 780 >write_at_stack_pointer_ignores_clock 781 >set_8051_sfr_ignores_clock 782 >write_at_stack_pointer_ignores_clock 783 >set_8051_sfr_ignores_clock >clock_set_clock 784 >set_program_counter_ignores_clock 785 cut (∀n,m. n+mm = n) [1,3:#n #m /by/ *: #H @H] (*Andrea: ???*) 786 1,4,5,6: >set_program_counter_ignores_clock normalize nodelta 787 >clock_set_clock >set_program_counter_ignores_clock 788 cut (∀n,m. n+mm = n) [1,3,5,7:#n #m /by/ *: #H @H] (*Andrea: ???*) 789 7: >set_8051_sfr_ignores_clock normalize nodelta 790 >clock_set_clock >set_program_counter_ignores_clock 791 cut (∀n,m. n+mm = n) [1,3:#n #m /by/ *: #H @H] 792 8: >set_8051_sfr_ignores_clock normalize nodelta 793 >set_program_counter_ignores_clock >clock_set_clock 794 >set_program_counter_ignores_clock 795 cut (∀n,m. n+mm = n) [1,3:#n #m /by/ *: #H @H]] *) 715 [1,2,3,4,5,7: @sig2 (*35s*) 716 8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ? 717 (λx. λs. 718 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 719 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r)) 720  _ ⇒ λabsd. ⊥ 721 ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H 722 *: normalize nodelta try // (*17s*) 723 >set_program_counter_ignores_clock // (* Andrea:??*) ] 796 724 qed. 797 725 … … 800 728 \snd (fetch (code_memory … s) (program_counter … s)). 801 729 802 definition execute_1 : ∀s:Status.730 definition execute_1': ∀s:Status. 803 731 Σs':Status. clock … s' = current_instruction_cost s + clock … s ≝ 804 732 λs: Status. 805 733 let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in 806 734 execute_1_0 s instr_pc_ticks. 735 736 definition execute_1: Status → Status ≝ execute_1'. 737 738 lemma execute_1_ok: ∀s. clock … (execute_1 s) = current_instruction_cost s + clock … s. 739 #s whd in match execute_1; normalize nodelta @sig2 740 qed. (*x Andrea: indexing takes ages here *) 807 741 808 742 definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
Note: See TracChangeset
for help on using the changeset viewer.