Changeset 2608


Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (6 years ago)
Author:
garnier
Message:

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

Location:
src
Files:
17 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2588 r2608  
    313313| cons h vars ⇒
    314314  let 〈id,ty〉 ≝ h in
    315   let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) XData in
     315  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) (* XData *) in
    316316      exec_alloc_variables (add ?? en id b1) m1 vars
    317317].
  • src/Clight/CexecSound.ma

    r2588 r2608  
    138138(* expressions that are lvalues *)
    139139| #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %;
    140     @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
     140    @bind2_OK *  (* #x cases x; #y cases y; #sp *) #loc #ofs #tr #H
    141141    @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
    142142    >H in He'; #He' @He'
     
    145145    lapply (refl ? (lookup SymbolTag block en v))
    146146    cases (lookup SymbolTag block en v) in ⊢ (???% → %);
    147     [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
     147    [ #eget @opt_bind_OK #sploc cases sploc; #sp (* #loc *) #efind
    148148        whd; @(eval_Evar_global … eget efind)
    149149    | #loc #eget @(eval_Evar_local … eget)
     
    257257] qed.
    258258
    259 lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr.
    260 exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
    261 exec_expr ge en m (Expr (Eaddrof e) (Tpointer Tvoid)) = OK ? 〈Vptr (mk_pointer (mk_block r loc) off), tr〉.
    262 #ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
    263 >H whd in ⊢ (??%?); cases r @refl
     259lemma addrof_exec_lvalue: ∀ge,en,m,e(*,r*),loc,off,tr.
     260exec_lvalue ge en m e = OK ? 〈〈mk_block (*r*) loc,off〉,tr〉 →
     261exec_expr ge en m (Expr (Eaddrof e) (Tpointer Tvoid)) = OK ? 〈Vptr (mk_pointer (mk_block (*r*) loc) off), tr〉.
     262#ge #en #m #e (* #r *) #loc #off #tr #H whd in ⊢ (??%?);
     263>H whd in ⊢ (??%?); (* cases r *) @refl
    264264qed.
    265265
     
    268268#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
    269269cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    270 [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H
     270[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #loci #H (* #locr #loci #H *)
    271271    @(addrof_eval_lvalue … (Tpointer Tvoid))
    272272    lapply (addrof_exec_lvalue … H) #H'
     
    305305[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
    306306| * #id #ty #t #IH #en #m #en' #m'
    307   lapply (refl ? (alloc m O (sizeof ty) XData)) whd in ⊢ (? → ??%? → ?);
    308   cases (alloc ????) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC
     307  lapply (refl ? (alloc m O (sizeof ty) (*XData*))) whd in ⊢ (? → ??%? → ?);
     308  cases (alloc ??? (*?*)) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC
    309309 @(alloc_variables_cons … ALLOC)
    310310 @IH @EXEC
     
    378378    ]
    379379  | #ex1 #ex2
    380     @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr1 #Hlval
     380    @res_bindIO2_OK #x cases x; (*#y cases y; *) #pcl (* #loc *) #ofs #tr1 #Hlval
    381381    @res_bindIO2_OK #v2 #tr2 #Hv2
    382382    @opt_bindIO_OK #m' #em'
     
    390390    [ @(step_call_none … Hvf Hvargs efd ety)
    391391    | #lhs'
    392         @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr3 #Hlocofs
     392        @res_bindIO2_OK #x cases x; (* #y cases y; *) #pcl (* #loc *) #ofs #tr3 #Hlocofs
    393393        whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety)
    394394    ]
     
    483483whd in ⊢ (???%);
    484484@bind_OK #m #Em
    485 @opt_bind_OK #x cases x; #sp #b #esb
     485@opt_bind_OK #x cases x; #sp #esb (* #b #esb *)
    486486@opt_bind_OK #f #ef
    487487@(initial_state_intro … Em esb ef) @refl
  • src/Clight/Csem.ma

    r2588 r2608  
    512512  | alloc_variables_cons:
    513513      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    514       alloc m 0 (sizeof ty) XData = 〈m1, b1〉 →
    515       alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 →
     514      alloc m 0 (sizeof ty) (* XData *) = 〈m1, b1〉 →
     515      alloc_variables (add … e id b1) m1 vars e2 m2 →
    516516      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    517517
  • src/Clight/MemProperties.ma

    r2483 r2608  
    227227
    228228lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).
    229 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
     229* #contents #next #nextpos * (*#br1*) #bid1 * (*#br2*) #bid2 normalize
    230230@(eqZb_elim … bid1 bid2)
    231 [ 1: #Heq >Heq cases br1 cases br2 normalize
     231[ 1: #Heq >Heq normalize #H
     232     @False_ind @(absurd … (refl ??) H)
     233(*     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
     234     #_ @refl *)
     235| 2: #Hneq #Hneq' @refl ]
     236qed.
     237
     238lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
     239* #contents #next #nextpos * (* #br1 *) #bid1 * (* #br2 *) #bid2 normalize
     240@(eqZb_elim … bid1 bid2)
     241[ 1: #Heq >Heq (* cases br1 cases br2 *) normalize #H
     242     @False_ind @(absurd … (refl ??) H)
     243(*
    232244     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
    233      #_ @refl
    234 | 2: cases br1 cases br2 normalize #_ #_ @refl ]
    235 qed.
    236 
    237 lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
    238 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
    239 @(eqZb_elim … bid1 bid2)
    240 [ 1: #Heq >Heq cases br1 cases br2 normalize
    241      [ 1,4: * #H @(False_ind … (H (refl ??))) ]
    242      #_ @refl
    243 | 2: cases br1 cases br2 normalize #_ #_ @refl ]
     245     #_ @refl *)
     246| 2: (* cases br1 cases br2 *) normalize #_ #_ @refl ]
    244247qed.
    245248
    246249lemma beloadv_free_blocks_neq :
    247250  ∀m,block,pblock,poff,res.
    248   beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block.
    249 * #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res
     251  beloadv (free m block) (mk_pointer pblock poff) = Some ? res →
     252  pblock ≠ block.
     253* #contents #next #nextpos * (* #br *) #bid * (* #pbr *) #pbid #poff #res
    250254normalize
    251255cases (Zltb pbid next) normalize nodelta
    252256[ 2: #Habsurd destruct (Habsurd) ]
    253 cases pbr cases br normalize nodelta
    254 [ 2,3: #_ % #Habsurd destruct (Habsurd) ]
     257(*cases pbr cases br normalize nodelta *)
    255258@(eqZb_elim pbid bid) normalize nodelta
    256259#Heq destruct (Heq)
    257 [ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
     260[ 1: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
    258261#_ % #H destruct (H) elim Heq #H @H @refl
    259262qed.
     
    517520destruct try @refl
    518521[ 1:
    519   #b' normalize cases b #br #bid cases b' #br' #bid'
    520   cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize
     522  #b' normalize cases b (* #br *) #bid cases b' (* #br' *) #bid'
     523  (* cases br' cases br *) normalize @(eqZb_elim … bid' bid) #H normalize
    521524  try /2 by conj, refl/
    522525| 2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H
    523526| 3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H
    524 | 4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize
     527| 4: normalize cases b (* #br *) #bid (* cases br *) normalize >eqZb_z_z normalize
    525528     >eqZb_z_z @refl
    526 | 5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta
     529| 5: #o #Hneq normalize in ⊢ (??%%); cases b #bid normalize nodelta
    527530     >eqZb_z_z normalize nodelta
    528531     @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs)))
     
    10271030lemma fe_to_be_to_fe_value_ptr :
    10281031  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
    1029 #b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta
    1030 cases br normalize nodelta >eqZb_z_z normalize nodelta
     1032#b * #o whd in ⊢ (??%%); normalize cases b (* #br *) #bid
     1033(* cases br normalize nodelta *) >eqZb_z_z normalize nodelta
    10311034cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
    10321035<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
  • src/Clight/frontend_misc.ma

    r2588 r2608  
    345345
    346346definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_block ?.
    347 * #r1 #id1 * #r2 #id2 @(eqZb_elim … id1 id2)
    348 [ 1: #Heq >Heq cases r1 cases r2 normalize
     347* (*#r1*) #id1 * (*#r2*) #id2 @(eqZb_elim … id1 id2)
     348[ 1: #Heq >Heq (* cases r1 cases r2 * normalize *)
    349349     >eqZb_z_z normalize try // @conj #H destruct (H)
    350      try @refl
    351 | 2: #Hneq cases r1 cases r2 normalize
     350     try @refl @eqZb_z_z
     351| 2: #Hneq (* cases r1 cases r2 *) normalize
    352352     >(eqZb_false … Hneq) normalize @conj
    353353     #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??)))
  • src/Clight/memoryInjections.ma

    r2600 r2608  
    33include "Clight/frontend_misc.ma".
    44
    5 (* This file contains some definitions and lemmas related to memory injections.
    6    Could be useful for the Clight → Cminor. Needs revision: the definitions are
    7    too lax and allow inconsistent embeddings (more precisely, these embeddings do
    8    not allow to prove that the semantics for pointer less-than comparisons is
    9    conserved). *)
    10 
     5(* This file contains some definitions and lemmas related to memory injections. 
     6 * The whole development is quite similar to the one described in the article by
     7 * Leroy & Blazy in J.A.R., except that in Cerco, we describe data down to the byte
     8 * level (similar to the memory model of CompCert v2 but not to the aforementioned
     9 * paper).
     10 * *)
    1111
    1212(* --------------------------------------------------------------------------- *)   
     
    2929
    3030lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
     31
     32lemma eqZb_symmetric : ∀x,y:Z. eqZb x y = eqZb y x.
     33#x #y @(eqZb_elim … x y)
     34[ * >eqZb_z_z @refl
     35| #Hneq >(eqZb_false … (sym_neq ??? Hneq)) @refl ]
     36qed.
    3137
    3238(* --------------------------------------------------------------------------- *)
     
    6066qed.
    6167
     68
    6269lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
    63 #a #b @(eq_block_elim … a b) /2/ qed.
     70* #a * #b
     71cases (decidable_eq_Z … a b)
     72[ * %1 @refl
     73| #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed.
    6474
    6575lemma block_decidable_eq : ∀a,b:block. (a = b) + (a ≠ b).
    66 * #ra #ida * #rb #idb
    67 cases ra cases rb
    68 [ 2: %2 % #H destruct
    69 | 3: %2 % #H destruct
    70 | *: cases (decidable_eq_Z_Type ida idb)
    71   [ 1,3: * %1 @refl
    72   | 2,4: #Hneq %2 % #H destruct (H) cases Hneq #H @H @refl ]
    73 ] qed.
     76* #a * #b
     77cases (decidable_eq_Z_Type … a b)
     78[ * %1 @refl
     79| #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed.
    7480
    7581lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
     
    8288        [ 1: #Heq >Heq /2 by not_to_not/
    8389        | 2: #x @x ]
    84    | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)
     90   | 2: #Hmem1 cases (mem_dec ? block_eq_dec ? tl)
    8591        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
    8692        | 2: #Hmem2 @Hind //
     
    103109   pblock ptr ≠ b →
    104110   valid_pointer (free m b) ptr = true.
    105 * #br #bid * #contents #next #posnext * * #pbr #pbid #poff
     111* (* #br *) #bid * #contents #next #posnext * * (* #pbr *) #pbid #poff
    106112normalize
    107113@(eqZb_elim pbid bid)
    108 [ 1: #Heqid >Heqid cases pbr cases br normalize
    109      [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
     114[ 1: #Heqid >Heqid (* cases pbr cases br normalize *)
    110115     cases (Zltb bid next) normalize nodelta
    111      [ 2,4: #Habsurd destruct (Habsurd) ]
    112      //
    113 | 2: #Hneqid cases pbr cases br normalize try // ]
     116     [ 2: #Habsurd destruct (Habsurd) ]
     117     #_ #H @False_ind @(absurd … (refl ??) H)
     118| 2: #Hneqid (* cases pbr cases br normalize *) try // ]
    114119qed.
    115120
     
    118123whd in match (free ??); @refl qed.
    119124
     125(*
    120126lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr.
    121127   valid_pointer (free m b) ptr = true →
     
    148154     [ 2: % #Heq @Hguard %2 @Heq
    149155     | 1: @H % #Heq @Hguard %1 @Heq ]
    150 ] qed.
     156] qed. *)
    151157
    152158(* An alternative version without the gard on the equality of blocks. *)
     159(*
    153160lemma valid_pointer_free_ok_alt : ∀b : block. ∀m,ptr.
    154161   valid_pointer (free m b) ptr = true →
     
    165172         ]
    166173     | *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ]
    167 ] qed.
     174] qed. *)
    168175
    169176(* Well in fact a valid pointer can be valid even after a free. Ah. *)
     
    207214
    208215(* An embedding is a function from block ids to (blocks × offset). *)
    209 definition embedding ≝ Z → option (block × offset).
     216definition embedding ≝ block → option (block × offset).
    210217
    211218definition offset_plus : offset → offset → offset ≝
     
    224231match p with
    225232[ mk_pointer pblock poff ⇒
    226    match E (block_id pblock) with
     233   match E pblock with
    227234   [ None ⇒ None ?
    228235   | Some loc ⇒
     
    236243definition embedding_compatible : embedding → embedding → Prop ≝
    237244λE,E'.
    238   ∀b:block. E (block_id b) = None ? ∨
    239             E (block_id b) = E' (block_id b).
     245  ∀b:block. E b = None ? ∨
     246            E b = E' b.
    240247
    241248(* We parameterise the "equivalence" relation on values with an embedding. *)
     
    258265 ∀b1,off1,b2,off2,ty,v1.
    259266  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 *)
    260   E (block_id b1) = Some ? 〈b2,off2〉 →
     267  E b1 = Some ? 〈b2,off2〉 →
    261268  load_value_of_type ty m1 b1 off1 = Some ? v1 →
    262269  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
     
    299306definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝
    300307λE.λb.λm,m'.
    301   match E (block_id b) with
     308  match E b with
    302309  [ None ⇒ True
    303310  | Some loc ⇒
     
    313320  ∀b1,b2,b1',b2',delta1,delta2.
    314321  b1 ≠ b2 → (* note that two blocks can be different only becuase of this region *)
    315   E (block_id b1) = Some ? 〈b1',delta1〉 →
    316   E (block_id b2) = Some ? 〈b2',delta2〉 →
    317   (if eqZb (block_id b1') (block_id b2') then
     322  E b1 = Some ? 〈b1',delta1〉 →
     323  E b2 = Some ? 〈b2',delta2〉 →
     324  (if eq_block b1' b2' then
    318325    (* block_is_empty m b1' ∨ *)
    319326    high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
     
    332339  mi_inj : load_sim_ptr E m1 m2;
    333340  (* Invalid blocks are not mapped *)
    334   mi_freeblock : ∀b. ¬ (valid_block m1 b) → E (block_id 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'.
     
    340347  (* Blocks in the codomain are valid *)
    341348  mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
    342   (* Regions are preserved *)
    343   mi_region : ∀b,b',o'. E (block_id b) = Some ? 〈b',o'〉 → block_region b = block_region b';
     349  (* Regions are preserved - this might be superfluous now ?. *)
     350  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
    344351  (* sub-blocks do not overlap (non-aliasing property) *)
    345352  mi_nonalias : non_aliasing E m1;
     
    468475(* If we succeed to load something by value from a 〈b,off〉 location,
    469476   [b] is a valid block. *)
     477(*   
    470478lemma load_by_value_success_valid_block_aux :
    471479  ∀ty,m,b,off,v.
     
    487495     try // #Habsurd destruct (Habsurd)
    488496| *: normalize in Hmode; destruct (Hmode)
    489 ] qed.
     497] qed. *)
    490498
    491499(* If we succeed in loading some data from a location, then this loc is a valid pointer. *)
     
    497505    Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧
    498506    Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.
    499 #ty #m * #brg #bid #off #v
     507#ty #m * (* #brg *) #bid #off #v
    500508cases ty
    501509[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     
    509517     whd in match (beloadv ??);
    510518     cases (Zltb bid (nextblock m)) normalize nodelta
    511      cases (Zleb (low (blocks m (mk_block brg bid)))
     519     cases (Zleb (low (blocks m (mk_block (*brg*) bid)))
    512520                  (Z_of_unsigned_bitvector offset_size (offv off)))
    513      cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block brg bid))))
     521     cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block (*brg*) bid))))
    514522     normalize nodelta
    515523     #Heq destruct (Heq)
     
    567575(* A valid block stays valid after an alloc. *)
    568576lemma alloc_valid_block_conservation :
    569   ∀m,m',z1,z2,r,new_block.
    570   alloc m z1 z2 r = 〈m', new_block〉 →
     577  ∀m,m',z1,z2,(*r,*)new_block.
     578  alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    571579  ∀b. valid_block m b → valid_block m' b.
    572 #m #m' #z1 #z2 #r * #b' #Hregion_eq
    573 elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
     580#m #m' #z1 #z2 (* #r*) * #b' (* #Hregion_eq *)
     581elim m #contents #nextblock #Hcorrect whd in match (alloc ???(*?*));
    574582#Halloc destruct (Halloc)
    575583#b whd in match (valid_block ??) in ⊢ (% → %); /2/
     
    609617
    610618lemma alloc_valid_pointer_conservation :
    611   ∀m,m',z1,z2,r,new_block.
    612   alloc m z1 z2 r=〈m',new_block〉 →
    613   ∀p. block_id (pblock p) ≠ block_id (pi1 … new_block)
     619  ∀m,m',z1,z2,(*r,*)new_block.
     620  alloc m z1 z2 (*r*) = 〈m',new_block〉 →
     621  ∀p. (pblock p) ≠ new_block
    614622      valid_pointer m' p = true →
    615623      valid_pointer m p = true.
    616 #m #m' #z1 #z2 #r * #new_block #Hregion
     624#m #m' #z1 #z2 (*#r*) #new_block
    617625cases m #cont #next #Hnext
    618626whd in ⊢ ((??%%) → ?);
     
    625633whd in match (update_block ?????);
    626634whd in match (update_block ?????);
    627 cut (b ≠ (mk_block r next))
    628 [ @(eq_block_elim … b (mk_block r next)) #H destruct try //
     635cut (b ≠ (mk_block (*r*) next))
     636[ @(eq_block_elim … b (mk_block (*r*) next)) #H destruct try //
    629637  @False_ind
    630638  @(absurd … (refl ??) Hneq) ] #Hneqb
    631639>(not_eq_block … Hneqb) normalize nodelta
    632640#HA #HB % [ % ] try assumption
    633 cases b in Hneqb Hneq Hblock_id; #r' #id * #Hnext_not_id #Hneq
     641cases b in Hneqb Hneq Hblock_id; (* #r'*) #id * #Hnext_not_id #Hneq
    634642#Hlt cut (id ≤ next)
    635643[ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ]
    636 #Hle @Zle_split try @Hle @Hneq
     644#Hle @Zle_split try @Hle % #Heq destruct
     645@(absurd … (refl ??) Hneq)
    637646qed.
    638647
    639648(* Allocating a new zone produces a valid block. *)
    640649lemma alloc_valid_new_block :
    641   ∀m,m',z1,z2,r,new_block.
    642   alloc m z1 z2 r = 〈m', new_block〉 →
     650  ∀m,m',z1,z2(*,r*),new_block.
     651  alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    643652  valid_block m' new_block.
    644 * #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
    645 whd in match (alloc ????); whd in match (valid_block ??);
     653* #contents #nextblock #Hcorrect #m' #z1 #z2 (* #r *) * #new_block (* #Hregion_eq *)
     654whd in match (alloc ???(*?*)); whd in match (valid_block ??);
    646655#Halloc destruct (Halloc) /2/
    647656qed.
     
    649658(* All data in a valid block is unchanged after an alloc. *)
    650659lemma alloc_beloadv_conservation :
    651   ∀m,m',block,offset,z1,z2,r,new_block.
     660  ∀m,m',block,offset,z1,z2,(*r,*)new_block.
    652661    valid_block m block →
    653     alloc m z1 z2 r = 〈m', new_block〉 →
     662    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    654663    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
    655 * #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
     664* #contents #next #Hcorrect #m' #block #offset #z1 #z2 (* #r*) #new_block #Hvalid #Halloc
    656665whd in Halloc:(??%?); destruct (Halloc)
    657666whd in match (beloadv ??) in ⊢ (??%%);
     
    661670cut (eqZb (block_id block) next = false)
    662671[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq
    663 >Hneq cases (eq_region ??) normalize nodelta  @refl
     672>Hneq @refl
    664673qed.
    665674
    666675(* Lift [alloc_beloadv_conservation] to loadn *)
    667676lemma alloc_loadn_conservation :
    668   ∀m,m',z1,z2,r,new_block.
    669     alloc m z1 z2 r = 〈m', new_block〉 →
     677  ∀m,m',z1,z2,(*r,*)new_block.
     678    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    670679    ∀n. ∀block,offset.
    671680    valid_block m block →
    672681    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
    673 #m #m' #z1 #z2 #r #new_block #Halloc #n
     682#m #m' #z1 #z2 (*#r*) #new_block #Halloc #n
    674683elim n try //
    675684#n' #Hind #block #offset #Hvalid_block
     
    682691
    683692lemma alloc_load_value_of_type_conservation :
    684   ∀m,m',z1,z2,r,new_block.
    685     alloc m z1 z2 r = 〈m', new_block〉 →
     693  ∀m,m',z1,z2(*,r*),new_block.
     694    alloc m z1 z2 (*r*) = 〈m', new_block〉 →
    686695    ∀block,offset.
    687696    valid_block m block →
    688697    ∀ty. load_value_of_type ty m block offset =
    689698         load_value_of_type ty m' block offset.
    690 #m #m' #z1 #z2 #r #new_block #Halloc #block #offset #Hvalid         
     699#m #m' #z1 #z2 (*#r*) #new_block #Halloc #block #offset #Hvalid         
    691700#ty cases ty
    692701[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     
    701710lemma alloc_memory_inj_m2 :
    702711  ∀E:embedding.
    703   ∀m1,m2,m2',z1,z2,r,new_block.
     712  ∀m1,m2,m2',z1,z2(*,r*),new_block.
    704713  ∀H:memory_inj E m1 m2.
    705   alloc m2 z1 z2 r = 〈m2', new_block〉 →
     714  alloc m2 z1 z2 (*r*) = 〈m2', new_block〉 →
    706715  block_implementable_bv m2' new_block →
    707716  memory_inj E m1 m2'.
    708 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc #Himpl
     717#E #m1 #m2 #m2' #z1 #z2 (*#r*) * #new_block (* #Hregion *) #Hmemory_inj #Halloc #Himpl
    709718%
    710719[ whd
     
    727736| #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
    728737     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
    729      elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
     738     elim p' * (*#br'*) #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
    730739     whd in match (valid_pointer ??) in ⊢ (% → %);
    731740     @Zltb_elim_Type0
    732741     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
    733      #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
     742     #Hbid' cut (Zltb bid' (Zsucc new_block) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
    734743     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
    735744     whd in match (high_bound ??) in ⊢ (% → %);
    736745     whd in match (update_block ?????);
    737746     whd in match (eq_block ??);
    738      cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]
    739      #Hbid_neq >Hbid_neq
    740      cases (eq_region br' r) normalize #H @H
     747     cut (eqZb bid' new_block = false) [ 1: @eqZb_false /2 by not_to_not/ ]
     748     #Hbid_neq >Hbid_neq #H @H
     749(*     cases (eq_region br' r) normalize #H @H*)
    741750| #b #b' #o' #Hembed lapply (mi_nodangling … Hmemory_inj b b' o' Hembed) #H
    742751  @(alloc_valid_block_conservation … Halloc … H)
     
    745754| #b lapply (mi_nowrap … Hmemory_inj b)
    746755   whd in ⊢ (% → %);
    747    lapply (mi_nodangling … Hmemory_inj (block_id b))
    748    cases (E (block_id b)) normalize nodelta try //
     756   lapply (mi_nodangling … Hmemory_inj b)
     757   cases (E b) normalize nodelta try //
    749758   * #B #OFF normalize nodelta #Hguard
    750759   * * #H1 #H2 #Hinbounds @conj try @conj try assumption
    751    @(eq_block_elim … new_block B)
     760   @(eq_block_elim … (mk_block new_block) B)
    752761   [ #H <H assumption
    753762   | #H cases m2 in Halloc H2; #contents #nextblock #notnull
     
    767776lemma alloc_memory_inj_m1 :
    768777  ∀E:embedding.
    769   ∀m1,m2,m1',z1,z2,r,new_block.
     778  ∀m1,m2,m1',z1,z2,(*r,*)new_block.
    770779  ∀H:memory_inj E m1 m2.
    771   alloc m1 z1 z2 r = 〈m1', new_block〉 →
    772   memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then None ? else E x) m1' m2 ∧
    773   embedding_compatible E (λx. if eqZb (block_id (pi1 … new_block)) x then None ? else E x).
    774 #E #m1 #m2 #m1' #z1 #z2 #r * #new_block #Hregion_eq #Hinj #Halloc
    775 cut (E (block_id new_block) = None ?)
     780  alloc m1 z1 z2 (*r*) = 〈m1', new_block〉 →
     781  memory_inj (λx. if eq_block new_block x then None ? else E x) m1' m2 ∧
     782  embedding_compatible E (λx. if eq_block new_block x then None ? else E x).
     783#E #m1 #m2 #m1' #z1 #z2 (* #r*) #new_block (* #Hregion_eq *) #Hinj #Halloc
     784cut (E new_block = None ?)
    776785[ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?);
    777786  #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
    778787#Hempty
    779788cut (embedding_compatible E
    780      (λx:Z.
    781        if eqZb (block_id new_block) x
    782        then None (block×offset) 
    783        else E x ))
    784 [ whd #b @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta try // #Heq <Heq %1 @Hempty ]
     789     (λx.
     790       if eq_block new_block x
     791       then None (block×offset)
     792       else E x))
     793[ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 @Hempty ]
    785794#Hembedding_compatible @conj try assumption
    786795%
    787796[ whd #b1 #off1 #b2 #off2 #ty #v1
    788797  @(eq_block_elim … b1 new_block)
    789   [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eqZb_z_z normalize nodelta
     798  [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta
    790799    #Habsurd destruct ]
    791800  #Hneq #Hvalid
    792801  whd in ⊢ ((??%?) → ?);
    793   @(eqZb_elim … (block_id new_block) (block_id b1))
     802  @(eq_block_elim … new_block b1)
    794803  normalize nodelta
    795804  [ #Heq #Habsurd destruct (Habsurd) ]
     
    806815  %{v2} @conj try assumption
    807816  @(embedding_compatibility_value_eq … Hveq2) assumption
    808 | #b #Hnot_valid @(eqZb_elim … (block_id new_block) (block_id b))
     817| #b #Hnot_valid @(eq_block_elim … new_block b)
    809818  normalize nodelta
    810819  [ #Heq @refl
     
    814823  cases p #b #o cases p' #b' #o' normalize nodelta #Hvalidptr #Hvalid1'
    815824  whd in ⊢ ((??%%) → ?); 
    816   @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta
     825  @(eq_block_elim … new_block b) normalize nodelta
    817826  [ #Heq #Habsurd destruct ]
    818827  #Hneq #Hembed
     
    820829  #Hvalid1
    821830  @(Hvalidptr Hvalid1 Hembed)
    822 | #b #b' #o' @(eqZb_elim … (block_id new_block) b)
     831| #b #b' #o' @(eq_block_elim … new_block b)
    823832  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
    824833  normalize nodelta #Henq
    825834  @(mi_nodangling … Hinj)
    826 | #b #b' #o' @(eqZb_elim … (block_id new_block) (block_id b))
     835| #b #b' #o' @(eq_block_elim … new_block b)
    827836  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
    828837  #Hneq @(mi_region … Hinj)
    829838| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
    830   @(eqZb_elim … (block_id new_block) (block_id b1))
     839  @(eq_block_elim … new_block b1)
    831840  normalize nodelta
    832841  [ #Heq #Habsurd destruct (Habsurd) ]
    833842  #Hneq1 #Hembed1
    834   @(eqZb_elim … (block_id new_block) (block_id b2))
     843  @(eq_block_elim … new_block b2)
    835844  normalize nodelta
    836845  [ #Heq #Habsurd destruct (Habsurd) ]
    837846  #Hneq2 #Hembed2
    838   @(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta try //
     847  @(eq_block_elim … b1' b2') normalize nodelta try //
    839848  #Heq
    840849  lapply (mi_nonalias … Hinj … b1 b2 b1' b2' delta1 delta2 Hneq Hembed1 Hembed2) >Heq
    841   >eqZb_z_z normalize nodelta
     850  >eq_block_b_b normalize nodelta
    842851  cases m1 in Halloc; #contents #next #Hnext
    843852  >unfold_high_bound >unfold_low_bound
     
    845854  >unfold_high_bound >unfold_low_bound
    846855  >unfold_high_bound >unfold_low_bound
    847   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    848   cut (eq_block b1 (mk_block r next) = false)
    849   [ whd in ⊢ (??%%);
    850     >(eqZb_false … (sym_neq ??? Hneq1))
    851     cases (eq_region ??) @refl ]
    852   cut (eq_block b2 (mk_block r next) = false)
    853   [ whd in ⊢ (??%%);
    854     >(eqZb_false … (sym_neq ??? Hneq2))
    855     cases (eq_region ??) @refl ]
     856  whd in ⊢ ((??%%) → ?); destruct (Heq) #Heq destruct (Heq)
     857  lapply (neq_block_eq_block_false … (sym_neq ??? Hneq1))
     858  lapply (neq_block_eq_block_false … (sym_neq ??? Hneq2))
    856859  #Heq_block_2
    857860  #Heq_block_1
     
    876879    >Heq_block_1 >Heq_block_2 @H
    877880  ]
    878 | #b whd @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta try //
     881| #b whd @(eq_block_elim … new_block b) normalize nodelta try //
    879882  #Hneq lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?);
    880   cases (E (block_id b)) normalize nodelta try //
     883  cases (E b) normalize nodelta try //
    881884  * #bb #oo normalize nodelta
    882885  * * * #HA #HB * #HC #HD #HE @conj try @conj
     
    892895 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) try //
    893896 whd in match (update_block ?????);
    894  cut (eq_block b (mk_block r next) = false)
    895  [ 1,3,5: whd in ⊢ (??%%);
    896           >(eqZb_false … (sym_neq ??? Hneq))
    897           cases (eq_region ??) @refl
     897 cut (eq_block b (mk_block next) = false)
     898 [ 1,3,5: @neq_block_eq_block_false @(sym_neq … Hneq)
    898899 | 2,4,6: #Heq_block >Heq_block // ]
    899 ] qed.
    900  
    901        
     900] qed.
     901
     902(* In CompCert, "∀v. value_eq Vundef v" holds. Not in our developments. In order
     903 * to prove the equivalent of lemma 68 of L&B, we need to provide an additional
     904 * property of the target memory: the /target/ portion of memory we are going to map a block
     905 * to must only contains BVundef (whereas in CompCert, the fact that the source block
     906 * contains BVundefs is enough to proceed).
     907 *
     908 * The following definition expresses the fact that a portion of memory [z1; z2] contains only
     909 * BVundefs.
     910 * Note that the bounds are /inclusive/. We do not check for their validity. *)
     911definition undef_memory_zone : mem → block → Z → Z → Prop ≝
     912  λm,b,z1,z2.
     913    ∀i. z1 ≤ i → i ≤ z2 → contents (blocks m b) i = BVundef.
     914
     915(* Explictly stating the properties of alloc. *)
     916lemma alloc_properties :
     917  ∀m,m',z1,z2(*,r*),b.
     918   alloc m z1 z2 (* r *) = 〈m',b〉 →
     919   low_bound m' b = z1 ∧
     920   high_bound m' b = z2 ∧
     921   undef_memory_zone m' b z1 z2.
     922#m #m'  #z1 #z2 * (* #br *) #bid
     923cases m #contents #next #Hnext
     924whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     925>unfold_low_bound >unfold_high_bound
     926@conj try @conj
     927/2 by refl, pair_destruct_2/
     928whd
     929#i #H1 #H2 whd in match (update_block ?????);
     930>eq_block_b_b normalize nodelta @refl
     931qed.
     932
     933(* Embed a fresh block inside an unmapped portion of the target block.
     934 * This is the equivalent of lemma 68 of Leroy&Blazy.
     935 * Compared to L&B, an additional "undef_memory_zone" proof object must be provided.
     936 *)
     937lemma alloc_memory_inj_m1_to_m2 :
     938  ∀E:embedding.
     939  ∀m1,m2,m1':mem.
     940  ∀z1,z2:Z.
     941  ∀target,new_block.
     942  ∀delta:offset.
     943  valid_block m2 target →
     944  alloc m1 z1 z2 = 〈m1', new_block〉 →
     945  low_bound m2 target ≤ z1 + Zoo delta →
     946  z2 + Zoo delta ≤ high_bound m2 target →
     947  undef_memory_zone m2 target (z1 + Zoo delta) (z2 + Zoo delta) →
     948  (∀b,delta'. b ≠ new_block →
     949              E b = Some ? 〈target, delta'〉 →
     950              high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨
     951              z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) →
     952  memory_inj E m1 m2 →
     953  memory_inj (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x) m1' m2.
     954#E #m1 #m2 #m1' #z1 #z2 (* * #tr *) #tid (* * * #newr *) #newid (* * *) #delta
     955#Hvalid #Halloc #Hlow #Hhigh #Hundef_zone #Hno_interference #Hinj
     956cut (E newid = (None ?))
     957[ @(mi_freeblock ??? Hinj newid) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj
     958  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
     959@cthulhu
     960qed.
     961(*
     962#Hnew_not_mapped
     963cut (embedding_compatible E (λx. if eqZb newid x then Some ? 〈mk_block newr tid, delta〉 else E x))
     964[ whd #b @(eqZb_elim … newid (block_id b)) normalize nodelta try // #Heq <Heq %1 assumption ]
     965#Hembedding_compatible
     966%
     967[ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid' #Hembed #Hload
     968  @(eqZb_elim … newid (block_id b1))
     969  [ 2: (* we do not load from the newly allocated block *)
     970     #Hneq
     971     (* prove that we can equivalently load from the memory before alloc *)
     972     cases (some_inversion ????? Hembed) * #target' #delta'
     973     >(eqZb_false … Hneq) normalize nodelta
     974     * #Hembed #Heq destruct (Heq)
     975     cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block' #Hlow #Hhigh
     976     lapply (alloc_valid_block_conservation2 … Halloc … (sym_neq ??? Hneq) Hvalid_block')
     977     #Hvalid_block
     978     lapply (alloc_load_value_of_type_conservation … Halloc b1 off1 … Hvalid_block ty)
     979     #Heq_load <Heq_load in Hload; #Hload
     980     lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … (sym_neq ??? Hneq) Hvalid')     
     981     #Hvalid_ptr
     982     lapply (mi_inj … Hinj b1 off1 b2 (offset_plus off1 delta') … Hvalid_ptr … Hload)
     983     [ whd in ⊢ (??%?); >Hembed @refl ]
     984     (* conclude *)
     985     * #v2 * #Hload2 #Hvalue_eq %{v2} @conj
     986     [ @Hload2
     987     | @(embedding_compatibility_value_eq … Hvalue_eq) @Hembedding_compatible ]
     988  | 1: (* we allegedly performed a load from a block with the same id as
     989        * the newly allocated block (which by def. of alloc contains only BVundefs) *)
     990     #Heq destruct (Heq)
     991     whd in Hembed:(??%?); >eqZb_z_z in Hembed; normalize nodelta
     992     #Heq_ptr
     993     (* cull out all boring cases *)
     994     lapply Hload -Hload cases ty
     995     [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     996     | #structname #fieldspec | #unionname #fieldspec | #id ]
     997     [ 1,6,7: whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
     998     | 4,5: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq_ptr Heq)
     999            %{(Vptr (mk_pointer (mk_block newr tid) (offset_plus off1 delta)))}
     1000            @conj
     1001            [ 1,3: @refl
     1002            | *: %4 whd in ⊢ (??%?); >eqZb_z_z @refl ] ]
     1003     (* Now: load-by-value cases. Outcome is either None or Undef. *)
     1004     lapply (load_by_value_after_alloc_undef m1 m1' z1 z2 b1 ?)
     1005     [ 1,3,5:
     1006     #Hload_eq
     1007     [ lapply (Hload_eq (Tint sz sg) (refl ??) off1)
     1008     | lapply (Hload_eq (Tpointer ptr_ty) (refl ??) off1)
     1009     | lapply (Hload_eq (Tcomp_ptr id) (refl ??) off1) ]
     1010     *
     1011     (* None case: absurd *)
     1012     [ 2,4,6: >Hload #Habsurd destruct (Habsurd) ]
     1013         >Hload #Heq destruct (Heq) %{Vundef}
     1014         @conj try //
     1015         cut (valid_pointer m2 (mk_pointer b2 (offset_plus off1 delta))=true)
     1016         [ 1,3,5: @valid_pointer_of_Prop @conj try @conj
     1017            [ 1,4,7: assumption
     1018            | 2,5,8: >unfold_low_bound
     1019         lapply (alloc_properties … Halloc) * *
     1020         >unfold_low_bound >unfold_high_bound #Hlow #Hhigh #Hundef
     1021         lapply (valid_pointer_to_Prop … Hvalid') * *
     1022         #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow >Hhigh
     1023*)
    9021024
    9031025(* Embed a fresh block inside an unmapped portion of the target block.
    9041026 * This is the equivalent of lemma 68 for Leroy&Blazy. *)
     1027(*
    9051028axiom alloc_memory_inj_m1_to_m2 :
    9061029  ∀E:embedding.
     
    9191042  memory_inj E m1 m2 →
    9201043  memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then Some ? 〈b2, delta〉 else E x) m1' m2.
     1044*)
    9211045
    9221046(* -------------------------------------- *)
     
    9691093  load_sim_ptr E m1 m2 →
    9701094  ∀b. free m2 b = m2' →
    971       (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
     1095      (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
    9721096      load_sim_ptr E m1 m2'.     
    9731097#E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped
     
    10541178#b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
    10551179#Hembed1 #Hembed2
    1056 @(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta
     1180@(eq_block_elim … b1' b2') normalize nodelta
    10571181[ 2: try // ]
    10581182#Hblocks_eq
     
    10601184lapply Hembed1 -Hembed1
    10611185lapply Hblocks_eq -Hblocks_eq
    1062 cases b1' #r1' #bid1'
    1063 cases b2' #r2' #bid2'
     1186(*cases b1' #r1' #bid1'
     1187  cases b2' #r2' #bid2' *)
    10641188#Heq destruct (Heq)
    1065 generalize in match bid2';
     1189generalize in match b2';
    10661190#target #Hembed1 #Hembed2
    10671191lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2)
    1068 >eqZb_z_z normalize nodelta
     1192>eq_block_b_b normalize nodelta
    10691193normalize nodelta <Hfree
    10701194@(eq_block_elim … b1 b)
     
    11121236| @(free_non_aliasing_m1 … Hinj … Hfree)
    11131237| #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?);
    1114   cases (E (block_id bb)) normalize nodelta try //
     1238  cases (E bb) normalize nodelta try //
    11151239  * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj
    11161240  try //
     
    11401264  memory_inj E m1 m2 →
    11411265  ∀b. free m2 b = m2' →
    1142       (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 →
     1266      (∀b1,delta. E b1 = Some ? 〈b, delta〉 →
    11431267      (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → 
    11441268      memory_inj E m1 m2'.
     
    11711295| @Hregion
    11721296| #bb lapply (Himpl bb)
    1173   whd in ⊢ (% → %); cases (E (block_id bb)) normalize nodelta try //
     1297  whd in ⊢ (% → %); cases (E bb) normalize nodelta try //
    11741298  * #BLO #OFF normalize nodelta * * destruct (Hfree)
    11751299  #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption
     
    11911315  memory_inj E m1 m2 →
    11921316  ∀blocklist,b2.
    1193   (∀b1,delta. E (block_id b1) = Some ? 〈b2, delta〉 → meml ? b1 blocklist) →
     1317  (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) →
    11941318  free m2 b2 = m2' →
    11951319  free_list m1 blocklist = m1' →
     
    12531377       else false) normalize nodelta
    12541378[ 2: #Habsurd destruct (Habsurd) ]
    1255 #Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
    1256 cases rr cases wr normalize try //
    1257 @(eqZb_elim … rid wid)
    1258 [ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
    1259 try //
     1379#Heq destruct (Heq)
     1380cases (Zltb (block_id rb) (nextblock mA)) normalize nodelta try //
     1381cut (eqZb (block_id rb) (block_id wb) = false)
     1382[ >eqZb_symmetric @Hblock_neq ]
     1383#Heqzb >Heqzb normalize nodelta @refl
    12601384qed.
    12611385
     
    13271451    memory_inj E mA mB →
    13281452    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
    1329     ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 →
     1453    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
    13301454    high_bound mA b1 + Zoo delta < Zoo wo →
    13311455    ∀ty,off.
     
    14051529    memory_inj E mA mB →
    14061530    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
    1407     ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 →
     1531    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
    14081532    Zoo wo < low_bound mA b1 + Zoo delta →
    14091533    ∀ty,off.
     
    14221546  ∀block2. ∀i : offset. ∀ty : type.
    14231547  (∀block1,delta.
    1424     E (block_id block1) = Some ? 〈block2, delta〉 →
     1548    E block1 = Some ? 〈block2, delta〉 →
    14251549    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
    14261550  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
     
    14781602  ∀block2. ∀i : offset. ∀ty : type.
    14791603  (∀block1,delta.
    1480     E (block_id block1) = Some ? 〈block2, delta〉 →
     1604    E block1 = Some ? 〈block2, delta〉 →
    14811605    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
    14821606  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
     
    15081632  >(Hnext_eq) try //
    15091633| #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %);
    1510   cases (E (block_id b)) try //
     1634  cases (E b) try //
    15111635  * #BLO #OFF normalize nodelta * *
    15121636  #Hb #HBLO #Hbound try @conj try @conj try assumption
     
    15261650lemma be_to_fe_value_ptr :
    15271651  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
    1528 #b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta
    1529 cases br normalize nodelta >eqZb_z_z normalize nodelta
     1652#b * #o whd in ⊢ (??%%); normalize cases b (* #br *) #bid normalize nodelta
     1653(*cases br normalize nodelta *) >eqZb_z_z normalize nodelta
    15301654cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
    15311655<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
     
    15701694  ∀E,m1,m2.
    15711695  memory_inj E m1 m2 →
    1572   ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 →
     1696  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
    15731697  ∀v1,v2. value_eq E v1 v2 →
    15741698  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
     
    16391763  ∀E,m1,m2.
    16401764  memory_inj E m1 m2 →
    1641   ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 →
     1765  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
    16421766  ∀v1,v2. value_eq E v1 v2 →
    16431767  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
     
    16621786  ∀Hinj:memory_inj E m1 m2.
    16631787  ∀v1,v2. value_eq E v1 v2 →
    1664   ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 →
     1788  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
    16651789  ∀ty,i,m1'.
    16661790  ast_typ_consistent_with_value ty v1 →
     
    17501874  ∀Hinj:memory_inj E m1 m2.
    17511875  ∀v1,v2. value_eq E v1 v2 →
    1752   ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 →
     1876  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
    17531877  ∀ty,i,m1'.
    17541878  type_consistent_with_value ty v1 →
     
    17701894  ∀Hinj:memory_inj E m1 m2.
    17711895  ∀ty,b,i,v.
    1772   E (block_id b) = None ? →
     1896  E b = None ? →
    17731897  store_value_of_type ty m1 b i v = Some ? m1' →
    17741898  load_sim_ptr E m1' m2.
     
    18201944  ∀Hinj:memory_inj E m1 m2.
    18211945  ∀ty,b,i,v.
    1822   E (block_id b) = None ? →
     1946  E b = None ? →
    18231947  store_value_of_type ty m1 b i v = Some ? m1' →
    18241948  memory_inj E m1' m2.
     
    18491973    | #bb whd
    18501974      lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?);
    1851       cases (E (block_id bb)) normalize nodelta try // * #bb' #off
     1975      cases (E bb) normalize nodelta try // * #bb' #off
    18521976      normalize nodelta
    18531977      whd in match (block_implementable_bv ??);     
     
    19522076          @(ex_intro … (conj … (refl …) ?))
    19532077          @vptr_eq whd in match (pointer_translation ??);
    1954           cases (E (block_id b1')) in Hembed;
     2078          cases (E b1') in Hembed;
    19552079          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    19562080          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     
    19942118     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    19952119     elim p1 in Hembed; #b1 #o1 normalize nodelta
    1996      cases (E (block_id b1))
     2120     cases (E b1)
    19972121     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    19982122     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     
    20932217          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    20942218          elim p1 in Hembed; #b1 #o1 normalize nodelta
    2095           cases (E (block_id b1))
     2219          cases (E b1)
    20962220          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    20972221          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     
    21092233               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
    21102234               whd in ⊢ ((??%?) → (??%?) → ?);
    2111                cases (E (block_id b1')) normalize nodelta
     2235               cases (E b1') normalize nodelta
    21122236               [ 1: #Habsurd destruct (Habsurd) ]
    21132237               * #dest_block #dest_off normalize nodelta
     
    25152639          lapply (mi_nowrap … Hinj bq1)
    25162640          whd in ⊢ (% → ?);
    2517           cases (E (block_id bq1)) normalize nodelta
     2641          cases (E bq1) normalize nodelta
    25182642          [ #_ #Habsurd destruct ]
    25192643          * #BLO #OFF normalize nodelta * *         
     
    25362660          lapply (mi_region … Hinj bq1)
    25372661          lapply (mi_region … Hinj bp1)
    2538           cases (E (block_id bq1)) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
     2662          cases (E bq1) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    25392663          * #BLOq #DELTAq normalize nodelta
    2540           cases (E (block_id bp1)) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
     2664          cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
    25412665          * #BLOp #DELTAp normalize nodelta #Hregion1 #Hregion2 #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
    25422666          lapply (Hregion1 … (refl ??)) lapply (Hregion2 … (refl ??)) -Hregion1 -Hregion2
     
    25562680          lapply (valid_pointer_to_Prop … Hvalid')
    25572681          * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp
    2558           >eqZb_z_z >eq_block_b_b normalize nodelta
     2682          >eq_block_b_b normalize nodelta
    25592683          *
    25602684          [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
  • src/Clight/switchRemoval.ma

    r2588 r2608  
    11881188  beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res.
    11891189* #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2 #writeable
    1190 * #br #bid * * #pr #pid #poff #res #Hext
     1190* (* #br *) #bid * * (* #pr *) #pid #poff #res #Hext
    11911191(*#Hme_nonempty #Hme_writeable #Hme_nonempty #Hvalid_conserv*)
    11921192#Hload
     
    12231223     [ 1: lapply Hvalid normalize //
    12241224     | 2: lapply Hlh normalize
    1225           cases (block_region b) normalize nodelta
    1226           cases (block_region bl) normalize nodelta try //
    12271225          @(eqZb_elim … (block_id b) (block_id bl))
    12281226          [ 1,3: * normalize *
     
    12321230lemma eqb_to_eq_block : ∀a,b : block. a == b = eq_block a b.
    12331231#a #b lapply (eqb_true ? a b) @(eq_block_elim … a b)
    1234 /2 by neq_block_eq_block_false, true_to_andb_true/
     1232#H #I
     1233try /2 by neq_block_eq_block_false, true_to_andb_true/
     1234cases I #J #K @K @H
    12351235qed.
    12361236
     
    13621362     #b normalize >Hcontents_eq @refl
    13631363| 5: #x1 #x2 #acc normalize @conj try @refl
    1364      * * #id normalize nodelta cases (block_region x1)
     1364     * (* * *) #id normalize nodelta cases (block_region x1)
    13651365     cases (block_region x2) normalize nodelta
    13661366     @(eqZb_elim id (block_id x1)) #Hx1 normalize nodelta
    13671367     @(eqZb_elim id (block_id x2)) #Hx2 normalize nodelta try @refl
    1368 | 6: * #r #i * #contents #nextblock #Hpos @conj
     1368| 6: * (* #r *) #i * #contents #nextblock #Hpos @conj
    13691369     [ 1: @refl
    1370      | 2: #b normalize cases (block_region b) normalize
    1371           cases r normalize cases (eqZb (block_id b) i)
     1370     | 2: #b normalize (* cases (block_region b) normalize
     1371          cases r normalize *) cases (eqZb (block_id b) i)
    13721372          normalize @refl
    13731373     ]
     
    16501650     [ 1: normalize cases H //
    16511651     | 2: cases H normalize #Hb_lt #Hb_nonempty2
    1652           cases (block_region b)
    1653           cases (block_region wb) normalize nodelta
    1654           //
     1652          (*
     1653            cases (block_region b)
     1654            cases (block_region wb) *)
    16551655          @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta
    16561656          // ]
     
    17051705            (nextblock m) (nextblock_pos m)) b.
    17061706#m #b #wb #offset #v * #Hvalid #Hnonempty % //
    1707 cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize
    1708 cases br normalize nodelta cases wbr normalize nodelta //
     1707cases b in Hvalid Hnonempty; (* #br *) #bid cases wb (* #wbr *) #wbid normalize
     1708(* cases br *) normalize nodelta (* cases wbr normalize nodelta // *)
    17091709@(eqZb_elim … bid wbid) // #Heq #Hlt normalize //
    17101710qed.
     
    17201720  nonempty_block m b.
    17211721#m #b #wb #offset #v * #Hvalid #Hnonempty % //
    1722 cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize
    1723 cases br normalize nodelta cases wbr normalize nodelta //
     1722cases b in Hvalid Hnonempty; (* #br *) #bid cases wb (* #wbr *) #wbid normalize
     1723(* cases br normalize nodelta cases wbr normalize nodelta // *)
    17241724@(eqZb_elim … bid wbid) // #Heq #Hlt normalize //
    17251725qed.
     
    17641764     @conj
    17651765     [ 1: @nonempty_block_update_ok //
    1766      | 2: normalize cases b in HB; #br #bid cases wb #wbr #wbid
    1767           cases br cases wbr normalize nodelta
    1768           @(eqZb_elim … bid wbid) normalize nodelta //
    1769           #Hid_eq >Hid_eq #Hblock_eq >Hblock_eq @refl ]
     1766     | 2: normalize (* cases b in HB; #br #bid cases wb #wbr #wbid
     1767          cases br cases wbr normalize nodelta *)
     1768          @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta //
     1769          #Hid_eq cut (b = wb)
     1770          [ cases b in Hid_eq; cases wb #wid #bid #H >H @refl ]
     1771          #Hblock_eq destruct (Hblock_eq) >HB @refl ]
    17701772| 2: #b #Hmem lapply (me_writeable_valid … Hext … Hmem) @nonempty_block_update_ok
    17711773| 3: #b #Hnonempty lapply (nonempty_block_update_ok2 … Hnonempty)
  • src/Clight/toCminorCorrectnessExpr.ma

    r2601 r2608  
    3636      | Some cl_blo ⇒
    3737        (* global symbols are mapped to themselves. Perhaps too strong. *)
    38         E (block_id cl_blo) = Some ? 〈cl_blo, zero_offset〉
     38        E cl_blo = Some ? 〈cl_blo, zero_offset〉
    3939      ]
    4040    | Some cl_blo ⇒
     
    4444            match vtype with
    4545            [ Stack n ⇒
    46               E (block_id cl_blo) = Some ? 〈sp, mk_offset (repr I16 n)〉
     46              E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
    4747            | Local ⇒
    4848              ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
     
    9898| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
    9999  whd in ⊢ ((??%?) → ? → ?);
    100   cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
     100  cases (alloc m 0 (sizeof ty') (*XData*)) #m0 #b (* #Hregion *)
    101101  normalize nodelta #Hexec #Hlookup
    102102  lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
    103103  cases env #env cases id' #id' cases var #var normalize
    104104  @(eqb_elim … id' var)
    105   [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
     105  [ 2: #Hneq * #Hlookup' #Hexists'
     106       lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
    106107       #Heq <Heq @conj try @Hlookup' % *
    107108       [ #Heq' destruct (Heq') cases Hneq #H @H @refl
     
    364365     destruct (Hexec_alloc) %1 @Hlookup
    365366| 2: * #id #ty #tail #Hind
    366      #init_env #env #var #clb #m #m' #Hlookup     
     367     #init_env #env #var #clb #m #m' #Hlookup
    367368     whd in ⊢ (??%? → ?);
    368      cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
     369     cases (alloc m 0 (sizeof ty) (*XData*)) #m0 #blo normalize nodelta
    369370     #Hexec_alloc
    370371     @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
     
    22122213       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
    22132214       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
    2214        cases (E (block_id cl_blo)) in Hptr_translate; normalize nodelta
     2215       cases (E cl_blo) in Hptr_translate; normalize nodelta
    22152216       [ #H destruct (H) ]
    22162217       * #BL #OFF normalize nodelta #Heq destruct (Heq)
  • src/Clight/toCminorOps.ma

    r2601 r2608  
    192192lapply H1 lapply H2 -H1 -H2
    193193whd in ⊢ ((??%?) → (??%?) → ?);
    194 cases (E (block_id b2)) normalize nodelta
     194cases (E b2) normalize nodelta
    195195[ #Habsurd destruct ]
    196196* #bx #ox normalize nodelta #Heq1 #Heq2 destruct
  • src/Cminor/Cminor_semantics.ma

    r2601 r2608  
    343343    match fd with
    344344    [ Internal f ⇒ err_to_io ?? (trace × state) (
    345         let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) XData in
     345        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) (* XData *) in
    346346        ! en ← bind_params args (f_params f);
    347347        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
  • src/RTLabs/RTLabs_semantics.ma

    r2601 r2608  
    175175        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
    176176           here *)
    177         let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) XData in
     177        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) (* XData *) in
    178178        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
    179179    | External fn ⇒
     
    294294| * #fn #args #retdst #stk #m #tr #s'
    295295  whd in ⊢ (??%? → ?);
    296   [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     296  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
    297297    #E destruct %3
    298298  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
     
    342342| * #fn #args #retdst #stk #m #tr #fd' #args' #dst' #fs' #m'
    343343  whd in ⊢ (??%? → ?);
    344   [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     344  [ @bind_res_value #loc #Eloc cases (alloc m O ?(*?*)) #m' #b whd in ⊢ (??%? → ?);
    345345    #E destruct
    346346  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
  • src/RTLabs/RTLabs_traces.ma

    r2601 r2608  
    540540cases fd
    541541[ #fn whd in ⊢ (??%? → % → ?);
    542   @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) XData)
     542  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) (*XData*))
    543543  #m' #b whd in ⊢ (??%? → ?); #E' destruct
    544544  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
  • src/common/ByteValues.ma

    r2470 r2608  
    55include "common/Pointers.ma".
    66include "utilities/hide.ma".
     7
    78
    89definition cpointer ≝ Σp.ptype p = Code.
     
    1011unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
    1112unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
     13
    1214
    1315(* this is like a code pointer, but with unbounded offset.
  • src/common/GenMem.ma

    r2332 r2608  
    4949  λA,x,v,f.
    5050    λy.match eq_block y x with [ true ⇒ v | false ⇒ f y ].
    51    
     51
    5252lemma update_block_s:
    5353  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    5454  update_block … x v f x = v.
    55 #A * * #ix #v #f whd in ⊢ (??%?);
     55#A * #ix #v #f whd in ⊢ (??%?);
    5656>eq_block_b_b //
    5757qed.
     
    119119qed.
    120120
    121 let rec alloc (m:mem) (lo:Z) (hi:Z) (r:region) on m : mem × Σb:block. block_region b = r
    122   let b ≝ mk_block r (nextblock … m) in
     121let rec alloc (m:mem) (lo:Z) (hi:Z) (*(r:region)*) on m : mem × block (*Σb:block. block_region b = r *)
     122  let b ≝ mk_block (nextblock … m) in
    123123  〈mk_mem
    124124    (update_block … b
     
    128128    (succ_nextblock_pos … m),
    129129    b〉.
    130 % qed.
     130(* % qed. *)
    131131
    132132(* Freeing a block.  Return the updated memory state where the given
  • src/common/Globalenvs.ma

    r2601 r2608  
    4747  symbols: identifier_map SymbolTag block;
    4848  functions_inv: ∀b. lookup_opt ? b functions ≠ None ? →
    49                  ∃id. lookup … symbols id = Some ? (mk_block Code (neg b))
     49                 ∃id. lookup … symbols id = Some ? (mk_block (*Code*) (neg b))
    5050}.
    5151
     
    6262  [ None ⇒ functions … g
    6363  | Some b' ⇒
    64       match b' with
     64      match block_id b' with
     65      [ neg p ⇒
     66        pm_set … p (None ?) (functions … g)
     67      | _ ⇒ functions … g
     68      ]
     69(*    match b' with
    6570      [ mk_block r x ⇒
    6671        match r with
     
    7378        ]
    7479      | _ ⇒ functions … g
    75       ]
     80      ] *)
    7681  ]
    7782in mk_genv_t F fns (nextfunction … g) (remove … (symbols … g) id) ?.
     83whd in match fns; -fns
     84#b #L
     85cases (functions_inv ? g b ?)
     86[ #id' #L'
     87  cases (identifier_eq … id id')
     88  [ #E destruct >L' in L; normalize >lookup_opt_pm_set_hit * #H cases (H (refl ??))
     89  | #NE %{id'} >lookup_remove_miss /2/
     90  ]
     91| cases (lookup ?? (symbols F g) id) in L;
     92  [ normalize //
     93  | normalize nodelta * * normalize nodelta try //
     94    #p
     95    @(eqb_elim … b p)
     96    [ #Heq destruct #NE
     97      >lookup_opt_pm_set_hit in NE; #Hneq
     98      @False_ind
     99      @(absurd … (refl ??) Hneq)
     100    | #id >lookup_opt_pm_set_miss // ]
     101  ]
     102] qed.
     103(*
    78104whd in match fns; -fns
    79105#b #L
     
    93119] qed.
    94120
     121*)
    95122lemma drop_fn_id : ∀F,id,ge.
    96123  lookup ?? (symbols … (drop_fn F id ge)) id = None ?.
     
    107134cases (lookup ??? id)
    108135[ normalize //
    109 | * * * [2,3,5,6: #b' ] normalize //
     136| * * [2,3: #b' ] normalize //
    110137  cases (decidable_eq_pos b b')
    111138  [ #E destruct >lookup_opt_pm_set_hit #E destruct
     
    117144λF,name_fun,g.
    118145  let blk_id ≝ nextfunction ? g in
    119   let b ≝ mk_block Code (neg blk_id) in
     146  let b ≝ mk_block (* Code *) (neg blk_id) in
    120147  let g' ≝ drop_fn F (\fst name_fun) g in
    121148  mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g'))
     
    260287      let init ≝ extract_init init_info in
    261288      let 〈g,st〉 ≝ g_st in
    262         let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) r in
     289        let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) (* r *) in
    263290          let g' ≝ add_symbol ? id b g in
    264291            〈g', st'〉
     
    360387  change with (add_globals B ????) in match (foldl (genv_t B × mem) ????);
    361388  cases (varsOK … p) #E1 #E2
    362   destruct >E2 cases (alloc ????) #m' #b
     389  destruct >E2 cases (alloc ???) (* cases (alloc ????)*) #m' #b
    363390  @IH /2/
    364391  whd in match (add_symbol ????); whd in match (drop_fn ???);
     
    425452] (refl ? (symbol_for_block F ge b)).
    426453whd in H:(??%?);
    427 cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
     454cases b in FFP H ⊢ %; * -b [2,3(*,5,6*): #b ] normalize in ⊢ (% → ?); [ 1,3: * #H cases (H (refl ??)) ]
     455#FFP
    428456cases (functions_inv … ge b FFP)
    429 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
    430 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
     457#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block (*Code*) (neg b)) b') id (mk_block (*Code*) (neg b)))
     458lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block (* Code *) (neg b)) b') id (mk_block (* Code *) (neg b)))
    431459cases (find ????)
    432460[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
    433461| * #id' #b' #_ normalize #_ #E destruct
    434462] qed.
    435 
    436463
    437464(*
     
    492519    [ #E destruct
    493520      (* Found one, but it might be shadowed later *)
    494       whd in match (foldl ?????); normalize nodelta
    495       cases (alloc ????) #m' #b normalize nodelta
     521      whd in match (foldl ?????); normalize nodelta     
     522      cases (alloc ???) (* cases (alloc ????) *) #m' #b normalize nodelta
    496523      cut (find_symbol F (add_symbol F id b ge) id = Some ? b)
    497524      [ change with (lookup ????) in ⊢ (??%?);
     
    499526        @lookup_add_hit ]
    500527      #F @IH %2 %{b} @F
    501     | #TL whd in match (foldl ?????); normalize nodelta
    502       cases (alloc ????) #m' #b'
     528    | #TL whd in match (foldl ?????); normalize nodelta     
     529      cases (alloc ???) (*cases (alloc ????)*) #m' #b'
    503530      @IH %1 @TL
    504531    ]
    505532  | #H whd in match (foldl ?????); normalize nodelta
    506     cases (alloc ????) #m' #b' normalize nodelta
     533    cases (alloc ???) (* cases (alloc ????) *) #m' #b' normalize nodelta
    507534    @IH %2
    508535    cases (identifier_eq ? id id')
     
    693720qed.
    694721
    695 lemma alloc_pair : ∀m,m',l,h,l',h',r. ∀P:mem×(Σb:block. block_region b = r) → mem×(Σb:block. block_region b = r) → Type[0].
     722lemma alloc_pair : ∀m,m',l,h,l',h'(*,r*). ∀P:mem×block (*(Σb:block. block_region b = r)*) → mem×block(*(Σb:block. block_region b = r)*) → Type[0].
    696723  nextblock m = nextblock m' →
    697724  (∀m1,m2,b. nextblock m1 = nextblock m2 → P 〈m1,b〉 〈m2,b〉) →
    698   P (alloc m l h r) (alloc m' l' h' r).
    699 * #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' #r #P #N destruct #H @H %
     725  P (alloc m l h (*r*)) (alloc m' l' h' (*r*)).
     726* #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' (* #r *) #P #N destruct #H @H %
    700727qed.
    701728
     
    711738  ∃f'.find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f' ∧ P f f'.
    712739#F #G #V #W #P #init #init'
    713 * * * [ 2,3,5,6: #blk ] [ 4: | *: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 normalize in H5; destruct ]
     740* * [ 2,3(*,5,6*): #blk ] [ 2: | 1,3: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 whd in H5:(??%?); destruct ]
    714741#vars elim vars
    715742[ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H
     
    731758      cases (lookup … id')
    732759      [ @FFP1
    733       | * * * try @FFP1 #p try @FFP1
     760      | * * (* * *) try @FFP1 #p try @FFP1
    734761        normalize
    735762        cases (decidable_eq_pos blk p)
     
    776803lemma lookup_drop_fn_different : ∀F,ge,id,b,f.
    777804  lookup_opt ? b (functions ? (drop_fn F id ge)) = Some ? f →
    778   lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)).
     805  lookup … (symbols ? ge) id ≠ Some ? (mk_block (*Code*) (neg b)).
    779806#F #ge #id #b #f
    780807whd in match (drop_fn F id ge);
    781808cases (lookup … id)
    782809[ #_ % #E destruct
    783 | * * * [2,3,5,6: #b'] normalize
    784   [4: cases (decidable_eq_pos b b')
     810| * * (* * *) [2,3(*,5,6*): #b'] normalize
     811  [ 2: cases (decidable_eq_pos b b')
    785812    [ #E destruct >lookup_opt_pm_set_hit #E destruct
    786813    | #NE #_ @(not_to_not … NE) #E destruct //
     
    788815  | *: #_ % #E destruct
    789816  ]
    790 ] qed. 
     817] qed.
    791818
    792819lemma lookup_drop_fn_irrelevant : ∀F,ge,id,b.
    793   lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)) →
     820  lookup … (symbols ? ge) id ≠ Some ? (mk_block (* Code *) (neg b)) →
    794821  lookup_opt ? b (functions ? (drop_fn F id ge)) = lookup_opt ? b (functions ? ge).
    795822#F #ge #id #b
     
    797824cases (lookup … id)
    798825[ //
    799 | * * * //
     826| * * (* * *) //
    800827  #b' normalize #NE
    801828  @lookup_opt_pm_set_miss
     
    811838#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
    812839#Mfns
    813 cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]
    814 [ 4: (*12:*) | *: #_ #F whd in F:(??%?); destruct ]
     840cases b * (* * *) [ 2,3 (*,5,6*) (*,8,9,11,12,14,15,17,18*): #bp ]
     841[ 2: (*12:*) | *: #_ #F whd in F:(??%?); destruct ]
    815842whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
    816843whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
  • src/common/Pointers.ma

    r2569 r2608  
    11include "ASM/BitVectorZ.ma".
    2 include "common/AST.ma". (* For the regions *)
     2include "common/AST.ma". (* For the /s/regions/size_pointer/ *)
    33include "utilities/extralib.ma".
     4include "basics/deqsets.ma".
    45
    56
     
    2021
    2122record block : Type[0] ≝
    22 { block_region : region
    23 ; block_id : Z
     23{ (* block_region : region ; *)
     24 block_id : Z
    2425}.
     26
     27definition block_region : block → region ≝
     28  λb.
     29  if Zltb (block_id b) OZ then
     30    Code
     31  else
     32    XData.
    2533
    2634definition eq_block ≝
    2735λb1,b2.
    28   eq_region (block_region b1) (block_region b2) ∧
     36(*  eq_region (block_region b1) (block_region b2) ∧*)
    2937  eqZb (block_id b1) (block_id b2)
    3038.
     
    3341  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
    3442  P (eq_block b1 b2).
     43#P * #i1 *#i2 #H1 #H2 whd in match (eq_block ??);
     44@(eqZb_elim … i1 i2)
     45[ #H @H1 >H @refl
     46| * #Hneq @H2 % #H @Hneq destruct (H) @refl ]
     47qed.
     48(*
    3549#P * #r1 #i1 * #r2 #i2 #H1 #H2
    3650whd in ⊢ (?%); @eq_region_elim #H3
    3751[ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
    3852| @H2 % #E destruct elim H3 /2/
    39 ] qed.
     53] qed. *)
    4054
    4155lemma eq_block_b_b : ∀b. eq_block b b = true.
    42 * * #z whd in ⊢ (??%?); >eqZb_z_z @refl
     56* #z whd in ⊢ (??%?); >eqZb_z_z @refl
    4357qed.
    4458
  • src/common/extraGlobalenvs.ma

    r2590 r2608  
    219219** #x1 #x2 #x3 #tl whd in match add_globals;
    220220normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
    221 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
     221cases(alloc m ? ? (*x2*)) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
    222222normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
    223223#f1 #H3 <(drop_fn_lfn … f1 H3) assumption
     
    227227lemma globalenv_no_minus_one :
    228228 ∀F,V,i,p.
    229   find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?.
     229  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) (-1)) = None ?.
    230230#F #V #i #p
    231231whd in match find_funct_ptr; normalize nodelta
     
    237237lemma globalenv_no_zero :
    238238 ∀F,V,i,p.
    239   find_funct_ptr … (globalenv F V i p) (mk_block Code OZ) = None ?. //
    240 qed.
    241 
     239  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) OZ) = None ?. //
     240qed.
     241
Note: See TracChangeset for help on using the changeset viewer.