Changeset 2483


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

Memory injections for Clight to Cminor, partially axiomatized.

Location:
src/Clight
Files:
2 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*)
  • src/Clight/memoryInjections.ma

    r2468 r2483  
    304304 ∀b1,off1,b2,off2,ty,v1.
    305305  valid_block m1 b1 →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
    306   E b1 = Some ? 〈b2,off2〉 →
     306  E b1 = Some ? 〈b2,off2〉 → 
    307307  load_value_of_type ty m1 b1 off1 = Some ? v1 →
    308308  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
     
    315315  load_value_of_type ty m1 b1 off1 = Some ? v1 →
    316316  (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).
    317  
     317
     318definition block_is_empty : mem → block → Prop ≝
     319λm,b.
     320  high_bound m b ≤ low_bound m b.
     321
    318322(* Adapted from Compcert's Memory *)
    319323definition non_aliasing : embedding → mem → Prop ≝
     
    321325  ∀b1,b2,b1',b2',delta1,delta2.
    322326  b1 ≠ b2 →
     327  block_region b1 = block_region b2 →
    323328  E b1 = Some ? 〈b1',delta1〉 →
    324329  E b2 = Some ? 〈b2',delta2〉 →
    325330  (b1' ≠ b2') ∨
     331  block_is_empty m b1' ∨
     332  block_is_empty m b2' ∨
    326333  high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
    327334  high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1).
     
    332339  mi_inj : load_sim_ptr E m1 m2;
    333340  (* 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 ?; *)
    335342  (* Valid pointers are mapped to valid pointers*)
    336343  mi_valid_pointers : ∀p,p'.
     
    347354
    348355(* ---------------------------------------------------------------------------- *)
     356(* Setting up an empty injection *)
     357(* ---------------------------------------------------------------------------- *)
     358
     359definition 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 ]
     366qed.
     367
     368(* ---------------------------------------------------------------------------- *)
    349369(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
     370
    350371
    351372(* A particular inversion. *)
     
    445466elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
    446467* #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @I
    447 qed. 
     468qed.
    448469
    449470(* Making explicit the contents of memory_inj for load_value_of_type.
     
    525546qed.
    526547
    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. *)
     550lemma alloc_memory_inj_m2 :
    529551  ∀E:embedding.
    530552  ∀m1,m2,m2',z1,z2,r,new_block.
     
    534556#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
    535557%
    536 [ 1:
    537   whd
     558[ whd
    538559  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
    539560  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
     
    553574     @Hload
    554575  | 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)
    557577     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
    558578     elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
     
    568588     #Hbid_neq >Hbid_neq
    569589     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)
     592qed.
     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. *)
     598axiom 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. *)
     608axiom 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 *)
     629lemma 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
     636whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans
     637cases 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
     646qed.
     647
     648(* lemma 47 of L&B *)
     649lemma 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
     657whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans
     658cases 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
     667qed.
     668
     669lemma 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
     678normalize >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 ]
     682qed.
     683
     684(* Lemma 49 in Leroy&Blazy *)
     685axiom 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 non-aliasing blocks (if not : trivial), in this case
     693   we proceed by a case analysis on the non-aliasing hypothesis in memory_inj. *)
     694
     695
     696(* Extending lemma 46 and 49 to memory injections *)
     697lemma 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
     704cases 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) ]
     711qed.
     712
     713(* Lifting lemma 47 to memory injs *)
     714lemma 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 by-value, cannot map to freed block [b]
     725     (otherwise contradiction), hence simulation proceeds through Hinj.
     726     If not by-value, 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 ]
     736qed.
     737
     738(* Lemma 64 of L&B on [freelist] *)
     739lemma 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
    572750qed.
    573751
    574752(* ---------------------------------------------------------- *)
    575753(* Lemma 40 of the paper of Leroy & Blazy on the memory model
    576  * and related lemmas *)
     754 * and store-related lemmas *)
    577755
    578756lemma bestorev_beloadv_conservation :
     
    643821     lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2
    644822     //
    645 ] qed.     
     823] qed.
     824
     825lemma 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
     831cases 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 ]
     835whd in ⊢ ((??%?) → ?); #Hstoren
     836@(storen_load_value_of_type_conservation … Hstoren … Heq_block)
     837qed.
    646838
    647839definition typesize' ≝ λty. typesize (typ_of_type ty).
     
    8081000#E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore %
    8091001lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try //
    810 cases Hinj #Hsim' #Hnot_valid #Hvalid #Hregion #Hnonalias try assumption
     1002cases Hinj #Hsim' #Hvalid #Hregion #Hnonalias try assumption
    8111003#p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid
    8121004cases ty in Hstore;
     
    8251017] qed.
    8261018
     1019
    8271020(* ---------------------------------------------------------- *)
    8281021(* Lemma 41 of the paper of Leroy & Blazy on the memory model
     
    8391032qed.
    8401033
     1034lemma 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) //
     1039qed.
     1040
    8411041lemma value_eq_to_be_and_back_again :
    8421042  ∀E,ty,v1,v2.
    8431043  value_eq E v1 v2 →
    8441044  ast_typ_consistent_with_value ty v1 →
    845   ast_typ_consistent_with_value ty v2 →
    8461045  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)).
    8471046#E #ty #v1 #v2 #Hvalue_eq
     
    8501049| 2: #sz #i cases ty
    8511050     [ 2: @False_ind
    852      | 1: #sz' #sg #H whd in ⊢ (% → ?); #Heq
    853           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 // ]
    8541053| 3: #p1 #p2 #Hembed cases ty
    8551054     [ 1: #sz #sg @False_ind
    856      | 2: #_ #_
     1055     | 2: #_
    8571056          cases p1 in Hembed; #b1 #o1
    8581057          cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H
     
    8641063] qed.
    8651064
     1065(* ------------------------------------------------------------ *)
     1066(* Lemma ?? of the paper of Leroy & Blazy on the memory model ? *)
     1067
    8661068lemma 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'
    8721074  ∃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
     1077lapply (mi_valid_pointers … Hinj)
     1078generalize in match m2;
     1079generalize in match m1;
     1080generalize in match i;
     1081lapply (fe_to_be_values_length … ty Hvalue_eq)
     1082generalize in match (fe_to_be_values ty v2);
     1083generalize 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
     1137lemma 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
     1146cases (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//
     1150qed.
     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_eq-compatible/ 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 back-end level : we could overwrite a pointer
     1158         and break the value_eq correspondence between the memories. *)       
     1159axiom storen_parallel_aux :
    8811160  ∀E,m1,m2.
    8821161  ∀Hinj:memory_inj E m1 m2.
     
    8851164  ∀ty,i,m1'.
    8861165  ast_typ_consistent_with_value ty v1 →
    887   ast_typ_consistent_with_value ty v2 → 
    8881166  storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' →
    8891167  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧
    8901168        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+S-1〉 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 front-end
     1179   value fv, the story is the following :
     1180   1) the value fv is marshelled into a list of back-end values (byte-sized) which correspond
     1181      to the actual size of the data in-memory. This list is then stored as-is 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 back-end 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 sub-loads :
     1221       . re-use the Case 2 above (disjoint areas) for the parts of the load that are before
     1222         and after the stored area
     1223       . re-use 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 back-end 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 high-level 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 *)
     1247lemma store_value_of_type_parallel :
    9021248  ∀E,m1,m2.
    9031249  ∀Hinj:memory_inj E m1 m2.
    9041250  ∀v1,v2. value_eq E v1 v2 →
    9051251  ∀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' →
    9071255  ∃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'
     1258cases 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 ]
     1263whd in match (store_value_of_type ?????);
     1264@(storen_parallel_aux … Hinj … Hembed … Hconsistent) //
     1265qed.
     1266
     1267lemma 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
     1275cases Hinj #Hsim #Hvalid #Hregion_eq #Hnonalias
     1276cases 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
     1282lapply (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
     1317lemma 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 ]
     1330qed.
    9111331
    9121332(* ------------------------------------------------------------------------- *)
Note: See TracChangeset for help on using the changeset viewer.