Changeset 2483
 Timestamp:
 Nov 22, 2012, 5:05:55 PM (9 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/MemProperties.ma
r2468 r2483 105 105 (*  *) 106 106 107 (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the backend values are equal. *) 107 (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the backend values are equal. 108 * This is allright for switch removal but false for Clight to Cminor *) 108 109 definition load_sim ≝ 109 110 λ(m1 : mem).λ(m2 : mem). … … 279 280 #_ normalize nodelta 280 281 #H @H 282 qed. 283 284 lemma loadn_free_loadn : 285 ∀n,m,block,ptr,res. 286 loadn (free m block) ptr n = Some ? res → 287 loadn m ptr n = Some ? res. 288 #n elim n 289 [ 1: normalize // 290  2: #n' #Hind #m #block #ptr #res #Hloadn 291 whd in Hloadn:(??%?); 292 cases (some_inversion ????? Hloadn) Hloadn 293 #be * #Hbeloadv #Hloadn 294 cases (some_inversion ????? Hloadn) Hloadn 295 #res' * #Hloadn #Heq destruct (Heq) 296 whd in match (loadn ???); 297 >(beloadv_free_beloadv … Hbeloadv) normalize nodelta 298 >(Hind … Hloadn) normalize nodelta @refl 299 ] qed. 300 301 lemma load_value_of_type_free_load_value_of_type : 302 ∀ty,m,block,b,o,res. 303 load_value_of_type ty (free m block) b o = Some ? res → 304 load_value_of_type ty m b o = Some ? res. 305 #ty 306 cases ty 307 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 308  #structname #fieldspec  #unionname #fieldspec  #id ] 309 #m #block #b #o #res 310 whd in ⊢ ((??%?) → (??%?)); // #H 311 cases (some_inversion ????? H) #be * #Hloadn #Heq 312 >(loadn_free_loadn … Hloadn) 313 normalize nodelta assumption 281 314 qed. 282 315 … … 512 545 serious PITA to prove. *) 513 546 axiom shiftn_no_wrap : ∀i. i ≤ 8 → ∀ofs. shiftn ofs i ≠ ofs. 547 548 (* Some stuff bunding the size of what we can write in memory *) 549 550 (* for leb_elim, shadowed in positive.ma *) 551 definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop. 552 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim. 553 554 (*include alias "arithmetics/nat.ma".*) 555 556 lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. l ≤ i → nth_opt A i l = None ?. 557 #A #l elim l // 558 #hd #tl #H #i elim i 559 [ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/ 560  2: #i' #H' #Hle whd in match (nth_opt ???); @H lapply (monotonic_pred … Hle) // 561 ] qed. 562 563 (* In order to prove the lemma on store_value_of_type and load_value_of_type, 564 we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *) 565 lemma typesize_bounded : ∀ty. typesize ty ≤ 8. 566 * try // * try // qed. 567 568 (* Lifting bound on make_list *) 569 lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → make_list A elt sz ≤ bound. 570 #A #sz elim sz try // 571 #sz' #Hind #bound #elt #Hbound normalize 572 cases bound in Hbound; 573 [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/ 574  2: #bound' #Hbound' lapply (Hind bound' elt ?) 575 [ 1: @(monotonic_pred … Hbound') 576  2: /2 by le_S_S/ ] 577 ] qed. 578 579 lemma bytes_of_bitvector_bounded : 580 ∀sz,bv. bytes_of_bitvector (size_intsize sz) bv = size_intsize sz. 581 * #bv normalize 582 [ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 // 583  2: cases (vsplit ????) normalize nodelta #bv0 #bv1 584 cases (vsplit ????) normalize nodelta #bv2 #bv3 // 585  3: cases (vsplit ????) normalize nodelta #bv0 #bv1 586 cases (vsplit ????) normalize nodelta #bv2 #bv3 587 cases (vsplit ????) normalize nodelta #bv4 #bv5 588 cases (vsplit ????) normalize nodelta #bv6 #bv7 589 // 590 ] qed. 591 592 lemma map_bounded : 593 ∀A,B:Type[0]. ∀l:list A. ∀f. map A B f l = l. 594 #A #B #l elim l try // 595 qed. 596 597 598 lemma fe_to_be_values_bounded : 599 ∀ty,v. fe_to_be_values ty v ≤ 8. 600 #ty cases ty 601 [ 1: #sz #sg ] 602 #v whd in match (fe_to_be_values ??); 603 cases v normalize nodelta 604 [ 1,5: @makelist_bounded @typesize_bounded 605  2,6: * normalize nodelta #bv 606 >map_bounded >bytes_of_bitvector_bounded // 607  3,7: // 608  4,8: #ptr // ] 609 qed. 610 611 lemma fe_to_be_values_nonempty : ∀typ,v. ∃hd,tl. fe_to_be_values typ v = hd :: tl. 612 * 613 [ 2: * /3 by ex_intro/ * #i 614 [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize 615 lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq 616 <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/ 617  2: whd in match (fe_to_be_values ??); normalize nodelta normalize 618 lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq 619 <(vsplit_prod … Heq) normalize nodelta 620 lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq' 621 /3 by ex_intro/ 622  3: whd in match (fe_to_be_values ??); normalize nodelta normalize 623 lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq 624 <(vsplit_prod … Heq) normalize nodelta 625 lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq' 626 <(vsplit_prod … Heq') normalize nodelta 627 lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq'' 628 <(vsplit_prod … Heq'') normalize nodelta 629 lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq''' 630 /3 by ex_intro/ ] 631  1: #sz #sg * /3 by ex_intro/ * #i 632 [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize 633 lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq 634 <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/ 635  2: whd in match (fe_to_be_values ??); normalize nodelta normalize 636 lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq 637 <(vsplit_prod … Heq) normalize nodelta 638 lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq' 639 /3 by ex_intro/ 640  3: whd in match (fe_to_be_values ??); normalize nodelta normalize 641 lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq 642 <(vsplit_prod … Heq) normalize nodelta 643 lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq' 644 <(vsplit_prod … Heq') normalize nodelta 645 lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq'' 646 <(vsplit_prod … Heq'') normalize nodelta 647 lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq''' 648 /3 by ex_intro/ ] 649 ] qed. 650 514 651 515 652 (* /!\ TODO the following proof is extremely ugly and indirect. I expect it to be … … 601 738 ] qed. 602 739 740 (* Adapting the lemma above to (fe_to_be_values ty v) *) 741 lemma mem_bounds_invariant_after_storen_bis : 742 ∀ty,v,m,m',b,ofs. 743 storen m (mk_pointer b ofs) (fe_to_be_values ty v) = Some ? m' → 744 (nextblock m' = nextblock m ∧ 745 (∀b.low (blocks m' b) = low (blocks m b) ∧ 746 high (blocks m' b) = high (blocks m b)) ∧ 747 (∀index. index < fe_to_be_values ty v → 748 low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧ 749 Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧ 750 (∀index. index < (fe_to_be_values ty v) → 751 nth_opt ? index (fe_to_be_values ty v) = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧ 752 (∀o. (∀i. i < fe_to_be_values ty v → o ≠ shiftn ofs i) → 753 contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧ 754 (valid_pointer m (mk_pointer b ofs) = true)). 755 #ty #v #m #m' #b #ofs #Hstoren 756 lapply (mem_bounds_invariant_after_storen … Hstoren) 757 [ @fe_to_be_values_bounded ] 758 * * * * * #H1 #H2 #H3 #H4 #H5 #H6 @conj try @conj try @conj try @conj try @conj 759 try assumption @H6 760 cases (fe_to_be_values_nonempty ty v) #hd * #tl #H >H // 761 qed. 762 603 763 (* extension of [bestorev_to_valid_pointer] to storen *) 604 764 lemma storen_to_valid_pointer : … … 633 793 ] qed. 634 794 635 lemma fe_to_be_values_nonempty : ∀typ,v. ∃hd,tl. fe_to_be_values typ v = hd :: tl. 636 * 637 [ 2: * /3 by ex_intro/ * #i 638 [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize 639 lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq 640 <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/ 641  2: whd in match (fe_to_be_values ??); normalize nodelta normalize 642 lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq 643 <(vsplit_prod … Heq) normalize nodelta 644 lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq' 645 /3 by ex_intro/ 646  3: whd in match (fe_to_be_values ??); normalize nodelta normalize 647 lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq 648 <(vsplit_prod … Heq) normalize nodelta 649 lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq' 650 <(vsplit_prod … Heq') normalize nodelta 651 lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq'' 652 <(vsplit_prod … Heq'') normalize nodelta 653 lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq''' 654 /3 by ex_intro/ ] 655  1: #sz #sg * /3 by ex_intro/ * #i 656 [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize 657 lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq 658 <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/ 659  2: whd in match (fe_to_be_values ??); normalize nodelta normalize 660 lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq 661 <(vsplit_prod … Heq) normalize nodelta 662 lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq' 663 /3 by ex_intro/ 664  3: whd in match (fe_to_be_values ??); normalize nodelta normalize 665 lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq 666 <(vsplit_prod … Heq) normalize nodelta 667 lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq' 668 <(vsplit_prod … Heq') normalize nodelta 669 lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq'' 670 <(vsplit_prod … Heq'') normalize nodelta 671 lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq''' 672 /3 by ex_intro/ ] 673 ] qed. 795 674 796 675 797 lemma storen_to_valid_pointer_fe_to_be : … … 704 826 >(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl 705 827 qed. 828 829 lemma storen_loadn_nonempty : 830 ∀data,m,m',b,ofs. 831 data ≤ 8 → 832 storen m (mk_pointer b ofs) data = Some ? m' → 833 ∃result. loadn m' (mk_pointer b ofs) (data) = Some ? result ∧ result=data. 834 #data elim data 835 [ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ] 836 #hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren 837 lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * 838 #Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr 839 cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0 840 whd in match (loadn ???); 841 lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?); 842 whd in match (beloadv ??); 843 whd in match (low_bound ??); whd in match (high_bound ??); 844 >Hnext 845 cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true 846 normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh 847 cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta 848 [ 2: #Habsurd destruct ] >andb_lsimpl_true 849 #Hltb >Hltb normalize nodelta 850 cases (Hind … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ] 851 #tl' * #Hloadn >Hloadn #Htl' normalize nodelta 852 %{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl 853 normalize >Htl' @refl 854 qed. 855 706 856 707 857 lemma loadn_beloadv_ok : … … 733 883 ] qed. 734 884 735 lemma storen_loadn_nonempty : 736 ∀data,m,m',b,ofs. 737 data ≤ 8 → 738 storen m (mk_pointer b ofs) data = Some ? m' → 739 ∃result. loadn m' (mk_pointer b ofs) (data) = Some ? result ∧ result=data. 740 #data elim data 741 [ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ] 742 #hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren 743 lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * 744 #Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr 745 cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0 746 whd in match (loadn ???); 747 lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?); 748 whd in match (beloadv ??); 749 whd in match (low_bound ??); whd in match (high_bound ??); 750 >Hnext 751 cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true 752 normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh 753 cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta 754 [ 2: #Habsurd destruct ] >andb_lsimpl_true 755 #Hltb >Hltb normalize nodelta 756 cases (Hind … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ] 757 #tl' * #Hloadn >Hloadn #Htl' normalize nodelta 758 %{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl 759 normalize >Htl' @refl 760 qed. 761 762 (* for leb_elim, shadowed in positive.ma *) 763 definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop. 764 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim. 765 766 (*include alias "arithmetics/nat.ma".*) 767 768 lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. l ≤ i → nth_opt A i l = None ?. 769 #A #l elim l // 770 #hd #tl #H #i elim i 771 [ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/ 772  2: #i' #H' #Hle whd in match (nth_opt ???); @H lapply (monotonic_pred … Hle) // 773 ] qed. 885 774 886 775 887 lemma storen_loadn_ok : … … 798 910 >nth_miss // >nth_miss // 799 911 ] qed. 800 801 (* In order to prove the lemma on store_value_of_type and load_value_of_type, 802 we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *) 803 lemma typesize_bounded : ∀ty. typesize ty ≤ 8. 804 * try // * try // qed. 805 806 (* Lifting bound on make_list *) 807 lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → make_list A elt sz ≤ bound. 808 #A #sz elim sz try // 809 #sz' #Hind #bound #elt #Hbound normalize 810 cases bound in Hbound; 811 [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/ 812  2: #bound' #Hbound' lapply (Hind bound' elt ?) 813 [ 1: @(monotonic_pred … Hbound') 814  2: /2 by le_S_S/ ] 815 ] qed. 816 817 lemma bytes_of_bitvector_bounded : 818 ∀sz,bv. bytes_of_bitvector (size_intsize sz) bv = size_intsize sz. 819 * #bv normalize 820 [ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 // 821  2: cases (vsplit ????) normalize nodelta #bv0 #bv1 822 cases (vsplit ????) normalize nodelta #bv2 #bv3 // 823  3: cases (vsplit ????) normalize nodelta #bv0 #bv1 824 cases (vsplit ????) normalize nodelta #bv2 #bv3 825 cases (vsplit ????) normalize nodelta #bv4 #bv5 826 cases (vsplit ????) normalize nodelta #bv6 #bv7 827 // 828 ] qed. 829 830 lemma map_bounded : 831 ∀A,B:Type[0]. ∀l:list A. ∀f. map A B f l = l. 832 #A #B #l elim l try // 833 qed. 834 835 lemma fe_to_be_values_bounded : 836 ∀ty,v. fe_to_be_values ty v ≤ 8. 837 #ty cases ty 838 [ 1: #sz #sg ] 839 #v whd in match (fe_to_be_values ??); 840 cases v normalize nodelta 841 [ 1,5: @makelist_bounded @typesize_bounded 842  2,6: * normalize nodelta #bv 843 >map_bounded >bytes_of_bitvector_bounded // 844  3,7: // 845  4,8: #ptr // ] 846 qed. 912 847 913 848 914 lemma mem_bounds_after_store_value_of_type : … … 916 982 917 983 (* Not verified for floats atm. Restricting to integers. *) 918 lemma fe_to_be_to_fe_value : ∀sz,sg,v.984 lemma fe_to_be_to_fe_value_int : ∀sz,sg,v. 919 985 ast_typ_consistent_with_value (ASTint sz sg) v → 920 986 (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v). … … 957 1023 <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF 958 1024 >(BitVector_O … iH) @refl ] 959 ] qed. 1025 ] qed. 1026 1027 lemma fe_to_be_to_fe_value_ptr : 1028 ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)). 1029 #b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta 1030 cases br normalize nodelta >eqZb_z_z normalize nodelta 1031 cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq 1032 <(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl 1033 * // 1034 qed. 960 1035 961 1036 (* It turns out that the following property is not true in general. Floats are converted to 962 1037 BVundef, which are converted back to Vundef. But we care only about ints. *) 963 lemma storev_loadv_ ok:1038 lemma storev_loadv_int_compatible : 964 1039 ∀sz,sg,m,b,ofs,v,m'. 965 1040 ast_typ_consistent_with_value (ASTint sz sg) v → … … 970 1045 lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren) 971 1046 >(fe_to_be_values_size … H) #H >H normalize nodelta 972 >fe_to_be_to_fe_value try // 973 qed. 974 975 (* For the arguments exposed before, we restrict the lemma to ints. 976 *) 977 lemma store_value_load_value_ok : 1047 >fe_to_be_to_fe_value_int try // 1048 qed. 1049 1050 (* For the arguments exposed before, we restrict the lemma to ints. *) 1051 lemma store_value_load_value_int_compatible : 978 1052 ∀sz,sg,m,b,ofs,v,m'. 979 1053 type_consistent_with_value (Tint sz sg) v → … … 989 1063 whd in match (load_value_of_type ????); 990 1064 >(fe_to_be_values_size … H) #H' >H' normalize nodelta 991 >fe_to_be_to_fe_value try // 992 qed. 993 994 1065 >fe_to_be_to_fe_value_int try // 1066 qed. 1067 1068 lemma store_value_load_value_compatible : 1069 ∀ty,m,b,ofs,v,m'. 1070 type_consistent_with_value ty v → 1071 store_value_of_type ty m b ofs v = Some ? m' → 1072 load_value_of_type ty m' b ofs = Some ? v. 1073 #ty #m #b #ofs #v #m' #H lapply H cases ty 1074 [  #sz #sg  #ty'  #ty' #n  #tl #ty'  #id #fl  #id #fl  #id ] 1075 [ 1,4,5,6,7: normalize in ⊢ (? → % → ?); #_ #Habsurd destruct 1076  2: @store_value_load_value_int_compatible 1077  3: #Hconsistent whd in match (store_value_of_type ?????); 1078 whd in match (load_value_of_type ????); #Hstoren 1079 lapply (storen_loadn_ok … Hstoren) 1080 [ @fe_to_be_values_bounded ] 1081 #Hloadn >(fe_to_be_values_size … Hconsistent) 1082 >Hloadn normalize nodelta 1083 cases v in Hconsistent; 1084 [ @False_ind  #sz' #i' @False_ind  3: @False_ind ] 1085 * #pb #poff #Hconsistent >fe_to_be_to_fe_value_ptr @refl 1086  8: #Hconsistent whd in match (store_value_of_type ?????); 1087 whd in match (load_value_of_type ????); #Hstoren 1088 lapply (storen_loadn_ok … Hstoren) 1089 [ @fe_to_be_values_bounded ] 1090 #Hloadn >(fe_to_be_values_size … Hconsistent) 1091 >Hloadn normalize nodelta 1092 cases v in Hconsistent; 1093 [ @False_ind  #sz' #i' @False_ind  3: @False_ind ] 1094 * #pb #poff #Hconsistent >fe_to_be_to_fe_value_ptr @refl 1095 ] qed. 1096 1097 (* storing something somewhere and loading at a disjoint loc yields the 1098 same result as before the store. *) 1099 lemma store_value_load_disjoint : 1100 ∀ty1,ty2,m,b1,ofs1,b2,ofs2,v,m'. 1101 ty1 ≠ ty2 → 1102 type_consistent_with_value ty1 v → 1103 store_value_of_type ty1 m b1 ofs1 v = Some ? m' → 1104 (b1 ≠ b2 1105 ∨ ((Z_of_offset ofs1) + (Z_of_nat (typesize (typ_of_type ty1))) ≤ (Z_of_offset ofs2)) 1106 ∨ ((Z_of_offset ofs2) + (Z_of_nat (typesize (typ_of_type ty2))) ≤ (Z_of_offset ofs1))) → 1107 load_value_of_type ty2 m b2 ofs2 = load_value_of_type ty2 m' b2 ofs2. 1108 #ty1 #ty2 #m #b1 #ofs1 #b2 #ofs2 #v #m' 1109 @cthulhu (* Provable using the invariants provided by storen (see prev. lemma) *) 1110 qed. 1111 1112 (* Can we say anything about what we load in the overlap case ? *) 1113 (* 1114 lemma store_value_load_overlap : 1115 ∀ty1,ty2,m,b,ofs1,ofs2,v,m'. 1116 ty1 ≠ ty2 → 1117 type_consistent_with_value ty1 v → 1118 store_value_of_type ty1 m b1 ofs1 v = Some ? m' → 1119 (Z_of_offset ofs2 < (Z_of_offset ofs1) + (Z_of_nat (typesize (typ_of_type ty1))) 1120 ∨ Z_of_offset ofs1 < (Z_of_offset ofs2) + (Z_of_nat (typesize (typ_of_type ty2)))) → 1121 load_value_of_type ty2 m b2 ofs2 = load_value_of_type ty2 m' b2 ofs2. 1122 *) 
src/Clight/memoryInjections.ma
r2468 r2483 304 304 ∀b1,off1,b2,off2,ty,v1. 305 305 valid_block m1 b1 → (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading byref *) 306 E b1 = Some ? 〈b2,off2〉 → 306 E b1 = Some ? 〈b2,off2〉 → 307 307 load_value_of_type ty m1 b1 off1 = Some ? v1 → 308 308 (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2). … … 315 315 load_value_of_type ty m1 b1 off1 = Some ? v1 → 316 316 (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2). 317 317 318 definition block_is_empty : mem → block → Prop ≝ 319 λm,b. 320 high_bound m b ≤ low_bound m b. 321 318 322 (* Adapted from Compcert's Memory *) 319 323 definition non_aliasing : embedding → mem → Prop ≝ … … 321 325 ∀b1,b2,b1',b2',delta1,delta2. 322 326 b1 ≠ b2 → 327 block_region b1 = block_region b2 → 323 328 E b1 = Some ? 〈b1',delta1〉 → 324 329 E b2 = Some ? 〈b2',delta2〉 → 325 330 (b1' ≠ b2') ∨ 331 block_is_empty m b1' ∨ 332 block_is_empty m b2' ∨ 326 333 high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ 327 334 high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1). … … 332 339 mi_inj : load_sim_ptr E m1 m2; 333 340 (* Invalid blocks are not mapped *) 334 mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;341 (* mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; *) 335 342 (* Valid pointers are mapped to valid pointers*) 336 343 mi_valid_pointers : ∀p,p'. … … 347 354 348 355 (*  *) 356 (* Setting up an empty injection *) 357 (*  *) 358 359 definition empty_injection : memory_inj (λx. None ?) empty empty. 360 % 361 [ 1: whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hptr_trans #Hload 362 normalize in Hptr_trans; destruct 363  2: * #b #o #p' #_ normalize #Habsurd destruct 364  3: #b #b' #o' #Habsurd destruct 365  4: normalize #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct ] 366 qed. 367 368 (*  *) 349 369 (* End of the definitions on memory injections. Now, on to proving some lemmas. *) 370 350 371 351 372 (* A particular inversion. *) … … 445 466 elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) 446 467 * #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @I 447 qed. 468 qed. 448 469 449 470 (* Making explicit the contents of memory_inj for load_value_of_type. … … 525 546 qed. 526 547 527 (* Memory allocation preserves [memory_inj] *) 528 lemma alloc_memory_inj : 548 (* Memory allocation in m2 preserves [memory_inj]. 549 * This is lemma 43 from Leroy&Blazy. *) 550 lemma alloc_memory_inj_m2 : 529 551 ∀E:embedding. 530 552 ∀m1,m2,m2',z1,z2,r,new_block. … … 534 556 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc 535 557 % 536 [ 1: 537 whd 558 [ whd 538 559 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload 539 560 elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload) … … 553 574 @Hload 554 575  4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ] 555  2: @(mi_freeblock … Hmemory_inj) 556  3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans) 576  #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans) 557 577 elim m2 in Halloc; #contentmap #nextblock #Hnextblock 558 578 elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc) … … 568 588 #Hbid_neq >Hbid_neq 569 589 cases (eq_region br' r) normalize #H @H 570  4: @(mi_region … Hmemory_inj) 571  5: @(mi_nonalias … Hmemory_inj) 590  @(mi_region … Hmemory_inj) 591  @(mi_nonalias … Hmemory_inj) 592 qed. 593 594 (* Allocating in m1 such that the resulting block has no image in m2 preserves 595 the injection. This is lemma 44 for Leroy&Blazy. The proof should proceed as 596 in Blazy & Leroy. Careful of using the mi_embedding hypothesis to rule out 597 absurd cases. *) 598 axiom alloc_memory_inj_m1 : 599 ∀E:embedding. 600 ∀m1,m2,m1',z1,z2,r,new_block. 601 ∀H:memory_inj E m1 m2. 602 alloc m1 z1 z2 r = 〈m1', new_block〉 → 603 E (pi1 … new_block) = None ? → 604 memory_inj E m1' m2. 605 606 (* Embed a fresh block inside an unmapped portion of the target 607 block. *) 608 axiom alloc_memory_inj_m1_to_m2 : 609 ∀E:embedding. 610 ∀m1,m2,m1':mem. 611 ∀z1,z2:Z. 612 ∀b2,new_block. 613 ∀delta:offset. 614 ∀H:memory_inj E m1 m2. 615 alloc m1 z1 z2 (block_region b2) = 〈m1', new_block〉 → 616 E (pi1 … new_block) = Some ? 〈b2, delta〉 → 617 low_bound m2 b2 ≤ z1 + Zoo delta → 618 z2 + Zoo delta ≤ high_bound m2 b2 → 619 (∀b,b',delta'. b ≠ (pi1 … new_block) → 620 E b = Some ? 〈b', delta'〉 → 621 high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨ 622 z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) → 623 memory_inj E m1' m2. 624 625 (*  *) 626 (* Lemmas pertaining to [free] *) 627 628 (* Lemma 46 by Leroy&Blazy *) 629 lemma free_load_sim_ptr_m1 : 630 ∀E:embedding. 631 ∀m1,m2,m1'. 632 load_sim_ptr E m1 m2 → 633 ∀b. free m1 b = m1' → 634 load_sim_ptr E m1' m2. 635 #E #m1 #m2 #m1' #Hinj #b #Hfree 636 whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans 637 cases ty 638 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 639  #structname #fieldspec  #unionname #fieldspec  #id ] 640 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 641 normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl 642 %4 @Htrans ] 643 #Hload <Hfree in Hload; #Hload lapply (load_value_of_type_free_load_value_of_type … Hload) 644 #Hload' @(Hinj … Hload') // 645 <Hfree in Hvalid; @valid_free_to_valid 646 qed. 647 648 (* lemma 47 of L&B *) 649 lemma free_load_sim_ptr_m2 : 650 ∀E:embedding. 651 ∀m1,m2,m2'. 652 load_sim_ptr E m1 m2 → 653 ∀b. free m2 b = m2' → 654 (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) → 655 load_sim_ptr E m1 m2'. 656 #E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped 657 whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans 658 cases ty 659 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 660  #structname #fieldspec  #unionname #fieldspec  #id ] 661 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 662 normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl 663 %4 @Htrans ] 664 #Hload <Hfree 665 (* routine *) 666 @cthulhu 667 qed. 668 669 lemma free_block_is_empty : 670 ∀m,m',b,b'. 671 block_region b = block_region b' → 672 block_is_empty m b → 673 free m b' = m' → 674 block_is_empty m' b. 675 * #contents #nextblock #Hpos 676 #m' #b #b' #Hregions_eq 677 #HA #HB normalize in HB; <HB whd 678 normalize >Hregions_eq cases (block_region b') normalize nodelta 679 @(eqZb_elim … (block_id b) (block_id b')) 680 [ 1,3: #Heq normalize nodelta // 681  2,4: #Hneq normalize nodelta @HA ] 682 qed. 683 684 (* Lemma 49 in Leroy&Blazy *) 685 axiom free_non_aliasing_m1 : 686 ∀E:embedding. 687 ∀m1,m2,m1'. 688 memory_inj E m1 m2 → 689 ∀b. free m1 b = m1' → 690 non_aliasing E m1'. 691 (* The proof proceeds by a first case analysis to see wether b lives in the 692 same world as the nonaliasing blocks (if not : trivial), in this case 693 we proceed by a case analysis on the nonaliasing hypothesis in memory_inj. *) 694 695 696 (* Extending lemma 46 and 49 to memory injections *) 697 lemma free_memory_inj_m1 : 698 ∀E:embedding. 699 ∀m1,m2,m1'. 700 memory_inj E m1 m2 → 701 ∀b. free m1 b = m1' → 702 memory_inj E m1' m2. 703 #E #m1 #m2 #m1' #Hinj #b #Hfree 704 cases Hinj 705 #Hload_sim #Hvalid #Hregion #Hnonalias 706 % try assumption 707 [ @(free_load_sim_ptr_m1 … Hload_sim … Hfree) 708  #p #p' #Hvalid_m1' #Hptr_translation @(Hvalid p p' ? Hptr_translation) 709 <Hfree in Hvalid_m1'; @valid_free_to_valid 710  @(free_non_aliasing_m1 … Hinj … Hfree) ] 711 qed. 712 713 (* Lifting lemma 47 to memory injs *) 714 lemma free_memory_inj_m2 : 715 ∀E:embedding. 716 ∀m1,m2,m2'. 717 memory_inj E m1 m2 → 718 ∀b. free m2 b = m2' → 719 (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) → 720 memory_inj E m1 m2'. 721 #E #m1 #m2 #m2' #Hinj #b #Hfree #b1_not_mapped 722 % cases Hinj try // 723 #Hload_sim #Hvalid #Hregion #Hnonalias 724 [ (* We succed performing a load from m1. Case analysis: if byvalue, cannot map to freed block [b] 725 (otherwise contradiction), hence simulation proceeds through Hinj. 726 If not byvalue, then simulation proceeds without examining the contents of the memory *) 727 @cthulhu 728  #p #p' #Hvalid #Hptr_trans 729 (* We now through Hinj that valid_pointer m2 p'=true, 730 if (pblock p') = b then using b1_not_mapped and Hptr_trans we 731 know that the original pointer must be either invalid or empty, 732 hence contradiction with Hvalid 733 if (pblock p') ≠ b then straightforward simulation *) 734 @cthulhu 735  @Hregion ] 736 qed. 737 738 (* Lemma 64 of L&B on [freelist] *) 739 lemma freelist_memory_inj_m1_m2 : 740 ∀E:embedding. 741 ∀m1,m2,m1',m2'. 742 memory_inj E m1 m2 → 743 ∀blocklist,b2. 744 (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) → 745 free m2 b2 = m2' → 746 free_list m1 blocklist = m1' → 747 memory_inj E m1' m2'. 748 (* nothing particular here, application of various lemmas and induction over blocklist. *) 749 @cthulhu 572 750 qed. 573 751 574 752 (*  *) 575 753 (* Lemma 40 of the paper of Leroy & Blazy on the memory model 576 * and related lemmas *)754 * and storerelated lemmas *) 577 755 578 756 lemma bestorev_beloadv_conservation : … … 643 821 lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2 644 822 // 645 ] qed. 823 ] qed. 824 825 lemma store_value_of_type_load_value_of_type_conservation : 826 ∀ty,mA,mB,wb,wo,v. 827 store_value_of_type ty mA wb wo v = Some ? mB → 828 ∀rb,ro. eq_block wb rb = false → 829 ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro. 830 #ty #mA #mB #wb #wo #v #Hstore #rb #ro #Heq_block 831 cases ty in Hstore; 832 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 833  #structname #fieldspec  #unionname #fieldspec  #id ] 834 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct ] 835 whd in ⊢ ((??%?) → ?); #Hstoren 836 @(storen_load_value_of_type_conservation … Hstoren … Heq_block) 837 qed. 646 838 647 839 definition typesize' ≝ λty. typesize (typ_of_type ty). … … 808 1000 #E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore % 809 1001 lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try // 810 cases Hinj #Hsim' #H not_valid #Hvalid #Hregion #Hnonalias try assumption1002 cases Hinj #Hsim' #Hvalid #Hregion #Hnonalias try assumption 811 1003 #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid 812 1004 cases ty in Hstore; … … 825 1017 ] qed. 826 1018 1019 827 1020 (*  *) 828 1021 (* Lemma 41 of the paper of Leroy & Blazy on the memory model … … 839 1032 qed. 840 1033 1034 lemma fe_to_be_values_length : 1035 ∀E,v1,v2,ty. 1036 value_eq E v1 v2 → fe_to_be_values ty v1 = fe_to_be_values ty v2. 1037 #E #v1 #v2 #ty #Hvalue_eq 1038 @(value_eq_inversion … Hvalue_eq) // 1039 qed. 1040 841 1041 lemma value_eq_to_be_and_back_again : 842 1042 ∀E,ty,v1,v2. 843 1043 value_eq E v1 v2 → 844 1044 ast_typ_consistent_with_value ty v1 → 845 ast_typ_consistent_with_value ty v2 →846 1045 value_eq E (be_to_fe_value ty (fe_to_be_values ty v1 )) (be_to_fe_value ty (fe_to_be_values ty v2)). 847 1046 #E #ty #v1 #v2 #Hvalue_eq … … 850 1049  2: #sz #i cases ty 851 1050 [ 2: @False_ind 852  1: #sz' #sg #H whd in ⊢ (% → ?); #Heq853 lapply (fe_to_be_to_fe_value … H) #H >H // ]1051  1: #sz' #sg #H lapply H whd in ⊢ (% → ?); #Heq 1052 lapply (fe_to_be_to_fe_value_int … H) #H >H // ] 854 1053  3: #p1 #p2 #Hembed cases ty 855 1054 [ 1: #sz #sg @False_ind 856  2: #_ #_1055  2: #_ 857 1056 cases p1 in Hembed; #b1 #o1 858 1057 cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H … … 864 1063 ] qed. 865 1064 1065 (*  *) 1066 (* Lemma ?? of the paper of Leroy & Blazy on the memory model ? *) 1067 866 1068 lemma storen_parallel_memory_exists : 867 ∀E,m1,m2 ,m1',b1,i,b2,delta,ty,v1,v2.868 memory_inj E m1 m2 → 869 value_eq E v1 v2→870 storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→871 E b1 = Some ? 〈b2, delta〉→1069 ∀E,m1,m2. 1070 memory_inj E m1 m2 → 1071 ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 → 1072 ∀v1,v2. value_eq E v1 v2 → 1073 ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ 872 1074 ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2'. 873 @cthulhu qed. 874 (* 875 #E #m1 #m2 #m1' #b1 #i #b2 #delta #ty #v1 #v2 #Hinj #Hvalue_eq 876 @(value_eq_inversion … Hvalue_eq) 877 [ 1: #v #Hstoren *) 878 879 880 lemma storen_parallel_aux : 1075 (* ∧ loadn m2' (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? (fe_to_be_values ty v2).*) 1076 #E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty 1077 lapply (mi_valid_pointers … Hinj) 1078 generalize in match m2; 1079 generalize in match m1; 1080 generalize in match i; 1081 lapply (fe_to_be_values_length … ty Hvalue_eq) 1082 generalize in match (fe_to_be_values ty v2); 1083 generalize in match (fe_to_be_values ty v1); 1084 #l1 elim l1 1085 [ 1: #l2 #Hl2 1086 cut (l2 = []) 1087 [ cases l2 in Hl2; // #hd' #tl' normalize #Habsurd destruct ] 1088 #Hl2_empty >Hl2_empty #o #m1 #m2 #_ normalize /2 by ex_intro/ 1089  2: #hd1 #tl1 #Hind #l2 #Hlength 1090 cut (∃hd2,tl2.l2 = hd2::tl2 ∧ tl1 = tl2) 1091 [ cases l2 in Hlength; 1092 [ normalize #Habsurd destruct 1093  #hd2 #tl2 normalize #H %{hd2} %{tl2} @conj try @refl destruct (H) assumption ] ] 1094 * #hd2 * #tl2 * #Heq2 destruct (Heq2) #Hlen_tl 1095 #o #m1 #m2 #Hvalid_embed #Hstoren 1096 cases (some_inversion ????? Hstoren) #m1_tmp * #Hbestorev #Hstoren_tl 1097 lapply (Hvalid_embed (mk_pointer b1 o) (mk_pointer b2 (offset_plus o delta)) ??) 1098 [ 1: whd in match (pointer_translation ??); 1099 >Hembed normalize nodelta @refl 1100  2: @(bestorev_to_valid_pointer … Hbestorev) ] 1101 #Hvalid_ptr_m2 1102 whd in match (storen ???); 1103 lapply (valid_pointer_to_bestorev_ok m2 (mk_pointer b2 (offset_plus o delta)) hd2 Hvalid_ptr_m2) 1104 * #m2_tmp #Hbestorev2 >Hbestorev2 normalize nodelta 1105 whd in match (shift_pointer ???) in Hstoren_tl ⊢ %; 1106 whd in match (shift_offset ???) in Hstoren_tl ⊢ %; 1107 (* normalize in match (sign_ext ???) in Hstoren_tl ⊢ %;*) 1108 cut (mk_offset (addition_n ? (offv (offset_plus o delta)) (sign_ext 2 offset_size (bitvector_of_nat 2 1))) = 1109 offset_plus (offset_plus o (mk_offset (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) delta) 1110 [ cases o #o' normalize nodelta whd in match (offset_plus ??) in ⊢ (??%%); 1111 whd in match (offset_plus ??) in ⊢ (???(?%)); 1112 /2 by associative_addition_n, commutative_addition_n, refl/ ] 1113 #Heq_cleanup >Heq_cleanup >Heq_cleanup in Hind; #Hind @(Hind … Hstoren_tl) 1114 try assumption 1115 #p #p' #Hvalid_in_m1_tmp #Hp_embed @valid_pointer_of_Prop 1116 lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * 1117 #Hnextblock_eq #Hbounds_eq #Hoffset_in_bounds #Hcontents_at_eq #Hcontents_else_eq 1118 lapply (mem_bounds_invariant_after_bestorev … Hbestorev2) * * * * 1119 #Hnextblock_eq2 #Hbounds_eq2 #Hoffset_in_bounds2 #Hcontents_at_eq2 #Hcontents_else_eq2 1120 cut (valid_pointer m1 p = true) 1121 [ @valid_pointer_of_Prop 1122 cases (valid_pointer_to_Prop … Hvalid_in_m1_tmp) 1123 >Hnextblock_eq cases (Hbounds_eq (pblock p)) #Hlow' #Hhigh' 1124 whd in match (low_bound ??); whd in match (high_bound ??); 1125 >Hlow' >Hhigh' * /3 by conj/ ] 1126 #Hvalid_in_m1 1127 lapply (Hvalid_embed p p' Hvalid_in_m1 Hp_embed) #Hvalid_in_m2 1128 cases (valid_pointer_to_Prop … Hvalid_in_m2) * #Hnextblock2' #Hlow2' #Hhigh2' 1129 @conj try @conj 1130 >Hnextblock_eq2 try assumption 1131 cases (Hbounds_eq2 … (pblock p')) #Hlow2'' #Hhigh2'' 1132 whd in match (low_bound ??); 1133 whd in match (high_bound ??); 1134 >Hlow2'' >Hhigh2'' assumption 1135 ] qed. 1136 1137 lemma storen_parallel_memory_exists_and_preserves_loads : 1138 ∀E,m1,m2. 1139 memory_inj E m1 m2 → 1140 ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 → 1141 ∀v1,v2. value_eq E v1 v2 → 1142 ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ 1143 ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧ 1144 loadn m2' (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? (fe_to_be_values ty v2). 1145 #E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty #Hstoren 1146 cases (storen_parallel_memory_exists … Hinj … Hembed … Hvalue_eq i m1' ty Hstoren) 1147 #m2' #Hstoren' %{m2'} @conj try assumption 1148 @(storen_loadn_ok … Hstoren') 1149 // 1150 qed. 1151 1152 (* If E ⊢ m1 ↦ m2 1153 *and* if E b1 = 〈b2,delta〉, 1154 *and* if we write /A PROPER VALUE/ at 〈b1,i〉 successfuly, 1155 *then* we can write /something value_eqcompatible/ in m2 at 〈b2,i+delta〉 successfuly yielding m2' 1156 *and* preserve the injection : E ⊢ m1' ↦ m2' 1157 N.B.: this result cannot be given at the backend level : we could overwrite a pointer 1158 and break the value_eq correspondence between the memories. *) 1159 axiom storen_parallel_aux : 881 1160 ∀E,m1,m2. 882 1161 ∀Hinj:memory_inj E m1 m2. … … 885 1164 ∀ty,i,m1'. 886 1165 ast_typ_consistent_with_value ty v1 → 887 ast_typ_consistent_with_value ty v2 →888 1166 storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' → 889 1167 ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧ 890 1168 memory_inj E m1' m2'. 891 #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hok1 #Hok2 892 #Hstoren lapply (storen_to_valid_pointer_fe_to_be … Hstoren) 893 * * * #Hblocks_eq1 #Hnextblock1 #Hvalid_m1 #Hvalid_m1' 894 lapply (mi_valid_pointers … Hinj … (mk_pointer b1 i) (mk_pointer b2 (offset_plus i delta)) Hvalid_m1 ?) 895 [ 1: whd in ⊢ (??%%); >Hembed @refl ] 896 #Hvalid_m2 897 cases (valid_pointer_to_Prop … Hvalid_m2) * #Hnextblock2 #Hlow2 #Hhigh2 898 @cthulhu 899 qed. 900 901 lemma foo : 1169 (* This lemma is not provable as in CompCert. In the following chunk of text, I'll try to 1170 * explain why, and how we might still be able to prove it given enough time. 1171 I'll be refering to paper by Leroy & Blazy in the J.A.R. 1172 In CompCert, when storing some data of size S in some location 〈block, offset〉, 1173 what happens is that 1174 1) the memory is extended with a map from 〈block,offset〉 to the actual data 1175 2) the memory inteval from 〈block,offset+1〉 to 〈block,offset+S1〉 is invalidated, 1176 meaning that every load in this interval will fail. 1177 This behaviour is documented at page 9 in the aforementioned paper. 1178 The memory model of Cerco is in a sense much more realistic. When storing a frontend 1179 value fv, the story is the following : 1180 1) the value fv is marshelled into a list of backend values (bytesized) which correspond 1181 to the actual size of the data inmemory. This list is then stored asis at the 1182 location 〈block, offset〉. 1183 1184 Now on to the lemma we want to prove. The difficult part is to prove [load_sim E m1' m2'], 1185 i.e. we want to prove that ∀c1,off1,c2,off2,delta. s.t. E c1 = 〈c2, off2〉 1186 load_value_of_type m1' c1 off1 = ⌊vA⌋ → 1187 load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋ ∧ 1188 value_eq E vA vB, 1189 where m1' and m2' are the result of storing some values v1 and v2 in resp. m1 and m2 1190 at some resp. locations 〈b1,i〉 and (pointer_translation E b1 i) (cf statement). 1191 1192 In CompCert, the proof of this statement goes by case analysis on 〈c1,off1〉. 1193 Case 1: 〈b1,i〉 = 〈c1,off1〉 → we read the freshly stored data. 1194 Case 2: b1 = c1 but [i; i+v1] and [c1, c1+vA] describe /disjoint/ areas of the 1195 same block. In this case, we can use the lemma store_value_load_disjoint 1196 on the hypothesis (load_value_of_type m1' c1 off1 = ⌊vA⌋) 1197 yielding (load_value_of_type m1' c1 off1 = load_value_of_type m1 c1 off1) 1198 allowing us to use the load_sim hypothesis on (m1, m2) to obtain 1199 (load_value_of_type m2 c2 (off1+off2) = ⌊vB⌋) 1200 which we can lift back to 1201 (load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋) 1202 using the disjointness hypothesis contained in the original memory injection [Hinj]. 1203 case 4: b1 ≠ c1, nothing difficult 1204 case 3: the intervals [i; i+v1] and [c1, c1+vA] /overalap/ ! 1205 in CompCert, the prof follows simply from the fact that the load 1206 (load_value_of_type m1' c1 off1) will fail because of invalidated memory, 1207 yielding a contradiction. We have no such possibility in Cerco. 1208 1209 I see a possible, convoluted way out of this problem. In the case of an overlap, we 1210 need to proceed to an inversion on load_value_of_type m1' c1 off1 = ⌊vA⌋ and to 1211 actually look at the data beeing written. If we succeeded in proceeding to this load, 1212 this means that the backend values stored are "consistent". 1213 Besides, we need to proceed to a case analysis on what we stored beforehand. 1214 A) If we stored an integer 1215 . of size 8: this means that the overlap actually includes all of the freshly stored 1216 area. This area contains one [BVByte]. If we succeeded in performing an overlapping load, 1217 we either overlapped from the beginning, from the end or from both ends of the stored 1218 area. In all cases, since this area contains a BVByte, all other offsets MUST contain 1219 BVBytes, otherwise we would have a contradiction ... (cumbersome to show but possible) 1220 Hence, we can splice the load in 2 or 3 subloads : 1221 . reuse the Case 2 above (disjoint areas) for the parts of the load that are before 1222 and after the stored area 1223 . reuse the Case 1 above for the stored area 1224 and show the whole successful load 1225 . of size 16,32: we have more freedom but only a finite number of overlap possibilities 1226 in each case. We can enumerate them and proceed along the same lines as in the 8 bit 1227 case. 1228 B) If we stored a pointer (of size 2 bytes, necessarily) 1229 . the bytes of a pointer are stored in order and (/!\ important /!\) are /numbered/. 1230 This means that any successful overlapping load has managed to read a pointer in 1231 the wrong order, which yields a contradiction. 1232 C) If we stored a Vnull, roughly the same reasoning as in the pointer case 1233 D) If we stored a Vundef ... This gets hairy. We must reason on the way fe_to_be_values 1234 and be_to_fe_value works. What we want is to show that the load 1235 [load_value_of_a type m1' c1 off1] yields a Vundef. This can happen in several ways. 1236 . If we try to load something of integer type, we will have a Vundef because 1237 we can show that some of the backend values are BVundef (cf [build_integer]) 1238 . If we try to load a pointer, it will also fail for the same reason. 1239 I'll admit that I'm not too sure about the last case. Also, my reasoning on pointers might 1240 fail if we have "longer that 2 bytes" pointers. 1241 1242 This was a highlevel and sketchy proof, and in the interests of time I decide to axiomatize 1243 it. 1244 *) 1245 1246 (* This is lemma 60 from Leroy&Blazy *) 1247 lemma store_value_of_type_parallel : 902 1248 ∀E,m1,m2. 903 1249 ∀Hinj:memory_inj E m1 m2. 904 1250 ∀v1,v2. value_eq E v1 v2 → 905 1251 ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → 906 ∀ty,i,m1'. store_value_of_type ty m1 b1 i v1 = Some ? m1' → 1252 ∀ty,i,m1'. 1253 type_consistent_with_value ty v1 → 1254 store_value_of_type ty m1 b1 i v1 = Some ? m1' → 907 1255 ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧ 908 memory_inj E m1' m2'. 909 #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hstore 910 @cthulhu qed. 1256 memory_inj E m1' m2'. 1257 #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' 1258 cases ty 1259 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1260  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1261 #Hconsistent whd in ⊢ ((??%?) → ?); 1262 [ 1,4,5,6,7: #Habsurd destruct ] 1263 whd in match (store_value_of_type ?????); 1264 @(storen_parallel_aux … Hinj … Hembed … Hconsistent) // 1265 qed. 1266 1267 lemma store_value_of_type_load_sim : 1268 ∀E,m1,m2,m1'. 1269 ∀Hinj:memory_inj E m1 m2. 1270 ∀ty,b,i,v. 1271 E b = None ? → 1272 store_value_of_type ty m1 b i v = Some ? m1' → 1273 load_sim_ptr E m1' m2. 1274 #E #m1 #m2 #m1' #Hinj #ty #b #i #v #Hembed #Hstore 1275 cases Hinj #Hsim #Hvalid #Hregion_eq #Hnonalias 1276 cases ty in Hstore; 1277 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1278  #structname #fieldspec  #unionname #fieldspec  #id ] 1279 [ 1,4,5,6,7: #Heq normalize in Heq; destruct ] 1280 #Hstore whd 1281 #b1 #off1 #b2 #off2 #ty' #v1 #Hvalid #Hembed' #Hload 1282 lapply (store_value_of_type_load_value_of_type_conservation … Hstore b1 off1 ? ty') 1283 [ 1,3,5: @(eq_block_elim … b b1) try // #Heq >Heq in Hembed; 1284 #Hembed whd in Hembed':(??%?); >Hembed in Hembed'; #H normalize in H; 1285 destruct ] 1286 #Heq <Heq in Hload; #Hload 1287 (* Three times the same proof, but computing the indices is a PITA *) 1288 [ 1: 1289 cases ty' in Hload; 1290 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1291  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1292 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????); 1293 #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))} 1294 @conj try @refl %4 assumption ] 1295 #Hload @(Hsim … Hembed' … Hload) 1296 @(load_by_value_success_valid_pointer … Hload) // 1297  2: 1298 cases ty' in Hload; 1299 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1300  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1301 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????); 1302 #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))} 1303 @conj try @refl %4 assumption ] 1304 #Hload @(Hsim … Hembed' … Hload) 1305 @(load_by_value_success_valid_pointer … Hload) // 1306  3: 1307 cases ty' in Hload; 1308 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1309  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1310 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????); 1311 #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))} 1312 @conj try @refl %4 assumption ] 1313 #Hload @(Hsim … Hembed' … Hload) 1314 @(load_by_value_success_valid_pointer … Hload) // 1315 ] qed. 1316 1317 lemma store_value_of_type_memory_inj : 1318 ∀E,m1,m2,m1'. 1319 ∀Hinj:memory_inj E m1 m2. 1320 ∀ty,b,i,v. 1321 E b = None ? → 1322 store_value_of_type ty m1 b i v = Some ? m1' → 1323 memory_inj E m1' m2. 1324 #E #m1 #m2 #m1' #Hinj #ty #b #i #v1 #Hnot_mapped #Hstore 1325 % 1326 [ 1: @(store_value_of_type_load_sim … Hinj … Hnot_mapped … Hstore) 1327  2: (* trivial *) @cthulhu 1328  3: (* easy *) @cthulhu 1329  4: (* writing doesn't alter the bound, straightforward *) @cthulhu ] 1330 qed. 911 1331 912 1332 (*  *)
Note: See TracChangeset
for help on using the changeset viewer.