Ignore:
Timestamp:
Jan 29, 2013, 8:28:44 PM (8 years ago)
Author:
garnier
Message:

Some fixes in memory injections, and some holes filled.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/memoryInjections.ma

    r2588 r2594  
    9898(* Lemmas related to freeing memory and pointer validity. *)
    9999(* --------------------------------------------------------------------------- *)   
    100 (*
    101 lemma nextblock_free_ok : ∀m,b. nextblock m = nextblock (free m b).
    102 * #contents #next #posnext * #rg #id
    103 normalize @refl
    104 qed.
    105 
    106 lemma low_bound_free_ok : ∀m,b,ptr.
    107    b ≠ (pblock ptr) →
    108    Zleb (low_bound (free m b) (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) =
    109    Zleb (low_bound m (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))).
    110 * #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize
    111 cases prg cases brg normalize nodelta try //
    112 @(eqZb_elim pid bid)
    113 [ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??)))
    114 | 2,4: #_ #_ @refl
    115 ] qed.
    116 
    117 lemma high_bound_free_ok : ∀m,b,ptr.
    118    b ≠ (pblock ptr) →
    119    Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound (free m b) (pblock ptr)) =
    120    Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound m (pblock ptr)).
    121 * #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize
    122 cases prg cases brg normalize nodelta try //
    123 @(eqZb_elim pid bid)
    124 [ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??)))
    125 | 2,4: #_ #_ @refl
    126 ] qed.
    127 
    128 lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr.
    129    valid_pointer m ptr = true →
    130    pblock ptr ≠ b →
    131    valid_pointer (free m b) ptr = true.
    132 * #br #bid * #contents #next #posnext * * #pbr #pbid #poff
    133 normalize
    134 @(eqZb_elim pbid bid)
    135 [ 1: #Heqid >Heqid cases pbr cases br normalize
    136      [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
    137      cases (Zltb bid next) normalize nodelta
    138      [ 2,4: #Habsurd destruct (Habsurd) ]
    139      //
    140 | 2: #Hneqid cases pbr cases br normalize try // ]
    141 qed.
    142 
    143 lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr.
    144    valid_pointer m ptr = true →
    145    ¬ mem ? (pblock ptr) blocks →
    146    valid_pointer (free_list m blocks) ptr = true.
    147 #blocks
    148 elim blocks
    149 [ 1: #m #ptr normalize #H #_ @H
    150 | 2: #b #tl #Hind #m #ptr #Hvalid
    151      whd in match (mem block (pblock ptr) ?);
    152      >free_list_cons * #Hguard
    153      @valid_pointer_free_ok
    154      [ 2: % #Heq @Hguard %1 @Heq ]
    155      @Hind
    156      [ 1: @Hvalid
    157      | 2: % #Hmem @Hguard %2 @Hmem ]
    158 ] qed. *)
    159 
    160100
    161101lemma valid_pointer_ok_free : ∀b : block. ∀m,ptr.
    … …  
    367307    (high_bound m b) + (Zoo delta) < Z_two_power_nat 16
    368308  ].
    369    
     309
    370310
    371311(* Adapted from Compcert's Memory *)
    … …  
    381321(*    block_is_empty m b1' ∨ *)
    382322    high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨
    383     high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1)
     323    high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1) ∨
     324    block_is_empty m b1 ∨
     325    block_is_empty m b2
    384326  | inr Hneq ⇒ True
    385327  ].
    … …  
    393335  mi_inj : load_sim_ptr E m1 m2;
    394336  (* Invalid blocks are not mapped *)
    395   (* mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; *)
     337  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
    396338  (* Valid pointers are mapped to valid pointers *)
    397339  mi_valid_pointers : ∀p,p'.
    … …  
    427369definition empty_injection : memory_inj (λx. None ?) empty empty.
    428370%
    429 [ 1: whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hptr_trans #Hload
    430      normalize in Hptr_trans; destruct
    431 | 2: * #b #o #p' #_ normalize #Habsurd destruct
    432 | 3: #b #b' #off #Habsurd destruct
    433 | 4: #b #b' #o' #Habsurd destruct
    434 | 5: whd #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct
    435 | 6: #b whd @I
     371[ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hptr_trans #Hload
     372  normalize in Hptr_trans; destruct
     373| #b #H @refl
     374| * #b #o #p' #_ normalize #Habsurd destruct
     375| #b #b' #off #Habsurd destruct
     376| #b #b' #o' #Habsurd destruct
     377| whd #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct
     378| #b whd @I
    436379] qed.
    437380
    … …  
    709652     @Hload
    710653  | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
     654| @(mi_freeblock … Hmemory_inj)
    711655| #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
    712656     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
    … …  
    744688       try assumption ]
    745689] qed.
    746 (*       
    747    | @(eq_block_elim … new_block B)
    748      [ 2: #H cases m2 in Halloc Hinbounds; #contents #nextblock #notnull
    749        whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    750        >unfold_high_bound in Himpl ⊢ %;
    751        whd in ⊢ (% → % → %);
    752        >unfold_low_bound >unfold_high_bound
    753        whd in match (update_block ?????); >eq_block_b_b
    754        normalize nodelta * #HA #HB
    755        >unfold_high_bound       
    756        whd in match (update_block ?????) in ⊢ (% → %);
    757        >(not_eq_block … (sym_neq ??? H)) normalize nodelta
    758        try //
    759      | (* absurd case *) #Heq destruct (Heq)
    760        lapply (Hguard ?? (refl ??)) #Hvalid
    761        (* hence new_block ≠ B *)
    762        cases m2 in Halloc Hvalid; #contents #nextblock #notnull
    763        whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    764        whd in ⊢ (% → ?); #Habsurd
    765        lapply (irreflexive_Zlt nextblock) *
    766        #H @False_ind @H @Habsurd
    767      ]
    768    ]
    769 ]
    770 qed. *)
    771690
    772691
    … …  
    786705  memory_inj E m1' m2.
    787706
    788 (* Embed a fresh block inside an unmapped portion of the target
    789    block. *)
     707(* Embed a fresh block inside an unmapped portion of the target block.
     708 * This is the equivalent of lemma 45 for Leroy&Blazy. *)
    790709axiom alloc_memory_inj_m1_to_m2 :
    791710  ∀E:embedding.
    … …  
    829748
    830749(* lemma 47 of L&B *)
     750
     751lemma free_loadn_sim_ptr_m2 :
     752  ∀sz,m,b,b',o,res.
     753   b ≠ b' →
     754   loadn m (mk_pointer b' o) sz = Some ? res →
     755   loadn (free m b) (mk_pointer b' o) sz = Some ? res.
     756#sz
     757elim sz
     758[ normalize //
     759| #sz' #Hind #m #b #b' #o #res #Hneq whd in ⊢ ((??%?) → (??%?));
     760  #H cases (some_inversion ????? H) -H #beres *
     761  #Hbeloadv #Hloadn
     762  lapply (beloadv_free_beloadv2 m b ??? Hbeloadv)
     763  [ @sym_neq @Hneq ]
     764  #Hbeloadv' >Hbeloadv' normalize nodelta
     765  cases (some_inversion ????? Hloadn) -Hloadn #bevals * #Hloadn
     766  #Heq destruct (Heq)
     767  >(Hind … Hneq Hloadn) normalize nodelta @refl
     768] qed. 
     769
    831770lemma free_load_sim_ptr_m2 :
    832771  ∀E:embedding.
    … …  
    844783             normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl
    845784             %4 @Htrans ]
    846 #Hload <Hfree
    847 (* routine *)
    848 @cthulhu
    849 qed.
     785lapply Htrans -Htrans lapply Hsim -Hsim lapply Hfree -Hfree
     786cases m2 #contents2 #next2 #Hnext2
     787whd in ⊢ ((??%?) → ?); #Hm2' destruct
     788#Hsim #Htrans
     789cases (some_inversion ????? Htrans) * #b2' #off2' * #Hembed normalize nodelta
     790#Heq destruct (Heq) #Hload
     791lapply (Hsim … Hvalid … Htrans … Hload)
     792* #v2' * #Hload_before_free #Hvalue_eq
     793@(eq_block_elim … b2 b)
     794[ 1,3,5: #Heq destruct
     795         lapply (Hunmapped b1 off2' Hembed) *
     796         [ 1,3,5: #Hnot_valid lapply (valid_pointer_to_Prop … Hvalid)
     797                  -Hvalid whd in match (valid_block ??) in Hnot_valid;
     798                  * * #Hvalid #_ #_ @False_ind
     799                  cases Hnot_valid #H @H @Hvalid
     800         | *: whd in ⊢ (% → ?); #Hempty
     801              lapply (valid_pointer_to_Prop … Hvalid)
     802              -Hvalid * * #_ #Hlow #Hhigh
     803              cut ((low_bound m1 b1 < high_bound m1 b1))
     804              [ 1,3,5: /2 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle_to_Zlt/ ]
     805              #Hnonempty @False_ind -Hlow -Hhigh
     806              lapply (Zlt_to_Zle_to_Zlt … Hnonempty Hempty)
     807              #H cases (irreflexive_Zlt (low_bound m1 b1)) #H' @H' @H ]
     808| *: #Hneq %{v2'} @conj try assumption
     809     whd in match (load_value_of_type ????) in Hload_before_free:(??%?) ⊢ (??%?);
     810     cases (some_inversion ????? Hload_before_free) -Hload_before_free
     811     #bevals * #Hloadn #Heq
     812     >(free_loadn_sim_ptr_m2 … Hloadn) normalize nodelta
     813     try assumption @sym_neq @Hneq
     814] qed.     
    850815
    851816lemma free_block_is_empty :
    … …  
    864829qed.
    865830
     831lemma high_bound_freed_block :
     832  ∀m,b. high_bound (free m b) b = OZ.
     833#m #b normalize
     834cases (block_region b) normalize
     835>eqZb_z_z normalize @refl
     836qed.
     837
     838lemma low_bound_freed_block :
     839  ∀m,b. low_bound (free m b) b = (pos one).
     840#m #b normalize
     841cases (block_region b) normalize
     842>eqZb_z_z normalize @refl
     843qed.
     844
    866845(* Lemma 49 in Leroy&Blazy *)
    867 axiom free_non_aliasing_m1 :
     846lemma free_non_aliasing_m1 :
    868847  ∀E:embedding.
    869848  ∀m1,m2,m1'.
    … …  
    873852(* The proof proceeds by a first case analysis to see wether b lives in the
    874853   same world as the non-aliasing blocks (if not : trivial), in this case
    875    we proceed by a case analysis on the non-aliasing hypothesis in memory_inj. *)
    876 
     854   we proceed to a second case analysis on the non-aliasing hypothesis in
     855   memory_inj. *)
     856#E #m1 #m2 #m1' #Hinj #b #Hfree
     857whd
     858#b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
     859#Hembed1 #Hembed2
     860cases (block_decidable_eq ??) normalize nodelta
     861[ 2: try // ]
     862#Hblocks_eq destruct (Hblocks_eq)
     863lapply Hembed1 -Hembed1
     864lapply Hembed2 -Hembed2
     865generalize in match b2';
     866#target #Hembed2 #Hembed1
     867lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2)
     868cases (block_decidable_eq ??)
     869[ 2: * #Habsurd @False_ind @Habsurd @refl ] #Hrefl
     870normalize nodelta <Hfree
     871@(eq_block_elim … b1 b)
     872[ #Heq destruct (Heq) #Hcase
     873  %1 %2 whd
     874  >high_bound_freed_block >low_bound_freed_block
     875  //
     876| #Hneq1 @(eq_block_elim … b2 b)
     877  [ #Heq destruct (Heq) #Hcase
     878    %2 whd
     879    >high_bound_freed_block >low_bound_freed_block
     880    // ] ]
     881#Hneq2
     882>unfold_high_bound >unfold_high_bound >unfold_high_bound >unfold_high_bound
     883>unfold_low_bound >unfold_low_bound >unfold_low_bound >unfold_low_bound
     884<(high_free_eq … Hneq1) <(high_free_eq … Hneq2)
     885<(low_free_eq … Hneq1) <(low_free_eq … Hneq2)
     886*
     887[ 2: #H %2 whd >unfold_high_bound >unfold_low_bound
     888     <(low_free_eq … Hneq2) <(high_free_eq … Hneq2) @H ]
     889*
     890[ 2: #H %1%2 whd >unfold_high_bound >unfold_low_bound
     891     <(low_free_eq … Hneq1) <(high_free_eq … Hneq1) @H ]
     892* #H
     893[ %1 %1 %1 @H
     894| %1 %1 %2 @H ]
     895qed.
    877896
    878897(* Extending lemma 46 and 49 to memory injections *)
    … …  
    885904#E #m1 #m2 #m1' #Hinj #b #Hfree
    886905cases Hinj
    887 #Hload_sim #Hvalid #Hnodangling #Hregion #Hnonalias #Himplementable
     906#Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himplementable
    888907% try assumption
    889908[ @(free_load_sim_ptr_m1 … Hload_sim … Hfree)
     909| #bb #Hnot_valid lapply (Hfreeblock bb) #HA @HA % #HB
     910  cases Hnot_valid #HC @HC <Hfree @HB
    890911| #p #p' #Hvalid_m1' #Hptr_translation @(Hvalid p p' ? Hptr_translation)
    891912  <Hfree in Hvalid_m1'; @valid_free_to_valid
    … …  
    908929      normalize nodelta try @conj try // % try //
    909930  ]
    910 ] qed.   
    911 
    912 (*
    913   #b0 #b' #o' #Hembed lapply (Himplementable b0 b' o' Hembed) *
    914   #HA #HB @conj try //
    915   cases m1 in Hfree HA; #contents1 #nextblock1 #Hpos1
    916   whd in ⊢ ((??%%) → ? → ?); #Heq destruct (Heq)
    917   whd in ⊢ (% → %); *
    918   whd in match (low_bound ??) in ⊢ (% → % → %);
    919   whd in match (high_bound ??) in ⊢ (% → % → %); #HA #HB
    920   @(eq_block_elim … b0 b)
    921   [ #H whd in match (update_block ?????); >H >eq_block_b_b @conj
    922     normalize nodelta
    923     normalize @conj try //
    924   | #H whd in match (update_block ?????); >(not_eq_block … H) @conj
    925     try // ] ]
    926 qed.*)
    927 
    928 (* Lifting lemma 47 to memory injs *)
     931] qed.
     932
     933(* Lifting lemma 47 to memory injs - note that we require a much stronger condition
     934 * on the freed block : no block of m1 can map to it. Not even an invalid block or
     935 * an empty one.
     936 * XXX this lemma is not given in Leroy&Blazy, and unless future developments requires
     937 * it I will comment it out. XXX *)
    929938lemma free_memory_inj_m2 :
    930939  ∀E:embedding.
    … …  
    932941  memory_inj E m1 m2 →
    933942  ∀b. free m2 b = m2' →
    934       (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →
     943      (∀b1,delta. E b1 = Some ? 〈b, delta〉 →
     944      (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → 
    935945      memory_inj E m1 m2'.
    936 #E #m1 #m2 #m2' #Hinj #b #Hfree #b1_not_mapped
     946#E #m1 #m2 #m2' #Hinj #b #Hfree #b_not_mapped
    937947% cases Hinj try //
    938 #Hload_sim #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl
    939 [ (* We succed performing a load from m1. Case analysis: if by-value, cannot map to freed block [b]
    940      (otherwise contradiction), hence simulation proceeds through Hinj.
    941      If not by-value, then simulation proceeds without examining the contents of the memory *)
    942    @cthulhu
    943 | #p #p' #Hvalid #Hptr_trans
    944   (* We now through Hinj that valid_pointer m2 p'=true,
    945      if (pblock p') = b then  using b1_not_mapped and Hptr_trans we
    946      know that the original pointer must be either invalid or empty,
    947      hence contradiction with Hvalid
    948      if (pblock p') ≠ b then straightforward simulation *)
    949   @cthulhu
    950 | #bb #b' #o' #Hembed
    951   lapply (Hnodangling bb b' o' Hembed) #Hvalid_before_free
    952   (* cf case above *)
    953   @cthulhu
     948#Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl
     949[ @(free_load_sim_ptr_m2 … Hload_sim … Hfree) #b1 #delta #Hembed
     950  @(b_not_mapped … b1 delta Hembed)
     951| @Hfreeblock   
     952| * #bp #op #p' #Hp_valid #Hptr_trans
     953  @(eq_block_elim … (pblock p') b)
     954  [ #Heq lapply (Hvalid … Hp_valid Hptr_trans) #Hp_valid' destruct (Heq)
     955    cases (some_inversion ????? Hptr_trans)
     956    * #bp' #op' * #Hembed normalize nodelta #Heq destruct (Heq)
     957    cases (b_not_mapped … Hembed)
     958    [ #Hnot_valid lapply (Hfreeblock … Hnot_valid) >Hembed #Habsurd destruct (Habsurd)
     959    | #Hempty @False_ind lapply (valid_pointer_to_Prop … Hp_valid) * * #_
     960      whd in Hempty; #Hle #Hlt
     961      lapply (Zlt_to_Zle_to_Zlt … Hlt Hempty) #Hlt2
     962      lapply (Zlt_to_Zle_to_Zlt … Hlt2 Hle) #Hlt3
     963      @(absurd … Hlt3 (irreflexive_Zlt ?)) ]
     964  | #Hneq lapply (Hvalid … Hp_valid Hptr_trans) <Hfree #HA
     965    @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … HA) -HA * *
     966    #HA #HB #HC @conj try @conj try assumption
     967    [ >unfold_low_bound <(low_free_eq m2 ?? Hneq) @HB
     968    | >unfold_high_bound <(high_free_eq m2 ?? Hneq) @HC ]
     969  ]
     970| #bb #b' #o' #Hembed
     971  lapply (Hnodangling … Hembed) <Hfree //
    954972| @Hregion
    955973| #bb lapply (Himpl bb)
    … …  
    964982  #H [ 1,3,5: destruct (H) normalize nodelta try //
    965983               @conj try //
    966      | *: normalize nodelta cases HBLO try // ]     
     984     | *: normalize nodelta cases HBLO try // ]
    967985] qed.
    968986
    … …  
    978996  free_list m1 blocklist = m1' →
    979997  memory_inj E m1' m2'.
    980 (* nothing particular here, application of various lemmas and induction over blocklist. *) 
    981 @cthulhu
    982 qed.
     998#E #m1 #m2 #m1' #m2' #Hinj #blocklist #b2 #Hnot_mapped #Hfree2 #Hfree_list
     999cut (memory_inj E m1' m2)
     1000[ <Hfree_list -Hfree_list
     1001  -Hnot_mapped
     1002  lapply Hinj -Hinj
     1003  lapply m1 -m1
     1004  elim blocklist
     1005  [ #m1 #Hinj @Hinj
     1006  | #hd #tl #Hind #m1 #Hinj
     1007    @(free_memory_inj_m1 ? (free_list m1 tl) ? (free (free_list m1 tl) hd) ? hd)
     1008    try @refl @(Hind … Hinj)
     1009  ]
     1010]
     1011#Hinj'
     1012@(free_memory_inj_m2 … Hinj' … Hfree2)
     1013#b1 #delta #Hembed %2
     1014lapply (Hnot_mapped … Hembed)
     1015lapply Hfree_list -Hfree_list
     1016generalize in match m1';
     1017generalize in match m1;
     1018elim blocklist
     1019[ #m1 #m1' whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @False_ind
     1020| #hd #tl #Hind #m1 #m1' #Hfree_list *
     1021  [ #Heq destruct whd
     1022    whd in match (free_list ??);
     1023    >unfold_high_bound >unfold_low_bound
     1024    whd in match (update_block ?????); >eq_block_b_b
     1025    normalize nodelta @I
     1026  | >free_list_cons in Hfree_list; #Hfree_list #H
     1027    <Hfree_list whd cases m1 #contents2 #n2 #Hn2
     1028    >unfold_high_bound >unfold_low_bound
     1029    whd in match (update_block ?????);
     1030    @(eq_block_elim … b1 hd)
     1031    [ #Heq normalize nodelta @I
     1032    | #Hneq normalize nodelta @(Hind … (mk_mem contents2 n2 Hn2) … (refl ??) … H)
     1033    ]
     1034  ]
     1035] qed. 
    9831036
    9841037(* ---------------------------------------------------------- *)
    … …  
    12321285#E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore %
    12331286lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try //
    1234 cases Hinj #Hsim' #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl try assumption
     1287cases Hinj #Hsim' #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl try assumption
    12351288[
    12361289  #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid
    … …  
    14181471(* This lemma is not provable as in CompCert. In the following chunk of text, I'll try to
    14191472 * explain why, and how we might still be able to prove it given enough time.
    1420    I'll be refering to paper by Leroy & Blazy in the J.A.R.
     1473   I'll be refering to a paper by Leroy & Blazy in the J.A.R.
    14211474   In CompCert, when storing some data of size S in some location 〈block, offset〉,
    14221475   what happens is that
    … …  
    14281481   value fv, the story is the following :
    14291482   1) the value fv is marshalled into a list of back-end values (byte-sized) which correspond
    1430       to the actual size of the data in-memory. This list is then stored as-is at the
     1483      to the actual size of the data in-memory. 2) This list is then stored as-is at the
    14311484      location 〈block, offset〉.
    14321485     
    … …  
    15221575  load_sim_ptr E m1' m2.
    15231576#E #m1 #m2 #m1' #Hinj #ty #b #i #v #Hembed #Hstore
    1524 cases Hinj #Hsim #Hvalid #Hnodangling #Hregion_eq #Hnonalias #Himpl
     1577cases Hinj #Hsim #Hfreeblock #Hvalid #Hnodangling #Hregion_eq #Hnonalias #Himpl
    15251578cases ty in Hstore;
    15261579[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    … …  
    15621615  #Hload @(Hsim … Hembed' … Hload)
    15631616  @(load_by_value_success_valid_pointer … Hload) //
    1564 ] qed. 
     1617] qed.
    15651618
    15661619lemma store_value_of_type_memory_inj :
    … …  
    15741627%
    15751628[ 1: @(store_value_of_type_load_sim … Hinj … Hnot_mapped … Hstore)
    1576 | *: (* writing doesn't alter the bound, straightforward *) @cthulhu  ]
    1577 qed. (* TODO *)
     1629| *: lapply (mem_bounds_after_store_value_of_type … Hstore)
     1630     * #H1 #H2
     1631    [ #b * #Hnot_valid @(mi_freeblock ??? Hinj)
     1632      % #H @Hnot_valid whd in H:% ⊢ %; >H1 @H
     1633    | #p #p' #Hvalid @(mi_valid_pointers ??? Hinj)
     1634      @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)
     1635      >H1 cases (H2 (pblock p)) #HA #HB
     1636      >unfold_high_bound >unfold_low_bound
     1637      >unfold_high_bound >unfold_low_bound
     1638      >HA >HB //
     1639    | @(mi_nodangling … Hinj)
     1640    | @(mi_region … Hinj)
     1641    | whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq #Hembed1 #Hembed2
     1642      whd in match (block_is_empty ??);
     1643      whd in match (block_is_empty m1' b2);
     1644      >unfold_high_bound >unfold_low_bound
     1645      >unfold_high_bound >unfold_low_bound
     1646      cases (H2 b1) #HA #HB
     1647      cases (H2 b2) #HC #HD
     1648      >HA >HB >HC >HD
     1649      @(mi_nonalias ??? Hinj) assumption
     1650    | #bb whd
     1651      lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?);
     1652      cases (E bb) normalize nodelta try // * #bb' #off
     1653      normalize nodelta
     1654      whd in match (block_implementable_bv ??);     
     1655      whd in match (block_implementable_bv m2 bb');
     1656      whd in match (block_implementable_bv m1' bb);
     1657      >unfold_high_bound >unfold_low_bound
     1658      >unfold_high_bound >unfold_low_bound
     1659      >unfold_high_bound
     1660      cases (H2 bb) #HA #HB
     1661      >HA >HB //
     1662    ]
     1663] qed.   
    15781664
    15791665(* ------------------------------------------------------------------------- *)
    … …  
    22512337          cases (E bq1) [ 1: #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    22522338          * #BLOq #DELTAq normalize nodelta
    2253           cases (E bp1) [ 1: #_ #_ #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
     2339          cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]
    22542340          * #BLOp #DELTAp normalize nodelta #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct
    22552341          cases op
    … …  
    22602346          #H
    22612347          [ 2: #_ >(not_eq_block … H) normalize nodelta %{Vfalse} @conj try @refl %2
    2262           | 4: #_ >(not_eq_block … H) normalize nodelta >(not_eq_block … H) normalize nodelta %{Vtrue} @conj try @refl %2 ]         
     2348          | 4: #_ >(not_eq_block … H) normalize nodelta >(not_eq_block … H) normalize nodelta %{Vtrue} @conj try @refl %2 ]
    22632349          destruct (H) generalize in match BLOq in Hnowrap1 Hnowrap2 Hvalid2 Hvalid2' ⊢ %;
    22642350          #target_block * * #Himplq1 #Himpltarget #Hnowrap_q1
    … …  
    22682354          * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp
    22692355          >eq_block_b_b normalize nodelta
     2356          *
     2357          [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
     2358                 cases (valid_pointer_to_Prop … Hvalid') * #_ #Hle #Hlt
     2359                 lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt'
     2360                 lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl
     2361                 @(absurd … Hlt_refl (irreflexive_Zlt ?)) ]
     2362          *
     2363          [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
     2364                 cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt
     2365                 lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt'
     2366                 lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl
     2367                 @(absurd … Hlt_refl (irreflexive_Zlt ?)) ]
    22702368          *
    22712369          #Hdisjoint
Note: See TracChangeset for help on using the changeset viewer.