Changeset 2654 for src


Ignore:
Timestamp:
Feb 8, 2013, 8:54:32 PM (7 years ago)
Author:
garnier
Message:

Memory injections in a coherent state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2608 r2654  
    3535| #Hneq >(eqZb_false … (sym_neq ??? Hneq)) @refl ]
    3636qed.
     37
     38(* TODO: move in frontend_misc. This axiom states that for small bitvectors, bitvector addition
     39 * commutes with conversion to Z, i.e. there is no overflow. *)
     40axiom Z_addition_bv_commute :
     41  ∀n. ∀v1,v2:BitVector n.
     42        (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2) < Z_two_power_nat n →
     43        Z_of_unsigned_bitvector ? (addition_n ? v1 v2) =
     44        (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2).
     45
     46(* TODO: move in frontend_misc *)
     47lemma Zlt_to_Zneq : ∀x,y:Z. x < y → x ≠ y.
     48#x #y /3 by absurd, nmk/
     49qed.
     50
     51lemma Zlt_translate : ∀x,y,delta:Z. x < y → x + delta < y + delta.
     52#x #y #delta /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle/
     53qed.
     54
     55lemma Zlt_weaken : ∀x,y,delta:Z. delta ≥ 0 → x < y → x < y + delta.
     56#x #y #delta cases delta try // #p
     57[ 2: #Habsurd @(False_ind … Habsurd) ]
     58/3 by Zlt_to_Zle_to_Zlt, Zplus_le_pos/
     59qed.
     60
     61lemma Zlt_sum_weaken : ∀a,a',b,c:Z. a+b < c → a' < a → a'+b < c.
     62#a #a' #b #c /3 by transitive_Zlt, Zlt_translate/ qed.
     63
     64
     65(* TODO: move to Z.ma *)
     66lemma monotonic_Zlt_Zsucc : monotonic Z Zlt Zsucc.
     67#x #y cases x cases y /2/
     68[ #n /3 by Zle_to_Zlt_to_Zlt, monotonic_Zle_Zplus_r/ ]
     69#n #m @(pos_cases … n) @(pos_cases … m) //
     70[ #n /3 by I, Zle_to_Zlt, monotonic_Zle_Zplus_r/
     71| #m #n /3 by I, Zle_to_Zlt, monotonic_Zle_Zplus_r/
     72| /2 by Zlt_translate/
     73| /3 by Zle_to_Zlt, monotonic_Zle_Zplus_r/
     74| #n' /3 by Zle_to_Zlt_to_Zlt, lt_to_Zlt_neg_neg, Zlt_to_Zle/
     75| #n' #m' /3 by lt_plus_to_lt_r, lt_to_Zlt_neg_neg/ ]
     76qed.
     77
     78lemma monotonic_Zlt_Zpred : monotonic Z Zlt Zpred.
     79#x #y cases x cases y /2/
     80[ #n /3 by Zle_to_Zlt, monotonic_Zle_Zpred/
     81| #m #n @(pos_cases … n) @(pos_cases … m)
     82  [ /3 by monotonic_Zlt_Zsucc/
     83  | /3 by refl, true_to_andb_true, Zltb_true_to_Zlt/
     84  | #n' cases n' normalize
     85    [ #H inversion H [ #H' destruct | #m' #_ #_ #Habsurd  @(absurd … Habsurd (not_eq_one_succ m')) ]
     86    | #p /3 by le_to_lt_to_lt, le_S_contradiction_1/
     87    | #p /3 by le_to_lt_to_lt, le_S_contradiction_1/ ]
     88  | #m' #n' /3 by lt_plus_to_lt_r, lt_to_Zlt_pos_pos/ ]
     89| #m #n /3 by Zplus_le_pos, Zle_to_Zlt/
     90] qed. 
     91
     92lemma monotonic_Zlt_Zplus_l: ∀n.monotonic Z Zlt (λm.m + n).
     93#n cases n // #n' #a #b #H
     94[ @(pos_elim … n')
     95  [ >sym_Zplus >(sym_Zplus b) <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) @monotonic_Zlt_Zsucc @H
     96  | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //
     97      >(Zplus_Zsucc …) >(Zplus_Zsucc …) //
     98      cases a in H; cases b /2/
     99      #p #H /3 by Zlt_to_Zle_to_Zlt, monotonic_Zle_Zsucc, monotonic_Zlt_Zsucc/
     100  ]
     101| @(pos_elim … n')
     102  [ >sym_Zplus >(sym_Zplus b)  <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;
     103  | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //
     104    /3 by Zle_to_Zlt_to_Zlt, monotonic_Zlt_Zpred/
     105  ]
     106] qed.
     107
     108
     109lemma Zlt_to_Zle' : ∀x,y:Z. x < y → x ≤ y.
     110#x #y /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/
     111qed.
     112
     113       
    37114
    38115(* --------------------------------------------------------------------------- *)
     
    347424  (* Blocks in the codomain are valid *)
    348425  mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
    349   (* Regions are preserved - this might be superfluous now ?. *)
     426  (* Regions are preserved *)
    350427  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
    351428  (* sub-blocks do not overlap (non-aliasing property) *)
     
    540617    access_mode ty = By_value (typ_of_type ty) →
    541618    load_value_of_type ty m b off = Some ? v →
    542     valid_pointer m (mk_pointer b off).
     619    valid_pointer m (mk_pointer b off) = true.
    543620#ty #m #b #off #v #Haccess_mode #Hload normalize
    544621elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
    545 * #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @I
     622* #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @refl
    546623qed.
    547624
     
    573650(* Lemmas pertaining to memory allocation *)
    574651
     652(*
     653lemma alloc_valid_block_not_eq :
     654  ∀m,m',z1,z2,(*r,*)new_block.
     655  alloc m z1 z2 (*r*) = 〈m', new_block〉 →
     656  ∀b. valid_block m b → b ≠ new_block.
     657* #c #n #Hn #m' #z1 #z2 #new
     658whd in ⊢ ((??%?) → ?); #Heq destruct
     659#b whd in ⊢ (% → ?); cases b #bid
     660#Hlt % #Heq destruct (Heq)
     661@(absurd … Hlt (irreflexive_Zlt n))
     662qed. 
     663*)
    575664(* A valid block stays valid after an alloc. *)
    576665lemma alloc_valid_block_conservation :
     
    584673qed.
    585674
    586 (* A valid pointer stays valid after an alloc *)
    587 (*
    588 lemma alloc_valid_pointer_conservation :
    589   ∀m,m',z1,z2,r,new_block.
    590   alloc m z1 z2 r = 〈m', new_block〉 →
    591   ∀p. valid_pointer m p = true → valid_pointer m' p = true.
    592 #m #m' #z1 #z2 #r * #new_block #Hregion_eq #Halloc
    593 #p #Hvalid @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)
    594 -Hvalid lapply Halloc -Halloc cases m #cont #next #Hnext
    595 whd in ⊢ ((??%%) → ?);
    596 #Heq destruct (Heq) * * #Hblock_id
    597 >unfold_low_bound >unfold_high_bound
    598 >unfold_low_bound >unfold_high_bound
    599 whd in match (update_block ?????);
    600 whd in match (update_block ?????);
    601 #HA #HB % [ % [ /2 by Zlt_to_Zle_to_Zlt/ ] ]
    602 @(eq_block_elim … (pblock p) (mk_block r next))
    603 [ 1,3: cases p in Hblock_id; #b #o #H #Heq destruct
    604        @False_ind
    605        @(absurd … H (irreflexive_Zlt ?))
    606 | *: #Hneq normalize nodelta try assumption ]
    607 qed.*)
    608 
    609 
    610675lemma Zle_split :
    611676  ∀a,b:Z. a ≤ b → a ≠ b → a <  b.
     
    614679@not_eq_to_le_to_lt
    615680try // % #Heq destruct cases Hneq #H @H @refl
    616 qed. 
     681qed.
     682
     683(* A valid block /after/ an alloc was valid before if it is different
     684 * from the newly allocated one. *)
     685lemma alloc_valid_block_conservation2 :
     686  ∀m,m',z1,z2,new_block.
     687  alloc m z1 z2 =〈m',new_block〉 →
     688  ∀b. b ≠ new_block →
     689      valid_block m' b →
     690      valid_block m b.
     691#m #m' #z1 #z2 #new_block
     692cases m #cont #next #Hnext
     693whd in ⊢ ((??%%) → ?);
     694#Heq destruct (Heq) #b #Hneq #Hvalid
     695whd in Hvalid ⊢ %;
     696cases b in Hneq Hvalid; #bid * #H #Hlt
     697cut (bid ≠ next)
     698[ % #Heq destruct @H @refl ]
     699#Hneq
     700@(Zle_split … Hneq)
     701/3 by monotonic_Zle_Zpred, Zlt_to_Zle/
     702qed.
     703
     704lemma alloc_bounds_conservation :
     705  ∀m,m',z1,z2,new_block.
     706  alloc m z1 z2 =〈m',new_block〉 →
     707  ∀b. b ≠ new_block →
     708      low_bound m' b = low_bound m b ∧
     709      high_bound m' b = high_bound m b.
     710#m #m' #z1 #z2 #new #Halloc #b
     711#Hneq cases m in Halloc; #c #n #Hn
     712whd in ⊢ ((??%?) → ?); #Heq destruct
     713@conj
     714[ >unfold_low_bound whd in match (update_block ?????);
     715  >(neq_block_eq_block_false … Hneq) @refl
     716| >unfold_high_bound whd in match (update_block ?????);
     717  >(neq_block_eq_block_false … Hneq) @refl
     718] qed.
     719
     720(* A valid pointer stays valid after an alloc *)
    617721
    618722lemma alloc_valid_pointer_conservation :
     
    9001004] qed.
    9011005
     1006(* loading by-value from a freshly allocated block yields either an undef value or
     1007 * None. *)
     1008lemma load_by_value_after_alloc_undef :
     1009  ∀m,m',z1,z2,b.
     1010    alloc m z1 z2 = 〈m', b〉 →
     1011    ∀ty. access_mode ty = By_value (typ_of_type ty) →
     1012    ∀off. load_value_of_type ty m' b off = Some ? Vundef ∨
     1013          load_value_of_type ty m' b off = None ?.
     1014#m #m' #z1 #z2 (* * #br  #bid *) #b
     1015cases m #contents #nextblock #Hnext
     1016whd in ⊢ ((??%?) → ?);
     1017#Heq destruct (Heq)
     1018#ty cases ty   
     1019[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1020| #structname #fieldspec | #unionname #fieldspec | #id ]
     1021whd in ⊢ ((??%?) → ?);
     1022#Heq destruct (Heq)
     1023#off
     1024whd in match (load_value_of_type ????);
     1025(* We can't generalize over the typesize, sadly. We thus perform three identical inductions.
     1026 * Another solution would be to provide an ad-hoc lemma, but the goal is too ugly for that. *)
     1027[ lapply off -off
     1028  generalize in match (typesize ?); #tsz
     1029| lapply off -off
     1030  generalize in match (typesize ?); #tsz
     1031| lapply off -off
     1032  generalize in match (typesize ?); #tsz
     1033]
     1034elim tsz 
     1035[ 1,3,5: #off whd in match (loadn ???); normalize nodelta %1 @refl
     1036| *: #tsz' #Hind #off
     1037    whd in match (loadn ???);
     1038    whd in match (beloadv ??);
     1039    cases (Zltb ??) normalize nodelta try /1 by or_intror/
     1040    cases (Zleb ??) normalize nodelta try /1 by or_intror/
     1041    >andb_lsimpl_true
     1042    cases (Zltb ??); normalize nodelta try /1 by or_intror/
     1043    whd in match (update_block ?????);
     1044    >eq_block_b_b normalize nodelta
     1045    cases (Hind (shift_offset 2 off (bitvector_of_nat 2 1)))
     1046    cases (loadn ???) normalize nodelta try //
     1047    #bevals #Heq %1 whd in match (be_to_fe_value ??);
     1048    try @refl ]
     1049qed.
     1050
     1051
    9021052(* In CompCert, "∀v. value_eq Vundef v" holds. Not in our developments. In order
    9031053 * to prove the equivalent of lemma 68 of L&B, we need to provide an additional
     
    9311081qed.
    9321082
     1083
    9331084(* Embed a fresh block inside an unmapped portion of the target block.
    9341085 * This is the equivalent of lemma 68 of Leroy&Blazy.
    9351086 * Compared to L&B, an additional "undef_memory_zone" proof object must be provided.
     1087 * We also constrain the memory bounds of the new block to be bitvector-implementable,
     1088 * otherwise we can't prove that addition commutes with conversions between Z and
     1089 * bitvectors.
    9361090 *)
    9371091lemma alloc_memory_inj_m1_to_m2 :
     
    9421096  ∀delta:offset.
    9431097  valid_block m2 target →
     1098  block_implementable_bv m1' new_block →
     1099  block_implementable_bv m2 target →
     1100  block_region new_block = block_region target →
     1101  (high_bound m1' new_block) + (Zoo delta) < Z_two_power_nat 16 →
    9441102  alloc m1 z1 z2 = 〈m1', new_block〉 →
    9451103  low_bound m2 target ≤ z1 + Zoo delta →
     
    9521110  memory_inj E m1 m2 →
    9531111  memory_inj (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x) m1' m2.
    954 #E #m1 #m2 #m1' #z1 #z2 (* * #tr *) #tid (* * * #newr *) #newid (* * *) #delta
    955 #Hvalid #Halloc #Hlow #Hhigh #Hundef_zone #Hno_interference #Hinj
    956 cut (E newid = (None ?))
    957 [ @(mi_freeblock ??? Hinj newid) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj
     1112#E #m1 #m2 #m1' #z1 #z2 (* * #tr *) #target (* * * #newr *) #new_block (* * *) #delta
     1113#Hvalid #Himpl1 #Himpl2 #Hregion #Hno_overflow #Halloc #Hlow #Hhigh #Hundef_zone #Hno_interference #Hinj
     1114cut (E new_block = (None ?))
     1115[ @(mi_freeblock ??? Hinj new_block) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj
    9581116  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
    959 @cthulhu
    960 qed.
    961 (*
    9621117#Hnew_not_mapped
    963 cut (embedding_compatible E (λx. if eqZb newid x then Some ? 〈mk_block newr tid, delta〉 else E x))
    964 [ whd #b @(eqZb_elim … newid (block_id b)) normalize nodelta try // #Heq <Heq %1 assumption ]
     1118cut (embedding_compatible E (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x))
     1119[ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 assumption ]
    9651120#Hembedding_compatible
    9661121%
    9671122[ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid' #Hembed #Hload
    968   @(eqZb_elim … newid (block_id b1))
     1123  @(eq_block_elim … new_block b1)
    9691124  [ 2: (* we do not load from the newly allocated block *)
    9701125     #Hneq
    9711126     (* prove that we can equivalently load from the memory before alloc *)
    9721127     cases (some_inversion ????? Hembed) * #target' #delta'
    973      >(eqZb_false … Hneq) normalize nodelta
     1128     >(neq_block_eq_block_false … Hneq) normalize nodelta
    9741129     * #Hembed #Heq destruct (Heq)
    9751130     cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block' #Hlow #Hhigh
     
    9891144        * the newly allocated block (which by def. of alloc contains only BVundefs) *)
    9901145     #Heq destruct (Heq)
    991      whd in Hembed:(??%?); >eqZb_z_z in Hembed; normalize nodelta
     1146     whd in Hembed:(??%?); >eq_block_b_b in Hembed; normalize nodelta
    9921147     #Heq_ptr
    9931148     (* cull out all boring cases *)
     
    9971152     [ 1,6,7: whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
    9981153     | 4,5: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq_ptr Heq)
    999             %{(Vptr (mk_pointer (mk_block newr tid) (offset_plus off1 delta)))}
     1154            %{(Vptr (mk_pointer b2 (offset_plus off1 delta)))}
    10001155            @conj
    10011156            [ 1,3: @refl
    1002             | *: %4 whd in ⊢ (??%?); >eqZb_z_z @refl ] ]
     1157            | *: %4 whd in ⊢ (??%?); >eq_block_b_b @refl ] ]
    10031158     (* Now: load-by-value cases. Outcome is either None or Undef. *)
    1004      lapply (load_by_value_after_alloc_undef m1 m1' z1 z2 b1 ?)
    1005      [ 1,3,5:
     1159     lapply (load_by_value_after_alloc_undef m1 m1' z1 z2 b1 Halloc)
    10061160     #Hload_eq
    10071161     [ lapply (Hload_eq (Tint sz sg) (refl ??) off1)
     
    10101164     *
    10111165     (* None case: absurd *)
    1012      [ 2,4,6: >Hload #Habsurd destruct (Habsurd) ]
    1013          >Hload #Heq destruct (Heq) %{Vundef}
    1014          @conj try //
    1015          cut (valid_pointer m2 (mk_pointer b2 (offset_plus off1 delta))=true)
    1016          [ 1,3,5: @valid_pointer_of_Prop @conj try @conj
    1017             [ 1,4,7: assumption
    1018             | 2,5,8: >unfold_low_bound
    1019          lapply (alloc_properties … Halloc) * *
    1020          >unfold_low_bound >unfold_high_bound #Hlow #Hhigh #Hundef
    1021          lapply (valid_pointer_to_Prop … Hvalid') * *
    1022          #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow >Hhigh
    1023 *)
    1024 
    1025 (* Embed a fresh block inside an unmapped portion of the target block.
    1026  * This is the equivalent of lemma 68 for Leroy&Blazy. *)
    1027 (*
    1028 axiom alloc_memory_inj_m1_to_m2 :
    1029   ∀E:embedding.
    1030   ∀m1,m2,m1':mem.
    1031   ∀z1,z2:Z.
    1032   ∀b2,new_block.
    1033   ∀delta:offset.
    1034   valid_block m2 b2 →
    1035   alloc m1 z1 z2 (block_region b2) = 〈m1', new_block〉 →
    1036   low_bound m2 b2 ≤ z1 + Zoo delta →
    1037   z2 + Zoo delta ≤ high_bound m2 b2 →
    1038   (∀b,b',delta'. b ≠ (pi1 … new_block) →
    1039                  E (block_id b) = Some ? 〈b', delta'〉 →
    1040                  high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨
    1041                  z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) →                 
    1042   memory_inj E m1 m2 →
    1043   memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then Some ? 〈b2, delta〉 else E x) m1' m2.
    1044 *)
     1166     [ 2,4,6: #Hload >Hload #Habsurd destruct (Habsurd) ]
     1167     #Hload >Hload #Heq destruct (Heq) %{Vundef}
     1168     @conj try // destruct (Heq_ptr)
     1169     (* prove the validity of this pointer  in order tu unfold load *)
     1170     cut (valid_pointer m2 (mk_pointer b2 (offset_plus off1 delta))=true)
     1171     [ 1,3,5: @valid_pointer_of_Prop @conj try @conj
     1172        [ 1,4,7: assumption
     1173        | 2,5,8: >unfold_low_bound
     1174           lapply (alloc_properties … Halloc) * *
     1175           >unfold_low_bound >unfold_high_bound #Hlow' #Hhigh' #Hundef
     1176           lapply (valid_pointer_to_Prop … Hvalid') * *
     1177           #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow' >Hhigh'
     1178           #Hle_low #Hlt_high destruct
     1179           cut (Z_of_unsigned_bitvector ? (offv (offset_plus off1 delta)) = Zoo off1 + Zoo delta)
     1180           [ 1,3,5: >Z_addition_bv_commute try @refl
     1181                    @(transitive_Zlt ???? Hno_overflow) @monotonic_Zlt_Zplus_l
     1182                    @Hlt_high
     1183           ]
     1184           #Hsum_split
     1185           cut (low (blocks m1' b1) + Zoo delta ≤ Z_of_unsigned_bitvector offset_size (offv (offset_plus off1 delta)))
     1186           [ 1,3,5: >Hsum_split @monotonic_Zle_Zplus_l assumption ]
     1187           @(transitive_Zle … Hlow)
     1188       | 3,6,9: >unfold_high_bound
     1189           lapply (alloc_properties … Halloc) * *
     1190           >unfold_low_bound >unfold_high_bound #Hlow' #Hhigh' #Hundef
     1191           lapply (valid_pointer_to_Prop … Hvalid') * *
     1192           #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow' >Hhigh'
     1193           #Hle_low #Hlt_high destruct
     1194           cut (Z_of_unsigned_bitvector ? (offv (offset_plus off1 delta)) = Zoo off1 + Zoo delta)
     1195           [ 1,3,5: >Z_addition_bv_commute try @refl
     1196                    @(transitive_Zlt ???? Hno_overflow) @monotonic_Zlt_Zplus_l
     1197                    @Hlt_high
     1198           ]
     1199           #Hsum_split
     1200           cut (Z_of_unsigned_bitvector offset_size (offv (offset_plus off1 delta)) < high (blocks m1' b1) + Zoo delta)
     1201           [ 1,3,5: >Hsum_split @monotonic_Zlt_Zplus_l assumption ]
     1202           #Hlt_aux @(Zlt_to_Zle_to_Zlt … Hlt_aux Hhigh)
     1203       ]
     1204    ]
     1205    -Hno_interference
     1206    #Hvalid_ptr2
     1207    (* reformulate the goals in an induction friendly way *)       
     1208    [ cut (∃bvals. loadn m2
     1209                       (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta))))
     1210                       (typesize (typ_of_type (Tint sz sg))) = Some ? bvals ∧
     1211                   (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef)))
     1212      [ 2: * #bvals * #Hloadn * #Heq destruct (Heq)
     1213           whd in match (load_value_of_type ????);
     1214           >Hloadn normalize nodelta try @refl
     1215           cases bvals in Heq; try //
     1216           #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?);
     1217           #Heq destruct (Heq) try @refl ]
     1218    | cut (∃bvals. loadn m2
     1219                       (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta))))
     1220                       (typesize (typ_of_type (Tpointer ptr_ty))) = Some ? bvals ∧
     1221                   (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef)))
     1222      [ 2: * #bvals * #Hloadn * #Heq destruct (Heq)
     1223           whd in match (load_value_of_type ????);
     1224           >Hloadn normalize nodelta try @refl
     1225           cases bvals in Heq; try //
     1226           #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?);
     1227           #Heq destruct (Heq) try @refl ]
     1228    | cut (∃bvals. loadn m2
     1229                       (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta))))
     1230                       (typesize (typ_of_type (Tcomp_ptr id))) = Some ? bvals ∧
     1231                   (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef)))
     1232      [ 2: * #bvals * #Hloadn * #Heq destruct (Heq)
     1233           whd in match (load_value_of_type ????);
     1234           >Hloadn normalize nodelta try @refl
     1235           cases bvals in Heq; try //
     1236           #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?);
     1237           #Heq destruct (Heq) try @refl ]
     1238    ]
     1239    cases (valid_pointer_to_Prop … Hvalid') -Hvalid' * #HA #HB #HC
     1240    cases (valid_pointer_to_Prop … Hvalid_ptr2) -Hvalid_ptr2 * #HD
     1241    whd in match (offset_plus ??); #HE #HF
     1242    cases Himpl1 cases Himpl2 -Himpl1 -Himpl2
     1243    >unfold_low_bound >unfold_low_bound >unfold_high_bound >unfold_high_bound
     1244    * #HG #HH * #HI #HJ * #HK #HL * #HM #HN
     1245    lapply (alloc_properties … Halloc) * * #HO #HP #Hsrc_undef destruct (HO HP)
     1246    cases (some_inversion ????? Hload)
     1247    #bevals *
     1248    #Hloadn #_ lapply Hloadn -Hloadn
     1249    whd in match (typesize ?);
     1250    [ generalize in match (S (pred_size_intsize sz));
     1251    | generalize in match (S (S O));
     1252    | generalize in match (S (S O)); ]
     1253    #typesize
     1254    lapply HE lapply HF lapply HB lapply HC
     1255    -HE -HF -HB -HC
     1256    lapply bevals
     1257    lapply off1
     1258    elim typesize
     1259    [ 1,3,5:
     1260      #off #bevals #HC #HB #HF #HE #_ %{[ ]} @conj try @refl
     1261      %1 @refl
     1262    | *:
     1263      #n #Hind #off #bevals #HC #HB #HF #HE #Hloadn
     1264      cases (some_inversion ????? Hloadn) -Hloadn
     1265      #bval1 * #Hbeloadv_eq #Hloadn
     1266      cases (some_inversion ????? Hloadn) -Hloadn
     1267      whd in match (shift_pointer ???);
     1268      whd in match (shift_offset ???);
     1269      #bevals1 * #Hloadn #Hbevals'
     1270      whd in match (loadn ???);
     1271      whd in match (beloadv ??);
     1272      >(Zlt_to_Zltb_true … HD) normalize nodelta
     1273      >(Zle_to_Zleb_true … HE)
     1274      >(Zlt_to_Zltb_true … HF) normalize nodelta
     1275      lapply (Hundef_zone (Z_of_unsigned_bitvector ? (addition_n offset_size (offv off) (offv delta))) ??)
     1276      [ 1,4,7: >Z_addition_bv_commute
     1277          [ 2,4,6: @(transitive_Zlt … Hno_overflow)
     1278                   @(monotonic_Zlt_Zplus_l) assumption
     1279          | 1,3,5: @(monotonic_Zle_Zplus_l) /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ ]
     1280          | 2,5,8: >Z_addition_bv_commute
     1281             [ 2,4,6: @(transitive_Zlt … Hno_overflow)
     1282                      @(monotonic_Zlt_Zplus_l) assumption
     1283             | 1,3,5: @(monotonic_Zle_Zplus_l) /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ ]
     1284      ]
     1285      #Hcontents_undef
     1286      cases n in Hind Hloadn;
     1287      [ 1,3,5: #_ normalize in match (loadn ???); normalize nodelta #Heq destruct
     1288               >Hcontents_undef %{[BVundef]} @conj try @refl %2 @refl ]
     1289      #n' #Hind #Hloadn
     1290      lapply Hloadn #Hloadn'
     1291      cases (some_inversion ????? Hloadn') -Hloadn'
     1292      #bval * whd in match (beloadv ??);
     1293      >(Zlt_to_Zltb_true … HA) normalize nodelta #Hbeloadv
     1294      cases (if_opt_inversion ???? Hbeloadv) -Hbeloadv #Hbounds
     1295      cases (andb_inversion … Hbounds) -Hbounds #Hle1 #Hlt1 #Hcontents1 #_
     1296      lapply (Hind (mk_offset (addition_n ? (offv off) (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) bevals1 ????)
     1297      (* lapply (Hind (mk_offset (addition_n ? (offv off) (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) bevals1 ???? Hloadn) *)
     1298      [ 1,6,11:
     1299        @(transitive_Zle ??? HE)
     1300        <associative_addition_n
     1301        >(commutative_addition_n ? (sign_ext ???) (offv delta))
     1302        >associative_addition_n
     1303        >(Z_addition_bv_commute ?? (sign_ext ???))
     1304        [ 2,4,6: normalize in match (Z_of_unsigned_bitvector ? (sign_ext ???));
     1305                 >(sym_Zplus ? (pos one)) <Zsucc_Zplus_pos_O
     1306                 @(Zle_to_Zlt_to_Zlt … HJ) @Zlt_to_Zle @HF
     1307        | 1,3,5: normalize in match (Z_of_unsigned_bitvector ? (sign_ext ???));
     1308                 >(sym_Zplus ? (pos one)) <Zsucc_Zplus_pos_O @Zsucc_le
     1309        ]
     1310      | 2,7,12:
     1311        @(Zlt_to_Zle_to_Zlt ??? ? Hhigh)
     1312        >Z_addition_bv_commute
     1313        [ 2,4,6: @(transitive_Zlt … Hno_overflow)
     1314                 @(monotonic_Zlt_Zplus_l) @(Zltb_true_to_Zlt … Hlt1)
     1315        | 1,3,5: @monotonic_Zlt_Zplus_l @(Zltb_true_to_Zlt … Hlt1) ]
     1316      | 3,8,13:
     1317        @(Zleb_true_to_Zle … Hle1)
     1318      | 4,9,14:
     1319        @(Zltb_true_to_Zlt … Hlt1)
     1320      ]
     1321      -Hind #Hind lapply (Hind Hloadn)
     1322      * #bevals2 * #Hloadn2 #Hbe_to_fe
     1323      whd in match (shift_pointer ???);
     1324      whd in match (shift_offset ???);
     1325      cases Hbe_to_fe
     1326      [ 1,3,5: #Heq destruct (Heq)
     1327        %{(contents (blocks m2 b2)
     1328             (Z_of_unsigned_bitvector offset_size
     1329              (addition_n offset_size (offv off) (offv delta)))
     1330               ::[ ])}
     1331        <associative_addition_n
     1332        >(commutative_addition_n ? (offv delta))
     1333        >associative_addition_n
     1334        >Hloadn2 normalize nodelta @conj try @refl %2
     1335        >Hcontents_undef @refl
     1336      | *: #Hhd_empty
     1337        %{(contents (blocks m2 b2)
     1338             (Z_of_unsigned_bitvector offset_size
     1339              (addition_n offset_size (offv off) (offv delta)))
     1340               :: bevals2)}
     1341        <associative_addition_n
     1342        >(commutative_addition_n ? (offv delta))
     1343        >associative_addition_n
     1344        >Hloadn2 normalize nodelta @conj try @refl %2
     1345        >Hcontents_undef @refl
     1346      ]
     1347    ]
     1348  ]
     1349| #b lapply (alloc_valid_new_block … Halloc) @(eq_block_elim … new_block b)
     1350  [ #Heq destruct #Ha #Hb @False_ind @(absurd … Ha Hb)
     1351  | #Hneq #Hvalid_new #Hnot_valid normalize nodelta
     1352    cut (¬valid_block m1 b)
     1353    [ cases m1 in Halloc; #cont #next #Hnext
     1354      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     1355      % #H cases Hnot_valid #H' @H'
     1356      whd whd in H; /2 by transitive_Zlt/ ]
     1357    @ (mi_freeblock … Hinj) ]
     1358| * #blo #off #p' #Hvalid1
     1359  @(eq_block_elim … new_block blo)
     1360  [ #Heq whd in match (pointer_translation ??);
     1361    destruct (Heq) >eq_block_b_b normalize nodelta
     1362    lapply (alloc_properties … Halloc) * *
     1363    #Hlow_eq #Hhigh_eq #Hundef destruct
     1364    cases (valid_pointer_to_Prop … Hvalid1) *
     1365    #Hvalid_block1 #Hlow1 #Hhigh1
     1366    #Heq destruct (Heq) @valid_pointer_of_Prop
     1367    @conj try @conj   
     1368    [ @Hvalid
     1369    | @(transitive_Zle … Hlow)
     1370      >Z_addition_bv_commute
     1371      [ @monotonic_Zle_Zplus_l assumption
     1372      | @(transitive_Zlt … Hno_overflow)
     1373        @monotonic_Zlt_Zplus_l assumption
     1374      ]
     1375    | @(Zlt_to_Zle_to_Zlt … Hhigh)
     1376      >Z_addition_bv_commute
     1377      [ @monotonic_Zlt_Zplus_l assumption
     1378      | @(transitive_Zlt … Hno_overflow)
     1379        @monotonic_Zlt_Zplus_l assumption
     1380      ]
     1381    ]
     1382  | #Hblocks_neq whd in match (pointer_translation ??);
     1383    >(neq_block_eq_block_false … Hblocks_neq) normalize nodelta
     1384    #Htranslate
     1385    lapply (mi_valid_pointers ??? Hinj (mk_pointer blo off) p' ?)
     1386    [ @(alloc_valid_pointer_conservation … Halloc … Hvalid1) @sym_neq assumption ]
     1387    #H @H
     1388    assumption
     1389  ]
     1390| #b #b' #o'
     1391  @(eq_block_elim … new_block b)
     1392  [ #Heq destruct (Heq) normalize nodelta
     1393    #Heq destruct (Heq) @Hvalid
     1394  | #Hneq normalize nodelta
     1395    #Hembed
     1396    @(mi_nodangling ??? Hinj … Hembed)
     1397  ]
     1398| #b #b' #o'
     1399  @(eq_block_elim … new_block b)
     1400  [ #Heq normalize nodelta #Heq' destruct (Heq Heq')
     1401    @Hregion
     1402  | #Hneq normalize nodelta #Hembed
     1403    @(mi_region … Hinj … Hembed)
     1404  ]
     1405| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq
     1406  cases (alloc_properties … Halloc) * #Hlow1 #Hhigh1 #Hundef
     1407  @(eq_block_elim … new_block b1)
     1408  normalize nodelta
     1409  [ #Heq #Heq' destruct
     1410    >(neq_block_eq_block_false … Hneq) normalize nodelta
     1411    #Hembed
     1412(*    lapply (alloc_bounds_conservation … Halloc) …  *)
     1413    @(eq_block_elim … b1' b2') normalize nodelta
     1414    [ #Heq destruct (Heq)
     1415      lapply (Hno_interference b2 ? (sym_neq ??? Hneq) Hembed) *
     1416      cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq)) #HA #HB
     1417      [ #H %1 %1 %2
     1418        >HB @H
     1419      | #H %1 %1 %1 >HA @H ]
     1420    | #Hneq @I ]
     1421  | #Hneq' #Hembed
     1422    @(eq_block_elim … new_block b2) normalize nodelta
     1423    [ #Heq #Heq' destruct
     1424      @(eq_block_elim … b1' b2') normalize nodelta
     1425      [ #Heq destruct (Heq)
     1426        lapply (Hno_interference b1 ? Hneq Hembed) *
     1427        cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq')) #HA #HB
     1428        [ #H %1 %1 %1
     1429          >HB @H
     1430        | #H %1 %1 %2 >HA @H ]
     1431      | #Hneq @I ]
     1432    | #Hneq'' #Hembed'
     1433      @(eq_block_elim … b1' b2') normalize nodelta
     1434      [ #Heq'' destruct (Heq'')
     1435        lapply (mi_nonalias … Hinj … Hneq … Hembed Hembed')
     1436        >eq_block_b_b normalize nodelta
     1437        cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq''))
     1438        #HA #HB
     1439        cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq'))
     1440        #HC #HD
     1441        * [ * [ * | ] | ]
     1442        [ #Hle %1 %1 %1 >HD >HA @Hle
     1443        | #Hle %1 %1 %2 >HB >HC @Hle
     1444        | #Hempty %1 %2 whd in Hempty ⊢ %; >HD >HC
     1445          @Hempty
     1446        | #Hempty %2 whd in Hempty ⊢ %; >HB >HA @Hempty
     1447        ]
     1448      | #_ @I
     1449      ]
     1450    ]
     1451  ]
     1452| #b whd
     1453  @(eq_block_elim … new_block b)
     1454  normalize nodelta
     1455  #Hneq destruct (Hneq)
     1456  [ @conj try @conj try assumption
     1457  | lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?);
     1458    cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq))
     1459    #HA #HB
     1460    cases (E b) normalize nodelta try //
     1461    * #blo #off normalize nodelta * * #HA' #HB' #HC'
     1462    @conj try @conj whd in HA'; whd in HB';
     1463    whd in match (block_implementable_bv ??);
     1464    [ 1,2: >HA >HB assumption
     1465    | *: >HB assumption ]
     1466  ]
     1467] qed.   
    10451468
    10461469(* -------------------------------------- *)
     
    25312954  (Zoo y) + (Zoo delta) < Z_two_power_nat 16 →
    25322955  cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
    2533 
    2534 (* TODO: move in frontend_misc *)
    2535 lemma Zlt_to_Zneq : ∀x,y:Z. x < y → x ≠ y.
    2536 #x #y /3 by absurd, nmk/
    2537 qed.
    2538 
    2539 lemma Zlt_translate : ∀x,y,delta:Z. x < y → x + delta < y + delta.
    2540 #x #y #delta /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle/
    2541 qed.
    2542 
    2543 lemma Zlt_weaken : ∀x,y,delta:Z. delta ≥ 0 → x < y → x < y + delta.
    2544 #x #y #delta cases delta try // #p
    2545 [ 2: #Habsurd @(False_ind … Habsurd) ]
    2546 /3 by Zlt_to_Zle_to_Zlt, Zplus_le_pos/
    2547 qed.
    2548 
    2549 lemma Zlt_sum_weaken : ∀a,a',b,c:Z. a+b < c → a' < a → a'+b < c.
    2550 #a #a' #b #c /3 by transitive_Zlt, Zlt_translate/ qed.
    2551 
    2552 (* TODO: move in frontend_misc. This axiom states that for small bitvectors, bitvector addition
    2553  * commutes with conversion to Z, i.e. there is no overflow. *)
    2554 axiom Z_addition_bv_commute :
    2555   ∀n. ∀v1,v2:BitVector n.
    2556         (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2) < Z_two_power_nat n →
    2557         Z_of_unsigned_bitvector ? (addition_n ? v1 v2) =
    2558         (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2).
    25592956
    25602957lemma valid_pointer_of_implementable_block_is_implementable :
Note: See TracChangeset for help on using the changeset viewer.