Changeset 2272 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jul 27, 2012, 5:53:25 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2256 r2272 335 335 qed. 336 336 337 inductive accumulator_address_map_entry: Type[0] ≝ 338 | data: accumulator_address_map_entry 339 | address: upper_lower → Word → accumulator_address_map_entry. 337 (* XXX: if upper then the byte in the entry is the least significant byte of the address and 338 the byte in the status is the most significant, otherwise if lower then the 339 other way around 340 *) 341 definition address_entry ≝ upper_lower × Byte. 340 342 341 343 definition eq_accumulator_address_map_entry: 342 accumulator_address_map_entry → accumulator_address_map_entry → bool ≝343 λleft : accumulator_address_map_entry.344 λright : accumulator_address_map_entry.344 option address_entry → option address_entry → bool ≝ 345 λleft. 346 λright. 345 347 match left with 346 [ data⇒348 [ None ⇒ 347 349 match right with 348 [ data⇒ true350 [ None ⇒ true 349 351 | _ ⇒ false 350 352 ] 351 | address upper_lower word ⇒ 353 | Some upper_lower_addr ⇒ 354 let 〈upper_lower, addr〉 ≝ upper_lower_addr in 352 355 match right with 353 [ address upper_lower' word' ⇒ 354 eq_upper_lower upper_lower upper_lower' ∧ eq_bv … word word' 356 [ Some upper_lower_addr' ⇒ 357 let 〈upper_lower', addr'〉 ≝ upper_lower_addr' in 358 eq_upper_lower upper_lower upper_lower' ∧ eq_bv … addr addr' 355 359 | _ ⇒ false 356 360 ] … … 358 362 359 363 lemma eq_accumulator_address_map_entry_true_to_eq: 360 ∀left: accumulator_address_map_entry.361 ∀right: accumulator_address_map_entry.364 ∀left: option address_entry. 365 ∀right: option address_entry. 362 366 eq_accumulator_address_map_entry left right = true → left = right. 363 367 #left #right cases left cases right … … 365 369 #_ % 366 370 |2,3: 367 #upper_lower#word normalize #absurd destruct(absurd)371 * * #word normalize #absurd destruct(absurd) 368 372 |4: 369 #upper_lower #word #upper_lower' #word' normalize 370 cases upper_lower' normalize nodelta 371 cases upper_lower normalize 373 * * #word * * #word' 372 374 [2,3: 373 #absurd destruct(absurd)375 #absurd normalize in absurd; destruct(absurd) 374 376 ] 375 change with (eq_bv 16 ?? = true → ?) 376 #relevant lapply (eq_bv_eq … relevant) 377 #word_refl >word_refl % 377 normalize change with (eq_bv 8 ?? = true → ?) 378 #relevant >(eq_bv_eq … relevant) % 378 379 ] 379 380 qed. … … 403 404 404 405 lemma eq_accumulator_address_map_entry_false_to_neq: 405 ∀left: accumulator_address_map_entry.406 ∀right: accumulator_address_map_entry.406 ∀left: option address_entry. 407 ∀right: option address_entry. 407 408 eq_accumulator_address_map_entry left right = false → left ≠ right. 408 409 #left #right cases left cases right … … 410 411 normalize #absurd destruct(absurd) 411 412 |2,3: 412 #upper_lower #word normalize #_ 413 @nmk #absurd destruct(absurd) 413 * * #word normalize #_ % #absurd destruct(absurd) 414 414 |4: 415 #upper_lower #word #upper_lower' #word' normalize 416 cases upper_lower' normalize nodelta 417 cases upper_lower normalize nodelta 415 * * #word * * #word' normalize 418 416 [2,3: 419 #_ @nmk#absurd destruct(absurd)417 #_ % #absurd destruct(absurd) 420 418 ] 421 419 change with (eq_bv ??? = false → ?) 422 #eq_bv_false_assm lapply (eq_bv_false_to_neq … eq_bv_false_assm)423 #word_neq_assm @nmk#address_eq_assm cases word_neq_assm420 #eq_bv_false_assm lapply (eq_bv_false_to_neq … eq_bv_false_assm) 421 #word_neq_assm % @Some_Some_elim #address_eq_assm cases word_neq_assm 424 422 #word_eq_assm @word_eq_assm destruct(address_eq_assm) % 425 423 ] 426 qed. 424 qed. 427 425 428 426 (* XXX: changed this type. Bool specifies whether byte is first or second … … 431 429 A. 432 430 *) 433 definition internal_pseudo_address_map ≝ list (Byte × (upper_lower × Word)) × accumulator_address_map_entry. 431 definition internal_pseudo_address_map ≝ 432 (* low, high, acc *) 433 (BitVectorTrie address_entry 7) × (BitVectorTrie address_entry 7) × (option address_entry). 434 434 435 435 include alias "ASM/BitVectorTrie.ma". … … 437 437 include "common/AssocList.ma". 438 438 439 axiom low_internal_ram_of_pseudo_low_internal_ram: 440 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 441 442 axiom high_internal_ram_of_pseudo_high_internal_ram: 443 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 444 439 axiom bvt_map2: 440 ∀A, B, C: Type[0]. 441 ∀n: nat. 442 ∀bvt_1: BitVectorTrie A n. 443 ∀bvt_2: BitVectorTrie B n. 444 ∀f: ∀a: option A. ∀b: option B. option C. 445 BitVectorTrie C n. 446 447 axiom is_in_domain: 448 ∀A: Type[0]. 449 ∀n: nat. 450 ∀bvt: BitVectorTrie A n. 451 ∀b: BitVector n. 452 Prop. 453 454 axiom bvt_map2_function_extensionality: 455 ∀A, B, C: Type[0]. 456 ∀n: nat. 457 ∀bvt_1: BitVectorTrie A n. 458 ∀bvt_2, bvt_2': BitVectorTrie B n. 459 ∀f: ∀a: option A. ∀b: option B. option C. 460 (∀addr. 461 is_in_domain … bvt_1 addr ∨ is_in_domain … bvt_2 addr ∨ is_in_domain … bvt_2' addr → 462 f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2) = f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2')) → 463 bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f. 464 465 definition internal_ram_of_pseudo_internal_ram: 466 ∀sigma: Word → Word. 467 ∀ram: BitVectorTrie Byte 7. 468 ∀map: BitVectorTrie address_entry 7. 469 BitVectorTrie Byte 7 ≝ 470 λsigma, ram, map. 471 bvt_map2 ??? ? ram map (λv. λul_addr. 472 match 473 match ul_addr with 474 [ None ⇒ v 475 | Some ul_addr' ⇒ 476 let 〈ul, addr〉 ≝ ul_addr' in 477 let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in 478 match ul with 479 [ upper ⇒ 480 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in 481 Some … high 482 | lower ⇒ 483 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in 484 Some … low 485 ] 486 ] with 487 [ None ⇒ None … 488 | Some v ⇒ 489 if eq_bv … v (zero …) then 490 None … 491 else 492 Some … v 493 ]). 494 495 definition low_internal_ram_of_pseudo_low_internal_ram: 496 ∀M: internal_pseudo_address_map. 497 ∀sigma: Word → Word. 498 ∀ram: BitVectorTrie Byte 7. 499 BitVectorTrie Byte 7 ≝ 500 λM, sigma, ram. 501 let 〈low, high, accA〉 ≝ M in 502 internal_ram_of_pseudo_internal_ram sigma ram low. 503 504 definition high_internal_ram_of_pseudo_high_internal_ram: 505 ∀M: internal_pseudo_address_map. 506 ∀sigma: Word → Word. 507 ∀ram: BitVectorTrie Byte 7. 508 BitVectorTrie Byte 7 ≝ 509 λM, sigma, ram. 510 let 〈low, high, accA〉 ≝ M in 511 internal_ram_of_pseudo_internal_ram sigma ram high. 512 513 (* 445 514 axiom low_internal_ram_of_pseudo_internal_ram_hit: 446 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.447 assoc_list_lookup?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉 →448 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in515 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7. 516 lookup_opt ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉 → 517 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in 449 518 let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in 450 519 let bl ≝ lookup ? 7 addr ram (zero 8) in 451 520 let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in 452 let 〈plower, phigher〉 ≝ vsplit ? 8 8 ( \fst (sigma points_to)) in521 let 〈plower, phigher〉 ≝ vsplit ? 8 8 (sigma points_to) in 453 522 if eq_upper_lower upper_lower upper then 454 523 (pbl = higher) ∧ (bl = phigher) 455 524 else 456 525 (pbl = lower) ∧ (bl = plower). 526 *) 457 527 458 528 (* changed from add to sub *) 459 529 axiom low_internal_ram_of_pseudo_internal_ram_miss: 460 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7. 461 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 462 assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false → 463 lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?). 464 465 definition addressing_mode_ok ≝ 530 ∀T.∀M:internal_pseudo_address_map.∀sigma. ∀cm.∀s:PreStatus T cm.∀addr:BitVector 7. 531 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in 532 lookup_opt … addr (\fst (\fst M)) = None … → 533 lookup … addr ram (zero …) = lookup … addr (low_internal_ram … s) (zero ?). 534 535 definition exists: 536 ∀A: Type[0]. 537 ∀n: nat. 538 ∀v: BitVector n. 539 ∀bvt: BitVectorTrie A n. 540 bool ≝ 541 λA, n, v, bvt. 542 match lookup_opt … v bvt with 543 [ None ⇒ false 544 | _ ⇒ true 545 ]. 546 547 definition data_or_address ≝ 466 548 λT. 467 549 λM: internal_pseudo_address_map. … … 469 551 λs: PreStatus T cm. 470 552 λaddr: addressing_mode. 471 match addr with 553 let 〈low, high, accA〉 ≝ M in 554 match addr return λx. option (option address_entry) with 472 555 [ DIRECT d ⇒ 473 if eq_bv … d (bitvector_of_nat … 224) then 474 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) ∧ eq_accumulator_address_map_entry (\snd M) data 475 else 476 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 556 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in 557 match head' … hd with 558 [ true ⇒ 559 if eq_bv … d (bitvector_of_nat … 224) then 560 Some … accA 561 else 562 Some … (None …) 563 | false ⇒ Some … (lookup_opt … seven_bits low) 564 ] 477 565 | INDIRECT i ⇒ 478 566 let d ≝ get_register … s [[false;false;i]] in 479 567 let address ≝ bit_address_of_register … s [[false;false;i]] in 480 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧ 481 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 568 if ¬exists … address low then 569 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in 570 if head' … 0 bit_one then 571 Some … (lookup_opt … seven_bits high) 572 else 573 Some … (lookup_opt … seven_bits low) 574 else 575 None ? 482 576 | EXT_INDIRECT e ⇒ 483 577 let address ≝ bit_address_of_register … s [[false;false;e]] in 484 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) 578 if ¬exists … address low then 579 Some … (None …) 580 else 581 None ? 485 582 | REGISTER r ⇒ 486 583 let address ≝ bit_address_of_register … s r in 487 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) 488 | ACC_A ⇒ 489 match \snd M with 490 [ data ⇒ true 491 | _ ⇒ false 492 ] 493 | ACC_B ⇒ true 494 | DPTR ⇒ true 495 | DATA _ ⇒ true 496 | DATA16 _ ⇒ true 497 | ACC_DPTR ⇒ true 498 | ACC_PC ⇒ true 499 | EXT_INDIRECT_DPTR ⇒ true 500 | INDIRECT_DPTR ⇒ true 501 | CARRY ⇒ true 584 Some … (lookup_opt … address low) 585 | ACC_A ⇒ Some … accA 586 | ACC_B ⇒ Some … (None …) 587 | DPTR ⇒ Some … (None …) 588 | DATA _ ⇒ Some … (None …) 589 | DATA16 _ ⇒ Some … (None …) 590 | ACC_DPTR ⇒ Some … (None …) 591 | ACC_PC ⇒ Some … (None …) 592 | EXT_INDIRECT_DPTR ⇒ Some … (None …) 593 | INDIRECT_DPTR ⇒ Some … (None …) 594 | CARRY ⇒ Some … (None …) 502 595 | BIT_ADDR b ⇒ 503 596 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in 597 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 504 598 if head' bool 0 bit_one then 505 eq_accumulator_address_map_entry (\snd M) data 599 if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *) 600 Some … accA 601 else 602 Some … (None …) 506 603 else 507 let address ≝ nat_of_bitvector 7 seven_bits in 508 let address' ≝ bitvector_of_nat 7 ((address÷8)+32) in 509 ¬assoc_list_exists ?? (false:::address') (eq_bv 8) (\fst M) 510 | N_BIT_ADDR b ⇒ ¬true (* TO BE COMPLETED *) 511 | RELATIVE _ ⇒ true 512 | ADDR11 _ ⇒ true 513 | ADDR16 _ ⇒ true 604 let address' ≝ [[true; false; false]]@@four_bits in 605 Some … (lookup_opt … address' low) 606 | N_BIT_ADDR b ⇒ 607 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in 608 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 609 if head' bool 0 bit_one then 610 if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *) 611 Some … accA 612 else 613 Some … (None …) 614 else 615 let address' ≝ [[true; false; false]]@@four_bits in 616 Some … (lookup_opt … address' low) 617 | RELATIVE _ ⇒ Some … (None …) 618 | ADDR11 _ ⇒ Some … (None …) 619 | ADDR16 _ ⇒ Some … (None …) 514 620 ]. 621 622 definition assert_data ≝ 623 λT. 624 λM: internal_pseudo_address_map. 625 λcm. 626 λs: PreStatus T cm. 627 λaddr: addressing_mode. 628 match data_or_address T M cm s addr with 629 [ None ⇒ false 630 | Some s ⇒ 631 match s with 632 [ None ⇒ true 633 | _ ⇒ false 634 ] 635 ]. 636 637 definition insert_into_internal_ram: 638 ∀addr: Byte. 639 ∀v: address_entry. 640 ∀M: internal_pseudo_address_map. 641 internal_pseudo_address_map ≝ 642 λaddr, v, M. 643 let 〈low, high, accA〉 ≝ M in 644 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in 645 if head' … bit_one then 646 〈insert … seven_bits v low, high, accA〉 647 else 648 〈low, insert … seven_bits v high, accA〉. 649 650 axiom delete: 651 ∀A: Type[0]. 652 ∀n: nat. 653 ∀b: BitVector n. 654 BitVectorTrie A n → BitVectorTrie A n. 655 656 definition delete_from_internal_ram: 657 ∀addr: Byte. 658 ∀M: internal_pseudo_address_map. 659 internal_pseudo_address_map ≝ 660 λaddr, M. 661 let 〈low, high, accA〉 ≝ M in 662 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in 663 if head' … bit_one then 664 〈delete … seven_bits low, high, accA〉 665 else 666 〈low, delete … seven_bits high, accA〉. 667 668 definition overwrite_or_delete_from_internal_ram: 669 ∀addr: Byte. 670 ∀v: option address_entry. 671 ∀M: internal_pseudo_address_map. 672 internal_pseudo_address_map ≝ 673 λaddr, v, M. 674 let 〈low, high, accA〉 ≝ M in 675 match v with 676 [ None ⇒ delete_from_internal_ram addr M 677 | Some v' ⇒ insert_into_internal_ram addr v' M 678 ]. 679 680 definition lookup_from_internal_ram: 681 ∀addr: Byte. 682 ∀M: internal_pseudo_address_map. 683 option address_entry ≝ 684 λaddr, M. 685 let 〈low, high, accA〉 ≝ M in 686 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in 687 if head' … bit_one then 688 lookup_opt … seven_bits high 689 else 690 lookup_opt … seven_bits low. 515 691 516 692 definition next_internal_pseudo_address_map0 ≝ … … 521 697 λM: internal_pseudo_address_map. 522 698 λs: PreStatus T cm. 699 let 〈low, high, accA〉 ≝ M in 523 700 match fetched with 524 701 [ Comment _ ⇒ Some ? M … … 527 704 | Call a ⇒ 528 705 let a' ≝ addr_of a s in 529 let 〈 callM, accM〉 ≝ Min530 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, a'〉〉::531 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈upper, a'〉〉::callM, accM〉706 let 〈upA, lowA〉 ≝ vsplit bool 8 8 a' in 707 Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) 〈lower, upA〉 708 (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) 〈upper, lowA〉 M)) 532 709 | Mov _ _ ⇒ Some … M 533 710 | Instruction instr ⇒ 534 711 match instr return λx. option internal_pseudo_address_map with 535 712 [ ADD addr1 addr2 ⇒ 536 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then713 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 537 714 Some ? M 538 715 else 539 716 None ? 540 717 | ADDC addr1 addr2 ⇒ 541 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then718 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 542 719 Some ? M 543 720 else 544 721 None ? 545 722 | SUBB addr1 addr2 ⇒ 546 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then723 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 547 724 Some ? M 548 725 else 549 726 None ? 550 727 | INC addr1 ⇒ 551 if a ddressing_mode_okT M ? s addr1 then728 if assert_data T M ? s addr1 then 552 729 Some ? M 553 730 else 554 731 None ? 555 732 | DEC addr1 ⇒ 556 if a ddressing_mode_okT M … s addr1 then733 if assert_data T M … s addr1 then 557 734 Some ? M 558 735 else 559 736 None ? 560 737 | MUL addr1 addr2 ⇒ 561 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then738 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 562 739 Some ? M 563 740 else 564 741 None ? 565 742 | DIV addr1 addr2 ⇒ 566 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then743 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 567 744 Some ? M 568 745 else 569 746 None ? 570 747 | DA addr1 ⇒ 571 if a ddressing_mode_okT M … s addr1 then748 if assert_data T M … s addr1 then 572 749 Some ? M 573 750 else … … 584 761 [ inl l ⇒ 585 762 let 〈left, right〉 ≝ l in 586 if a ddressing_mode_ok T M … s left ∧ addressing_mode_okT M … s right then763 if assert_data T M … s left ∧ assert_data T M … s right then 587 764 Some ? M 588 else if ¬(a ddressing_mode_ok T M … s left) ∧ ¬(addressing_mode_okT M … s right) then765 else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then 589 766 Some ? M 590 767 else … … 592 769 | inr r ⇒ 593 770 let 〈left, right〉 ≝ r in 594 if a ddressing_mode_ok T M … s left ∧ addressing_mode_okT M … s right then771 if assert_data T M … s left ∧ assert_data T M … s right then 595 772 Some ? M 596 else if ¬(a ddressing_mode_ok T M … s left) ∧ ¬(addressing_mode_okT M … s right) then773 else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then 597 774 Some ? M 598 775 else … … 600 777 ] 601 778 | DJNZ addr1 addr2 ⇒ 602 if a ddressing_mode_okT M … s addr1 then779 if assert_data T M … s addr1 then 603 780 Some ? M 604 781 else 605 782 None ? 606 783 | CLR addr1 ⇒ 607 if a ddressing_mode_okT M … s addr1 then784 if assert_data T M … s addr1 then 608 785 Some ? M 609 786 else 610 787 None ? 611 788 | CPL addr1 ⇒ 612 if a ddressing_mode_okT M … s addr1 then789 if assert_data T M … s addr1 then 613 790 Some ? M 614 791 else 615 792 None ? 616 793 | RL addr1 ⇒ 617 if a ddressing_mode_okT M … s addr1 then794 if assert_data T M … s addr1 then 618 795 Some ? M 619 796 else 620 797 None ? 621 798 | RLC addr1 ⇒ 622 if a ddressing_mode_okT M … s addr1 then799 if assert_data T M … s addr1 then 623 800 Some ? M 624 801 else 625 802 None ? 626 803 | RR addr1 ⇒ 627 if a ddressing_mode_okT M … s addr1 then804 if assert_data T M … s addr1 then 628 805 Some ? M 629 806 else 630 807 None ? 631 808 | RRC addr1 ⇒ 632 if a ddressing_mode_okT M … s addr1 then809 if assert_data T M … s addr1 then 633 810 Some ? M 634 811 else 635 812 None ? 636 813 | SWAP addr1 ⇒ 637 if a ddressing_mode_okT M … s addr1 then814 if assert_data T M … s addr1 then 638 815 Some ? M 639 816 else 640 817 None ? 641 818 | SETB addr1 ⇒ 642 if a ddressing_mode_okT M … s addr1 then819 if assert_data T M … s addr1 then 643 820 Some ? M 644 821 else … … 646 823 (* XXX: need to track addresses pushed and popped off the stack? *) 647 824 | PUSH addr1 ⇒ 648 let 〈callM, accM〉 ≝ M in649 825 match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with 650 826 [ DIRECT d ⇒ λproof. 651 let extended ≝ pad 8 8 d in 652 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, extended〉〉::callM, accM〉 827 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in 828 if head' … bit_one then 829 if eq_bv … seven_bits (bitvector_of_nat … 224) then 830 Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) accA M) 831 else 832 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M) 833 else 834 match lookup_from_internal_ram … d M with 835 [ None ⇒ 836 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M) 837 | Some ul_addr ⇒ 838 Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) ul_addr M) 839 ] 653 840 | _ ⇒ λother: False. ⊥ 654 841 ] (subaddressing_modein … addr1) 655 | POP addr1 ⇒ Some … M 842 | POP addr1 ⇒ 843 let sp ≝ get_8051_sfr ?? s SFR_SP in 844 match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with 845 [ DIRECT d ⇒ λproof. 846 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in 847 if head' … bit_one then 848 if eq_bv … d (bitvector_of_nat … 224) then 849 Some … 〈low, high, lookup_from_internal_ram … sp M〉 850 else 851 match lookup_from_internal_ram sp M with 852 [ None ⇒ Some ? M 853 | _ ⇒ None ? 854 ] 855 else 856 Some … (overwrite_or_delete_from_internal_ram d (lookup_from_internal_ram … sp M) M) 857 | _ ⇒ λother: False. ⊥ 858 ] (subaddressing_modein … addr1) 656 859 | XCH addr1 addr2 ⇒ 657 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then860 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 658 861 Some ? M 659 862 else 660 863 None ? 661 864 | XCHD addr1 addr2 ⇒ 662 if a ddressing_mode_ok T M … s addr1 ∧ addressing_mode_okT M … s addr2 then865 if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then 663 866 Some ? M 664 867 else 665 868 None ? 666 869 | RET ⇒ 667 let 〈callM, accM〉 ≝ M in 668 let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in 669 let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in 670 if sp_plus_1 ∧ sp_plus_2 then 671 Some … M 672 else 673 None ? 870 let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in 871 let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in 872 match lookup_from_internal_ram sp_minus_1 M with 873 [ None ⇒ None … 874 | Some low_addr_high ⇒ 875 match lookup_from_internal_ram sp_minus_2 M with 876 [ None ⇒ None … 877 | Some high_addr_low ⇒ 878 let 〈low, addr_high〉 ≝ low_addr_high in 879 let 〈high, addr_low〉 ≝ high_addr_low in 880 let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in 881 let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in 882 if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then 883 Some ? M 884 else 885 None ? 886 ] 887 ] 674 888 | RETI ⇒ 675 let 〈callM, accM〉 ≝ M in 676 let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in 677 let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in 678 if sp_plus_1 ∧ sp_plus_2 then 679 Some … M 680 else 681 None ? 889 let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in 890 let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in 891 match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M with 892 [ None ⇒ None … 893 | Some low_addr_high ⇒ 894 match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) M with 895 [ None ⇒ None … 896 | Some high_addr_low ⇒ 897 let 〈low, addr_high〉 ≝ low_addr_high in 898 let 〈high, addr_low〉 ≝ high_addr_low in 899 let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in 900 let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in 901 if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then 902 Some ? M 903 else 904 None ? 905 ] 906 ] 682 907 | NOP ⇒ Some … M 683 908 | MOVX addr1 ⇒ 684 909 match addr1 with 685 910 [ inl l ⇒ 686 let 〈acc_a, others〉 ≝ l in 687 let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in 688 let others_ok ≝ addressing_mode_ok T M … s others in 689 if acc_a_ok ∧ others_ok then 690 Some ? M 691 else 692 None ? 911 Some ? 〈low, high, None …〉 693 912 | inr r ⇒ 694 913 let 〈others, acc_a〉 ≝ r in 695 let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in 696 let others_ok ≝ addressing_mode_ok T M … s others in 697 if others_ok ∧ acc_a_ok then 914 if assert_data T M … s acc_a then 698 915 Some ? M 699 916 else … … 704 921 [ inl l ⇒ 705 922 let 〈acc_a, others〉 ≝ l in 706 let acc_a_ok ≝ a ddressing_mode_okT M … s acc_a in707 let others_ok ≝ a ddressing_mode_okT M … s others in923 let acc_a_ok ≝ assert_data T M … s acc_a in 924 let others_ok ≝ assert_data T M … s others in 708 925 if acc_a_ok ∧ others_ok then 709 926 Some ? M … … 712 929 | inr r ⇒ 713 930 let 〈direct, others〉 ≝ r in 714 let direct_ok ≝ a ddressing_mode_okT M … s direct in715 let others_ok ≝ a ddressing_mode_okT M … s others in931 let direct_ok ≝ assert_data T M … s direct in 932 let others_ok ≝ assert_data T M … s others in 716 933 if direct_ok ∧ others_ok then 717 934 Some ? M … … 725 942 [ inl l ⇒ 726 943 let 〈acc_a, others〉 ≝ l in 727 let acc_a_ok ≝ a ddressing_mode_okT M … s acc_a in728 let others_ok ≝ a ddressing_mode_okT M … s others in944 let acc_a_ok ≝ assert_data T M … s acc_a in 945 let others_ok ≝ assert_data T M … s others in 729 946 if acc_a_ok ∧ others_ok then 730 947 Some ? M … … 733 950 | inr r ⇒ 734 951 let 〈direct, others〉 ≝ r in 735 let direct_ok ≝ a ddressing_mode_okT M … s direct in736 let others_ok ≝ a ddressing_mode_okT M … s others in952 let direct_ok ≝ assert_data T M … s direct in 953 let others_ok ≝ assert_data T M … s others in 737 954 if direct_ok ∧ others_ok then 738 955 Some ? M … … 742 959 | inr r ⇒ 743 960 let 〈carry, others〉 ≝ r in 744 let carry_ok ≝ a ddressing_mode_okT M … s carry in745 let others_ok ≝ a ddressing_mode_okT M … s others in961 let carry_ok ≝ assert_data T M … s carry in 962 let others_ok ≝ assert_data T M … s others in 746 963 if carry_ok ∧ others_ok then 747 964 Some ? M … … 755 972 [ inl l ⇒ 756 973 let 〈acc_a, others〉 ≝ l in 757 let acc_a_ok ≝ a ddressing_mode_okT M … s acc_a in758 let others_ok ≝ a ddressing_mode_okT M … s others in974 let acc_a_ok ≝ assert_data T M … s acc_a in 975 let others_ok ≝ assert_data T M … s others in 759 976 if acc_a_ok ∧ others_ok then 760 977 Some ? M … … 763 980 | inr r ⇒ 764 981 let 〈direct, others〉 ≝ r in 765 let direct_ok ≝ a ddressing_mode_okT M … s direct in766 let others_ok ≝ a ddressing_mode_okT M … s others in982 let direct_ok ≝ assert_data T M … s direct in 983 let others_ok ≝ assert_data T M … s others in 767 984 if direct_ok ∧ others_ok then 768 985 Some ? M … … 772 989 | inr r ⇒ 773 990 let 〈carry, others〉 ≝ r in 774 let carry_ok ≝ a ddressing_mode_okT M … s carry in775 let others_ok ≝ a ddressing_mode_okT M … s others in991 let carry_ok ≝ assert_data T M … s carry in 992 let others_ok ≝ assert_data T M … s others in 776 993 if carry_ok ∧ others_ok then 777 994 Some ? M … … 780 997 ] 781 998 | MOV addr1 ⇒ 999 (* XXX: wrong *) 782 1000 match addr1 with 783 1001 [ inl l ⇒ … … 791 1009 [ inl l'''' ⇒ 792 1010 let 〈acc_a, others〉 ≝ l'''' in 793 if addressing_mode_ok T M … s acc_a ∧ addressing_mode_ok T M … s others then 794 Some ? M 795 else 796 None ? 1011 match data_or_address T M … s others with 1012 [ None ⇒ None ? 1013 | Some s ⇒ 1014 Some … 〈low, high, s〉 1015 ] 797 1016 | inr r ⇒ 798 1017 let 〈others, others'〉 ≝ r in 799 if addressing_mode_ok T M … s others ∧ addressing_mode_ok T M … s others' then 800 Some ? M 801 else 802 None ? 1018 let address ≝ 1019 match others return λx. bool_to_Prop (is_in … [[ registr; indirect ]] x) → ? with 1020 [ REGISTER r ⇒ λproof. false:::bit_address_of_register … s r 1021 | INDIRECT i ⇒ λproof. get_register … s [[false; false; i]] 1022 | _ ⇒ λother: False. ⊥ 1023 ] (subaddressing_modein … others) 1024 in 1025 match data_or_address T M … s others' with 1026 [ None ⇒ None ? 1027 | Some s ⇒ 1028 Some … (overwrite_or_delete_from_internal_ram address s M) 1029 ] 803 1030 ] 804 1031 | inr r ⇒ 805 let 〈direct, others〉 ≝ r in 806 if addressing_mode_ok T M … s direct ∧ addressing_mode_ok T M … s others then 807 Some ? M 808 else 809 None ? 1032 let 〈direct', others〉 ≝ r in 1033 match direct' return λx. bool_to_Prop (is_in … [[direct]] x) → ? with 1034 [ DIRECT d ⇒ λproof. 1035 match data_or_address T M … s others with 1036 [ None ⇒ None ? 1037 | Some s' ⇒ 1038 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in 1039 if head' … bit_one then 1040 if eq_bv … d (bitvector_of_nat … 224) then 1041 Some … 〈low, high, s'〉 1042 else 1043 match s' with 1044 [ None ⇒ Some ? M 1045 | Some s'' ⇒ None ? 1046 ] 1047 else 1048 Some … (overwrite_or_delete_from_internal_ram d s' M) 1049 ] 1050 | _ ⇒ λother: False. ⊥ 1051 ] (subaddressing_modein … direct') 810 1052 ] 811 | inr r ⇒ 812 let 〈dptr, data_16〉 ≝ r in 813 if addressing_mode_ok T M … s dptr ∧ addressing_mode_ok T M … s data_16 then 814 Some ? M 815 else 816 None ? 1053 | inr r ⇒ Some … M 817 1054 ] 818 1055 | inr r ⇒ 819 1056 let 〈carry, bit_addr〉 ≝ r in 820 if a ddressing_mode_ok T M … s carry ∧ addressing_mode_okT M … s bit_addr then1057 if assert_data T M … s bit_addr then 821 1058 Some ? M 822 1059 else … … 825 1062 | inr r ⇒ 826 1063 let 〈bit_addr, carry〉 ≝ r in 827 if a ddressing_mode_ok T M … s bit_addr ∧ addressing_mode_ok T M … s carrythen1064 if assert_data T M … s bit_addr then 828 1065 Some ? M 829 1066 else … … 858 1095 λsigma: Word → Word. 859 1096 match \snd M with 860 [ data⇒ sfrs861 | address upper_loweraddress ⇒1097 [ None ⇒ sfrs 1098 | Some upper_lower_address ⇒ 862 1099 let index ≝ sfr_8051_index SFR_ACC_A in 863 let 〈high, low〉 ≝ vsplit ? 8 8 (sigma address) in 1100 let acc_a ≝ get_index_v … sfrs index ? in 1101 let 〈upper_lower, address〉 ≝ upper_lower_address in 864 1102 if eq_upper_lower upper_lower upper then 865 set_index Byte 19 sfrs index high ? 1103 let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (acc_a@@address)) in 1104 set_index Byte 19 sfrs index high ? 866 1105 else 867 set_index Byte 19 sfrs index low ? 1106 let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (address@@acc_a)) in 1107 set_index Byte 19 sfrs index low ? 868 1108 ]. 869 1109 // … … 881 1121 let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in 882 1122 let pc ≝ sigma (program_counter … ps) in 883 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in884 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in1123 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … ps) in 1124 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M sigma (high_internal_ram … ps) in 885 1125 mk_PreStatus (BitVectorTrie Byte 16) 886 1126 cm … … 1206 1446 ∀arg: Byte. 1207 1447 ∀b: bool. 1208 a ddressing_mode_okm s (DIRECT arg) = true →1448 assert_data m s (DIRECT arg) = true → 1209 1449 get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) = 1210 1450 get_arg_8 ? s b (DIRECT arg). … … 1265 1505 get_arg_8 (internal_ram ...) (DIRECT arg) 1266 1506 1267 ((if a ddressing_mode_ok M ps ACC_A∧addressing_mode_okM ps (DIRECT ARG2)1507 ((if assert_data M ps ACC_A∧assert_data M ps (DIRECT ARG2) 1268 1508 then Some internal_pseudo_address_map M 1269 1509 else None internal_pseudo_address_map )
Note: See TracChangeset
for help on using the changeset viewer.