Changeset 2255 for src/Clight/switchRemoval.ma

Timestamp:

Jul 24, 2012, 8:12:00 PM (9 years ago)

Author:

garnier

Message:

Had to modify the definition of memory injections to prove that valid_pointer is preserved.

File:

• src/Clight/switchRemoval.ma (modified) (13 diffs)

src/Clight/switchRemoval.ma

@@ -1251 +1251 @@
   pointer_translation p1 E = Some ? p2 →
   value_eq E (Vptr p1) (Vptr p2).
-  
+
 (* [load_sim] states the fact that each successful load in [m1] is matched by such a load in [m2] s.t.
  * the values are equivalent. *)
@@ -1257 +1257 @@
 λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
  ∀b1,off1,b2,off2,ty,v1.
-  valid_block m1 b1 →
+  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〉 →
   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).
 
+definition load_sim_ptr ≝
+λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
+ ∀b1,off1,b2,off2,ty,v1.
+  valid_pointer m1 (mk_pointer b1 off1) = true →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
+  pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) →
+  load_value_of_type ty m1 b1 off1 = Some ? v1 →
+  (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).
+
 (* Definition of a memory injection *)
 record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
 { (* Load simulation *)
-  mi_inj : load_sim E m1 m2;
+  mi_inj : load_sim_ptr E m1 m2;
   (* Invalid blocks are not mapped *)
   mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
+  (* Valid pointers are mapped to valid pointers*)
+  mi_valid_pointers : ∀p,p'. 
+                       valid_pointer m1 p = true → 
+                       pointer_translation p E = Some ? p' →
+                       valid_pointer m2 p' = true;
   (* Blocks in the codomain are valid *)
-  mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
+  (* mi_incl : ∀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';
@@ -1283 +1296 @@
 
 (* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\ 
- * A memory extension is a [memory_inj] with some particular blocks designated *)
+ * A memory extension is a [memory_inj] with some particular blocks designated as
+ * being writeable. *)
 
 alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
@@ -1289 +1303 @@
 record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
 { me_inj : memory_inj E m1 m2;
+  (* A list of blocks where we can write freely *)
   me_writeable : list block;
+  (* These blocks are valid *)
   me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;
-  me_writeable_ok : ∀b,b',o'. 
-                    valid_block m1 b → 
-                    E b = Some ? 〈b',o'〉 →
-                    ¬ (meml ? b' me_writeable)
+  (* And pointers to m1 are oblivious to these blocks *)
+  me_writeable_ok : ∀p,p'. 
+                     valid_pointer m1 p = true →
+                     pointer_translation p E = Some ? p' →
+                     ¬ (meml ? (pblock p') me_writeable)
 }.
 
@@ -1420 +1437 @@
 #E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
 lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
-     normalize in Hembed;
-     lapply (mi_inj … Hinj b1 off1)
-     cases (E b1) in Hembed;
-     [ 1: normalize #Habsurd destruct (Habsurd)
-     | 2: * #b2' #off2' #H normalize in H; destruct (H) #Hyp lapply (Hyp b2 off2' ty v1) -Hyp ]
-     lapply (refl ? (access_mode ty))
-     cases ty
-     [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
-     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
-     normalize in ⊢ ((???%) → ?); #Hmode #Hyp
-     [ 1,7,8: #Habsurd normalize in Habsurd; destruct (Habsurd)
-     | 5,6: #Heq normalize in Heq; destruct (Heq) /4 by ex_intro, conj/ ]
-     #Hload_success
-     lapply (load_by_value_success_valid_block … Hmode … Hload_success)
-     #Hvalid_block @(Hyp Hvalid_block (refl ??) Hload_success)
-qed.
+lapply (refl ? (access_mode ty))
+cases ty
+[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
+| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
+normalize in ⊢ ((???%) → ?); #Hmode #Hyp
+[ 1,7,8: normalize in Hyp; destruct (Hyp)
+| 5,6: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]
+lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer
+lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H
+qed.     
 
 
@@ -1523 +1534 @@
   | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
 | 2: @(mi_freeblock … Hmemory_inj)
-| 3: #b #b' #o' #HE
-     lapply (mi_incl … Hmemory_inj … HE)
-     elim m2 in Halloc; #contents #nextblock #Hnextblock
-     whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
-     whd in match (valid_block ??) in ⊢ (% → %); /2/
+| 3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
+     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
+     elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
+     whd in match (valid_pointer ??) in ⊢ (% → %);
+     @Zltb_elim_Type0
+     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
+     #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
+     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
+     whd in match (high_bound ??) in ⊢ (% → %); 
+     whd in match (update_block ?????); 
+     whd in match (eq_block ??); 
+     cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]
+     #Hbid_neq >Hbid_neq
+     cases (eq_region br' r) normalize #H @H
 | 4: @(mi_region … Hmemory_inj)
 | 5: @(mi_disjoint … Hmemory_inj)
@@ -1547 +1567 @@
       whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
       /2/
-| 4: #b #b' #o' normalize in ⊢ (% → ?); #Hvalid_b #Hload %
-     normalize in ⊢ (% → ?); * [ 2: #H @(False_ind … H) ]
-     #Heq destruct (Heq) 
-     lapply (mi_incl … Hmemory_inj … Hload)
-     whd in ⊢ (% → ?); #Habsurd
-     (* contradiction car ¬ (valid_block m2 new_block)  *)
-     elim m2 in Halloc Habsurd;
+| 4: * #b #o * #b' #o' #Hvalid_ptr #Hembed %
+     normalize in ⊢ (% → ?); * [ 2: #H @H ]
+     #Heq destruct (Heq)
+     lapply (mi_valid_pointers … Hmemory_inj … Hvalid_ptr Hembed)
+     whd in ⊢ (% → ?);
+     (* contradiction because ¬ (valid_block m2 new_block)  *)
+     elim m2 in Halloc;
      #contents_m2 #nextblock_m2 #Hnextblock_m2
      whd in ⊢ ((??%?) → ?);
      #Heq_alloc destruct (Heq_alloc)
-     lapply (irreflexive_Zlt nextblock_m2) * #Hcontr #Habsurd @(Hcontr Habsurd)
+     normalize
+     lapply (irreflexive_Zlt nextblock_m2)
+     @Zltb_elim_Type0
+     [ #H * #Habsurd @(False_ind … (Habsurd H)) ] #_ #_ normalize #Habsurd destruct (Habsurd)
 ] qed.
 
@@ -1618 +1641 @@
   ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 
   bestorev mB (mk_pointer wb wo) v = Some ? mC →
-  load_sim E mA mC.
+  load_sim_ptr E mA mC.
 #E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
-(* Show that (wb ≠ b2) *)
-lapply (me_writeable_ok … Hext … Hvalid Hembed) #Hb2
+(* Show that (wb ≠ b2) by showing b2 ∉ (me_writeable ...) *)
+lapply (me_writeable_ok … Hext (mk_pointer b1 off1) (mk_pointer b2 off2) Hvalid Hembed) #Hb2
 lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
 cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
@@ -1642 +1665 @@
 elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
 #Hmem
-[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] - Hvalid -Hregion -Hdisjoint -Hwriteable_ok -Hinj
+[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] -Hvalid -Hregion -Hdisjoint
 whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
 normalize in ⊢ (% → ?); #Hlt_wb
+#p #p' #HvalidA #Hembed lapply (Hcodomain … HvalidA Hembed) -Hcodomain
+normalize in match (valid_pointer ??) in ⊢ (% → %);
 >(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
 cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb)))
@@ -1650 +1675 @@
 [ 2: #Habsurd destruct (Habsurd) ]
 #Heq destruct (Heq)
-#b #b' #o' #Hembed @(Hcodomain … Hembed)
+cases (Zltb (block_id (pblock p')) nextblockB) normalize nodelta
+[ 2: // ]
+whd in match (update_block ?????);
+cut (eq_block (pblock p') wb = false)
+[ 2: #Heq >Heq normalize nodelta #H @H ]
+@neq_block_eq_block_false @sym_neq
+@(mem_not_mem_neq writeable … Hmem)
+@(Hwriteable_ok … HvalidA Hembed)
 qed.
 
@@ -2711 +2743 @@
 ] qed.
 
-(* We want to prove that, but we can't since valid_pointers can in fact be one off outside the block,
-   and [memory_inj] handles only stuff that is loadable (i.e. inside a block). TODO *)
-lemma pointer_eq_valid :
-∀E,m,m',p,p'.
- memory_inj E m m' → 
- pointer_translation p E = Some ? p' →
- valid_pointer m p → 
- valid_pointer m' p'.
+lemma Zplus_eq_eq : ∀x,y,delta:Z. eqZb x y = eqZb (x + delta) (y + delta).
+#x #y #delta
+@eqZb_elim
+[ 1: #Heq >Heq >eqZb_z_z @refl
+| 2: * #Hneq cut (x+delta ≠ y + delta)
+     [ 1: % #H cut (x = y) [ 1: @(injective_Zplus_l delta) @H ] #H' @Hneq @H' ]
+     #H @sym_eq @eqZb_false @H ] qed.
+
+(* offset equality is invariant by translation *)
+lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
+#delta #x #y normalize
+elim delta #zdelta @sym_eq @Zplus_eq_eq qed.
+
+lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y.
+#delta #x #y normalize
+elim delta #zdelta @sym_eq <Zplus_eq_eq @refl qed.
+
+(* The key problem is that [sem_cmp] is a let-rec defined on [op], but we /don't want/ to
+   perform a case-analysis on [op]. TODO: try and see if specifying another pseudo-decreasing
+   argument is ok. This just won't cut it.. *)
+lemma sem_cmp_value_eq :
+  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
+   value_eq E v1 v2 →
+   value_eq E v1' v2' →
+   memory_inj E m1 m2 →   
+   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→
+           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
 @cthulhu qed.
 
-
+(*           
+#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
+elim m1 in Hinj; #contents_map1 #nextblock1 #Hnextblock1 #Hinj
+cases op whd in match (sem_cmp ??????) in ⊢ (% → ?);
+cases (classify_cmp ty ty') normalize nodelta
+[ 1,9,17: #sz #sg
+  @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
+  [ 1,6,11: #v #Habsurd destruct (Habsurd)
+  | 2,7,12: #sz #i @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
+    [ 1,6,11: #v' #Habsurd destruct (Habsurd)
+    | 2,7,12: #sz' #i'
+    | 3,8,13: #f #Habsurd destruct (Habsurd)
+    | 4,9,14: #Habsurd destruct (Habsurd)
+    | 5,10,15: #p1 #p2 #Hembed destruct (Habsurd) ]
+
+  | 3,8,13: #f #Habsurd destruct (Habsurd)    
+  | 4,9,14: #Habsurd destruct (Habsurd)
+  | 5,10,15: #p1 #p2 #Hembed destruct (Habsurd) ]
+| 2,10,18: #n #ty0 | 3,11,19: #fsz | 4,12,20: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
+[ 1,6,11,16,21,26,31,36,41,46,51,56,61,66,71,76,81,86,91,96: #v #Habsurd destruct (Habsurd)
+| 2,7,12,17,22,27,32,37,42,47,52,57,62,67,72,77,82,87,92,97: #sz' #i
+
+| 
+| 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
+*)
+
+
+(* The proof of the following lemma begs for factorization. *)
+(*
 lemma sem_cmp_value_eq :
   ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
@@ -2731 +2810 @@
 #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
 cases op whd in match (sem_cmp ??????); whd in match (sem_cmp ??????);
-[ 1:
+[ 1: (* Equality *)
   cases (classify_cmp ty ty') normalize nodelta
   [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
@@ -2752 +2831 @@
   | 16,19: whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
         /3 by ex_intro, conj, vint_eq/
-  | 20: @cthulhu (* relies on [pointer_eq_valid] TODO *)   
+  | 20: lapply (mi_valid_pointers … Hinj p1' p2')
+        lapply (mi_valid_pointers … Hinj p1 p2)
+        cases (valid_pointer m1 p1')
+        [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
+        cases (valid_pointer m1 p1)
+        [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
+        #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
+        >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
+        elim p1 in Hembed; #b1 #o1
+        elim p1' in Hembed'; #b1' #o1'
+        whd in match (pointer_translation ??);
+        whd in match (pointer_translation ??);
+        @(eq_block_elim … b1 b1')
+        [ 1: #Heq destruct (Heq)
+              cases (E b1')
+              [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
+              * #eb1' #eo1' normalize nodelta
+              #Heq1 #Heq2 #Heq3 destruct
+              >eq_block_identity normalize nodelta
+              >eq_offset_translation cases (cmp_offset ???)
+              /3 by ex_intro, conj, vint_eq/
+        | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
+             cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
+             * #eb1 #eo1
+             cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
+             * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
+             lapply (H ???? Hneq (refl ??) (refl ??))
+             #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
+             #Heq destruct (Heq) whd in match (sem_cmp_mismatch Ceq);
+             %{Vfalse} @conj try @refl normalize in Heq; destruct (Heq)
+             @vint_eq ]
   | *: #Habsurd destruct (Habsurd) ]
-| *: @cthulhu ]
-qed.
+| 2: (* Inequality *)
+  cases (classify_cmp ty ty') normalize nodelta
+  [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
+  @(value_eq_inversion E … Hvalue_eq1)
+  [ 1,6,11: #v | 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
+  normalize nodelta
+  [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ]
+  @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
+  [ 1,6,11,16: #v' | 2,7,12,17: #sz' #i' | 3,8,13,18: #f' | 4,9,14,19: | 5,10,15,20: #p1' #p2' #Hembed' ]
+  [ 5: cases sg normalize nodelta
+       @intsize_eq_elim_elim
+       [ 1,3: #_ #Habsurd destruct (Habsurd)
+       | 2,4: #Heq destruct (Heq) normalize nodelta
+              [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq)
+              | 2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ]
+              /3 by ex_intro, conj, vint_eq/ ]
+  | 10: #Heq destruct (Heq) cases (Fcmp Cne f f') /3 by ex_intro, conj, vint_eq/
+  | 15: whd in match (sem_cmp_match ?) in ⊢ (% → %); #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
+  | 16,19: whd in match (sem_cmp_mismatch ?) in ⊢ (% → %); #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
+  | 20: lapply (mi_valid_pointers … Hinj p1' p2')
+        lapply (mi_valid_pointers … Hinj p1 p2)
+        cases (valid_pointer m1 p1')
+        [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
+        cases (valid_pointer m1 p1)
+        [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
+        #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
+        >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
+        elim p1 in Hembed; #b1 #o1
+        elim p1' in Hembed'; #b1' #o1'
+        whd in match (pointer_translation ??);
+        whd in match (pointer_translation ??);
+        @(eq_block_elim … b1 b1')
+        [ 1: #Heq destruct (Heq)
+              cases (E b1')
+              [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
+              * #eb1' #eo1' normalize nodelta
+              #Heq1 #Heq2 #Heq3 destruct
+              >eq_block_identity normalize nodelta
+              >neq_offset_translation cases (cmp_offset ???)
+              /3 by ex_intro, conj, vint_eq/
+        | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
+             cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
+             * #eb1 #eo1
+             cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
+             * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
+             lapply (H ???? Hneq (refl ??) (refl ??))
+             #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
+             #Heq destruct (Heq) whd in match (sem_cmp_mismatch Cne);
+             %{Vtrue} @conj try @refl normalize in Heq; destruct (Heq)
+             @vint_eq ]
+  | *: #Habsurd destruct (Habsurd) ]
+| 3: (* Less-than *)
+  
+| 3: *: @cthulhu ]
+qed.*)
  
 (* Commutation result for binary operators. *)