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