Ignore:
Timestamp:
Nov 22, 2012, 5:05:55 PM (8 years ago)
Author:
garnier
Message:

Memory injections for Clight to Cminor, partially axiomatized.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/MemProperties.ma

    r2468 r2483  
    105105(* --------------------------------------------------------------------------- *)
    106106
    107 (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the back-end 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 back-end values are equal.
     108 * This is allright for switch removal but false for Clight to Cminor *)
    108109definition load_sim ≝
    109110λ(m1 : mem).λ(m2 : mem).
     
    279280#_ normalize nodelta
    280281#H @H
     282qed.
     283
     284lemma 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
     301lemma 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
     306cases ty
     307[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     308| #structname #fieldspec | #unionname #fieldspec | #id ]
     309#m #block #b #o #res
     310whd in ⊢ ((??%?) → (??%?)); // #H
     311cases (some_inversion ????? H) #be * #Hloadn #Heq
     312>(loadn_free_loadn … Hloadn)
     313normalize nodelta assumption
    281314qed.
    282315
     
    512545   serious PITA to prove. *)
    513546axiom 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 *)
     551definition 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
     556lemma 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. *)
     565lemma typesize_bounded : ∀ty. typesize ty ≤ 8.
     566* try // * try // qed.
     567
     568(* Lifting bound on make_list *)
     569lemma 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
     572cases 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
     579lemma 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
     592lemma map_bounded :
     593  ∀A,B:Type[0]. ∀l:list A. ∀f. |map A B f l| = |l|.
     594  #A #B #l elim l try //
     595qed.
     596
     597
     598lemma 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 // ]
     609qed.     
     610
     611lemma 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
    514651
    515652(* /!\ TODO the following proof is extremely ugly and indirect. I expect it to be
     
    601738] qed.
    602739
     740(* Adapting the lemma above to (fe_to_be_values ty v) *)
     741lemma 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   
     756lapply (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
     759try assumption @H6
     760cases (fe_to_be_values_nonempty ty v) #hd * #tl #H >H //
     761qed.
     762
    603763(* extension of [bestorev_to_valid_pointer] to storen *)
    604764lemma storen_to_valid_pointer :
     
    633793] qed.
    634794
    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     
    674796
    675797lemma storen_to_valid_pointer_fe_to_be :
     
    704826>(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl
    705827qed.
     828
     829lemma 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
     837lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
     838#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
     839cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0
     840whd in match (loadn ???);
     841lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
     842whd in match (beloadv ??);
     843whd in match (low_bound ??); whd in match (high_bound ??);
     844>Hnext
     845cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
     846normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh
     847cases (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
     850cases (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
     853normalize >Htl' @refl
     854qed.
     855
    706856
    707857lemma loadn_beloadv_ok :
     
    733883] qed.
    734884
    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
    774886
    775887lemma storen_loadn_ok :
     
    798910     >nth_miss // >nth_miss //
    799911] 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 
    847913
    848914lemma mem_bounds_after_store_value_of_type :
     
    916982
    917983(* Not verified for floats atm. Restricting to integers. *)
    918 lemma fe_to_be_to_fe_value : ∀sz,sg,v.
     984lemma fe_to_be_to_fe_value_int : ∀sz,sg,v.
    919985  ast_typ_consistent_with_value (ASTint sz sg) v →
    920986  (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v).
     
    9571023          <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF
    9581024          >(BitVector_O … iH) @refl ]
    959 ] qed.                   
     1025] qed.
     1026
     1027lemma 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
     1030cases br normalize nodelta >eqZb_z_z normalize nodelta
     1031cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
     1032<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
     1033* //
     1034qed.
    9601035
    9611036(* It turns out that the following property is not true in general. Floats are converted to
    9621037   BVundef, which are converted back to Vundef. But we care only about ints.  *)
    963 lemma storev_loadv_ok :
     1038lemma storev_loadv_int_compatible :
    9641039  ∀sz,sg,m,b,ofs,v,m'.
    9651040    ast_typ_consistent_with_value (ASTint sz sg) v →
     
    9701045lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren)
    9711046>(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 //
     1048qed.
     1049
     1050(* For the arguments exposed before, we restrict the lemma to ints. *)
     1051lemma store_value_load_value_int_compatible :
    9781052  ∀sz,sg,m,b,ofs,v,m'.
    9791053    type_consistent_with_value (Tint sz sg) v →
     
    9891063whd in match (load_value_of_type ????);
    9901064>(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 //
     1066qed.
     1067
     1068lemma 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. *)
     1099lemma 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) *)
     1110qed.
     1111
     1112(* Can we say anything about what we load in the overlap case ?  *)
     1113(*
     1114lemma 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.