Changeset 2468 for src/Clight/memoryInjections.ma
 Timestamp:
 Nov 15, 2012, 6:12:57 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/memoryInjections.ma
r2448 r2468 1 1 include "Clight/Cexec.ma". 2 include "Clight/MemProperties.ma". 2 3 include "Clight/frontend_misc.ma". 3 4 … … 7 8 not allow to prove that the semantics for pointer lessthan comparisons is 8 9 conserved). *) 9 10 (*  *)11 (* Some general lemmas on bitvectors (offsets /are/ bitvectors) *)12 (*  *)13 14 lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉.15 #n #bv whd in match (add_with_carries ????); elim bv //16 #n #hd #tl #Hind whd in match (fold_right2_i ????????);17 >Hind normalize18 cases n in tl;19 [ 1: #tl cases hd normalize @refl20  2: #n' #tl cases hd normalize @refl ]21 qed.22 23 lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv.24 #n #bv whd in match (addition_n ???);25 >add_with_carries_n_O //26 qed.27 28 lemma replicate_Sn : ∀A,sz,elt.29 replicate A (S sz) elt = elt ::: (replicate A sz elt).30 // qed.31 32 lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed.33 34 lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a).35 #n #xa #a normalize @refl qed.36 37 (* useful facts on carry_of *)38 lemma carry_of_TT : ∀x. carry_of true true x = true. // qed.39 lemma carry_of_TF : ∀x. carry_of true false x = x. // qed.40 lemma carry_of_FF : ∀x. carry_of false false x = false. // qed.41 lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed.42 lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed.43 44 45 46 definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)).47 48 lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n).49 add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 →50 add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉.51 #n elim n52 [ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits53 elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags54 >(BitVector_O … tl_flags) >(BitVector_O … tl_bits)55 normalize #Heq destruct (Heq) @refl56  2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits57 destruct #Hind >add_with_carries_Sn >replicate_Sn58 whd in match (zero ?) in Hind; lapply Hind59 elim (add_with_carries (S (S n'))60 (false:::replicate bool (S n') false)61 (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct62 normalize >add_with_carries_Sn in Hind;63 elim (add_with_carries (S n') (replicate bool (S n') false)64 (replicate bool (S n') false) true) #flags' #bits'65 normalize66 cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with67 [VEmpty⇒trueVCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy])68 normalize #Heq destruct @refl69 ] qed.70 71 lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)).72 #n lapply (one_bv_Sn_aux n)73 whd in match (one_bv ?) in ⊢ (? → (??%%));74 elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags75 #H lapply (H bits flags (refl ??)) #H2 >H2 @refl76 qed.77 78 lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n.79 add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false.80 #n81 elim n82 [ 1: #a >(BitVector_O … a) normalize @refl83  2: #n' cases n'84 [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct85 >(BitVector_O … tl) normalize cases xa @refl86  2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct87 >one_bv_Sn >zero_Sn88 lapply (Hind tl)89 >add_with_carries_Sn >add_with_carries_Sn90 #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags91 normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq92 normalize nodelta @refl93 ] qed.94 95 (* In order to use associativity on increment, we hide it under addition_n. *)96 lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n).97 #n98 whd in match (increment ??) in ⊢ (∀_.??%?);99 whd in match (addition_n ???) in ⊢ (∀_.???%);100 #a lapply (increment_to_addition_n_aux n a)101 #Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl102 qed.103 104 (* Explicit formulation of addition *)105 106 (* Explicit formulation of the last carry bit *)107 let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝108 match n return λx. BitVector x → BitVector x → bool with109 [ O ⇒ λ_,_. init110  S x ⇒ λa',b'.111 let hd_a ≝ head' … a' in112 let hd_b ≝ head' … b' in113 let tl_a ≝ tail … a' in114 let tl_b ≝ tail … b' in115 carry_of hd_a hd_b (ith_carry x tl_a tl_b init)116 ] a b.117 118 lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).119 ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)).120 #n #init #a #b @refl qed.121 122 lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.123 ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed.124 125 (* correction of [ith_carry] *)126 lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).127 〈res_ab,flags_ab〉 = add_with_carries ? a b init →128 head' … flags_ab = ith_carry ? a b init.129 #n elim n130 [ 1: #init #a #b #res_ab #flags_ab131 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a132 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b133 elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res134 elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags135 destruct136 >(BitVector_O … tl_a) >(BitVector_O … tl_b)137 cases hd_a cases hd_b cases init normalize #Heq destruct (Heq)138 @refl139  2: #n' #Hind #init #a #b #res_ab #flags_ab140 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a141 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b142 elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res143 elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags144 destruct145 lapply (Hind … init tl_a tl_b tl_res tl_flags)146 >add_with_carries_Sn >(ith_carry_Sn (S n'))147 elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab148 elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab149 normalize nodelta cases hd_flags_ab normalize nodelta150 whd in match (head' ? (S n') ?); #H1 #H2151 destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl152 ] qed.153 154 (* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *)155 definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit.156 match n return λx. BitVector x → BitVector x → bool with157 [ O ⇒ λ_,_. init158  S x ⇒ λa',b'.159 let hd_a ≝ head' … a' in160 let hd_b ≝ head' … b' in161 let tl_a ≝ tail … a' in162 let tl_b ≝ tail … b' in163 xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init)164 ] a b.165 166 lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).167 ith_bit ? a b init = xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init).168 #n #a #b // qed.169 170 lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.171 ith_bit ? (xa ::: a) (xb ::: b) init = xorb (xorb xa xb) (ith_carry ? a b init). // qed.172 173 (* correction of ith_bit *)174 lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).175 〈res_ab,flags_ab〉 = add_with_carries ? a b init →176 head' … res_ab = ith_bit ? a b init.177 #n178 cases n179 [ 1: #init #a #b #res_ab #flags_ab180 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a181 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b182 elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res183 elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags184 destruct185 >(BitVector_O … tl_a) >(BitVector_O … tl_b)186 >(BitVector_O … tl_flags) >(BitVector_O … tl_res)187 normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl188  2: #n' #init #a #b #res_ab #flags_ab189 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a190 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b191 elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res192 elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags193 destruct194 lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags)195 #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry;196 #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags'197 >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2)198 cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %;199 <(H1 (refl ??)) @refl200 ] qed.201 202 (* Transform a function from bitvectors to bits into a vector by folding *)203 let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝204 match v with205 [ VEmpty ⇒ VEmpty ?206  VCons sz elt tl ⇒207 let bit ≝ f ? v in208 bit ::: (bitvector_fold ? tl f)209 ].210 211 (* Twoarguments version *)212 let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝213 match v1 with214 [ VEmpty ⇒ λ_. VEmpty ?215  VCons sz elt tl ⇒ λv2'.216 let bit ≝ f ? v1 v2 in217 bit ::: (bitvector_fold2 ? tl (tail … v2') f)218 ] v2.219 220 lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f.221 bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed.222 223 (* These functions pack all the relevant information (including carries) directly. *)224 definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init).225 226 lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init.227 addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed.228 229 lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed.230 231 (* Prove the equivalence of addition_n_direct with add_with_carries *)232 lemma addition_n_direct_ok : ∀n,carry,v1,v2.233 (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry.234 #n elim n235 [ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl236  2: #n' #Hind #carry #v1 #v2237 elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1238 elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2239 lapply (Hind carry tl1 tl2)240 lapply (ith_bit_ok ? carry v1 v2)241 lapply (ith_carry_ok ? carry v1 v2)242 destruct243 #Hind >addition_n_direct_Sn244 >ith_bit_Sn >add_with_carries_Sn245 elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta246 cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with247 [VEmpty⇒carryVCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy])248 normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??))249 whd in match head'; normalize nodelta250 #H1 #H2 >H1 >H2 @refl251 ] qed.252 253 lemma addition_n_direct_ok2 : ∀n,carry,v1,v2.254 (let 〈a,b〉 ≝ add_with_carries n v1 v2 carry in a) = addition_n_direct n v1 v2 carry.255 #n #carry #v1 #v2 <addition_n_direct_ok256 cases (add_with_carries ????) //257 qed.258 259 (* trivially lift associativity to our new setting *)260 lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n.261 addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 =262 addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2.263 #n #carry1 #carry2 #v1 #v2 #v3264 <addition_n_direct_ok <addition_n_direct_ok265 <addition_n_direct_ok <addition_n_direct_ok266 lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3)267 elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta268 elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta269 #H @(sym_eq … H)270 qed.271 272 lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n.273 addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false.274 #n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/275 qed.276 277 definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.278 definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).279 280 281 (* fold andb on a bitvector. *)282 let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝283 match b with284 [ VEmpty ⇒ true285  VCons sz elt tl ⇒286 andb elt (andb_fold ? tl)287 ].288 289 lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed.290 291 lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true.292 #n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl293 qed.294 295 lemma ith_increment_carry : ∀n. ∀a : BitVector (S n).296 ith_carry … a (one_bv ?) false = andb_fold … a.297 #n elim n298 [ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl)299 cases hd normalize @refl300  2: #n' #Hind #a301 elim (BitVector_Sn … a) #hd * #tl #Heq >Heq302 lapply (Hind … tl) #Hind >one_bv_Sn303 >ith_carry_Sn whd in match (andb_fold ??);304 cases hd >Hind @refl305 ] qed.306 307 lemma ith_increment_bit : ∀n. ∀a : BitVector (S n).308 ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)).309 #n #a310 elim (BitVector_Sn … a) #hd * #tl #Heq >Heq311 whd in match (head' ???);312 a cases n in tl;313 [ 1: #tl >(BitVector_O … tl) cases hd normalize try //314  2: #n' #tl >one_bv_Sn >ith_bit_Sn315 >ith_increment_carry >tail_Sn316 cases hd try //317 ] qed.318 319 (* Lemma used to prove involutivity of twocomplement negation *)320 lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n).321 (andb_fold (S n) (negation_bv (S n) v) =322 andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))).323 #n elim n324 [ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl325  2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq326 lapply (Hind tl) Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn327 >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind328 cases hd normalize nodelta329 [ 1: >xorb_false >(xorb_comm false ?) >xorb_false330  2: >xorb_false >(xorb_comm true ?) >xorb_true ]331 >ith_increment_carry332 cases (andb_fold (S n') (negation_bv (S n') tl)) @refl333 ] qed.334 335 (* Test of the 'direct' approach: proof of the involutivity of twocomplement negation. *)336 lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v.337 #n elim n338 [ 1: #v >(BitVector_O v) @refl339  2: #n' cases n'340 [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq341 >(BitVector_O … tl) normalize cases hd @refl342  2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq343 lapply (Hind tl) Hind #Hind <Hind in ⊢ (???%);344 whd in match twocomp_neg_direct; normalize nodelta345 whd in match increment_direct; normalize nodelta346 >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??)347 >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn348 generalize in match (addition_n_direct (S n'')349 (negation_bv (S n'')350 (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false))351 (one_bv (S n'')) false); #tail352 >ith_increment_carry >ith_increment_carry353 cases hd normalize nodelta354 [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false355  2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ]356 <twocomp_neg_involutive_aux357 cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl358 ]359 ] qed.360 361 lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb.362 #n #a #b #va #vb #H destruct (H) @conj @refl qed.363 364 lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed.365 366 (* Injectivity of increment *)367 lemma increment_inj : ∀n. ∀a,b : BitVector n.368 increment_direct ? a = increment_direct ? b →369 a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false).370 #n whd in match increment_direct; normalize nodelta elim n371 [ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj //372  2: #n' cases n'373 [ 1: #_ #a #b374 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a375 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b376 >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b377 normalize #H @conj try //378  2: #n'' #Hind #a #b379 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a380 elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b381 lapply (Hind … tl_a tl_b) Hind #Hind382 >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn383 >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false384 #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2385 lapply (Hind Heq2) * #Heq3 #Heq4386 cut (hd_a = hd_b)387 [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b)388 * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm ? hd_b) #Heq6 >(Heq6 Heq5)389 @refl ]390 #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ]391 >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl392 ] qed.393 394 (* Inverse of injecivity of increment, does not lose information (cf increment_inj) *)395 lemma increment_inj_inv : ∀n. ∀a,b : BitVector n.396 a = b → increment_direct ? a = increment_direct ? b. // qed.397 398 (* A more general result. *)399 lemma addition_n_direct_inj : ∀n. ∀x,y,delta: BitVector n.400 addition_n_direct ? x delta false = addition_n_direct ? y delta false →401 x = y ∧ (ith_carry n x delta false = ith_carry n y delta false).402 #n elim n403 [ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * @conj @refl404  2: #n' #Hind #x #y #delta405 elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx406 elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy407 elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd408 >addition_n_direct_Sn >ith_bit_Sn409 >addition_n_direct_Sn >ith_bit_Sn410 >ith_carry_Sn >ith_carry_Sn411 lapply (Hind … tlx tly tld) Hind #Hind #Heq412 elim (bitvector_cons_inj_inv … Heq) #Heq_hd #Heq_tl413 lapply (Hind Heq_tl) Hind * #HindA #HindB414 >HindA >HindB >HindB in Heq_hd; #Heq_hd415 cut (hdx = hdy)416 [ 1: cases hdd in Heq_hd; cases (ith_carry n' tly tld false)417 cases hdx cases hdy normalize #H try @H try @refl418 >H try @refl ]419 #Heq_hd >Heq_hd @conj @refl420 ] qed.421 422 (* We also need it the other way around. *)423 lemma addition_n_direct_inj_inv : ∀n. ∀x,y,delta: BitVector n.424 x ≠ y → (* ∧ (ith_carry n x delta false = ith_carry n y delta false). *)425 addition_n_direct ? x delta false ≠ addition_n_direct ? y delta false.426 #n elim n427 [ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * #H @(False_ind … (H (refl ??)))428  2: #n' #Hind #x #y #delta429 elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx430 elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy431 elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd432 #Hneq433 cut (hdx ≠ hdy ∨ tlx ≠ tly)434 [ @(eq_bv_elim … tlx tly)435 [ #Heq_tl >Heq_tl >Heq_tl in Hneq;436 #Hneq cut (hdx ≠ hdy) [ % #Heq_hd >Heq_hd in Hneq; *437 #H @H @refl ]438 #H %1 @H439  #H %2 @H ] ]440 Hneq #Hneq441 >addition_n_direct_Sn >addition_n_direct_Sn442 >ith_bit_Sn >ith_bit_Sn cases Hneq443 [ 1: #Hneq_hd444 lapply (addition_n_direct_inj … tlx tly tld)445 @(eq_bv_elim … (addition_n_direct ? tlx tld false) (addition_n_direct ? tly tld false))446 [ 1: #Heq Hind #Hind elim (Hind Heq) #Heq_tl >Heq_tl #Heq_carry >Heq_carry447 % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) Habsurd448 lapply Hneq_hd449 cases hdx cases hdd cases hdy cases (ith_carry ? tly tld false)450 normalize in ⊢ (? → % → ?); #Hneq_hd #Heq_hd #_451 try @(absurd … Heq_hd Hneq_hd)452 elim Hneq_hd Hneq_hd #Hneq_hd @Hneq_hd453 try @refl try assumption try @(sym_eq … Heq_hd)454  2: #Htl_not_eq #_ % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_455 elim Htl_not_eq Htl_not_eq #HA #HB @HA @HB ]456  2: #Htl_not_eq lapply (Hind tlx tly tld Htl_not_eq) Hind #Hind457 % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_458 elim Hind Hind #HA #HB @HA @HB ]459 ] qed.460 461 lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed.462 463 lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n).464 ith_carry (S n) a (one_bv (S n)) false465 = ith_carry (S n) a (zero (S n)) true.466 #n elim n467 [ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl468  2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq469 lapply (Hind tl_a) #Hind470 >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl471 ] qed.472 473 lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false.474 #n elim n //475 #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn476 >ith_carry_Sn >(Hind tl) cases hd @refl.477 qed.478 479 lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n.480 addition_n_direct ? v (zero ?) false = v.481 #n elim n482 [ 1: #v >(BitVector_O … v) normalize @refl483  2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq484 lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn485 >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux486 >xorb_false @refl487 ] qed.488 489 lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true.490 #n elim n491 [ 1: #a >(BitVector_O … a) normalize @refl492  2: #n' cases n'493 [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl494  2: #n'' #Hind #a495 elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq496 lapply (Hind tl_a) Hind #Hind497 >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn498 >addition_n_direct_Sn >ith_bit_Sn499 >xorb_false >Hind @bitvector_cons_eq500 >increment_to_carry_aux @refl501 ]502 ] qed.503 504 lemma increment_to_carry : ∀n. ∀a,b : BitVector n.505 addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true.506 #n #a #b >increment_to_carry_zero <associative_addition_n_direct507 >neutral_addition_n_direct @refl508 qed.509 510 lemma increment_direct_ok : ∀n,v. increment_direct n v = increment n v.511 #n #v whd in match (increment ??);512 >addition_n_direct_ok <increment_to_carry_zero @refl513 qed.514 515 (* Prove (a + b) = a + b *)516 lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n.517 twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false.518 whd in match twocomp_neg_direct; normalize nodelta519 lapply increment_inj_inv520 whd in match increment_direct; normalize nodelta521 #H #n #a #b522 <associative_addition_n_direct @H523 >associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n))524 >increment_to_carry525 H lapply b lapply a b a526 cases n527 [ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl528  2: #n' #a #b529 cut (negation_bv ? (addition_n_direct ? a b false)530 = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧531 notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true))532 [ n lapply b lapply a elim n'533 [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a)534 elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b)535 cases hd_a cases hd_b normalize @conj @refl536  2: #n #Hind #a #b537 elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa538 elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb539 lapply (Hind tl_a tl_b) * #H1 #H2540 @conj541 [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn542 >carry_notb >H2 @refl543  1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn544 >negation_bv_Sn >negation_bv_Sn545 >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq546 >xorb_lneg >xorb_rneg >notb_notb547 <xorb_rneg >H2 @refl548 ]549 ] ]550 * #H1 #H2 @H1551 ] qed.552 553 lemma addition_n_direct_neg : ∀n. ∀a.554 (addition_n_direct n a (negation_bv n a) false) = replicate ?? true555 ∧ (ith_carry n a (negation_bv n a) false = false).556 #n elim n557 [ 1: #a >(BitVector_O … a) @conj @refl558  2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq559 lapply (Hind … tl) Hind * #HA #HB560 @conj561 [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl562  1: >negation_bv_Sn >addition_n_direct_Sn563 >ith_bit_Sn >HB >xorb_false >HA564 @bitvector_cons_eq elim hd @refl565 ]566 ] qed.567 568 (* a + a = 0 *)569 lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?).570 whd in match twocomp_neg_direct;571 whd in match increment_direct;572 normalize nodelta573 #n #a <associative_addition_n_direct574 elim (addition_n_direct_neg … a) #H #_ >H575 H a576 cases n try //577 #n'578 cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n')))579 ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true))580 [ elim n'581 [ 1: @conj @refl582  2: #n' * #HA #HB @conj583 [ 1: >replicate_Sn >one_bv_Sn >addition_n_direct_Sn584 >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl585  2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ]586 ]587 ] * #H1 #H2 @H1588 qed.589 590 (* Lift back the previous result to standard operations. *)591 lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v.592 #n #v whd in match twocomp_neg_direct; normalize nodelta593 whd in match increment_direct; normalize nodelta594 whd in match two_complement_negation; normalize nodelta595 >increment_to_addition_n <addition_n_direct_ok596 whd in match addition_n; normalize nodelta597 elim (add_with_carries ????) #a #b @refl598 qed.599 600 lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n.601 two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b).602 #n #a #b603 lapply (twocomp_neg_plus ? a b)604 >twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok605 <addition_n_direct_ok <addition_n_direct_ok606 whd in match addition_n; normalize nodelta607 elim (add_with_carries n a b false) #bits #flags normalize nodelta608 elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags'609 normalize nodelta #H @H610 qed.611 612 lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?).613 #n #a lapply (bitvector_opp_direct ? a)614 >twocomp_neg_direct_ok <addition_n_direct_ok615 whd in match (addition_n ???);616 elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H617 qed.618 619 lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a.620 #n #a621 lapply (neutral_addition_n_direct n a)622 <addition_n_direct_ok623 whd in match (addition_n ???);624 elim (add_with_carries n a (zero n) false) #bits #flags #H @H625 qed.626 627 lemma injective_addition_n : ∀n. ∀x,y,delta : BitVector n.628 addition_n ? x delta = addition_n ? y delta → x = y.629 #n #x #y #delta630 lapply (addition_n_direct_inj … x y delta)631 <addition_n_direct_ok <addition_n_direct_ok632 whd in match addition_n; normalize nodelta633 elim (add_with_carries n x delta false) #bitsx #flagsx634 elim (add_with_carries n y delta false) #bitsy #flagsy635 normalize #H1 #H2 elim (H1 H2) #Heq #_ @Heq636 qed.637 638 lemma injective_inv_addition_n : ∀n. ∀x,y,delta : BitVector n.639 x ≠ y → addition_n ? x delta ≠ addition_n ? y delta.640 #n #x #y #delta641 lapply (addition_n_direct_inj_inv … x y delta)642 <addition_n_direct_ok <addition_n_direct_ok643 whd in match addition_n; normalize nodelta644 elim (add_with_carries n x delta false) #bitsx #flagsx645 elim (add_with_carries n y delta false) #bitsy #flagsy646 normalize #H1 #H2 @(H1 H2)647 qed.648 10 649 11 … … 667 29 668 30 lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed. 31 32 (*  *) 33 (* Some shorthands for conversion functions from BitVectorZ. *) 34 (*  *) 35 36 definition Zoub ≝ Z_of_unsigned_bitvector. 37 definition boZ ≝ bitvector_of_Z. 38 39 (* Offsets are just bitvectors packed inside some useless and annoying constructor. *) 40 definition Zoo ≝ λx. Zoub ? (offv x). 41 definition boo ≝ λx. mk_offset (boZ ? x). 669 42 670 43 (*  *) … … 915 288 (* Frontend values. *) 916 289 inductive value_eq (E : embedding) : val → val → Prop ≝ 917  undef_eq : ∀v.918 value_eq E Vundef v290  undef_eq : 291 value_eq E Vundef Vundef 919 292  vint_eq : ∀sz,i. 920 293 value_eq E (Vint sz i) (Vint sz i) 921  vfloat_eq : ∀f.922 value_eq E (Vfloat f) (Vfloat f)923 294  vnull_eq : 924 295 value_eq E Vnull Vnull … … 944 315 load_value_of_type ty m1 b1 off1 = Some ? v1 → 945 316 (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2). 946 317 318 (* Adapted from Compcert's Memory *) 319 definition non_aliasing : embedding → mem → Prop ≝ 320 λE,m. 321 ∀b1,b2,b1',b2',delta1,delta2. 322 b1 ≠ b2 → 323 E b1 = Some ? 〈b1',delta1〉 → 324 E b2 = Some ? 〈b2',delta2〉 → 325 (b1' ≠ b2') ∨ 326 high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ 327 high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1). 328 947 329 (* Definition of a memory injection *) 948 record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0]≝330 record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Prop ≝ 949 331 { (* Load simulation *) 950 332 mi_inj : load_sim_ptr E m1 m2; … … 960 342 (* Regions are preserved *) 961 343 mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b'; 962 (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's. 963 * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where 964 * all variables are allocated in the same block. *) 965 mi_disjoint : ∀b1,b2,b1',b2',o1',o2'. 966 b1 ≠ b2 → 967 E b1 = Some ? 〈b1',o1'〉 → 968 E b2 = Some ? 〈b2',o2'〉 → 969 b1' ≠ b2' 970 }. 971 972 (* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\ 973 * A memory extension is a [memory_inj] with some particular blocks designated as 974 * being writeable. *) 975 976 alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)". 977 978 record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝ 979 { me_inj : memory_inj E m1 m2; 980 (* A list of blocks where we can write freely *) 981 me_writeable : list block; 982 (* These blocks are valid *) 983 me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b; 984 (* And pointers to m1 are oblivious to these blocks *) 985 me_writeable_ok : ∀p,p'. 986 valid_pointer m1 p = true → 987 pointer_translation p E = Some ? p' → 988 ¬ (meml ? (pblock p') me_writeable) 344 (* subblocks do not overlap (nonaliasing property) *) 345 mi_nonalias : non_aliasing E m1 989 346 }. 990 347 … … 996 353 ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2. 997 354 #E #p1 #v #Heq inversion Heq 998 [ 1: # v #Habsurd destruct (Habsurd)355 [ 1: #Habsurd destruct (Habsurd) 999 356  2: #sz #i #Habsurd destruct (Habsurd) 1000  3: #f #Habsurd destruct (Habsurd) 1001  4: #Habsurd destruct (Habsurd) 1002  5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct 357  3: #Habsurd destruct (Habsurd) 358  4: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct 1003 359 %{p2} @conj try @refl try assumption 1004 360 ] qed. … … 1007 363 lemma value_eq_inversion : 1008 364 ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 → 1009 ( ∀v. P Vundef v) →365 (P Vundef Vundef) → 1010 366 (∀sz,i. P (Vint sz i) (Vint sz i)) → 1011 (∀f. P (Vfloat f) (Vfloat f)) →1012 367 (P Vnull Vnull) → 1013 368 (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) → 1014 369 P v1 v2. 1015 #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5370 #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 1016 371 inversion Heq 1017 [ 1: # v #Hv1 #Hv2 #_ destruct @H1372 [ 1: #Hv1 #Hv2 #_ destruct @H1 1018 373  2: #sz #i #Hv1 #Hv2 #_ destruct @H2 1019  3: #f #Hv1 #Hv2 #_ destruct @H3 1020  4: #Hv1 #Hv2 #_ destruct @H4 1021  5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed. 1022 374  3: #Hv1 #Hv2 #_ destruct @H3 375  4: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H4 // ] qed. 376 1023 377 (* If we succeed to load something by value from a 〈b,off〉 location, 1024 378 [b] is a valid block. *) … … 1030 384 #ty #m * #brg #bid #off #v 1031 385 cases ty 1032 [ 1:  2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6:#domain #codomain1033  7: #structname #fieldspec  8: #unionname #fieldspec  9:#id ]386 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 387  #structname #fieldspec  #unionname #fieldspec  #id ] 1034 388 whd in match (load_value_of_type ????); 1035 [ 1, 7,8: #_ #Habsurd destruct (Habsurd) ]389 [ 1,6,7: #_ #Habsurd destruct (Habsurd) ] 1036 390 #Hmode 1037 [ 1,2, 3,6: [ 1: elim sz  2: elim fsz ]391 [ 1,2,5: [ 1: elim sz ] 1038 392 normalize in match (typesize ?); 1039 393 whd in match (loadn ???); … … 1054 408 #ty #m * #brg #bid #off #v 1055 409 cases ty 1056 [ 1:  2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6:#domain #codomain1057  7: #structname #fieldspec  8: #unionname #fieldspec  9:#id ]410 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 411  #structname #fieldspec  #unionname #fieldspec  #id ] 1058 412 whd in match (load_value_of_type ????); 1059 [ 1, 7,8: #_ #Habsurd destruct (Habsurd) ]413 [ 1,6,7: #_ #Habsurd destruct (Habsurd) ] 1060 414 #Hmode 1061 [ 1,2, 3,6: [ 1: elim sz  2: elim fsz]415 [ 1,2,5: [ 1: elim sz ] 1062 416 normalize in match (typesize ?); 1063 417 whd in match (loadn ???); … … 1073 427 ] qed. 1074 428 1075 1076 lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.1077 * #rg #id #m normalize1078 elim id /2/ qed.1079 1080 lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.1081 * #rg #id #m normalize1082 elim id /2/ qed.1083 1084 429 lemma load_by_value_success_valid_block : 1085 430 ∀ty,m,b,off,v. … … 1088 433 valid_block m b. 1089 434 #ty #m #b #off #v #Haccess_mode #Hload 1090 @ valid_block_from_bool435 @Zltb_true_to_Zlt 1091 436 elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * // 1092 437 qed. … … 1102 447 qed. 1103 448 1104 (* Making explicit the contents of memory_inj for load_value_of_type *) 449 (* Making explicit the contents of memory_inj for load_value_of_type. 450 * Equivalent to Lemma 59 of Leroy & Blazy *) 1105 451 lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty. 1106 452 memory_inj E m1 m2 → … … 1112 458 lapply (refl ? (access_mode ty)) 1113 459 cases ty 1114 [ 1:  2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6:#domain #codomain1115  7: #structname #fieldspec  8: #unionname #fieldspec  9:#id ]460 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 461  #structname #fieldspec  #unionname #fieldspec  #id ] 1116 462 normalize in ⊢ ((???%) → ?); #Hmode #Hyp 1117 [ 1, 7,8: normalize in Hyp; destruct (Hyp)1118  5,6: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]463 [ 1,6,7: normalize in Hyp; destruct (Hyp) 464  4,5: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ] 1119 465 lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer 1120 466 lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H 1121 qed. 467 qed. 1122 468 1123 469 (*  *) … … 1154 500 whd in Halloc:(??%?); destruct (Halloc) 1155 501 whd in match (beloadv ??) in ⊢ (??%%); 1156 lapply ( valid_block_to_bool… Hvalid) #Hlt502 lapply (Zlt_to_Zltb_true … Hvalid) #Hlt 1157 503 >Hlt >(zlt_succ … Hlt) 1158 504 normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??); 1159 505 cut (eqZb (block_id block) next = false) 1160 [ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 / ] #Hneq506 [ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq 1161 507 >Hneq cases (eq_region ??) normalize nodelta @refl 1162 508 qed. … … 1181 527 (* Memory allocation preserves [memory_inj] *) 1182 528 lemma alloc_memory_inj : 1183 ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2. 529 ∀E:embedding. 530 ∀m1,m2,m2',z1,z2,r,new_block. 531 ∀H:memory_inj E m1 m2. 1184 532 alloc m2 z1 z2 r = 〈m2', new_block〉 → 1185 533 memory_inj E m1 m2'. … … 1193 541 lapply (refl ? (access_mode ty)) 1194 542 cases ty in Hload_eq; 1195 [ 1:  2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6:#domain #codomain1196  7: #structname #fieldspec  8: #unionname #fieldspec  9:#id ]543 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 544  #structname #fieldspec  #unionname #fieldspec  #id ] 1197 545 #Hload normalize in ⊢ ((???%) → ?); #Haccess 1198 [ 1, 7,8: normalize in Hload; destruct (Hload)1199  2,3, 4,9: whd in match (load_value_of_type ????);546 [ 1,6,7: normalize in Hload; destruct (Hload) 547  2,3,8: whd in match (load_value_of_type ????); 1200 548 whd in match (load_value_of_type ????); 1201 549 lapply (load_by_value_success_valid_block … Haccess Hload) … … 1204 552 <(alloc_loadn_conservation … Halloc … Hvalid_block) 1205 553 @Hload 1206  5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]554  4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ] 1207 555  2: @(mi_freeblock … Hmemory_inj) 1208 556  3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans) … … 1221 569 cases (eq_region br' r) normalize #H @H 1222 570  4: @(mi_region … Hmemory_inj) 1223  5: @(mi_disjoint … Hmemory_inj) 1224 ] qed. 1225 1226 (* Memory allocation induces a memory extension. *) 1227 lemma alloc_memory_ext : 1228 ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2. 1229 alloc m2 z1 z2 r = 〈m2', new_block〉 → 1230 memory_ext E m1 m2'. 1231 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc 1232 lapply (alloc_memory_inj … Hmemory_inj Halloc) 1233 #Hinj' % 1234 [ 1: @Hinj' 1235  2: @[new_block] 1236  3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ] 1237 #Heq destruct (Heq) whd elim m2 in Halloc; 1238 #Hcontents #nextblock #Hnextblock 1239 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 1240 /2/ 1241  4: * #b #o * #b' #o' #Hvalid_ptr #Hembed % 1242 normalize in ⊢ (% → ?); * [ 2: #H @H ] 1243 #Heq destruct (Heq) 1244 lapply (mi_valid_pointers … Hmemory_inj … Hvalid_ptr Hembed) 1245 whd in ⊢ (% → ?); 1246 (* contradiction because ¬ (valid_block m2 new_block) *) 1247 elim m2 in Halloc; 1248 #contents_m2 #nextblock_m2 #Hnextblock_m2 1249 whd in ⊢ ((??%?) → ?); 1250 #Heq_alloc destruct (Heq_alloc) 1251 normalize 1252 lapply (irreflexive_Zlt nextblock_m2) 1253 @Zltb_elim_Type0 1254 [ #H * #Habsurd @(False_ind … (Habsurd H)) ] #_ #_ normalize #Habsurd destruct (Habsurd) 1255 ] qed. 571  5: @(mi_nonalias … Hmemory_inj) 572 qed. 573 574 (*  *) 575 (* Lemma 40 of the paper of Leroy & Blazy on the memory model 576 * and related lemmas *) 1256 577 1257 578 lemma bestorev_beloadv_conservation : … … 1300 621 #mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty 1301 622 cases ty 1302 [ 1:  2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 1303  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] try // 1304 [ 1: elim sz  2: elim fsz  3:  4: ] 623 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 624  #structname #fieldspec  #unionname #fieldspec  #id ] 625 // 626 [ 1: elim sz ] 1305 627 whd in ⊢ (??%%); 1306 628 >(bestorev_loadn_conservation … Hstore … Hneq) @refl 1307 629 qed. 1308 630 1309 (* Writing in the "extended" part of a memory preserves the underlying injection *) 1310 lemma bestorev_memory_ext_to_load_sim : 631 (* lift [bestorev_load_value_of_type_conservation] to storen *) 632 lemma storen_load_value_of_type_conservation : 633 ∀l,mA,mB,wb,wo. 634 storen mA (mk_pointer wb wo) l = Some ? mB → 635 ∀rb,ro. eq_block wb rb = false → 636 ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro. 637 #l elim l 638 [ 1: #mA #mB #wb #wo normalize #Heq destruct // 639  2: #hd #tl #Hind #mA #mB #wb #wo #Hstoren 640 cases (some_inversion ????? Hstoren) #mA' * #Hbestorev #Hstoren' 641 whd in match (shift_pointer ???) in Hstoren':(??%?); #rb #ro #Hneq_block #ty 642 lapply (Hind ???? Hstoren' … ro … Hneq_block ty) #Heq1 643 lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2 644 // 645 ] qed. 646 647 definition typesize' ≝ λty. typesize (typ_of_type ty). 648 649 lemma storen_load_value_of_type_conservation_in_block_high : 650 ∀E,mA,mB,mC,wo,l. 651 memory_inj E mA mB → 652 ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → 653 ∀b1,delta. E b1 = Some ? 〈blo,delta〉 → 654 high_bound mA b1 + Zoo delta < Zoo wo → 655 ∀ty,off. 656 Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 → 657 low_bound … mA b1 ≤ Zoo off → 658 Zoo off < high_bound … mA b1 → 659 load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) = 660 load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))). 661 #E #mA #mB #mC #wo #data #Hinj #blo #Hstoren #b1 #delta #Hembed #Hhigh #ty 662 (* need some stuff asserting that if a ptr is valid at the start of a write it's valid at the end. *) 663 cases data in Hstoren; 664 [ 1: normalize in ⊢ (% → ?); #Heq destruct // 665  2: #xd #data ] 666 #Hstoren 667 cases ty 668 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 669  #structname #fieldspec  #unionname #fieldspec  #id ]#off #Hofflt #Hlow_load #Hhigh_load try @refl 670 whd in match (load_value_of_type ????) in ⊢ (??%%); 671 [ 1: lapply (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hbefore #Hafter 672 lapply Hofflt Hofflt lapply Hlow_load Hlow_load lapply Hhigh_load Hhigh_load 673 lapply off off whd in match typesize'; normalize nodelta 674 generalize in match (typesize ?); #n elim n try // 675 #n' #Hind #o #Hhigh_load #Hlow_load #Hlt 676 whd in match (loadn ???) in ⊢ (??%%); 677 whd in match (beloadv ??) in ⊢ (??%%); 678 cases (valid_pointer_to_Prop … Hbefore) * #HltB_store #HlowB_store #HhighB_store 679 cases (valid_pointer_to_Prop … Hafter) * #HltC_store #HlowC_store #HhighC_store 680 >(Zlt_to_Zltb_true … HltB_store) >(Zlt_to_Zltb_true … HltC_store) normalize nodelta 681 cut (Zleb (low (blocks mB blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true) 682 [ 1: (* Notice that: 683 low mA b1 ≤ o < high mA b1 684 hence, since E b1 = 〈blo, delta〉 with delta >= 0 685 low mB blo ≤ (low mA b1 + delta) ≤ o+delta < (high mA b1 + delta) ≤ high mB blo *) 686 @cthulhu ] 687 #HA >HA >andb_lsimpl_true HA 688 cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mB blo)) = true) 689 [ 1: (* Same argument as above *) @cthulhu ] 690 #HA >HA normalize nodelta HA 691 cut (Zleb (low (blocks mC blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true) 692 [ 1: (* Notice that storen does not modify the bounds of a block. Related lemma present in [MemProperties]. 693 This cut follows from this lemma (which needs some info on the size of the data written, which we 694 have but must make explicit) and from the first cut. *) 695 @cthulhu ] 696 #HA >HA >andb_lsimpl_true HA 697 cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mC blo)) = true) 698 [ 1: (* Same argument as above *) @cthulhu ] 699 #HA >HA normalize nodelta HA 700 normalize in match (bitvector_of_nat ??); whd in match (shift_pointer ???); 701 whd in match (shift_offset ???); >commutative_addition_n >associative_addition_n 702 lapply (Hind (mk_offset (addition_n offset_size (sign_ext 2 ? [[false; true]]) (offv o))) ???) 703 [ 1: (* Provable from Hlt *) @cthulhu 704  2: (* Provable from Hlow_load, need to make a "succ" commute from bitvector to Z *) @cthulhu 705  3: (* Provable from Hlt, again *) @cthulhu ] 706 cases (loadn mB (mk_pointer blo 707 (mk_offset (addition_n ? (addition_n ? 708 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n') 709 normalize nodelta 710 cases (loadn mC (mk_pointer blo 711 (mk_offset (addition_n ? (addition_n ? 712 (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n') 713 normalize nodelta try // 714 [ 1,2: #l #Habsurd destruct ] 715 #l1 #l2 #Heq 716 cut (contents (blocks mB blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = 717 contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta)))) 718 [ 1: (* Follows from Hhigh, indirectly *) @cthulhu ] 719 #Hcontents_eq >Hcontents_eq whd in match (be_to_fe_value ??) in ⊢ (??%%); 720 cases (contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta)))) 721 normalize nodelta try // 722 (* Ok this is going to be more painful than what I thought. *) 723 @cthulhu 724  *: @cthulhu 725 ] qed. 726 727 lemma storen_load_value_of_type_conservation_in_block_low : 728 ∀E,mA,mB,mC,wo,l. 729 memory_inj E mA mB → 730 ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → 731 ∀b1,delta. E b1 = Some ? 〈blo,delta〉 → 732 Zoo wo < low_bound mA b1 + Zoo delta → 733 ∀ty,off. 734 Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 → 735 low_bound … mA b1 ≤ Zoo off → 736 Zoo off < high_bound … mA b1 → 737 load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) = 738 load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))). 739 @cthulhu 740 qed. 741 742 (* Writing in the "extended" part of a memory preserves the underlying injection. *) 743 lemma bestorev_memory_inj_to_load_sim : 1311 744 ∀E,mA,mB,mC. 1312 ∀Hext:memory_ext E mA mB. 1313 ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 1314 bestorev mB (mk_pointer wb wo) v = Some ? mC → 745 ∀Hext:memory_inj E mA mB. 746 ∀block2. ∀i : offset. ∀ty : type. 747 (∀block1,delta. 748 E block1 = Some ? 〈block2, delta〉 → 749 (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → 750 ∀v.store_value_of_type ty mB block2 i v = Some ? mC → 1315 751 load_sim_ptr E mA mC. 1316 #E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd 1317 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload 1318 (* Show that (wb ≠ b2) by showing b2 ∉ (me_writeable ...) *) 1319 lapply (me_writeable_ok … Hext (mk_pointer b1 off1) (mk_pointer b2 off2) Hvalid Hembed) #Hb2 1320 lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2 1321 cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false 1322 <(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false) 1323 @(mi_inj … (me_inj … Hext) … Hvalid … Hembed … Hload) 1324 qed. 1325 1326 (* Writing in the "extended" part of a memory preserves the whole memory injection *) 1327 lemma bestorev_memory_ext_to_memory_inj : 752 #E #mA #mB #mC #Hinj #block2 #i #storety 753 cases storety 754 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 755  #structname #fieldspec  #unionname #fieldspec  #id ]#Hout #storeval #Hstore whd 756 #b1 #off1 #b2 #off2 #ty #readval #Hvalid #Hptr_trans #Hload_value 757 whd in Hstore:(??%?); 758 [ 1,5,6,7,8: destruct ] 759 [ 1: 760 lapply (mi_inj … Hinj … Hvalid … Hptr_trans … Hload_value) 761 lapply Hload_value Hload_value 762 cases ty 763 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 764  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 765 #Hload_value 766 (* Prove that the contents of mB where v1 was were untouched. *) 767 * #readval' * #Hload_value2 #Hvalue_eq %{readval'} @conj try assumption 768 cases (some_inversion ????? Hptr_trans) * #b2' #delta' * #Hembed Hptr_trans normalize nodelta 769 #Heq destruct (Heq) 770 @(eq_block_elim … b2 block2) 771 [ 2,4,6,8: #Hblocks_neq <Hload_value2 @sym_eq @(storen_load_value_of_type_conservation … Hstore) 772 @not_eq_block @sym_neq @Hblocks_neq 773  1,3,5,7: #Heq destruct (Heq) lapply (Hout … Hembed) * 774 [ 1,3,5,7: #Hhigh <Hload_value2 Hload_value2 @sym_eq 775 lapply (load_by_value_success_valid_ptr_aux … Hload_value) // 776 * * #Hlt #Hlowb_off1 #Hhighb_off1 777 lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 Hlowb_off1 778 lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 Hhighb_off1 779 @(storen_load_value_of_type_conservation_in_block_high … Hinj … Hstore … Hembed) 780 try // 781 (* remaining stuff provable from Hload_value *) 782 @cthulhu 783  2,4,6,8: #Hlow <Hload_value2 Hload_value2 @sym_eq 784 lapply (load_by_value_success_valid_ptr_aux … Hload_value) // 785 * * #Hlt #Hlowb_off1 #Hhighb_off1 786 lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 Hlowb_off1 787 lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 Hhighb_off1 788 @(storen_load_value_of_type_conservation_in_block_low … Hinj … Hstore … Hembed) 789 try // 790 [ 1,3,5,7: (* deductible from Hlow + (sizeof ?) > 0 *) @cthulhu 791  2,4,6,8: (* deductible from Hload_value *) @cthulhu ] 792 ] 793 ] 794  *: (* exactly the same proof as above *) @cthulhu ] 795 qed. 796 797 (* Lift the above result to memory_inj 798 * This is Lemma 40 of Leroy & Blazy *) 799 lemma bestorev_memory_inj_to_memory_inj : 1328 800 ∀E,mA,mB,mC. 1329 ∀Hext:memory_ext E mA mB. 1330 ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 1331 bestorev mB (mk_pointer wb wo) v = Some ? mC → 801 ∀Hext:memory_inj E mA mB. 802 ∀block2. ∀i : offset. ∀ty : type. 803 (∀block1,delta. 804 E block1 = Some ? 〈block2, delta〉 → 805 (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → 806 ∀v.store_value_of_type ty mB block2 i v = Some ? mC → 1332 807 memory_inj E mA mC. 1333 #E #mA * #contentsB #nextblockB #HnextblockB #mC 1334 #Hext #wb #wo #v #Hwb #Hstore 1335 % 1336 [ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ] 1337 elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok 1338 #Hmem 1339 [ 1: @Hvalid  3: @Hregion  4: @Hdisjoint ] Hvalid Hregion Hdisjoint 1340 whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem) 1341 normalize in ⊢ (% → ?); #Hlt_wb 1342 #p #p' #HvalidA #Hembed lapply (Hcodomain … HvalidA Hembed) Hcodomain 1343 normalize in match (valid_pointer ??) in ⊢ (% → %); 1344 >(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta 1345 cases (Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector offset_size (offv wo)) 1346 ∧Zltb (Z_of_unsigned_bitvector offset_size (offv wo)) (high (contentsB wb))) 1347 normalize nodelta 1348 [ 2: #Habsurd destruct (Habsurd) ] 1349 #Heq destruct (Heq) 1350 cases (Zltb (block_id (pblock p')) nextblockB) normalize nodelta 1351 [ 2: #H @H ] 1352 whd in match (update_block ?????); 1353 cut (eq_block (pblock p') wb = false) 1354 [ 2: #Heq >Heq normalize nodelta #H @H ] 1355 @neq_block_eq_block_false @sym_neq 1356 @(mem_not_mem_neq writeable … Hmem) 1357 @(Hwriteable_ok … HvalidA Hembed) 1358 qed. 1359 1360 (* It even preserves memory extensions, with the same writeable blocks. *) 1361 lemma bestorev_memory_ext_to_memory_ext : 1362 ∀E,mA,mB. 1363 ∀Hext:memory_ext E mA mB. 1364 ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 1365 ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC → 1366 ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext). 1367 #E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore 1368 %{(mk_memory_ext … 1369 (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore) 1370 (me_writeable … Hext) 1371 ? 1372 (me_writeable_ok … Hext) 1373 )} try @refl 1374 #b #Hmemb 1375 lapply (me_writeable_valid … Hext b Hmemb) 1376 lapply (me_writeable_valid … Hext wb Hmem) 1377 elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid 1378 lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?); 1379 >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta 1380 cases (if Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector 16 (offv wo)) 1381 then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (contentsB wb)) 1382 else false) 1383 normalize [ 2: #Habsurd destruct (Habsurd) ] 1384 #Heq destruct (Heq) @Hb_valid 1385 qed. 1386 1387 (* Lift [bestorev_memory_ext_to_memory_ext] to storen *) 1388 lemma storen_memory_ext_to_memory_ext : 1389 ∀E,mA,l,mB,mC. 1390 ∀Hext:memory_ext E mA mB. 1391 ∀wb,wo. meml ? wb (me_writeable … Hext) → 1392 storen mB (mk_pointer wb wo) l = Some ? mC → 1393 memory_ext E mA mC. 1394 #E #mA #l elim l 1395 [ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq) 1396 @Hext 1397  2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem 1398 whd in ⊢ ((??%?) → ?); 1399 lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem) 1400 cases (bestorev mB (mk_pointer wb wo) hd) 1401 normalize nodelta 1402 [ 1: #H #Habsurd destruct (Habsurd) ] 1403 #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore 1404 @(Hind … HextD … Hstore) 1405 <Heq @Hmem 1406 ] qed. 1407 1408 (* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *) 1409 lemma store_value_of_type_memory_ext_to_memory_ext : 1410 ∀E,mA,mB,mC. 1411 ∀Hext:memory_ext E mA mB. 1412 ∀wb,wo. meml ? wb (me_writeable … Hext) → 1413 ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC → 1414 memory_ext E mA mC. 1415 #E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v 1416 cases ty 1417 [ 1:  2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 1418  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] 1419 whd in ⊢ ((??%?) → ?); 1420 [ 1,5,6,7,8: #Habsurd destruct (Habsurd) ] 1421 #Hstore 1422 @(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore) 1423 qed. 1424 1425 (* Commutation results of standard binary operations with value_eq. *) 808 #E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore % 809 lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try // 810 cases Hinj #Hsim' #Hnot_valid #Hvalid #Hregion #Hnonalias try assumption 811 #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid 812 cases ty in Hstore; 813 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 814  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 815 whd in ⊢ ((??%?) → ?); 816 [ 1,4,5,6,7: #Habsurd destruct ] 817 cases (fe_to_be_values ??) 818 [ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid Hvalid destruct @refl 819  *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_ 820 @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh 821 @conj try @conj try assumption >Hnext try // 822 cases (Hbounds (pblock p')) #HA #HB 823 whd in match (low_bound ??); whd in match (high_bound ??); 824 >HA >HB try assumption 825 ] qed. 826 827 (*  *) 828 (* Lemma 41 of the paper of Leroy & Blazy on the memory model 829 * and related lemmas *) 830 831 (* The backend might contain something similar to this lemma. *) 832 lemma be_to_fe_value_ptr : 833 ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)). 834 #b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta 835 cases br normalize nodelta >eqZb_z_z normalize nodelta 836 cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq 837 <(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl 838 * // 839 qed. 840 841 lemma value_eq_to_be_and_back_again : 842 ∀E,ty,v1,v2. 843 value_eq E v1 v2 → 844 ast_typ_consistent_with_value ty v1 → 845 ast_typ_consistent_with_value ty v2 → 846 value_eq E (be_to_fe_value ty (fe_to_be_values ty v1 )) (be_to_fe_value ty (fe_to_be_values ty v2)). 847 #E #ty #v1 #v2 #Hvalue_eq 848 @(value_eq_inversion … Hvalue_eq) try // 849 [ 1: cases ty // 850  2: #sz #i cases ty 851 [ 2: @False_ind 852  1: #sz' #sg #H whd in ⊢ (% → ?); #Heq 853 lapply (fe_to_be_to_fe_value … H) #H >H // ] 854  3: #p1 #p2 #Hembed cases ty 855 [ 1: #sz #sg @False_ind 856  2: #_ #_ 857 cases p1 in Hembed; #b1 #o1 858 cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H 859 cases (some_inversion ????? H) * #b3 #o3 * #Hembed 860 normalize nodelta #Heq >be_to_fe_value_ptr >be_to_fe_value_ptr 861 destruct %4 whd in match (pointer_translation ??); 862 >Hembed normalize nodelta @refl 863 ] 864 ] qed. 865 866 lemma storen_parallel_memory_exists : 867 ∀E,m1,m2,m1',b1,i,b2,delta,ty,v1,v2. 868 memory_inj E m1 m2 → 869 value_eq E v1 v2 → 870 storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' → 871 E b1 = Some ? 〈b2, delta〉 → 872 ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2'. 873 @cthulhu qed. 874 (* 875 #E #m1 #m2 #m1' #b1 #i #b2 #delta #ty #v1 #v2 #Hinj #Hvalue_eq 876 @(value_eq_inversion … Hvalue_eq) 877 [ 1: #v #Hstoren *) 878 879 880 lemma storen_parallel_aux : 881 ∀E,m1,m2. 882 ∀Hinj:memory_inj E m1 m2. 883 ∀v1,v2. value_eq E v1 v2 → 884 ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → 885 ∀ty,i,m1'. 886 ast_typ_consistent_with_value ty v1 → 887 ast_typ_consistent_with_value ty v2 → 888 storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' → 889 ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧ 890 memory_inj E m1' m2'. 891 #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hok1 #Hok2 892 #Hstoren lapply (storen_to_valid_pointer_fe_to_be … Hstoren) 893 * * * #Hblocks_eq1 #Hnextblock1 #Hvalid_m1 #Hvalid_m1' 894 lapply (mi_valid_pointers … Hinj … (mk_pointer b1 i) (mk_pointer b2 (offset_plus i delta)) Hvalid_m1 ?) 895 [ 1: whd in ⊢ (??%%); >Hembed @refl ] 896 #Hvalid_m2 897 cases (valid_pointer_to_Prop … Hvalid_m2) * #Hnextblock2 #Hlow2 #Hhigh2 898 @cthulhu 899 qed. 900 901 lemma foo : 902 ∀E,m1,m2. 903 ∀Hinj:memory_inj E m1 m2. 904 ∀v1,v2. value_eq E v1 v2 → 905 ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → 906 ∀ty,i,m1'. store_value_of_type ty m1 b1 i v1 = Some ? m1' → 907 ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧ 908 memory_inj E m1' m2'. 909 #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hstore 910 @cthulhu qed. 911 912 (*  *) 913 (* Commutation results of standard unary and binary operations with value_eq. *) 914 1426 915 lemma unary_operation_value_eq : 1427 916 ∀E,op,v1,v2,ty. … … 1432 921 #E #op #v1 #v2 #ty #Hvalue_eq #r1 1433 922 inversion Hvalue_eq 1434 [ 1: #v #Hv1 #Hv2 #_destruct923 [ 1: #v #Hv1 #Hv2 destruct 1435 924 cases op normalize 1436 [ 1: cases ty [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9:#ty ]925 [ 1: cases ty [  #sz #sg  #ty  #ty #n  #tl #ty  #id #fl  #id #fl  #ty ] 1437 926 normalize #Habsurd destruct (Habsurd) 1438  3: cases ty [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9:#ty ]927  3: cases ty [  #sz #sg  #ty  #ty #n  #tl #ty  #id #fl  #id #fl  #ty ] 1439 928 normalize #Habsurd destruct (Habsurd) 1440 929  2: #Habsurd destruct (Habsurd) ] 1441 930  2: #vsz #i #Hv1 #Hv2 #_ 1442 931 cases op 1443 [ 1: cases ty 1444 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 932 [ 1: cases ty [  #sz #sg  #ty  #ty #n  #tl #ty  #id #fl  #id #fl  #ty ] 1445 933 whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???); 1446 934 [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct … … 1452 940 #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj // 1453 941  3: whd in match (sem_unary_operation ???); 1454 cases ty 1455 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 942 cases ty [  #sz #sg  #ty  #ty #n  #tl #ty  #id #fl  #id #fl  #ty ] 1456 943 normalize nodelta 1457 944 whd in ⊢ ((??%?) → ?); … … 1459 946 %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj // 1460 947  *: #Habsurd destruct (Habsurd) ] ] 1461  3: # f #Hv1 #Hv2 #_ destruct whd in match (sem_unary_operation ???);948  3: #Hv1 #Hv2 #_ destruct whd in match (sem_unary_operation ???); 1462 949 cases op normalize nodelta 1463 [ 1: cases ty 1464 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 1465 whd in match (sem_notbool ??); 1466 #Heq1 destruct 1467 cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/ 1468  2: normalize #Habsurd destruct (Habsurd) 1469  3: cases ty 1470 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 1471 whd in match (sem_neg ??); 1472 #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ] 1473  4: #Hv1 #Hv2 #_ destruct whd in match (sem_unary_operation ???); 1474 cases op normalize nodelta 1475 [ 1: cases ty 1476 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 950 [ 1: cases ty [  #sz #sg  #ty  #ty #n  #tl #ty  #id #fl  #id #fl  #ty ] 1477 951 whd in match (sem_notbool ??); 1478 952 #Heq1 destruct /3 by ex_intro, vint_eq, conj/ 1479 953  2: normalize #Habsurd destruct (Habsurd) 1480  3: cases ty 1481 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 954  3: cases ty [  #sz #sg  #ty  #ty #n  #tl #ty  #id #fl  #id #fl  #ty ] 1482 955 whd in match (sem_neg ??); 1483 956 #Heq1 destruct ] 1484  5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_ whd in match (sem_unary_operation ???);957  4: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_ whd in match (sem_unary_operation ???); 1485 958 cases op normalize nodelta 1486 [ 1: cases ty 1487 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 959 [ 1: cases ty [  #sz #sg  #ty  #ty #n  #tl #ty  #id #fl  #id #fl  #ty ] 1488 960 whd in match (sem_notbool ??); 1489 961 #Heq1 destruct /3 by ex_intro, vint_eq, conj/ 1490 962  2: normalize #Habsurd destruct (Habsurd) 1491  3: cases ty 1492 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 963  3: cases ty [  #sz #sg  #ty  #ty #n  #tl #ty  #id #fl  #id #fl  #ty ] 1493 964 whd in match (sem_neg ??); 1494 965 #Heq1 destruct ] … … 1506 977 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 1507 978 @(value_eq_inversion E … Hvalue_eq1) 1508 [ 1: #v  2: #sz #i  3: #f  4:  5: #p1 #p2 #Hembed ]979 [ 1:  2: #sz #i  3:  4: #p1 #p2 #Hembed ] 1509 980 [ 1: whd in match (sem_add ????); normalize nodelta 1510 981 cases (classify_add ty1 ty2) normalize nodelta 1511 [ 1: #sz #sg  2: # fsz  3: #n #ty #sz #sg  4: #n #sz #sg #ty  5: #ty1' #ty2' ]982 [ 1: #sz #sg  2: #n #ty #sz #sg  3: #n #sz #sg #ty  4: #ty1' #ty2' ] 1512 983 #Habsurd destruct (Habsurd) 1513 984  2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 1514 cases (classify_add ty1 ty2) normalize nodelta 1515 [ 1: #tsz #tsg  2: #t fsz  3: #tn #ty #tsz #tsg  4: #tn #tsz #tsg #ty  5: #ty1' #ty2' ]1516 [ 2, 3,5: #Habsurd destruct (Habsurd) ]985 cases (classify_add ty1 ty2) normalize nodelta 986 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] 987 [ 2,4: #Habsurd destruct (Habsurd) ] 1517 988 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1518 [ 1, 6: #v'  2,7: #sz' #i'  3,8: #f'  4,9:  5,10: #p1' #p2' #Hembed' ]1519 [ 1,2,4,5, 6,7,9: #Habsurd destruct (Habsurd) ]989 [ 1,5:  2,6: #sz' #i'  3,7:  4,8: #p1' #p2' #Hembed' ] 990 [ 1,2,4,5,7: #Habsurd destruct (Habsurd) ] 1520 991 [ 1: @intsize_eq_elim_elim 1521 992 [ 1: #_ #Habsurd destruct (Habsurd) … … 1541 1012 #Heq >Heq @refl ] 1542 1013 ] 1014 (*  3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 1015 cases (classify_add ty1 ty2) normalize nodelta 1016 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] 1017 [ 1,3,4: #Habsurd destruct (Habsurd) ] 1018 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1019 [ 1:  2: #sz' #i' 3:  4: #p1' #p2' #Hembed' ] 1020 [ 1,3,4,5,7: #Habsurd destruct (Habsurd) ] 1021 #Heq >Heq %{r1} @conj // 1022 /3 by ex_intro, conj, vfloat_eq/ *) 1543 1023  3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 1544 cases (classify_add ty1 ty2) normalize nodelta 1545 [ 1: #tsz #tsg  2: #tfsz  3: #tn #ty #tsz #tsg  4: #tn #tsz #tsg #ty  5: #ty1' #ty2' ] 1024 cases (classify_add ty1 ty2) normalize nodelta 1025 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] 1026 [ 1,3,4: #Habsurd destruct (Habsurd) ] 1027 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1028 [ 1:  2: #sz' #i'  3:  4: #p1' #p2' #Hembed' ] 1546 1029 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 1547 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1548 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5: #p1' #p2' #Hembed' ] 1549 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 1550 #Heq destruct (Heq) 1551 /3 by ex_intro, conj, vfloat_eq/ 1552  4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 1553 cases (classify_add ty1 ty2) normalize nodelta 1554 [ 1: #tsz #tsg  2: #tfsz  3: #tn #ty #tsz #tsg  4: #tn #tsz #tsg #ty  5: #ty1' #ty2' ] 1555 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 1556 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1557 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5: #p1' #p2' #Hembed' ] 1558 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 1559 @eq_bv_elim 1030 @eq_bv_elim 1560 1031 [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ 1561 1032  2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 1562  5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta1033  4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta 1563 1034 cases (classify_add ty1 ty2) normalize nodelta 1564 [ 1: #tsz #tsg  2: #t fsz  3: #tn #ty #tsz #tsg  4: #tn #tsz #tsg #ty  5: #ty1' #ty2' ]1565 [ 1, 2,4,5: #Habsurd destruct (Habsurd) ]1035 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] 1036 [ 1,3,4: #Habsurd destruct (Habsurd) ] 1566 1037 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1567 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5: #p1' #p2' #Hembed' ]1038 [ 1:  2: #sz' #i'  3:  4: #p1' #p2' #Hembed' ] 1568 1039 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 1569 1040 #Heq destruct (Heq) … … 1618 1089 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 1619 1090 @(value_eq_inversion E … Hvalue_eq1) 1620 [ 1: #v  2: #sz #i  3: #f  4:  5: #p1 #p2 #Hembed ]1091 [  #sz #i  3:  4: #p1 #p2 #Hembed ] 1621 1092 [ 1: whd in match (sem_sub ????); normalize nodelta 1622 1093 cases (classify_sub ty1 ty2) normalize nodelta 1623 [ 1: #sz #sg  2: #fsz  3: #n #ty #sz #sg  4: #n #sz #sg #ty  5:#ty1' #ty2' ]1094 [ #sz #sg  #n #ty #sz #sg  #n #sz #sg #ty #ty1' #ty2' ] 1624 1095 #Habsurd destruct (Habsurd) 1625 1096  2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 1626 1097 cases (classify_sub ty1 ty2) normalize nodelta 1627 [ 1: #tsz #tsg  2: #t fsz  3: #tn #ty #tsz #tsg  4: #tn #tsz #tsg #ty  5: #ty1' #ty2' ]1628 [ 2,3, 5: #Habsurd destruct (Habsurd) ]1098 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] 1099 [ 2,3,4: #Habsurd destruct (Habsurd) ] 1629 1100 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1630 [ 1,6: #v'  2,7: #sz' #i'  3,8: #f'  4,9:  5,10:#p1' #p2' #Hembed' ]1631 [ 1, 2,4,5,6,7,8,9,10: #Habsurd destruct (Habsurd) ]1101 [  #sz' #i'   #p1' #p2' #Hembed' ] 1102 [ 1,3,4: #Habsurd destruct (Habsurd) ] 1632 1103 @intsize_eq_elim_elim 1633 1104 [ 1: #_ #Habsurd destruct (Habsurd) … … 1636 1107 /3 by ex_intro, conj, vint_eq/ 1637 1108 ] 1638  3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta1639 cases (classify_sub ty1 ty2) normalize nodelta 1640 [ 1: #tsz #tsg  2: #t fsz  3: #tn #ty #tsz #tsg  4: #tn #tsz #tsg #ty  5: #ty1' #ty2' ]1641 [ 1, 3,4,5: #Habsurd destruct (Habsurd) ]1109 (* 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 1110 cases (classify_sub ty1 ty2) normalize nodelta 1111 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] 1112 [ 1,4: #Habsurd destruct (Habsurd) ] 1642 1113 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1643 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5:#p1' #p2' #Hembed' ]1114 [  #sz' #i'   #p1' #p2' #Hembed' ] 1644 1115 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 1645 1116 #Heq destruct (Heq) 1646 /3 by ex_intro, conj, vfloat_eq/ 1647  4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta1117 /3 by ex_intro, conj, vfloat_eq/ *) 1118  3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 1648 1119 cases (classify_sub ty1 ty2) normalize nodelta 1649 [ 1: #tsz #tsg  2: #t fsz  3: #tn #ty #tsz #tsg  4: #tn #tsz #tsg #ty  5: #ty1' #ty2' ]1650 [ 1, 2,5: #Habsurd destruct (Habsurd) ]1120 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] 1121 [ 1,4: #Habsurd destruct (Habsurd) ] 1651 1122 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1652 [ 1, 6: #v'  2,7: #sz' #i'  3,8: #f'  4,9:  5,10: #p1' #p2' #Hembed' ]1653 [ 1,2,4,5, 6,7,9,10: #Habsurd destruct (Habsurd) ]1123 [ 1,5:  2,6: #sz' #i'  3,7:  4,8: #p1' #p2' #Hembed' ] 1124 [ 1,2,4,5,7,8: #Habsurd destruct (Habsurd) ] 1654 1125 [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ 1655 1126  2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 1656 1127  2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ] 1657  5: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta1128  4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 1658 1129 cases (classify_sub ty1 ty2) normalize nodelta 1659 [ 1: #tsz #tsg  2: #t fsz  3: #tn #ty #tsz #tsg  4: #tn #tsz #tsg #ty  5: #ty1' #ty2' ]1660 [ 1, 2,5: #Habsurd destruct (Habsurd) ]1130 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] 1131 [ 1,4: #Habsurd destruct (Habsurd) ] 1661 1132 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1662 [ 1, 6: #v'  2,7: #sz' #i'  3,8: #f'  4,9:  5,10: #p1' #p2' #Hembed' ]1663 [ 1,2,4,5,6,7 ,8,9: #Habsurd destruct (Habsurd) ]1133 [ 1,5:  2,6: #sz' #i'  3,7:  4,8: #p1' #p2' #Hembed' ] 1134 [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ] 1664 1135 #Heq destruct (Heq) 1665 1136 [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl … … 1707 1178 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 1708 1179 @(value_eq_inversion E … Hvalue_eq1) 1709 [ 1: #v  2: #sz #i  3: #f  4:  5: #p1 #p2 #Hembed ]1180 [  #sz #i  3:  4: #p1 #p2 #Hembed ] 1710 1181 [ 1: whd in match (sem_mul ????); normalize nodelta 1711 1182 cases (classify_aop ty1 ty2) normalize nodelta 1712 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1183 [ 1: #sz #sg  2: #ty1' #ty2' ] 1713 1184 #Habsurd destruct (Habsurd) 1714 1185  2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 1715 1186 cases (classify_aop ty1 ty2) normalize nodelta 1716 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1717 [ 2 ,3: #Habsurd destruct (Habsurd) ]1187 [ 1: #sz #sg  2: #ty1' #ty2' ] 1188 [ 2: #Habsurd destruct (Habsurd) ] 1718 1189 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1719 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5:#p1' #p2' #Hembed' ]1720 [ 1,3,4 ,5: #Habsurd destruct (Habsurd) ]1190 [  #sz' #i'   #p1' #p2' #Hembed' ] 1191 [ 1,3,4: #Habsurd destruct (Habsurd) ] 1721 1192 @intsize_eq_elim_elim 1722 1193 [ 1: #_ #Habsurd destruct (Habsurd) … … 1727 1198  3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 1728 1199 cases (classify_aop ty1 ty2) normalize nodelta 1729 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ] 1730 [ 1,3: #Habsurd destruct (Habsurd) ] 1731 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1732 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5: #p1' #p2' #Hembed' ] 1733 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 1734 #Heq destruct (Heq) 1735 /3 by ex_intro, conj, vfloat_eq/ 1200 [ 1: #sz #sg  2: #ty1' #ty2' ] 1201 [ 1,2: #Habsurd destruct (Habsurd) ] 1736 1202  4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 1737 1203 cases (classify_aop ty1 ty2) normalize nodelta 1738 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1204 [ 1: #sz #sg  2: #ty1' #ty2' ] 1739 1205 #Habsurd destruct (Habsurd) 1740  5: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 1741 cases (classify_aop ty1 ty2) normalize nodelta 1742 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ] 1743 #Habsurd destruct (Habsurd) 1744 ] qed. 1206 ] qed. 1745 1207 1746 1208 lemma div_value_eq : … … 1752 1214 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 1753 1215 @(value_eq_inversion E … Hvalue_eq1) 1754 [ 1: #v  2: #sz #i  3: #f  4:  5: #p1 #p2 #Hembed ]1216 [  #sz #i  3:  4: #p1 #p2 #Hembed ] 1755 1217 [ 1: whd in match (sem_div ????); normalize nodelta 1756 1218 cases (classify_aop ty1 ty2) normalize nodelta 1757 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1219 [ 1: #sz #sg  2: #ty1' #ty2' ] 1758 1220 #Habsurd destruct (Habsurd) 1759 1221  2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 1760 1222 cases (classify_aop ty1 ty2) normalize nodelta 1761 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1762 [ 2 ,3: #Habsurd destruct (Habsurd) ]1223 [ 1: #sz #sg  2: #ty1' #ty2' ] 1224 [ 2: #Habsurd destruct (Habsurd) ] 1763 1225 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1764 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5:#p1' #p2' #Hembed' ]1765 [ 1,3,4 ,5: #Habsurd destruct (Habsurd) ]1226 [  #sz' #i'   #p1' #p2' #Hembed' ] 1227 [ 1,3,4: #Habsurd destruct (Habsurd) ] 1766 1228 elim sg normalize nodelta 1767 1229 @intsize_eq_elim_elim … … 1785 1247  3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 1786 1248 cases (classify_aop ty1 ty2) normalize nodelta 1787 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ] 1788 [ 1,3: #Habsurd destruct (Habsurd) ] 1789 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1790 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5: #p1' #p2' #Hembed' ] 1791 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 1792 #Heq destruct (Heq) 1793 /3 by ex_intro, conj, vfloat_eq/ 1249 [ 1: #sz #sg  2: #ty1' #ty2' ] 1250 [ 1,2: #Habsurd destruct (Habsurd) ] 1794 1251  4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 1795 1252 cases (classify_aop ty1 ty2) normalize nodelta 1796 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1253 [ 1: #sz #sg  2: #ty1' #ty2' ] 1797 1254 #Habsurd destruct (Habsurd) 1798  5: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 1799 cases (classify_aop ty1 ty2) normalize nodelta 1800 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ] 1801 #Habsurd destruct (Habsurd) 1802 ] qed. 1255 ] qed. 1803 1256 1804 1257 lemma mod_value_eq : … … 1810 1263 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 1811 1264 @(value_eq_inversion E … Hvalue_eq1) 1812 [ 1: #v  2: #sz #i  3: #f  4:  5: #p1 #p2 #Hembed ]1265 [  #sz #i  3:  4: #p1 #p2 #Hembed ] 1813 1266 [ 1: whd in match (sem_mod ????); normalize nodelta 1814 1267 cases (classify_aop ty1 ty2) normalize nodelta 1815 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1268 [ 1: #sz #sg  2: #ty1' #ty2' ] 1816 1269 #Habsurd destruct (Habsurd) 1817 1270  2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 1818 1271 cases (classify_aop ty1 ty2) normalize nodelta 1819 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1820 [ 2 ,3: #Habsurd destruct (Habsurd) ]1272 [ 1: #sz #sg  2: #ty1' #ty2' ] 1273 [ 2: #Habsurd destruct (Habsurd) ] 1821 1274 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1822 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5:#p1' #p2' #Hembed' ]1823 [ 1,3,4 ,5: #Habsurd destruct (Habsurd) ]1275 [  #sz' #i'   #p1' #p2' #Hembed' ] 1276 [ 1,3,4: #Habsurd destruct (Habsurd) ] 1824 1277 elim sg normalize nodelta 1825 1278 @intsize_eq_elim_elim … … 1839 1292 #H destruct (H) 1840 1293 /3 by ex_intro, conj, vint_eq/ ] 1841 ] 1842  3: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 1843 cases (classify_aop ty1 ty2) normalize nodelta 1844 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ] 1845 #Habsurd destruct (Habsurd) 1846  4: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 1847 cases (classify_aop ty1 ty2) normalize nodelta 1848 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ] 1849 #Habsurd destruct (Habsurd) 1850  5: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 1851 cases (classify_aop ty1 ty2) normalize nodelta 1852 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ] 1853 #Habsurd destruct (Habsurd) 1294 ] 1295  *: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 1296 cases (classify_aop ty1 ty2) normalize nodelta #foo #bar #Habsurd destruct (Habsurd) 1854 1297 ] qed. 1855 1298 … … 1929 1372 #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 1930 1373 @(value_eq_inversion E … Hvalue_eq1) 1931 [ 1: #v  2: #sz #i  3: #f  4:  5: #p1 #p2 #Hembed ]1374 [  #sz #i  3:  4: #p1 #p2 #Hembed ] 1932 1375 [ 2: 1933 1376 @(value_eq_inversion E … Hvalue_eq2) 1934 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5:#p1' #p2' #Hembed' ]1377 [  #sz' #i'   #p1' #p2' #Hembed' ] 1935 1378 [ 2: whd in match (sem_shl ??); 1936 1379 cases (lt_u ???) normalize nodelta … … 1950 1393 #E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1 1951 1394 @(value_eq_inversion E … Hvalue_eq1) 1952 [ 1: #v  2: #sz #i  3: #f  4:  5: #p1 #p2 #Hembed ]1395 [  #sz #i  3:  4: #p1 #p2 #Hembed ] 1953 1396 whd in match (sem_shr ????); whd in match (sem_shr ????); 1954 1397 [ 1: cases (classify_aop ty ty') normalize nodelta 1955 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1398 [ 1: #sz #sg  2: #ty1' #ty2' ] 1956 1399 #Habsurd destruct (Habsurd) 1957 1400  2: cases (classify_aop ty ty') normalize nodelta 1958 [ 1: #sz #sg  2: # fsz  3: #ty1' #ty2' ]1959 [ 2 ,3: #Habsurd destruct (Habsurd) ]1401 [ 1: #sz #sg  2: #ty1' #ty2' ] 1402 [ 2: #Habsurd destruct (Habsurd) ] 1960 1403 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1961 [ 1: #v'  2: #sz' #i'  3: #f'  4:  5:#p1' #p2' #Hembed' ]1962 [ 1,3,4 ,5: #Habsurd destruct (Habsurd) ]1404 [  #sz' #i'   #p1' #p2' #Hembed' ] 1405 [ 1,3,4: #Habsurd destruct (Habsurd) ] 1963 1406 elim sg normalize nodelta 1964 1407 cases (lt_u ???) normalize nodelta #Heq destruct (Heq) 1965 1408 /3 by ex_intro, conj, refl, vint_eq/ 1966  3: cases (classify_aop ty ty') normalize nodelta1967 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ]1409  *: cases (classify_aop ty ty') normalize nodelta 1410 #foo #bar 1968 1411 #Habsurd destruct (Habsurd) 1969  4: cases (classify_aop ty ty') normalize nodelta 1970 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ] 1971 #Habsurd destruct (Habsurd) 1972  5: cases (classify_aop ty ty') normalize nodelta 1973 [ 1: #sz #sg  2: #fsz  3: #ty1' #ty2' ] 1974 #Habsurd destruct (Habsurd) 1975 ] qed. 1412 ] qed. 1976 1413 1977 1414 lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
Note: See TracChangeset
for help on using the changeset viewer.