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/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.