| 1 | (* This file is dedicated to general properties of memory w.r.t. writing and reading to it. |
|---|
| 2 | It also contains facts about related functions and predicates, such as valid_pointer. *) |
|---|
| 3 | |
|---|
| 4 | include "Clight/frontend_misc.ma". |
|---|
| 5 | include "common/FrontEndMem.ma". |
|---|
| 6 | |
|---|
| 7 | (* for store_value_of_type' *) |
|---|
| 8 | include "Clight/Cexec.ma". |
|---|
| 9 | |
|---|
| 10 | |
|---|
| 11 | (* --------------------------------------------------------------------------- *) |
|---|
| 12 | (* Stuff on [valid_pointer m p]. *) |
|---|
| 13 | (* --------------------------------------------------------------------------- *) |
|---|
| 14 | |
|---|
| 15 | (* [do_if_in_bounds] is used to check consistency when reading and storing stuff. *) |
|---|
| 16 | definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res. |
|---|
| 17 | |
|---|
| 18 | lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p. |
|---|
| 19 | #m #p @conj |
|---|
| 20 | [ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??); |
|---|
| 21 | whd in match (do_if_in_bounds); normalize nodelta |
|---|
| 22 | cases (Zltb (block_id (pblock p)) (nextblock m)) |
|---|
| 23 | [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] |
|---|
| 24 | >andb_lsimpl_true normalize nodelta |
|---|
| 25 | cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) |
|---|
| 26 | [ 2: normalize nodelta #Habsurd destruct (Habsurd) ] |
|---|
| 27 | >andb_lsimpl_true normalize nodelta |
|---|
| 28 | #Hlt >Hlt normalize nodelta #A #f /2 by ex_intro/ |
|---|
| 29 | | 2: whd in match (valid_pointer ??); |
|---|
| 30 | whd in match (in_bounds_pointer ??); #H |
|---|
| 31 | lapply (H bool (λblock,contents,off. true)) |
|---|
| 32 | * #foo whd in match (do_if_in_bounds ????); |
|---|
| 33 | cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta |
|---|
| 34 | [ 2: #Habsurd destruct (Habsurd) ] |
|---|
| 35 | >andb_lsimpl_true |
|---|
| 36 | cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) |
|---|
| 37 | normalize nodelta |
|---|
| 38 | [ 2: #Habsurd destruct (Habsurd) ] |
|---|
| 39 | >andb_lsimpl_true |
|---|
| 40 | elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p)))) |
|---|
| 41 | [ 1: #H >H // |
|---|
| 42 | | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ] |
|---|
| 43 | ] qed. |
|---|
| 44 | |
|---|
| 45 | lemma valid_pointer_to_Prop : |
|---|
| 46 | ∀m,p. valid_pointer m p = true → |
|---|
| 47 | (block_id (pblock p)) < (nextblock m) ∧ |
|---|
| 48 | (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧ |
|---|
| 49 | (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)). |
|---|
| 50 | #m #p whd in match (valid_pointer ??); |
|---|
| 51 | #H |
|---|
| 52 | lapply (Zleb_true_to_Zle (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) |
|---|
| 53 | lapply (Zltb_true_to_Zlt (block_id (pblock p)) (nextblock m)) |
|---|
| 54 | cases (Zltb (block_id (pblock p)) (nextblock m)) in H; |
|---|
| 55 | [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true |
|---|
| 56 | cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) |
|---|
| 57 | normalize nodelta |
|---|
| 58 | [ 2: #Habsurd destruct ] |
|---|
| 59 | #Hlt1 #Hlt2 #Hle @conj try @conj |
|---|
| 60 | try @(Hlt2 (refl ??)) try @(Hle (refl ??)) @(Zltb_true_to_Zlt … Hlt1) |
|---|
| 61 | qed. |
|---|
| 62 | |
|---|
| 63 | lemma valid_pointer_of_Prop : |
|---|
| 64 | ∀m,p. (block_id (pblock p)) < (nextblock m) ∧ |
|---|
| 65 | (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧ |
|---|
| 66 | (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)) → |
|---|
| 67 | valid_pointer m p = true. |
|---|
| 68 | #m #p * * #Hnextblock #Hlowbound #Hhighbound whd in match (valid_pointer ??); |
|---|
| 69 | >(Zle_to_Zleb_true … Hlowbound) |
|---|
| 70 | >(Zlt_to_Zltb_true … Hhighbound) |
|---|
| 71 | >(Zlt_to_Zltb_true … Hnextblock) @refl |
|---|
| 72 | qed. |
|---|
| 73 | |
|---|
| 74 | (* --------------------------------------------------------------------------- *) |
|---|
| 75 | (* "Observational" memory equivalence. Memories use closures to represent contents, |
|---|
| 76 | so we have to use that short of asserting functional extensionality to reason |
|---|
| 77 | on reordering of operations on memories, among others. For our |
|---|
| 78 | limited purposes, we do not need (at this time of writing, i.e. 22 sept. 2012) |
|---|
| 79 | to push the observation in the content_map. *) |
|---|
| 80 | (* --------------------------------------------------------------------------- *) |
|---|
| 81 | definition memory_eq ≝ λm1,m2. |
|---|
| 82 | nextblock m1 = nextblock m2 ∧ |
|---|
| 83 | ∀b. blocks m1 b = blocks m2 b. |
|---|
| 84 | |
|---|
| 85 | (* memory_eq is an equivalence relation. *) |
|---|
| 86 | lemma reflexive_memory_eq : reflexive ? memory_eq. |
|---|
| 87 | whd * #contents #nextblock #Hpos normalize @conj try // |
|---|
| 88 | qed. |
|---|
| 89 | |
|---|
| 90 | lemma symmetric_memory_eq : symmetric ? memory_eq. |
|---|
| 91 | whd * #contents #nextblock #Hpos * #contents' #nextblock' #Hpos' |
|---|
| 92 | normalize * #H1 #H2 @conj >H1 try // |
|---|
| 93 | qed. |
|---|
| 94 | |
|---|
| 95 | lemma transitive_memory_eq : transitive ? memory_eq. |
|---|
| 96 | whd |
|---|
| 97 | * #contents #nextblock #Hpos |
|---|
| 98 | * #contents1 #nextblock1 #Hpos1 |
|---|
| 99 | * #contents2 #nextblock2 #Hpos2 |
|---|
| 100 | normalize * #H1 #H2 * #H3 #H4 @conj // |
|---|
| 101 | qed. |
|---|
| 102 | |
|---|
| 103 | (* --------------------------------------------------------------------------- *) |
|---|
| 104 | (* Some definitions and results useful for simulation proofs. *) |
|---|
| 105 | (* --------------------------------------------------------------------------- *) |
|---|
| 106 | |
|---|
| 107 | (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the back-end values are equal. |
|---|
| 108 | * This is allright for switch removal but false for Clight to Cminor *) |
|---|
| 109 | definition load_sim ≝ |
|---|
| 110 | λ(m1 : mem).λ(m2 : mem). |
|---|
| 111 | ∀ptr,bev. |
|---|
| 112 | beloadv m1 ptr = Some ? bev → |
|---|
| 113 | beloadv m2 ptr = Some ? bev. |
|---|
| 114 | |
|---|
| 115 | (* --------------------------------------------------------------------------- *) |
|---|
| 116 | (* Lift beloadv simulation to the front-end. *) |
|---|
| 117 | |
|---|
| 118 | (* Lift load_sim to loadn. *) |
|---|
| 119 | lemma load_sim_loadn : |
|---|
| 120 | ∀m1,m2. load_sim m1 m2 → |
|---|
| 121 | ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res. |
|---|
| 122 | #m1 #m2 #Hload_sim #sz |
|---|
| 123 | elim sz |
|---|
| 124 | [ 1: #p #res #H @H |
|---|
| 125 | | 2: #n' #Hind #p #res |
|---|
| 126 | whd in match (loadn ???); |
|---|
| 127 | whd in match (loadn m2 ??); |
|---|
| 128 | lapply (Hload_sim p) |
|---|
| 129 | cases (beloadv m1 p) normalize nodelta |
|---|
| 130 | [ 1: #_ #Habsurd destruct (Habsurd) ] |
|---|
| 131 | #bval #H >(H ? (refl ??)) normalize nodelta |
|---|
| 132 | lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1))) |
|---|
| 133 | cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n') |
|---|
| 134 | normalize nodelta |
|---|
| 135 | [ 1: #_ #Habsurd destruct (Habsurd) ] |
|---|
| 136 | #res' #H >(H ? (refl ??)) normalize |
|---|
| 137 | #H @H |
|---|
| 138 | ] qed. |
|---|
| 139 | |
|---|
| 140 | (* Lift load_sim to front-end values. *) |
|---|
| 141 | lemma load_sim_fe : |
|---|
| 142 | ∀m1,m2. load_sim m1 m2 → |
|---|
| 143 | ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v → |
|---|
| 144 | load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v. |
|---|
| 145 | #m1 #m2 #Hloadsim #ptr #ty #v |
|---|
| 146 | cases ty |
|---|
| 147 | [ 1: | 2: #sz #sg | 3: #ptrty | 4: #arrayty #arraysz | 5: #argsty #retty |
|---|
| 148 | | 6: #sid #fields | 7: #uid #fields | 8: #cptr_id ] |
|---|
| 149 | whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?)); |
|---|
| 150 | [ 1,6,7: #Habsurd destruct (Habsurd) |
|---|
| 151 | | 4,5: #H @H |
|---|
| 152 | | 2,3,8: |
|---|
| 153 | generalize in match (mk_pointer (pblock ptr) (poff ptr)); |
|---|
| 154 | elim (typesize ?) |
|---|
| 155 | [ 1,3,5: #p #H @H |
|---|
| 156 | | *: #n' #Hind #p |
|---|
| 157 | lapply (load_sim_loadn … Hloadsim (S n') p) |
|---|
| 158 | cases (loadn m1 p (S n')) normalize nodelta |
|---|
| 159 | [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ] |
|---|
| 160 | #bv #H >(H ? (refl ??)) #H @H |
|---|
| 161 | ] |
|---|
| 162 | ] qed. |
|---|
| 163 | |
|---|
| 164 | (* --------------------------------------------------------------------------- *) |
|---|
| 165 | (* Lemmas relating reading and writing operation to memory properties. *) |
|---|
| 166 | |
|---|
| 167 | (* Successful beloadv implies valid_pointer. The converse is *NOT* true. *) |
|---|
| 168 | lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true. |
|---|
| 169 | * #contents #next #nextpos #ptr #res |
|---|
| 170 | whd in match (beloadv ??); |
|---|
| 171 | whd in match (valid_pointer ??); |
|---|
| 172 | cases (Zltb (block_id (pblock ptr)) next) |
|---|
| 173 | normalize nodelta |
|---|
| 174 | [ 2: #Habsurd destruct (Habsurd) ] |
|---|
| 175 | >andb_lsimpl_true |
|---|
| 176 | whd in match (low_bound ??); |
|---|
| 177 | whd in match (high_bound ??); |
|---|
| 178 | cases (Zleb (low (contents (pblock ptr))) |
|---|
| 179 | (Z_of_unsigned_bitvector offset_size (offv (poff ptr)))) |
|---|
| 180 | [ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ] |
|---|
| 181 | >andb_lsimpl_true |
|---|
| 182 | normalize nodelta #H |
|---|
| 183 | cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H; |
|---|
| 184 | try // normalize #Habsurd destruct (Habsurd) |
|---|
| 185 | qed. |
|---|
| 186 | |
|---|
| 187 | lemma bestorev_to_valid_pointer : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer m ptr = true. |
|---|
| 188 | * #contents #next #nextpos #ptr #v #res |
|---|
| 189 | whd in match (bestorev ???); |
|---|
| 190 | whd in match (valid_pointer ??); |
|---|
| 191 | cases (Zltb (block_id (pblock ptr)) next) |
|---|
| 192 | normalize nodelta |
|---|
| 193 | [ 2: #Habsurd destruct (Habsurd) ] |
|---|
| 194 | >andb_lsimpl_true |
|---|
| 195 | whd in match (low_bound ??); |
|---|
| 196 | whd in match (high_bound ??); |
|---|
| 197 | cases (Zleb (low (contents (pblock ptr))) |
|---|
| 198 | (Z_of_unsigned_bitvector offset_size (offv (poff ptr)))) |
|---|
| 199 | [ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ] |
|---|
| 200 | >andb_lsimpl_true |
|---|
| 201 | cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) |
|---|
| 202 | normalize nodelta try // #Habsurd destruct (Habsurd) |
|---|
| 203 | qed. |
|---|
| 204 | |
|---|
| 205 | lemma bestorev_to_valid_pointer_after : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer res ptr = true. |
|---|
| 206 | * #contents #next #nextpos #ptr #v #res |
|---|
| 207 | whd in match (bestorev ???); |
|---|
| 208 | whd in match (valid_pointer ??); #Hvalid |
|---|
| 209 | cases (if_opt_inversion ???? Hvalid) #Hnextblock normalize nodelta -Hvalid #Hvalid |
|---|
| 210 | cases (if_opt_inversion ???? Hvalid) #Hin_bounds #Heq destruct (Heq) normalize |
|---|
| 211 | >Hnextblock normalize nodelta cases (block_region (pblock ptr)) normalize nodelta |
|---|
| 212 | >eqZb_z_z normalize nodelta @Hin_bounds |
|---|
| 213 | qed. |
|---|
| 214 | |
|---|
| 215 | (* valid pointer implies successful bestorev *) |
|---|
| 216 | lemma valid_pointer_to_bestorev_ok : ∀m,ptr,v. valid_pointer m ptr = true → ∃m'. bestorev m ptr v = Some ? m'. |
|---|
| 217 | #m * #b #o #v #Hvalid cases (valid_pointer_to_Prop … Hvalid) * |
|---|
| 218 | #Hnext #Hlow #Hhigh normalize |
|---|
| 219 | >(Zlt_to_Zltb_true … Hnext) normalize nodelta |
|---|
| 220 | >(Zle_to_Zleb_true … Hlow) normalize nodelta |
|---|
| 221 | >(Zlt_to_Zltb_true … Hhigh) normalize nodelta |
|---|
| 222 | /2 by ex_intro/ |
|---|
| 223 | qed. |
|---|
| 224 | |
|---|
| 225 | (* --------------------------------------------------------------------------- *) |
|---|
| 226 | (* Some facts on [free] *) |
|---|
| 227 | |
|---|
| 228 | lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1). |
|---|
| 229 | * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize |
|---|
| 230 | @(eqZb_elim … bid1 bid2) |
|---|
| 231 | [ 1: #Heq >Heq cases br1 cases br2 normalize |
|---|
| 232 | [ 1,4: * #H @(False_ind … (H (refl ??))) ] |
|---|
| 233 | #_ @refl |
|---|
| 234 | | 2: cases br1 cases br2 normalize #_ #_ @refl ] |
|---|
| 235 | qed. |
|---|
| 236 | |
|---|
| 237 | lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1). |
|---|
| 238 | * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize |
|---|
| 239 | @(eqZb_elim … bid1 bid2) |
|---|
| 240 | [ 1: #Heq >Heq cases br1 cases br2 normalize |
|---|
| 241 | [ 1,4: * #H @(False_ind … (H (refl ??))) ] |
|---|
| 242 | #_ @refl |
|---|
| 243 | | 2: cases br1 cases br2 normalize #_ #_ @refl ] |
|---|
| 244 | qed. |
|---|
| 245 | |
|---|
| 246 | lemma beloadv_free_blocks_neq : |
|---|
| 247 | ∀m,block,pblock,poff,res. |
|---|
| 248 | beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block. |
|---|
| 249 | * #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res |
|---|
| 250 | normalize |
|---|
| 251 | cases (Zltb pbid next) normalize nodelta |
|---|
| 252 | [ 2: #Habsurd destruct (Habsurd) ] |
|---|
| 253 | cases pbr cases br normalize nodelta |
|---|
| 254 | [ 2,3: #_ % #Habsurd destruct (Habsurd) ] |
|---|
| 255 | @(eqZb_elim pbid bid) normalize nodelta |
|---|
| 256 | #Heq destruct (Heq) |
|---|
| 257 | [ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ] |
|---|
| 258 | #_ % #H destruct (H) elim Heq #H @H @refl |
|---|
| 259 | qed. |
|---|
| 260 | |
|---|
| 261 | lemma beloadv_free_beloadv : |
|---|
| 262 | ∀m,block,ptr,res. |
|---|
| 263 | beloadv (free m block) ptr = Some ? res → |
|---|
| 264 | beloadv m ptr = Some ? res. |
|---|
| 265 | * #contents #next #nextpos #block * #pblock #poff #res |
|---|
| 266 | #H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq |
|---|
| 267 | lapply H |
|---|
| 268 | whd in match (beloadv ??); |
|---|
| 269 | whd in match (beloadv ??) in ⊢ (? → %); |
|---|
| 270 | whd in match (nextblock (free ??)); |
|---|
| 271 | cases (Zltb (block_id pblock) next) |
|---|
| 272 | [ 2: normalize #Habsurd destruct (Habsurd) ] |
|---|
| 273 | normalize nodelta |
|---|
| 274 | <(low_free_eq … Hblocks_neq) |
|---|
| 275 | <(high_free_eq … Hblocks_neq) |
|---|
| 276 | whd in match (free ??); |
|---|
| 277 | whd in match (update_block ?????); |
|---|
| 278 | @(eq_block_elim … pblock block) |
|---|
| 279 | [ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ] |
|---|
| 280 | #_ normalize nodelta |
|---|
| 281 | #H @H |
|---|
| 282 | qed. |
|---|
| 283 | |
|---|
| 284 | lemma loadn_free_loadn : |
|---|
| 285 | ∀n,m,block,ptr,res. |
|---|
| 286 | loadn (free m block) ptr n = Some ? res → |
|---|
| 287 | loadn m ptr n = Some ? res. |
|---|
| 288 | #n elim n |
|---|
| 289 | [ 1: normalize // |
|---|
| 290 | | 2: #n' #Hind #m #block #ptr #res #Hloadn |
|---|
| 291 | whd in Hloadn:(??%?); |
|---|
| 292 | cases (some_inversion ????? Hloadn) -Hloadn |
|---|
| 293 | #be * #Hbeloadv #Hloadn |
|---|
| 294 | cases (some_inversion ????? Hloadn) -Hloadn |
|---|
| 295 | #res' * #Hloadn #Heq destruct (Heq) |
|---|
| 296 | whd in match (loadn ???); |
|---|
| 297 | >(beloadv_free_beloadv … Hbeloadv) normalize nodelta |
|---|
| 298 | >(Hind … Hloadn) normalize nodelta @refl |
|---|
| 299 | ] qed. |
|---|
| 300 | |
|---|
| 301 | lemma load_value_of_type_free_load_value_of_type : |
|---|
| 302 | ∀ty,m,block,b,o,res. |
|---|
| 303 | load_value_of_type ty (free m block) b o = Some ? res → |
|---|
| 304 | load_value_of_type ty m b o = Some ? res. |
|---|
| 305 | #ty |
|---|
| 306 | cases ty |
|---|
| 307 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
|---|
| 308 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
|---|
| 309 | #m #block #b #o #res |
|---|
| 310 | whd in ⊢ ((??%?) → (??%?)); // #H |
|---|
| 311 | cases (some_inversion ????? H) #be * #Hloadn #Heq |
|---|
| 312 | >(loadn_free_loadn … Hloadn) |
|---|
| 313 | normalize nodelta assumption |
|---|
| 314 | qed. |
|---|
| 315 | |
|---|
| 316 | lemma beloadv_free_beloadv2 : |
|---|
| 317 | ∀m,block,ptr,res. |
|---|
| 318 | pblock ptr ≠ block → |
|---|
| 319 | beloadv m ptr = Some ? res → |
|---|
| 320 | beloadv (free m block) ptr = Some ? res. |
|---|
| 321 | * #contents #next #nextpos #block * #pblock #poff #res #Hneq |
|---|
| 322 | whd in match (beloadv ??); |
|---|
| 323 | whd in match (beloadv ??) in ⊢ (? → %); |
|---|
| 324 | whd in match (nextblock (free ??)); |
|---|
| 325 | cases (Zltb (block_id pblock) next) |
|---|
| 326 | [ 2: normalize #Habsurd destruct (Habsurd) ] |
|---|
| 327 | normalize nodelta |
|---|
| 328 | <(low_free_eq … Hneq) |
|---|
| 329 | <(high_free_eq … Hneq) |
|---|
| 330 | whd in match (free ??); |
|---|
| 331 | whd in match (update_block ?????); |
|---|
| 332 | @(eq_block_elim … pblock block) |
|---|
| 333 | [ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ] |
|---|
| 334 | #_ normalize nodelta |
|---|
| 335 | #H @H |
|---|
| 336 | qed. |
|---|
| 337 | |
|---|
| 338 | (* If a pointer is still valid after a free (meaning we freed another block), then it was valid before. *) |
|---|
| 339 | lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p. |
|---|
| 340 | #m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %); |
|---|
| 341 | #H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %); |
|---|
| 342 | elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b))) |
|---|
| 343 | [ 1: #Hlt >Hlt normalize nodelta |
|---|
| 344 | @(eq_block_elim … b (pblock p)) |
|---|
| 345 | [ 1: #Heq >Heq whd in match (free ??); |
|---|
| 346 | whd in match (update_block ?????); >eq_block_b_b |
|---|
| 347 | normalize nodelta normalize in match (low ?); |
|---|
| 348 | >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta |
|---|
| 349 | #Habsurd destruct (Habsurd) |
|---|
| 350 | | 2: #Hblock_neq whd in match (free ? ?); |
|---|
| 351 | whd in match (update_block ?????); |
|---|
| 352 | >(not_eq_block_rev … Hblock_neq) normalize nodelta |
|---|
| 353 | cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p)))) |
|---|
| 354 | [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] |
|---|
| 355 | >andb_lsimpl_true |
|---|
| 356 | lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) |
|---|
| 357 | (high (blocks m (pblock p)))) |
|---|
| 358 | cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p)))) |
|---|
| 359 | [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] |
|---|
| 360 | normalize nodelta #H #_ /2 by ex_intro/ |
|---|
| 361 | ] |
|---|
| 362 | | 2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ] |
|---|
| 363 | qed. |
|---|
| 364 | |
|---|
| 365 | (* Cf [in_bounds_free_to_in_bounds] *) |
|---|
| 366 | lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true. |
|---|
| 367 | #m #b #p #Hvalid |
|---|
| 368 | cases (valid_pointer_def … m p) #HA #HB |
|---|
| 369 | cases (valid_pointer_def … (free m b) p) #HC #HD |
|---|
| 370 | @HB @(in_bounds_free_to_in_bounds … b) |
|---|
| 371 | @HC @Hvalid |
|---|
| 372 | qed. |
|---|
| 373 | |
|---|
| 374 | (* Making explicit the argument above. *) |
|---|
| 375 | lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p. |
|---|
| 376 | #m #b #p |
|---|
| 377 | whd in match (valid_pointer ??); |
|---|
| 378 | whd in match (free ??); |
|---|
| 379 | whd in match (update_block ????); |
|---|
| 380 | whd in match (low_bound ??); |
|---|
| 381 | whd in match (high_bound ??); |
|---|
| 382 | @(eq_block_elim … b (pblock p)) |
|---|
| 383 | [ 1: #Heq <Heq >eq_block_b_b normalize nodelta |
|---|
| 384 | whd in match (low ?); whd in match (high ?); |
|---|
| 385 | cases (Zltb ? (nextblock m)) |
|---|
| 386 | [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ] |
|---|
| 387 | >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd) |
|---|
| 388 | | 2: #Hneq #_ @Hneq ] |
|---|
| 389 | qed. |
|---|
| 390 | |
|---|
| 391 | (* --------------------------------------------------------------------------- *) |
|---|
| 392 | (* loading and storing are inverse operations for integers. (Paolo's work |
|---|
| 393 | * contain a proof of this fact for pointers) *) |
|---|
| 394 | (* --------------------------------------------------------------------------- *) |
|---|
| 395 | |
|---|
| 396 | lemma fold_left_neq_acc_neq : |
|---|
| 397 | ∀m. ∀acc1,acc2. ∀y1,y2:BitVector m. |
|---|
| 398 | acc1 ≠ acc2 → |
|---|
| 399 | fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc1 y1 ≠ |
|---|
| 400 | fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc2 y2. |
|---|
| 401 | #m elim m |
|---|
| 402 | [ 1: #acc1 #acc2 #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) // |
|---|
| 403 | | 2: #m' #Hind #acc1 #acc2 #y1 #y2 |
|---|
| 404 | elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1 |
|---|
| 405 | elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2 |
|---|
| 406 | >Heq1 >Heq2 * #Hneq % whd in ⊢ ((??%%) → ?); |
|---|
| 407 | cases hd1 cases hd2 normalize nodelta #H |
|---|
| 408 | [ 1: lapply (Hind (p1 acc1) (p1 acc2) tl1 tl2 ?) |
|---|
| 409 | [ 1: % #H' @Hneq destruct (H') @refl ] |
|---|
| 410 | * #H' @H' @H |
|---|
| 411 | | 4: lapply (Hind (p0 acc1) (p0 acc2) tl1 tl2 ?) |
|---|
| 412 | [ 1: % #H' @Hneq destruct (H') @refl ] |
|---|
| 413 | * #H' @H' @H |
|---|
| 414 | | 2: lapply (Hind (p1 acc1) (p0 acc2) tl1 tl2 ?) |
|---|
| 415 | [ 1: % #H' destruct ] |
|---|
| 416 | * #H' @H' try @H |
|---|
| 417 | | 3: lapply (Hind (p0 acc1) (p1 acc2) tl1 tl2 ?) |
|---|
| 418 | [ 1: % #H' destruct ] |
|---|
| 419 | * #H' @H' try @H ] |
|---|
| 420 | ] qed. |
|---|
| 421 | |
|---|
| 422 | lemma fold_left_aux : |
|---|
| 423 | ∀m. ∀acc. ∀y1,y2:BitVector m. |
|---|
| 424 | fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y1 = |
|---|
| 425 | fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y2 → |
|---|
| 426 | y1 = y2. |
|---|
| 427 | #m elim m |
|---|
| 428 | [ 1: #acc #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) // |
|---|
| 429 | | 2: #m' #Hind #acc #y1 #y2 |
|---|
| 430 | elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1 |
|---|
| 431 | elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2 |
|---|
| 432 | >Heq1 >Heq2 whd in ⊢ ((??%%) → ?); |
|---|
| 433 | cases hd1 cases hd2 normalize nodelta |
|---|
| 434 | [ 1,4: #H >(Hind … H) @refl |
|---|
| 435 | | 2: #Habsurd lapply (fold_left_neq_acc_neq ? (p1 acc) (p0 acc) tl1 tl2 ?) |
|---|
| 436 | [ 1: % #H' destruct ] |
|---|
| 437 | * #H @(False_ind … (H Habsurd)) |
|---|
| 438 | | 3: #Habsurd lapply (fold_left_neq_acc_neq ? (p0 acc) (p1 acc) tl1 tl2 ?) |
|---|
| 439 | [ 1: % #H' destruct ] |
|---|
| 440 | * #H @(False_ind … (H Habsurd)) ] |
|---|
| 441 | ] qed. |
|---|
| 442 | |
|---|
| 443 | |
|---|
| 444 | lemma bv_neq_Z_neq_aux : |
|---|
| 445 | ∀n. ∀bv1,bv2 : BitVector n. ∀f. |
|---|
| 446 | Z_of_unsigned_bitvector n bv1 ≠ |
|---|
| 447 | pos (fold_left Pos bool n (λacc:Pos.λb:bool.if b then p1 acc else p0 acc ) (f one) bv2). |
|---|
| 448 | #n elim n |
|---|
| 449 | [ 1: #bv1 #bv2 >(BitVector_O … bv1) >(BitVector_O … bv2) #f normalize % #H destruct |
|---|
| 450 | | 2: #n' #Hind #bv1 #bv2 #f |
|---|
| 451 | elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1 |
|---|
| 452 | elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2 |
|---|
| 453 | >Heq1 >Heq2 % |
|---|
| 454 | whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?); |
|---|
| 455 | cases hd1 cases hd2 normalize nodelta |
|---|
| 456 | normalize in ⊢ ((??%%) → ?); |
|---|
| 457 | [ 1: #Hpos destruct (Hpos) |
|---|
| 458 | lapply (fold_left_neq_acc_neq ? one (p1 (f one)) tl1 tl2 ?) |
|---|
| 459 | [ 1: % #H destruct ] |
|---|
| 460 | * #H @H @e0 |
|---|
| 461 | | 2: #Hpos destruct (Hpos) |
|---|
| 462 | lapply (fold_left_neq_acc_neq ? one (p0 (f one)) tl1 tl2 ?) |
|---|
| 463 | [ 1: % #H destruct ] |
|---|
| 464 | * #H @H @e0 |
|---|
| 465 | | 3: #H cases (Hind tl1 tl2 (λx. p1 (f x))) #H' @H' @H |
|---|
| 466 | | 4: #H cases (Hind tl1 tl2 (λx. p0 (f x))) #H' @H' @H |
|---|
| 467 | ] |
|---|
| 468 | ] qed. |
|---|
| 469 | |
|---|
| 470 | (* Some aux. lemmas (and axioms ...) first *) |
|---|
| 471 | lemma bv_neq_Z_neq : ∀n. ∀bv1,bv2: BitVector n. |
|---|
| 472 | bv1 ≠ bv2 → Z_of_unsigned_bitvector n bv1 ≠ Z_of_unsigned_bitvector n bv2. |
|---|
| 473 | #n #bv1 #bv2 * #Hneq % #Hneq' @Hneq -Hneq lapply Hneq' -Hneq' |
|---|
| 474 | lapply bv2 lapply bv1 -bv1 -bv2 |
|---|
| 475 | elim n |
|---|
| 476 | [ 1: #bv1 #bv2 >(BitVector_O bv1) >(BitVector_O bv2) // |
|---|
| 477 | | 2: #n' #Hind #bv1 #bv2 |
|---|
| 478 | elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1 |
|---|
| 479 | elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2 |
|---|
| 480 | >Heq1 >Heq2 |
|---|
| 481 | whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?); |
|---|
| 482 | cases hd1 cases hd2 normalize nodelta |
|---|
| 483 | [ 1: #Heq destruct (Heq) lapply (fold_left_aux … e0) * @refl |
|---|
| 484 | | 4: #H >(Hind ?? H) @refl |
|---|
| 485 | | 2: #H lapply (sym_eq ??? H) -H #H |
|---|
| 486 | cases (bv_neq_Z_neq_aux ? tl2 tl1 (λx.x)) #H' @(False_ind … (H' H)) |
|---|
| 487 | | 3: #H |
|---|
| 488 | cases (bv_neq_Z_neq_aux ? tl1 tl2 (λx.x)) #H' @(False_ind … (H' H)) ] |
|---|
| 489 | ] qed. |
|---|
| 490 | |
|---|
| 491 | definition Z_of_offset ≝ λofs.Z_of_unsigned_bitvector ? (offv ofs). |
|---|
| 492 | |
|---|
| 493 | |
|---|
| 494 | (* We prove the following properties for bestorev : |
|---|
| 495 | 1) storing doesn't modify the nextblock |
|---|
| 496 | 2) it does not modify the extents of the block written to |
|---|
| 497 | 3) since we succeeded in storing, the offset is in the bounds |
|---|
| 498 | 4) reading where we wrote yields the obvious result |
|---|
| 499 | 5) besides the written offset, the memory contains the same stuff |
|---|
| 500 | *) |
|---|
| 501 | lemma mem_bounds_invariant_after_bestorev : |
|---|
| 502 | ∀m,m',b,ofs,bev. |
|---|
| 503 | bestorev m (mk_pointer b ofs) bev = Some ? m' → |
|---|
| 504 | nextblock m' = nextblock m ∧ |
|---|
| 505 | (∀b.low (blocks m' b) = low (blocks m b) ∧ |
|---|
| 506 | high (blocks m' b) = high (blocks m b)) ∧ |
|---|
| 507 | (low (blocks m b) ≤ (Z_of_offset ofs) ∧ |
|---|
| 508 | (Z_of_offset ofs) < high (blocks m b)) ∧ |
|---|
| 509 | (contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv ofs)) = bev) ∧ |
|---|
| 510 | (∀o. o ≠ ofs → contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv o)) = |
|---|
| 511 | contents (blocks m b) (Z_of_unsigned_bitvector ? (offv o))). |
|---|
| 512 | #m #m' #b #ofs #bev whd in ⊢ ((??%?) → ?); |
|---|
| 513 | #H |
|---|
| 514 | cases (if_opt_inversion ???? H) #Hlt -H normalize nodelta #H |
|---|
| 515 | cases (if_opt_inversion ???? H) #Hlelt -H #H |
|---|
| 516 | cases (andb_inversion … Hlelt) #Hle #Hlt @conj try @conj try @conj try @conj |
|---|
| 517 | destruct try @refl |
|---|
| 518 | [ 1: |
|---|
| 519 | #b' normalize cases b #br #bid cases b' #br' #bid' |
|---|
| 520 | cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize |
|---|
| 521 | try /2 by conj, refl/ |
|---|
| 522 | | 2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H |
|---|
| 523 | | 3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H |
|---|
| 524 | | 4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize |
|---|
| 525 | >eqZb_z_z @refl |
|---|
| 526 | | 5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta |
|---|
| 527 | >eqZb_z_z normalize nodelta |
|---|
| 528 | @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs))) |
|---|
| 529 | [ 1,3: lapply Hneq cases o #bv1 cases ofs #bv2 |
|---|
| 530 | #Hneq lapply (bv_neq_Z_neq ? bv1 bv2 ?) |
|---|
| 531 | [ 1,3: % #Heq destruct cases Hneq #H @H @refl ] |
|---|
| 532 | * #H #Habsurd @(False_ind … (H Habsurd)) |
|---|
| 533 | | 2,4: normalize nodelta #H @refl ] |
|---|
| 534 | ] qed. |
|---|
| 535 | |
|---|
| 536 | (* Shifts an offset [i] times. storen uses a similar operation internally. *) |
|---|
| 537 | let rec shiftn (off:offset) (i:nat) on i : offset ≝ |
|---|
| 538 | match i with |
|---|
| 539 | [ O ⇒ off |
|---|
| 540 | | S n ⇒ |
|---|
| 541 | shiftn (shift_offset 2 off (bitvector_of_nat … 1)) n |
|---|
| 542 | ]. |
|---|
| 543 | |
|---|
| 544 | (* This axioms states that if we do not stray too far, we cannot circle back to ourselves. Pretty trivial, but a |
|---|
| 545 | serious PITA to prove. *) |
|---|
| 546 | axiom shiftn_no_wrap : ∀i. i ≤ 8 → ∀ofs. shiftn ofs i ≠ ofs. |
|---|
| 547 | |
|---|
| 548 | (* Some stuff bunding the size of what we can write in memory *) |
|---|
| 549 | |
|---|
| 550 | (* for leb_elim, shadowed in positive.ma *) |
|---|
| 551 | definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop. |
|---|
| 552 | (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim. |
|---|
| 553 | |
|---|
| 554 | (*include alias "arithmetics/nat.ma".*) |
|---|
| 555 | |
|---|
| 556 | lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. |l| ≤ i → nth_opt A i l = None ?. |
|---|
| 557 | #A #l elim l // |
|---|
| 558 | #hd #tl #H #i elim i |
|---|
| 559 | [ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/ |
|---|
| 560 | | 2: #i' #H' #Hle whd in match (nth_opt ???); @H lapply (monotonic_pred … Hle) // |
|---|
| 561 | ] qed. |
|---|
| 562 | |
|---|
| 563 | (* In order to prove the lemma on store_value_of_type and load_value_of_type, |
|---|
| 564 | we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *) |
|---|
| 565 | lemma typesize_bounded : ∀ty. typesize ty ≤ 8. |
|---|
| 566 | * try // * try // qed. |
|---|
| 567 | |
|---|
| 568 | (* Lifting bound on make_list *) |
|---|
| 569 | lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → |make_list A elt sz| ≤ bound. |
|---|
| 570 | #A #sz elim sz try // |
|---|
| 571 | #sz' #Hind #bound #elt #Hbound normalize |
|---|
| 572 | cases bound in Hbound; |
|---|
| 573 | [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/ |
|---|
| 574 | | 2: #bound' #Hbound' lapply (Hind bound' elt ?) |
|---|
| 575 | [ 1: @(monotonic_pred … Hbound') |
|---|
| 576 | | 2: /2 by le_S_S/ ] |
|---|
| 577 | ] qed. |
|---|
| 578 | |
|---|
| 579 | lemma bytes_of_bitvector_bounded : |
|---|
| 580 | ∀sz,bv. |bytes_of_bitvector (size_intsize sz) bv| = size_intsize sz. |
|---|
| 581 | * #bv normalize |
|---|
| 582 | [ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 // |
|---|
| 583 | | 2: cases (vsplit ????) normalize nodelta #bv0 #bv1 |
|---|
| 584 | cases (vsplit ????) normalize nodelta #bv2 #bv3 // |
|---|
| 585 | | 3: cases (vsplit ????) normalize nodelta #bv0 #bv1 |
|---|
| 586 | cases (vsplit ????) normalize nodelta #bv2 #bv3 |
|---|
| 587 | cases (vsplit ????) normalize nodelta #bv4 #bv5 |
|---|
| 588 | cases (vsplit ????) normalize nodelta #bv6 #bv7 |
|---|
| 589 | // |
|---|
| 590 | ] qed. |
|---|
| 591 | |
|---|
| 592 | lemma map_bounded : |
|---|
| 593 | ∀A,B:Type[0]. ∀l:list A. ∀f. |map A B f l| = |l|. |
|---|
| 594 | #A #B #l elim l try // |
|---|
| 595 | qed. |
|---|
| 596 | |
|---|
| 597 | |
|---|
| 598 | lemma fe_to_be_values_bounded : |
|---|
| 599 | ∀ty,v. |fe_to_be_values ty v| ≤ 8. |
|---|
| 600 | #ty cases ty |
|---|
| 601 | [ 1: #sz #sg ] |
|---|
| 602 | #v whd in match (fe_to_be_values ??); |
|---|
| 603 | cases v normalize nodelta |
|---|
| 604 | [ 1,5: @makelist_bounded @typesize_bounded |
|---|
| 605 | | 2,6: * normalize nodelta #bv |
|---|
| 606 | >map_bounded >bytes_of_bitvector_bounded // |
|---|
| 607 | | 3,7: // |
|---|
| 608 | | 4,8: #ptr // ] |
|---|
| 609 | qed. |
|---|
| 610 | |
|---|
| 611 | lemma fe_to_be_values_nonempty : ∀typ,v. ∃hd,tl. fe_to_be_values typ v = hd :: tl. |
|---|
| 612 | * |
|---|
| 613 | [ 2: * /3 by ex_intro/ * #i |
|---|
| 614 | [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize |
|---|
| 615 | lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq |
|---|
| 616 | <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/ |
|---|
| 617 | | 2: whd in match (fe_to_be_values ??); normalize nodelta normalize |
|---|
| 618 | lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq |
|---|
| 619 | <(vsplit_prod … Heq) normalize nodelta |
|---|
| 620 | lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq' |
|---|
| 621 | /3 by ex_intro/ |
|---|
| 622 | | 3: whd in match (fe_to_be_values ??); normalize nodelta normalize |
|---|
| 623 | lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq |
|---|
| 624 | <(vsplit_prod … Heq) normalize nodelta |
|---|
| 625 | lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq' |
|---|
| 626 | <(vsplit_prod … Heq') normalize nodelta |
|---|
| 627 | lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq'' |
|---|
| 628 | <(vsplit_prod … Heq'') normalize nodelta |
|---|
| 629 | lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq''' |
|---|
| 630 | /3 by ex_intro/ ] |
|---|
| 631 | | 1: #sz #sg * /3 by ex_intro/ * #i |
|---|
| 632 | [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize |
|---|
| 633 | lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq |
|---|
| 634 | <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/ |
|---|
| 635 | | 2: whd in match (fe_to_be_values ??); normalize nodelta normalize |
|---|
| 636 | lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq |
|---|
| 637 | <(vsplit_prod … Heq) normalize nodelta |
|---|
| 638 | lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq' |
|---|
| 639 | /3 by ex_intro/ |
|---|
| 640 | | 3: whd in match (fe_to_be_values ??); normalize nodelta normalize |
|---|
| 641 | lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq |
|---|
| 642 | <(vsplit_prod … Heq) normalize nodelta |
|---|
| 643 | lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq' |
|---|
| 644 | <(vsplit_prod … Heq') normalize nodelta |
|---|
| 645 | lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq'' |
|---|
| 646 | <(vsplit_prod … Heq'') normalize nodelta |
|---|
| 647 | lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq''' |
|---|
| 648 | /3 by ex_intro/ ] |
|---|
| 649 | ] qed. |
|---|
| 650 | |
|---|
| 651 | |
|---|
| 652 | (* /!\ TODO the following proof is extremely ugly and indirect. I expect it to be |
|---|
| 653 | * hugely improvable. |
|---|
| 654 | * /!\ *) |
|---|
| 655 | |
|---|
| 656 | (* We prove some properties of [storen m ptr data]. Note that [data] is a list of back-end chunks. |
|---|
| 657 | What we expect [storen] to do is to store this list starting at [ptr]. The property we expect to |
|---|
| 658 | have is that the contents of this particular zone (ptr to ptr+|data|-1) match exactly [data], and |
|---|
| 659 | that elsewhere the memory is untouched. |
|---|
| 660 | Not so simple. Some observations: |
|---|
| 661 | A) Pointers are encoded as block+offsets, and offsets are bitvectors, hence limited in range (2^16). |
|---|
| 662 | On the other hand, block extents are encoded on Zs and are unbounded. This entails some problems |
|---|
| 663 | when writing at the edge of the range of offsets and wrapping around, but that can be solved |
|---|
| 664 | resorting to ugliness and trickery. |
|---|
| 665 | B) The [data] list is unbounded. Taking into account the point A), this means that we can lose |
|---|
| 666 | data when writing (exactly as when we write in a circular buffer, overwriting previous stuff). |
|---|
| 667 | The only solution to that is to explicitly bound |data| with something reasonable. |
|---|
| 668 | Taking these observations into account, we prove the following invariants: |
|---|
| 669 | 1) storing doesn't modify the nextblock (trivial) |
|---|
| 670 | 2) it does not modify the extents of the block written to (trivial) |
|---|
| 671 | 3) all the offsets on which we run while writing are legal (trivial) |
|---|
| 672 | 3) if we index properly, we hit the stored data in the same order as in the list |
|---|
| 673 | 4) If we hit elsewhere, we find the memory unmodified. We have a problem for defining "elsewhere", |
|---|
| 674 | because bitvectors (hence offsets) are limited in their range. For now, we define "elsewhere" as |
|---|
| 675 | "not reachable by shiftn from [ofs] to |data|" |
|---|
| 676 | 5) the pointer we write to is valid (trivial) |
|---|
| 677 | *) |
|---|
| 678 | lemma mem_bounds_invariant_after_storen : |
|---|
| 679 | ∀data,m,m',b,ofs. |
|---|
| 680 | |data| ≤ 8 → (* 8 is the size of a double. *) |
|---|
| 681 | storen m (mk_pointer b ofs) data = Some ? m' → |
|---|
| 682 | (nextblock m' = nextblock m ∧ |
|---|
| 683 | (∀b.low (blocks m' b) = low (blocks m b) ∧ |
|---|
| 684 | high (blocks m' b) = high (blocks m b)) ∧ |
|---|
| 685 | (∀index. index < |data| → low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧ |
|---|
| 686 | Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧ |
|---|
| 687 | (∀index. index < |data| → nth_opt ? index data = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧ |
|---|
| 688 | (∀o. (∀i. i < |data| → o ≠ shiftn ofs i) → |
|---|
| 689 | contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧ |
|---|
| 690 | (|data| > 0 → valid_pointer m (mk_pointer b ofs) = true)). |
|---|
| 691 | #l elim l |
|---|
| 692 | [ 1: #m #m' #b #ofs #_ normalize #H destruct @conj try @conj try @conj try @conj try @conj try @refl |
|---|
| 693 | [ 1: #b0 @conj try @refl |
|---|
| 694 | (* | 2: #Habsurd @False_ind /2 by le_S_O_absurd/*) |
|---|
| 695 | | 2,3: #i #Habsurd @False_ind elim i in Habsurd; try /2/ |
|---|
| 696 | | 4: #o #Hout @refl |
|---|
| 697 | | 5: #H @False_ind /2 by le_S_O_absurd/ ] |
|---|
| 698 | | 2: #hd #tl #Hind #m #m' #b #ofs #Hsize_bound #Hstoren |
|---|
| 699 | whd in Hstoren:(??%?); |
|---|
| 700 | cases (some_inversion ????? Hstoren) #m'' * #Hbestorev -Hstoren #Hstoren |
|---|
| 701 | lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HI #HJ #HK |
|---|
| 702 | lapply (Hind … Hstoren) [ 1: /2 by le_S_to_le/ ] * * * * * |
|---|
| 703 | #HC #HD #HE #HF #HV #HW @conj try @conj try @conj try @conj try @conj |
|---|
| 704 | [ 1: <HA <HC @refl |
|---|
| 705 | | 2: #b elim (HB b) #HF #HG elim (HD b) #HG #HH @conj try // |
|---|
| 706 | | 4: * |
|---|
| 707 | [ 1: #_ <HJ whd in match (nth 0 ???); |
|---|
| 708 | lapply (HV ofs ?) |
|---|
| 709 | [ 1: #i #Hlt @sym_neq % #Heq lapply (shiftn_no_wrap (S i) ? ofs) |
|---|
| 710 | [ 1: normalize in Hsize_bound; |
|---|
| 711 | cut (|tl| < 8) [ /2 by lt_plus_to_minus_r/ ] |
|---|
| 712 | #Hlt' lapply (transitive_lt … Hlt Hlt') // ] |
|---|
| 713 | * #H @H whd in match (shiftn ??); @Heq |
|---|
| 714 | | 2: cases ofs #ofs' normalize // ] |
|---|
| 715 | | 2: #i' #Hlt lapply (HF i' ?) |
|---|
| 716 | [ 1: normalize normalize in Hlt; lapply (monotonic_pred … Hlt) // |
|---|
| 717 | | 2: #H whd in match (nth_opt ???); >H @refl ] ] |
|---|
| 718 | | 5: #o #H >HV |
|---|
| 719 | [ 2: #i #Hlt @(H (S i) ?) |
|---|
| 720 | normalize normalize in Hlt; /2 by le_S_S/ |
|---|
| 721 | | 1: @HK @(H 0) // ] |
|---|
| 722 | | 6: #_ @(bestorev_to_valid_pointer … Hbestorev) |
|---|
| 723 | | 3: * |
|---|
| 724 | [ 1: #_ <HJ whd in match (shiftn ??); |
|---|
| 725 | lapply (Zleb_true_to_Zle (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) |
|---|
| 726 | lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?); |
|---|
| 727 | whd in match (low_bound ??); whd in match (high_bound ??); |
|---|
| 728 | cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true |
|---|
| 729 | cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) |
|---|
| 730 | [ 2: normalize #Habsurd destruct ] normalize nodelta #Hltb |
|---|
| 731 | lapply (Zltb_true_to_Zlt … Hltb) #Hlt' #Hleb lapply (Hleb (refl ??)) -Hleb #Hleb' |
|---|
| 732 | normalize @conj try assumption |
|---|
| 733 | | 2: #i' #Hlt cases (HB b) #Hlow1 #Hhigh1 cases (HD b) #Hlow2 #Hhigh2 |
|---|
| 734 | lapply (HE i' ?) [ 1: normalize in Hlt ⊢ %;lapply (monotonic_pred … Hlt) // ] |
|---|
| 735 | >Hlow1 >Hhigh1 * #H1 #H2 @conj try @H1 try @H2 |
|---|
| 736 | ] |
|---|
| 737 | ] |
|---|
| 738 | ] qed. |
|---|
| 739 | |
|---|
| 740 | (* Adapting the lemma above to (fe_to_be_values ty v) *) |
|---|
| 741 | lemma mem_bounds_invariant_after_storen_bis : |
|---|
| 742 | ∀ty,v,m,m',b,ofs. |
|---|
| 743 | storen m (mk_pointer b ofs) (fe_to_be_values ty v) = Some ? m' → |
|---|
| 744 | (nextblock m' = nextblock m ∧ |
|---|
| 745 | (∀b.low (blocks m' b) = low (blocks m b) ∧ |
|---|
| 746 | high (blocks m' b) = high (blocks m b)) ∧ |
|---|
| 747 | (∀index. index < |fe_to_be_values ty v| → |
|---|
| 748 | low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧ |
|---|
| 749 | Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧ |
|---|
| 750 | (∀index. index < |(fe_to_be_values ty v)| → |
|---|
| 751 | nth_opt ? index (fe_to_be_values ty v) = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧ |
|---|
| 752 | (∀o. (∀i. i < |fe_to_be_values ty v| → o ≠ shiftn ofs i) → |
|---|
| 753 | contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧ |
|---|
| 754 | (valid_pointer m (mk_pointer b ofs) = true)). |
|---|
| 755 | #ty #v #m #m' #b #ofs #Hstoren |
|---|
| 756 | lapply (mem_bounds_invariant_after_storen … Hstoren) |
|---|
| 757 | [ @fe_to_be_values_bounded ] |
|---|
| 758 | * * * * * #H1 #H2 #H3 #H4 #H5 #H6 @conj try @conj try @conj try @conj try @conj |
|---|
| 759 | try assumption @H6 |
|---|
| 760 | cases (fe_to_be_values_nonempty ty v) #hd * #tl #H >H // |
|---|
| 761 | qed. |
|---|
| 762 | |
|---|
| 763 | (* extension of [bestorev_to_valid_pointer] to storen *) |
|---|
| 764 | lemma storen_to_valid_pointer : |
|---|
| 765 | ∀data,xd,m,ptr,m'. storen m ptr (xd::data) = Some ? m' → |
|---|
| 766 | (∀b.low (blocks m' b) = low (blocks m b) ∧ |
|---|
| 767 | high (blocks m' b) = high (blocks m b)) ∧ |
|---|
| 768 | nextblock m' = nextblock m ∧ |
|---|
| 769 | valid_pointer m ptr = true ∧ |
|---|
| 770 | valid_pointer m' ptr = true. |
|---|
| 771 | #data elim data |
|---|
| 772 | [ 1: #xd #m #ptr #res #Hstoren whd in Hstoren:(??%?); |
|---|
| 773 | cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren' |
|---|
| 774 | normalize in Hstoren'; destruct (Hstoren') |
|---|
| 775 | lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF |
|---|
| 776 | lapply (bestorev_to_valid_pointer … Hbestorev) #Hvalid_ptr @conj try @conj try @conj try assumption |
|---|
| 777 | @(bestorev_to_valid_pointer_after … Hbestorev) |
|---|
| 778 | | 2: #hd #tl #Hind #xd #m #ptr #res whd in match (storen ???); #Hstoren |
|---|
| 779 | cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren' -Hstoren |
|---|
| 780 | whd in match (shift_pointer ???) in Hstoren'; |
|---|
| 781 | lapply (bestorev_to_valid_pointer … Hbestorev) #H @conj try @conj try @conj try // |
|---|
| 782 | lapply (Hind … Hstoren') * * * #Hbounds #Hnext #Hvalid1 #Hvalid2 |
|---|
| 783 | lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF |
|---|
| 784 | [ 1: #b @conj cases (Hbounds b) #HG #HH cases (HB b) #HI #HJ try // |
|---|
| 785 | | 2: >Hnext >HA @refl ] |
|---|
| 786 | @valid_pointer_of_Prop @conj try @conj try @conj |
|---|
| 787 | cases (Hbounds (pblock ptr)) #HG #HH cases (HB (pblock ptr)) #HI #HJ |
|---|
| 788 | [ 2: cases HC #Hlow #_ whd in match (low_bound ??); |
|---|
| 789 | whd in match (Z_of_offset ?) in Hlow; |
|---|
| 790 | >HG >HI @Hlow |
|---|
| 791 | | 3: cases HC #_ #Hhigh whd in match (high_bound ??); >HH >HJ @Hhigh ] |
|---|
| 792 | lapply (valid_pointer_to_Prop … Hvalid2) * * #Hnext #Hlow #Hhigh // |
|---|
| 793 | ] qed. |
|---|
| 794 | |
|---|
| 795 | |
|---|
| 796 | |
|---|
| 797 | lemma storen_to_valid_pointer_fe_to_be : |
|---|
| 798 | ∀typ,v,m,ptr,m'. storen m ptr (fe_to_be_values typ v) = Some ? m' → |
|---|
| 799 | (∀b.low (blocks m' b) = low (blocks m b) ∧ |
|---|
| 800 | high (blocks m' b) = high (blocks m b)) ∧ |
|---|
| 801 | nextblock m' = nextblock m ∧ |
|---|
| 802 | valid_pointer m ptr = true ∧ |
|---|
| 803 | valid_pointer m' ptr = true. |
|---|
| 804 | #typ #v cases (fe_to_be_values_nonempty … typ v) #hd * #tl #Heq >Heq |
|---|
| 805 | @storen_to_valid_pointer |
|---|
| 806 | qed. |
|---|
| 807 | |
|---|
| 808 | lemma storen_beloadv_ok : |
|---|
| 809 | ∀m,m',b,ofs,hd,tl. |
|---|
| 810 | |hd::tl| ≤ 8 → (* 8 is the size of a double. *) |
|---|
| 811 | storen m (mk_pointer b ofs) (hd::tl) = Some ? m' → |
|---|
| 812 | ∀i. i < |hd::tl| → beloadv m' (mk_pointer b (shiftn ofs i)) = nth_opt ? i (hd::tl). |
|---|
| 813 | #m #m' #b #ofs #hd #tl #Hle #Hstoren |
|---|
| 814 | lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * |
|---|
| 815 | #Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr |
|---|
| 816 | #i #Hle lapply (Hdata i Hle) #Helt >Helt |
|---|
| 817 | whd in match (beloadv ??); whd in match (nth_opt ???); |
|---|
| 818 | lapply (Hvalid_ptr ?) try // |
|---|
| 819 | whd in ⊢ ((??%?) → ?); |
|---|
| 820 | >Hnext cases (Zltb (block_id b) (nextblock m)) |
|---|
| 821 | [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct ] |
|---|
| 822 | >andb_lsimpl_true normalize nodelta |
|---|
| 823 | whd in match (low_bound ??); whd in match (high_bound ??); |
|---|
| 824 | cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh #H |
|---|
| 825 | lapply (Hvalid_offs i Hle) * #Hzle #Hzlt |
|---|
| 826 | >(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl |
|---|
| 827 | qed. |
|---|
| 828 | |
|---|
| 829 | lemma storen_loadn_nonempty : |
|---|
| 830 | ∀data,m,m',b,ofs. |
|---|
| 831 | |data| ≤ 8 → |
|---|
| 832 | storen m (mk_pointer b ofs) data = Some ? m' → |
|---|
| 833 | ∃result. loadn m' (mk_pointer b ofs) (|data|) = Some ? result ∧ |result|=|data|. |
|---|
| 834 | #data elim data |
|---|
| 835 | [ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ] |
|---|
| 836 | #hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren |
|---|
| 837 | lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * |
|---|
| 838 | #Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr |
|---|
| 839 | cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0 |
|---|
| 840 | whd in match (loadn ???); |
|---|
| 841 | lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?); |
|---|
| 842 | whd in match (beloadv ??); |
|---|
| 843 | whd in match (low_bound ??); whd in match (high_bound ??); |
|---|
| 844 | >Hnext |
|---|
| 845 | cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true |
|---|
| 846 | normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh |
|---|
| 847 | cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta |
|---|
| 848 | [ 2: #Habsurd destruct ] >andb_lsimpl_true |
|---|
| 849 | #Hltb >Hltb normalize nodelta |
|---|
| 850 | cases (Hind … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ] |
|---|
| 851 | #tl' * #Hloadn >Hloadn #Htl' normalize nodelta |
|---|
| 852 | %{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl |
|---|
| 853 | normalize >Htl' @refl |
|---|
| 854 | qed. |
|---|
| 855 | |
|---|
| 856 | |
|---|
| 857 | lemma loadn_beloadv_ok : |
|---|
| 858 | ∀size,m,b,ofs,result. |
|---|
| 859 | loadn m (mk_pointer b ofs) size = Some ? result → |
|---|
| 860 | ∀i. i < size → beloadv m (mk_pointer b (shiftn ofs i)) = nth_opt ? i result. |
|---|
| 861 | #size elim size |
|---|
| 862 | [ 1: #m #b #ofs #result #Hloadn * |
|---|
| 863 | [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/ |
|---|
| 864 | | 2: #i' #Habsurd @False_ind /2 by le_S_O_absurd/ ] |
|---|
| 865 | | 2: #size' #Hind_size #m #b #ofs #result #Hloadn #i |
|---|
| 866 | elim i |
|---|
| 867 | [ 1: #_ |
|---|
| 868 | cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn' |
|---|
| 869 | cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq |
|---|
| 870 | destruct (Heq) whd in match (shiftn ofs 0); |
|---|
| 871 | >Hbeloadv @refl |
|---|
| 872 | | 2: #i' #Hind #Hlt |
|---|
| 873 | whd in match (shiftn ofs (S i')); |
|---|
| 874 | lapply (Hind ?) |
|---|
| 875 | [ /2 by lt_S_to_lt/ ] #Hbeloadv_ind |
|---|
| 876 | whd in Hloadn:(??%?); |
|---|
| 877 | cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn' |
|---|
| 878 | cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq -Hloadn' |
|---|
| 879 | destruct (Heq) |
|---|
| 880 | @Hind_size [ 2: lapply Hlt normalize @monotonic_pred ] |
|---|
| 881 | @Hloadn_tl |
|---|
| 882 | ] |
|---|
| 883 | ] qed. |
|---|
| 884 | |
|---|
| 885 | |
|---|
| 886 | |
|---|
| 887 | lemma storen_loadn_ok : |
|---|
| 888 | ∀data. |
|---|
| 889 | |data| ≤ 8 → (* 8 is the size of a double. *) |
|---|
| 890 | ∀m,m',b,ofs. |
|---|
| 891 | storen m (mk_pointer b ofs) data = Some ? m' → |
|---|
| 892 | loadn m' (mk_pointer b ofs) (|data|) = Some ? data. |
|---|
| 893 | #data elim data try // #hd #tl #Hind #Hle #m #m' #b #ofs #Hstoren |
|---|
| 894 | lapply (storen_beloadv_ok m m' … Hle Hstoren) #Hyp_storen |
|---|
| 895 | cases (storen_loadn_nonempty … Hle Hstoren) #result * #Hloadn #Hresult_sz |
|---|
| 896 | lapply (loadn_beloadv_ok (|hd::tl|) m' b ofs … Hloadn) #Hyp_loadn |
|---|
| 897 | cut (∀i. i < |hd::tl| → nth_opt ? i (hd::tl) = nth_opt ? i result) |
|---|
| 898 | [ #i #Hlt lapply (Hyp_storen … i Hlt) #Heq1 |
|---|
| 899 | lapply (Hyp_loadn … i Hlt) #Heq2 >Heq1 in Heq2; // ] |
|---|
| 900 | #Hyp |
|---|
| 901 | cut (result = hd :: tl) |
|---|
| 902 | [ 2: #Heq destruct (Heq) @Hloadn ] |
|---|
| 903 | @nth_eq_to_eq #i @sym_eq |
|---|
| 904 | @(leb_elim' … (S i) (|hd::tl|)) |
|---|
| 905 | [ 1: #Hle @(Hyp ? Hle) |
|---|
| 906 | | 2: #Hnle cut (|hd::tl| ≤ i) |
|---|
| 907 | [ lapply (not_le_to_lt … Hnle) normalize |
|---|
| 908 | @monotonic_pred ] |
|---|
| 909 | #Hle' |
|---|
| 910 | >nth_miss // >nth_miss // |
|---|
| 911 | ] qed. |
|---|
| 912 | |
|---|
| 913 | |
|---|
| 914 | lemma mem_bounds_after_store_value_of_type : |
|---|
| 915 | ∀m,m',ty,b,o,v. |
|---|
| 916 | store_value_of_type ty m b o v = Some ? m' → |
|---|
| 917 | (nextblock m' = nextblock m ∧ |
|---|
| 918 | (∀b.low (blocks m' b) = low (blocks m b) ∧ |
|---|
| 919 | high (blocks m' b) = high (blocks m b))). |
|---|
| 920 | #m #m' #ty #b #o #v |
|---|
| 921 | lapply (fe_to_be_values_bounded (typ_of_type ty) v) |
|---|
| 922 | cases ty |
|---|
| 923 | [ 1: | 2: #sz #sg | 3: #ptrty | 4: #arrayty #arraysz | 5: #argsty #retty |
|---|
| 924 | | 6: #sid #fields | 7: #uid #fields | 8: #cptr_id ] |
|---|
| 925 | whd in match (typ_of_type ?); #Hbounded |
|---|
| 926 | whd in match (store_value_of_type ?????); |
|---|
| 927 | [ 1,4,5,6,7: #Habsurd destruct (Habsurd) |
|---|
| 928 | | *: #Hstoren lapply (mem_bounds_invariant_after_storen … Hbounded Hstoren) |
|---|
| 929 | * * * * * #Hnextblock #Hbounds_eq #Hnonempty |
|---|
| 930 | #Hcontents_upd #Hcontents_inv #Hvalid_ptr |
|---|
| 931 | >Hnextblock @conj // |
|---|
| 932 | ] qed. |
|---|
| 933 | |
|---|
| 934 | lemma mem_bounds_after_store_value_of_type' : |
|---|
| 935 | ∀m,m',ty,p,v. |
|---|
| 936 | store_value_of_type' ty m p v = Some ? m' → |
|---|
| 937 | (nextblock m' = nextblock m ∧ |
|---|
| 938 | (∀b.low (blocks m' b) = low (blocks m b) ∧ |
|---|
| 939 | high (blocks m' b) = high (blocks m b))). |
|---|
| 940 | #m #m' #ty * #b #o #v whd in match (store_value_of_type' ????); |
|---|
| 941 | @mem_bounds_after_store_value_of_type |
|---|
| 942 | qed. |
|---|
| 943 | |
|---|
| 944 | |
|---|
| 945 | definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v. |
|---|
| 946 | match ty with |
|---|
| 947 | [ ASTint sz sg ⇒ |
|---|
| 948 | match v with |
|---|
| 949 | [ Vint sz' sg' ⇒ sz = sz' (* The sign does not matter *) |
|---|
| 950 | | _ ⇒ False ] |
|---|
| 951 | | ASTptr ⇒ |
|---|
| 952 | match v with |
|---|
| 953 | [ Vptr p ⇒ True |
|---|
| 954 | | _ ⇒ False ] |
|---|
| 955 | ]. |
|---|
| 956 | |
|---|
| 957 | |
|---|
| 958 | definition type_consistent_with_value : type → val → Prop ≝ λty,v. |
|---|
| 959 | match access_mode ty with |
|---|
| 960 | [ By_value chunk ⇒ ast_typ_consistent_with_value chunk v |
|---|
| 961 | | _ ⇒ True |
|---|
| 962 | ]. |
|---|
| 963 | |
|---|
| 964 | (* We also need the following property. It is not provable unless [v] and [ty] are consistent. *) |
|---|
| 965 | lemma fe_to_be_values_size : |
|---|
| 966 | ∀ty,v. ast_typ_consistent_with_value ty v → |
|---|
| 967 | typesize ty = |fe_to_be_values ty v|. |
|---|
| 968 | * |
|---|
| 969 | [ 1: #sz #sg #v |
|---|
| 970 | whd in match (fe_to_be_values ??); cases v |
|---|
| 971 | normalize in ⊢ (% → ?); |
|---|
| 972 | [ 1,3: @False_ind |
|---|
| 973 | | 2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta |
|---|
| 974 | >map_bounded >bytes_of_bitvector_bounded cases sz' // |
|---|
| 975 | | 4: #p normalize in ⊢ (% → ?); @False_ind ] |
|---|
| 976 | | 2: #v cases v |
|---|
| 977 | normalize in ⊢ (% → ?); |
|---|
| 978 | [ 1,3: @False_ind |
|---|
| 979 | | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind |
|---|
| 980 | | 4: #p #_ // ] |
|---|
| 981 | ] qed. |
|---|
| 982 | |
|---|
| 983 | (* Not verified for floats atm. Restricting to integers. *) |
|---|
| 984 | lemma fe_to_be_to_fe_value_int : ∀sz,sg,v. |
|---|
| 985 | ast_typ_consistent_with_value (ASTint sz sg) v → |
|---|
| 986 | (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v). |
|---|
| 987 | #sz #sg #v |
|---|
| 988 | whd in match (fe_to_be_values ??); |
|---|
| 989 | cases v normalize in ⊢ (% → ?); |
|---|
| 990 | [ 1,3: @False_ind |
|---|
| 991 | | 4: #p @False_ind |
|---|
| 992 | | 2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta |
|---|
| 993 | cases sz' in i'; #i normalize nodelta |
|---|
| 994 | normalize in i; |
|---|
| 995 | whd in match (be_to_fe_value ??); |
|---|
| 996 | normalize in match (size_intsize ?); |
|---|
| 997 | whd in match (bytes_of_bitvector ??); |
|---|
| 998 | [ 1: lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i |
|---|
| 999 | <(vsplit_prod … Heq_i) normalize nodelta >Heq_i |
|---|
| 1000 | whd in match (build_integer_val ??); |
|---|
| 1001 | >(BitVector_O … ri) // |
|---|
| 1002 | | 2: lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i |
|---|
| 1003 | <(vsplit_prod … Heq_i) normalize nodelta >Heq_i |
|---|
| 1004 | whd in match (build_integer_val ??); |
|---|
| 1005 | normalize in match (size_intsize ?); |
|---|
| 1006 | whd in match (bytes_of_bitvector ??); |
|---|
| 1007 | lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri |
|---|
| 1008 | <(vsplit_prod … Heq_ri) normalize nodelta >Heq_ri |
|---|
| 1009 | whd in match (build_integer_val ??); |
|---|
| 1010 | >(BitVector_O … rri) // |
|---|
| 1011 | | 3: lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i |
|---|
| 1012 | <(vsplit_prod … Heq_i) normalize nodelta >Heq_i |
|---|
| 1013 | whd in match (build_integer_val ??); |
|---|
| 1014 | normalize in match (size_intsize ?); |
|---|
| 1015 | whd in match (bytes_of_bitvector ??); |
|---|
| 1016 | lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB |
|---|
| 1017 | <(vsplit_prod … Heq_iB) normalize nodelta >Heq_iB |
|---|
| 1018 | whd in match (bytes_of_bitvector ??); |
|---|
| 1019 | lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD |
|---|
| 1020 | <(vsplit_prod … Heq_iD) normalize nodelta >Heq_iD |
|---|
| 1021 | whd in match (bytes_of_bitvector ??); |
|---|
| 1022 | lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF |
|---|
| 1023 | <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF |
|---|
| 1024 | >(BitVector_O … iH) @refl ] |
|---|
| 1025 | ] qed. |
|---|
| 1026 | |
|---|
| 1027 | lemma fe_to_be_to_fe_value_ptr : |
|---|
| 1028 | ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)). |
|---|
| 1029 | #b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta |
|---|
| 1030 | cases br normalize nodelta >eqZb_z_z normalize nodelta |
|---|
| 1031 | cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq |
|---|
| 1032 | <(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl |
|---|
| 1033 | * // |
|---|
| 1034 | qed. |
|---|
| 1035 | |
|---|
| 1036 | (* It turns out that the following property is not true in general. Floats are converted to |
|---|
| 1037 | BVundef, which are converted back to Vundef. But we care only about ints. *) |
|---|
| 1038 | lemma storev_loadv_int_compatible : |
|---|
| 1039 | ∀sz,sg,m,b,ofs,v,m'. |
|---|
| 1040 | ast_typ_consistent_with_value (ASTint sz sg) v → |
|---|
| 1041 | store (ASTint sz sg) m (mk_pointer b ofs) v = Some ? m' → |
|---|
| 1042 | load (ASTint sz sg) m' (mk_pointer b ofs) = Some ? v. |
|---|
| 1043 | #sz #sg #m #b #ofs #v #m' #H |
|---|
| 1044 | whd in ⊢ ((??%?) → (??%?)); #Hstoren |
|---|
| 1045 | lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren) |
|---|
| 1046 | >(fe_to_be_values_size … H) #H >H normalize nodelta |
|---|
| 1047 | >fe_to_be_to_fe_value_int try // |
|---|
| 1048 | qed. |
|---|
| 1049 | |
|---|
| 1050 | (* For the arguments exposed before, we restrict the lemma to ints. *) |
|---|
| 1051 | lemma store_value_load_value_int_compatible : |
|---|
| 1052 | ∀sz,sg,m,b,ofs,v,m'. |
|---|
| 1053 | type_consistent_with_value (Tint sz sg) v → |
|---|
| 1054 | store_value_of_type (Tint sz sg) m b ofs v = Some ? m' → |
|---|
| 1055 | load_value_of_type (Tint sz sg) m' b ofs = Some ? v. |
|---|
| 1056 | #sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?); |
|---|
| 1057 | cases v in H; normalize nodelta |
|---|
| 1058 | [ 1: #_ @False_ind | 2: #vsz #vi #H | 3: #_ @False_ind | 4: #vp #_ @False_ind ] |
|---|
| 1059 | #Heq >Heq in H; #H |
|---|
| 1060 | (* The lack of control on unfolds is extremely annoying. *) |
|---|
| 1061 | whd in match (store_value_of_type ?????); #Hstoren |
|---|
| 1062 | lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint vsz sg) (Vint vsz vi)) m m' b ofs Hstoren) |
|---|
| 1063 | whd in match (load_value_of_type ????); |
|---|
| 1064 | >(fe_to_be_values_size … H) #H' >H' normalize nodelta |
|---|
| 1065 | >fe_to_be_to_fe_value_int try // |
|---|
| 1066 | qed. |
|---|
| 1067 | |
|---|
| 1068 | lemma store_value_load_value_compatible : |
|---|
| 1069 | ∀ty,m,b,ofs,v,m'. |
|---|
| 1070 | type_consistent_with_value ty v → |
|---|
| 1071 | store_value_of_type ty m b ofs v = Some ? m' → |
|---|
| 1072 | load_value_of_type ty m' b ofs = Some ? v. |
|---|
| 1073 | #ty #m #b #ofs #v #m' #H lapply H cases ty |
|---|
| 1074 | [ | #sz #sg | #ty' | #ty' #n | #tl #ty' | #id #fl | #id #fl | #id ] |
|---|
| 1075 | [ 1,4,5,6,7: normalize in ⊢ (? → % → ?); #_ #Habsurd destruct |
|---|
| 1076 | | 2: @store_value_load_value_int_compatible |
|---|
| 1077 | | 3: #Hconsistent whd in match (store_value_of_type ?????); |
|---|
| 1078 | whd in match (load_value_of_type ????); #Hstoren |
|---|
| 1079 | lapply (storen_loadn_ok … Hstoren) |
|---|
| 1080 | [ @fe_to_be_values_bounded ] |
|---|
| 1081 | #Hloadn >(fe_to_be_values_size … Hconsistent) |
|---|
| 1082 | >Hloadn normalize nodelta |
|---|
| 1083 | cases v in Hconsistent; |
|---|
| 1084 | [ @False_ind | #sz' #i' @False_ind | 3: @False_ind ] |
|---|
| 1085 | * #pb #poff #Hconsistent >fe_to_be_to_fe_value_ptr @refl |
|---|
| 1086 | | 8: #Hconsistent whd in match (store_value_of_type ?????); |
|---|
| 1087 | whd in match (load_value_of_type ????); #Hstoren |
|---|
| 1088 | lapply (storen_loadn_ok … Hstoren) |
|---|
| 1089 | [ @fe_to_be_values_bounded ] |
|---|
| 1090 | #Hloadn >(fe_to_be_values_size … Hconsistent) |
|---|
| 1091 | >Hloadn normalize nodelta |
|---|
| 1092 | cases v in Hconsistent; |
|---|
| 1093 | [ @False_ind | #sz' #i' @False_ind | 3: @False_ind ] |
|---|
| 1094 | * #pb #poff #Hconsistent >fe_to_be_to_fe_value_ptr @refl |
|---|
| 1095 | ] qed. |
|---|
| 1096 | |
|---|
| 1097 | (* storing something somewhere and loading at a disjoint loc yields the |
|---|
| 1098 | same result as before the store. *) |
|---|
| 1099 | lemma store_value_load_disjoint : |
|---|
| 1100 | ∀ty1,ty2,m,b1,ofs1,b2,ofs2,v,m'. |
|---|
| 1101 | ty1 ≠ ty2 → |
|---|
| 1102 | type_consistent_with_value ty1 v → |
|---|
| 1103 | store_value_of_type ty1 m b1 ofs1 v = Some ? m' → |
|---|
| 1104 | (b1 ≠ b2 |
|---|
| 1105 | ∨ ((Z_of_offset ofs1) + (Z_of_nat (typesize (typ_of_type ty1))) ≤ (Z_of_offset ofs2)) |
|---|
| 1106 | ∨ ((Z_of_offset ofs2) + (Z_of_nat (typesize (typ_of_type ty2))) ≤ (Z_of_offset ofs1))) → |
|---|
| 1107 | load_value_of_type ty2 m b2 ofs2 = load_value_of_type ty2 m' b2 ofs2. |
|---|
| 1108 | #ty1 #ty2 #m #b1 #ofs1 #b2 #ofs2 #v #m' |
|---|
| 1109 | @cthulhu (* Provable using the invariants provided by storen (see prev. lemma) *) |
|---|
| 1110 | qed. |
|---|
| 1111 | |
|---|
| 1112 | (* Can we say anything about what we load in the overlap case ? *) |
|---|
| 1113 | (* |
|---|
| 1114 | lemma store_value_load_overlap : |
|---|
| 1115 | ∀ty1,ty2,m,b,ofs1,ofs2,v,m'. |
|---|
| 1116 | ty1 ≠ ty2 → |
|---|
| 1117 | type_consistent_with_value ty1 v → |
|---|
| 1118 | store_value_of_type ty1 m b1 ofs1 v = Some ? m' → |
|---|
| 1119 | (Z_of_offset ofs2 < (Z_of_offset ofs1) + (Z_of_nat (typesize (typ_of_type ty1))) |
|---|
| 1120 | ∨ Z_of_offset ofs1 < (Z_of_offset ofs2) + (Z_of_nat (typesize (typ_of_type ty2)))) → |
|---|
| 1121 | load_value_of_type ty2 m b2 ofs2 = load_value_of_type ty2 m' b2 ofs2. |
|---|
| 1122 | *) |
|---|
