Changeset 1970
 Timestamp:
 May 18, 2012, 9:18:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r1873 r1970 1 1 include "Clight/Csyntax.ma". 2 2 include "Clight/TypeComparison.ma". 3 4 (* IG: used to prove preservation of the semantics. *) 5 include "Clight/Cexec.ma". 6 include "Clight/casts.ma". 7 8 (* include "ASM/AssemblyProof.ma". *) (* I had to manually copy some of the lemmas in this file, including an axiom ... *) 3 9 4 10 (* Attempt to remove unnecessary integer casts in Clight programs. … … 14 20 *) 15 21 22 23 16 24 (* Attempt to squeeze integer constant into a given type. 17 25 18 26 This might be too conservative  if we're going to cast it anyway, can't 19 27 I just ignore the fact that the integer doesn't fit? 20 *) 21 28 *) 29 30 (* [reduce_bits n m exp v] takes avector of size n + m + 1 and returns (if all goes well) a vector of size 31 * m+1 (an empty vector of bits makes no sense). It proceeds by removing /all/ the [n] leading bits equal 32 * to [exp]. If it fails, it returns None. *) 22 33 let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝ 23 34 match n return λn. BitVector (n+S m) → option (BitVector (S m)) with … … 26 37 ] v. 27 38 39 lemma reduce_bits_ok : ∀n,m.∀exp.∀v,v'. reduce_bits (S n) m exp v = Some ? v'→ reduce_bits n m exp (tail ?? v) = Some ? v'. 40 #n #m #exp #v #v' #H whd in H:(??%?); lapply H H 41 cases (eq_b ? exp) 42 [ 1: #H whd in H:(??%?); // 43  2: #H normalize in H; destruct ] qed. 44 45 lemma reduce_bits_trunc : ∀n,m.∀exp.∀v:(BitVector (plus n (S m))).∀v'. 46 reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v. 47 #n #m elim n 48 [ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >split_O_n // 49  2: #n' #Hind #exp #v #v' #H >truncate_tail 50 > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed. 51 52 lemma reduce_bits_dec : ∀n,m.∀exp.∀v. (∃v'.reduce_bits n m exp v = Some ? v') ∨ reduce_bits n m exp v = None ?. 53 #n #m #exp #v elim (reduce_bits n m exp v) 54 [ 1: %2 // 55  2: #v' %1 @(ex_intro … v') // ] qed. 56 57 (* pred_bitsize_of_intsize I32 = 31, … *) 28 58 definition pred_bitsize_of_intsize : intsize → nat ≝ 29 59 λsz. pred (bitsize_of_intsize sz). … … 32 62 λsg. match sg with [ Unsigned ⇒ false  Signed ⇒ true ]. 33 63 64 (* [simplify_int sz sz' sg sg' i] tries to convert an integer [i] of width [sz] and signedness [sg] 65 * into an integer of size [sz'] of signedness [sg']. 66 *  It first proceeds by comparing the source and target width: if the target width is strictly superior 67 * to the source width, the conversion fails. 68 *  If the size is equal, the argument is returned asis. 69 *  If the target type is strictly smaller than the source, it tries to squeeze the integer to 70 * the desired size. 71 *) 34 72 let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝ 35 73 let bit ≝ signed sg ∧ head' … i in 74 (* [nat_compare] does more than an innocent postdoc might think. It also computes the difference between the two args. 75 * if x < y, nat_compare x y = lt(x, y(x+1)) 76 * if x = y, nat_compare x y = eq x 77 * if x > y, nat_compare x y = gt(x(y+1), y) *) 36 78 match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz') 37 79 return λn,m,x.BitVector (S n) → option (BitVector (S m)) with 38 80 [ nat_lt _ _ ⇒ λi. None ? (* refuse to make constants larger *) 39 81  nat_eq _ ⇒ λi. Some ? i 40  nat_gt x y ⇒ λi. 82  nat_gt x y ⇒ λi. 83 (* Here, we have [x]=31([y]+1) and [y] ∈ {15; 7} OR [x] = 15(7+1) and [y] = 7. I.e.: x=15,y=15 or x=23,y=7 or x=7,y=7. 84 * In [reduce_bits n m bit i], [i] is supposed to have type BitVector n + (S m). Since its type is here (S x) + (S y), 85 * we deduce that the actual arguments of [reduce_bits] are (S x) and (S y), which is consistent. 86 * If [i] is of signed type and if it is negative, then it tries to remove the (S x) first "1" bits. 87 * Otherwise, it tries to remove the (S x) first "0" bits. 88 *) 41 89 match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with 42 [ Some i' ⇒ if signed sg' then if eq_b bit (head' … i') then Some ? i' else None ? else Some ? i' 90 [ Some i' ⇒ 91 if signed sg' then 92 if eq_b bit (head' … i') then 93 Some ? i' 94 else None ? 95 else Some ? i' 43 96  None ⇒ None ? 44 97 ] … … 47 100 qed. 48 101 49 (* Compare integer types to decide if we can omit casts. *) 50 51 inductive inttype_cmp : Type[0] ≝ 52  itc_le : inttype_cmp 53  itc_no : inttype_cmp. 54 55 definition inttype_compare ≝ 56 λt1,t2. 57 match t1 with 58 [ Tint sz sg ⇒ 59 match t2 with 60 [ Tint sz' sg' ⇒ 61 match sz with 62 [ I8 ⇒ itc_le 63  I16 ⇒ match sz' with [ I8 ⇒ itc_no  _ ⇒ itc_le ] 64  I32 ⇒ match sz' with [ I32 ⇒ itc_le  _ ⇒ itc_no ] 102 103 (* /!\ This lemma uses the "uniqueness of identity proofs" K axiom. I've tried doing a proper 104 * induction on t but it turns out to be a nonwellfounded pandora box. /!\ *) 105 lemma type_eq_dec_identity : ∀t. type_eq_dec t t = inl ?? (refl ? t). 106 #t elim (type_eq_dec t t) 107 [ 1: @streicherK // 108  2: #H elim H #Hcontr elim (Hcontr (refl ? t)) ] qed. 109 110 111 lemma sign_eq_dec : ∀s1,s2:signedness. (s1 = s2) ∨ (s1 ≠ s2). 112 * * /2/ %2 % #H destruct 113 qed. 114 115 lemma eq_intsize_identity : ∀id. eq_intsize id id = true. 116 * normalize // 117 qed. 118 119 lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s). 120 * normalize // 121 qed. 122 123 lemma type_eq_identity : ∀t. type_eq t t = true. 124 #t normalize elim (type_eq_dec t t) 125 [ 1: #Heq normalize // 126  2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed. 127 128 lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false. 129 #t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2) 130 [ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2)) 131  2: #Hneq' normalize // ] qed. 132 133 lemma type_eq_eq : ∀t1, t2. type_eq t1 t2 = true → t1 = t2. 134 #t1 #t2 whd in match (type_eq ??); cases (type_eq_dec t1 t2) normalize 135 [ 1: //  2: #_ #H destruct ] qed. 136 137 definition size_le ≝ λsz1,sz2. 138 match sz1 with 139 [ I8 ⇒ True 140  I16 ⇒ 141 match sz2 with 142 [ I16 ⇒ True  I32 ⇒ True  _ ⇒ False ] 143  I32 ⇒ 144 match sz2 with 145 [ I32 ⇒ True  _ ⇒ False ] 146 ]. 147 148 definition size_lt ≝ λsz1,sz2. 149 match sz1 with 150 [ I8 ⇒ 151 match sz2 with 152 [ I16 ⇒ True  I32 ⇒ True  _ ⇒ False ] 153  I16 ⇒ 154 match sz2 with 155 [ I32 ⇒ True  _ ⇒ False ] 156  I32 ⇒ False 157 ]. 158 159 lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)). 160 * * normalize /2/ /3/ 161 qed. 162 163 lemma size_not_lt_to_ge : ∀sz1,sz2. ¬(size_lt sz1 sz2) → (sz1 = sz2) + (size_lt sz2 sz1). 164 * * normalize /2/ /3/ 165 qed. 166 167 (* This function already exists in prop, we want it in type. *) 168 definition sign_eq_dect : ∀sg1,sg2:signedness. (sg1 = sg2) + (sg1 ≠ sg2). 169 * * normalize // qed. 170 171 lemma size_absurd : ∀a,b. size_le a b → size_lt b a → False. 172 * * normalize 173 #H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed. 174 175 176 (* This defines necessary conditions for [src_expr] to be coerced to "target_ty". 177 * Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *) 178 definition necessary_conditions ≝ λsrc_sz.λsrc_sg.λtarget_sz.λtarget_sg. 179 match size_lt_dec target_sz src_sz with 180 [ inl Hlt ⇒ true 181  inr Hnlt ⇒ 182 match sz_eq_dec target_sz src_sz with 183 [ inl Hsz_eq ⇒ 184 match sign_eq_dect src_sg target_sg with 185 [ inl Hsg_eq ⇒ false 186  inr Hsg_neq ⇒ true 187 ] 188  inr Hsz_neq ⇒ false 189 ] 190 ]. 191 192 (* Used to inject boolean functions in invariants. *) 193 definition is_true : bool → Prop ≝ λb. 194 match b with 195 [ true ⇒ True 196  false ⇒ False ]. 197 198 (* An useful lemma to cull out recursive calls: the guard forces the target type to be different from the origin type. *) 199 200 (* aux lemma *) 201 lemma size_lt_dec_not_refl : ∀sz. ∃H. size_lt_dec sz sz = inr ??H. 202 * normalize @(ex_intro … (nmk False (λauto:False.auto))) // qed. 203 204 205 206 lemma necessary_conditions_spec : 207 ∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) → 208 ((size_lt target_sz src_sz) ∨ (src_sz = target_sz ∧ src_sg ≠ target_sg)). 209 #src_sz #src_sg #target_sz #target_sg 210 whd in match (necessary_conditions ????); 211 cases (size_lt_dec target_sz src_sz) normalize nodelta 212 [ 1: #Hlt #_ %1 // 213  2: #Hnlt 214 cases (sz_eq_dec target_sz src_sz) normalize nodelta 215 [ 2: #_ #Hcontr destruct 216  1: #Heq cases (sign_eq_dect src_sg target_sg) normalize nodelta 217 [ 1: #_ #Hcontr destruct 218  2: #Hsg_neq #_ %2 destruct /2/ ] 219 ] 220 ] qed. 221 222 223 224 (* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an 225 * integer value smaller but containing the same stuff than [r2] then all is well. 226 * If the two evaluations are erroneous, all is well too. *) 227 definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res (val×trace). 228 match r1 with 229 [ OK res1 ⇒ 230 match r2 with 231 [ OK res2 ⇒ 232 let 〈v1, tr1〉 ≝ res1 in 233 let 〈v2, tr2〉 ≝ res2 in 234 match v1 with 235 [ Vint sz1 v1 ⇒ 236 match v2 with 237 [ Vint sz2 v2 ⇒ 238 match sz_eq_dec sz1 src_sz with 239 [ inl Hsrc_eq ⇒ 240 match sz_eq_dec sz2 dst_sz with 241 [ inl Hdst_eq ⇒ 242 v2 = cast_int_int sz1 sg sz2 v1 243 ∧ tr1 = tr2 244 ∧ size_le dst_sz src_sz 245  inr _ ⇒ False ] 246  inr _ ⇒ False ] 247  _ ⇒ False ] 248  _ ⇒ False ] 249  _ ⇒ False ] 250  Error errmsg1 ⇒ True (* Simulation ... *) 251 (* match r2 with 252 [ OK _ ⇒ False 253  Error errmsg2 ⇒ True (* Note that the two expressions may fail for different reasons ... Too lax maybe ? *) 254 ] *) 255 ]. 256 257 lemma smaller_integer_val_spec : ∀src_sz,dst_sz,sg,val1,val2,tr1,tr2. 258 smaller_integer_val src_sz dst_sz sg (OK ? 〈val1, tr1〉) (OK ? 〈val2, tr2〉) → 259 ∃v1,v2. val1 = Vint src_sz v1 ∧ val2 = Vint dst_sz v2 ∧ 260 v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz. 261 #src_sz #dst_sz #sg #val1 #val2 #tr1 #tr2 262 whd in ⊢ (% → ?); 263 elim val1 normalize nodelta 264 [ 1: #Hcontr @(False_ind … Hcontr)  3,4,5: #foo #Hcontr @(False_ind … Hcontr) 265  2: #size1 #int1 cases val2 266 [ 1: #Hcontr @(False_ind … Hcontr)  3,4,5: #foo #Hcontr @(False_ind … Hcontr) 267  2: #size2 #int2 normalize nodelta 268 cases (sz_eq_dec size1 src_sz) 269 cases (sz_eq_dec size2 dst_sz) 270 [ 2,3,4: #Hneq #Heq #Hcontr @(False_ind … Hcontr) 271  1: #Heq1 #Heq2 * * #Hcast #Htrace #H destruct 272 @(ex_intro … int1) @(ex_intro … (cast_int_int src_sz sg dst_sz int1)) 273 try @conj try @conj try @conj try @conj try @conj try @conj // 274 ] 275 ] 276 ] qed. 277 278 definition is_integer_type ≝ λty. 279 match ty with 280 [ Tint _ _ ⇒ True 281  _ ⇒ False 282 ]. 283 284 285 286 inductive simulate (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝ 287  SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → simulate A r1 r2 288  SimFail : (∃err. r1 = Error ? err) → simulate A r1 r2. 289 290 inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝ 291  Inv_eq : ∀result_flag. 292 result_flag = false → 293 typeof e1 = typeof e2 → 294 simulate ? (exec_expr ge en m e1) (exec_expr ge en m e2) → 295 simulate ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) → 296 simplify_inv ge en m e1 e2 target_sz target_sg result_flag 297  Inv_coerce_ok : ∀src_sz,src_sg. 298 (typeof e1) = (Tint src_sz src_sg) → 299 (typeof e2) = (Tint target_sz target_sg) → 300 (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) → 301 simplify_inv ge en m e1 e2 target_sz target_sg true. 302 303 304 (* This lemma proves that simplify_int actually implements an integer cast. This is central to the proof of correctness. *) 305 (* The case 4 can be merged with cases 7 and 8. *) 306 lemma simplify_int_implements_cast : ∀sz,sz'.∀sg,sg'.∀i,i'. simplify_int sz sz' sg sg' i = Some ? i' → i' = cast_int_int sz sg sz' i. 307 * * 308 [ 1: #sg #sg' #i #i' #Hsimp normalize in Hsimp ⊢ %; elim sg normalize destruct // 309  2,3,6: #sg #sg' #i #i' #Hsimp normalize in Hsimp; destruct (* ⊢ %; destruct destruct whd in Hsimp:(??%?); destruct *) 310  4: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %; 311 normalize in match (signed ?) in Hsimp; 312 normalize in match (S (plus ??)) in Hsimp; 313 normalize in match (plus 7 8) in Hsimp; 314 lapply Hsimp Hsimp 315 cases (head' bool 15 i) 316 normalize in match (andb ??); 317 [ 1,3: elim (reduce_bits_dec 8 7 true i) 318 [ 1,3: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta 319 [ 1: cases (eq_b true ?) normalize #H destruct normalize @refl 320  2: #H destruct normalize @refl ] 321  2,4: #Heq >Heq normalize nodelta #H destruct ] 322  2,4,5,6,7,8: 323 elim (reduce_bits_dec 8 7 false i) 324 [ 1,3,5,7,9,11: * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq) 325 [ 1,3,4: cases (eq_b false ?) normalize nodelta 326 #H destruct normalize @refl 327  2,5,6: #H destruct normalize @refl ] 328  2,4,6,8,10,12: #Heq >Heq normalize nodelta #H destruct 65 329 ] 66  _ ⇒ itc_no 330 ] 331  5,9: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); destruct @refl 332  7, 8: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %; 333 normalize in match (signed ?) in Hsimp; 334 normalize in match (S (plus ??)) in Hsimp; 335 normalize in match (plus 7 24) in Hsimp; 336 lapply Hsimp Hsimp 337 cases (head' bool ? i) 338 normalize in match (andb ??); 339 [ 1,3,9,11: 340 [ 1,2: (elim (reduce_bits_dec 24 7 true i))  3,4: (elim (reduce_bits_dec 16 15 true i)) ] 341 [ 1,3,5,7: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta 342 [ 1,3: cases (eq_b true ?) normalize #H destruct normalize @refl 343  2,4: #H destruct normalize @refl ] 344  2,4,6,8: #Heq >Heq normalize nodelta #H destruct ] 345  2,4,5,6,7,8,10,12,13,14,15,16: 346 [ 1,2,3,4,5,6: elim (reduce_bits_dec 24 7 false i) 347  6,7,8,9,10,11,12: elim (reduce_bits_dec 16 15 false i) ] 348 [ 1,3,5,7,9,11,13,15,17,19,21,23: 349 * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq) 350 [ 1,3,4,7,9,10: 351 cases (eq_b false ?) normalize nodelta #H destruct normalize @refl 352  2,5,6,8,11,12: #H destruct normalize @refl ] 353  2,4,6,8,10,12,14,16,18,20,22,24: #Heq >Heq normalize nodelta #H destruct 354 ] 355 ] 356 ] qed. 357 358 (* Facts about cast_int_int *) 359 360 (* copied from AssemblyProof *) 361 lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A. 362 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); // 363 #n #hd #tl #abs @⊥ destruct (abs) 364 qed. 365 366 lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n). 367 ∃hd.∃tl.v ≃ VCons A n hd tl. 368 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); 369 [ #abs @⊥ destruct (abs) 370  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 371 qed. 372 373 lemma vector_append_zero: 374 ∀A,m. 375 ∀v: Vector A m. 376 ∀q: Vector A 0. 377 v = q@@v. 378 #A #m #v #q 379 >(Vector_O A q) % 380 qed. 381 382 lemma prod_eq_left: 383 ∀A: Type[0]. 384 ∀p, q, r: A. 385 p = q → 〈p, r〉 = 〈q, r〉. 386 #A #p #q #r #hyp 387 >hyp % 388 qed. 389 390 lemma prod_eq_right: 391 ∀A: Type[0]. 392 ∀p, q, r: A. 393 p = q → 〈r, p〉 = 〈r, q〉. 394 #A #p #q #r #hyp 395 >hyp % 396 qed. 397 398 corollary prod_vector_zero_eq_left: 399 ∀A, n. 400 ∀q: Vector A O. 401 ∀r: Vector A n. 402 〈q, r〉 = 〈[[ ]], r〉. 403 #A #n #q #r 404 generalize in match (Vector_O A q …); 405 #hyp 406 >hyp in ⊢ (??%?); 407 % 408 qed. 409 410 lemma split_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n). ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2. 411 # A #m #n elim m 412 [ 1: normalize #v 413 elim (Vector_Sn ?? v) #hd * #tl #Eq 414 @(ex_intro … (hd ::: [[]])) @(ex_intro … tl) 415 >Eq normalize // 416  2: #n' #Hind #v 417 elim (Vector_Sn ?? v) #hd * #tl #Eq 418 elim (Hind tl) 419 #tl1 * #tl2 #Eq_tl 420 @(ex_intro … (hd ::: tl1)) 421 @(ex_intro … tl2) 422 destruct normalize // 423 ] qed. 424 425 lemma split_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n). ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2. 426 # A #m #n elim m 427 [ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize // 428  2: #n' #Hind #v 429 elim (Vector_Sn ?? v) #hd * #tl #Eq 430 elim (Hind tl) 431 #tl1 * #tl2 #Eq_tl 432 @(ex_intro … (hd ::: tl1)) 433 @(ex_intro … tl2) 434 destruct normalize // 435 ] qed. 436 437 lemma split_zero: 438 ∀A,m. 439 ∀v: Vector A m. 440 〈[[]], v〉 = split A 0 m v. 441 #A #m #v 442 elim v 443 [ % 444  #n #hd #tl #ih 445 normalize in ⊢ (???%); % 67 446 ] 68  _ ⇒ itc_no 447 qed. 448 449 450 lemma split_zero2: 451 ∀A,m. 452 ∀v: Vector A m. 453 〈[[]], v〉 = split' A 0 m v. 454 #A #m #v 455 elim v 456 [ % 457  #n #hd #tl #ih 458 normalize in ⊢ (???%); % 459 ] 460 qed. 461 462 (* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma. 463 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *) 464 axiom split_succ: 465 ∀A, m, n. 466 ∀l: Vector A m. 467 ∀r: Vector A n. 468 ∀v: Vector A (m + n). 469 ∀hd. 470 v = l@@r → (〈l, r〉 = split ? m n v → 〈hd:::l, r〉 = split ? (S m) n (hd:::v)). 471 472 axiom split_succ2: 473 ∀A, m, n. 474 ∀l: Vector A m. 475 ∀r: Vector A n. 476 ∀v: Vector A (m + n). 477 ∀hd. 478 v = l@@r → (〈l, r〉 = split' ? m n v → 〈hd:::l, r〉 = split' ? (S m) n (hd:::v)). 479 480 lemma split_prod2: 481 ∀A,m,n. 482 ∀p: Vector A (m + n). 483 ∀v: Vector A m. 484 ∀q: Vector A n. 485 p = v@@q → 〈v, q〉 = split' A m n p. 486 #A #m 487 elim m 488 [ #n #p #v #q #hyp 489 >hyp <(vector_append_zero A n q v) 490 >(prod_vector_zero_eq_left A …) 491 @split_zero2 492  #r #ih #n #p #v #q #hyp 493 >hyp 494 cases (Vector_Sn A r v) 495 #hd #exists 496 cases exists 497 #tl #jmeq >jmeq 498 @split_succ2 [1: % 2: @ih % ] 499 ] 500 qed. 501 502 lemma split_prod: 503 ∀A,m,n. 504 ∀p: Vector A (m + n). 505 ∀v: Vector A m. 506 ∀q: Vector A n. 507 p = v@@q → 〈v, q〉 = split A m n p. 508 #A #m 509 elim m 510 [ #n #p #v #q #hyp 511 >hyp <(vector_append_zero A n q v) 512 >(prod_vector_zero_eq_left A …) 513 @split_zero 514  #r #ih #n #p #v #q #hyp 515 >hyp 516 cases (Vector_Sn A r v) 517 #hd #exists 518 cases exists 519 #tl #jmeq >jmeq 520 @split_succ [1: % 2: @ih % ] 521 ] 522 qed. 523 524 525 (* Stolen from AssemblyProof.ma *) 526 lemma super_rewrite2: 527 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m. 528 ∀P: ∀m. Vector A m → Prop. 529 n=m → v1 ≃ v2 → P n v1 → P m v2. 530 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ // 531 qed. 532 533 lemma vector_cons_append: 534 ∀A: Type[0]. 535 ∀n: nat. 536 ∀e: A. 537 ∀v: Vector A n. 538 e ::: v = [[ e ]] @@ v. 539 # A # N # E # V 540 elim V 541 [ normalize % 542  # NN # AA # VV # IH 543 normalize 544 % 545 qed. 546 547 lemma vector_cons_append2: 548 ∀A: Type[0]. 549 ∀n, m: nat. 550 ∀v: Vector A n. 551 ∀q: Vector A m. 552 ∀hd: A. 553 hd:::(v@@q) = (hd:::v)@@q. 554 #A #n #m #v #q 555 elim v 556 [ #hd % 557  #n' #hd' #tl' #ih #hd' <ih % 558 ] 559 qed. 560 561 lemma jmeq_cons_vector_monotone: 562 ∀A: Type[0]. 563 ∀m, n: nat. 564 ∀v: Vector A m. 565 ∀q: Vector A n. 566 ∀prf: m = n. 567 ∀hd: A. 568 v ≃ q → hd:::v ≃ hd:::q. 569 #A #m #n #v #q #prf #hd #E 570 @(super_rewrite2 A … E) 571 [ assumption  % ] 572 qed. 573 574 lemma vector_associative_append: 575 ∀A: Type[0]. 576 ∀n, m, o: nat. 577 ∀v: Vector A n. 578 ∀q: Vector A m. 579 ∀r: Vector A o. 580 ((v @@ q) @@ r) 581 ≃ 582 (v @@ (q @@ r)). 583 #A #n #m #o #v #q #r 584 elim v 585 [ % 586  #n' #hd #tl #ih 587 <(vector_cons_append2 A … hd) 588 @jmeq_cons_vector_monotone 589 // 590 ] 591 qed. 592 593 lemma tail_eat_cons : ∀A. ∀n. ∀hd:A. ∀v:Vector A n. tail A n (hd ::: v) = v. 594 #A #n #hd #v normalize // 595 qed. 596 597 lemma tail_eat_pad : ∀A. ∀padelt. ∀padlen, veclen. ∀v:Vector A veclen. 598 tail A ? (pad_vector A padelt (S padlen) veclen v) = pad_vector A padelt padlen veclen v. 599 # A #padelt #padlen #veclen #v 600 normalize // 601 qed. 602 603 lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)). 604 #s1 #v normalize elim s1 normalize nodelta 605 normalize in v; 606 elim (split_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) 607 [ 2,4: // 608  1,3: #l * #r normalize nodelta #Eq1 609 <(split_prod bool 16 16 … Eq1) 610 elim (split_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) 611 [ 2,4: // 612  1,3: #lr * #rr normalize nodelta #Eq2 613 <(split_prod bool 8 8 … Eq2) 614 cut (v = (l @@ lr) @@ rr) 615 [ 1,3 : destruct >(vector_associative_append ? 16 8) // 616  2,4: #Hrewrite destruct 617 <(split_prod bool 24 8 … Hrewrite) @refl 618 ] 619 ] 620 ] qed. 621 622 lemma cast_idempotent : ∀s1,s2,sz1,sz2,v. size_lt sz1 sz2 → cast_int_int sz2 s1 sz1 (cast_int_int sz1 s2 sz2 v) = v. 623 #s1 #s2 * * #v elim s1 elim s2 624 normalize #H try @refl 625 @(False_ind … H) 626 qed. 627 628 lemma cast_identity : ∀sz,sg,v. cast_int_int sz sg sz v = v. 629 * * #v normalize // qed. 630 631 lemma cast_collapse : ∀s1,s2,v. cast_int_int I32 s1 I8 (cast_int_int I16 s2 I32 v) = (cast_int_int I16 s1 I8 v). 632 #s1 #s2 #v >cast_decompose >cast_idempotent 633 [ 1: @refl  2: // ] 634 qed. 635 636 lemma cast_composition_lt : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val. 637 size_lt c_sz a_sz → size_lt c_sz b_sz → 638 (cast_int_int a_sz a_sg c_sz val = 639 cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)). 640 * #a_sg * #b_sg * #val whd in match (size_lt ??); whd in match (size_lt ??); 641 #Hlt1 #Hlt2 642 [ 1,2,3,4,5,6,7,8,9,10,11,12,14,15,17,18,19,20,21,23,24,27: 643 @(False_ind … Hlt1) @(False_ind … Hlt2) 644  13,25,26: >cast_identity elim a_sg elim b_sg normalize // 645  22: normalize elim b_sg elim a_sg normalize 646 normalize in val; 647 elim (split_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) 648 [ 2,4,6,8: normalize // 649  1,3,5,7: #left * #right normalize #Eq1 650 <(split_prod bool 16 16 … Eq1) 651 elim (split_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) 652 [ 2,4,6,8: // 653  1,3,5,7: #rightleft * #rightright normalize #Eq2 654 <(split_prod bool 8 8 … Eq2) 655 cut (val = (left @@ rightleft) @@ rightright) 656 [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) // 657  2,4,6,8: #Hrewrite destruct 658 <(split_prod bool 24 8 … Hrewrite) @refl 659 ] 660 ] 661 ] 662  16: elim b_sg elim a_sg >cast_collapse @refl 663 ] qed. 664 665 lemma cast_composition : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val. 666 size_le c_sz a_sz → size_le c_sz b_sz → 667 (cast_int_int a_sz a_sg c_sz val = 668 cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)). 669 #a_sz #a_sg #b_sz #b_sg #c_sz #val #Hle_c_a #Hle_c_b 670 cases (size_lt_dec c_sz a_sz) 671 cases (size_lt_dec c_sz b_sz) 672 [ 1: #Hltb #Hlta @(cast_composition_lt … Hlta Hltb) 673  2: #Hnltb #Hlta 674 cases (size_not_lt_to_ge … Hnltb) 675 [ 1: #Heq destruct >cast_identity // 676  2: #Hltb @(False_ind … (size_absurd ?? Hle_c_b Hltb)) 677 ] 678  3: #Hltb #Hnlta 679 cases (size_not_lt_to_ge … Hnlta) 680 [ 1: #Heq destruct >cast_idempotent // 681  2: #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) 682 ] 683  4: #Hnltb #Hnlta 684 cases (size_not_lt_to_ge … Hnlta) 685 cases (size_not_lt_to_ge … Hnltb) 686 [ 1: #Heq_b #Heq_a destruct >cast_identity >cast_identity // 687  2: #Hltb #Heq @(False_ind … (size_absurd ?? Hle_c_b Hltb)) 688  3: #Eq #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) 689  4: #Hltb #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) 690 ] 691 ] qed. 692 693 let rec assert_int_value (v : option val) (expected_size : intsize) : option (BitVector (bitsize_of_intsize expected_size)) ≝ 694 match v with 695 [ None ⇒ None ? 696  Some v ⇒ 697 match v with 698 [ Vint sz i ⇒ 699 match sz_eq_dec sz expected_size with 700 [ inl Heq ⇒ Some ?? 701  inr _ ⇒ None ? 702 ] 703  _ ⇒ None ? 704 ] 69 705 ]. 706 >Heq in i; #i @i qed. 707 708 (* cast_int_int behaves as truncate (≃ split) when downsizing *) 709 (* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *) 710 711 lemma split_to_truncate : ∀m,n,i. (\snd (split bool m n i)) = truncate m n i. 712 #m #n #i normalize // qed. 713 714 (* Somme lemmas on how "simplifiable" operations behave under cast_int_int. *) 715 716 lemma integer_add_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz → 717 (addition_n (bitsize_of_intsize target_sz) 718 (cast_int_int src_sz sg target_sz lhs_int) 719 (cast_int_int src_sz sg target_sz rhs_int) 720 = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). 721 #src_sz #target_sz #sg #lhs_int #rhs_int #Hlt 722 elim src_sz in Hlt lhs_int rhs_int; elim target_sz 723 [ 1,2,3,5,6,9: normalize #H @(False_ind … H) 724  *: elim sg #_ 725 normalize in match (bitsize_of_intsize ?); 726 normalize in match (bitsize_of_intsize ?); 727 #lint #rint 728 normalize in match (cast_int_int ????); 729 normalize in match (cast_int_int ????); 730 whd in match (addition_n ???); 731 whd in match (addition_n ???) in ⊢ (???%); 732 >split_to_truncate >split_to_truncate 733 <truncate_add_with_carries 734 [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false); 735  3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint rint false); 736  5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint rint false); 737 ] 738 * #result #carry 739 normalize nodelta // 740 qed. 741 742 lemma integer_add_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz → 743 (addition_n (bitsize_of_intsize target_sz) 744 (cast_int_int src_sz sg target_sz lhs_int) 745 (cast_int_int src_sz sg target_sz rhs_int) 746 = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). 747 #src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct 748 >cast_identity >cast_identity >cast_identity // qed. 749 750 lemma integer_add_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz → 751 (addition_n (bitsize_of_intsize target_sz) 752 (cast_int_int src_sz sg target_sz lhs_int) 753 (cast_int_int src_sz sg target_sz rhs_int) 754 = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). 755 #src_sz #target_sz #sg #lhs_int #rhs_int #Hle 756 cases (sz_eq_dec target_sz src_sz) 757 [ 1: #Heq @(integer_add_cast_eq … Heq) 758  2: #Hneq cut (size_lt target_sz src_sz) 759 [ 1: elim target_sz in Hle Hneq; elim src_sz normalize // 760 #_ * #H @(H … (refl ??)) 761  2: #Hlt @(integer_add_cast_lt … Hlt) 762 ] 763 ] qed. 764 765 lemma truncate_eat : ∀l,n,m,v. l = n → ∃tl. truncate (S n) m v = truncate l m tl. 766 #l #n #m #v #len elim (Vector_Sn … v) #hd * #tl #Heq >len 767 @(ex_intro … tl) 768 >Heq >Heq 769 elim (split_eq2 … tl) #l * #r #Eq 770 normalize 771 <(split_prod bool n m tl l r Eq) 772 <(split_prod2 bool n m tl l r Eq) 773 normalize // 774 qed. 775 776 777 lemma integer_neg_trunc : ∀m,n. ∀i: BitVector (m+n). two_complement_negation n (truncate m n i) = truncate m n (two_complement_negation (m+n) i). 778 #m elim m 779 [ 1: #n #i normalize in i; 780 whd in match (truncate ???); 781 whd in match (truncate ???) in ⊢ (???%); 782 <split_zero <split_zero // 783  2: #m' #Hind #n #i normalize in i; 784 elim (Vector_Sn … i) #hd * #tl #Heq 785 whd in match (two_complement_negation (S ?) ?); 786 >Heq in ⊢ (??%?); >truncate_tail whd in match (tail ???) in ⊢ (??%?); 787 whd in match (two_complement_negation ??) in ⊢ (??%?); 788 lapply (Hind ? tl) #H 789 whd in match (two_complement_negation ??) in H; 790 (* trying to reduce add_with_carries *) 791 normalize in match (S m'+n); 792 whd in match (zero ?) in ⊢ (???%); 793 >Heq in match (negation_bv ??) in ⊢ (???%); 794 whd in match (negation_bv ??) in ⊢ (???%); 795 >add_with_carries_unfold in ⊢ (???%); 796 (* >truncate_tail *) 797 normalize in ⊢ (???%); 798 cases hd normalize nodelta 799 [ 1,2: <add_with_carries_unfold in ⊢ (???%); (* Good. Some progress. *) 800 (* try to transform the rhs of H into what we need. *) 801 whd in match (two_complement_negation ??) in H:(???%); 802 lapply H H 803 generalize in match (add_with_carries (m'+n) (negation_bv (m'+n) tl) (zero (m'+n)) true); 804 * #Left #Right normalize nodelta 805 #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ?  _ ⇒ ?]))))); 806 #b >(split_to_truncate (S m')) >truncate_tail 807 cases b 808 normalize nodelta 809 normalize in match (tail ???); @H 810 ] 811 ] qed. (* This was painful. *) 812 813 lemma integer_sub_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz → 814 (subtraction (bitsize_of_intsize target_sz) 815 (cast_int_int src_sz sg target_sz lhs_int) 816 (cast_int_int src_sz sg target_sz rhs_int) 817 = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). 818 #src_sz #target_sz #sg #lhs_int #rhs_int #Hlt 819 elim src_sz in Hlt lhs_int rhs_int; elim target_sz 820 [ 1,2,3,5,6,9: normalize #H @(False_ind … H) 821  *: elim sg #_ 822 normalize in match (bitsize_of_intsize ?); 823 normalize in match (bitsize_of_intsize ?); 824 #lint #rint 825 normalize in match (cast_int_int ????); 826 normalize in match (cast_int_int ????); 827 whd in match (subtraction ???); 828 whd in match (subtraction ???) in ⊢ (???%); 829 >split_to_truncate >split_to_truncate 830 >integer_neg_trunc <truncate_add_with_carries 831 [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false); 832  3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint ? false); 833  5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint ? false); 834 ] 835 * #result #carry 836 normalize nodelta // 837 qed. 838 839 lemma integer_sub_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz → 840 (subtraction (bitsize_of_intsize target_sz) 841 (cast_int_int src_sz sg target_sz lhs_int) 842 (cast_int_int src_sz sg target_sz rhs_int) 843 = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). 844 #src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct 845 >cast_identity >cast_identity >cast_identity // 846 qed. 847 848 lemma integer_sub_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz → 849 (subtraction (bitsize_of_intsize target_sz) 850 (cast_int_int src_sz sg target_sz lhs_int) 851 (cast_int_int src_sz sg target_sz rhs_int) 852 = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). 853 #src_sz #target_sz #sg #lhs_int #rhs_int #Hle 854 cases (sz_eq_dec target_sz src_sz) 855 [ 1: #Heq @(integer_sub_cast_eq … Heq) 856  2: #Hneq cut (size_lt target_sz src_sz) 857 [ 1: elim target_sz in Hle Hneq; elim src_sz normalize // 858 #_ * #H @(H … (refl ??)) 859  2: #Hlt @(integer_sub_cast_lt … Hlt) 860 ] 861 ] qed. 862 863 lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg. 864 * * // qed. 865 866 lemma classify_sub_int : ∀sz,sg. classify_sub (Tint sz sg) (Tint sz sg) = sub_case_ii sz sg. 867 * * // qed. 868 869 (* This ought to be somewhere else. Lemma used in proving the correctness of the Binop case. *) 870 lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true. 871 * * normalize #H @conj // qed. 872 873 lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le sz' sz. 874 * #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed. 70 875 71 876 (* Operations where it is safe to use a smaller integer type on the assumption 72 877 that we would cast it down afterwards anyway. *) 73 74 878 definition binop_simplifiable ≝ 75 879 λop. match op with [ Oadd ⇒ true  Osub ⇒ true  _ ⇒ false ]. 880 881 notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)" 882 with precedence 10 883 for @{ match $t return λx.x = $t → ? with [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}.$s ] (refl ? $t) }. 884 885 notation > "hvbox('let' « 〈ident x1,ident x2〉, ident y» 'as' ident E, ident F ≝ t 'in' s)" 886 with precedence 10 887 for @{ match $t return λx.x = $t → ? with 888 [ mk_Sig ${fresh a} ${ident y} ⇒ λ${ident E}. 889 match ${fresh a} return λx.x = ${fresh a} → ? with 890 [ mk_Prod ${ident x1} ${ident x2} ⇒ λ${ident F}. $s ] (refl ? ${fresh a}) 891 ] (refl ? $t) 892 }. 893 894 notation > "hvbox('do' «ident x, ident y» 'as' ident E ← t; break s)" 895 with precedence 48 896 for @{ match $t with 897 [ Some ${fresh res} ⇒ 898 match ${fresh res} return λx.x = ${fresh res} → ? with 899 [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}. $s 900 ] (refl ? ${fresh res}) 901  None ⇒ None ? 902 ] }. 903 904 905 (* This function will make your eyes bleed. You've been warned. 906 * Implements a correctbyconstruction version of Brian's original castremoval code. Does so by 907 * threading an invariant defined in [simplify_inv], which says roughly "simplification yields either 908 what you hoped for, i.e. an integer value of the right size, OR something equivalent to the original 909 expression". [simplify_expr] is not to be called directly: simplify inside is the proper wrapper. 910 * TODO: proper doc. Some cases are simplifiable. Some type equality tests are maybe dispensable. 911 * This function is slightly more conservative than the original one, but this should be incrementally 912 * modifiable (replacing calls to simplify_inside by calls to simplify_expr, + proving correction). 913 * Also, I think that the proofs are factorizable to a great deal, but I'd rather have something 914 * more or less "modular", casebycase wise. 915 *) 916 let rec simplify_expr2 (e:expr) (target_sz:intsize) (target_sg:signedness) 917 : Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ 918 match e return λx. x = e → ? with 919 [ Expr ed ty ⇒ λHexpr_eq. 920 match ed return λx. ed = x → ? with 921 [ Econst_int cst_sz i ⇒ λHdesc_eq. 922 match ty return λx. x=ty → ? with 923 [ Tint ty_sz sg ⇒ λHexprtype_eq. 924 (* Ensure that the displayed type size [cst_sz] and actual size [sz] are equal ... *) 925 match sz_eq_dec cst_sz ty_sz with 926 [ inl Hsz_eq ⇒ 927 match type_eq_dec ty (Tint target_sz target_sg) with 928 [ inl Hdonothing ⇒ «〈true, e〉, ?» 929  inr Hdosomething ⇒ 930 (* Do the actual useful work *) 931 match simplify_int cst_sz target_sz sg target_sg i return λx. (simplify_int cst_sz target_sz sg target_sg i) = x → ? with 932 [ Some i' ⇒ λHsimpl_eq. 933 «〈true, Expr (Econst_int target_sz i') (Tint target_sz target_sg)〉, ?» 934  None ⇒ λ_. 935 «〈false, e〉, ?» 936 ] (refl ? (simplify_int cst_sz target_sz sg target_sg i)) 937 ] 938  inr _ ⇒ (* The expression is illtyped. *) 939 «〈false, e〉, ?» 940 ] 941  _ ⇒ λ_. 942 «〈false, e〉, ?» 943 ] (refl ? ty) 944  Ederef e1 ⇒ λHdesc_eq. 945 let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in 946 «〈false, Expr (Ederef e2) ty〉, ?» 947  Eaddrof e1 ⇒ λHdesc_eq. 948 let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in 949 «〈false, Expr (Eaddrof e2) ty〉, ?» 950  Eunop op e1 ⇒ λHdesc_eq. 951 let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in 952 «〈false, Expr (Eunop op e2) ty〉, ?» 953  Ebinop op lhs rhs ⇒ λHdesc_eq. 954 (* Type equality is enforced to prove the equalities needed in return by the invariant. *) 955 match binop_simplifiable op 956 return λx. (binop_simplifiable op) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) 957 with 958 [ true ⇒ λHop_simplifiable_eq. 959 match assert_type_eq ty (typeof lhs) with 960 [ OK Hty_eq_lhs ⇒ 961 match assert_type_eq (typeof lhs) (typeof rhs) with 962 [ OK Htylhs_eq_tyrhs ⇒ 963 let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr2 lhs target_sz target_sg in 964 let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr2 rhs target_sz target_sg in 965 match desired_type_lhs ∧ desired_type_rhs 966 return λx. (desired_type_lhs ∧ desired_type_rhs) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) 967 with 968 [ true ⇒ λHdesired_eq. 969 «〈true, Expr (Ebinop op lhs1 rhs1) (Tint target_sz target_sg)〉, ?» 970  false ⇒ λHdesired_eq. 971 let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in 972 let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in 973 «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» 974 ] (refl ? (desired_type_lhs ∧ desired_type_rhs)) 975  Error _ ⇒ 976 let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in 977 let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in 978 «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» 979 ] 980  Error _ ⇒ 981 let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in 982 let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in 983 «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» 984 ] 985  false ⇒ λHop_simplifiable_eq. 986 let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in 987 let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in 988 «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» 989 ] (refl ? (binop_simplifiable op)) 990  Ecast cast_ty castee ⇒ λHdesc_eq. 991 match cast_ty return λx. x = cast_ty → ? with 992 [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq. 993 match type_eq_dec ty cast_ty with 994 [ inl Hcast_eq ⇒ 995 match necessary_conditions cast_sz cast_sg target_sz target_sg 996 return λx. x = (necessary_conditions cast_sz cast_sg target_sz target_sg) → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) 997 with 998 [ true ⇒ λHconditions. 999 let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr2 castee target_sz target_sg in 1000 match desired_type return λx. desired_type = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) 1001 with 1002 [ true ⇒ λHdesired_eq. 1003 «〈true, castee1〉, ?» 1004  false ⇒ λHdesired_eq. 1005 let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr2 castee cast_sz cast_sg in 1006 match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) 1007 with 1008 [ true ⇒ λHdesired2_eq. 1009 «〈false, castee2〉, ?» 1010  false ⇒ λHdesired2_eq. 1011 «〈false, Expr (Ecast ty castee2) cast_ty〉, ?» 1012 ] (refl ? desired_type2) 1013 ] (refl ? desired_type) 1014  false ⇒ λHconditions. 1015 let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr2 castee cast_sz cast_sg in 1016 match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) 1017 with 1018 [ true ⇒ λHdesired2_eq. 1019 «〈false, castee2〉, ?» 1020  false ⇒ λHdesired2_eq. 1021 «〈false, Expr (Ecast ty castee2) cast_ty〉, ?» 1022 ] (refl ? desired_type2) 1023 ] (refl ? (necessary_conditions cast_sz cast_sg target_sz target_sg)) 1024  inr Hcast_neq ⇒ 1025 (* inconsistent types ... *) 1026 let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in 1027 «〈false, Expr (Ecast cast_ty castee1) ty〉, ?» 1028 ] 1029  _ ⇒ λHcast_ty_eq. 1030 let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in 1031 «〈false, Expr (Ecast cast_ty castee1) ty〉, ?» 1032 ] (refl ? cast_ty) 1033  Econdition cond iftrue iffalse ⇒ λHdesc_eq. 1034 let «cond1, Hcond_equiv» as Hsimplify ≝ simplify_inside cond in 1035 match assert_type_eq ty (typeof iftrue) with 1036 [ OK Hty_eq_iftrue ⇒ 1037 match assert_type_eq (typeof iftrue) (typeof iffalse) with 1038 [ OK Hiftrue_eq_iffalse ⇒ 1039 let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue ≝ simplify_expr2 iftrue target_sz target_sg in 1040 let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr2 iffalse target_sz target_sg in 1041 match desired_true ∧ desired_false 1042 return λx. (desired_true ∧ desired_false) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) 1043 with 1044 [ true ⇒ λHdesired_eq. 1045 «〈true, Expr (Econdition cond1 iftrue1 iffalse1) (Tint target_sz target_sg)〉, ?» 1046  false ⇒ λHdesired_eq. 1047 let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in 1048 let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in 1049 «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» 1050 ] (refl ? (desired_true ∧ desired_false)) 1051  _ ⇒ 1052 let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in 1053 let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in 1054 «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» 1055 ] 1056  _ ⇒ 1057 let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in 1058 let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in 1059 «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» 1060 ] 1061 (* Could probably do better with these, too. *) 1062  Eandbool lhs rhs ⇒ λHdesc_eq. 1063 let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in 1064 let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in 1065 «〈false, Expr (Eandbool lhs1 rhs1) ty〉, ?» 1066  Eorbool lhs rhs ⇒ λHdesc_eq. 1067 let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in 1068 let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in 1069 «〈false, Expr (Eorbool lhs1 rhs1) ty〉,?» 1070 (* Could also improve Esizeof *) 1071  Efield rec_expr f ⇒ λHdesc_eq. 1072 let «rec_expr1, Hrec_expr_equiv» as Hsimplify ≝ simplify_inside rec_expr in 1073 «〈false,Expr (Efield rec_expr1 f) ty〉, ?» 1074  Ecost l e1 ⇒ λHdesc_eq. 1075 (* The invariant requires that the toplevel [ty] type matches the type of [e1]. *) 1076 (* /!\ XXX /!\ We assume that the type of a costlabelled expr is the type of the underlying expr. *) 1077 match type_eq_dec ty (typeof e1) with 1078 [ inl Heq ⇒ 1079 let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr2 e1 target_sz target_sg in 1080 «〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?» 1081  inr Heq ⇒ 1082 let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in 1083 «〈false, Expr (Ecost l e2) ty〉, ?» 1084 ] 1085  Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» 1086  Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» 1087  Esizeof t ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» 1088 ] (refl ? ed) 1089 ] (refl ? e) 1090 1091 and simplify_inside (e:expr) : Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result) 1092 ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 1093 ∧ typeof e = typeof result) ≝ 1094 match e return λx. x = e → ? with 1095 [ Expr ed ty ⇒ λHexpr_eq. 1096 match ed return λx. x = ed → ? with 1097 [ Ederef e1 ⇒ λHdesc_eq. 1098 let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in 1099 «Expr (Ederef e2) ty, ?» 1100  Eaddrof e1 ⇒ λHdesc_eq. 1101 let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in 1102 «Expr (Eaddrof e2) ty, ?» 1103  Eunop op e1 ⇒ λHdesc_eq. 1104 let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in 1105 «Expr (Eunop op e2) ty, ?» 1106  Ebinop op lhs rhs ⇒ λHdesc_eq. 1107 let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in 1108 let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in 1109 «Expr (Ebinop op lhs1 rhs1) ty, ?» 1110  Ecast cast_ty castee ⇒ λHdesc_eq. 1111 match cast_ty with 1112 [ Tint cast_sz cast_sg ⇒ 1113 let «〈success, castee〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr2 castee cast_sz cast_sg in 1114 match success with 1115 [ true ⇒ 1116 «castee, ?» 1117  false ⇒ 1118 «Expr (Ecast cast_ty castee) ty, ?» 1119 ] 1120  _ ⇒ 1121 «e, ?» 1122 ] 1123  _ ⇒ λHdesc_eq. 1124 (* TODO, replace this stub by the actual recursive calls to simplify_inside. Should be nonproblematic. *) 1125 «e, ?» 1126 ] (refl ? ed) 1127 ] (refl ? e). 1128 #ge #en #m 1129 [ 1,3,5,6,7,8,9,10,11,12: %1 // 1130 cases (exec_expr ge en m e) #res 1131 try (@(SimOk ???) //) 1132  13,14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res 1133 try (@(SimOk ???) //) 1134  2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct // 1135 whd in match (exec_expr ????); >eq_intsize_identity whd 1136 >sz_eq_identity normalize % [ 1: @conj //  2: elim target_sz in i; normalize #i @I ] 1137  4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) // 1138 whd in match (exec_expr ????); 1139 whd in match (exec_expr ????); 1140 >eq_intsize_identity >eq_intsize_identity whd 1141 >sz_eq_identity >sz_eq_identity whd @conj try @conj // 1142 [ 1: @(simplify_int_implements_cast … Hsimpl_eq) 1143  2: @(simplify_int_success_lt … Hsimpl_eq) ] 1144  15: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 1145 [ 1: (* Proving preservation of the semantics for expressions. *) 1146 cases Hexpr_sim 1147 [ 2: (* Case where the evaluation of e1 as an expression fails *) 1148 normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2/ 1149  1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1150 #Hsim %1 * #val #trace normalize #Hstep 1151 cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ 1152 (load_value_of_type ty m (pblock ptr) (poff ptr) = Some ? val)) 1153 [ 1: lapply Hstep Hstep 1154 cases (exec_expr ge en m e1) 1155 [ 1: * #val' #trace' normalize nodelta 1156 cases val' normalize nodelta 1157 [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct 1158  5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) 1159 cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq; 1160 normalize nodelta 1161 [ 1: #Heq destruct  2: #val2 #Heq destruct @conj // ] 1162 ] 1163  2: normalize nodelta #errmesg #Hcontr destruct 1164 ] 1165  2: * #e1_ptr * #He1_eq_ptr #Hloadptr 1166 cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) 1167 ∧ (load_value_of_type ty m (pblock ptr1) (poff ptr1) = Some ? val)) 1168 [ 1: @(ex_intro … e1_ptr) @conj 1169 [ 1: @Hsim //  2: // ] 1170  2: * #e2_ptr * #He2_exec #Hload_e2_ptr 1171 normalize >He2_exec normalize nodelta >Hload_e2_ptr normalize nodelta @refl 1172 ] 1173 ] 1174 ] 1175  2: (* Proving the preservation of the semantics for lvalues. *) 1176 cases Hexpr_sim 1177 [ 2: (* Case where the evaluation of e1 as an lvalue fails *) 1178 normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2/ 1179  1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1180 #Hsim %1 * * #block #offset #trace normalize #Hstep 1181 cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ pblock ptr = block ∧ poff ptr = offset) 1182 [ 1: lapply Hstep Hstep 1183 cases (exec_expr ge en m e1) 1184 [ 1: * #val' #trace' normalize nodelta 1185 cases val' normalize nodelta 1186 [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct 1187  5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) 1188 destruct try @conj try @conj // 1189 ] 1190  2: normalize nodelta #errmesg #Hcontr destruct 1191 ] 1192  2: * #e1_ptr * * #He1_eq_ptr #Hblock #Hoffset 1193 cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) ∧ pblock ptr1 = block ∧ poff ptr1 = offset) 1194 [ 1: @(ex_intro … e1_ptr) @conj try @conj // @Hsim // 1195  2: * #e2_ptr * * #He2_exec #Hblock #Hoffset 1196 normalize >He2_exec normalize nodelta // 1197 ] 1198 ] 1199 ] 1200 ] 1201  16: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 1202 [ 1: (* Proving preservation of the semantics for expressions. *) 1203 cases Hlvalue_sim 1204 [ 2: (* Case where the evaluation of e1 as an expression fails *) 1205 * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2/ 1206  1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1207 #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep 1208 cut (∃block,offset,r,ptype,pc. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧ 1209 (pointer_compat_dec block r = inl ?? pc) ∧ 1210 (ty = Tpointer r ptype) ∧ 1211 val = Vptr (mk_pointer r block pc offset)) 1212 [ 1: lapply Hstep Hstep 1213 cases (exec_lvalue ge en m e1) 1214 [ 1: * * #block #offset #trace' normalize nodelta 1215 cases ty 1216 [ 2: #sz #sg  3: #fsz  4: #rg #ptr_ty  5: #rg #array_ty #array_sz  6: #domain #codomain 1217  7: #structname #fieldspec  8: #unionname #fieldspec  9: #rg #id ] 1218 normalize nodelta try (#Heq destruct) 1219 @(ex_intro … block) @(ex_intro … offset) @(ex_intro … rg) @(ex_intro … ptr_ty) 1220 cases (pointer_compat_dec block rg) in Heq; normalize 1221 [ 2: #Hnotcompat #Hcontr destruct 1222  1: #compat #Heq @(ex_intro … compat) try @conj try @conj try @conj destruct // ] 1223  2: normalize nodelta #errmesg #Hcontr destruct 1224 ] 1225  2: * #block * #offset * #region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat #Hty_eq #Hval_eq 1226 whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta 1227 >Hptr_compat normalize nodelta // 1228 ] 1229 ] 1230  2: (* Proving preservation of the semantics of lvalues. *) 1231 normalize @SimFail /2/ 1232 ] 1233  17: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 1234 [ 1: whd in match (exec_expr ge en m (Expr ??)); 1235 whd in match (exec_expr ge en m (Expr ??)); 1236 cases Hexpr_sim 1237 [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2/ 1238  1: cases (exec_expr ge en m e1) 1239 [ 2: #error #Hexec normalize nodelta @SimFail /2/ 1240  1: * #val #trace #Hexec 1241 >(Hexec ? (refl ? (OK ? 〈val,trace〉))) 1242 normalize nodelta @SimOk #a >Htype_eq #H @H 1243 ] 1244 ] 1245  2: normalize @SimFail /2/ 1246 ] 1247  18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs Hdesired_eq 1248 inversion (Hinv_lhs ge en m) 1249 [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true 1250 #Hinv <Hresult_flag_lhs_eq_true in Hresult_lhs; >Hdesired_lhs #Habsurd destruct 1251  2: #lhs_src_sz #lhs_src_sg #Htype_lhs #Htype_lhs1 #Hsmaller_lhs #Hdesired_type_lhs #_ 1252 inversion (Hinv_rhs ge en m) 1253 [ 1: #result_flag_rhs #Hresult_rhs #Htype_rhs #Hsim_expr_rhs #Hsim_lvalue_rhs #Hdesired_type_rhs_eq #_ 1254 <Hdesired_type_rhs_eq in Hresult_rhs; >Hdesired_rhs #Habsurd destruct 1255  2: #rhs_src_sz #rhs_src_sg #Htype_rhs #Htype_rhs1 #Hsmaller_rhs #Hdesired_type_rhs #_ 1256 @(Inv_coerce_ok ge en m … target_sz target_sg lhs_src_sz lhs_src_sg) 1257 [ 1: >Htype_lhs // 1258  2: // 1259  3: whd in match (exec_expr ??? (Expr ??)); 1260 whd in match (exec_expr ??? (Expr ??)); 1261 (* Enumerate all the cases for the evaluation of the source expressions ... *) 1262 cases (exec_expr ge en m lhs) in Hsmaller_lhs; 1263 [ 2: #error normalize // 1264  1: * #val_lhs #trace_lhs normalize nodelta cases (exec_expr ge en m lhs1) 1265 [ 2: #error normalize #H @(False_ind … H) 1266  1: * #val_lhs1 #trace_lhs1 #Hsmaller_lhs 1267 elim (smaller_integer_val_spec … Hsmaller_lhs) 1268 #lhs_int * #lhs1_int * * * * #Hval_lhs #Hval_lhs1 #Hlhs_cast #Hlhs_trace #Hlhs_size 1269 cases (exec_expr ge en m rhs) in Hsmaller_rhs; 1270 [ 2: #error normalize // 1271  1: * #val_rhs #trace_rhs normalize nodelta cases (exec_expr ge en m rhs1) 1272 [ 2: #error normalize #H @(False_ind … H) 1273  1: * #val_rhs1 #trace_rhs1 #Hsmaller_rhs 1274 elim (smaller_integer_val_spec … Hsmaller_rhs) 1275 #rhs_int * #rhs1_int * * * * #Hval_rhs #Hval_rhs1 #Hrhs_cast #Hrhs_trace #Hrhs_size 1276 whd in match (m_bind ?????); 1277 whd in match (m_bind ?????); 1278 <Htylhs_eq_tyrhs >Htype_lhs 1279 >Htype_lhs1 >Htype_rhs1 1280 cut (lhs_src_sz = rhs_src_sz ∧ lhs_src_sg = rhs_src_sg) 1281 [ 1: >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Hty_eq destruct (Hty_eq) 1282 @conj // ] 1283 * #Hsrc_sz_eq #Hsrc_sg_eq 1284 cases op in Hop_simplifiable_eq; 1285 normalize in match (binop_simplifiable ?); 1286 [ 3,4,5,6,7,8,9,10,11,12,13,14,15,16: #H destruct (H) 1287  1: #_ (* addition case *) 1288 >Hval_lhs >Hval_rhs destruct 1289 whd in match (sem_binary_operation Oadd ?????); 1290 whd in match (sem_binary_operation Oadd ?????); normalize nodelta 1291 >classify_add_int >classify_add_int normalize nodelta 1292 >intsize_eq_elim_true >intsize_eq_elim_true 1293 whd in match (opt_to_res ???); whd in match (opt_to_res ???); 1294 whd in match (smaller_integer_val ?????); normalize nodelta 1295 >sz_eq_identity >sz_eq_identity normalize nodelta 1296 try @conj try @conj try // 1297 >integer_add_cast_le // 1298  2: #_ (* subtraction case *) 1299 >Hval_lhs >Hval_rhs destruct 1300 whd in match (sem_binary_operation Osub ?????); 1301 whd in match (sem_binary_operation Osub ?????); normalize nodelta 1302 >classify_sub_int >classify_sub_int normalize nodelta 1303 >intsize_eq_elim_true >intsize_eq_elim_true 1304 whd in match (opt_to_res ???); whd in match (opt_to_res ???); 1305 whd in match (smaller_integer_val ?????); normalize nodelta 1306 >sz_eq_identity >sz_eq_identity normalize nodelta 1307 try @conj try @conj try // 1308 >integer_sub_cast_le // 1309 ] 1310 ] 1311 ] 1312 ] 1313 ] 1314 ] 1315 ] 1316 ] 1317  19,20,21,22: destruct %1 // 1318 elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs 1319 elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs 1320 [ 1,3,5,7: 1321 whd in match (exec_expr ????); whd in match (exec_expr ????); 1322 cases Hexpr_sim_lhs 1323 [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/ 1324  *: cases (exec_expr ge en m lhs) 1325 [ 2,4,6,8: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/ 1326  *: * #lval #ltrace #Hsim_lhs normalize nodelta 1327 cases Hexpr_sim_rhs 1328 [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/ 1329  *: cases (exec_expr ge en m rhs) 1330 [ 2,4,6,8: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/ 1331  *: * #rval #rtrace #Hsim_rhs 1332 whd in match (exec_expr ??? (Expr (Ebinop ???) ?)); 1333 >(Hsim_lhs 〈lval,ltrace〉 (refl ? (OK ? 〈lval,ltrace〉))) 1334 >(Hsim_rhs 〈rval,rtrace〉 (refl ? (OK ? 〈rval,rtrace〉))) 1335 normalize nodelta 1336 >Htype_eq_lhs >Htype_eq_rhs 1337 @SimOk * #val #trace #H @H 1338 ] 1339 ] 1340 ] 1341 ] 1342  *: normalize @SimFail /2 by refl, ex_intro/ 1343 ] 1344 (* Jump to the cast cases *) 1345  23,30,31,32,33,34,35,36: %1 try @refl 1346 [ 1,4,7,10,13,16,19,22: destruct // ] 1347 elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq 1348 (* exec_expr simulation *) 1349 [ 1,3,5,7,9,11,13,15: cases Hexec_sim 1350 [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail @SimFail whd in match (exec_expr ge en m ?); 1351 >Hexec_fail /2 by refl, ex_intro/ 1352  1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq 1353 whd in match (exec_expr ge en m ?); #Hstep 1354 cut (∃v1. exec_expr ge en m castee = OK ? 〈v1,trace〉 1355 ∧ exec_cast m v1 (typeof castee) cast_ty = OK ? val) 1356 [ 1,3,5,7,9,11,13,15: 1357 lapply Hstep Hstep cases (exec_expr ge en m castee) 1358 [ 2,4,6,8,10,12,14,16: #error1 normalize nodelta #Hcontr destruct 1359  1,3,5,7,9,11,13,15: * #val1 #trace1 normalize nodelta 1360 #Hstep @(ex_intro … val1) 1361 cases (exec_cast m val1 (typeof castee) cast_ty) in Hstep; 1362 [ 2,4,6,8,10,12,14,16: #error #Hstep normalize in Hstep; destruct 1363  1,3,5,7,9,11,13,15: #result #Hstep normalize in Hstep; destruct 1364 @conj @refl 1365 ] 1366 ] 1367  2,4,6,8,10,12,14,16: * #v1 * #Hexec_expr #Hexec_cast 1368 whd in match (exec_expr ge en m ?); 1369 >(Hsim … Hexec_expr ) normalize nodelta 1370 <Htype_eq >Hexec_cast // 1371 ] 1372 ] 1373  2,4,6,8,10,12,14,16: destruct normalize @SimFail /2/ 1374 ] 1375  24: destruct inversion (Hcastee_inv ge en m) 1376 [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2 1377 <Hresult_flag_2 in Hresult_flag; #Hcontr destruct 1378  2: #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller_eval #_ #Hinv_eq 1379 @(Inv_coerce_ok ??????? cast_sz cast_sg) 1380 [ 1: //  2: <Htype_castee1 // 1381  3: whd in match (exec_expr ??? (Expr ??)); 1382 >Htype_castee 1383 (* Simplify the goal by culling impossible cases, using Hsmaller_val *) 1384 cases (exec_expr ge en m castee) in Hsmaller_eval; 1385 [ 2: #error normalize // 1386  1: * #castee_val #castee_trace cases (exec_expr ge en m castee1) 1387 [ 2: #error normalize #Hcontr @(False_ind … Hcontr) 1388  1: * #castee1_val #castee1_trace #Hsmaller 1389 elim (smaller_integer_val_spec … Hsmaller) 1390 #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle 1391 normalize nodelta destruct whd in match (exec_cast ????); 1392 normalize nodelta >intsize_eq_elim_true whd 1393 >sz_eq_identity >sz_eq_identity whd try @conj try @conj 1394 [ 3: elim (necessary_conditions_spec … (sym_eq … Hconditions)) 1395 [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt) 1396  2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ] 1397  2: @refl 1398  1: @cast_composition // 1399 elim (necessary_conditions_spec … (sym_eq … Hconditions)) (* Clearly suboptimal stuff in this mess *) 1400 [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt) 1401  2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ] 1402 ] 1403 ] 1404 ] 1405 ] 1406 ] 1407  25,27: destruct 1408 inversion (Hcast2 ge en m) 1409 [ 1,3: (* Impossible case. *) 1410 #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult; 1411 #Hcontr destruct 1412  2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself. 1413 We did not successfuly cast the subexpression to target_sz, though. *) 1414 #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq 1415 @(Inv_eq ???????) // 1416 [ 1,4: >Htype_castee2 normalize // 1417  2,5: (* Prove simulation for exec_expr *) 1418 whd in match (exec_expr ??? (Expr ??)); 1419 cases (exec_expr ge en m castee) in Hsmaller_eval; 1420 [ 2,4: (* erroneous evaluation of the original expression *) 1421 #error #Hsmaller_eval @SimFail @(ex_intro … error) 1422 normalize nodelta // 1423  1,3: * #val #trace 1424 cases (exec_expr ge en m castee2) 1425 [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … Hsmaller_eval) 1426  1,3: * #val1 #trace1 #Hsmaller_eval elim (smaller_integer_val_spec … Hsmaller_eval) 1427 #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle 1428 @SimOk * #val2 #trace2 normalize nodelta >Htype_castee 1429 whd in match (exec_cast ????); 1430 cases val in Hint1; normalize nodelta 1431 [ 1,6: #Hint1 destruct  3,4,5,8,9,10: #foo #Hint1 destruct 1432  2,7: destruct cases src_sz in int1; #int1 * #int2 #Hint1 1433 whd in match (intsize_eq_elim ???????); 1434 whd in match (m_bind ?????); 1435 [ 1,5,9,10,14,18: (* correct cases *) destruct #H @H 1436  2,3,4,6,7,8,11,12,13,15,16,17: #Habsurd destruct ] 1437 ] 1438 ] 1439 ] 1440  3,6: normalize @SimFail /2/ 1441 ] 1442 ] 1443  26,28: destruct 1444 inversion (Hcast2 ge en m) 1445 [ 2,4: (* Impossible case. *) 1446 #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #Habsurd #Hinv_eq 1447 (* Do some gymnastic to transform the Habsurd jmeq into a proper, 'destruct'able eq *) 1448 letin Habsurd_eq ≝ (jmeq_to_eq ??? Habsurd) lapply Habsurd_eq 1449 Habsurd_eq Habsurd #Habsurd destruct 1450  1,3: (* All our attempts at casting down the expression have failed. We still use the 1451 resulting expression, as we may have discovered and simplified unrelated casts. *) 1452 #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv 1453 @(Inv_eq ???????) // 1454 [ 1,3: (* Simulation for exec_expr *) 1455 whd in match (exec_expr ??? (Expr ??)); 1456 whd in match (exec_expr ??? (Expr ??)); 1457 cases Hsim_expr 1458 [ 2,4: * #error #Hexec_err >Hexec_err @SimFail @(ex_intro … error) // 1459  1,3: #Hexec_ok 1460 cases (exec_expr ge en m castee) in Hexec_ok; 1461 [ 2,4: #error #Hsim @SimFail normalize nodelta /2/ 1462  1,3: * #val #trace #Hsim normalize nodelta 1463 >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta 1464 @SimOk #a #H @H 1465 ] 1466 ] 1467  2,4: normalize @SimFail /2/ 1468 ] 1469 ] 1470  29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1471 @(Inv_eq ???????) // 1472 whd in match (exec_expr ??? (Expr ??)); 1473 whd in match (exec_expr ??? (Expr ??)); 1474 [ 1: cases Hsim_expr 1475 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2/ 1476  1: #Hexec_ok @SimOk * #val #trace 1477 cases (exec_expr ge en m castee) in Hexec_ok; 1478 [ 2: #error #Habsurd normalize in Habsurd; normalize nodelta #H destruct 1479  1: * #val #trace #Hexec_ok normalize nodelta 1480 >(Hexec_ok … 〈val, trace〉 (refl ? (OK ? 〈val, trace〉))) 1481 >Htype_eq 1482 normalize nodelta #H @H 1483 ] 1484 ] 1485  2: normalize @SimFail /2/ 1486 ] 1487  37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false Hdesired_eq 1488 inversion (Htrue_inv ge en m) 1489 [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false 1490 #Hinv <Hresult_flag_true_eq_false in Hresult_true; >Hdesired_true #Habsurd destruct 1491  2: #true_src_sz #true_src_sg #Htype_eq_true #Htype_eq_true1 #Hsmaller_true #_ #Hinv_true 1492 inversion (Hfalse_inv ge en m) 1493 [ 1: #result_flag_false #Hresult_false #Htype_false #Hsim_expr_false #Hsim_lvalue_false #Hresult_flag_false_eq_false 1494 #Hinv <Hresult_flag_false_eq_false in Hresult_false; >Hdesired_false #Habsurd destruct 1495  2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false 1496 >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg) 1497 [ 1,2: normalize // 1498  3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??)); 1499 elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq 1500 cases Hexec_cond_sim 1501 [ 2: * #error #Herror >Herror normalize @I 1502  1: cases (exec_expr ge en m cond) 1503 [ 2: #error #_ normalize @I 1504  1: * #cond_val #cond_trace #Hcond_sim 1505 >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) 1506 1507 normalize nodelta 1508 >Htype_cond_eq 1509 cases (exec_bool_of_val cond_val (typeof cond1)) * 1510 [ 3,4: normalize // 1511  1,2: normalize in match (m_bind ?????); 1512 normalize in match (m_bind ?????); 1513 Hexec_cond_sim Hcond_sim cond_val 1514 [ 1: (* true branch taken *) 1515 cases (exec_expr ge en m iftrue) in Hsmaller_true; 1516 [ 2: #error #_ @I 1517  1: * #val_true_branch #trace_true_branch 1518 cases (exec_expr ge en m iftrue1) 1519 [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H) 1520  1: * #val_true1_branch #trace_true1_branch #Hsmaller 1521 elim (smaller_integer_val_spec … Hsmaller) 1522 #true_val * #true1_val * * * * #Htrue_val #Htrue1_val #Hcast 1523 #Htrace_eq #Hsize_le normalize nodelta destruct 1524 whd in match (smaller_integer_val ?????); 1525 >sz_eq_identity normalize nodelta 1526 >sz_eq_identity normalize nodelta 1527 try @conj try @conj // ] 1528 ] 1529  2: (* false branch taken. Same proof as above, different arguments ... *) 1530 cases (exec_expr ge en m iffalse) in Hsmaller_false; 1531 [ 2: #error #_ @I 1532  1: * #val_false_branch #trace_false_branch 1533 cases (exec_expr ge en m iffalse1) 1534 [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H) 1535  1: * #val_false1_branch #trace_false1_branch #Hsmaller 1536 elim (smaller_integer_val_spec … Hsmaller) 1537 #false_val * #false1_val * * * * #Hfalse_val #Hfalse1_val #Hcast 1538 #Htrace_eq #Hsize_le normalize nodelta destruct 1539 whd in match (smaller_integer_val ?????); 1540 cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg) 1541 [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq 1542 destruct (Htype_eq) @conj @refl 1543  2: * #Hsize_eq #Hsg_eq destruct 1544 >sz_eq_identity normalize nodelta 1545 >sz_eq_identity normalize nodelta 1546 try @conj try @conj try @refl assumption 1547 ] 1548 ] 1549 ] 1550 ] 1551 ] 1552 ] 1553 ] 1554 ] 1555 ] 1556 ] 1557  38,39,40: destruct 1558 elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq 1559 elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq 1560 elim (Hfalse_equiv ge en m) * #Hsim_expr_false #Hsim_vlalue_false #Htype_false_eq 1561 %1 try @refl 1562 [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 1563 cases (exec_expr ge en m cond) in Hsim_expr_cond; 1564 [ 2,4,6: #error #_ @SimFail /2 by ex_intro/ 1565  1,3,5: * #cond_val #cond_trace normalize nodelta 1566 cases (exec_expr ge en m cond1) 1567 [ 2,4,6: #error * 1568 [ 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) 1569 #Habsurd destruct 1570  *: * #error #Habsurd destruct ] 1571  1,3,5: * #cond_val1 #cond_trace1 * 1572 [ 2,4,6: * #error #Habsurd destruct 1573  1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) 1574 #Hcond_eq normalize nodelta destruct (Hcond_eq) 1575 >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1)) 1576 [ 2,4,6: #error @SimFail normalize /2 by refl, ex_intro / 1577  1,3,5: * (* true branch *) 1578 [ 1,3,5: 1579 normalize in match (m_bind ?????); 1580 normalize in match (m_bind ?????); 1581 cases Hsim_expr_true 1582 [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/ 1583  1,3,5: cases (exec_expr ge en m iftrue) 1584 [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/ 1585  1,3,5: * #val_true #trace_true normalize nodelta #Hsim 1586 >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉))) 1587 normalize nodelta @SimOk #a #H @H 1588 ] 1589 ] 1590  2,4,6: 1591 normalize in match (m_bind ?????); 1592 normalize in match (m_bind ?????); 1593 cases Hsim_expr_false 1594 [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/ 1595  1,3,5: cases (exec_expr ge en m iffalse) 1596 [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/ 1597  1,3,5: * #val_false #trace_false normalize nodelta #Hsim 1598 >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉))) 1599 normalize nodelta @SimOk #a #H @H 1600 ] 1601 ] 1602 ] 1603 ] 1604 ] 1605 ] 1606 ] 1607  2,4,6: normalize @SimFail /2 by ex_intro/ 1608 ] 1609  41,42: destruct 1610 elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs 1611 elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs 1612 %1 try @refl 1613 [ 1,3: whd in match (exec_expr ??? (Expr ??)); 1614 whd in match (exec_expr ??? (Expr ??)); 1615 cases Hsim_expr_lhs 1616 [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/ 1617  1,3: cases (exec_expr ge en m lhs) 1618 [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/ 1619  1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta 1620 >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉))) 1621 normalize nodelta >Htype_eq_lhs 1622 cases (exec_bool_of_val lhs_val (typeof lhs1)) 1623 [ 2,4: #error normalize @SimFail /2 by refl, ex_intro/ 1624  1,3: * 1625 whd in match (m_bind ?????); 1626 whd in match (m_bind ?????); 1627 [ 2,3: (* lhs evaluates to true *) 1628 @SimOk #a #H @H 1629  1,4: cases Hsim_expr_rhs 1630 [ 2,4: * #error #Hexec >Hexec @SimFail /2 by refl, ex_intro/ 1631  1,3: cases (exec_expr ge en m rhs) 1632 [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/ 1633  1,3: * #rhs_val #rhs_trace Hsim #Hsim 1634 >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉))) 1635 normalize nodelta >Htype_eq_rhs 1636 @SimOk #a #H @H 1637 ] 1638 ] 1639 ] 1640 ] 1641 ] 1642 ] 1643  2,4: normalize @SimFail /2 by ex_intro/ 1644 ] 1645  43: destruct 1646 cases (type_eq_dec ty (Tint target_sz target_sg)) 1647 [ 1: #Htype_eq >Htype_eq >type_eq_identity 1648 @(Inv_coerce_ok ??????? target_sz target_sg) 1649 [ 1,2: // 1650  3: cases target_sz cases target_sg normalize try @conj try @conj try @refl try @I ] 1651  2: #Hneq >(type_neq_not_identity … Hneq) 1652 %1 // @SimOk #a #H @H 1653 ] 1654  44: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1655 %1 try @refl 1656 [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 1657 whd in match (exec_lvalue ????) in Hsim_lvalue; 1658 whd in match (exec_lvalue' ?????); 1659 whd in match (exec_lvalue' ?????); 1660 >Htype_eq 1661 cases (typeof rec_expr1) normalize nodelta 1662 [ 2: #sz #sg  3: #fl  4: #rg #ty  5: #rg #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #rg #ty ] 1663 [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/ 1664  6,7: cases Hsim_lvalue 1665 [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/ 1666  1,3: cases (exec_lvalue ge en m rec_expr) 1667 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/ 1668  1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) 1669 whd in match (m_bind ?????); 1670 @SimOk #a #H @H 1671 ] 1672 ] 1673 ] 1674  2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??)); 1675 >Htype_eq 1676 cases (typeof rec_expr1) normalize nodelta 1677 [ 2: #sz #sg  3: #fl  4: #rg #ty  5: #rg #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #rg #ty ] 1678 [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/ 1679  6,7: cases Hsim_lvalue 1680 [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/ 1681  1,3: cases (exec_lvalue ge en m rec_expr) 1682 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/ 1683  1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) 1684 whd in match (m_bind ?????); 1685 @SimOk #a #H @H 1686 ] 1687 ] 1688 ] 1689 ] 1690  45: destruct 1691 inversion (Hinv ge en m) 1692 [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_ 1693 @(Inv_coerce_ok ??????? src_sz src_sg) 1694 [ 1: >Htypeof_e1 // 1695  2: >Htypeof_e2 // 1696  3: whd in match (exec_expr ??? (Expr ??)); 1697 whd in match (exec_expr ??? (Expr ??)); 1698 cases (exec_expr ge en m e1) in Hsmaller; 1699 [ 2: #error normalize // 1700  1: * #val1 #trace1 cases (exec_expr ge en m e2) 1701 [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … Habsurd) 1702  1: * #val2 #trace #Hsmaller 1703 elim (smaller_integer_val_spec … Hsmaller) 1704 #i1 * #i2 * * * * #Hval1 #Hval2 #Hcast #Htrace_eq #Hsize_le 1705 normalize nodelta destruct whd in match (smaller_integer_val ?????); 1706 >sz_eq_identity >sz_eq_identity normalize nodelta 1707 try @conj try @conj try @conj try @refl assumption 1708 ] 1709 ] 1710 ] 1711  1: #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hdesired_typ #_ 1712 >Hresult %1 try @refl 1713 [ 1: >Htype_eq // 1714  2: whd in match (exec_expr ??? (Expr ??)); 1715 whd in match (exec_expr ??? (Expr ??)); 1716 cases Hsim_expr 1717 [ 2: * #error #Hexec_error >Hexec_error normalize nodelta @SimFail /2 by ex_intro/ 1718  1: cases (exec_expr ge en m e1) 1719 [ 2: #error #_ normalize nodelta @SimFail /2 by ex_intro/ 1720  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec 1721 normalize nodelta @SimOk #a #H @H 1722 ] 1723 ] 1724  3: normalize @SimFail /2 by ex_intro/ 1725 ] 1726 ] 1727  46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1728 whd in match (exec_expr ??? (Expr ??)); 1729 whd in match (exec_expr ??? (Expr ??)); 1730 %1 try @refl 1731 [ 1: >Htype_eq // 1732  2: whd in match (exec_expr ??? (Expr ??)); 1733 whd in match (exec_expr ??? (Expr ??)); 1734 cases Hsim_expr 1735 [ 2: * #error #Hexec_error >Hexec_error normalize nodelta @SimFail /2 by ex_intro/ 1736  1: cases (exec_expr ge en m e1) 1737 [ 2: #error #_ normalize nodelta @SimFail /2 by ex_intro/ 1738  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec 1739 normalize nodelta @SimOk #a #H @H 1740 ] 1741 ] 1742  3: normalize @SimFail 1743 ] 1744 1745 1746 1747 1748 1749 1750 1751 76 1752 77 1753 (* simplify_expr [e] [ty'] takes an expression e and a desired type ty', and 78 1754 returns a flag stating whether the desired type was achieved and a simplified 79 1755 version of e. *) 80 81 1756 let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝ 82 1757 match e with … … 85 1760 [ Econst_int sz i ⇒ 86 1761 match ty with 87 [ Tint _sg ⇒1762 [ Tint ty_sz sg ⇒ 88 1763 match ty' with 89 1764 [ Tint sz' sg' ⇒ 90 match simplify_int sz sz' sg sg' i with 91 [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉 92  None ⇒ 〈false, e〉 1765 (* IG: checking that the displayed type size [ty_sz] and [sz] are equal ... *) 1766 match sz_eq_dec sz ty_sz with 1767 [ inl Heq ⇒ 1768 match simplify_int sz sz' sg sg' i with 1769 [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉 1770  None ⇒ 〈false, e〉 1771 ] 1772  inr _ ⇒ 1773 (* The expression is illtyped. *) 1774 〈false, e〉 93 1775 ] 94 1776  _ ⇒ 〈false, e〉 ] … … 195 1877 definition simplify_program : clight_program → clight_program ≝ 196 1878 λp. transform_program … p simplify_fundef. 1879 1880 1881 (* We have to prove that simplify_expr doesn't alter the semantics. Since expressions are pure, 1882 * we state that expressions before and after conversion should evaluate to the same value, or 1883 * fail in a similar way when placed into a given context. *) 1884 1885 1886 let rec expr_ind2 1887 (P : expr → Prop) (Q : expr_descr → Prop) 1888 (IE : ∀ed. ∀t. Q ed → P (Expr ed t)) 1889 (Iconst_int : ∀sz, i. Q (Econst_int sz i)) 1890 (Iconst_float : ∀f. Q (Econst_float f)) 1891 (Ivar : ∀id. Q (Evar id)) 1892 (Ideref : ∀e. P e → Q (Ederef e)) 1893 (Iaddrof : ∀e. P e → Q (Eaddrof e)) 1894 (Iunop : ∀op,arg. P arg → Q (Eunop op arg)) 1895 (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2)) 1896 (Icast : ∀t. ∀e . P e → Q (Ecast t e)) 1897 (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3)) 1898 (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2)) 1899 (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2)) 1900 (Isizeof : ∀t. Q (Esizeof t)) 1901 (Ifield : ∀e,f. P e → Q (Efield e f)) 1902 (Icost : ∀c,e. P e → Q (Ecost c e)) 1903 (e : expr) on e : P e ≝ 1904 match e with 1905 [ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed) ] 1906 1907 and expr_desc_ind2 1908 (P : expr → Prop) (Q : expr_descr → Prop) 1909 (IE : ∀ed. ∀t. Q ed → P (Expr ed t)) 1910 (Iconst_int : ∀sz, i. Q (Econst_int sz i)) 1911 (Iconst_float : ∀f. Q (Econst_float f)) 1912 (Ivar : ∀id. Q (Evar id)) 1913 (Ideref : ∀e. P e → Q (Ederef e)) 1914 (Iaddrof : ∀e. P e → Q (Eaddrof e)) 1915 (Iunop : ∀op,arg. P arg → Q (Eunop op arg)) 1916 1917 (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2)) 1918 (Icast : ∀t. ∀e . P e → Q (Ecast t e)) 1919 (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3)) 1920 (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2)) 1921 (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2)) 1922 (Isizeof : ∀t. Q (Esizeof t)) 1923 (Ifield : ∀e,f. P e → Q (Efield e f)) 1924 (Icost : ∀c,e. P e → Q (Ecost c e)) 1925 (ed : expr_descr) on ed : Q ed ≝ 1926 match ed with 1927 [ Econst_int sz i ⇒ Iconst_int sz i 1928  Econst_float f ⇒ Iconst_float f 1929  Evar id ⇒ Ivar id 1930  Ederef e ⇒ Ideref e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 1931  Eaddrof e ⇒ Iaddrof e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 1932  Eunop op e ⇒ Iunop op e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 1933  Ebinop op e1 e2 ⇒ Ibinop op e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) 1934  Ecast t e ⇒ Icast t e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 1935  Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e3) 1936  Eandbool e1 e2 ⇒ Iandbool e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) 1937  Eorbool e1 e2 ⇒ Iorbool e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) 1938  Esizeof t ⇒ Isizeof t 1939  Efield e field ⇒ Ifield e field (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 1940  Ecost c e ⇒ Icost c e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof
Note: See TracChangeset
for help on using the changeset viewer.