Changeset 2483 for src/Clight/MemProperties.ma
 Timestamp:
 Nov 22, 2012, 5:05:55 PM (7 years ago)
 File:

 1 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 *)
Note: See TracChangeset
for help on using the changeset viewer.