Changeset 2600

Timestamp:

Feb 1, 2013, 12:13:22 PM (7 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:

• memoryInjections.ma (modified) (45 diffs)
• toCminorCorrectnessExpr.ma (modified) (4 diffs)
• toCminorOps.ma (modified) (1 diff)

src/Clight/memoryInjections.ma

@@ -206 +206 @@
 (* --------------------------------------------------------------------------- *)   
 
-(* An embedding is a function from blocks to (blocks × offset). *)
-definition embedding ≝ block → option (block × offset).
+(* An embedding is a function from block ids to (blocks × offset). *)
+definition embedding ≝ Z → option (block × offset).
 
 definition offset_plus : offset → offset → offset ≝
@@ -224 +224 @@
 match p with
 [ mk_pointer pblock poff ⇒
-   match E pblock with
+   match E (block_id pblock) with
    [ None ⇒ None ?
    | Some loc ⇒
@@ -236 +236 @@
 definition embedding_compatible : embedding → embedding → Prop ≝ 
 λE,E'.
-  ∀b:block. E b = None ? ∨
-            E b = E' b.
+  ∀b:block. E (block_id b) = None ? ∨
+            E (block_id b) = E' (block_id b).
 
 (* We parameterise the "equivalence" relation on values with an embedding. *)
@@ -258 +258 @@
  ∀b1,off1,b2,off2,ty,v1.
   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 *)
-  E b1 = Some ? 〈b2,off2〉 → 
+  E (block_id b1) = Some ? 〈b2,off2〉 → 
   load_value_of_type ty m1 b1 off1 = Some ? v1 →
   (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
@@ -299 +299 @@
 definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝ 
 λE.λb.λm,m'.
-  match E b with
+  match E (block_id b) with
   [ None ⇒ True
   | Some loc ⇒
@@ -308 +308 @@
   ].
 
-
 (* Adapted from Compcert's Memory *)
 definition non_aliasing : embedding → mem → Prop ≝
   λE,m.
   ∀b1,b2,b1',b2',delta1,delta2.
-  b1 ≠ b2 →
-  (* block_region b1 = block_region b2 →  *) (* let's be generous with this one *) 
-  E b1 = Some ? 〈b1',delta1〉 →
-  E b2 = Some ? 〈b2',delta2〉 →
-  match block_decidable_eq b1' b2' with
-  [ inl Heq ⇒
-(*    block_is_empty m b1' ∨ *)
+  b1 ≠ b2 → (* note that two blocks can be different only becuase of this region *)
+  E (block_id b1) = Some ? 〈b1',delta1〉 →
+  E (block_id b2) = Some ? 〈b2',delta2〉 →
+  (if eqZb (block_id b1') (block_id b2') then
+    (* block_is_empty m b1' ∨ *)
     high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
     high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1) ∨
     block_is_empty m b1 ∨
     block_is_empty m b2
-  | inr Hneq ⇒ True
-  ].
+   else
+    True).
 
 
@@ -335 +332 @@
   mi_inj : load_sim_ptr E m1 m2;
   (* Invalid blocks are not mapped *)
-  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
+  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E (block_id b) = None ?;
   (* Valid pointers are mapped to valid pointers *)
   mi_valid_pointers : ∀p,p'. 
@@ -344 +341 @@
   mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
   (* Regions are preserved *)
-  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
+  mi_region : ∀b,b',o'. E (block_id b) = Some ? 〈b',o'〉 → block_region b = block_region b';
   (* sub-blocks do not overlap (non-aliasing property) *)
   mi_nonalias : non_aliasing E m1;
@@ -614 +611 @@
   ∀m,m',z1,z2,r,new_block.
   alloc m z1 z2 r=〈m',new_block〉 →
-  ∀p. (pblock p) ≠ (pi1 … new_block) →
-      block_region (pblock p) = block_region (pi1 … new_block) →
+  ∀p. block_id (pblock p) ≠ block_id (pi1 … new_block) →
       valid_pointer m' p = true → 
       valid_pointer m p = true.
@@ -621 +617 @@
 cases m #cont #next #Hnext
 whd in ⊢ ((??%%) → ?);
-#Heq destruct (Heq) * #b #o #Hneq #Hregion #Hvalid
+#Heq destruct (Heq) * #b #o #Hneq #Hvalid
 @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)
 -Hvalid
@@ -629 +625 @@
 whd in match (update_block ?????);
 whd in match (update_block ?????);
->(not_eq_block … Hneq) normalize nodelta
+cut (b ≠ (mk_block r next))
+[ @(eq_block_elim … b (mk_block r next)) #H destruct try //
+  @False_ind
+  @(absurd … (refl ??) Hneq) ] #Hneqb
+>(not_eq_block … Hneqb) normalize nodelta
 #HA #HB % [ % ] try assumption
-cases b in Hneq Hregion Hblock_id; #r' #id * #Hnext_not_id #Hregion destruct
-cut (next ≠ id)
-[ % #H destruct @Hnext_not_id @refl ]
-#Hneq #Hlt cut (id ≤ next)
+cases b in Hneqb Hneq Hblock_id; #r' #id * #Hnext_not_id #Hneq
+#Hlt cut (id ≤ next)
 [ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ]
-#Hle @Zle_split try @Hle @sym_neq @Hneq
+#Hle @Zle_split try @Hle @Hneq
 qed.
 
@@ -681 +679 @@
 #bev normalize nodelta
 whd in match (shift_pointer ???); >Hind try //
+qed.
+
+lemma alloc_load_value_of_type_conservation :
+  ∀m,m',z1,z2,r,new_block.
+    alloc m z1 z2 r = 〈m', new_block〉 →
+    ∀block,offset.
+    valid_block m block →
+    ∀ty. load_value_of_type ty m block offset = 
+         load_value_of_type ty m' block offset.
+#m #m' #z1 #z2 #r #new_block #Halloc #block #offset #Hvalid         
+#ty cases ty
+[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
+| #structname #fieldspec | #unionname #fieldspec | #id ]
+try //
+whd in match (load_value_of_type ????) in ⊢ (??%%);
+>(alloc_loadn_conservation … Halloc … Hvalid) @refl
 qed.
 
@@ -704 +718 @@
   #Hload normalize in ⊢ ((???%) → ?); #Haccess
   [ 1,6,7: normalize in Hload; destruct (Hload)
-  | 2,3,8: whd in match (load_value_of_type ????);
-     whd in match (load_value_of_type ????);
+  | 2,3,8:
      lapply (load_by_value_success_valid_block … Haccess Hload)
      #Hvalid_block
-     whd in match (load_value_of_type ????) in Hload;
-     <(alloc_loadn_conservation … Halloc … Hvalid_block) 
-     @Hload
+      <(alloc_load_value_of_type_conservation … Halloc … Hvalid_block)
+     assumption
   | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
 | @(mi_freeblock … Hmemory_inj)
@@ -733 +745 @@
 | #b lapply (mi_nowrap … Hmemory_inj b)
    whd in ⊢ (% → %);
-   lapply (mi_nodangling … Hmemory_inj b)
-   cases (E b) normalize nodelta try //
+   lapply (mi_nodangling … Hmemory_inj (block_id b))
+   cases (E (block_id b)) normalize nodelta try //
    * #B #OFF normalize nodelta #Hguard
    * * #H1 #H2 #Hinbounds @conj try @conj try assumption
    @(eq_block_elim … new_block B)
-     [ #H destruct try //
-     | #H cases m2 in Halloc H2; #contents #nextblock #notnull
+   [ #H <H assumption
+   | #H cases m2 in Halloc H2; #contents #nextblock #notnull
        whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) *
        >unfold_low_bound >unfold_high_bound #HA #HB 
@@ -749 +761 @@
 ] qed.
 
-
-(* TODO: these axioms are not enough for memory injections. We need the updated embedding as a byproduct
- * of the allocation. *)
-
-lemma block_neq_elim : 
-  ∀b1,b2. b1 ≠ b2 →
-    (block_id b1 ≠ block_id b2 ∧ block_region b1 = block_region b2) ∨
-    (block_id b1 = block_id b2 ∧ block_region b1 ≠ block_region b2) ∨
-    (block_id b1 ≠ block_id b2 ∧ block_region b1 ≠ block_region b2).
-* #r #id * #r' #id'
-cases r cases r'
-@(eqZb_elim …  id id')
-#H1 #H2
-[ 1,7: destruct @False_ind @(absurd … (refl ??) H2) ]
-try /4 by or_introl, or_intror, conj/
-destruct
-[ %1 %2 @conj // % #H destruct
-| %2 @conj try @H1 % #H destruct
-| %1 %2 @conj // % #H destruct
-| %2 @conj try @H1 % #H destruct ]
-qed.
-
 (* Allocating in m1 such that the resulting block has no image in m2 preserves
    the injection. This is lemma 67 for Leroy&Blazy. The proof should proceed as 
-   in Blazy & Leroy. Careful of using the mi_embedding hypothesis to rule out 
-   absurd cases. *)
+   in Blazy & Leroy. Notice that we must consider blocks with different regions but
+   same id as equal. *)
 lemma alloc_memory_inj_m1 :
   ∀E:embedding.
@@ -780 +770 @@
   ∀H:memory_inj E m1 m2.
   alloc m1 z1 z2 r = 〈m1', new_block〉 →
-  memory_inj (λx. if eq_block x (pi1 … new_block) then None ? else E x) m1' m2 ∧
-  embedding_compatible E (λx. if eq_block x (pi1 … new_block) then None ? else E x).
-@cthulhu
-qed. (* XXX finish this. *)
-(*  
+  memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then None ? else E x) m1' m2 ∧
+  embedding_compatible E (λx. if eqZb (block_id (pi1 … new_block)) x then None ? else E x).
 #E #m1 #m2 #m1' #z1 #z2 #r * #new_block #Hregion_eq #Hinj #Halloc
-cut (E new_block = None ?)
+cut (E (block_id new_block) = None ?)
 [ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?);
   #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
-#Hempty %
-[ 2: whd #b @(eq_block_elim … b new_block) try // #Heq destruct (Heq) >Hempty %1 @refl ]  
+#Hempty
+cut (embedding_compatible E
+     (λx:Z.
+       if eqZb (block_id new_block) x
+       then None (block×offset) 
+       else E x ))
+[ whd #b @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta try // #Heq <Heq %1 @Hempty ]
+#Hembedding_compatible @conj try assumption
 %
 [ whd #b1 #off1 #b2 #off2 #ty #v1
   @(eq_block_elim … b1 new_block)
-  [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta
+  [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eqZb_z_z normalize nodelta
     #Habsurd destruct ]
   #Hneq #Hvalid
-  whd in ⊢ ((??%?) → ?); >(not_eq_block … Hneq) normalize nodelta
-  #Hembed cases (some_inversion ????? Hembed) * #b1' #off' * #Hembed
-  normalize nodelta #Heq destruct (Heq)
-  lapply (block_neq_elim … Hneq)
-  *
-  [ 2: * #Hid_neq #Hregion_neq
-         lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … Hneq)
-*)  
-      
+  whd in ⊢ ((??%?) → ?);
+  @(eqZb_elim … (block_id new_block) (block_id b1))
+  normalize nodelta
+  [ #Heq #Habsurd destruct (Habsurd) ]
+  #Hneq_id
+  #Hembed #Hload
+  lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) (sym_neq ??? Hneq_id) Hvalid)
+  #Hvalid'
+  cut (valid_block m1 b1)
+  [ cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block #_ #_ @Hvalid_block ]
+  #Hvalid_block
+  lapply (alloc_load_value_of_type_conservation … Halloc … off1 … Hvalid_block ty)
+  #Heq <Heq in Hload; #Hload
+  lapply (mi_inj … Hinj … Hvalid' … Hembed … Hload) * #v2 * #Hload2 #Hveq2
+  %{v2} @conj try assumption
+  @(embedding_compatibility_value_eq … Hveq2) assumption
+| #b #Hnot_valid @(eqZb_elim … (block_id new_block) (block_id b))
+  normalize nodelta
+  [ #Heq @refl
+  | #Hneq @(mi_freeblock … Hinj) % #Hvalid cases Hnot_valid #H @H
+    @(alloc_valid_block_conservation … Halloc) assumption ]
+| #p #p' lapply (mi_valid_pointers … Hinj p p')
+  cases p #b #o cases p' #b' #o' normalize nodelta #Hvalidptr #Hvalid1'
+  whd in ⊢ ((??%%) → ?);  
+  @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta
+  [ #Heq #Habsurd destruct ]
+  #Hneq #Hembed
+  lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b o) (sym_neq ??? Hneq) Hvalid1')
+  #Hvalid1
+  @(Hvalidptr Hvalid1 Hembed)
+| #b #b' #o' @(eqZb_elim … (block_id new_block) b)
+  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
+  normalize nodelta #Henq
+  @(mi_nodangling … Hinj)
+| #b #b' #o' @(eqZb_elim … (block_id new_block) (block_id b))
+  [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ]
+  #Hneq @(mi_region … Hinj)
+| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
+  @(eqZb_elim … (block_id new_block) (block_id b1))
+  normalize nodelta
+  [ #Heq #Habsurd destruct (Habsurd) ]
+  #Hneq1 #Hembed1
+  @(eqZb_elim … (block_id new_block) (block_id b2))
+  normalize nodelta
+  [ #Heq #Habsurd destruct (Habsurd) ]
+  #Hneq2 #Hembed2
+  @(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta try //
+  #Heq
+  lapply (mi_nonalias … Hinj … b1 b2 b1' b2' delta1 delta2 Hneq Hembed1 Hembed2) >Heq
+  >eqZb_z_z normalize nodelta
+  cases m1 in Halloc; #contents #next #Hnext
+  >unfold_high_bound >unfold_low_bound
+  >unfold_high_bound >unfold_low_bound
+  >unfold_high_bound >unfold_low_bound
+  >unfold_high_bound >unfold_low_bound
+  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
+  cut (eq_block b1 (mk_block r next) = false)
+  [ whd in ⊢ (??%%); 
+    >(eqZb_false … (sym_neq ??? Hneq1)) 
+    cases (eq_region ??) @refl ]
+  cut (eq_block b2 (mk_block r next) = false)
+  [ whd in ⊢ (??%%);
+    >(eqZb_false … (sym_neq ??? Hneq2))
+    cases (eq_region ??) @refl ]
+  #Heq_block_2
+  #Heq_block_1
+  * [ * [ * | ] | ]
+  whd in match (update_block ?????);
+  >Heq_block_1 normalize nodelta
+  whd in match (update_block ?????);
+  >Heq_block_2 normalize nodelta
+  #H
+  try /4 by or_introl, or_intror, conj/
+  [ %1 %2 whd whd in H;
+    >unfold_high_bound
+    whd in match (update_block ?????);
+    >unfold_low_bound
+    whd in match (update_block ?????);
+    >Heq_block_1 normalize nodelta @H
+  | %2 whd whd in H; 
+    >unfold_high_bound
+    whd in match (update_block ?????);
+    >unfold_low_bound
+    whd in match (update_block ?????);
+    >Heq_block_1 >Heq_block_2 @H
+  ]
+| #b whd @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta try //
+  #Hneq lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?);
+  cases (E (block_id b)) normalize nodelta try //
+  * #bb #oo normalize nodelta
+  * * * #HA #HB * #HC #HD #HE @conj try @conj
+  try @conj
+  lapply HE -HE
+  lapply HD -HD
+  lapply HC -HC
+  lapply HB -HB
+  lapply HA -HA
+  >unfold_low_bound >unfold_low_bound [ >unfold_low_bound ]
+  >unfold_high_bound >unfold_high_bound [ 2,5: >unfold_high_bound ]
+ cases m1 in Halloc; #cont #next #Hnext
+ whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) try //
+ whd in match (update_block ?????);
+ cut (eq_block b (mk_block r next) = false)
+ [ 1,3,5: whd in ⊢ (??%%); 
+          >(eqZb_false … (sym_neq ??? Hneq)) 
+          cases (eq_region ??) @refl
+ | 2,4,6: #Heq_block >Heq_block // ]
+] qed. 
+  
+       
 
 (* Embed a fresh block inside an unmapped portion of the target block.
@@ -820 +914 @@
   z2 + Zoo delta ≤ high_bound m2 b2 →
   (∀b,b',delta'. b ≠ (pi1 … new_block) →
-                 E b = Some ? 〈b', delta'〉 →
+                 E (block_id b) = Some ? 〈b', delta'〉 →
                  high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨
                  z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) →                 
   memory_inj E m1 m2 →
-  memory_inj (λx. if eq_block x (pi1 … new_block) then Some ? 〈b2, delta〉 else E x) m1' m2.
+  memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then Some ? 〈b2, delta〉 else E x) m1' m2.
 
 (* -------------------------------------- *)
@@ -875 +969 @@
   load_sim_ptr E m1 m2 →
   ∀b. free m2 b = m2' →
-      (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
+      (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
       load_sim_ptr E m1 m2'.      
 #E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped
@@ -960 +1054 @@
 #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
 #Hembed1 #Hembed2
-cases (block_decidable_eq ??) normalize nodelta
+@(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta
 [ 2: try // ]
-#Hblocks_eq destruct (Hblocks_eq)
+#Hblocks_eq
+lapply Hembed2 -Hembed2
 lapply Hembed1 -Hembed1
-lapply Hembed2 -Hembed2
-generalize in match b2';
-#target #Hembed2 #Hembed1
+lapply Hblocks_eq -Hblocks_eq
+cases b1' #r1' #bid1'
+cases b2' #r2' #bid2'
+#Heq destruct (Heq)
+generalize in match bid2';
+#target #Hembed1 #Hembed2
 lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2)
-cases (block_decidable_eq ??)
-[ 2: * #Habsurd @False_ind @Habsurd @refl ] #Hrefl
+>eqZb_z_z normalize nodelta
 normalize nodelta <Hfree
 @(eq_block_elim … b1 b)
@@ -1015 +1112 @@
 | @(free_non_aliasing_m1 … Hinj … Hfree)
 | #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?);
-  cases (E bb) normalize nodelta try //
+  cases (E (block_id bb)) normalize nodelta try //
   * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj
   try //
@@ -1043 +1140 @@
   memory_inj E m1 m2 →
   ∀b. free m2 b = m2' →
-      (∀b1,delta. E b1 = Some ? 〈b, delta〉 →
+      (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 →
       (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) →  
       memory_inj E m1 m2'.
@@ -1051 +1148 @@
 [ @(free_load_sim_ptr_m2 … Hload_sim … Hfree) #b1 #delta #Hembed
   @(b_not_mapped … b1 delta Hembed)
-| @Hfreeblock   
+| @Hfreeblock
 | * #bp #op #p' #Hp_valid #Hptr_trans
   @(eq_block_elim … (pblock p') b)
@@ -1074 +1171 @@
 | @Hregion
 | #bb lapply (Himpl bb)
-  whd in ⊢ (% → %); cases (E bb) normalize nodelta try //
+  whd in ⊢ (% → %); cases (E (block_id bb)) normalize nodelta try //
   * #BLO #OFF normalize nodelta * * destruct (Hfree)
   #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption
@@ -1094 +1191 @@
   memory_inj E m1 m2 →
   ∀blocklist,b2.
-  (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) → 
+  (∀b1,delta. E (block_id b1) = Some ? 〈b2, delta〉 → meml ? b1 blocklist) → 
   free m2 b2 = m2' → 
   free_list m1 blocklist = m1' →
@@ -1135 +1232 @@
     ]
   ]
-] qed.  
+] qed.
 
 (* ---------------------------------------------------------- *)
@@ -1230 +1327 @@
     memory_inj E mA mB →
     ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
-    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
+    ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 →
     high_bound mA b1 + Zoo delta < Zoo wo →
     ∀ty,off. 
@@ -1308 +1405 @@
     memory_inj E mA mB →
     ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC →
-    ∀b1,delta. E b1 = Some ? 〈blo,delta〉 →
+    ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 →
     Zoo wo < low_bound mA b1 + Zoo delta →
     ∀ty,off. 
@@ -1325 +1422 @@
   ∀block2. ∀i : offset. ∀ty : type.
   (∀block1,delta.
-    E block1 = Some ? 〈block2, delta〉 →
+    E (block_id block1) = Some ? 〈block2, delta〉 →
     (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
   ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
@@ -1381 +1478 @@
   ∀block2. ∀i : offset. ∀ty : type.
   (∀block1,delta.
-    E block1 = Some ? 〈block2, delta〉 →
+    E (block_id block1) = Some ? 〈block2, delta〉 →
     (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) →
   ∀v.store_value_of_type ty mB block2 i v = Some ? mC →
@@ -1411 +1508 @@
   >(Hnext_eq) try //
 | #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %);
-  cases (E b) try //
+  cases (E (block_id b)) try //
   * #BLO #OFF normalize nodelta * *
   #Hb #HBLO #Hbound try @conj try @conj try assumption
@@ -1473 +1570 @@
   ∀E,m1,m2.
   memory_inj E m1 m2 →
-  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
+  ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 →
   ∀v1,v2. value_eq E v1 v2 →
   ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
@@ -1542 +1639 @@
   ∀E,m1,m2.
   memory_inj E m1 m2 →
-  ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 →
+  ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 →
   ∀v1,v2. value_eq E v1 v2 →
   ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→
@@ -1565 +1662 @@
   ∀Hinj:memory_inj E m1 m2.
   ∀v1,v2. value_eq E v1 v2 →
-  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
+  ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 →
   ∀ty,i,m1'. 
   ast_typ_consistent_with_value ty v1 →
@@ -1653 +1750 @@
   ∀Hinj:memory_inj E m1 m2.
   ∀v1,v2. value_eq E v1 v2 →
-  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
+  ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 →
   ∀ty,i,m1'. 
   type_consistent_with_value ty v1 →
@@ -1673 +1770 @@
   ∀Hinj:memory_inj E m1 m2.
   ∀ty,b,i,v.
-  E b = None ? →
+  E (block_id b) = None ? →
   store_value_of_type ty m1 b i v = Some ? m1' →
   load_sim_ptr E m1' m2.
@@ -1723 +1820 @@
   ∀Hinj:memory_inj E m1 m2.
   ∀ty,b,i,v.
-  E b = None ? →
+  E (block_id b) = None ? →
   store_value_of_type ty m1 b i v = Some ? m1' →
   memory_inj E m1' m2.
@@ -1752 +1849 @@
     | #bb whd
       lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?);
-      cases (E bb) normalize nodelta try // * #bb' #off
+      cases (E (block_id bb)) normalize nodelta try // * #bb' #off
       normalize nodelta
       whd in match (block_implementable_bv ??);      
@@ -1763 +1860 @@
       >HA >HB //
     ]
-] qed.    
+] qed.
 
 (* ------------------------------------------------------------------------- *)
@@ -1855 +1952 @@
           @(ex_intro … (conj … (refl …) ?))
           @vptr_eq whd in match (pointer_translation ??);
-          cases (E b1') in Hembed;
+          cases (E (block_id b1')) in Hembed;
           [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
           | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
@@ -1897 +1994 @@
      @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
      elim p1 in Hembed; #b1 #o1 normalize nodelta
-     cases (E b1)
+     cases (E (block_id b1))
      [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
      | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
@@ -1996 +2093 @@
           @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
           elim p1 in Hembed; #b1 #o1 normalize nodelta
-          cases (E b1)
+          cases (E (block_id b1))
           [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
           | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
@@ -2012 +2109 @@
                elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
                whd in ⊢ ((??%?) → (??%?) → ?);
-               cases (E b1') normalize nodelta
+               cases (E (block_id b1')) normalize nodelta
                [ 1: #Habsurd destruct (Habsurd) ]
                * #dest_block #dest_off normalize nodelta
@@ -2418 +2515 @@
           lapply (mi_nowrap … Hinj bq1) 
           whd in ⊢ (% → ?);
-          cases (E bq1) normalize nodelta
+          cases (E (block_id bq1)) normalize nodelta
           [ #_ #Habsurd destruct ]
           * #BLO #OFF normalize nodelta * *          
@@ -2437 +2534 @@
           lapply (mi_nowrap … Hinj bp1) whd in ⊢ (% → ?);
           lapply (mi_nowrap … Hinj bq1) whd in ⊢ (% → ?);
-          cases (E bq1) [ 1: #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
+          lapply (mi_region … Hinj bq1)
+          lapply (mi_region … Hinj bp1)
+          cases (E (block_id bq1)) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
           * #BLOq #DELTAq normalize nodelta
-          cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
-          * #BLOp #DELTAp normalize nodelta #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
+          cases (E (block_id bp1)) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
+          * #BLOp #DELTAp normalize nodelta #Hregion1 #Hregion2 #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
+          lapply (Hregion1 … (refl ??)) lapply (Hregion2 … (refl ??)) -Hregion1 -Hregion2
+          #Hregion2 #Hregion1
           cases op
           whd in ⊢ ((??%?) → ?); #H' destruct (H')
@@ -2455 +2556 @@
           lapply (valid_pointer_to_Prop … Hvalid')
           * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp
-          >eq_block_b_b normalize nodelta
+          >eqZb_z_z >eq_block_b_b normalize nodelta
           * 
           [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind

src/Clight/toCminorCorrectnessExpr.ma

@@ -34 +34 @@
       match find_symbol ? (ge_cl cminv) id with
       [ None ⇒ True
-      | Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
+      | Some cl_blo ⇒ 
+        (* global symbols are mapped to themselves. Perhaps too strong. *)
+        E (block_id cl_blo) = Some ? 〈cl_blo, zero_offset〉
       ]
     | Some cl_blo ⇒
@@ -42 +44 @@
             match vtype with
             [ Stack n ⇒
-              E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
+              E (block_id cl_blo) = Some ? 〈sp, mk_offset (repr I16 n)〉
             | Local ⇒
               ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
@@ -2210 +2212 @@
        @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
        %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
-       cases (E cl_blo) in Hptr_translate; normalize nodelta
+       cases (E (block_id cl_blo)) in Hptr_translate; normalize nodelta
        [ #H destruct (H) ]
        * #BL #OFF normalize nodelta #Heq destruct (Heq)
@@ -2222 +2224 @@
        >(commutative_addition_n … (repr I16 field_off) (offv OFF))
        >(associative_addition_n ? (offv off))
-       @refl        
+       @refl
   | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
        cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)

src/Clight/toCminorOps.ma

@@ -192 +192 @@
 lapply H1 lapply H2 -H1 -H2
 whd in ⊢ ((??%?) → (??%?) → ?);
-cases (E b2) normalize nodelta
+cases (E (block_id b2)) normalize nodelta
 [ #Habsurd destruct ]
 * #bx #ox normalize nodelta #Heq1 #Heq2 destruct