Changeset 883 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 3, 2011, 6:36:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r877 r883 439 439 ∀P. instruction_elim P = true → ∀i. P i = true. 440 440 441 definition eq_instruction ≝441 (*definition eq_instruction ≝ 442 442 λi, j: instruction. 443 true. 444 443 true.*) 444 axiom eq_instruction: instruction → instruction → bool. 445 445 let rec vect_member 446 446 (A: Type[0]) (n: nat) (eq: A → A → bool) … … 495 495 # A15 # A16 # A17 # A18 # A19 # X 496 496 cases X 497 # SUB 497 # SUB cases daemon ] qed.(* 498 498 cases SUB 499 499 [ # BYTE … … 577 577 cases (is_a hd (subaddressing_modeel y tl H)) whd // ] 578 578 qed. 579 579 *) 580 580 (* 581 581 lemma test: … … 590 590 ]*) 591 591 592 lemma BitVectorTrie_O: 593 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. 594 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)) 595 [ #w #_ %1 %[@w] % 596  #n #l #r #abs @⊥ // 597  #n #EQ %2 >EQ %] 598 qed. 599 600 lemma BitVectorTrie_Sn: 601 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). 602 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%) 603 [ #m #abs @⊥ // 604  #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // 605  #m #EQ %2 // ] 606 qed. 607 608 lemma lookup_prepare_trie_for_insertion_hit: 609 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n. 610 lookup … b (prepare_trie_for_insertion … b v) a = v. 611 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize // 612 qed. 613 614 lemma lookup_insert_hit: 615 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. 616 lookup … b (insert … b v t) a = v. 617 #A #a #v #n #b elim b b n // 618 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t) 619 [ * #l * #r #JMEQ >JMEQ cases hd normalize // 620  #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ] 621 qed. 622 623 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. 624 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // 625 #n #hd #tl #abs @⊥ // 626 qed. 627 628 lemma BitVector_Sn: ∀n.∀v:BitVector (S n). 629 ∃hd.∃tl.v ≃ VCons bool n hd tl. 630 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) 631 [ #abs @⊥ // 632  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 633 qed. 634 635 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 636 637 lemma lookup_prepare_trie_for_insertion_miss: 638 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n. 639 (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a. 640 #A #a #v #n #c elim c 641 [ #b >(BitVector_O … b) normalize #abs @⊥ // 642  #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 643 cases hd cases hd' normalize 644 [2,3: #_ cases tl' // 645 *: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]] 646 qed. 647 648 lemma lookup_insert_miss: 649 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. 650 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. 651 #A #a #v #n #c elim c c n 652 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // 653  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 654 #t cases(BitVectorTrie_Sn … t) 655 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 656 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 657  #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 658 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize 659 [3,4: cases tl' //  *: @lookup_prepare_trie_for_insertion_miss //]]] 660 qed. 661 662 definition load_code_memory_aux ≝ 663 fold_left_i_aux … ( 664 λi, mem, v. 665 insert … (bitvector_of_nat … i) v mem) (Stub Byte 16). 666 667 axiom split_elim: 668 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop. 669 (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v). 670 671 axiom half_add_SO: 672 ∀pc. 673 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc). 674 675 axiom not_eqvb_S: 676 ∀pc. 677 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))). 678 679 axiom not_eqvb_SS: 680 ∀pc. 681 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))). 682 592 683 lemma test: 593 ∀ i.594 595 let code_memory ≝ load_code_memory assembled in596 let fetched ≝ fetch code_memory ?in684 ∀pc,i. 685 (let assembled ≝ assembly1 i in 686 let code_memory ≝ load_code_memory_aux pc assembled in 687 let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in 597 688 let 〈instr_pc, ticks〉 ≝ fetched in 598 689 eq_instruction (\fst instr_pc)) i = true. 599 [ #i cases i #arg try #arg2 whd in ⊢ (??%?) 600 [2: whd in ⊢ (??(match ? (? %) ?with [ _ ⇒ ?] ?)?) 690 #pc #i cases i #arg try #arg2 whd in ⊢ (??%?) 691 [2,4: @(list_addressing_mode_tags_elim_prop ? [[addr16]] ???????????????????? arg) whd try % #XX 692 whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) 601 693 cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP; 602 whd in ⊢ (??(match ? (? %) ? with [ _ ⇒ ?] ?)?) 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; 697 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 698 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 699 >lookup_insert_miss // 700 >lookup_insert_miss // 701 >lookup_insert_hit 702 whd in ⊢ (??(match % with [ _ ⇒ ?] ?)?) 703 whd in ⊢ (??%?) whd in ⊢ (??(?%?)?) 704 >half_add_SO >half_add_SO 705 >lookup_insert_miss [2,4: @not_eqvb_S] 706 >lookup_insert_hit >lookup_insert_hit] 707  708 709 710 603 711 604 712 [2: #addr whd in ⊢ (??%?) … … 698 806 qed. 699 807 700 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].701 702 808 lemma index_of_internal_None: ∀i,id,instr_list,n. 703 809 occurs_exactly_once id (instr_list@[〈None …,i〉]) → … … 733 839 → False. 734 840 735 lemma BitVectorTrie_O:736 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.737 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))738 [ #w #_ %1 %[@w] %739  #n #l #r #abs @⊥ //740  #n #EQ %2 >EQ %]741 qed.742 743 lemma BitVectorTrie_Sn:744 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).745 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)746 [ #m #abs @⊥ //747  #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //748  #m #EQ %2 // ]749 qed.750 751 lemma lookup_prepare_trie_for_insertion_hit:752 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.753 lookup … b (prepare_trie_for_insertion … b v) a = v.754 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //755 qed.756 757 lemma lookup_insert_hit:758 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.759 lookup … b (insert … b v t) a = v.760 #A #a #v #n #b elim b b n //761 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)762 [ * #l * #r #JMEQ >JMEQ cases hd normalize //763  #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]764 qed.765 766 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.767 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //768 #n #hd #tl #abs @⊥ //769 qed.770 771 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).772 ∃hd.∃tl.v ≃ VCons bool n hd tl.773 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))774 [ #abs @⊥ //775  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]776 qed.777 778 lemma lookup_prepare_trie_for_insertion_miss:779 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.780 (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.781 #A #a #v #n #c elim c782 [ #b >(BitVector_O … b) normalize #abs @⊥ //783  #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ784 cases hd cases hd' normalize785 [2,3: #_ cases tl' //786 *: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]787 qed.788 789 lemma lookup_insert_miss:790 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.791 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.792 #A #a #v #n #c elim c c n793 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //794  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ795 #t cases(BitVectorTrie_Sn … t)796 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;797 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //798  #JMEQ >JMEQ cases hd cases hd' #H normalize in H;799 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize800 [3,4: cases tl' //  *: @lookup_prepare_trie_for_insertion_miss //]]]801 qed.802 841 803 842 definition build_maps' ≝
Note: See TracChangeset
for help on using the changeset viewer.