[1198] | 1 | include "Clight/Csyntax.ma". |
---|
| 2 | include "Clight/TypeComparison.ma". |
---|
| 3 | |
---|
[1970] | 4 | (* IG: used to prove preservation of the semantics. *) |
---|
| 5 | include "Clight/Cexec.ma". |
---|
| 6 | include "Clight/casts.ma". |
---|
[2030] | 7 | include "Clight/CexecSound.ma". |
---|
[1970] | 8 | |
---|
[2441] | 9 | include "Clight/frontend_misc.ma". |
---|
[2030] | 10 | |
---|
[2441] | 11 | |
---|
[1970] | 12 | (* include "ASM/AssemblyProof.ma". *) (* I had to manually copy some of the lemmas in this file, including an axiom ... *) |
---|
| 13 | |
---|
[1198] | 14 | (* Attempt to remove unnecessary integer casts in Clight programs. |
---|
| 15 | |
---|
| 16 | This differs from the OCaml prototype by attempting to recursively determine |
---|
| 17 | whether subexpressions can be changed rather than using a fixed size pattern. |
---|
| 18 | As a result more complex expressions such as (char)((int)x + (int)y + (int)z) |
---|
| 19 | where x,y and z are chars can be simplified. |
---|
| 20 | |
---|
| 21 | A possible improvement that doesn't quite fit into this scheme would be to |
---|
| 22 | spot that casts can be removed in expressions like (int)x == (int)y where |
---|
| 23 | x and y have some smaller integer type. |
---|
| 24 | *) |
---|
| 25 | |
---|
| 26 | (* Attempt to squeeze integer constant into a given type. |
---|
| 27 | |
---|
| 28 | This might be too conservative --- if we're going to cast it anyway, can't |
---|
[2011] | 29 | I just ignore the fact that the integer doesn't fit? |
---|
[1970] | 30 | *) |
---|
[1198] | 31 | |
---|
[1970] | 32 | (* [reduce_bits n m exp v] takes avector of size n + m + 1 and returns (if all goes well) a vector of size |
---|
| 33 | * m+1 (an empty vector of bits makes no sense). It proceeds by removing /all/ the [n] leading bits equal |
---|
| 34 | * to [exp]. If it fails, it returns None. *) |
---|
[1198] | 35 | let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝ |
---|
| 36 | match n return λn. BitVector (n+S m) → option (BitVector (S m)) with |
---|
| 37 | [ O ⇒ λv. Some ? v |
---|
| 38 | | S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ? |
---|
| 39 | ] v. |
---|
| 40 | |
---|
[1970] | 41 | 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'. |
---|
| 42 | #n #m #exp #v #v' #H whd in H:(??%?); lapply H -H |
---|
| 43 | cases (eq_b ? exp) |
---|
| 44 | [ 1: #H whd in H:(??%?); // |
---|
| 45 | | 2: #H normalize in H; destruct ] qed. |
---|
| 46 | |
---|
| 47 | lemma reduce_bits_trunc : ∀n,m.∀exp.∀v:(BitVector (plus n (S m))).∀v'. |
---|
| 48 | reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v. |
---|
| 49 | #n #m elim n |
---|
[2032] | 50 | [ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >vsplit_O_n // |
---|
[1970] | 51 | | 2: #n' #Hind #exp #v #v' #H >truncate_tail |
---|
| 52 | > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed. |
---|
| 53 | |
---|
| 54 | lemma reduce_bits_dec : ∀n,m.∀exp.∀v. (∃v'.reduce_bits n m exp v = Some ? v') ∨ reduce_bits n m exp v = None ?. |
---|
| 55 | #n #m #exp #v elim (reduce_bits n m exp v) |
---|
| 56 | [ 1: %2 // |
---|
| 57 | | 2: #v' %1 @(ex_intro … v') // ] qed. |
---|
| 58 | |
---|
| 59 | (* pred_bitsize_of_intsize I32 = 31, … *) |
---|
[1198] | 60 | definition pred_bitsize_of_intsize : intsize → nat ≝ |
---|
[1873] | 61 | λsz. pred (bitsize_of_intsize sz). |
---|
[1198] | 62 | |
---|
| 63 | definition signed : signedness → bool ≝ |
---|
| 64 | λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ]. |
---|
| 65 | |
---|
[1970] | 66 | (* [simplify_int sz sz' sg sg' i] tries to convert an integer [i] of width [sz] and signedness [sg] |
---|
| 67 | * into an integer of size [sz'] of signedness [sg']. |
---|
| 68 | * - It first proceeds by comparing the source and target width: if the target width is strictly superior |
---|
| 69 | * to the source width, the conversion fails. |
---|
| 70 | * - If the size is equal, the argument is returned as-is. |
---|
| 71 | * - If the target type is strictly smaller than the source, it tries to squeeze the integer to |
---|
| 72 | * the desired size. |
---|
| 73 | *) |
---|
[1198] | 74 | let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝ |
---|
| 75 | let bit ≝ signed sg ∧ head' … i in |
---|
[1970] | 76 | (* [nat_compare] does more than an innocent post-doc might think. It also computes the difference between the two args. |
---|
| 77 | * if x < y, nat_compare x y = lt(x, y-(x+1)) |
---|
| 78 | * if x = y, nat_compare x y = eq x |
---|
| 79 | * if x > y, nat_compare x y = gt(x-(y+1), y) *) |
---|
[1198] | 80 | match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz') |
---|
| 81 | return λn,m,x.BitVector (S n) → option (BitVector (S m)) with |
---|
| 82 | [ nat_lt _ _ ⇒ λi. None ? (* refuse to make constants larger *) |
---|
| 83 | | nat_eq _ ⇒ λi. Some ? i |
---|
[1970] | 84 | | nat_gt x y ⇒ λi. |
---|
| 85 | (* 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. |
---|
| 86 | * 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), |
---|
| 87 | * we deduce that the actual arguments of [reduce_bits] are (S x) and (S y), which is consistent. |
---|
| 88 | * If [i] is of signed type and if it is negative, then it tries to remove the (S x) first "1" bits. |
---|
| 89 | * Otherwise, it tries to remove the (S x) first "0" bits. |
---|
| 90 | *) |
---|
[1198] | 91 | match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with |
---|
[1970] | 92 | [ Some i' ⇒ |
---|
| 93 | if signed sg' then |
---|
| 94 | if eq_b bit (head' … i') then |
---|
| 95 | Some ? i' |
---|
| 96 | else None ? |
---|
| 97 | else Some ? i' |
---|
[1198] | 98 | | None ⇒ None ? |
---|
| 99 | ] |
---|
| 100 | ] i. |
---|
| 101 | >(commutative_plus_faster (S x)) @refl |
---|
| 102 | qed. |
---|
| 103 | |
---|
| 104 | |
---|
[1970] | 105 | lemma eq_intsize_identity : ∀id. eq_intsize id id = true. |
---|
| 106 | * normalize // |
---|
| 107 | qed. |
---|
| 108 | |
---|
| 109 | lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s). |
---|
| 110 | * normalize // |
---|
| 111 | qed. |
---|
| 112 | |
---|
| 113 | lemma type_eq_identity : ∀t. type_eq t t = true. |
---|
| 114 | #t normalize elim (type_eq_dec t t) |
---|
| 115 | [ 1: #Heq normalize // |
---|
| 116 | | 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed. |
---|
| 117 | |
---|
| 118 | lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false. |
---|
| 119 | #t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2) |
---|
| 120 | [ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2)) |
---|
| 121 | | 2: #Hneq' normalize // ] qed. |
---|
| 122 | |
---|
| 123 | definition size_le ≝ λsz1,sz2. |
---|
| 124 | match sz1 with |
---|
| 125 | [ I8 ⇒ True |
---|
| 126 | | I16 ⇒ |
---|
| 127 | match sz2 with |
---|
| 128 | [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ] |
---|
| 129 | | I32 ⇒ |
---|
| 130 | match sz2 with |
---|
| 131 | [ I32 ⇒ True | _ ⇒ False ] |
---|
| 132 | ]. |
---|
| 133 | |
---|
| 134 | definition size_lt ≝ λsz1,sz2. |
---|
| 135 | match sz1 with |
---|
| 136 | [ I8 ⇒ |
---|
| 137 | match sz2 with |
---|
| 138 | [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ] |
---|
| 139 | | I16 ⇒ |
---|
| 140 | match sz2 with |
---|
| 141 | [ I32 ⇒ True | _ ⇒ False ] |
---|
| 142 | | I32 ⇒ False |
---|
| 143 | ]. |
---|
| 144 | |
---|
[2030] | 145 | lemma size_lt_to_le : ∀sz1,sz2. size_lt sz1 sz2 → size_le sz1 sz2. |
---|
| 146 | #sz1 #sz2 elim sz1 elim sz2 normalize // qed. |
---|
| 147 | |
---|
[1970] | 148 | lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)). |
---|
| 149 | * * normalize /2/ /3/ |
---|
| 150 | qed. |
---|
| 151 | |
---|
| 152 | lemma size_not_lt_to_ge : ∀sz1,sz2. ¬(size_lt sz1 sz2) → (sz1 = sz2) + (size_lt sz2 sz1). |
---|
| 153 | * * normalize /2/ /3/ |
---|
| 154 | qed. |
---|
| 155 | |
---|
| 156 | (* This function already exists in prop, we want it in type. *) |
---|
| 157 | definition sign_eq_dect : ∀sg1,sg2:signedness. (sg1 = sg2) + (sg1 ≠ sg2). |
---|
| 158 | * * normalize // qed. |
---|
| 159 | |
---|
| 160 | lemma size_absurd : ∀a,b. size_le a b → size_lt b a → False. |
---|
| 161 | * * normalize |
---|
| 162 | #H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed. |
---|
| 163 | |
---|
| 164 | (* This defines necessary conditions for [src_expr] to be coerced to "target_ty". |
---|
| 165 | * Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *) |
---|
| 166 | definition necessary_conditions ≝ λsrc_sz.λsrc_sg.λtarget_sz.λtarget_sg. |
---|
| 167 | match size_lt_dec target_sz src_sz with |
---|
| 168 | [ inl Hlt ⇒ true |
---|
| 169 | | inr Hnlt ⇒ |
---|
| 170 | match sz_eq_dec target_sz src_sz with |
---|
| 171 | [ inl Hsz_eq ⇒ |
---|
| 172 | match sign_eq_dect src_sg target_sg with |
---|
| 173 | [ inl Hsg_eq ⇒ false |
---|
| 174 | | inr Hsg_neq ⇒ true |
---|
| 175 | ] |
---|
| 176 | | inr Hsz_neq ⇒ false |
---|
| 177 | ] |
---|
| 178 | ]. |
---|
| 179 | |
---|
[2009] | 180 | (* Inversion on necessary_conditions *) |
---|
[1970] | 181 | lemma necessary_conditions_spec : |
---|
| 182 | ∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) → |
---|
| 183 | ((size_lt target_sz src_sz) ∨ (src_sz = target_sz ∧ src_sg ≠ target_sg)). |
---|
| 184 | #src_sz #src_sg #target_sz #target_sg |
---|
| 185 | whd in match (necessary_conditions ????); |
---|
| 186 | cases (size_lt_dec target_sz src_sz) normalize nodelta |
---|
| 187 | [ 1: #Hlt #_ %1 // |
---|
| 188 | | 2: #Hnlt |
---|
| 189 | cases (sz_eq_dec target_sz src_sz) normalize nodelta |
---|
| 190 | [ 2: #_ #Hcontr destruct |
---|
| 191 | | 1: #Heq cases (sign_eq_dect src_sg target_sg) normalize nodelta |
---|
| 192 | [ 1: #_ #Hcontr destruct |
---|
| 193 | | 2: #Hsg_neq #_ %2 destruct /2/ ] |
---|
| 194 | ] |
---|
[2030] | 195 | ] qed. |
---|
[1970] | 196 | |
---|
| 197 | (* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an |
---|
| 198 | * integer value smaller but containing the same stuff than [r2] then all is well. |
---|
[2011] | 199 | * If the first evaluation is erroneous, we don't care about anything else. *) |
---|
[2030] | 200 | definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res(val×trace). |
---|
[1970] | 201 | match r1 with |
---|
| 202 | [ OK res1 ⇒ |
---|
[2030] | 203 | let 〈val1, tr1〉 ≝ res1 in |
---|
| 204 | ∀v1. val1 = Vint src_sz v1 → |
---|
[1970] | 205 | match r2 with |
---|
[2030] | 206 | [ OK res2 ⇒ |
---|
| 207 | let 〈val2, tr2〉 ≝ res2 in |
---|
| 208 | ∃v2. (val2 = Vint dst_sz v2 ∧ |
---|
| 209 | v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz) |
---|
[1970] | 210 | | _ ⇒ False ] |
---|
[2030] | 211 | | Error errmsg1 ⇒ True |
---|
[1970] | 212 | ]. |
---|
| 213 | |
---|
[2009] | 214 | (* Simulation relation used for expression evaluation. *) |
---|
[2074] | 215 | inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝ |
---|
| 216 | | SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2 |
---|
| 217 | | SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2. |
---|
[1970] | 218 | |
---|
[2219] | 219 | (* Trick to reduce checking time by eliminating a load of costly automation. |
---|
| 220 | It would be nice to do this by refactoring the type and code instead, but we |
---|
| 221 | don't want to spend lots of time on something that already works. *) |
---|
| 222 | |
---|
| 223 | lemma SimFailNicely : ∀A,err,r2. res_sim A (Error ? err) r2. |
---|
| 224 | #A #err #r2 @SimFail %{err} % |
---|
| 225 | qed. |
---|
| 226 | |
---|
[2009] | 227 | (* Invariant of simplify_expr *) |
---|
[1970] | 228 | inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝ |
---|
[2009] | 229 | (* Inv_eq states a standard simulation result. We enforce some needed equations on types to prove the cast cases. *) |
---|
[1970] | 230 | | Inv_eq : ∀result_flag. |
---|
| 231 | result_flag = false → |
---|
| 232 | typeof e1 = typeof e2 → |
---|
[2074] | 233 | res_sim ? (exec_expr ge en m e1) (exec_expr ge en m e2) → |
---|
| 234 | res_sim ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) → |
---|
[1970] | 235 | simplify_inv ge en m e1 e2 target_sz target_sg result_flag |
---|
[2009] | 236 | (* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *) |
---|
[1970] | 237 | | Inv_coerce_ok : ∀src_sz,src_sg. |
---|
| 238 | (typeof e1) = (Tint src_sz src_sg) → |
---|
| 239 | (typeof e2) = (Tint target_sz target_sg) → |
---|
| 240 | (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) → |
---|
| 241 | simplify_inv ge en m e1 e2 target_sz target_sg true. |
---|
[2009] | 242 | |
---|
[2030] | 243 | (* Invariant of simplify_inside *) |
---|
[2009] | 244 | definition conservation ≝ λe,result:expr. |
---|
[2074] | 245 | ∀ge,en,m. res_sim ? (exec_expr ge en m e) (exec_expr ge en m result) |
---|
| 246 | ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) |
---|
[2009] | 247 | ∧ typeof e = typeof result. |
---|
[1970] | 248 | |
---|
[2009] | 249 | (* This lemma proves that simplify_int actually implements an integer cast. *) |
---|
| 250 | (* The case 4 can be merged with cases 7 and 8. *) |
---|
| 251 | |
---|
[1970] | 252 | 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. |
---|
| 253 | * * |
---|
| 254 | [ 1: #sg #sg' #i #i' #Hsimp normalize in Hsimp ⊢ %; elim sg normalize destruct // |
---|
| 255 | | 2,3,6: #sg #sg' #i #i' #Hsimp normalize in Hsimp; destruct (* ⊢ %; destruct destruct whd in Hsimp:(??%?); destruct *) |
---|
| 256 | | 4: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %; |
---|
| 257 | normalize in match (signed ?) in Hsimp; |
---|
| 258 | normalize in match (S (plus ??)) in Hsimp; |
---|
| 259 | normalize in match (plus 7 8) in Hsimp; |
---|
| 260 | lapply Hsimp -Hsimp |
---|
| 261 | cases (head' bool 15 i) |
---|
| 262 | normalize in match (andb ??); |
---|
| 263 | [ 1,3: elim (reduce_bits_dec 8 7 true i) |
---|
| 264 | [ 1,3: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta |
---|
| 265 | [ 1: cases (eq_b true ?) normalize #H destruct normalize @refl |
---|
| 266 | | 2: #H destruct normalize @refl ] |
---|
| 267 | | 2,4: #Heq >Heq normalize nodelta #H destruct ] |
---|
| 268 | | 2,4,5,6,7,8: |
---|
| 269 | elim (reduce_bits_dec 8 7 false i) |
---|
| 270 | [ 1,3,5,7,9,11: * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq) |
---|
| 271 | [ 1,3,4: cases (eq_b false ?) normalize nodelta |
---|
| 272 | #H destruct normalize @refl |
---|
| 273 | | 2,5,6: #H destruct normalize @refl ] |
---|
| 274 | | 2,4,6,8,10,12: #Heq >Heq normalize nodelta #H destruct |
---|
[1198] | 275 | ] |
---|
[1970] | 276 | ] |
---|
| 277 | | 5,9: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); destruct @refl |
---|
| 278 | | 7, 8: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %; |
---|
| 279 | normalize in match (signed ?) in Hsimp; |
---|
| 280 | normalize in match (S (plus ??)) in Hsimp; |
---|
| 281 | normalize in match (plus 7 24) in Hsimp; |
---|
| 282 | lapply Hsimp -Hsimp |
---|
| 283 | cases (head' bool ? i) |
---|
| 284 | normalize in match (andb ??); |
---|
| 285 | [ 1,3,9,11: |
---|
| 286 | [ 1,2: (elim (reduce_bits_dec 24 7 true i)) | 3,4: (elim (reduce_bits_dec 16 15 true i)) ] |
---|
| 287 | [ 1,3,5,7: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta |
---|
| 288 | [ 1,3: cases (eq_b true ?) normalize #H destruct normalize @refl |
---|
| 289 | | 2,4: #H destruct normalize @refl ] |
---|
| 290 | | 2,4,6,8: #Heq >Heq normalize nodelta #H destruct ] |
---|
| 291 | | 2,4,5,6,7,8,10,12,13,14,15,16: |
---|
| 292 | [ 1,2,3,4,5,6: elim (reduce_bits_dec 24 7 false i) |
---|
| 293 | | 6,7,8,9,10,11,12: elim (reduce_bits_dec 16 15 false i) ] |
---|
| 294 | [ 1,3,5,7,9,11,13,15,17,19,21,23: |
---|
| 295 | * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq) |
---|
| 296 | [ 1,3,4,7,9,10: |
---|
| 297 | cases (eq_b false ?) normalize nodelta #H destruct normalize @refl |
---|
| 298 | | 2,5,6,8,11,12: #H destruct normalize @refl ] |
---|
| 299 | | 2,4,6,8,10,12,14,16,18,20,22,24: #Heq >Heq normalize nodelta #H destruct |
---|
| 300 | ] |
---|
| 301 | ] |
---|
| 302 | ] qed. |
---|
| 303 | |
---|
| 304 | (* Facts about cast_int_int *) |
---|
| 305 | |
---|
| 306 | |
---|
| 307 | 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)). |
---|
| 308 | #s1 #v normalize elim s1 normalize nodelta |
---|
| 309 | normalize in v; |
---|
[2032] | 310 | elim (vsplit_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) |
---|
[1970] | 311 | [ 2,4: // |
---|
| 312 | | 1,3: #l * #r normalize nodelta #Eq1 |
---|
[2032] | 313 | <(vsplit_prod bool 16 16 … Eq1) |
---|
| 314 | elim (vsplit_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) |
---|
[1970] | 315 | [ 2,4: // |
---|
| 316 | | 1,3: #lr * #rr normalize nodelta #Eq2 |
---|
[2032] | 317 | <(vsplit_prod bool 8 8 … Eq2) |
---|
[1970] | 318 | cut (v = (l @@ lr) @@ rr) |
---|
| 319 | [ 1,3 : destruct >(vector_associative_append ? 16 8) // |
---|
| 320 | | 2,4: #Hrewrite destruct |
---|
[2032] | 321 | <(vsplit_prod bool 24 8 … Hrewrite) @refl |
---|
[1970] | 322 | ] |
---|
| 323 | ] |
---|
| 324 | ] qed. |
---|
| 325 | |
---|
| 326 | 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. |
---|
| 327 | #s1 #s2 * * #v elim s1 elim s2 |
---|
| 328 | normalize #H try @refl |
---|
| 329 | @(False_ind … H) |
---|
| 330 | qed. |
---|
| 331 | |
---|
| 332 | lemma cast_identity : ∀sz,sg,v. cast_int_int sz sg sz v = v. |
---|
| 333 | * * #v normalize // qed. |
---|
| 334 | |
---|
| 335 | 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). |
---|
| 336 | #s1 #s2 #v >cast_decompose >cast_idempotent |
---|
| 337 | [ 1: @refl | 2: // ] |
---|
| 338 | qed. |
---|
| 339 | |
---|
| 340 | lemma cast_composition_lt : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val. |
---|
| 341 | size_lt c_sz a_sz → size_lt c_sz b_sz → |
---|
| 342 | (cast_int_int a_sz a_sg c_sz val = |
---|
| 343 | cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)). |
---|
| 344 | * #a_sg * #b_sg * #val whd in match (size_lt ??); whd in match (size_lt ??); |
---|
| 345 | #Hlt1 #Hlt2 |
---|
| 346 | [ 1,2,3,4,5,6,7,8,9,10,11,12,14,15,17,18,19,20,21,23,24,27: |
---|
| 347 | @(False_ind … Hlt1) @(False_ind … Hlt2) |
---|
| 348 | | 13,25,26: >cast_identity elim a_sg elim b_sg normalize // |
---|
| 349 | | 22: normalize elim b_sg elim a_sg normalize |
---|
| 350 | normalize in val; |
---|
[2032] | 351 | elim (vsplit_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) |
---|
[1970] | 352 | [ 2,4,6,8: normalize // |
---|
| 353 | | 1,3,5,7: #left * #right normalize #Eq1 |
---|
[2032] | 354 | <(vsplit_prod bool 16 16 … Eq1) |
---|
| 355 | elim (vsplit_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) |
---|
[1970] | 356 | [ 2,4,6,8: // |
---|
| 357 | | 1,3,5,7: #rightleft * #rightright normalize #Eq2 |
---|
[2032] | 358 | <(vsplit_prod bool 8 8 … Eq2) |
---|
[1970] | 359 | cut (val = (left @@ rightleft) @@ rightright) |
---|
| 360 | [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) // |
---|
| 361 | | 2,4,6,8: #Hrewrite destruct |
---|
[2032] | 362 | <(vsplit_prod bool 24 8 … Hrewrite) @refl |
---|
[1970] | 363 | ] |
---|
| 364 | ] |
---|
| 365 | ] |
---|
| 366 | | 16: elim b_sg elim a_sg >cast_collapse @refl |
---|
| 367 | ] qed. |
---|
| 368 | |
---|
| 369 | lemma cast_composition : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val. |
---|
| 370 | size_le c_sz a_sz → size_le c_sz b_sz → |
---|
| 371 | (cast_int_int a_sz a_sg c_sz val = |
---|
| 372 | cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)). |
---|
| 373 | #a_sz #a_sg #b_sz #b_sg #c_sz #val #Hle_c_a #Hle_c_b |
---|
| 374 | cases (size_lt_dec c_sz a_sz) |
---|
| 375 | cases (size_lt_dec c_sz b_sz) |
---|
| 376 | [ 1: #Hltb #Hlta @(cast_composition_lt … Hlta Hltb) |
---|
| 377 | | 2: #Hnltb #Hlta |
---|
| 378 | cases (size_not_lt_to_ge … Hnltb) |
---|
| 379 | [ 1: #Heq destruct >cast_identity // |
---|
| 380 | | 2: #Hltb @(False_ind … (size_absurd ?? Hle_c_b Hltb)) |
---|
| 381 | ] |
---|
| 382 | | 3: #Hltb #Hnlta |
---|
| 383 | cases (size_not_lt_to_ge … Hnlta) |
---|
| 384 | [ 1: #Heq destruct >cast_idempotent // |
---|
| 385 | | 2: #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) |
---|
| 386 | ] |
---|
| 387 | | 4: #Hnltb #Hnlta |
---|
| 388 | cases (size_not_lt_to_ge … Hnlta) |
---|
| 389 | cases (size_not_lt_to_ge … Hnltb) |
---|
| 390 | [ 1: #Heq_b #Heq_a destruct >cast_identity >cast_identity // |
---|
| 391 | | 2: #Hltb #Heq @(False_ind … (size_absurd ?? Hle_c_b Hltb)) |
---|
| 392 | | 3: #Eq #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) |
---|
| 393 | | 4: #Hltb #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) |
---|
| 394 | ] |
---|
| 395 | ] qed. |
---|
| 396 | |
---|
| 397 | let rec assert_int_value (v : option val) (expected_size : intsize) : option (BitVector (bitsize_of_intsize expected_size)) ≝ |
---|
| 398 | match v with |
---|
| 399 | [ None ⇒ None ? |
---|
| 400 | | Some v ⇒ |
---|
| 401 | match v with |
---|
| 402 | [ Vint sz i ⇒ |
---|
| 403 | match sz_eq_dec sz expected_size with |
---|
| 404 | [ inl Heq ⇒ Some ?? |
---|
| 405 | | inr _ ⇒ None ? |
---|
| 406 | ] |
---|
| 407 | | _ ⇒ None ? |
---|
| 408 | ] |
---|
[1198] | 409 | ]. |
---|
[1970] | 410 | >Heq in i; #i @i qed. |
---|
[1198] | 411 | |
---|
[2032] | 412 | (* cast_int_int behaves as truncate (≃ vsplit) when downsizing *) |
---|
[1970] | 413 | (* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *) |
---|
| 414 | |
---|
[2032] | 415 | lemma vsplit_to_truncate : ∀m,n,i. (\snd (vsplit bool m n i)) = truncate m n i. |
---|
[1970] | 416 | #m #n #i normalize // qed. |
---|
| 417 | |
---|
| 418 | (* Somme lemmas on how "simplifiable" operations behave under cast_int_int. *) |
---|
| 419 | |
---|
| 420 | lemma integer_add_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz → |
---|
| 421 | (addition_n (bitsize_of_intsize target_sz) |
---|
| 422 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
| 423 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
| 424 | = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
| 425 | #src_sz #target_sz #sg #lhs_int #rhs_int #Hlt |
---|
| 426 | elim src_sz in Hlt lhs_int rhs_int; elim target_sz |
---|
| 427 | [ 1,2,3,5,6,9: normalize #H @(False_ind … H) |
---|
| 428 | | *: elim sg #_ |
---|
| 429 | normalize in match (bitsize_of_intsize ?); |
---|
| 430 | normalize in match (bitsize_of_intsize ?); |
---|
| 431 | #lint #rint |
---|
| 432 | normalize in match (cast_int_int ????); |
---|
| 433 | normalize in match (cast_int_int ????); |
---|
| 434 | whd in match (addition_n ???); |
---|
| 435 | whd in match (addition_n ???) in ⊢ (???%); |
---|
[2032] | 436 | >vsplit_to_truncate >vsplit_to_truncate |
---|
[1970] | 437 | <truncate_add_with_carries |
---|
| 438 | [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false); |
---|
| 439 | | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint rint false); |
---|
| 440 | | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint rint false); |
---|
| 441 | ] |
---|
| 442 | * #result #carry |
---|
| 443 | normalize nodelta // |
---|
| 444 | qed. |
---|
| 445 | |
---|
| 446 | lemma integer_add_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz → |
---|
| 447 | (addition_n (bitsize_of_intsize target_sz) |
---|
| 448 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
| 449 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
| 450 | = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
| 451 | #src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct |
---|
| 452 | >cast_identity >cast_identity >cast_identity // qed. |
---|
| 453 | |
---|
| 454 | lemma integer_add_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz → |
---|
| 455 | (addition_n (bitsize_of_intsize target_sz) |
---|
| 456 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
| 457 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
| 458 | = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
| 459 | #src_sz #target_sz #sg #lhs_int #rhs_int #Hle |
---|
| 460 | cases (sz_eq_dec target_sz src_sz) |
---|
| 461 | [ 1: #Heq @(integer_add_cast_eq … Heq) |
---|
| 462 | | 2: #Hneq cut (size_lt target_sz src_sz) |
---|
| 463 | [ 1: elim target_sz in Hle Hneq; elim src_sz normalize // |
---|
| 464 | #_ * #H @(H … (refl ??)) |
---|
| 465 | | 2: #Hlt @(integer_add_cast_lt … Hlt) |
---|
| 466 | ] |
---|
| 467 | ] qed. |
---|
| 468 | |
---|
| 469 | lemma truncate_eat : ∀l,n,m,v. l = n → ∃tl. truncate (S n) m v = truncate l m tl. |
---|
| 470 | #l #n #m #v #len elim (Vector_Sn … v) #hd * #tl #Heq >len |
---|
| 471 | @(ex_intro … tl) |
---|
| 472 | >Heq >Heq |
---|
[2032] | 473 | elim (vsplit_eq2 … tl) #l * #r #Eq |
---|
[1970] | 474 | normalize |
---|
[2032] | 475 | <(vsplit_prod bool n m tl l r Eq) |
---|
| 476 | <(vsplit_prod2 bool n m tl l r Eq) |
---|
[1970] | 477 | normalize // |
---|
| 478 | qed. |
---|
| 479 | |
---|
| 480 | |
---|
| 481 | 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). |
---|
| 482 | #m elim m |
---|
| 483 | [ 1: #n #i normalize in i; |
---|
| 484 | whd in match (truncate ???); |
---|
| 485 | whd in match (truncate ???) in ⊢ (???%); |
---|
[2032] | 486 | <vsplit_zero <vsplit_zero // |
---|
[1970] | 487 | | 2: #m' #Hind #n #i normalize in i; |
---|
| 488 | elim (Vector_Sn … i) #hd * #tl #Heq |
---|
| 489 | whd in match (two_complement_negation (S ?) ?); |
---|
| 490 | >Heq in ⊢ (??%?); >truncate_tail whd in match (tail ???) in ⊢ (??%?); |
---|
| 491 | whd in match (two_complement_negation ??) in ⊢ (??%?); |
---|
| 492 | lapply (Hind ? tl) #H |
---|
| 493 | whd in match (two_complement_negation ??) in H; |
---|
[2030] | 494 | (* trying to reduce add_with_carries *) |
---|
[1970] | 495 | normalize in match (S m'+n); |
---|
| 496 | whd in match (zero ?) in ⊢ (???%); |
---|
| 497 | >Heq in match (negation_bv ??) in ⊢ (???%); |
---|
| 498 | whd in match (negation_bv ??) in ⊢ (???%); |
---|
| 499 | >add_with_carries_unfold in ⊢ (???%); |
---|
| 500 | normalize in ⊢ (???%); |
---|
| 501 | cases hd normalize nodelta |
---|
| 502 | [ 1,2: <add_with_carries_unfold in ⊢ (???%); (* Good. Some progress. *) |
---|
| 503 | (* try to transform the rhs of H into what we need. *) |
---|
| 504 | whd in match (two_complement_negation ??) in H:(???%); |
---|
| 505 | lapply H -H |
---|
| 506 | generalize in match (add_with_carries (m'+n) (negation_bv (m'+n) tl) (zero (m'+n)) true); |
---|
| 507 | * #Left #Right normalize nodelta |
---|
| 508 | #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ? | _ ⇒ ?]))))); |
---|
[2032] | 509 | #b >(vsplit_to_truncate (S m')) >truncate_tail |
---|
[1970] | 510 | cases b |
---|
| 511 | normalize nodelta |
---|
| 512 | normalize in match (tail ???); @H |
---|
| 513 | ] |
---|
| 514 | ] qed. (* This was painful. *) |
---|
| 515 | |
---|
| 516 | lemma integer_sub_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz → |
---|
| 517 | (subtraction (bitsize_of_intsize target_sz) |
---|
| 518 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
| 519 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
| 520 | = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
| 521 | #src_sz #target_sz #sg #lhs_int #rhs_int #Hlt |
---|
| 522 | elim src_sz in Hlt lhs_int rhs_int; elim target_sz |
---|
| 523 | [ 1,2,3,5,6,9: normalize #H @(False_ind … H) |
---|
| 524 | | *: elim sg #_ |
---|
| 525 | normalize in match (bitsize_of_intsize ?); |
---|
| 526 | normalize in match (bitsize_of_intsize ?); |
---|
| 527 | #lint #rint |
---|
| 528 | normalize in match (cast_int_int ????); |
---|
| 529 | normalize in match (cast_int_int ????); |
---|
| 530 | whd in match (subtraction ???); |
---|
| 531 | whd in match (subtraction ???) in ⊢ (???%); |
---|
[2032] | 532 | >vsplit_to_truncate >vsplit_to_truncate |
---|
[1970] | 533 | >integer_neg_trunc <truncate_add_with_carries |
---|
| 534 | [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false); |
---|
| 535 | | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint ? false); |
---|
| 536 | | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint ? false); |
---|
| 537 | ] |
---|
| 538 | * #result #carry |
---|
| 539 | normalize nodelta // |
---|
| 540 | qed. |
---|
| 541 | |
---|
| 542 | lemma integer_sub_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz → |
---|
| 543 | (subtraction (bitsize_of_intsize target_sz) |
---|
| 544 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
| 545 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
| 546 | = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
| 547 | #src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct |
---|
| 548 | >cast_identity >cast_identity >cast_identity // |
---|
| 549 | qed. |
---|
| 550 | |
---|
| 551 | lemma integer_sub_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz → |
---|
| 552 | (subtraction (bitsize_of_intsize target_sz) |
---|
| 553 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
| 554 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
| 555 | = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
| 556 | #src_sz #target_sz #sg #lhs_int #rhs_int #Hle |
---|
| 557 | cases (sz_eq_dec target_sz src_sz) |
---|
| 558 | [ 1: #Heq @(integer_sub_cast_eq … Heq) |
---|
| 559 | | 2: #Hneq cut (size_lt target_sz src_sz) |
---|
| 560 | [ 1: elim target_sz in Hle Hneq; elim src_sz normalize // |
---|
| 561 | #_ * #H @(H … (refl ??)) |
---|
| 562 | | 2: #Hlt @(integer_sub_cast_lt … Hlt) |
---|
| 563 | ] |
---|
| 564 | ] qed. |
---|
[2030] | 565 | |
---|
| 566 | 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. |
---|
| 567 | * #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed. |
---|
| 568 | |
---|
| 569 | lemma smaller_integer_val_identity : ∀sz,sg,x. |
---|
| 570 | smaller_integer_val sz sz sg x x. |
---|
| 571 | #sz #sg * |
---|
| 572 | [ 2: #error // |
---|
| 573 | | 1: * #val #trace whd in match (smaller_integer_val ?????); |
---|
| 574 | #v1 #Hval %{v1} @conj try @conj try @conj // |
---|
| 575 | elim sz // |
---|
| 576 | ] qed. |
---|
| 577 | |
---|
| 578 | (* Inversion on exec_cast *) |
---|
| 579 | lemma exec_cast_inv : ∀castee_val,src_sz,src_sg,cast_sz,cast_sg,m,result. |
---|
| 580 | exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg) = OK ? result → |
---|
| 581 | ∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i). |
---|
| 582 | #castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result |
---|
| 583 | elim castee_val |
---|
[2176] | 584 | [ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ] |
---|
[2030] | 585 | [ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ] |
---|
| 586 | whd in ⊢ ((??%?) → ?); |
---|
| 587 | cases (sz_eq_dec sz' src_sz) |
---|
| 588 | [ 1: #Heq destruct >intsize_eq_elim_true normalize nodelta #Heq destruct |
---|
| 589 | %{i} /2/ |
---|
| 590 | | 2: #Hneq >intsize_eq_elim_false; try assumption #H destruct ] |
---|
| 591 | qed. |
---|
| 592 | |
---|
| 593 | |
---|
| 594 | (* Lemmas related to the Ebinop case *) |
---|
| 595 | |
---|
[1970] | 596 | lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg. |
---|
| 597 | * * // qed. |
---|
| 598 | |
---|
| 599 | lemma classify_sub_int : ∀sz,sg. classify_sub (Tint sz sg) (Tint sz sg) = sub_case_ii sz sg. |
---|
| 600 | * * // qed. |
---|
| 601 | |
---|
| 602 | lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true. |
---|
[2441] | 603 | * * normalize #H @conj try @refl assumption qed. |
---|
[1970] | 604 | |
---|
[1198] | 605 | (* Operations where it is safe to use a smaller integer type on the assumption |
---|
| 606 | that we would cast it down afterwards anyway. *) |
---|
| 607 | definition binop_simplifiable ≝ |
---|
| 608 | λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ]. |
---|
| 609 | |
---|
[2030] | 610 | (* Inversion principle for integer addition *) |
---|
| 611 | lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r → |
---|
| 612 | ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)). |
---|
| 613 | #sz #sg #v1 #v2 #m #r |
---|
| 614 | elim v1 |
---|
[2176] | 615 | [ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ] |
---|
[2030] | 616 | whd in ⊢ ((??%?) → ?); normalize nodelta |
---|
| 617 | >classify_add_int normalize nodelta #H destruct |
---|
| 618 | elim v2 in H; |
---|
[2176] | 619 | [ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ] |
---|
[2030] | 620 | whd in ⊢ ((??%?) → ?); #H destruct |
---|
| 621 | elim (sz_eq_dec sz' sz'') |
---|
| 622 | [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ |
---|
| 623 | | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct |
---|
| 624 | ] qed. |
---|
| 625 | |
---|
| 626 | (* Inversion principle for integer subtraction. *) |
---|
| 627 | lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r → |
---|
| 628 | ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)). |
---|
| 629 | #sz #sg #v1 #v2 #m #r |
---|
| 630 | elim v1 |
---|
[2176] | 631 | [ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ] |
---|
[2030] | 632 | whd in ⊢ ((??%?) → ?); normalize nodelta |
---|
| 633 | >classify_sub_int normalize nodelta #H destruct |
---|
| 634 | elim v2 in H; |
---|
[2176] | 635 | [ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ] |
---|
[2030] | 636 | whd in ⊢ ((??%?) → ?); #H destruct |
---|
| 637 | elim (sz_eq_dec sz' sz'') |
---|
| 638 | [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ |
---|
| 639 | | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct |
---|
| 640 | ] qed. |
---|
| 641 | |
---|
| 642 | definition is_int : val → Prop ≝ |
---|
| 643 | λv. |
---|
| 644 | match v with |
---|
| 645 | [ Vint _ _ ⇒ True |
---|
| 646 | | _ ⇒ False ]. |
---|
| 647 | |
---|
| 648 | (* "negative" (in the sense of ¬ Some) inversion principle for integer addition *) |
---|
| 649 | lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? → |
---|
| 650 | ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ |
---|
| 651 | ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. |
---|
| 652 | #sz #sg #v1 #v2 #m |
---|
| 653 | elim v1 |
---|
[2176] | 654 | [ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ] |
---|
[2030] | 655 | [ 2: | *: #_ %1 %1 % #H @H ] |
---|
| 656 | elim v2 |
---|
[2176] | 657 | [ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ] |
---|
[2030] | 658 | [ 2: | *: #_ %1 %2 % #H @H ] |
---|
| 659 | whd in ⊢ ((??%?) → ?); normalize nodelta |
---|
| 660 | >classify_add_int normalize nodelta |
---|
| 661 | elim (sz_eq_dec sz' sz'') |
---|
| 662 | [ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd) |
---|
| 663 | | 2: #Hneq >intsize_eq_elim_false try assumption #_ |
---|
| 664 | %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj // |
---|
| 665 | ] qed. |
---|
| 666 | |
---|
| 667 | (* "negative" inversion principle for integer subtraction *) |
---|
| 668 | lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? → |
---|
| 669 | ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ |
---|
| 670 | ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. |
---|
| 671 | #sz #sg #v1 #v2 #m |
---|
| 672 | elim v1 |
---|
[2176] | 673 | [ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ] |
---|
[2030] | 674 | [ 2: | *: #_ %1 %1 % #H @H ] |
---|
| 675 | elim v2 |
---|
[2176] | 676 | [ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ] |
---|
[2030] | 677 | [ 2: | *: #_ %1 %2 % #H @H ] |
---|
| 678 | whd in ⊢ ((??%?) → ?); normalize nodelta |
---|
| 679 | >classify_sub_int normalize nodelta |
---|
| 680 | elim (sz_eq_dec sz' sz'') |
---|
| 681 | [ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd) |
---|
| 682 | | 2: #Hneq >intsize_eq_elim_false try assumption #_ |
---|
| 683 | %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj // |
---|
| 684 | ] qed. |
---|
| 685 | |
---|
| 686 | |
---|
| 687 | lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m. |
---|
| 688 | ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?. |
---|
| 689 | #op #sz #sg #v1 #v2 #m #H |
---|
| 690 | elim op normalize in match (binop_simplifiable ?); #H destruct |
---|
| 691 | elim v1 in H; |
---|
[2176] | 692 | [ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: | 5,10: #ptr ] |
---|
[2030] | 693 | #_ |
---|
| 694 | whd in match (sem_binary_operation ??????); normalize nodelta |
---|
| 695 | >classify_add_int normalize nodelta // |
---|
| 696 | >classify_sub_int normalize nodelta // |
---|
| 697 | qed. |
---|
| 698 | |
---|
[1970] | 699 | notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)" |
---|
| 700 | with precedence 10 |
---|
| 701 | for @{ match $t return λx.x = $t → ? with [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}.$s ] (refl ? $t) }. |
---|
| 702 | |
---|
| 703 | notation > "hvbox('let' « 〈ident x1,ident x2〉, ident y» 'as' ident E, ident F ≝ t 'in' s)" |
---|
| 704 | with precedence 10 |
---|
| 705 | for @{ match $t return λx.x = $t → ? with |
---|
| 706 | [ mk_Sig ${fresh a} ${ident y} ⇒ λ${ident E}. |
---|
| 707 | match ${fresh a} return λx.x = ${fresh a} → ? with |
---|
| 708 | [ mk_Prod ${ident x1} ${ident x2} ⇒ λ${ident F}. $s ] (refl ? ${fresh a}) |
---|
| 709 | ] (refl ? $t) |
---|
| 710 | }. |
---|
[2030] | 711 | |
---|
[1970] | 712 | (* This function will make your eyes bleed. You've been warned. |
---|
| 713 | * Implements a correct-by-construction version of Brian's original cast-removal code. Does so by |
---|
| 714 | * threading an invariant defined in [simplify_inv], which says roughly "simplification yields either |
---|
| 715 | what you hoped for, i.e. an integer value of the right size, OR something equivalent to the original |
---|
| 716 | expression". [simplify_expr] is not to be called directly: simplify inside is the proper wrapper. |
---|
| 717 | * TODO: proper doc. Some cases are simplifiable. Some type equality tests are maybe dispensable. |
---|
| 718 | * This function is slightly more conservative than the original one, but this should be incrementally |
---|
| 719 | * modifiable (replacing calls to simplify_inside by calls to simplify_expr, + proving correction). |
---|
| 720 | * Also, I think that the proofs are factorizable to a great deal, but I'd rather have something |
---|
| 721 | * more or less "modular", case-by-case wise. |
---|
| 722 | *) |
---|
[2009] | 723 | let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) |
---|
[1970] | 724 | : Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ |
---|
| 725 | match e return λx. x = e → ? with |
---|
| 726 | [ Expr ed ty ⇒ λHexpr_eq. |
---|
| 727 | match ed return λx. ed = x → ? with |
---|
| 728 | [ Econst_int cst_sz i ⇒ λHdesc_eq. |
---|
| 729 | match ty return λx. x=ty → ? with |
---|
| 730 | [ Tint ty_sz sg ⇒ λHexprtype_eq. |
---|
| 731 | (* Ensure that the displayed type size [cst_sz] and actual size [sz] are equal ... *) |
---|
| 732 | match sz_eq_dec cst_sz ty_sz with |
---|
| 733 | [ inl Hsz_eq ⇒ |
---|
| 734 | match type_eq_dec ty (Tint target_sz target_sg) with |
---|
| 735 | [ inl Hdonothing ⇒ «〈true, e〉, ?» |
---|
| 736 | | inr Hdosomething ⇒ |
---|
| 737 | (* Do the actual useful work *) |
---|
| 738 | 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 |
---|
| 739 | [ Some i' ⇒ λHsimpl_eq. |
---|
| 740 | «〈true, Expr (Econst_int target_sz i') (Tint target_sz target_sg)〉, ?» |
---|
| 741 | | None ⇒ λ_. |
---|
| 742 | «〈false, e〉, ?» |
---|
| 743 | ] (refl ? (simplify_int cst_sz target_sz sg target_sg i)) |
---|
| 744 | ] |
---|
| 745 | | inr _ ⇒ (* The expression is ill-typed. *) |
---|
| 746 | «〈false, e〉, ?» |
---|
| 747 | ] |
---|
| 748 | | _ ⇒ λ_. |
---|
| 749 | «〈false, e〉, ?» |
---|
| 750 | ] (refl ? ty) |
---|
| 751 | | Ederef e1 ⇒ λHdesc_eq. |
---|
| 752 | let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
| 753 | «〈false, Expr (Ederef e2) ty〉, ?» |
---|
| 754 | | Eaddrof e1 ⇒ λHdesc_eq. |
---|
| 755 | let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
| 756 | «〈false, Expr (Eaddrof e2) ty〉, ?» |
---|
| 757 | | Eunop op e1 ⇒ λHdesc_eq. |
---|
| 758 | let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
| 759 | «〈false, Expr (Eunop op e2) ty〉, ?» |
---|
| 760 | | Ebinop op lhs rhs ⇒ λHdesc_eq. |
---|
| 761 | (* Type equality is enforced to prove the equalities needed in return by the invariant. *) |
---|
| 762 | match binop_simplifiable op |
---|
| 763 | 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))) |
---|
| 764 | with |
---|
| 765 | [ true ⇒ λHop_simplifiable_eq. |
---|
| 766 | match assert_type_eq ty (typeof lhs) with |
---|
| 767 | [ OK Hty_eq_lhs ⇒ |
---|
| 768 | match assert_type_eq (typeof lhs) (typeof rhs) with |
---|
| 769 | [ OK Htylhs_eq_tyrhs ⇒ |
---|
[2009] | 770 | let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr lhs target_sz target_sg in |
---|
| 771 | let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr rhs target_sz target_sg in |
---|
[1970] | 772 | match desired_type_lhs ∧ desired_type_rhs |
---|
| 773 | 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))) |
---|
| 774 | with |
---|
| 775 | [ true ⇒ λHdesired_eq. |
---|
| 776 | «〈true, Expr (Ebinop op lhs1 rhs1) (Tint target_sz target_sg)〉, ?» |
---|
| 777 | | false ⇒ λHdesired_eq. |
---|
| 778 | let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in |
---|
| 779 | let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in |
---|
| 780 | «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» |
---|
| 781 | ] (refl ? (desired_type_lhs ∧ desired_type_rhs)) |
---|
| 782 | | Error _ ⇒ |
---|
| 783 | let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in |
---|
| 784 | let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in |
---|
| 785 | «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» |
---|
| 786 | ] |
---|
| 787 | | Error _ ⇒ |
---|
| 788 | let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in |
---|
| 789 | let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in |
---|
| 790 | «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» |
---|
| 791 | ] |
---|
| 792 | | false ⇒ λHop_simplifiable_eq. |
---|
| 793 | let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in |
---|
| 794 | let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in |
---|
| 795 | «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» |
---|
| 796 | ] (refl ? (binop_simplifiable op)) |
---|
| 797 | | Ecast cast_ty castee ⇒ λHdesc_eq. |
---|
| 798 | match cast_ty return λx. x = cast_ty → ? with |
---|
| 799 | [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq. |
---|
| 800 | match type_eq_dec ty cast_ty with |
---|
| 801 | [ inl Hcast_eq ⇒ |
---|
| 802 | match necessary_conditions cast_sz cast_sg target_sz target_sg |
---|
| 803 | 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))) |
---|
| 804 | with |
---|
| 805 | [ true ⇒ λHconditions. |
---|
[2009] | 806 | let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr castee target_sz target_sg in |
---|
[1970] | 807 | 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)) |
---|
| 808 | with |
---|
| 809 | [ true ⇒ λHdesired_eq. |
---|
| 810 | «〈true, castee1〉, ?» |
---|
| 811 | | false ⇒ λHdesired_eq. |
---|
[2009] | 812 | let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in |
---|
[1970] | 813 | 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)) |
---|
| 814 | with |
---|
| 815 | [ true ⇒ λHdesired2_eq. |
---|
| 816 | «〈false, castee2〉, ?» |
---|
| 817 | | false ⇒ λHdesired2_eq. |
---|
| 818 | «〈false, Expr (Ecast ty castee2) cast_ty〉, ?» |
---|
| 819 | ] (refl ? desired_type2) |
---|
| 820 | ] (refl ? desired_type) |
---|
| 821 | | false ⇒ λHconditions. |
---|
[2009] | 822 | let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in |
---|
[1970] | 823 | 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)) |
---|
| 824 | with |
---|
| 825 | [ true ⇒ λHdesired2_eq. |
---|
| 826 | «〈false, castee2〉, ?» |
---|
| 827 | | false ⇒ λHdesired2_eq. |
---|
| 828 | «〈false, Expr (Ecast ty castee2) cast_ty〉, ?» |
---|
| 829 | ] (refl ? desired_type2) |
---|
| 830 | ] (refl ? (necessary_conditions cast_sz cast_sg target_sz target_sg)) |
---|
| 831 | | inr Hcast_neq ⇒ |
---|
| 832 | (* inconsistent types ... *) |
---|
| 833 | let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in |
---|
| 834 | «〈false, Expr (Ecast cast_ty castee1) ty〉, ?» |
---|
| 835 | ] |
---|
| 836 | | _ ⇒ λHcast_ty_eq. |
---|
| 837 | let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in |
---|
| 838 | «〈false, Expr (Ecast cast_ty castee1) ty〉, ?» |
---|
| 839 | ] (refl ? cast_ty) |
---|
| 840 | | Econdition cond iftrue iffalse ⇒ λHdesc_eq. |
---|
| 841 | let «cond1, Hcond_equiv» as Hsimplify ≝ simplify_inside cond in |
---|
| 842 | match assert_type_eq ty (typeof iftrue) with |
---|
| 843 | [ OK Hty_eq_iftrue ⇒ |
---|
| 844 | match assert_type_eq (typeof iftrue) (typeof iffalse) with |
---|
| 845 | [ OK Hiftrue_eq_iffalse ⇒ |
---|
[2009] | 846 | let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue ≝ simplify_expr iftrue target_sz target_sg in |
---|
| 847 | let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr iffalse target_sz target_sg in |
---|
[1970] | 848 | match desired_true ∧ desired_false |
---|
| 849 | 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))) |
---|
| 850 | with |
---|
| 851 | [ true ⇒ λHdesired_eq. |
---|
| 852 | «〈true, Expr (Econdition cond1 iftrue1 iffalse1) (Tint target_sz target_sg)〉, ?» |
---|
| 853 | | false ⇒ λHdesired_eq. |
---|
| 854 | let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in |
---|
| 855 | let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in |
---|
| 856 | «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» |
---|
| 857 | ] (refl ? (desired_true ∧ desired_false)) |
---|
| 858 | | _ ⇒ |
---|
| 859 | let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in |
---|
| 860 | let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in |
---|
| 861 | «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» |
---|
| 862 | ] |
---|
| 863 | | _ ⇒ |
---|
| 864 | let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in |
---|
| 865 | let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in |
---|
| 866 | «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» |
---|
| 867 | ] |
---|
| 868 | (* Could probably do better with these, too. *) |
---|
| 869 | | Eandbool lhs rhs ⇒ λHdesc_eq. |
---|
| 870 | let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in |
---|
| 871 | let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in |
---|
| 872 | «〈false, Expr (Eandbool lhs1 rhs1) ty〉, ?» |
---|
| 873 | | Eorbool lhs rhs ⇒ λHdesc_eq. |
---|
| 874 | let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in |
---|
| 875 | let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in |
---|
| 876 | «〈false, Expr (Eorbool lhs1 rhs1) ty〉,?» |
---|
| 877 | (* Could also improve Esizeof *) |
---|
| 878 | | Efield rec_expr f ⇒ λHdesc_eq. |
---|
| 879 | let «rec_expr1, Hrec_expr_equiv» as Hsimplify ≝ simplify_inside rec_expr in |
---|
| 880 | «〈false,Expr (Efield rec_expr1 f) ty〉, ?» |
---|
| 881 | | Ecost l e1 ⇒ λHdesc_eq. |
---|
| 882 | (* The invariant requires that the toplevel [ty] type matches the type of [e1]. *) |
---|
| 883 | (* /!\ XXX /!\ We assume that the type of a cost-labelled expr is the type of the underlying expr. *) |
---|
| 884 | match type_eq_dec ty (typeof e1) with |
---|
| 885 | [ inl Heq ⇒ |
---|
[2009] | 886 | let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr e1 target_sz target_sg in |
---|
[1970] | 887 | «〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?» |
---|
[2009] | 888 | | inr Hneq ⇒ |
---|
[1970] | 889 | let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in |
---|
| 890 | «〈false, Expr (Ecost l e2) ty〉, ?» |
---|
| 891 | ] |
---|
| 892 | | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» |
---|
[2030] | 893 | (* | Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *) |
---|
| 894 | (* In order for the simplification function to be less dymp, we would have to use this line, which would in fact |
---|
| 895 | require to alter the semantics of [load_value_of_type]. *) |
---|
| 896 | | Evar id ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» |
---|
[1970] | 897 | | Esizeof t ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» |
---|
| 898 | ] (refl ? ed) |
---|
| 899 | ] (refl ? e) |
---|
| 900 | |
---|
[2009] | 901 | and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝ |
---|
[1970] | 902 | match e return λx. x = e → ? with |
---|
| 903 | [ Expr ed ty ⇒ λHexpr_eq. |
---|
| 904 | match ed return λx. x = ed → ? with |
---|
| 905 | [ Ederef e1 ⇒ λHdesc_eq. |
---|
| 906 | let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
| 907 | «Expr (Ederef e2) ty, ?» |
---|
| 908 | | Eaddrof e1 ⇒ λHdesc_eq. |
---|
| 909 | let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
| 910 | «Expr (Eaddrof e2) ty, ?» |
---|
| 911 | | Eunop op e1 ⇒ λHdesc_eq. |
---|
| 912 | let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
| 913 | «Expr (Eunop op e2) ty, ?» |
---|
| 914 | | Ebinop op lhs rhs ⇒ λHdesc_eq. |
---|
| 915 | let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in |
---|
| 916 | let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in |
---|
| 917 | «Expr (Ebinop op lhs1 rhs1) ty, ?» |
---|
| 918 | | Ecast cast_ty castee ⇒ λHdesc_eq. |
---|
[1974] | 919 | match type_eq_dec ty cast_ty with |
---|
| 920 | [ inl Hcast_eq ⇒ |
---|
[2009] | 921 | match cast_ty return λx. x = cast_ty → Σresult:expr. conservation e result |
---|
[1974] | 922 | with |
---|
| 923 | [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq. |
---|
[2009] | 924 | let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr castee cast_sz cast_sg in |
---|
| 925 | match success return λx. x = success → Σresult:expr. conservation e result |
---|
[1974] | 926 | with |
---|
| 927 | [ true ⇒ λHsuccess_eq. |
---|
| 928 | «castee1, ?» |
---|
| 929 | | false ⇒ λHsuccess_eq. |
---|
| 930 | «Expr (Ecast cast_ty castee1) ty, ?» |
---|
| 931 | ] (refl ? success) |
---|
| 932 | | _ ⇒ λHcast_ty_eq. |
---|
| 933 | «e, ?» |
---|
| 934 | ] (refl ? cast_ty) |
---|
| 935 | | inr Hcast_neq ⇒ |
---|
| 936 | «e, ?» |
---|
| 937 | ] |
---|
| 938 | | Econdition cond iftrue iffalse ⇒ λHdesc_eq. |
---|
| 939 | let «cond1, Hequiv_cond» as Eq_cond ≝ simplify_inside cond in |
---|
| 940 | let «iftrue1, Hequiv_iftrue» as Eq_iftrue ≝ simplify_inside iftrue in |
---|
| 941 | let «iffalse1, Hequiv_iffalse» as Eq_iffalse ≝ simplify_inside iffalse in |
---|
| 942 | «Expr (Econdition cond1 iftrue1 iffalse1) ty, ?» |
---|
| 943 | | Eandbool lhs rhs ⇒ λHdesc_eq. |
---|
| 944 | let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in |
---|
| 945 | let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in |
---|
| 946 | «Expr (Eandbool lhs1 rhs1) ty, ?» |
---|
| 947 | | Eorbool lhs rhs ⇒ λHdesc_eq. |
---|
| 948 | let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in |
---|
| 949 | let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in |
---|
| 950 | «Expr (Eorbool lhs1 rhs1) ty, ?» |
---|
| 951 | | Efield rec_expr f ⇒ λHdesc_eq. |
---|
| 952 | let «rec_expr1, Hequiv_rec» as Eq_rec ≝ simplify_inside rec_expr in |
---|
| 953 | «Expr (Efield rec_expr1 f) ty, ?» |
---|
| 954 | | Ecost l e1 ⇒ λHdesc_eq. |
---|
| 955 | let «e2, Hequiv» as Eq ≝ simplify_inside e1 in |
---|
| 956 | «Expr (Ecost l e2) ty, ?» |
---|
[1970] | 957 | | _ ⇒ λHdesc_eq. |
---|
| 958 | «e, ?» |
---|
| 959 | ] (refl ? ed) |
---|
| 960 | ] (refl ? e). |
---|
| 961 | #ge #en #m |
---|
[2009] | 962 | [ 1,3,5,6,7,8,9,10,11,12: %1 try @refl |
---|
[1970] | 963 | cases (exec_expr ge en m e) #res |
---|
| 964 | try (@(SimOk ???) //) |
---|
[2009] | 965 | | 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/ |
---|
[2030] | 966 | (* |
---|
[1970] | 967 | whd in match (exec_expr ????); >eq_intsize_identity whd |
---|
[2009] | 968 | >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ] |
---|
[2030] | 969 | *) |
---|
[2009] | 970 | | 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/ |
---|
[1970] | 971 | whd in match (exec_expr ????); |
---|
| 972 | whd in match (exec_expr ????); |
---|
| 973 | >eq_intsize_identity >eq_intsize_identity whd |
---|
[2030] | 974 | #v1 #Heq destruct (Heq) %{i'} try @conj try @conj try @conj // |
---|
[1970] | 975 | [ 1: @(simplify_int_implements_cast … Hsimpl_eq) |
---|
| 976 | | 2: @(simplify_int_success_lt … Hsimpl_eq) ] |
---|
[2030] | 977 | | 13: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res |
---|
| 978 | try (@(SimOk ???) //) |
---|
| 979 | | 14: elim (type_eq_dec ty (Tint target_sz target_sg)) |
---|
| 980 | [ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg) |
---|
| 981 | destruct |
---|
| 982 | [ 1,2: // |
---|
| 983 | | 3: @smaller_integer_val_identity ] |
---|
| 984 | | 2: #Hneq >(type_neq_not_identity … Hneq) %1 // destruct |
---|
| 985 | @(SimOk ???) // |
---|
| 986 | ] |
---|
[2009] | 987 | | 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq |
---|
[1970] | 988 | [ 1: (* Proving preservation of the semantics for expressions. *) |
---|
| 989 | cases Hexpr_sim |
---|
| 990 | [ 2: (* Case where the evaluation of e1 as an expression fails *) |
---|
[2219] | 991 | normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely |
---|
[1970] | 992 | | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) |
---|
| 993 | #Hsim %1 * #val #trace normalize #Hstep |
---|
| 994 | cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ |
---|
| 995 | (load_value_of_type ty m (pblock ptr) (poff ptr) = Some ? val)) |
---|
| 996 | [ 1: lapply Hstep -Hstep |
---|
| 997 | cases (exec_expr ge en m e1) |
---|
| 998 | [ 1: * #val' #trace' normalize nodelta |
---|
| 999 | cases val' normalize nodelta |
---|
| 1000 | [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct |
---|
| 1001 | | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) |
---|
| 1002 | cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq; |
---|
| 1003 | normalize nodelta |
---|
| 1004 | [ 1: #Heq destruct | 2: #val2 #Heq destruct @conj // ] |
---|
| 1005 | ] |
---|
| 1006 | | 2: normalize nodelta #errmesg #Hcontr destruct |
---|
| 1007 | ] |
---|
| 1008 | | 2: * #e1_ptr * #He1_eq_ptr #Hloadptr |
---|
| 1009 | cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) |
---|
| 1010 | ∧ (load_value_of_type ty m (pblock ptr1) (poff ptr1) = Some ? val)) |
---|
| 1011 | [ 1: @(ex_intro … e1_ptr) @conj |
---|
| 1012 | [ 1: @Hsim // | 2: // ] |
---|
| 1013 | | 2: * #e2_ptr * #He2_exec #Hload_e2_ptr |
---|
| 1014 | normalize >He2_exec normalize nodelta >Hload_e2_ptr normalize nodelta @refl |
---|
| 1015 | ] |
---|
| 1016 | ] |
---|
| 1017 | ] |
---|
| 1018 | | 2: (* Proving the preservation of the semantics for lvalues. *) |
---|
| 1019 | cases Hexpr_sim |
---|
| 1020 | [ 2: (* Case where the evaluation of e1 as an lvalue fails *) |
---|
[2219] | 1021 | normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely |
---|
[1970] | 1022 | | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) |
---|
| 1023 | #Hsim %1 * * #block #offset #trace normalize #Hstep |
---|
| 1024 | cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ pblock ptr = block ∧ poff ptr = offset) |
---|
| 1025 | [ 1: lapply Hstep -Hstep |
---|
| 1026 | cases (exec_expr ge en m e1) |
---|
| 1027 | [ 1: * #val' #trace' normalize nodelta |
---|
| 1028 | cases val' normalize nodelta |
---|
| 1029 | [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct |
---|
| 1030 | | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) |
---|
| 1031 | destruct try @conj try @conj // |
---|
| 1032 | ] |
---|
| 1033 | | 2: normalize nodelta #errmesg #Hcontr destruct |
---|
| 1034 | ] |
---|
| 1035 | | 2: * #e1_ptr * * #He1_eq_ptr #Hblock #Hoffset |
---|
| 1036 | cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) ∧ pblock ptr1 = block ∧ poff ptr1 = offset) |
---|
| 1037 | [ 1: @(ex_intro … e1_ptr) @conj try @conj // @Hsim // |
---|
| 1038 | | 2: * #e2_ptr * * #He2_exec #Hblock #Hoffset |
---|
| 1039 | normalize >He2_exec normalize nodelta // |
---|
| 1040 | ] |
---|
| 1041 | ] |
---|
| 1042 | ] |
---|
| 1043 | ] |
---|
[2009] | 1044 | | 16: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq |
---|
[1970] | 1045 | [ 1: (* Proving preservation of the semantics for expressions. *) |
---|
| 1046 | cases Hlvalue_sim |
---|
| 1047 | [ 2: (* Case where the evaluation of e1 as an expression fails *) |
---|
[2219] | 1048 | * #err #Hfail whd in match (exec_expr ????); >Hfail @SimFailNicely |
---|
[1970] | 1049 | | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) |
---|
| 1050 | #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep |
---|
[2176] | 1051 | cut (∃block,offset,ptype. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧ |
---|
| 1052 | (ty = Tpointer ptype) ∧ |
---|
| 1053 | val = Vptr (mk_pointer block offset)) |
---|
[1970] | 1054 | [ 1: lapply Hstep -Hstep |
---|
| 1055 | cases (exec_lvalue ge en m e1) |
---|
| 1056 | [ 1: * * #block #offset #trace' normalize nodelta |
---|
| 1057 | cases ty |
---|
[2176] | 1058 | [ 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain |
---|
| 1059 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] |
---|
[1970] | 1060 | normalize nodelta try (#Heq destruct) |
---|
[2176] | 1061 | @(ex_intro … block) @(ex_intro … offset) @(ex_intro … ptr_ty) |
---|
| 1062 | try @conj try @conj destruct // |
---|
[1970] | 1063 | | 2: normalize nodelta #errmesg #Hcontr destruct |
---|
| 1064 | ] |
---|
[2176] | 1065 | | 2: * #block * #offset * #ptype * * #Hexec_lvalue #Hty_eq #Hval_eq |
---|
[1970] | 1066 | whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta |
---|
[2176] | 1067 | // |
---|
[1970] | 1068 | ] |
---|
| 1069 | ] |
---|
[2009] | 1070 | | 2: (* Proving preservation of the semantics of lvalues. *) |
---|
[2219] | 1071 | @SimFailNicely |
---|
[2009] | 1072 | ] |
---|
| 1073 | | 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq |
---|
[1970] | 1074 | [ 1: whd in match (exec_expr ge en m (Expr ??)); |
---|
| 1075 | whd in match (exec_expr ge en m (Expr ??)); |
---|
| 1076 | cases Hexpr_sim |
---|
[2219] | 1077 | [ 2: * #error #Hexec >Hexec normalize nodelta @SimFailNicely |
---|
[1970] | 1078 | | 1: cases (exec_expr ge en m e1) |
---|
[2219] | 1079 | [ 2: #error #Hexec normalize nodelta @SimFailNicely |
---|
[1970] | 1080 | | 1: * #val #trace #Hexec |
---|
| 1081 | >(Hexec ? (refl ? (OK ? 〈val,trace〉))) |
---|
| 1082 | normalize nodelta @SimOk #a >Htype_eq #H @H |
---|
| 1083 | ] |
---|
| 1084 | ] |
---|
[2219] | 1085 | | 2: @SimFailNicely |
---|
[2009] | 1086 | ] |
---|
[1970] | 1087 | | 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq |
---|
| 1088 | inversion (Hinv_lhs ge en m) |
---|
| 1089 | [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true |
---|
| 1090 | #Hinv <Hresult_flag_lhs_eq_true in Hresult_lhs; >Hdesired_lhs #Habsurd destruct |
---|
| 1091 | | 2: #lhs_src_sz #lhs_src_sg #Htype_lhs #Htype_lhs1 #Hsmaller_lhs #Hdesired_type_lhs #_ |
---|
| 1092 | inversion (Hinv_rhs ge en m) |
---|
| 1093 | [ 1: #result_flag_rhs #Hresult_rhs #Htype_rhs #Hsim_expr_rhs #Hsim_lvalue_rhs #Hdesired_type_rhs_eq #_ |
---|
| 1094 | <Hdesired_type_rhs_eq in Hresult_rhs; >Hdesired_rhs #Habsurd destruct |
---|
| 1095 | | 2: #rhs_src_sz #rhs_src_sg #Htype_rhs #Htype_rhs1 #Hsmaller_rhs #Hdesired_type_rhs #_ |
---|
| 1096 | @(Inv_coerce_ok ge en m … target_sz target_sg lhs_src_sz lhs_src_sg) |
---|
| 1097 | [ 1: >Htype_lhs // |
---|
| 1098 | | 2: // |
---|
| 1099 | | 3: whd in match (exec_expr ??? (Expr ??)); |
---|
| 1100 | whd in match (exec_expr ??? (Expr ??)); |
---|
[2030] | 1101 | (* Tidy up the type equations *) |
---|
| 1102 | >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Heq destruct |
---|
| 1103 | lapply Hsmaller_rhs lapply Hsmaller_lhs |
---|
| 1104 | generalize in match rhs_src_sz; #src_sz |
---|
| 1105 | generalize in match rhs_src_sg; #src_sg |
---|
| 1106 | -Hsmaller_lhs -Hsmaller_rhs -Htype_lhs -Htype_rhs -Hinv_lhs -Hinv_rhs |
---|
| 1107 | >Htype_lhs1 >Htype_rhs1 -Htype_lhs1 -Htype_rhs1 |
---|
[1970] | 1108 | (* Enumerate all the cases for the evaluation of the source expressions ... *) |
---|
[2030] | 1109 | cases (exec_expr ge en m lhs); |
---|
| 1110 | try // * #val_lhs #trace_lhs normalize nodelta |
---|
| 1111 | cases (exec_expr ge en m rhs); |
---|
| 1112 | try // * #val_rhs #trace_rhs normalize nodelta |
---|
| 1113 | whd in match (m_bind ?????); |
---|
| 1114 | (* specialize to the actual simplifiable operations. *) |
---|
| 1115 | cases op in Hop_simplifiable_eq; |
---|
| 1116 | [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_ |
---|
| 1117 | [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m) |
---|
| 1118 | | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ] |
---|
| 1119 | cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m) |
---|
| 1120 | [ 1,3: #_ #_ #_ normalize @I ] |
---|
| 1121 | #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result))) |
---|
| 1122 | #src_result_sz * #i1 * #i2 * * #Hval_lhs_eq #Hval_rhs_eq #Hsrc_result_eq |
---|
| 1123 | whd in match (opt_to_res ???); whd in match (m_bind ?????); normalize nodelta |
---|
| 1124 | >Hval_lhs_eq >Hval_rhs_eq #Hsmaller_rhs #Hsmaller_lhs |
---|
| 1125 | whd |
---|
| 1126 | #result_int #Hsrc_result >Hsrc_result in Hsrc_result_eq; #Hsrc_result_eq |
---|
| 1127 | lapply (sym_eq ??? Hsrc_result_eq) -Hsrc_result_eq #Hsrc_result_eq |
---|
| 1128 | cut (src_result_sz = src_sz) [ 1,3: destruct // ] #Hsz_eq |
---|
| 1129 | lapply Hsmaller_lhs lapply Hsmaller_rhs |
---|
| 1130 | cases (exec_expr ge en m lhs1) normalize nodelta |
---|
| 1131 | [ 2,4: destruct #error normalize in ⊢ (% → ?); #H @(False_ind … (H i1 (refl ? (Vint src_sz i1)))) ] |
---|
| 1132 | * #val_lhs1 #trace_lhs1 |
---|
| 1133 | cases (exec_expr ge en m rhs1) |
---|
| 1134 | [ 2,4: destruct #error #_ normalize in ⊢ (% → ?); #H @(False_ind … (H i2 (refl ? (Vint src_sz i2)))) ] |
---|
| 1135 | * #val_rhs1 #trace_rhs1 |
---|
| 1136 | whd in match (m_bind ?????); normalize nodelta |
---|
| 1137 | [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) |
---|
| 1138 | lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) |
---|
| 1139 | | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m) |
---|
| 1140 | lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ] |
---|
| 1141 | cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m) |
---|
| 1142 | [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?))) |
---|
| 1143 | (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *) |
---|
| 1144 | * |
---|
| 1145 | [ 1,4: whd in ⊢ (? → % → ?); normalize nodelta |
---|
| 1146 | #Habsurd #Hcounterexample elim (Hcounterexample i1 (refl ? (Vint src_sz i1))) |
---|
| 1147 | #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd |
---|
| 1148 | @(False_ind … (Habsurd I)) |
---|
| 1149 | | 2,5: whd in ⊢ (? → ? → % → ?); normalize nodelta |
---|
| 1150 | #Habsurd #_ #Hcounterexample elim (Hcounterexample i2 (refl ? (Vint src_sz i2))) |
---|
| 1151 | #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd |
---|
| 1152 | @(False_ind … (Habsurd I)) |
---|
| 1153 | | 3,6: #dsz1 * #dsz2 * #j1 * #j2 * * #Hval_lhs1 #Hval_rhs1 #Hsz_neq |
---|
| 1154 | whd in ⊢ (% → % → ?); normalize nodelta |
---|
| 1155 | #Hsmaller_lhs #Hsmaller_rhs |
---|
| 1156 | elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) |
---|
| 1157 | #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le |
---|
| 1158 | elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2))) |
---|
| 1159 | #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_ |
---|
| 1160 | destruct elim Hsz_neq #Habsurd @(Habsurd (refl ? target_sz)) |
---|
| 1161 | ] |
---|
| 1162 | | 2,4: destruct #result #Hinversion #_ #Hsmaller_lhs #Hsmaller_rhs normalize nodelta |
---|
| 1163 | elim (Hinversion result (refl ? (Some ? result))) |
---|
| 1164 | #result_sz * #lhs_int * #rhs_int * * #Hlhs1_eq #Hrhs1_eq #Hop_eq |
---|
| 1165 | elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) |
---|
| 1166 | #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le |
---|
| 1167 | elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2))) |
---|
| 1168 | #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_ |
---|
| 1169 | destruct |
---|
| 1170 | [ 1: %{(addition_n (bitsize_of_intsize target_sz) |
---|
| 1171 | (cast_int_int src_sz src_sg target_sz i1) |
---|
| 1172 | (cast_int_int src_sz src_sg target_sz i2))} |
---|
| 1173 | try @conj try @conj try @conj // |
---|
| 1174 | >integer_add_cast_le try // |
---|
| 1175 | | 2: %{(subtraction (bitsize_of_intsize target_sz) |
---|
| 1176 | (cast_int_int src_sz src_sg target_sz i1) |
---|
| 1177 | (cast_int_int src_sz src_sg target_sz i2))} |
---|
| 1178 | try @conj try @conj try @conj // |
---|
| 1179 | >integer_sub_cast_le try // |
---|
| 1180 | ] |
---|
| 1181 | ] ] ] ] |
---|
[2009] | 1182 | | 19,20,21,22: destruct %1 try @refl |
---|
[1970] | 1183 | elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs |
---|
| 1184 | elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs |
---|
| 1185 | [ 1,3,5,7: |
---|
| 1186 | whd in match (exec_expr ????); whd in match (exec_expr ????); |
---|
| 1187 | cases Hexpr_sim_lhs |
---|
[2219] | 1188 | [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely |
---|
[1970] | 1189 | | *: cases (exec_expr ge en m lhs) |
---|
[2219] | 1190 | [ 2,4,6,8: #error #_ @SimFailNicely |
---|
[2009] | 1191 | | *: * #lval #ltrace #Hsim_lhs normalize nodelta |
---|
[1970] | 1192 | cases Hexpr_sim_rhs |
---|
[2219] | 1193 | [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely |
---|
[1970] | 1194 | | *: cases (exec_expr ge en m rhs) |
---|
[2219] | 1195 | [ 2,4,6,8: #error #_ @SimFailNicely |
---|
[1970] | 1196 | | *: * #rval #rtrace #Hsim_rhs |
---|
| 1197 | whd in match (exec_expr ??? (Expr (Ebinop ???) ?)); |
---|
| 1198 | >(Hsim_lhs 〈lval,ltrace〉 (refl ? (OK ? 〈lval,ltrace〉))) |
---|
| 1199 | >(Hsim_rhs 〈rval,rtrace〉 (refl ? (OK ? 〈rval,rtrace〉))) |
---|
| 1200 | normalize nodelta |
---|
| 1201 | >Htype_eq_lhs >Htype_eq_rhs |
---|
| 1202 | @SimOk * #val #trace #H @H |
---|
| 1203 | ] |
---|
| 1204 | ] |
---|
| 1205 | ] |
---|
| 1206 | ] |
---|
[2219] | 1207 | | *: @SimFailNicely |
---|
[1970] | 1208 | ] |
---|
| 1209 | (* Jump to the cast cases *) |
---|
| 1210 | | 23,30,31,32,33,34,35,36: %1 try @refl |
---|
| 1211 | [ 1,4,7,10,13,16,19,22: destruct // ] |
---|
| 1212 | elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq |
---|
| 1213 | (* exec_expr simulation *) |
---|
| 1214 | [ 1,3,5,7,9,11,13,15: cases Hexec_sim |
---|
[2219] | 1215 | [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail whd in match (exec_expr ge en m ?); |
---|
| 1216 | >Hexec_fail @SimFailNicely |
---|
[1970] | 1217 | | 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq |
---|
| 1218 | whd in match (exec_expr ge en m ?); #Hstep |
---|
| 1219 | cut (∃v1. exec_expr ge en m castee = OK ? 〈v1,trace〉 |
---|
| 1220 | ∧ exec_cast m v1 (typeof castee) cast_ty = OK ? val) |
---|
| 1221 | [ 1,3,5,7,9,11,13,15: |
---|
| 1222 | lapply Hstep -Hstep cases (exec_expr ge en m castee) |
---|
| 1223 | [ 2,4,6,8,10,12,14,16: #error1 normalize nodelta #Hcontr destruct |
---|
| 1224 | | 1,3,5,7,9,11,13,15: * #val1 #trace1 normalize nodelta |
---|
| 1225 | #Hstep @(ex_intro … val1) |
---|
| 1226 | cases (exec_cast m val1 (typeof castee) cast_ty) in Hstep; |
---|
| 1227 | [ 2,4,6,8,10,12,14,16: #error #Hstep normalize in Hstep; destruct |
---|
| 1228 | | 1,3,5,7,9,11,13,15: #result #Hstep normalize in Hstep; destruct |
---|
| 1229 | @conj @refl |
---|
| 1230 | ] |
---|
| 1231 | ] |
---|
| 1232 | | 2,4,6,8,10,12,14,16: * #v1 * #Hexec_expr #Hexec_cast |
---|
| 1233 | whd in match (exec_expr ge en m ?); |
---|
| 1234 | >(Hsim … Hexec_expr ) normalize nodelta |
---|
| 1235 | <Htype_eq >Hexec_cast // |
---|
| 1236 | ] |
---|
| 1237 | ] |
---|
[2219] | 1238 | | 2,4,6,8,10,12,14,16: destruct @SimFailNicely |
---|
[1970] | 1239 | ] |
---|
| 1240 | | 24: destruct inversion (Hcastee_inv ge en m) |
---|
| 1241 | [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2 |
---|
| 1242 | <Hresult_flag_2 in Hresult_flag; #Hcontr destruct |
---|
| 1243 | | 2: #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller_eval #_ #Hinv_eq |
---|
| 1244 | @(Inv_coerce_ok ??????? cast_sz cast_sg) |
---|
| 1245 | [ 1: // | 2: <Htype_castee1 // |
---|
| 1246 | | 3: whd in match (exec_expr ??? (Expr ??)); |
---|
[2030] | 1247 | >Htype_castee |
---|
[1970] | 1248 | (* Simplify the goal by culling impossible cases, using Hsmaller_val *) |
---|
| 1249 | cases (exec_expr ge en m castee) in Hsmaller_eval; |
---|
[2009] | 1250 | [ 2: #error // |
---|
[2030] | 1251 | | 1: * #castee_val #castee_trace #Hsmaller normalize nodelta |
---|
| 1252 | lapply (exec_cast_inv castee_val src_sz src_sg cast_sz cast_sg m) |
---|
| 1253 | cases (exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg)) |
---|
| 1254 | [ 2: #error #_ @I |
---|
| 1255 | | 1: #result #Hinversion elim (Hinversion result (refl ? (OK ? result))) |
---|
| 1256 | #castee_int * #Hcastee_val_eq #Hresult_eq |
---|
| 1257 | whd in match (m_bind ?????); |
---|
| 1258 | #result_int #Hresult_eq2 |
---|
| 1259 | cases (exec_expr ge en m castee1) in Hsmaller; |
---|
| 1260 | [ 2: #error normalize in ⊢ (% → ?); #Habsurd |
---|
| 1261 | @(False_ind … (Habsurd castee_int Hcastee_val_eq)) |
---|
| 1262 | | 1: * #val1 #trace1 whd in ⊢ (% → ?); normalize nodelta |
---|
| 1263 | #Hsmaller elim (Hsmaller castee_int Hcastee_val_eq) |
---|
| 1264 | #val1_int * * * #Hval1_eq #Hval1_int_eq #Hcastee_trace_eq |
---|
| 1265 | destruct #Hle %{(cast_int_int src_sz src_sg target_sz castee_int)} |
---|
| 1266 | try @conj try @conj try @conj try // |
---|
| 1267 | [ 1: @cast_composition ] try assumption |
---|
| 1268 | elim (necessary_conditions_spec … (sym_eq … Hconditions)) |
---|
| 1269 | [ 2,4: * #Heq >Heq #_ elim target_sz // |
---|
| 1270 | | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ] |
---|
| 1271 | ] ] ] ] ] |
---|
[1970] | 1272 | | 25,27: destruct |
---|
| 1273 | inversion (Hcast2 ge en m) |
---|
| 1274 | [ 1,3: (* Impossible case. *) |
---|
| 1275 | #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult; |
---|
| 1276 | #Hcontr destruct |
---|
[2030] | 1277 | | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself. |
---|
[1970] | 1278 | We did not successfuly cast the subexpression to target_sz, though. *) |
---|
| 1279 | #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq |
---|
| 1280 | @(Inv_eq ???????) // |
---|
[2219] | 1281 | [ 1,3: >Htype_castee2 // |
---|
| 1282 | | 2,4: (* Prove simulation for exec_expr *) |
---|
[1970] | 1283 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1284 | cases (exec_expr ge en m castee) in Hsmaller_eval; |
---|
| 1285 | [ 2,4: (* erroneous evaluation of the original expression *) |
---|
[2219] | 1286 | #error #Hsmaller_eval @SimFailNicely |
---|
[2030] | 1287 | | 1,3: * #val #trace normalize nodelta >Htype_castee |
---|
| 1288 | lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) |
---|
| 1289 | cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg)) |
---|
[2219] | 1290 | [ 2,4: #error #_ #_ @SimFailNicely |
---|
[2030] | 1291 | | 1,3: #result #Hinversion elim (Hinversion result (refl ??)) |
---|
| 1292 | #val_int * #Hval_eq #Hresult_eq |
---|
| 1293 | cases (exec_expr ge en m castee2) |
---|
| 1294 | [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … (Hsmaller_eval val_int Hval_eq)) |
---|
| 1295 | | 1,3: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq) |
---|
| 1296 | #val1_int * * * #Hval1_eq #Hcast_eq #Htrace_eq #Hle |
---|
| 1297 | destruct @SimOk normalize #a #H @H ] |
---|
| 1298 | ] ] |
---|
| 1299 | ] ] |
---|
[1970] | 1300 | | 26,28: destruct |
---|
| 1301 | inversion (Hcast2 ge en m) |
---|
| 1302 | [ 2,4: (* Impossible case. *) |
---|
| 1303 | #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #Habsurd #Hinv_eq |
---|
| 1304 | (* Do some gymnastic to transform the Habsurd jmeq into a proper, 'destruct'able eq *) |
---|
| 1305 | letin Habsurd_eq ≝ (jmeq_to_eq ??? Habsurd) lapply Habsurd_eq |
---|
| 1306 | -Habsurd_eq -Habsurd #Habsurd destruct |
---|
| 1307 | | 1,3: (* All our attempts at casting down the expression have failed. We still use the |
---|
| 1308 | resulting expression, as we may have discovered and simplified unrelated casts. *) |
---|
| 1309 | #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv |
---|
| 1310 | @(Inv_eq ???????) // |
---|
| 1311 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1312 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1313 | cases Hsim_expr |
---|
[2219] | 1314 | [ 2,4: * #error #Hexec_err >Hexec_err @SimFailNicely |
---|
[1970] | 1315 | | 1,3: #Hexec_ok |
---|
| 1316 | cases (exec_expr ge en m castee) in Hexec_ok; |
---|
[2219] | 1317 | [ 2,4: #error #Hsim @SimFailNicely |
---|
[1970] | 1318 | | 1,3: * #val #trace #Hsim normalize nodelta |
---|
| 1319 | >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta |
---|
| 1320 | @SimOk #a #H @H |
---|
| 1321 | ] |
---|
| 1322 | ] |
---|
| 1323 | ] |
---|
| 1324 | | 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 1325 | @(Inv_eq ???????) // |
---|
| 1326 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1327 | whd in match (exec_expr ??? (Expr ??)); |
---|
[2219] | 1328 | cases Hsim_expr |
---|
| 1329 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1970] | 1330 | | 1: #Hexec_ok @SimOk * #val #trace |
---|
| 1331 | cases (exec_expr ge en m castee) in Hexec_ok; |
---|
| 1332 | [ 2: #error #Habsurd normalize in Habsurd; normalize nodelta #H destruct |
---|
| 1333 | | 1: * #val #trace #Hexec_ok normalize nodelta |
---|
| 1334 | >(Hexec_ok … 〈val, trace〉 (refl ? (OK ? 〈val, trace〉))) |
---|
| 1335 | >Htype_eq |
---|
| 1336 | normalize nodelta #H @H |
---|
| 1337 | ] |
---|
| 1338 | ] |
---|
| 1339 | | 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq |
---|
| 1340 | inversion (Htrue_inv ge en m) |
---|
| 1341 | [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false |
---|
| 1342 | #Hinv <Hresult_flag_true_eq_false in Hresult_true; >Hdesired_true #Habsurd destruct |
---|
| 1343 | | 2: #true_src_sz #true_src_sg #Htype_eq_true #Htype_eq_true1 #Hsmaller_true #_ #Hinv_true |
---|
| 1344 | inversion (Hfalse_inv ge en m) |
---|
| 1345 | [ 1: #result_flag_false #Hresult_false #Htype_false #Hsim_expr_false #Hsim_lvalue_false #Hresult_flag_false_eq_false |
---|
| 1346 | #Hinv <Hresult_flag_false_eq_false in Hresult_false; >Hdesired_false #Habsurd destruct |
---|
| 1347 | | 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false |
---|
| 1348 | >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg) |
---|
[2009] | 1349 | [ 1,2: // |
---|
[1970] | 1350 | | 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??)); |
---|
| 1351 | elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq |
---|
| 1352 | cases Hexec_cond_sim |
---|
| 1353 | [ 2: * #error #Herror >Herror normalize @I |
---|
| 1354 | | 1: cases (exec_expr ge en m cond) |
---|
| 1355 | [ 2: #error #_ normalize @I |
---|
| 1356 | | 1: * #cond_val #cond_trace #Hcond_sim |
---|
[2009] | 1357 | >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) |
---|
[1970] | 1358 | normalize nodelta |
---|
| 1359 | >Htype_cond_eq |
---|
| 1360 | cases (exec_bool_of_val cond_val (typeof cond1)) * |
---|
| 1361 | [ 3,4: normalize // |
---|
| 1362 | | 1,2: normalize in match (m_bind ?????); |
---|
| 1363 | normalize in match (m_bind ?????); |
---|
| 1364 | -Hexec_cond_sim -Hcond_sim -cond_val |
---|
| 1365 | [ 1: (* true branch taken *) |
---|
| 1366 | cases (exec_expr ge en m iftrue) in Hsmaller_true; |
---|
| 1367 | [ 2: #error #_ @I |
---|
[2030] | 1368 | | 1: * #val_true_branch #trace_true_branch #Hsmaller |
---|
| 1369 | #val_true_branch #Hval_true_branch lapply Hsmaller -Hsmaller |
---|
[1970] | 1370 | cases (exec_expr ge en m iftrue1) |
---|
[2030] | 1371 | [ 2: #error normalize in ⊢ (% → ?); #Hsmaller |
---|
| 1372 | @(False_ind … (Hsmaller val_true_branch Hval_true_branch)) |
---|
| 1373 | | 1: * #val_true1_branch #trace_true1_branch #Hsmaller normalize nodelta |
---|
| 1374 | elim (Hsmaller val_true_branch Hval_true_branch) |
---|
| 1375 | #val_true1_int * * * #val_true1_branch #Hval_cast_eq #Htrace_eq #Hle |
---|
| 1376 | %{val_true1_int} try @conj try @conj try @conj // |
---|
| 1377 | ] ] |
---|
| 1378 | | 2: (* false branch taken. Same proof as above, different arguments ... *) |
---|
| 1379 | cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg) |
---|
| 1380 | [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq |
---|
| 1381 | destruct (Htype_eq) @conj @refl ] * #Hsz_eq #Hsg_eq destruct |
---|
[1970] | 1382 | cases (exec_expr ge en m iffalse) in Hsmaller_false; |
---|
| 1383 | [ 2: #error #_ @I |
---|
[2030] | 1384 | | 1: destruct * #val_false_branch #trace_false_branch #Hsmaller |
---|
| 1385 | #val_false_branch #Hval_false_branch lapply Hsmaller -Hsmaller |
---|
[1970] | 1386 | cases (exec_expr ge en m iffalse1) |
---|
[2030] | 1387 | [ 2: #error normalize in ⊢ (% → ?); #Hsmaller |
---|
| 1388 | @(False_ind … (Hsmaller val_false_branch Hval_false_branch)) |
---|
| 1389 | | 1: * #val_false1_branch #trace_false1_branch #Hsmaller normalize nodelta |
---|
| 1390 | elim (Hsmaller val_false_branch Hval_false_branch) |
---|
| 1391 | #val_false1_int * * * #val_false1_branch #Hval_cast_eq #Htrace_eq #Hle |
---|
| 1392 | %{val_false1_int} try @conj try @conj try @conj // |
---|
| 1393 | ] ] |
---|
| 1394 | ] ] ] ] ] ] ] |
---|
[1970] | 1395 | | 38,39,40: destruct |
---|
| 1396 | elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq |
---|
| 1397 | elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq |
---|
| 1398 | elim (Hfalse_equiv ge en m) * #Hsim_expr_false #Hsim_vlalue_false #Htype_false_eq |
---|
| 1399 | %1 try @refl |
---|
| 1400 | [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
| 1401 | cases (exec_expr ge en m cond) in Hsim_expr_cond; |
---|
[2219] | 1402 | [ 2,4,6: #error #_ @SimFailNicely |
---|
[1970] | 1403 | | 1,3,5: * #cond_val #cond_trace normalize nodelta |
---|
| 1404 | cases (exec_expr ge en m cond1) |
---|
| 1405 | [ 2,4,6: #error * |
---|
| 1406 | [ 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) |
---|
| 1407 | #Habsurd destruct |
---|
| 1408 | | *: * #error #Habsurd destruct ] |
---|
| 1409 | | 1,3,5: * #cond_val1 #cond_trace1 * |
---|
| 1410 | [ 2,4,6: * #error #Habsurd destruct |
---|
| 1411 | | 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) |
---|
| 1412 | #Hcond_eq normalize nodelta destruct (Hcond_eq) |
---|
| 1413 | >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1)) |
---|
[2219] | 1414 | [ 2,4,6: #error @SimFailNicely |
---|
[1970] | 1415 | | 1,3,5: * (* true branch *) |
---|
| 1416 | [ 1,3,5: |
---|
| 1417 | normalize in match (m_bind ?????); |
---|
| 1418 | normalize in match (m_bind ?????); |
---|
| 1419 | cases Hsim_expr_true |
---|
[2219] | 1420 | [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1970] | 1421 | | 1,3,5: cases (exec_expr ge en m iftrue) |
---|
[2219] | 1422 | [ 2,4,6: #error #_ normalize nodelta @SimFailNicely |
---|
[1970] | 1423 | | 1,3,5: * #val_true #trace_true normalize nodelta #Hsim |
---|
| 1424 | >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉))) |
---|
| 1425 | normalize nodelta @SimOk #a #H @H |
---|
| 1426 | ] |
---|
| 1427 | ] |
---|
| 1428 | | 2,4,6: |
---|
| 1429 | normalize in match (m_bind ?????); |
---|
| 1430 | normalize in match (m_bind ?????); |
---|
| 1431 | cases Hsim_expr_false |
---|
[2219] | 1432 | [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely |
---|
[1970] | 1433 | | 1,3,5: cases (exec_expr ge en m iffalse) |
---|
[2219] | 1434 | [ 2,4,6: #error #_ normalize nodelta @SimFailNicely |
---|
[1970] | 1435 | | 1,3,5: * #val_false #trace_false normalize nodelta #Hsim |
---|
| 1436 | >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉))) |
---|
| 1437 | normalize nodelta @SimOk #a #H @H |
---|
| 1438 | ] |
---|
| 1439 | ] |
---|
| 1440 | ] |
---|
| 1441 | ] |
---|
| 1442 | ] |
---|
| 1443 | ] |
---|
| 1444 | ] |
---|
[2219] | 1445 | | 2,4,6: @SimFailNicely |
---|
[1970] | 1446 | ] |
---|
| 1447 | | 41,42: destruct |
---|
| 1448 | elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs |
---|
| 1449 | elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs |
---|
| 1450 | %1 try @refl |
---|
| 1451 | [ 1,3: whd in match (exec_expr ??? (Expr ??)); |
---|
| 1452 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1453 | cases Hsim_expr_lhs |
---|
[2219] | 1454 | [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely |
---|
[1970] | 1455 | | 1,3: cases (exec_expr ge en m lhs) |
---|
[2219] | 1456 | [ 2,4: #error #_ @SimFailNicely |
---|
[1970] | 1457 | | 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta |
---|
| 1458 | >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉))) |
---|
| 1459 | normalize nodelta >Htype_eq_lhs |
---|
| 1460 | cases (exec_bool_of_val lhs_val (typeof lhs1)) |
---|
[2219] | 1461 | [ 2,4: #error normalize @SimFailNicely |
---|
[1970] | 1462 | | 1,3: * |
---|
| 1463 | whd in match (m_bind ?????); |
---|
| 1464 | whd in match (m_bind ?????); |
---|
| 1465 | [ 2,3: (* lhs evaluates to true *) |
---|
| 1466 | @SimOk #a #H @H |
---|
| 1467 | | 1,4: cases Hsim_expr_rhs |
---|
[2219] | 1468 | [ 2,4: * #error #Hexec >Hexec @SimFailNicely |
---|
[1970] | 1469 | | 1,3: cases (exec_expr ge en m rhs) |
---|
[2219] | 1470 | [ 2,4: #error #_ @SimFailNicely |
---|
[1970] | 1471 | | 1,3: * #rhs_val #rhs_trace -Hsim #Hsim |
---|
| 1472 | >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉))) |
---|
| 1473 | normalize nodelta >Htype_eq_rhs |
---|
| 1474 | @SimOk #a #H @H |
---|
| 1475 | ] |
---|
| 1476 | ] |
---|
| 1477 | ] |
---|
| 1478 | ] |
---|
[2009] | 1479 | ] |
---|
| 1480 | ] |
---|
[2219] | 1481 | | 2,4: @SimFailNicely |
---|
[1970] | 1482 | ] |
---|
| 1483 | | 43: destruct |
---|
| 1484 | cases (type_eq_dec ty (Tint target_sz target_sg)) |
---|
| 1485 | [ 1: #Htype_eq >Htype_eq >type_eq_identity |
---|
| 1486 | @(Inv_coerce_ok ??????? target_sz target_sg) |
---|
| 1487 | [ 1,2: // |
---|
[2030] | 1488 | | 3: @smaller_integer_val_identity ] |
---|
[1970] | 1489 | | 2: #Hneq >(type_neq_not_identity … Hneq) |
---|
| 1490 | %1 // @SimOk #a #H @H |
---|
| 1491 | ] |
---|
| 1492 | | 44: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 1493 | %1 try @refl |
---|
| 1494 | [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
| 1495 | whd in match (exec_lvalue ????) in Hsim_lvalue; |
---|
| 1496 | whd in match (exec_lvalue' ?????); |
---|
| 1497 | whd in match (exec_lvalue' ?????); |
---|
| 1498 | >Htype_eq |
---|
| 1499 | cases (typeof rec_expr1) normalize nodelta |
---|
[2176] | 1500 | [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
[2219] | 1501 | [ 1,2,3,4,5,8,9: @SimFailNicely |
---|
[1970] | 1502 | | 6,7: cases Hsim_lvalue |
---|
[2219] | 1503 | [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely |
---|
[1970] | 1504 | | 1,3: cases (exec_lvalue ge en m rec_expr) |
---|
[2219] | 1505 | [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely |
---|
[1970] | 1506 | | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) |
---|
| 1507 | whd in match (m_bind ?????); |
---|
| 1508 | @SimOk #a #H @H |
---|
| 1509 | ] |
---|
| 1510 | ] |
---|
| 1511 | ] |
---|
| 1512 | | 2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??)); |
---|
| 1513 | >Htype_eq |
---|
| 1514 | cases (typeof rec_expr1) normalize nodelta |
---|
[2176] | 1515 | [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
[2219] | 1516 | [ 1,2,3,4,5,8,9: @SimFailNicely |
---|
[1970] | 1517 | | 6,7: cases Hsim_lvalue |
---|
[2219] | 1518 | [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely |
---|
[1970] | 1519 | | 1,3: cases (exec_lvalue ge en m rec_expr) |
---|
[2219] | 1520 | [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely |
---|
[1970] | 1521 | | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) |
---|
| 1522 | whd in match (m_bind ?????); |
---|
| 1523 | @SimOk #a #H @H |
---|
| 1524 | ] |
---|
| 1525 | ] |
---|
| 1526 | ] |
---|
| 1527 | ] |
---|
| 1528 | | 45: destruct |
---|
| 1529 | inversion (Hinv ge en m) |
---|
| 1530 | [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_ |
---|
| 1531 | @(Inv_coerce_ok ??????? src_sz src_sg) |
---|
| 1532 | [ 1: >Htypeof_e1 // |
---|
| 1533 | | 2: >Htypeof_e2 // |
---|
| 1534 | | 3: whd in match (exec_expr ??? (Expr ??)); |
---|
| 1535 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1536 | cases (exec_expr ge en m e1) in Hsmaller; |
---|
| 1537 | [ 2: #error normalize // |
---|
[2030] | 1538 | | 1: * #val1 #trace1 #Hsmaller #val1_int #Hval1_eq |
---|
| 1539 | cases (exec_expr ge en m e2) in Hsmaller; |
---|
| 1540 | [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … (Habsurd val1_int Hval1_eq)) |
---|
| 1541 | | 1: * #val2 #trace #Hsmaller elim (Hsmaller val1_int Hval1_eq) |
---|
| 1542 | #val2_int * * * #Hval2_eq #Hcast #Htrace #Hle normalize nodelta |
---|
| 1543 | %{val2_int} try @conj try @conj try @conj // |
---|
[1970] | 1544 | ] |
---|
| 1545 | ] |
---|
| 1546 | ] |
---|
| 1547 | | 1: #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hdesired_typ #_ |
---|
| 1548 | >Hresult %1 try @refl |
---|
| 1549 | [ 1: >Htype_eq // |
---|
| 1550 | | 2: whd in match (exec_expr ??? (Expr ??)); |
---|
| 1551 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1552 | cases Hsim_expr |
---|
[2219] | 1553 | [ 2: * #error #Hexec_error >Hexec_error @SimFailNicely |
---|
[1970] | 1554 | | 1: cases (exec_expr ge en m e1) |
---|
[2219] | 1555 | [ 2: #error #_ @SimFailNicely |
---|
[1970] | 1556 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec |
---|
[1974] | 1557 | @SimOk #a #H @H |
---|
[1970] | 1558 | ] |
---|
| 1559 | ] |
---|
[2219] | 1560 | | 3: @SimFailNicely |
---|
[1970] | 1561 | ] |
---|
| 1562 | ] |
---|
| 1563 | | 46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 1564 | %1 try @refl |
---|
[1974] | 1565 | [ 1: whd in match (exec_expr ??? (Expr ??)); |
---|
| 1566 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1567 | cases Hsim_expr |
---|
[2219] | 1568 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1569 | | 1: cases (exec_expr ge en m e1) |
---|
[2219] | 1570 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1571 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ] |
---|
| 1572 | ] |
---|
| 1573 | | 2: @SimFail /2 by ex_intro/ ] |
---|
| 1574 | (* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls |
---|
[2009] | 1575 | * simplify_expr *) |
---|
[1974] | 1576 | | 47, 48, 49: (* trivial const_int, const_float and var cases *) |
---|
| 1577 | try @conj try @conj try @refl |
---|
| 1578 | @SimOk #a #H @H |
---|
| 1579 | | 50: (* Deref case *) destruct |
---|
| 1580 | elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 1581 | try @conj try @conj |
---|
| 1582 | [ 1: |
---|
| 1583 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1584 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1585 | whd in match (exec_lvalue' ?????); |
---|
| 1586 | whd in match (exec_lvalue' ?????); |
---|
| 1587 | | 2: |
---|
| 1588 | whd in match (exec_lvalue ??? (Expr ??)); |
---|
| 1589 | whd in match (exec_lvalue ??? (Expr ??)); |
---|
| 1590 | ] |
---|
| 1591 | [ 1,2: |
---|
| 1592 | cases Hsim_expr |
---|
[2219] | 1593 | [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1594 | | 1,3: cases (exec_expr ge en m e1) |
---|
[2219] | 1595 | [ 2,4: #error #_ @SimFailNicely |
---|
[1974] | 1596 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] |
---|
| 1597 | | 3: // ] |
---|
| 1598 | | 51: (* Addrof *) destruct |
---|
| 1599 | elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 1600 | try @conj try @conj |
---|
| 1601 | [ 1: |
---|
| 1602 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1603 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1604 | cases Hsim_lvalue |
---|
[2219] | 1605 | [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely |
---|
[1974] | 1606 | | 1: cases (exec_lvalue ge en m e1) |
---|
[2219] | 1607 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1608 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] |
---|
[2219] | 1609 | | 2: @SimFailNicely |
---|
[1974] | 1610 | | 3: // ] |
---|
| 1611 | | 52: (* Unop *) destruct |
---|
| 1612 | elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 1613 | try @conj try @conj |
---|
| 1614 | [ 1: |
---|
| 1615 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1616 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1617 | cases Hsim_expr |
---|
[2219] | 1618 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1619 | | 1: cases (exec_expr ge en m e1) |
---|
[2219] | 1620 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1621 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk |
---|
| 1622 | >Htype_eq #a #H @H ] ] |
---|
[2219] | 1623 | | 2: @SimFailNicely |
---|
[1974] | 1624 | | 3: // ] |
---|
| 1625 | | 53: (* Binop *) destruct |
---|
| 1626 | elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs |
---|
| 1627 | elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs |
---|
| 1628 | try @conj try @conj |
---|
| 1629 | [ 1: |
---|
| 1630 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1631 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1632 | cases Hsim_expr_lhs |
---|
[2219] | 1633 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1634 | | 1: cases (exec_expr ge en m lhs) |
---|
[2219] | 1635 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1636 | | 1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs |
---|
[2219] | 1637 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1638 | | 1: cases (exec_expr ge en m rhs) |
---|
[2219] | 1639 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1640 | | 1: #rhs_value #Hsim_rhs |
---|
| 1641 | lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value))) |
---|
| 1642 | lapply (Hsim_rhs rhs_value (refl ? (OK ? rhs_value))) |
---|
| 1643 | #Hrhs >Hrhs #Hlhs >Hlhs >Htype_eq_rhs >Htype_eq_lhs |
---|
| 1644 | @SimOk #a #H @H |
---|
| 1645 | ] |
---|
| 1646 | ] |
---|
| 1647 | ] |
---|
| 1648 | ] |
---|
[2219] | 1649 | | 2: @SimFailNicely |
---|
[1974] | 1650 | | 3: // |
---|
| 1651 | ] |
---|
| 1652 | | 54: (* Cast, fallback case *) |
---|
| 1653 | try @conj try @conj try @refl |
---|
| 1654 | @SimOk #a #H @H |
---|
| 1655 | | 55: (* Cast, success case *) destruct |
---|
| 1656 | inversion (Htrans_inv ge en m) |
---|
| 1657 | [ 1: (* contradiction *) |
---|
| 1658 | #result_flag #Hresult_flag #Htype_eq #Hsim_epr #Hsim_lvalue #Hresult_flag_true |
---|
| 1659 | <Hresult_flag_true in Hresult_flag; #Habsurd destruct |
---|
| 1660 | | 2: #src_sz #src_sg #Hsrc_type_eq #Htarget_type_eq #Hsmaller #_ #_ |
---|
| 1661 | try @conj try @conj try @conj |
---|
| 1662 | [ 1: whd in match (exec_expr ??? (Expr ??)); |
---|
| 1663 | cases (exec_expr ge en m castee) in Hsmaller; |
---|
[2219] | 1664 | [ 2: #error #_ @SimFailNicely |
---|
[2030] | 1665 | | 1: * #val #trace normalize nodelta >Hsrc_type_eq |
---|
| 1666 | lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) |
---|
| 1667 | cases (exec_cast m val ??) |
---|
[2219] | 1668 | [ 2: #error #_ #_ @SimFailNicely |
---|
[2030] | 1669 | | 1: #result #Hinversion elim (Hinversion result (refl ??)) |
---|
| 1670 | #val_int * #Hval_eq #Hcast |
---|
| 1671 | cases (exec_expr ge en m castee1) |
---|
| 1672 | [ 2: #error #Habsurd normalize in Habsurd; @(False_ind … (Habsurd val_int Hval_eq)) |
---|
| 1673 | | 1: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq) |
---|
| 1674 | #val1_int * * * #Hval1_int #Hval18int #Htrace #Hle |
---|
| 1675 | @SimOk destruct normalize // ] |
---|
[1974] | 1676 | ] |
---|
[2030] | 1677 | ] |
---|
[2219] | 1678 | | 2: @SimFailNicely |
---|
[1974] | 1679 | | 3: >Htarget_type_eq // |
---|
| 1680 | ] |
---|
| 1681 | ] |
---|
| 1682 | | 56: (* Cast, "failure" case *) destruct |
---|
| 1683 | inversion (Htrans_inv ge en m) |
---|
| 1684 | [ 2: (* contradiction *) |
---|
| 1685 | #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller #Habsurd |
---|
| 1686 | lapply (jmeq_to_eq ??? Habsurd) -Habsurd #Herror destruct |
---|
| 1687 | | 1: #result_flag #Hresult_flag #Htype_eq #Hsim_expr #Hsim_lvalue #_ #_ |
---|
| 1688 | try @conj try @conj try @conj |
---|
| 1689 | [ 1: whd in match (exec_expr ????); |
---|
| 1690 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1691 | cases Hsim_expr |
---|
[2219] | 1692 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1693 | | 1: cases (exec_expr ??? castee) |
---|
[2219] | 1694 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1695 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok |
---|
| 1696 | @SimOk >Htype_eq #a #H @H ] |
---|
| 1697 | ] |
---|
[2219] | 1698 | | 2: @SimFailNicely |
---|
[1974] | 1699 | | 3: // |
---|
| 1700 | ] |
---|
| 1701 | ] |
---|
| 1702 | | 57,58,59,60,61,62,63,64,68: |
---|
| 1703 | try @conj try @conj try @refl |
---|
| 1704 | @SimOk #a #H @H |
---|
| 1705 | | 65: destruct |
---|
| 1706 | elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond |
---|
| 1707 | elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true |
---|
| 1708 | elim (Hequiv_iffalse ge en m) * #Hsim_exec_false #Hsim_lvalue_false #Htype_eq_false |
---|
| 1709 | try @conj try @conj |
---|
| 1710 | [ 1: whd in match (exec_expr ??? (Expr ??)); |
---|
| 1711 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1712 | cases Hsim_exec_cond |
---|
[2219] | 1713 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1714 | | 1: cases (exec_expr ??? cond) |
---|
[2219] | 1715 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1716 | | 1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉))) |
---|
| 1717 | #Hcond_ok >Hcond_ok >Htype_eq_cond |
---|
| 1718 | normalize nodelta |
---|
| 1719 | cases (exec_bool_of_val condb (typeof cond1)) |
---|
[2219] | 1720 | [ 2: #error @SimFailNicely |
---|
[1974] | 1721 | | 1: * whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 1722 | normalize nodelta |
---|
| 1723 | [ 1: (* true branch taken *) |
---|
| 1724 | cases Hsim_exec_true |
---|
[2219] | 1725 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1726 | | 1: cases (exec_expr ??? iftrue) |
---|
[2219] | 1727 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1728 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H |
---|
| 1729 | @SimOk #a #H @H |
---|
| 1730 | ] |
---|
| 1731 | ] |
---|
| 1732 | | 2: (* false branch taken *) |
---|
| 1733 | cases Hsim_exec_false |
---|
[2219] | 1734 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1735 | | 1: cases (exec_expr ??? iffalse) |
---|
[2219] | 1736 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1737 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H |
---|
| 1738 | @SimOk #a #H @H |
---|
| 1739 | ] |
---|
| 1740 | ] |
---|
| 1741 | ] |
---|
| 1742 | ] |
---|
| 1743 | ] |
---|
| 1744 | ] |
---|
[2219] | 1745 | | 2: @SimFailNicely |
---|
[1974] | 1746 | | 3: // |
---|
| 1747 | ] |
---|
| 1748 | | 66,67: destruct |
---|
| 1749 | elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs |
---|
| 1750 | elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs |
---|
| 1751 | try @conj try @conj |
---|
| 1752 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1753 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1754 | [ 1,4: cases Hsim_exec_lhs |
---|
[2219] | 1755 | [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1756 | | 1,3: cases (exec_expr ??? lhs) |
---|
[2219] | 1757 | [ 2,4: #error #_ @SimFailNicely |
---|
[1974] | 1758 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs |
---|
| 1759 | normalize nodelta elim a #lhs_val #lhs_trace |
---|
| 1760 | cases (exec_bool_of_val lhs_val (typeof lhs1)) |
---|
[2219] | 1761 | [ 2,4: #error @SimFailNicely |
---|
[1974] | 1762 | | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 1763 | [ 2,3: @SimOk // |
---|
| 1764 | | 1,4: cases Hsim_exec_rhs |
---|
[2219] | 1765 | [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
[1974] | 1766 | | 1,3: cases (exec_expr ??? rhs) |
---|
[2219] | 1767 | [ 2,4: #error #_ @SimFailNicely |
---|
[1974] | 1768 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs |
---|
| 1769 | @SimOk #a #H @H |
---|
| 1770 | ] |
---|
| 1771 | ] |
---|
| 1772 | ] |
---|
| 1773 | ] |
---|
[1970] | 1774 | ] |
---|
[1974] | 1775 | ] |
---|
[2219] | 1776 | | 2,5: @SimFailNicely |
---|
[1974] | 1777 | | 3,6: // |
---|
| 1778 | ] |
---|
| 1779 | | 69: (* record field *) destruct |
---|
| 1780 | elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 1781 | try @conj try @conj |
---|
| 1782 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1783 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1784 | whd in match (exec_lvalue' ??? (Efield rec_expr f) ty); |
---|
| 1785 | whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); |
---|
| 1786 | [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta |
---|
[2176] | 1787 | [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty' |
---|
| 1788 | | 7: #id #fl | 8: #id #fl | 9: #id ] |
---|
[2219] | 1789 | try (@SimFailNicely) |
---|
[1974] | 1790 | cases Hsim_lvalue |
---|
[2219] | 1791 | [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely |
---|
[1974] | 1792 | | 1,3: cases (exec_lvalue ge en m rec_expr) |
---|
[2219] | 1793 | [ 2,4: #error #_ @SimFailNicely |
---|
[1974] | 1794 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec |
---|
| 1795 | @SimOk #a #H @H ] |
---|
| 1796 | ] |
---|
| 1797 | | 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *) |
---|
| 1798 | >Htype_eq cases (typeof rec_expr1) normalize nodelta |
---|
[2176] | 1799 | [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty' |
---|
| 1800 | | 7: #id #fl | 8: #id #fl | 9: #id ] |
---|
[2219] | 1801 | try (@SimFailNicely) |
---|
[1974] | 1802 | cases Hsim_lvalue |
---|
[2219] | 1803 | [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely |
---|
[1974] | 1804 | | 1,3: cases (exec_lvalue ge en m rec_expr) |
---|
[2219] | 1805 | [ 2,4: #error #_ @SimFailNicely |
---|
[1974] | 1806 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec |
---|
| 1807 | @SimOk #a #H @H ] |
---|
| 1808 | ] |
---|
| 1809 | | 3: // ] |
---|
| 1810 | | 70: (* cost label *) destruct |
---|
| 1811 | elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 1812 | try @conj try @conj |
---|
| 1813 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1814 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 1815 | [ 1: |
---|
| 1816 | cases Hsim_expr |
---|
[2219] | 1817 | [ 2: * #error #Hexec >Hexec @SimFailNicely |
---|
[1974] | 1818 | | 1: cases (exec_expr ??? e1) |
---|
[2219] | 1819 | [ 2: #error #_ @SimFailNicely |
---|
[1974] | 1820 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H |
---|
| 1821 | @SimOk #a #H @H ] |
---|
| 1822 | ] |
---|
| 1823 | | 2: @SimFail /2 by ex_intro/ |
---|
| 1824 | | 3: // |
---|
| 1825 | ] |
---|
[2009] | 1826 | ] qed. |
---|
[1970] | 1827 | |
---|
[2009] | 1828 | (* Propagate cast simplification through statements and programs. *) |
---|
[1970] | 1829 | |
---|
[2009] | 1830 | definition simplify_e ≝ λe. pi1 … (simplify_inside e). |
---|
[1198] | 1831 | |
---|
| 1832 | let rec simplify_statement (s:statement) : statement ≝ |
---|
| 1833 | match s with |
---|
| 1834 | [ Sskip ⇒ Sskip |
---|
| 1835 | | Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2) |
---|
| 1836 | | Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es) |
---|
| 1837 | | Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2) |
---|
| 1838 | | Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *) |
---|
[2391] | 1839 | | Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) |
---|
[1198] | 1840 | | Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) |
---|
| 1841 | | Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *) |
---|
| 1842 | | Sbreak ⇒ Sbreak |
---|
| 1843 | | Scontinue ⇒ Scontinue |
---|
| 1844 | | Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo) |
---|
| 1845 | | Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls) |
---|
| 1846 | | Slabel l s1 ⇒ Slabel l (simplify_statement s1) |
---|
| 1847 | | Sgoto l ⇒ Sgoto l |
---|
| 1848 | | Scost l s1 ⇒ Scost l (simplify_statement s1) |
---|
| 1849 | ] |
---|
| 1850 | and simplify_ls ls ≝ |
---|
| 1851 | match ls with |
---|
| 1852 | [ LSdefault s ⇒ LSdefault (simplify_statement s) |
---|
| 1853 | | LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls') |
---|
| 1854 | ]. |
---|
| 1855 | |
---|
| 1856 | definition simplify_function : function → function ≝ |
---|
| 1857 | λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)). |
---|
| 1858 | |
---|
| 1859 | definition simplify_fundef : clight_fundef → clight_fundef ≝ |
---|
| 1860 | λf. match f with |
---|
| 1861 | [ CL_Internal f ⇒ CL_Internal (simplify_function f) |
---|
| 1862 | | _ ⇒ f |
---|
| 1863 | ]. |
---|
| 1864 | |
---|
| 1865 | definition simplify_program : clight_program → clight_program ≝ |
---|
[2103] | 1866 | λp. transform_program … p (λ_.simplify_fundef). |
---|
[1970] | 1867 | |
---|
[2009] | 1868 | (* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *) |
---|
| 1869 | inductive cont_cast : cont → cont → Prop ≝ |
---|
| 1870 | | cc_stop : cont_cast Kstop Kstop |
---|
| 1871 | | cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k') |
---|
[2391] | 1872 | | cc_while : ∀e,s,k,k'. |
---|
[2009] | 1873 | cont_cast k k' → |
---|
[2391] | 1874 | cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') |
---|
[2009] | 1875 | | cc_dowhile : ∀e,s,k,k'. |
---|
| 1876 | cont_cast k k' → |
---|
| 1877 | cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') |
---|
| 1878 | | cc_for1 : ∀e,s1,s2,k,k'. |
---|
| 1879 | cont_cast k k' → |
---|
| 1880 | cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k') |
---|
| 1881 | | cc_for2 : ∀e,s1,s2,k,k'. |
---|
| 1882 | cont_cast k k' → |
---|
| 1883 | cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k') |
---|
| 1884 | | cc_for3 : ∀e,s1,s2,k,k'. |
---|
| 1885 | cont_cast k k' → |
---|
| 1886 | cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k') |
---|
| 1887 | | cc_switch : ∀k,k'. |
---|
| 1888 | cont_cast k k' → cont_cast (Kswitch k) (Kswitch k') |
---|
| 1889 | | cc_call : ∀r,f,en,k,k'. |
---|
| 1890 | cont_cast k k' → |
---|
| 1891 | cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k'). |
---|
[1970] | 1892 | |
---|
[2009] | 1893 | lemma call_cont_cast : ∀k,k'. |
---|
| 1894 | cont_cast k k' → |
---|
| 1895 | cont_cast (call_cont k) (call_cont k'). |
---|
| 1896 | #k0 #k0' #K elim K /2/ |
---|
| 1897 | qed. |
---|
[1970] | 1898 | |
---|
[2009] | 1899 | inductive state_cast : state → state → Prop ≝ |
---|
| 1900 | | swc_state : ∀f,s,k,k',e,m. |
---|
| 1901 | cont_cast k k' → |
---|
| 1902 | state_cast (State f s k e m) (State (simplify_function f) (simplify_statement s ) k' e m) |
---|
| 1903 | | swc_callstate : ∀fd,args,k,k',m. |
---|
| 1904 | cont_cast k k' → state_cast (Callstate fd args k m) (Callstate (simplify_fundef fd) args k' m) |
---|
| 1905 | | swc_returnstate : ∀res,k,k',m. |
---|
| 1906 | cont_cast k k' → state_cast (Returnstate res k m) (Returnstate res k' m) |
---|
| 1907 | | swc_finalstate : ∀r. |
---|
| 1908 | state_cast (Finalstate r) (Finalstate r) |
---|
| 1909 | . |
---|
[1970] | 1910 | |
---|
[2009] | 1911 | record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { |
---|
| 1912 | rg_find_symbol: ∀s. |
---|
| 1913 | find_symbol ? ge s = find_symbol ? ge' s; |
---|
| 1914 | rg_find_funct: ∀v,f. |
---|
| 1915 | find_funct ? ge v = Some ? f → |
---|
| 1916 | find_funct ? ge' v = Some ? (t f); |
---|
| 1917 | rg_find_funct_ptr: ∀b,f. |
---|
| 1918 | find_funct_ptr ? ge b = Some ? f → |
---|
| 1919 | find_funct_ptr ? ge' b = Some ? (t f) |
---|
| 1920 | }. |
---|
[1970] | 1921 | |
---|
[2009] | 1922 | (* The return type of any function is invariant under cast simplification *) |
---|
| 1923 | lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f. |
---|
| 1924 | // qed. |
---|
| 1925 | |
---|
[2030] | 1926 | |
---|
| 1927 | definition expr_lvalue_ind_combined ≝ |
---|
| 1928 | λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. |
---|
| 1929 | conj ?? |
---|
| 1930 | (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx) |
---|
| 1931 | (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). |
---|
[2009] | 1932 | |
---|
[2074] | 1933 | lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2. |
---|
[2009] | 1934 | #A #r0 #r1 #r2 * |
---|
| 1935 | [ 2: * #error #H >H #_ @SimFail /2 by ex_intro/ |
---|
| 1936 | | 1: cases r0 |
---|
| 1937 | [ 2: #error #_ #_ @SimFail /2 by ex_intro/ |
---|
| 1938 | | 1: #elt #Hsim lapply (Hsim elt (refl ? (OK ? elt))) #H >H // ] |
---|
| 1939 | ] qed. |
---|
| 1940 | |
---|
| 1941 | lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → |
---|
[2074] | 1942 | (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧ |
---|
| 1943 | (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)). |
---|
[2009] | 1944 | #ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined |
---|
| 1945 | [ 1: #sz #ty #i @SimOk #a normalize // |
---|
| 1946 | | 2: #ty #f @SimOk #a normalize // |
---|
| 1947 | | 3: * |
---|
| 1948 | [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
| 1949 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
| 1950 | #ty #Hsim_lvalue try // |
---|
| 1951 | whd in match (Plvalue ???); |
---|
| 1952 | whd in match (exec_expr ????); |
---|
| 1953 | whd in match (exec_expr ????); |
---|
| 1954 | cases Hsim_lvalue |
---|
| 1955 | [ 2,4,6: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ |
---|
| 1956 | | *: cases (exec_lvalue' ge en m ? ty) |
---|
| 1957 | [ 2,4,6: #error #_ @SimFail /2 by ex_intro/ |
---|
| 1958 | | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 1959 | @SimOk // ] |
---|
| 1960 | ] |
---|
| 1961 | | 4: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); |
---|
| 1962 | cases (lookup SymbolTag block en v) normalize nodelta |
---|
| 1963 | [ 2: #block @SimOk // |
---|
| 1964 | | 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk // |
---|
| 1965 | ] |
---|
| 1966 | | 5: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); |
---|
| 1967 | cases Hsim_expr |
---|
| 1968 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
| 1969 | | 1: cases (exec_expr ge en m e) |
---|
| 1970 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
| 1971 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 1972 | @SimOk // ] |
---|
| 1973 | ] |
---|
| 1974 | | 6: #ty #ed #ty' #Hsim_lvalue |
---|
| 1975 | whd in match (exec_expr ????); whd in match (exec_expr ????); |
---|
| 1976 | whd in match (exec_lvalue ????); whd in match (exec_lvalue ????); |
---|
| 1977 | cases Hsim_lvalue |
---|
| 1978 | [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ |
---|
| 1979 | | 1: cases (exec_lvalue' ge en m ed ty') |
---|
| 1980 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
| 1981 | | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 1982 | @SimOk // ] |
---|
| 1983 | ] |
---|
| 1984 | | 7: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
| 1985 | cases Hsim |
---|
| 1986 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
| 1987 | | 1: cases (exec_expr ge en m e) |
---|
| 1988 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
| 1989 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 1990 | @SimOk // ] |
---|
| 1991 | ] |
---|
| 1992 | | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
| 1993 | cases Hsim1 |
---|
| 1994 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
| 1995 | | 1: cases (exec_expr ge en m e1) |
---|
| 1996 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
| 1997 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 1998 | cases Hsim2 |
---|
| 1999 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
| 2000 | | 1: cases (exec_expr ge en m e2) |
---|
| 2001 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
| 2002 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 2003 | @SimOk // ] |
---|
| 2004 | ] |
---|
| 2005 | ] |
---|
| 2006 | ] |
---|
| 2007 | | 9: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
| 2008 | cases Hsim |
---|
| 2009 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
| 2010 | | 1: cases (exec_expr ge en m e) |
---|
| 2011 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
| 2012 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 2013 | @SimOk // ] |
---|
| 2014 | ] (* mergeable with 7 modulo intros *) |
---|
| 2015 | | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
| 2016 | cases Hsim1 |
---|
| 2017 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
| 2018 | | 1: cases (exec_expr ge en m e1) |
---|
| 2019 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
| 2020 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta |
---|
| 2021 | cases (exec_bool_of_val (\fst a) (typeof e1)) |
---|
| 2022 | [ 2: #error @SimFail /2 by ex_intro/ |
---|
| 2023 | | 1: * |
---|
| 2024 | [ 1: (* true branch *) cases Hsim2 |
---|
| 2025 | | 2: (* false branch *) cases Hsim3 ] |
---|
| 2026 | [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
| 2027 | | 1: cases (exec_expr ge en m e2) | 3: cases (exec_expr ge en m e3) ] |
---|
| 2028 | [ 2,4: #error #_ @SimFail /2 by ex_intro/ |
---|
| 2029 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] |
---|
| 2030 | ] |
---|
| 2031 | ] |
---|
| 2032 | ] |
---|
| 2033 | | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
| 2034 | cases Hsim1 |
---|
[2219] | 2035 | [ 2,4: * #error #Hfail >Hfail @SimFailNicely |
---|
[2009] | 2036 | | 1,3: cases (exec_expr ge en m e1) |
---|
[2219] | 2037 | [ 2,4: #error #_ @SimFailNicely |
---|
[2009] | 2038 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta |
---|
| 2039 | cases (exec_bool_of_val ??) |
---|
[2219] | 2040 | [ 2,4: #erro @SimFailNicely |
---|
[2009] | 2041 | | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 2042 | [ 2,3: @SimOk // |
---|
| 2043 | | 1,4: cases Hsim2 |
---|
| 2044 | [ 2,4: * #error #Hfail >Hfail normalize nodelta @SimFail /2 by ex_intro/ |
---|
| 2045 | | 1,3: cases (exec_expr ge en m e2) |
---|
| 2046 | [ 2,4: #error #_ @SimFail /2 by ex_intro/ |
---|
| 2047 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 2048 | @SimOk // ] |
---|
| 2049 | ] |
---|
| 2050 | ] |
---|
| 2051 | ] |
---|
| 2052 | ] |
---|
| 2053 | ] |
---|
| 2054 | | 13: #ty #sizeof_ty @SimOk normalize // |
---|
| 2055 | | 14: #ty #e #ty' #field #Hsim_lvalue |
---|
| 2056 | whd in match (exec_lvalue' ? en m (Efield ??) ty); |
---|
| 2057 | whd in match (exec_lvalue' ge' en m (Efield ??) ty); |
---|
| 2058 | normalize in match (typeof (Expr ??)); |
---|
| 2059 | cases ty' in Hsim_lvalue; normalize nodelta |
---|
[2176] | 2060 | [ 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain |
---|
| 2061 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] |
---|
[2009] | 2062 | #Hsim_lvalue |
---|
| 2063 | try (@SimFail /2 by ex_intro/) |
---|
| 2064 | normalize in match (exec_lvalue ge en m ?); |
---|
| 2065 | normalize in match (exec_lvalue ge' en m ?); |
---|
| 2066 | cases Hsim_lvalue |
---|
| 2067 | [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
| 2068 | | 1,3: cases (exec_lvalue' ge en m e ?) |
---|
| 2069 | [ 2,4: #error #_ @SimFail /2 by ex_intro/ |
---|
| 2070 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 2071 | @SimOk /2 by ex_intro/ ] |
---|
| 2072 | ] |
---|
| 2073 | | 15: #ty #lab #e #Hsim |
---|
| 2074 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 2075 | whd in match (exec_expr ??? (Expr ??)); |
---|
| 2076 | cases Hsim |
---|
| 2077 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
| 2078 | | 1: cases (exec_expr ge en m e) |
---|
| 2079 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
| 2080 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 2081 | @SimOk // ] |
---|
| 2082 | ] (* cf case 7, again *) |
---|
| 2083 | | 16: * |
---|
| 2084 | [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
| 2085 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
| 2086 | #ty normalize in match (is_not_lvalue ?); |
---|
| 2087 | [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_ |
---|
[2219] | 2088 | @SimFailNicely |
---|
[2009] | 2089 | ] qed. |
---|
| 2090 | |
---|
| 2091 | lemma related_globals_expr_simulation : ∀ge,ge',en,m. |
---|
| 2092 | related_globals ? simplify_fundef ge ge' → |
---|
[2074] | 2093 | ∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧ |
---|
[2009] | 2094 | typeof e = typeof (simplify_e e). |
---|
| 2095 | #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); |
---|
| 2096 | cases e #ed #ty cases ed |
---|
| 2097 | [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
| 2098 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
| 2099 | elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) |
---|
| 2100 | * * try // |
---|
| 2101 | cases (exec_expr ge en m (Expr ??)) |
---|
[2219] | 2102 | try (#error #_ #_ #_ @SimFailNicely) |
---|
[2009] | 2103 | * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 2104 | try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?)) |
---|
| 2105 | qed. |
---|
| 2106 | |
---|
| 2107 | lemma related_globals_lvalue_simulation : ∀ge,ge',en,m. |
---|
| 2108 | related_globals ? simplify_fundef ge ge' → |
---|
[2074] | 2109 | ∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧ |
---|
[2009] | 2110 | typeof e = typeof (simplify_e e). |
---|
| 2111 | #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); |
---|
| 2112 | cases e #ed #ty cases ed |
---|
| 2113 | [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
| 2114 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
| 2115 | elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) |
---|
| 2116 | * * try // |
---|
| 2117 | cases (exec_lvalue ge en m (Expr ??)) |
---|
[2219] | 2118 | try (#error #_ #_ #_ @SimFailNicely) |
---|
[2009] | 2119 | * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
| 2120 | (* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *) |
---|
| 2121 | cases e' in Hsim_lvalue ⊢ %; #ed' #ty' whd in match (exec_lvalue ????); whd in match (exec_lvalue ????); |
---|
| 2122 | lapply (proj2 ?? (sim_related_globals ge ge' en m Hrelated) ed' ty') #Hsim_lvalue2 #Hsim_lvalue1 |
---|
| 2123 | try @(simulation_transitive ???? Hsim_lvalue1 Hsim_lvalue2) |
---|
| 2124 | qed. |
---|
| 2125 | |
---|
| 2126 | lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. |
---|
| 2127 | related_globals ? simplify_fundef ge ge' → |
---|
[2074] | 2128 | ∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)). |
---|
[2009] | 2129 | #ge #ge' #en #m #Hrelated #args |
---|
| 2130 | elim args |
---|
| 2131 | [ 1: /3/ |
---|
| 2132 | | 2: #hd #tl #Hind normalize |
---|
| 2133 | elim (related_globals_expr_simulation ge ge' en m Hrelated hd) |
---|
| 2134 | * |
---|
| 2135 | [ 2: * #error #Hfail >Hfail #_ @SimFail /2 by refl, ex_intro/ |
---|
| 2136 | | 1: cases (exec_expr ge en m hd) |
---|
| 2137 | [ 2: #error #_ #_ @SimFail /2 by refl, ex_intro/ |
---|
| 2138 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq |
---|
| 2139 | cases Hind normalize |
---|
| 2140 | [ 2: * #error #Hfail >Hfail @SimFail /2 by refl, ex_intro/ |
---|
| 2141 | | 1: cases (exec_exprlist ??? tl) |
---|
| 2142 | [ 2: #error #_ @SimFail /2 by refl, ex_intro/ |
---|
| 2143 | | 1: * #values #trace #Hsim lapply (Hsim 〈values, trace〉 (refl ? (OK ? 〈values, trace〉))) |
---|
| 2144 | #Heq >Heq @SimOk // ] |
---|
| 2145 | ] |
---|
| 2146 | ] |
---|
| 2147 | ] |
---|
| 2148 | ] qed. |
---|
| 2149 | |
---|
| 2150 | lemma simplify_type_of_fundef_eq : ∀clfd. (type_of_fundef (simplify_fundef clfd)) = (type_of_fundef clfd). |
---|
| 2151 | * // qed. |
---|
| 2152 | |
---|
| 2153 | lemma simplify_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. typeof (simplify_e func) = typeof func. |
---|
| 2154 | #ge #en #m #func whd in match (simplify_e func); elim (simplify_inside func) |
---|
| 2155 | #func' #H lapply (H ge en m) * * #_ #_ // |
---|
| 2156 | qed. |
---|
| 2157 | |
---|
| 2158 | lemma simplify_fun_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. fun_typeof (simplify_e func) = fun_typeof func. |
---|
| 2159 | #ge #en #m #func whd in match (simplify_e func); whd in match (fun_typeof ?) in ⊢ (??%%); |
---|
| 2160 | >simplify_typeof_eq whd in match (simplify_e func); // qed. |
---|
| 2161 | |
---|
| 2162 | lemma simplify_is_not_skip: ∀s.s ≠ Sskip → ∃pf. is_Sskip (simplify_statement s) = inr … pf. |
---|
| 2163 | * |
---|
| 2164 | [ 1: * #Habsurd elim (Habsurd (refl ? Sskip)) |
---|
| 2165 | | *: #a try #b try #c try #d try #e |
---|
| 2166 | whd in match (simplify_statement ?); |
---|
| 2167 | whd in match (is_Sskip ?); |
---|
| 2168 | try /2 by refl, ex_intro/ |
---|
| 2169 | ] qed. |
---|
| 2170 | |
---|
| 2171 | lemma call_cont_simplify : ∀k,k'. |
---|
| 2172 | cont_cast k k' → |
---|
| 2173 | cont_cast (call_cont k) (call_cont k'). |
---|
| 2174 | #k0 #k0' #K elim K /2/ |
---|
| 2175 | qed. |
---|
| 2176 | |
---|
| 2177 | lemma simplify_ls_commute : ∀l. (simplify_statement (seq_of_labeled_statement l)) = (seq_of_labeled_statement (simplify_ls l)). |
---|
| 2178 | #l @(labeled_statements_ind … l) |
---|
| 2179 | [ 1: #default_statement // |
---|
| 2180 | | 2: #sz #i #s #tl #Hind |
---|
| 2181 | whd in match (seq_of_labeled_statement ?) in ⊢ (??%?); |
---|
| 2182 | whd in match (simplify_ls ?) in ⊢ (???%); |
---|
| 2183 | whd in match (seq_of_labeled_statement ?) in ⊢ (???%); |
---|
| 2184 | whd in match (simplify_statement ?) in ⊢ (??%?); |
---|
| 2185 | >Hind // |
---|
| 2186 | ] qed. |
---|
| 2187 | |
---|
[2428] | 2188 | lemma select_switch_simplify_elim : ∀sz,i,l. ∀P:option labeled_statements → option labeled_statements → Prop. |
---|
| 2189 | (P (None ?) (None ?)) → |
---|
| 2190 | (∀l'. P (Some ? l') (Some ? (simplify_ls l'))) → |
---|
| 2191 | P (select_switch sz i l) (select_switch sz i (simplify_ls l)). |
---|
| 2192 | #sz #i #l #P #NONE #SOME @(labeled_statements_ind … l) |
---|
[2009] | 2193 | [ 1: #default_statement // |
---|
| 2194 | | 2: #sz' #i' #s #tl #Hind |
---|
[2428] | 2195 | whd in match (simplify_ls ?); |
---|
| 2196 | whd in match (select_switch ???); whd in match (select_switch ???); |
---|
[2009] | 2197 | cases (sz_eq_dec sz sz') |
---|
| 2198 | [ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true |
---|
[2428] | 2199 | cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta // |
---|
[2009] | 2200 | | 2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq) |
---|
[2428] | 2201 | @NONE |
---|
[2009] | 2202 | ] |
---|
| 2203 | ] qed. |
---|
| 2204 | |
---|
[2011] | 2205 | lemma elim_IH_aux : |
---|
[2009] | 2206 | ∀lab. ∀s:statement.∀k,k'. cont_cast k k' → |
---|
| 2207 | ∀Hind:(∀k:cont.∀k':cont. |
---|
| 2208 | cont_cast k k' → |
---|
| 2209 | match find_label lab s k with |
---|
| 2210 | [ None ⇒ find_label lab (simplify_statement s) k'=None (statement×cont) |
---|
| 2211 | | Some (r:(statement×cont))⇒ |
---|
| 2212 | let 〈s',ks〉 ≝r in |
---|
| 2213 | ∃ks':cont. find_label lab (simplify_statement s) k' = Some (statement×cont) 〈simplify_statement s',ks'〉 |
---|
| 2214 | ∧ cont_cast ks ks']). |
---|
| 2215 | (find_label lab s k = None ? ∧ find_label lab (simplify_statement s) k' = None ?) ∨ |
---|
| 2216 | (∃st,kst,kst'. find_label lab s k = Some ? 〈st,kst〉 ∧ find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement st,kst'〉 ∧ cont_cast kst kst'). |
---|
| 2217 | #lab #s #k #k' #Hcont_cast #Hind |
---|
| 2218 | lapply (Hind k k' Hcont_cast) |
---|
| 2219 | cases (find_label lab s k) |
---|
| 2220 | [ 1: normalize nodelta #Heq >Heq /3/ |
---|
| 2221 | | 2: * #st #kst normalize nodelta * #kst' * #Heq #Hcont_cast' >Heq %2 |
---|
| 2222 | %{st} %{kst} %{kst'} @conj try @conj // |
---|
| 2223 | ] qed. |
---|
| 2224 | |
---|
| 2225 | |
---|
| 2226 | lemma cast_find_label : ∀lab,s,k,k'. |
---|
| 2227 | cont_cast k k' → |
---|
| 2228 | match find_label lab s k with |
---|
| 2229 | [ Some r ⇒ |
---|
| 2230 | let 〈s',ks〉 ≝ r in |
---|
| 2231 | ∃ks'. find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement s', ks'〉 |
---|
| 2232 | ∧ cont_cast ks ks' |
---|
| 2233 | | None ⇒ |
---|
| 2234 | find_label lab (simplify_statement s) k' = None ? |
---|
| 2235 | ]. |
---|
| 2236 | #lab #s @(statement_ind2 ? (λls. |
---|
| 2237 | ∀k:cont |
---|
| 2238 | .∀k':cont |
---|
| 2239 | .cont_cast k k' |
---|
| 2240 | →match find_label_ls lab ls k with |
---|
| 2241 | [None⇒ |
---|
| 2242 | find_label_ls lab (simplify_ls ls) k' = None ? |
---|
| 2243 | |Some r ⇒ |
---|
| 2244 | let 〈s',ks〉 ≝r in |
---|
| 2245 | ∃ks':cont |
---|
| 2246 | .find_label_ls lab (simplify_ls ls) k' |
---|
| 2247 | =Some (statement×cont) 〈simplify_statement s',ks'〉 |
---|
| 2248 | ∧cont_cast ks ks'] |
---|
| 2249 | ) … s) |
---|
| 2250 | [ 1: #k #k' #Hcont_cast |
---|
| 2251 | whd in match (find_label ? Sskip ?); normalize nodelta @refl |
---|
| 2252 | | 2: #e1 #e2 #k #k' #Hcont_cast |
---|
| 2253 | whd in match (find_label ? (Sassign e1 e2) ?); normalize nodelta @refl |
---|
| 2254 | | 3: #e0 #e #args #k #k' #Hcont_cast |
---|
| 2255 | whd in match (find_label ? (Scall e0 e args) ?); normalize nodelta @refl |
---|
| 2256 | | 4: #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast |
---|
| 2257 | whd in match (find_label ? (Ssequence s1 s2) ?); |
---|
| 2258 | whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?); |
---|
[2011] | 2259 | elim (elim_IH_aux lab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1) |
---|
[2009] | 2260 | [ 3: try ( @cc_seq // ) |
---|
| 2261 | | 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2262 | normalize nodelta %{kst'} /2/ |
---|
| 2263 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta |
---|
[2011] | 2264 | elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2) |
---|
[2009] | 2265 | [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' |
---|
| 2266 | normalize nodelta %{kst'} /2/ |
---|
| 2267 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
| 2268 | ] ] |
---|
| 2269 | | 5: #e #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast |
---|
| 2270 | whd in match (find_label ???); |
---|
| 2271 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
[2011] | 2272 | elim (elim_IH_aux lab s1 k k' Hcont_cast Hind_s1) |
---|
[2009] | 2273 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2274 | normalize nodelta %{kst'} /2/ |
---|
| 2275 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta |
---|
[2011] | 2276 | elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2) |
---|
[2009] | 2277 | [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' |
---|
| 2278 | normalize nodelta %{kst'} /2/ |
---|
| 2279 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
| 2280 | ] ] |
---|
[2391] | 2281 | | 6: #e #s #Hind_s #k #k' #Hcont_cast |
---|
[2009] | 2282 | whd in match (find_label ???); |
---|
| 2283 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
[2391] | 2284 | elim (elim_IH_aux lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s) |
---|
[2009] | 2285 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2286 | normalize nodelta %{kst'} /2/ |
---|
| 2287 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
| 2288 | | 3: @cc_while // ] |
---|
| 2289 | | 7: #e #s #Hind_s #k #k' #Hcont_cast |
---|
| 2290 | whd in match (find_label ???); |
---|
| 2291 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
[2011] | 2292 | elim (elim_IH_aux lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s) |
---|
[2009] | 2293 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2294 | normalize nodelta %{kst'} /2/ |
---|
| 2295 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
| 2296 | | 3: @cc_dowhile // ] |
---|
| 2297 | | 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast |
---|
| 2298 | whd in match (find_label ???); |
---|
| 2299 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
[2011] | 2300 | elim (elim_IH_aux lab s1 |
---|
[2009] | 2301 | (Kseq (Sfor Sskip cond s2 s3) k) |
---|
| 2302 | (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k') |
---|
| 2303 | ? Hind_s1) |
---|
| 2304 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2305 | normalize nodelta %{kst'} /2/ |
---|
| 2306 | | 3: @cc_for1 // |
---|
| 2307 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta |
---|
[2011] | 2308 | elim (elim_IH_aux lab s3 |
---|
[2009] | 2309 | (Kfor2 cond s2 s3 k) |
---|
| 2310 | (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') |
---|
| 2311 | ? Hind_s3) |
---|
| 2312 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2313 | normalize nodelta %{kst'} /2/ |
---|
| 2314 | | 3: @cc_for2 // |
---|
| 2315 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta |
---|
[2011] | 2316 | elim (elim_IH_aux lab s2 |
---|
[2009] | 2317 | (Kfor3 cond s2 s3 k) |
---|
| 2318 | (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') |
---|
| 2319 | ? Hind_s2) |
---|
| 2320 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2321 | normalize nodelta %{kst'} /2/ |
---|
| 2322 | | 3: @cc_for3 // |
---|
| 2323 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
| 2324 | ] ] ] |
---|
| 2325 | | 9,10: #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta // |
---|
| 2326 | | 11: #e #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta // |
---|
| 2327 | | 12: #e #ls #Hind #k #k' #Hcont_cast |
---|
| 2328 | whd in match (find_label ???); |
---|
| 2329 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
[2011] | 2330 | (* We can't elim the Hind on a list of labeled statements. We must proceed more manually. *) |
---|
[2009] | 2331 | lapply (Hind (Kswitch k) (Kswitch k') ?) |
---|
| 2332 | [ 1: @cc_switch // |
---|
| 2333 | | 2: cases (find_label_ls lab ls (Kswitch k)) normalize nodelta |
---|
| 2334 | [ 1: // |
---|
| 2335 | | 2: * #st #kst normalize nodelta // ] ] |
---|
| 2336 | | 13: #lab' #s0 #Hind #k #k' #Hcont_cast |
---|
| 2337 | whd in match (find_label ???); |
---|
| 2338 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
| 2339 | cases (ident_eq lab lab') normalize nodelta |
---|
| 2340 | [ 1: #_ %{k'} /2/ |
---|
[2011] | 2341 | | 2: #_ elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) |
---|
[2009] | 2342 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2343 | normalize nodelta %{kst'} /2/ |
---|
| 2344 | | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] |
---|
| 2345 | ] |
---|
| 2346 | | 14: #l #k #k' #Hcont_cast // |
---|
| 2347 | | 15: #l #s0 #Hind #k #k' #Hcont_cast |
---|
| 2348 | whd in match (find_label ???); |
---|
| 2349 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
[2011] | 2350 | elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) |
---|
[2009] | 2351 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2352 | normalize nodelta %{kst'} /2/ |
---|
| 2353 | | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] |
---|
| 2354 | | 16: #s0 #Hind #k #k' #Hcont_cast |
---|
| 2355 | whd in match (find_label ???); |
---|
| 2356 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
[2011] | 2357 | elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) |
---|
[2009] | 2358 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
| 2359 | normalize nodelta %{kst'} /2/ |
---|
| 2360 | | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] |
---|
| 2361 | | 17: #sz #i #s0 #t #Hind_s0 #Hind_ls #k #k' #Hcont_cast |
---|
| 2362 | whd in match (simplify_ls ?); |
---|
| 2363 | whd in match (find_label_ls ???); |
---|
| 2364 | lapply Hind_ls |
---|
| 2365 | @(labeled_statements_ind … t) |
---|
| 2366 | [ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?); |
---|
[2011] | 2367 | elim (elim_IH_aux lab s0 |
---|
[2009] | 2368 | (Kseq default_case k) |
---|
| 2369 | (Kseq (simplify_statement default_case) k') ? Hind_s0) |
---|
| 2370 | [ 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast' |
---|
| 2371 | >Hrewrite >Hrewrite1 |
---|
| 2372 | normalize nodelta whd in match (find_label_ls ???); |
---|
| 2373 | >Hrewrite >Hrewrite1 normalize nodelta |
---|
| 2374 | %{kst'} /2/ |
---|
| 2375 | | 3: @cc_seq // |
---|
| 2376 | | 1: * #Hrewrite #Hrewrite1 >Hrewrite normalize nodelta |
---|
| 2377 | lapply (Hind_ls k k' Hcont_cast) |
---|
| 2378 | cases (find_label_ls lab (LSdefault default_case) k) |
---|
| 2379 | [ 1: normalize nodelta #Heq1 |
---|
| 2380 | whd in match (simplify_ls ?); |
---|
| 2381 | whd in match (find_label_ls lab ??); |
---|
| 2382 | whd in match (seq_of_labeled_statement ?); |
---|
| 2383 | whd in match (find_label_ls lab ??); |
---|
| 2384 | >Hrewrite1 normalize nodelta @Heq1 |
---|
| 2385 | | 2: * #st #kst normalize nodelta #H |
---|
| 2386 | whd in match (find_label_ls lab ??); |
---|
| 2387 | whd in match (simplify_ls ?); |
---|
| 2388 | whd in match (seq_of_labeled_statement ?); |
---|
| 2389 | >Hrewrite1 normalize nodelta @H |
---|
| 2390 | ] |
---|
| 2391 | ] |
---|
| 2392 | | 2: #sz' #i' #s' #tl' #Hind #A |
---|
| 2393 | |
---|
| 2394 | whd in match (seq_of_labeled_statement ?); |
---|
[2011] | 2395 | elim (elim_IH_aux lab s0 |
---|
[2009] | 2396 | (Kseq (Ssequence s' (seq_of_labeled_statement tl')) k) |
---|
| 2397 | (Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k') |
---|
| 2398 | ? |
---|
| 2399 | Hind_s0) |
---|
| 2400 | [ 3: @cc_seq // |
---|
| 2401 | | 1: * #Heq #Heq2 >Heq >Heq2 normalize nodelta |
---|
| 2402 | lapply (A k k' Hcont_cast) |
---|
| 2403 | cases (find_label_ls lab (LScase sz' i' s' tl') k) normalize nodelta |
---|
| 2404 | [ 1: #H whd in match (find_label_ls ???); |
---|
| 2405 | <simplify_ls_commute |
---|
| 2406 | whd in match (seq_of_labeled_statement ?); |
---|
| 2407 | >Heq2 normalize nodelta |
---|
| 2408 | assumption |
---|
| 2409 | | 2: * #st #kst normalize nodelta #H |
---|
| 2410 | whd in match (find_label_ls ???); |
---|
| 2411 | <simplify_ls_commute >Heq2 normalize nodelta @H |
---|
| 2412 | ] |
---|
| 2413 | | 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast' |
---|
| 2414 | >Hrewrite normalize nodelta |
---|
| 2415 | %{kst'} @conj try // |
---|
| 2416 | whd in match (find_label_ls ???); |
---|
| 2417 | <simplify_ls_commute >Hrewrite1 // |
---|
| 2418 | ] |
---|
| 2419 | ] |
---|
| 2420 | ] qed. |
---|
| 2421 | |
---|
| 2422 | lemma cast_find_label_fn : ∀lab,f,k,k',s,ks. |
---|
| 2423 | cont_cast k k' → |
---|
| 2424 | find_label lab (fn_body f) k = Some ? 〈s,ks〉 → |
---|
| 2425 | ∃ks'. find_label lab (fn_body (simplify_function f)) k' = Some ? 〈simplify_statement s,ks'〉 |
---|
| 2426 | ∧ cont_cast ks ks'. |
---|
| 2427 | #lab * #rettype #args #vars #body #k #k' #s #ks #Hcont_cast #Hfind_lab |
---|
| 2428 | whd in match (simplify_function ?); |
---|
| 2429 | lapply (cast_find_label lab body ?? Hcont_cast) |
---|
| 2430 | >Hfind_lab normalize nodelta // |
---|
| 2431 | qed. |
---|
| 2432 | |
---|
| 2433 | theorem cast_correction : ∀ge, ge'. |
---|
| 2434 | related_globals ? simplify_fundef ge ge' → |
---|
| 2435 | ∀s1, s1', tr, s2. |
---|
| 2436 | state_cast s1 s1' → |
---|
| 2437 | exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
| 2438 | ∃s2'. exec_step ge' s1' = Value … 〈tr,s2'〉 ∧ |
---|
| 2439 | state_cast s2 s2'. |
---|
| 2440 | #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hs1_sim_s1' #Houtcome |
---|
| 2441 | inversion Hs1_sim_s1' |
---|
| 2442 | [ 1: (* regular state *) |
---|
| 2443 | #f #stm #k #k' #en #m #Hcont_cast |
---|
| 2444 | lapply (related_globals_expr_simulation ge ge' en m Hrelated) #Hsim_related |
---|
| 2445 | lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related |
---|
| 2446 | cases stm |
---|
| 2447 | (* Perform the intros for the statements*) |
---|
| 2448 | [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body |
---|
| 2449 | | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body |
---|
| 2450 | | 14: #lab | 15: #cost #body ] |
---|
| 2451 | [ 1: (* Skip *) |
---|
| 2452 | #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 |
---|
| 2453 | whd in match (exec_step ??); whd in match (exec_step ??); |
---|
| 2454 | inversion Hcont_cast |
---|
| 2455 | [ 1: (* Kstop *) |
---|
| 2456 | #Hk #Hk' #_ >fn_return_simplify cases (fn_return f) normalize nodelta |
---|
| 2457 | [ 1: >Heq_s1 in Hs1_sim_s1'; >Heq_s1' #Hsim inversion Hsim |
---|
| 2458 | [ 1: #f0 #s #k0 #k0' #e #m0 #Hcont_cast0 #Hstate_eq #Hstate_eq' #_ |
---|
| 2459 | #Eq whd in match (ret ??) in Eq; destruct (Eq) |
---|
| 2460 | %{(Returnstate Vundef Kstop (free_list m (blocks_of_env en)))} @conj |
---|
| 2461 | [ 1: // | 2: %3 %1 ] |
---|
| 2462 | | 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd) |
---|
| 2463 | | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd) |
---|
| 2464 | | 4: #r #Habsurd destruct (Habsurd) ] |
---|
[2176] | 2465 | | 3,4,9: #irrelevant #Habsurd destruct |
---|
[2009] | 2466 | | *: #irrelevant1 #irrelevant2 #Habsurd destruct ] |
---|
| 2467 | | 2: (* Kseq stm' k' *) |
---|
| 2468 | #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
| 2469 | whd in match (ret ??) in Eq; destruct (Eq) |
---|
| 2470 | %{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj |
---|
| 2471 | [ 1: // | 2: %1 // ] |
---|
| 2472 | | 3: (* Kwhile *) |
---|
[2391] | 2473 | #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
[2009] | 2474 | whd in match (ret ??) in Eq; destruct (Eq) |
---|
[2391] | 2475 | %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj |
---|
[2009] | 2476 | [ 1: // | 2: %1 // ] |
---|
| 2477 | | 4: (* Kdowhile *) |
---|
| 2478 | #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
| 2479 | elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond |
---|
| 2480 | [ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct |
---|
| 2481 | | 1: cases (exec_expr ge en m cond) in Eq; |
---|
| 2482 | [ 2: #error whd in match (m_bind ?????) in ⊢ (% → ?); #Habsurd destruct |
---|
| 2483 | | 1: * #val #trace whd in match (m_bind ?????) in ⊢ (% → ?); <Htype_cond_eq |
---|
| 2484 | #Eq #Hsim_cond lapply (Hsim_cond 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) |
---|
| 2485 | #Hrewrite_cond >Hrewrite_cond whd in match (m_bind ?????); |
---|
| 2486 | (* case analysis on the outcome of the conditional *) |
---|
| 2487 | cases (exec_bool_of_val val (typeof cond)) in Eq ⊢ %; |
---|
| 2488 | [ 2: (* evaluation of the conditional fails *) |
---|
| 2489 | #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
| 2490 | | 1: * whd in match (bindIO ??????); |
---|
| 2491 | whd in match (bindIO ??????); |
---|
| 2492 | #Eq destruct (Eq) |
---|
| 2493 | [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)} |
---|
| 2494 | @conj [ 1: // | 2: %1 // ] |
---|
| 2495 | | 2: %{(State (simplify_function f) Sskip k0' en m)} |
---|
| 2496 | @conj [ 1: // | 2: %1 // ] |
---|
| 2497 | ] |
---|
| 2498 | ] |
---|
| 2499 | ] |
---|
| 2500 | ] |
---|
| 2501 | | 5,6,7: |
---|
| 2502 | #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
| 2503 | whd in match (ret ??) in Eq ⊢ %; destruct (Eq) |
---|
| 2504 | [ 1: %{(State (simplify_function f) |
---|
| 2505 | (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) |
---|
| 2506 | k0' en m)} @conj |
---|
| 2507 | [ 1: // | 2: %1 // ] |
---|
| 2508 | | 2: %{(State (simplify_function f) |
---|
| 2509 | (simplify_statement step) |
---|
| 2510 | (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') |
---|
| 2511 | en m)} @conj |
---|
| 2512 | [ 1: // | 2: %1 @cc_for3 // ] |
---|
| 2513 | | 3: %{(State (simplify_function f) |
---|
| 2514 | (Sfor Sskip (simplify_e cond) (simplify_statement step) |
---|
| 2515 | (simplify_statement body)) |
---|
| 2516 | k0' en m)} @conj |
---|
| 2517 | [ 1: // | 2: %1 // ] |
---|
| 2518 | ] |
---|
| 2519 | | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
| 2520 | whd in match (ret ??) in Eq ⊢ %; destruct (Eq) |
---|
| 2521 | %{(State (simplify_function f) Sskip k0' en m)} @conj |
---|
| 2522 | [ 1: // | 2: %1 // ] |
---|
| 2523 | | 9: (* Call *) |
---|
| 2524 | #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ #Eq |
---|
| 2525 | >fn_return_simplify cases (fn_return f) in Eq; normalize nodelta |
---|
| 2526 | [ 1: #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq) |
---|
| 2527 | %{(Returnstate Vundef (Kcall r (simplify_function f0) en0 k0') |
---|
| 2528 | (free_list m (blocks_of_env en)))} @conj |
---|
| 2529 | [ 1: // | 2: %3 @cc_call // ] |
---|
[2176] | 2530 | | 3,4,9: #irrelevant #Habsurd destruct (Habsurd) |
---|
[2009] | 2531 | | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ] |
---|
| 2532 | ] |
---|
| 2533 | | 2: (* Assign *) |
---|
| 2534 | #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 |
---|
| 2535 | whd in match (simplify_statement ?); #Heq |
---|
| 2536 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2537 | (* Begin by making the simplify_e disappear using Hsim_related *) |
---|
| 2538 | elim (Hsim_lvalue_related lhs) * |
---|
| 2539 | [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2540 | | 1: cases (exec_lvalue ge en m lhs) in Heq; |
---|
| 2541 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2542 | | 1: * * #block #offset #trace |
---|
| 2543 | whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_lhs |
---|
| 2544 | lapply (Hsim 〈block, offset, trace〉 (refl ? (OK ? 〈block, offset, trace〉))) |
---|
| 2545 | #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????); |
---|
| 2546 | (* After [lhs], treat [rhs] *) |
---|
| 2547 | elim (Hsim_related rhs) * |
---|
| 2548 | [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2549 | | 1: cases (exec_expr ge en m rhs) in Heq; |
---|
| 2550 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2551 | | 1: * #val #trace |
---|
| 2552 | whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_rhs |
---|
| 2553 | lapply (Hsim 〈val, trace〉 (refl ? (OK ? 〈val, trace〉))) |
---|
| 2554 | #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????); |
---|
| 2555 | <Htype_eq_lhs <Htype_eq_rhs |
---|
| 2556 | cases (opt_to_io ?????) in Heq; |
---|
| 2557 | [ 1: #o #resumption whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
| 2558 | | 3: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
| 2559 | | 2: #mem whd in match (bindIO ??????); #Heq destruct (Heq) |
---|
| 2560 | %{(State (simplify_function f) Sskip k' en mem)} @conj |
---|
| 2561 | [ 1: // | 2: %1 // ] |
---|
| 2562 | ] |
---|
| 2563 | ] |
---|
| 2564 | ] |
---|
| 2565 | ] |
---|
| 2566 | ] |
---|
| 2567 | | 3: (* Call *) |
---|
| 2568 | #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 |
---|
| 2569 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2570 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2571 | elim (Hsim_related func) in Heq; * |
---|
| 2572 | [ 2: * #error #Hfail >Hfail #Htype_eq #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2573 | | 1: cases (exec_expr ??? func) |
---|
| 2574 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2575 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq |
---|
| 2576 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
| 2577 | elim (related_globals_exprlist_simulation ge ge' en m Hrelated args) |
---|
| 2578 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2579 | | 1: cases (exec_exprlist ge en m args) |
---|
| 2580 | [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2581 | | 1: #l -Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq |
---|
| 2582 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
| 2583 | elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a)) |
---|
| 2584 | cases (find_funct clight_fundef ge (\fst a)); |
---|
| 2585 | [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2586 | | 2: #clfd -Hsim #Hsim lapply (Hsim clfd (refl ? (Some ? clfd))) #Heq >Heq |
---|
| 2587 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
| 2588 | >simplify_type_of_fundef_eq >(simplify_fun_typeof_eq ge en m) |
---|
| 2589 | cases (assert_type_eq (type_of_fundef clfd) (fun_typeof func)) |
---|
| 2590 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2591 | | 1: #Htype_eq cases ret |
---|
| 2592 | [ 1: whd in match (bindIO ??????) in ⊢ (% → %); |
---|
| 2593 | #Eq destruct (Eq) |
---|
| 2594 | %{(Callstate (simplify_fundef clfd) (\fst l) |
---|
| 2595 | (Kcall (None (block×offset×type)) (simplify_function f) en k') m)} |
---|
| 2596 | @conj |
---|
| 2597 | [ 1: // | 2: %2 @cc_call // ] |
---|
| 2598 | | 2: #fptr whd in match (bindIO ??????) in ⊢ (% → %); |
---|
| 2599 | elim (Hsim_lvalue_related fptr) * |
---|
| 2600 | [ 2: * #error #Hfail >Hfail #_ |
---|
| 2601 | #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2602 | | 1: cases (exec_lvalue ge en m fptr) |
---|
| 2603 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2604 | | 1: #a #Hsim #Htype_eq_fptr >(Hsim a (refl ? (OK ? a))) |
---|
| 2605 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
| 2606 | #Heq destruct (Heq) |
---|
| 2607 | %{(Callstate (simplify_fundef clfd) (\fst l) |
---|
| 2608 | (Kcall (Some (block×offset×type) 〈\fst a,typeof (simplify_e fptr)〉) |
---|
| 2609 | (simplify_function f) en k') m)} |
---|
| 2610 | @conj [ 1: // | 2: >(simplify_typeof_eq ge en m) %2 @cc_call // ] |
---|
| 2611 | ] ] ] ] ] ] ] ] ] |
---|
| 2612 | | 4: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2613 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2614 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2615 | destruct (Heq) |
---|
| 2616 | %{(State (simplify_function f) (simplify_statement stm1) (Kseq (simplify_statement stm2) k') en m)} |
---|
| 2617 | @conj |
---|
| 2618 | [ 1: // | 2: %1 @cc_seq // ] |
---|
| 2619 | | 5: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2620 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2621 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2622 | elim (Hsim_related cond) in Heq; * |
---|
| 2623 | [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2624 | | 1: cases (exec_expr ge en m cond) |
---|
| 2625 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2626 | | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq |
---|
| 2627 | #Htype_eq_cond |
---|
| 2628 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
| 2629 | >(simplify_typeof_eq ge en m) |
---|
| 2630 | cases (exec_bool_of_val condval (typeof cond)) |
---|
| 2631 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2632 | | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %; |
---|
| 2633 | [ 1: destruct skip (condtrace) |
---|
| 2634 | %{(State (simplify_function f) (simplify_statement iftrue) k' en m)} @conj |
---|
| 2635 | [ 1: // | 2: <e0 %1 // ] |
---|
| 2636 | | 2: destruct skip (condtrace) |
---|
| 2637 | %{(State (simplify_function f) (simplify_statement iffalse) k' en m)} @conj |
---|
| 2638 | [ 1: // | 2: <e0 %1 // ] |
---|
| 2639 | ] ] ] ] |
---|
[2391] | 2640 | | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
[2009] | 2641 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2642 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2643 | elim (Hsim_related cond) in Heq; * |
---|
| 2644 | [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2645 | | 1: cases (exec_expr ge en m cond) |
---|
| 2646 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2647 | | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq |
---|
| 2648 | #Htype_eq_cond |
---|
| 2649 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
| 2650 | >(simplify_typeof_eq ge en m) |
---|
| 2651 | cases (exec_bool_of_val condval (typeof cond)) |
---|
| 2652 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2653 | | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %; |
---|
| 2654 | [ 1: destruct skip (condtrace) |
---|
[2391] | 2655 | %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)} |
---|
[2009] | 2656 | @conj |
---|
| 2657 | [ 1: // | 2: <e0 %1 @cc_while // ] |
---|
| 2658 | | 2: destruct skip (condtrace) |
---|
[2391] | 2659 | %{(State (simplify_function f) Sskip k' en m)} @conj |
---|
| 2660 | [ 1: // | 2: <e0 %1 // ] |
---|
[2009] | 2661 | ] ] ] ] |
---|
| 2662 | | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2663 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2664 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2665 | destruct (Heq) |
---|
| 2666 | %{(State (simplify_function f) (simplify_statement body) |
---|
| 2667 | (Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj |
---|
| 2668 | [ 1: // | 2: %1 @cc_dowhile // ] |
---|
| 2669 | | 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2670 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2671 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2672 | cases (is_Sskip init) in Heq; |
---|
| 2673 | [ 2: #Hinit_neq_Sskip elim (simplify_is_not_skip init Hinit_neq_Sskip) #pf #Hrewrite >Hrewrite |
---|
| 2674 | normalize nodelta |
---|
| 2675 | whd in match (ret ??) in ⊢ (% → %); |
---|
| 2676 | #Eq destruct (Eq) |
---|
| 2677 | %{(State (simplify_function f) (simplify_statement init) |
---|
| 2678 | (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj |
---|
| 2679 | [ 1: // | 2: %1 @cc_for1 // ] |
---|
| 2680 | | 1: #Hinit_eq_Sskip >Hinit_eq_Sskip |
---|
| 2681 | whd in match (simplify_statement ?); |
---|
| 2682 | whd in match (is_Sskip ?); |
---|
| 2683 | normalize nodelta |
---|
| 2684 | elim (Hsim_related cond) * |
---|
| 2685 | [ 2: * #error #Hfail #_ >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2686 | | 1: cases (exec_expr ge en m cond) |
---|
| 2687 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2688 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite #Htype_eq_cond >Hrewrite |
---|
| 2689 | whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 2690 | <Htype_eq_cond |
---|
| 2691 | cases (exec_bool_of_val ? (typeof cond)) |
---|
| 2692 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2693 | | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????); |
---|
| 2694 | normalize nodelta #Heq destruct (Heq) |
---|
| 2695 | [ 1: %{(State (simplify_function f) (simplify_statement body) |
---|
| 2696 | (Kfor2 (simplify_e cond) (simplify_statement step) (simplify_statement body) k') en m)} |
---|
| 2697 | @conj [ 1: // | 2: %1 @cc_for2 // ] |
---|
| 2698 | | 2: %{(State (simplify_function f) Sskip k' en m)} @conj |
---|
| 2699 | [ 1: // | 2: %1 // ] |
---|
| 2700 | ] ] ] ] ] |
---|
| 2701 | | 9: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2702 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2703 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2704 | inversion Hcont_cast in Heq; normalize nodelta |
---|
| 2705 | [ 1: #Hk #Hk' #_ |
---|
| 2706 | | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
[2391] | 2707 | | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
[2009] | 2708 | | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
| 2709 | | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
| 2710 | | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
| 2711 | | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] |
---|
| 2712 | #H whd in match (ret ??) in H ⊢ %; |
---|
| 2713 | destruct (H) |
---|
| 2714 | [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ] |
---|
[2391] | 2715 | | 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ] |
---|
[2009] | 2716 | | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2717 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2718 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2719 | inversion Hcont_cast in Heq; normalize nodelta |
---|
| 2720 | [ 1: #Hk #Hk' #_ |
---|
| 2721 | | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
[2391] | 2722 | | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
[2009] | 2723 | | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
| 2724 | | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
| 2725 | | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
| 2726 | | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] |
---|
| 2727 | #H whd in match (ret ??) in H ⊢ %; |
---|
| 2728 | destruct (H) |
---|
| 2729 | [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 // |
---|
[2391] | 2730 | | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} |
---|
[2009] | 2731 | @conj try // %1 // |
---|
| 2732 | | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H; |
---|
| 2733 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2734 | | 1: cases (exec_expr ??? cond) |
---|
| 2735 | [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2736 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
| 2737 | whd in match (m_bind ?????) in ⊢ (% → %); |
---|
| 2738 | <Htype_cond_eq |
---|
| 2739 | cases (exec_bool_of_val ? (typeof cond)) |
---|
| 2740 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2741 | | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????); |
---|
| 2742 | normalize nodelta #Heq destruct (Heq) |
---|
| 2743 | [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)} |
---|
| 2744 | @conj [ 1: // | 2: %1 // ] |
---|
| 2745 | | 2: %{(State (simplify_function f) Sskip k0' en m)} |
---|
| 2746 | @conj [ 1: // | 2: %1 // ] |
---|
| 2747 | ] ] ] ] |
---|
| 2748 | | 5: %{(State (simplify_function f) (simplify_statement step) |
---|
| 2749 | (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj |
---|
| 2750 | [ 1: // | 2: %1 @cc_for3 // ] |
---|
| 2751 | ] |
---|
| 2752 | | 11: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2753 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2754 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2755 | cases retval in Heq; normalize nodelta |
---|
| 2756 | [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta |
---|
| 2757 | whd in match (ret ??) in ⊢ (% → %); |
---|
[2176] | 2758 | [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty' |
---|
| 2759 | | 7: #id #fl | 8: #id #fl | 9: #id ] |
---|
[2009] | 2760 | #H destruct (H) |
---|
| 2761 | %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))} |
---|
| 2762 | @conj [ 1: // | 2: %3 @call_cont_simplify // ] |
---|
| 2763 | | 2: #e >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta |
---|
| 2764 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
| 2765 | | 2: #_ elim (Hsim_related e) * |
---|
| 2766 | [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2767 | | 1: cases (exec_expr ??? e) |
---|
| 2768 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2769 | | 1: #a #Hsim #Htype_eq_e lapply (Hsim a (refl ? (OK ? a))) |
---|
| 2770 | #Hrewrite >Hrewrite |
---|
| 2771 | whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 2772 | #Heq destruct (Heq) |
---|
| 2773 | %{(Returnstate (\fst a) (call_cont k') (free_list m (blocks_of_env en)))} |
---|
| 2774 | @conj [ 1: // | 2: %3 @call_cont_simplify // ] |
---|
| 2775 | ] ] ] ] |
---|
| 2776 | | 12: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2777 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2778 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2779 | elim (Hsim_related cond) in Heq; * |
---|
| 2780 | [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2781 | | 1: cases (exec_expr ??? cond) |
---|
| 2782 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2783 | | 1: #a #Hsim #Htype_eq_cond lapply (Hsim a (refl ? (OK ? a))) |
---|
| 2784 | #Hrewrite >Hrewrite |
---|
| 2785 | whd in match (bindIO ??????); whd in match (bindIO ??????); |
---|
| 2786 | cases (\fst a) normalize nodelta |
---|
| 2787 | [ 1,3,4,5: #a destruct (a) #b destruct (b) |
---|
[2428] | 2788 | | 2: #sz #i <Htype_eq_cond cases (typeof cond) |
---|
| 2789 | [ 1,3,4,5,6,7,8,9: normalize nodelta #a try #b try #c destruct] |
---|
| 2790 | #sz' #sg normalize nodelta cases (sz_eq_dec sz sz') |
---|
| 2791 | #SZ [2: normalize nodelta #E destruct ] |
---|
| 2792 | normalize nodelta @select_switch_simplify_elim |
---|
| 2793 | [ #H whd in H:(??%?); destruct ] |
---|
| 2794 | #l' whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 2795 | #Heq destruct (Heq) |
---|
[2009] | 2796 | %{(State (simplify_function f) |
---|
[2428] | 2797 | (seq_of_labeled_statement (simplify_ls l')) |
---|
[2009] | 2798 | (Kswitch k') en m)} @conj |
---|
| 2799 | [ 1: // |
---|
[2428] | 2800 | | 2: @(labeled_statements_ind … l') |
---|
[2009] | 2801 | [ 1: #default_s |
---|
| 2802 | whd in match (simplify_ls ?); |
---|
| 2803 | whd in match (select_switch sz i ?) in ⊢ (?%%); |
---|
| 2804 | whd in match (seq_of_labeled_statement ?) in ⊢ (?%%); |
---|
| 2805 | %1 @cc_switch // |
---|
| 2806 | | 2: #sz' #i' #top_case #tail #Hind |
---|
[2428] | 2807 | <simplify_ls_commute |
---|
| 2808 | %1 @cc_switch // |
---|
| 2809 | ] ] ] ] ] |
---|
[2009] | 2810 | | 13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2811 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2812 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2813 | destruct (Heq) |
---|
| 2814 | %{(State (simplify_function f) (simplify_statement body) k' en m)} |
---|
| 2815 | @conj %1 // |
---|
| 2816 | | 14: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2817 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2818 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2819 | lapply (cast_find_label_fn lab f (call_cont k) (call_cont k')) |
---|
| 2820 | cases (find_label lab (fn_body f) (call_cont k)) in Heq; |
---|
| 2821 | normalize nodelta |
---|
| 2822 | [ 1: #Habsurd destruct (Habsurd) |
---|
| 2823 | | 2: * #st #kst normalize nodelta |
---|
| 2824 | #Heq whd in match (ret ??) in Heq; |
---|
| 2825 | #H lapply (H st kst (call_cont_simplify ???) (refl ? (Some ? 〈st,kst〉))) try // |
---|
| 2826 | * #kst' * #Heq2 #Hcont_cast' >Heq2 normalize nodelta |
---|
| 2827 | destruct (Heq) |
---|
| 2828 | %{(State (simplify_function f) (simplify_statement st) kst' en m)} @conj |
---|
| 2829 | [ 1: // | 2: %1 // ] |
---|
| 2830 | ] |
---|
| 2831 | | 15: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2832 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
| 2833 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
| 2834 | destruct (Heq) |
---|
| 2835 | %{(State (simplify_function f) (simplify_statement body) k' en m)} |
---|
| 2836 | @conj |
---|
| 2837 | [ 1: // | 2: %1 // ] |
---|
| 2838 | ] |
---|
| 2839 | | 2: (* Call state *) |
---|
| 2840 | #fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2841 | whd in match (exec_step ??) in ⊢ (% → %); |
---|
| 2842 | elim fd in Heq_s1'; normalize nodelta |
---|
| 2843 | [ 1: * #rettype #args #vars #body #Heq_s1' |
---|
| 2844 | whd in match (simplify_function ?); |
---|
| 2845 | cases (exec_alloc_variables empty_env ??) |
---|
| 2846 | #local_env #new_mem normalize nodelta |
---|
| 2847 | cases (exec_bind_parameters ????) |
---|
| 2848 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2849 | | 1: #new_mem_init |
---|
| 2850 | whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 2851 | #Heq destruct (Heq) |
---|
| 2852 | %{(State (mk_function rettype args vars (simplify_statement body)) |
---|
| 2853 | (simplify_statement body) k' local_env new_mem_init)} @conj |
---|
| 2854 | [ 1: // | 2: %1 // ] |
---|
| 2855 | ] |
---|
| 2856 | | 2: #id #argtypes #rettype #Heq_s1' |
---|
| 2857 | cases (check_eventval_list args ?) |
---|
| 2858 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 2859 | | 1: #l whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 2860 | #Habsurd destruct (Habsurd) ] |
---|
| 2861 | ] |
---|
| 2862 | | 3: (* Return state *) |
---|
| 2863 | #res #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2864 | whd in match (exec_step ??) in ⊢ (% → %); |
---|
| 2865 | inversion Hcont_cast |
---|
| 2866 | [ 1: #Hk #Hk' #_ |
---|
| 2867 | | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
[2391] | 2868 | | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
[2009] | 2869 | | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
| 2870 | | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
| 2871 | | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
| 2872 | | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] |
---|
| 2873 | normalize nodelta |
---|
| 2874 | [ 1: cases res normalize nodelta |
---|
| 2875 | [ 2: * normalize nodelta #i |
---|
| 2876 | [ 3: #Heq whd in match (ret ??) in Heq; destruct (Heq) |
---|
| 2877 | %{(Finalstate i)} @conj [ 1: // | 2: // ] |
---|
| 2878 | | * : #Habsurd destruct (Habsurd) ] |
---|
| 2879 | | *: #a try #b destruct ] |
---|
| 2880 | | 9: elim r normalize nodelta |
---|
| 2881 | [ 2: * * #block #offset #typ normalize nodelta |
---|
| 2882 | cases (opt_to_io io_out io_in mem ? (store_value_of_type' ????)) |
---|
| 2883 | [ 2: #mem whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 2884 | #Heq destruct (Heq) |
---|
| 2885 | %{(State (simplify_function f0) Sskip k0' en0 mem)} @conj |
---|
| 2886 | [ 1: // | 2: %1 // ] |
---|
| 2887 | | 1: #output #resumption |
---|
| 2888 | whd in match (m_bind ?????); #Habsurd destruct (Habsurd) |
---|
| 2889 | | 3: #eror #Habsurd normalize in Habsurd; destruct (Habsurd) ] |
---|
| 2890 | | 1: #Heq whd in match (ret ??) in Heq; destruct (Heq) |
---|
| 2891 | %{(State (simplify_function f0) Sskip k0' en0 m)} @conj |
---|
| 2892 | [ 1: // | 2: %1 // ] |
---|
| 2893 | ] |
---|
| 2894 | | *: #Habsurd destruct (Habsurd) ] |
---|
| 2895 | | 4: (* Final state *) |
---|
| 2896 | #r #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
| 2897 | whd in match (exec_step ??) in ⊢ (% → %); |
---|
| 2898 | #Habsurd destruct (Habsurd) |
---|
[2184] | 2899 | ] qed. |
---|