Changeset 2600


Ignore:
Timestamp:
Feb 1, 2013, 12:13:22 PM (6 years ago)
Author:
garnier
Message:

Memory injections are now only defined relatively to block ids, not regions. Used to prove some more unfinished lemmas.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2598 r2600  
    206206(* --------------------------------------------------------------------------- *)   
    207207
    208 (* An embedding is a function from blocks to (blocks × offset). *)
    209 definition embedding ≝ block → option (block × offset).
     208(* An embedding is a function from block ids to (blocks × offset). *)
     209definition embedding ≝ Z → option (block × offset).
    210210
    211211definition offset_plus : offset → offset → offset ≝
     
    224224match p with
    225225[ mk_pointer pblock poff ⇒
    226    match E pblock with
     226   match E (block_id pblock) with
    227227   [ None ⇒ None ?
    228228   | Some loc ⇒
     
    236236definition embedding_compatible : embedding → embedding → Prop ≝
    237237λE,E'.
    238   ∀b:block. E b = None ? ∨
    239             E b = E' b.
     238  ∀b:block. E (block_id b) = None ? ∨
     239            E (block_id b) = E' (block_id b).
    240240
    241241(* We parameterise the "equivalence" relation on values with an embedding. *)
     
    258258 ∀b1,off1,b2,off2,ty,v1.
    259259  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 b1 = Some ? 〈b2,off2〉 →
     260  E (block_id b1) = Some ? 〈b2,off2〉 →
    261261  load_value_of_type ty m1 b1 off1 = Some ? v1 →
    262262  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
     
    299299definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝
    300300λE.λb.λm,m'.
    301   match E b with
     301  match E (block_id b) with
    302302  [ None ⇒ True
    303303  | Some loc ⇒
     
    308308  ].
    309309
    310 
    311310(* Adapted from Compcert's Memory *)
    312311definition non_aliasing : embedding → mem → Prop ≝
    313312  λE,m.
    314313  ∀b1,b2,b1',b2',delta1,delta2.
    315   b1 ≠ b2 →
    316   (* block_region b1 = block_region b2 →  *) (* let's be generous with this one *)
    317   E b1 = Some ? 〈b1',delta1〉 →
    318   E b2 = Some ? 〈b2',delta2〉 →
    319   match block_decidable_eq b1' b2' with
    320   [ inl Heq ⇒
    321 (*    block_is_empty m b1' ∨ *)
     314  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
     318    (* block_is_empty m b1' ∨ *)
    322319    high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
    323320    high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1) ∨
    324321    block_is_empty m b1 ∨
    325322    block_is_empty m b2
    326   | inr Hneq ⇒ True
    327   ].
     323   else
     324    True).
    328325
    329326
     
    335332  mi_inj : load_sim_ptr E m1 m2;
    336333  (* Invalid blocks are not mapped *)
    337   mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
     334  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E (block_id b) = None ?;
    338335  (* Valid pointers are mapped to valid pointers *)
    339336  mi_valid_pointers : ∀p,p'.
     
    344341  mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
    345342  (* Regions are preserved *)
    346   mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
     343  mi_region : ∀b,b',o'. E (block_id b) = Some ? 〈b',o'〉 → block_region b = block_region b';
    347344  (* sub-blocks do not overlap (non-aliasing property) *)
    348345  mi_nonalias : non_aliasing E m1;
     
    614611  ∀m,m',z1,z2,r,new_block.
    615612  alloc m z1 z2 r=〈m',new_block〉 →
    616   ∀p. (pblock p) ≠ (pi1 … new_block) →
    617       block_region (pblock p) = block_region (pi1 … new_block) →
     613  ∀p. block_id (pblock p) ≠ block_id (pi1 … new_block) →
    618614      valid_pointer m' p = true →
    619615      valid_pointer m p = true.
     
    621617cases m #cont #next #Hnext
    622618whd in ⊢ ((??%%) → ?);
    623 #Heq destruct (Heq) * #b #o #Hneq #Hregion #Hvalid
     619#Heq destruct (Heq) * #b #o #Hneq #Hvalid
    624620@valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)
    625621-Hvalid
     
    629625whd in match (update_block ?????);
    630626whd in match (update_block ?????);
    631 >(not_eq_block … Hneq) normalize nodelta
     627cut (b ≠ (mk_block r next))
     628[ @(eq_block_elim … b (mk_block r next)) #H destruct try //
     629  @False_ind
     630  @(absurd … (refl ??) Hneq) ] #Hneqb
     631>(not_eq_block … Hneqb) normalize nodelta
    632632#HA #HB % [ % ] try assumption
    633 cases b in Hneq Hregion Hblock_id; #r' #id * #Hnext_not_id #Hregion destruct
    634 cut (next ≠ id)
    635 [ % #H destruct @Hnext_not_id @refl ]
    636 #Hneq #Hlt cut (id ≤ next)
     633cases b in Hneqb Hneq Hblock_id; #r' #id * #Hnext_not_id #Hneq
     634#Hlt cut (id ≤ next)
    637635[ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ]
    638 #Hle @Zle_split try @Hle @sym_neq @Hneq
     636#Hle @Zle_split try @Hle @Hneq
    639637qed.
    640638
     
    681679#bev normalize nodelta
    682680whd in match (shift_pointer ???); >Hind try //
     681qed.
     682
     683lemma alloc_load_value_of_type_conservation :
     684  ∀m,m',z1,z2,r,new_block.
     685    alloc m z1 z2 r = 〈m', new_block〉 →
     686    ∀block,offset.
     687    valid_block m block →
     688    ∀ty. load_value_of_type ty m block offset =
     689         load_value_of_type ty m' block offset.
     690#m #m' #z1 #z2 #r #new_block #Halloc #block #offset #Hvalid         
     691#ty cases ty
     692[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     693| #structname #fieldspec | #unionname #fieldspec | #id ]
     694try //
     695whd in match (load_value_of_type ????) in ⊢ (??%%);
     696>(alloc_loadn_conservation … Halloc … Hvalid) @refl
    683697qed.
    684698
     
    704718  #Hload normalize in ⊢ ((???%) → ?); #Haccess
    705719  [ 1,6,7: normalize in Hload; destruct (Hload)
    706   | 2,3,8: whd in match (load_value_of_type ????);
    707      whd in match (load_value_of_type ????);
     720  | 2,3,8:
    708721     lapply (load_by_value_success_valid_block … Haccess Hload)
    709722     #Hvalid_block
    710      whd in match (load_value_of_type ????) in Hload;
    711      <(alloc_loadn_conservation … Halloc … Hvalid_block)
    712      @Hload
     723      <(alloc_load_value_of_type_conservation … Halloc … Hvalid_block)
     724     assumption
    713725  | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
    714726| @(mi_freeblock … Hmemory_inj)
     
    733745| #b lapply (mi_nowrap … Hmemory_inj b)
    734746   whd in ⊢ (% → %);
    735    lapply (mi_nodangling … Hmemory_inj b)
    736    cases (E b) normalize nodelta try //
     747   lapply (mi_nodangling … Hmemory_inj (block_id b))
     748   cases (E (block_id b)) normalize nodelta try //
    737749   * #B #OFF normalize nodelta #Hguard
    738750   * * #H1 #H2 #Hinbounds @conj try @conj try assumption
    739751   @(eq_block_elim … new_block B)
    740      [ #H destruct try //
    741      | #H cases m2 in Halloc H2; #contents #nextblock #notnull
     752   [ #H <H assumption
     753   | #H cases m2 in Halloc H2; #contents #nextblock #notnull
    742754       whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) *
    743755       >unfold_low_bound >unfold_high_bound #HA #HB
     
    749761] qed.
    750762
    751 
    752 (* TODO: these axioms are not enough for memory injections. We need the updated embedding as a byproduct
    753  * of the allocation. *)
    754 
    755 lemma block_neq_elim :
    756   ∀b1,b2. b1 ≠ b2 →
    757     (block_id b1 ≠ block_id b2 ∧ block_region b1 = block_region b2) ∨
    758     (block_id b1 = block_id b2 ∧ block_region b1 ≠ block_region b2) ∨
    759     (block_id b1 ≠ block_id b2 ∧ block_region b1 ≠ block_region b2).
    760 * #r #id * #r' #id'
    761 cases r cases r'
    762 @(eqZb_elim …  id id')
    763 #H1 #H2
    764 [ 1,7: destruct @False_ind @(absurd … (refl ??) H2) ]
    765 try /4 by or_introl, or_intror, conj/
    766 destruct
    767 [ %1 %2 @conj // % #H destruct
    768 | %2 @conj try @H1 % #H destruct
    769 | %1 %2 @conj // % #H destruct
    770 | %2 @conj try @H1 % #H destruct ]
    771 qed.
    772 
    773763(* Allocating in m1 such that the resulting block has no image in m2 preserves
    774764   the injection. This is lemma 67 for Leroy&Blazy. The proof should proceed as
    775    in Blazy & Leroy. Careful of using the mi_embedding hypothesis to rule out
    776    absurd cases. *)
     765   in Blazy & Leroy. Notice that we must consider blocks with different regions but
     766   same id as equal. *)
    777767lemma alloc_memory_inj_m1 :
    778768  ∀E:embedding.
     
    780770  ∀H:memory_inj E m1 m2.
    781771  alloc m1 z1 z2 r = 〈m1', new_block〉 →
    782   memory_inj (λx. if eq_block x (pi1 … new_block) then None ? else E x) m1' m2 ∧
    783   embedding_compatible E (λx. if eq_block x (pi1 … new_block) then None ? else E x).
    784 @cthulhu
    785 qed. (* XXX finish this. *)
    786 (* 
     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).
    787774#E #m1 #m2 #m1' #z1 #z2 #r * #new_block #Hregion_eq #Hinj #Halloc
    788 cut (E new_block = None ?)
     775cut (E (block_id new_block) = None ?)
    789776[ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?);
    790777  #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
    791 #Hempty %
    792 [ 2: whd #b @(eq_block_elim … b new_block) try // #Heq destruct (Heq) >Hempty %1 @refl ] 
     778#Hempty
     779cut (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 ]
     785#Hembedding_compatible @conj try assumption
    793786%
    794787[ whd #b1 #off1 #b2 #off2 #ty #v1
    795788  @(eq_block_elim … b1 new_block)
    796   [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta
     789  [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eqZb_z_z normalize nodelta
    797790    #Habsurd destruct ]
    798791  #Hneq #Hvalid
    799   whd in ⊢ ((??%?) → ?); >(not_eq_block … Hneq) normalize nodelta
    800   #Hembed cases (some_inversion ????? Hembed) * #b1' #off' * #Hembed
    801   normalize nodelta #Heq destruct (Heq)
    802   lapply (block_neq_elim … Hneq)
    803   *
    804   [ 2: * #Hid_neq #Hregion_neq
    805          lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … Hneq)
    806 *) 
    807      
     792  whd in ⊢ ((??%?) → ?);
     793  @(eqZb_elim … (block_id new_block) (block_id b1))
     794  normalize nodelta
     795  [ #Heq #Habsurd destruct (Habsurd) ]
     796  #Hneq_id
     797  #Hembed #Hload
     798  lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) (sym_neq ??? Hneq_id) Hvalid)
     799  #Hvalid'
     800  cut (valid_block m1 b1)
     801  [ cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block #_ #_ @Hvalid_block ]
     802  #Hvalid_block
     803  lapply (alloc_load_value_of_type_conservation … Halloc … off1 … Hvalid_block ty)
     804  #Heq <Heq in Hload; #Hload
     805  lapply (mi_inj … Hinj … Hvalid' … Hembed … Hload) * #v2 * #Hload2 #Hveq2
     806  %{v2} @conj try assumption
     807  @(embedding_compatibility_value_eq … Hveq2) assumption
     808| #b #Hnot_valid @(eqZb_elim … (block_id new_block) (block_id b))
     809  normalize nodelta
     810  [ #Heq @refl
     811  | #Hneq @(mi_freeblock … Hinj) % #Hvalid cases Hnot_valid #H @H
     812    @(alloc_valid_block_conservation … Halloc) assumption ]
     813| #p #p' lapply (mi_valid_pointers … Hinj p p')
     814  cases p #b #o cases p' #b' #o' normalize nodelta #Hvalidptr #Hvalid1'
     815  whd in ⊢ ((??%%) → ?); 
     816  @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta
     817  [ #Heq #Habsurd destruct ]
     818  #Hneq #Hembed
     819  lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b o) (sym_neq ??? Hneq) Hvalid1')
     820  #Hvalid1
     821  @(Hvalidptr Hvalid1 Hembed)
     822| #b #b' #o' @(eqZb_elim … (block_id new_block) b)
     823  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
     824  normalize nodelta #Henq
     825  @(mi_nodangling … Hinj)
     826| #b #b' #o' @(eqZb_elim … (block_id new_block) (block_id b))
     827  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
     828  #Hneq @(mi_region … Hinj)
     829| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
     830  @(eqZb_elim … (block_id new_block) (block_id b1))
     831  normalize nodelta
     832  [ #Heq #Habsurd destruct (Habsurd) ]
     833  #Hneq1 #Hembed1
     834  @(eqZb_elim … (block_id new_block) (block_id b2))
     835  normalize nodelta
     836  [ #Heq #Habsurd destruct (Habsurd) ]
     837  #Hneq2 #Hembed2
     838  @(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta try //
     839  #Heq
     840  lapply (mi_nonalias … Hinj … b1 b2 b1' b2' delta1 delta2 Hneq Hembed1 Hembed2) >Heq
     841  >eqZb_z_z normalize nodelta
     842  cases m1 in Halloc; #contents #next #Hnext
     843  >unfold_high_bound >unfold_low_bound
     844  >unfold_high_bound >unfold_low_bound
     845  >unfold_high_bound >unfold_low_bound
     846  >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  #Heq_block_2
     857  #Heq_block_1
     858  * [ * [ * | ] | ]
     859  whd in match (update_block ?????);
     860  >Heq_block_1 normalize nodelta
     861  whd in match (update_block ?????);
     862  >Heq_block_2 normalize nodelta
     863  #H
     864  try /4 by or_introl, or_intror, conj/
     865  [ %1 %2 whd whd in H;
     866    >unfold_high_bound
     867    whd in match (update_block ?????);
     868    >unfold_low_bound
     869    whd in match (update_block ?????);
     870    >Heq_block_1 normalize nodelta @H
     871  | %2 whd whd in H;
     872    >unfold_high_bound
     873    whd in match (update_block ?????);
     874    >unfold_low_bound
     875    whd in match (update_block ?????);
     876    >Heq_block_1 >Heq_block_2 @H
     877  ]
     878| #b whd @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta try //
     879  #Hneq lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?);
     880  cases (E (block_id b)) normalize nodelta try //
     881  * #bb #oo normalize nodelta
     882  * * * #HA #HB * #HC #HD #HE @conj try @conj
     883  try @conj
     884  lapply HE -HE
     885  lapply HD -HD
     886  lapply HC -HC
     887  lapply HB -HB
     888  lapply HA -HA
     889  >unfold_low_bound >unfold_low_bound [ >unfold_low_bound ]
     890  >unfold_high_bound >unfold_high_bound [ 2,5: >unfold_high_bound ]
     891 cases m1 in Halloc; #cont #next #Hnext
     892 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) try //
     893 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
     898 | 2,4,6: #Heq_block >Heq_block // ]
     899] qed.
     900 
     901       
    808902
    809903(* Embed a fresh block inside an unmapped portion of the target block.
     
    820914  z2 + Zoo delta ≤ high_bound m2 b2 →
    821915  (∀b,b',delta'. b ≠ (pi1 … new_block) →
    822                  E b = Some ? 〈b', delta'〉 →
     916                 E (block_id b) = Some ? 〈b', delta'〉 →
    823917                 high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨
    824918                 z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) →                 
    825919  memory_inj E m1 m2 →
    826   memory_inj (λx. if eq_block x (pi1 … new_block) then Some ? 〈b2, delta〉 else E x) m1' m2.
     920  memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then Some ? 〈b2, delta〉 else E x) m1' m2.
    827921
    828922(* -------------------------------------- *)
     
    875969  load_sim_ptr E m1 m2 →
    876970  ∀b. free m2 b = m2' →
    877       (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
     971      (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
    878972      load_sim_ptr E m1 m2'.     
    879973#E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped
     
    9601054#b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
    9611055#Hembed1 #Hembed2
    962 cases (block_decidable_eq ??) normalize nodelta
     1056@(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta
    9631057[ 2: try // ]
    964 #Hblocks_eq destruct (Hblocks_eq)
     1058#Hblocks_eq
     1059lapply Hembed2 -Hembed2
    9651060lapply Hembed1 -Hembed1
    966 lapply Hembed2 -Hembed2
    967 generalize in match b2';
    968 #target #Hembed2 #Hembed1
     1061lapply Hblocks_eq -Hblocks_eq
     1062cases b1' #r1' #bid1'
     1063cases b2' #r2' #bid2'
     1064#Heq destruct (Heq)
     1065generalize in match bid2';
     1066#target #Hembed1 #Hembed2
    9691067lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2)
    970 cases (block_decidable_eq ??)
    971 [ 2: * #Habsurd @False_ind @Habsurd @refl ] #Hrefl
     1068>eqZb_z_z normalize nodelta
    9721069normalize nodelta <Hfree
    9731070@(eq_block_elim … b1 b)
     
    10151112| @(free_non_aliasing_m1 … Hinj … Hfree)
    10161113| #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?);
    1017   cases (E bb) normalize nodelta try //
     1114  cases (E (block_id bb)) normalize nodelta try //
    10181115  * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj
    10191116  try //
     
    10431140  memory_inj E m1 m2 →
    10441141  ∀b. free m2 b = m2' →
    1045       (∀b1,delta. E b1 = Some ? 〈b, delta〉 →
     1142      (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 →
    10461143      (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → 
    10471144      memory_inj E m1 m2'.
     
    10511148[ @(free_load_sim_ptr_m2 … Hload_sim … Hfree) #b1 #delta #Hembed
    10521149  @(b_not_mapped … b1 delta Hembed)
    1053 | @Hfreeblock   
     1150| @Hfreeblock
    10541151| * #bp #op #p' #Hp_valid #Hptr_trans
    10551152  @(eq_block_elim … (pblock p') b)
     
    10741171| @Hregion
    10751172| #bb lapply (Himpl bb)
    1076   whd in ⊢ (% → %); cases (E bb) normalize nodelta try //
     1173  whd in ⊢ (% → %); cases (E (block_id bb)) normalize nodelta try //
    10771174  * #BLO #OFF normalize nodelta * * destruct (Hfree)
    10781175  #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption
     
    10941191  memory_inj E m1 m2 →
    10951192  ∀blocklist,b2.
    1096   (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) →
     1193  (∀b1,delta. E (block_id b1) = Some ? 〈b2, delta〉 → meml ? b1 blocklist) →
    10971194  free m2 b2 = m2' →
    10981195  free_list m1 blocklist = m1' →
     
    11351232    ]
    11361233  ]
    1137 ] qed. 
     1234] qed.
    11381235
    11391236(* ---------------------------------------------------------- *)
     
    12301327    memory_inj E mA mB →
    12311328    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
    1232     ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
     1329    ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 →
    12331330    high_bound mA b1 + Zoo delta < Zoo wo →
    12341331    ∀ty,off.
     
    13081405    memory_inj E mA mB →
    13091406    ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
    1310     ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
     1407    ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 →
    13111408    Zoo wo < low_bound mA b1 + Zoo delta →
    13121409    ∀ty,off.
     
    13251422  ∀block2. ∀i : offset. ∀ty : type.
    13261423  (∀block1,delta.
    1327     E block1 = Some ? 〈block2, delta〉 →
     1424    E (block_id block1) = Some ? 〈block2, delta〉 →
    13281425    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
    13291426  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
     
    13811478  ∀block2. ∀i : offset. ∀ty : type.
    13821479  (∀block1,delta.
    1383     E block1 = Some ? 〈block2, delta〉 →
     1480    E (block_id block1) = Some ? 〈block2, delta〉 →
    13841481    (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
    13851482  ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
     
    14111508  >(Hnext_eq) try //
    14121509| #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %);
    1413   cases (E b) try //
     1510  cases (E (block_id b)) try //
    14141511  * #BLO #OFF normalize nodelta * *
    14151512  #Hb #HBLO #Hbound try @conj try @conj try assumption
     
    14731570  ∀E,m1,m2.
    14741571  memory_inj E m1 m2 →
    1475   ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
     1572  ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 →
    14761573  ∀v1,v2. value_eq E v1 v2 →
    14771574  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
     
    15421639  ∀E,m1,m2.
    15431640  memory_inj E m1 m2 →
    1544   ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
     1641  ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 →
    15451642  ∀v1,v2. value_eq E v1 v2 →
    15461643  ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
     
    15651662  ∀Hinj:memory_inj E m1 m2.
    15661663  ∀v1,v2. value_eq E v1 v2 →
    1567   ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
     1664  ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 →
    15681665  ∀ty,i,m1'.
    15691666  ast_typ_consistent_with_value ty v1 →
     
    16531750  ∀Hinj:memory_inj E m1 m2.
    16541751  ∀v1,v2. value_eq E v1 v2 →
    1655   ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
     1752  ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 →
    16561753  ∀ty,i,m1'.
    16571754  type_consistent_with_value ty v1 →
     
    16731770  ∀Hinj:memory_inj E m1 m2.
    16741771  ∀ty,b,i,v.
    1675   E b = None ? →
     1772  E (block_id b) = None ? →
    16761773  store_value_of_type ty m1 b i v = Some ? m1' →
    16771774  load_sim_ptr E m1' m2.
     
    17231820  ∀Hinj:memory_inj E m1 m2.
    17241821  ∀ty,b,i,v.
    1725   E b = None ? →
     1822  E (block_id b) = None ? →
    17261823  store_value_of_type ty m1 b i v = Some ? m1' →
    17271824  memory_inj E m1' m2.
     
    17521849    | #bb whd
    17531850      lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?);
    1754       cases (E bb) normalize nodelta try // * #bb' #off
     1851      cases (E (block_id bb)) normalize nodelta try // * #bb' #off
    17551852      normalize nodelta
    17561853      whd in match (block_implementable_bv ??);     
     
    17631860      >HA >HB //
    17641861    ]
    1765 ] qed.   
     1862] qed.
    17661863
    17671864(* ------------------------------------------------------------------------- *)
     
    18551952          @(ex_intro … (conj … (refl …) ?))
    18561953          @vptr_eq whd in match (pointer_translation ??);
    1857           cases (E b1') in Hembed;
     1954          cases (E (block_id b1')) in Hembed;
    18581955          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    18591956          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     
    18971994     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    18981995     elim p1 in Hembed; #b1 #o1 normalize nodelta
    1899      cases (E b1)
     1996     cases (E (block_id b1))
    19001997     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    19011998     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     
    19962093          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    19972094          elim p1 in Hembed; #b1 #o1 normalize nodelta
    1998           cases (E b1)
     2095          cases (E (block_id b1))
    19992096          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    20002097          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     
    20122109               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
    20132110               whd in ⊢ ((??%?) → (??%?) → ?);
    2014                cases (E b1') normalize nodelta
     2111               cases (E (block_id b1')) normalize nodelta
    20152112               [ 1: #Habsurd destruct (Habsurd) ]
    20162113               * #dest_block #dest_off normalize nodelta
     
    24182515          lapply (mi_nowrap … Hinj bq1)
    24192516          whd in ⊢ (% → ?);
    2420           cases (E bq1) normalize nodelta
     2517          cases (E (block_id bq1)) normalize nodelta
    24212518          [ #_ #Habsurd destruct ]
    24222519          * #BLO #OFF normalize nodelta * *         
     
    24372534          lapply (mi_nowrap … Hinj bp1) whd in ⊢ (% → ?);
    24382535          lapply (mi_nowrap … Hinj bq1) whd in ⊢ (% → ?);
    2439           cases (E bq1) [ 1: #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
     2536          lapply (mi_region … Hinj bq1)
     2537          lapply (mi_region … Hinj bp1)
     2538          cases (E (block_id bq1)) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    24402539          * #BLOq #DELTAq normalize nodelta
    2441           cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
    2442           * #BLOp #DELTAp normalize nodelta #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
     2540          cases (E (block_id bp1)) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
     2541          * #BLOp #DELTAp normalize nodelta #Hregion1 #Hregion2 #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
     2542          lapply (Hregion1 … (refl ??)) lapply (Hregion2 … (refl ??)) -Hregion1 -Hregion2
     2543          #Hregion2 #Hregion1
    24432544          cases op
    24442545          whd in ⊢ ((??%?) → ?); #H' destruct (H')
     
    24552556          lapply (valid_pointer_to_Prop … Hvalid')
    24562557          * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp
    2457           >eq_block_b_b normalize nodelta
     2558          >eqZb_z_z >eq_block_b_b normalize nodelta
    24582559          *
    24592560          [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
  • src/Clight/toCminorCorrectnessExpr.ma

    r2591 r2600  
    3434      match find_symbol ? (ge_cl cminv) id with
    3535      [ None ⇒ True
    36       | Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
     36      | Some cl_blo ⇒
     37        (* global symbols are mapped to themselves. Perhaps too strong. *)
     38        E (block_id cl_blo) = Some ? 〈cl_blo, zero_offset〉
    3739      ]
    3840    | Some cl_blo ⇒
     
    4244            match vtype with
    4345            [ Stack n ⇒
    44               E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
     46              E (block_id cl_blo) = Some ? 〈sp, mk_offset (repr I16 n)〉
    4547            | Local ⇒
    4648              ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
     
    22102212       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
    22112213       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
    2212        cases (E cl_blo) in Hptr_translate; normalize nodelta
     2214       cases (E (block_id cl_blo)) in Hptr_translate; normalize nodelta
    22132215       [ #H destruct (H) ]
    22142216       * #BL #OFF normalize nodelta #Heq destruct (Heq)
     
    22222224       >(commutative_addition_n … (repr I16 field_off) (offv OFF))
    22232225       >(associative_addition_n ? (offv off))
    2224        @refl       
     2226       @refl
    22252227  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
    22262228       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
  • src/Clight/toCminorOps.ma

    r2588 r2600  
    192192lapply H1 lapply H2 -H1 -H2
    193193whd in ⊢ ((??%?) → (??%?) → ?);
    194 cases (E b2) normalize nodelta
     194cases (E (block_id b2)) normalize nodelta
    195195[ #Habsurd destruct ]
    196196* #bx #ox normalize nodelta #Heq1 #Heq2 destruct
Note: See TracChangeset for help on using the changeset viewer.