Changeset 2654
 Timestamp:
 Feb 8, 2013, 8:54:32 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/memoryInjections.ma
r2608 r2654 35 35  #Hneq >(eqZb_false … (sym_neq ??? Hneq)) @refl ] 36 36 qed. 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. *) 40 axiom 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 *) 47 lemma Zlt_to_Zneq : ∀x,y:Z. x < y → x ≠ y. 48 #x #y /3 by absurd, nmk/ 49 qed. 50 51 lemma 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/ 53 qed. 54 55 lemma 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/ 59 qed. 60 61 lemma 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 *) 66 lemma 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/ ] 76 qed. 77 78 lemma 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 92 lemma 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 109 lemma Zlt_to_Zle' : ∀x,y:Z. x < y → x ≤ y. 110 #x #y /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ 111 qed. 112 113 37 114 38 115 (*  *) … … 347 424 (* Blocks in the codomain are valid *) 348 425 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 *) 350 427 mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b'; 351 428 (* subblocks do not overlap (nonaliasing property) *) … … 540 617 access_mode ty = By_value (typ_of_type ty) → 541 618 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. 543 620 #ty #m #b #off #v #Haccess_mode #Hload normalize 544 621 elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) 545 * #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @ I622 * #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @refl 546 623 qed. 547 624 … … 573 650 (* Lemmas pertaining to memory allocation *) 574 651 652 (* 653 lemma 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 658 whd in ⊢ ((??%?) → ?); #Heq destruct 659 #b whd in ⊢ (% → ?); cases b #bid 660 #Hlt % #Heq destruct (Heq) 661 @(absurd … Hlt (irreflexive_Zlt n)) 662 qed. 663 *) 575 664 (* A valid block stays valid after an alloc. *) 576 665 lemma alloc_valid_block_conservation : … … 584 673 qed. 585 674 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 #Halloc593 #p #Hvalid @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)594 Hvalid lapply Halloc Halloc cases m #cont #next #Hnext595 whd in ⊢ ((??%%) → ?);596 #Heq destruct (Heq) * * #Hblock_id597 >unfold_low_bound >unfold_high_bound598 >unfold_low_bound >unfold_high_bound599 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 destruct604 @False_ind605 @(absurd … H (irreflexive_Zlt ?))606  *: #Hneq normalize nodelta try assumption ]607 qed.*)608 609 610 675 lemma Zle_split : 611 676 ∀a,b:Z. a ≤ b → a ≠ b → a < b. … … 614 679 @not_eq_to_le_to_lt 615 680 try // % #Heq destruct cases Hneq #H @H @refl 616 qed. 681 qed. 682 683 (* A valid block /after/ an alloc was valid before if it is different 684 * from the newly allocated one. *) 685 lemma 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 692 cases m #cont #next #Hnext 693 whd in ⊢ ((??%%) → ?); 694 #Heq destruct (Heq) #b #Hneq #Hvalid 695 whd in Hvalid ⊢ %; 696 cases b in Hneq Hvalid; #bid * #H #Hlt 697 cut (bid ≠ next) 698 [ % #Heq destruct @H @refl ] 699 #Hneq 700 @(Zle_split … Hneq) 701 /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ 702 qed. 703 704 lemma 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 712 whd 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 *) 617 721 618 722 lemma alloc_valid_pointer_conservation : … … 900 1004 ] qed. 901 1005 1006 (* loading byvalue from a freshly allocated block yields either an undef value or 1007 * None. *) 1008 lemma 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 1015 cases m #contents #nextblock #Hnext 1016 whd 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 ] 1021 whd in ⊢ ((??%?) → ?); 1022 #Heq destruct (Heq) 1023 #off 1024 whd 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 adhoc 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 ] 1034 elim 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 ] 1049 qed. 1050 1051 902 1052 (* In CompCert, "∀v. value_eq Vundef v" holds. Not in our developments. In order 903 1053 * to prove the equivalent of lemma 68 of L&B, we need to provide an additional … … 931 1081 qed. 932 1082 1083 933 1084 (* Embed a fresh block inside an unmapped portion of the target block. 934 1085 * This is the equivalent of lemma 68 of Leroy&Blazy. 935 1086 * 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 bitvectorimplementable, 1088 * otherwise we can't prove that addition commutes with conversions between Z and 1089 * bitvectors. 936 1090 *) 937 1091 lemma alloc_memory_inj_m1_to_m2 : … … 942 1096 ∀delta:offset. 943 1097 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 → 944 1102 alloc m1 z1 z2 = 〈m1', new_block〉 → 945 1103 low_bound m2 target ≤ z1 + Zoo delta → … … 952 1110 memory_inj E m1 m2 → 953 1111 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 *) #t id (* * * #newr *) #newid(* * *) #delta955 #Hvalid #H alloc #Hlow #Hhigh #Hundef_zone #Hno_interference #Hinj956 cut (E new id= (None ?))957 [ @(mi_freeblock ??? Hinj new id) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj1112 #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 1114 cut (E new_block = (None ?)) 1115 [ @(mi_freeblock ??? Hinj new_block) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj 958 1116 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ] 959 @cthulhu960 qed.961 (*962 1117 #Hnew_not_mapped 963 cut (embedding_compatible E (λx. if eq Zb newid x then Some ? 〈mk_block newr tid, delta〉 else E x))964 [ whd #b @(eq Zb_elim … newid (block_id b)) normalize nodelta try // #Heq <Heq %1 assumption ]1118 cut (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 ] 965 1120 #Hembedding_compatible 966 1121 % 967 1122 [ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid' #Hembed #Hload 968 @(eq Zb_elim … newid (block_id b1))1123 @(eq_block_elim … new_block b1) 969 1124 [ 2: (* we do not load from the newly allocated block *) 970 1125 #Hneq 971 1126 (* prove that we can equivalently load from the memory before alloc *) 972 1127 cases (some_inversion ????? Hembed) * #target' #delta' 973 >( eqZb_false … Hneq) normalize nodelta1128 >(neq_block_eq_block_false … Hneq) normalize nodelta 974 1129 * #Hembed #Heq destruct (Heq) 975 1130 cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block' #Hlow #Hhigh … … 989 1144 * the newly allocated block (which by def. of alloc contains only BVundefs) *) 990 1145 #Heq destruct (Heq) 991 whd in Hembed:(??%?); >eq Zb_z_zin Hembed; normalize nodelta1146 whd in Hembed:(??%?); >eq_block_b_b in Hembed; normalize nodelta 992 1147 #Heq_ptr 993 1148 (* cull out all boring cases *) … … 997 1152 [ 1,6,7: whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd) 998 1153  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)))} 1000 1155 @conj 1001 1156 [ 1,3: @refl 1002  *: %4 whd in ⊢ (??%?); >eq Zb_z_z@refl ] ]1157  *: %4 whd in ⊢ (??%?); >eq_block_b_b @refl ] ] 1003 1158 (* Now: loadbyvalue 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) 1006 1160 #Hload_eq 1007 1161 [ lapply (Hload_eq (Tint sz sg) (refl ??) off1) … … 1010 1164 * 1011 1165 (* 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. 1045 1468 1046 1469 (*  *) … … 2531 2954 (Zoo y) + (Zoo delta) < Z_two_power_nat 16 → 2532 2955 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 // #p2545 [ 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 addition2553 * 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).2559 2956 2560 2957 lemma valid_pointer_of_implementable_block_is_implementable :
Note: See TracChangeset
for help on using the changeset viewer.