- Timestamp:
- Jun 4, 2011, 6:16:08 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r883 r884 455 455 (n: nat) 456 456 (l: Vector addressing_mode_tag (S n)) 457 (P: addressing_mode → Prop) on l: 457 on l: 458 ∀P: l → Prop. 458 459 ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a. 459 460 ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a. … … 465 466 match y with 466 467 [ O ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True 467 | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n. 468 | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop. 468 469 ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True. 469 470 ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True. … … 489 490 [ VEmpty ⇒ λAbsurd. ⊥ 490 491 | VCons len hd tl ⇒ λProof. ? 491 ] (refl ? (S n)). 492 ] (refl ? (S n)). cases daemon. qed. (* 492 493 [ destruct(Absurd) 493 494 | # A1 # A2 # A3 # A4 # A5 # A6 # A7 … … 495 496 # A15 # A16 # A17 # A18 # A19 # X 496 497 cases X 497 # SUB cases daemon ] qed. (*498 # SUB cases daemon ] qed. 498 499 cases SUB 499 500 [ # BYTE … … 681 682 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))). 682 683 684 axiom bitvector_elim_complete: 685 ∀n,P. bitvector_elim n P = true → ∀bv. P bv. 686 687 lemma bitvector_elim_complete': 688 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true. 689 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv 690 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ // 691 qed. 692 693 lemma andb_elim': 694 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true. 695 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize // 696 qed. 697 683 698 lemma test: 684 699 ∀pc,i. … … 689 704 eq_instruction (\fst instr_pc)) i = true. 690 705 #pc #i cases i #arg try #arg2 whd in ⊢ (??%?) 691 [2,4: @(list_addressing_mode_tags_elim_prop ? [[addr16]] ????????????????????arg) whd try % #XX706 [2,4: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX 692 707 whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) 693 cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP; 694 whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) try cases PP normalize in XX; 695 [1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17: cases XX 696 |*:@split_elim #b1 #b2 #EQ >EQ -EQ; 708 @split_elim #b1 #b2 #EQ >EQ -EQ; 697 709 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 698 whd in ⊢ (??(match ? ?% with [ _ ⇒ ?] ?)?)699 >lookup_insert_miss //710 whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?) 711 >lookup_insert_miss try @not_eqvb_SS 700 712 >lookup_insert_miss // 701 713 >lookup_insert_hit 702 whd in ⊢ (??(match % with [ _ ⇒ ?] ?)?)703 714 whd in ⊢ (??%?) whd in ⊢ (??(?%?)?) 704 715 >half_add_SO >half_add_SO 705 >lookup_insert_miss [2,4: @not_eqvb_S] 706 >lookup_insert_hit >lookup_insert_hit] 707 | 708 716 >lookup_insert_miss try @not_eqvb_S 717 >lookup_insert_hit 718 >lookup_insert_hit 719 (* REFL MISSING *) 720 cases daemon 721 |1,3: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX 722 whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) 723 @split_elim #b1 #b2 #EQ >EQ -EQ; 724 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 725 whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?) 726 >lookup_insert_miss // 727 >lookup_insert_hit 728 generalize in match b1 @(bitvector_elim_complete') 729 @andb_elim' @andb_elim' @andb_elim' whd in ⊢ (??%?) 730 >half_add_SO >lookup_insert_hit normalize 731 (* FALSO!!! AJMP vs ACALL *) 732 733 734 whd in ⊢ (??%?) whd in ⊢ (??(match % with [ _ ⇒ % | _ ⇒ ?])?) 735 check andb_elim. 736 (λV.(let 〈instr_pc,ticks〉 ≝ 737 fetch0 738 (insert Byte 16 (bitvector_of_nat 16 (S pc)) b2 739 (insert Byte 16 (bitvector_of_nat 16 pc) 740 (V@@[[true; false; false; false; true]]) (Stub Byte 16))) 741 〈\snd (half_add 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 1)), 742 V@@[[true; false; false; false; true]]〉 in 743 eq_instruction (\fst instr_pc)) 744 (ACALL (ADDR11 (V@@b2)))) ?) 745 whd in ⊢ (??%?) whd in ⊢ (??(?%?)?) 746 >half_add_SO 747 709 748 710 749
Note: See TracChangeset
for help on using the changeset viewer.