Changeset 2009 for src/Clight/SimplifyCasts.ma
- Timestamp:
- May 30, 2012, 9:34:19 PM (7 years ago)
- File:
-
- 1 edited
-
src/Clight/SimplifyCasts.ma (modified) (45 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/SimplifyCasts.ma
r1974 r2009 20 20 *) 21 21 22 23 24 22 (* Attempt to squeeze integer constant into a given type. 25 23 26 24 This might be too conservative --- if we're going to cast it anyway, can't 27 I just ignore the fact that the integer doesn't fit? 25 I just ignore the fact that the integer doesn't fit?let (++) 28 26 *) 29 27 … … 103 101 (* /!\ This lemma uses the "uniqueness of identity proofs" K axiom. I've tried doing a proper 104 102 * induction on t but it turns out to be a non-well-founded pandora box. /!\ *) 103 (* Finally useless 105 104 lemma type_eq_dec_identity : ∀t. type_eq_dec t t = inl ?? (refl ? t). 106 105 #t elim (type_eq_dec t t) 107 106 [ 1: @streicherK // 108 107 | 2: #H elim H #Hcontr elim (Hcontr (refl ? t)) ] qed. 109 110 108 *) 109 110 (* Useless 111 111 lemma sign_eq_dec : ∀s1,s2:signedness. (s1 = s2) ∨ (s1 ≠ s2). 112 112 * * /2/ %2 % #H destruct 113 113 qed. 114 *) 114 115 115 116 lemma eq_intsize_identity : ∀id. eq_intsize id id = true. … … 131 132 | 2: #Hneq' normalize // ] qed. 132 133 134 (* Useless 133 135 lemma type_eq_eq : ∀t1, t2. type_eq t1 t2 = true → t1 = t2. 134 136 #t1 #t2 whd in match (type_eq ??); cases (type_eq_dec t1 t2) normalize 135 137 [ 1: // | 2: #_ #H destruct ] qed. 138 *) 136 139 137 140 definition size_le ≝ λsz1,sz2. … … 173 176 #H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed. 174 177 175 176 178 (* This defines necessary conditions for [src_expr] to be coerced to "target_ty". 177 179 * Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *) … … 191 193 192 194 (* Used to inject boolean functions in invariants. *) 195 (* Useless 193 196 definition is_true : bool → Prop ≝ λb. 194 197 match b with 195 198 [ true ⇒ True 196 199 | false ⇒ False ]. 200 *) 197 201 198 202 (* An useful lemma to cull out recursive calls: the guard forces the target type to be different from the origin type. *) 199 203 200 204 (* aux lemma *) 205 (* Useless 201 206 lemma size_lt_dec_not_refl : ∀sz. ∃H. size_lt_dec sz sz = inr ??H. 202 207 * normalize @(ex_intro … (nmk False (λauto:False.auto))) // qed. 203 204 205 208 *) 209 210 (* Inversion on necessary_conditions *) 206 211 lemma necessary_conditions_spec : 207 212 ∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) → … … 219 224 ] 220 225 ] qed. 221 222 226 223 227 … … 255 259 ]. 256 260 261 (* Inversion on smaller_integer_val *) 257 262 lemma smaller_integer_val_spec : ∀src_sz,dst_sz,sg,val1,val2,tr1,tr2. 258 263 smaller_integer_val src_sz dst_sz sg (OK ? 〈val1, tr1〉) (OK ? 〈val2, tr2〉) → … … 274 279 ] 275 280 ] 276 ] qed. 277 278 definition is_integer_type ≝ λty. 279 match ty with 280 [ Tint _ _ ⇒ True 281 | _ ⇒ False 282 ]. 283 284 285 281 ] qed. 282 283 (* Simulation relation used for expression evaluation. *) 286 284 inductive simulate (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝ 287 285 | SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → simulate A r1 r2 288 286 | SimFail : (∃err. r1 = Error ? err) → simulate A r1 r2. 289 287 288 (* Invariant of simplify_expr *) 290 289 inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝ 290 (* Inv_eq states a standard simulation result. We enforce some needed equations on types to prove the cast cases. *) 291 291 | Inv_eq : ∀result_flag. 292 292 result_flag = false → … … 295 295 simulate ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) → 296 296 simplify_inv ge en m e1 e2 target_sz target_sg result_flag 297 (* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *) 297 298 | Inv_coerce_ok : ∀src_sz,src_sg. 298 299 (typeof e1) = (Tint src_sz src_sg) → … … 300 301 (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) → 301 302 simplify_inv ge en m e1 e2 target_sz target_sg true. 302 303 304 (* This lemma proves that simplify_int actually implements an integer cast. This is central to the proof of correctness. *) 305 (* The case 4 can be merged with cases 7 and 8. *) 303 304 definition conservation ≝ λe,result:expr. 305 ∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result) 306 ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 307 ∧ typeof e = typeof result. 308 309 (* This lemma proves that simplify_int actually implements an integer cast. *) 310 (* The case 4 can be merged with cases 7 and 8. *) 311 306 312 lemma simplify_int_implements_cast : ∀sz,sz'.∀sg,sg'.∀i,i'. simplify_int sz sz' sg sg' i = Some ? i' → i' = cast_int_int sz sg sz' i. 307 313 * * … … 380 386 qed. 381 387 382 lemma prod_eq_left:383 ∀A: Type[0].384 ∀p, q, r: A.385 p = q → 〈p, r〉 = 〈q, r〉.386 #A #p #q #r #hyp387 >hyp %388 qed.389 390 lemma prod_eq_right:391 ∀A: Type[0].392 ∀p, q, r: A.393 p = q → 〈r, p〉 = 〈r, q〉.394 #A #p #q #r #hyp395 >hyp %396 qed.397 398 388 corollary prod_vector_zero_eq_left: 399 389 ∀A, n. … … 589 579 // 590 580 ] 591 qed.592 593 lemma tail_eat_cons : ∀A. ∀n. ∀hd:A. ∀v:Vector A n. tail A n (hd ::: v) = v.594 #A #n #hd #v normalize //595 qed.596 597 lemma tail_eat_pad : ∀A. ∀padelt. ∀padlen, veclen. ∀v:Vector A veclen.598 tail A ? (pad_vector A padelt (S padlen) veclen v) = pad_vector A padelt padlen veclen v.599 # A #padelt #padlen #veclen #v600 normalize //601 581 qed. 602 582 … … 914 894 * more or less "modular", case-by-case wise. 915 895 *) 916 let rec simplify_expr 2(e:expr) (target_sz:intsize) (target_sg:signedness)896 let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) 917 897 : Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ 918 898 match e return λx. x = e → ? with … … 961 941 match assert_type_eq (typeof lhs) (typeof rhs) with 962 942 [ OK Htylhs_eq_tyrhs ⇒ 963 let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr 2lhs target_sz target_sg in964 let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr 2rhs target_sz target_sg in943 let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr lhs target_sz target_sg in 944 let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr rhs target_sz target_sg in 965 945 match desired_type_lhs ∧ desired_type_rhs 966 946 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))) … … 997 977 with 998 978 [ true ⇒ λHconditions. 999 let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr 2castee target_sz target_sg in979 let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr castee target_sz target_sg in 1000 980 match desired_type return λx. desired_type = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) 1001 981 with … … 1003 983 «〈true, castee1〉, ?» 1004 984 | false ⇒ λHdesired_eq. 1005 let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr 2castee cast_sz cast_sg in985 let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in 1006 986 match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) 1007 987 with … … 1013 993 ] (refl ? desired_type) 1014 994 | false ⇒ λHconditions. 1015 let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr 2castee cast_sz cast_sg in995 let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in 1016 996 match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) 1017 997 with … … 1037 1017 match assert_type_eq (typeof iftrue) (typeof iffalse) with 1038 1018 [ OK Hiftrue_eq_iffalse ⇒ 1039 let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue ≝ simplify_expr 2iftrue target_sz target_sg in1040 let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr 2iffalse target_sz target_sg in1019 let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue ≝ simplify_expr iftrue target_sz target_sg in 1020 let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr iffalse target_sz target_sg in 1041 1021 match desired_true ∧ desired_false 1042 1022 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))) … … 1077 1057 match type_eq_dec ty (typeof e1) with 1078 1058 [ inl Heq ⇒ 1079 let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr 2e1 target_sz target_sg in1059 let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr e1 target_sz target_sg in 1080 1060 «〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?» 1081 | inr H eq ⇒1061 | inr Hneq ⇒ 1082 1062 let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in 1083 1063 «〈false, Expr (Ecost l e2) ty〉, ?» … … 1089 1069 ] (refl ? e) 1090 1070 1091 and simplify_inside (e:expr) : Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result) 1092 ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 1093 ∧ typeof e = typeof result) ≝ 1071 and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝ 1094 1072 match e return λx. x = e → ? with 1095 1073 [ Expr ed ty ⇒ λHexpr_eq. … … 1111 1089 match type_eq_dec ty cast_ty with 1112 1090 [ inl Hcast_eq ⇒ 1113 match cast_ty return λx. x = cast_ty → Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result) 1114 ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 1115 ∧ typeof e = typeof result) 1091 match cast_ty return λx. x = cast_ty → Σresult:expr. conservation e result 1116 1092 with 1117 1093 [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq. 1118 let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr2 castee cast_sz cast_sg in 1119 match success return λx. x = success → Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result) 1120 ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 1121 ∧ typeof e = typeof result) 1094 let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr castee cast_sz cast_sg in 1095 match success return λx. x = success → Σresult:expr. conservation e result 1122 1096 with 1123 1097 [ true ⇒ λHsuccess_eq. … … 1156 1130 ] (refl ? e). 1157 1131 #ge #en #m 1158 [ 1,3,5,6,7,8,9,10,11,12: %1 //1132 [ 1,3,5,6,7,8,9,10,11,12: %1 try @refl 1159 1133 cases (exec_expr ge en m e) #res 1160 1134 try (@(SimOk ???) //) 1161 1135 | 13,14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res 1162 1136 try (@(SimOk ???) //) 1163 | 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct / /1137 | 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/ 1164 1138 whd in match (exec_expr ????); >eq_intsize_identity whd 1165 >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ] 1166 | 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / /1139 >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ] 1140 | 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/ 1167 1141 whd in match (exec_expr ????); 1168 1142 whd in match (exec_expr ????); 1169 1143 >eq_intsize_identity >eq_intsize_identity whd 1170 >sz_eq_identity >sz_eq_identity whd @conj try @conj //1144 >sz_eq_identity >sz_eq_identity whd @conj try @conj try @refl 1171 1145 [ 1: @(simplify_int_implements_cast … Hsimpl_eq) 1172 1146 | 2: @(simplify_int_success_lt … Hsimpl_eq) ] 1173 | 15: destruct %1 //elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq1147 | 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 1174 1148 [ 1: (* Proving preservation of the semantics for expressions. *) 1175 1149 cases Hexpr_sim 1176 1150 [ 2: (* Case where the evaluation of e1 as an expression fails *) 1177 normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 /1151 normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/ 1178 1152 | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1179 1153 #Hsim %1 * #val #trace normalize #Hstep … … 1205 1179 cases Hexpr_sim 1206 1180 [ 2: (* Case where the evaluation of e1 as an lvalue fails *) 1207 normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 /1181 normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/ 1208 1182 | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1209 1183 #Hsim %1 * * #block #offset #trace normalize #Hstep … … 1228 1202 ] 1229 1203 ] 1230 | 16: destruct %1 //elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq1204 | 16: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 1231 1205 [ 1: (* Proving preservation of the semantics for expressions. *) 1232 1206 cases Hlvalue_sim 1233 1207 [ 2: (* Case where the evaluation of e1 as an expression fails *) 1234 * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2 /1208 * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2 by ex_intro/ 1235 1209 | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1236 1210 #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep … … 1254 1228 | 2: * #block * #offset * #region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat #Hty_eq #Hval_eq 1255 1229 whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta 1256 >Hptr_compat normalize nodelta//1230 >Hptr_compat // 1257 1231 ] 1258 1232 ] 1259 | 2: (* Proving preservation of the semantics of lvalues. *)1260 normalize @SimFail /2/1261 ]1262 | 17: destruct %1 //elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq1233 | 2: (* Proving preservation of the semantics of lvalues. *) 1234 @SimFail /2 by ex_intro/ 1235 ] 1236 | 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 1263 1237 [ 1: whd in match (exec_expr ge en m (Expr ??)); 1264 1238 whd in match (exec_expr ge en m (Expr ??)); 1265 1239 cases Hexpr_sim 1266 [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2 /1240 [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2 by ex_intro/ 1267 1241 | 1: cases (exec_expr ge en m e1) 1268 [ 2: #error #Hexec normalize nodelta @SimFail /2 /1242 [ 2: #error #Hexec normalize nodelta @SimFail /2 by ex_intro/ 1269 1243 | 1: * #val #trace #Hexec 1270 1244 >(Hexec ? (refl ? (OK ? 〈val,trace〉))) … … 1272 1246 ] 1273 1247 ] 1274 | 2: normalize @SimFail /2/1275 ] 1248 | 2: @SimFail /2 by ex_intro/ 1249 ] 1276 1250 | 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq 1277 1251 inversion (Hinv_lhs ge en m) … … 1290 1264 (* Enumerate all the cases for the evaluation of the source expressions ... *) 1291 1265 cases (exec_expr ge en m lhs) in Hsmaller_lhs; 1292 [ 2: #error normalize//1266 [ 2: #error // 1293 1267 | 1: * #val_lhs #trace_lhs normalize nodelta cases (exec_expr ge en m lhs1) 1294 [ 2: #error normalize#H @(False_ind … H)1268 [ 2: #error #H @(False_ind … H) 1295 1269 | 1: * #val_lhs1 #trace_lhs1 #Hsmaller_lhs 1296 1270 elim (smaller_integer_val_spec … Hsmaller_lhs) 1297 1271 #lhs_int * #lhs1_int * * * * #Hval_lhs #Hval_lhs1 #Hlhs_cast #Hlhs_trace #Hlhs_size 1298 1272 cases (exec_expr ge en m rhs) in Hsmaller_rhs; 1299 [ 2: #error normalize//1273 [ 2: #error // 1300 1274 | 1: * #val_rhs #trace_rhs normalize nodelta cases (exec_expr ge en m rhs1) 1301 [ 2: #error normalize#H @(False_ind … H)1275 [ 2: #error #H @(False_ind … H) 1302 1276 | 1: * #val_rhs1 #trace_rhs1 #Hsmaller_rhs 1303 1277 elim (smaller_integer_val_spec … Hsmaller_rhs) … … 1324 1298 >sz_eq_identity >sz_eq_identity normalize nodelta 1325 1299 try @conj try @conj try // 1326 >integer_add_cast_le // 1300 >integer_add_cast_le // 1327 1301 | 2: #_ (* subtraction case *) 1328 1302 >Hval_lhs >Hval_rhs destruct … … 1344 1318 ] 1345 1319 ] 1346 | 19,20,21,22: destruct %1 //1320 | 19,20,21,22: destruct %1 try @refl 1347 1321 elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs 1348 1322 elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs … … 1352 1326 [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/ 1353 1327 | *: cases (exec_expr ge en m lhs) 1354 [ 2,4,6,8: #error #_ normalize nodelta@SimFail /2 by refl, ex_intro/1355 | *: * #lval #ltrace #Hsim_lhs normalize nodelta 1328 [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/ 1329 | *: * #lval #ltrace #Hsim_lhs normalize nodelta 1356 1330 cases Hexpr_sim_rhs 1357 1331 [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/ 1358 1332 | *: cases (exec_expr ge en m rhs) 1359 [ 2,4,6,8: #error #_ normalize nodelta@SimFail /2 by refl, ex_intro/1333 [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/ 1360 1334 | *: * #rval #rtrace #Hsim_rhs 1361 1335 whd in match (exec_expr ??? (Expr (Ebinop ???) ?)); … … 1369 1343 ] 1370 1344 ] 1371 | *: normalize@SimFail /2 by refl, ex_intro/1345 | *: @SimFail /2 by refl, ex_intro/ 1372 1346 ] 1373 1347 (* Jump to the cast cases *) … … 1400 1374 ] 1401 1375 ] 1402 | 2,4,6,8,10,12,14,16: destruct normalize @SimFail /2/1376 | 2,4,6,8,10,12,14,16: destruct @SimFail /2 by refl, ex_intro/ 1403 1377 ] 1404 1378 | 24: destruct inversion (Hcastee_inv ge en m) … … 1412 1386 (* Simplify the goal by culling impossible cases, using Hsmaller_val *) 1413 1387 cases (exec_expr ge en m castee) in Hsmaller_eval; 1414 [ 2: #error normalize//1388 [ 2: #error // 1415 1389 | 1: * #castee_val #castee_trace cases (exec_expr ge en m castee1) 1416 [ 2: #error normalize#Hcontr @(False_ind … Hcontr)1390 [ 2: #error #Hcontr @(False_ind … Hcontr) 1417 1391 | 1: * #castee1_val #castee1_trace #Hsmaller 1418 1392 elim (smaller_integer_val_spec … Hsmaller) … … 1443 1417 #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq 1444 1418 @(Inv_eq ???????) // 1445 [ 1,4: >Htype_castee2 normalize//1419 [ 1,4: >Htype_castee2 // 1446 1420 | 2,5: (* Prove simulation for exec_expr *) 1447 1421 whd in match (exec_expr ??? (Expr ??)); 1448 1422 cases (exec_expr ge en m castee) in Hsmaller_eval; 1449 1423 [ 2,4: (* erroneous evaluation of the original expression *) 1450 #error #Hsmaller_eval @SimFail @(ex_intro … error) 1451 normalize nodelta // 1424 #error #Hsmaller_eval @SimFail @(ex_intro … error) // 1452 1425 | 1,3: * #val #trace 1453 1426 cases (exec_expr ge en m castee2) … … 1467 1440 ] 1468 1441 ] 1469 | 3,6: normalize @SimFail /2/1442 | 3,6: @SimFail /2 by refl, ex_intro/ 1470 1443 ] 1471 1444 ] … … 1494 1467 ] 1495 1468 ] 1496 | 2,4: normalize @SimFail /2/1469 | 2,4: @SimFail /2 by refl, ex_intro/ 1497 1470 ] 1498 1471 ] … … 1502 1475 whd in match (exec_expr ??? (Expr ??)); 1503 1476 [ 1: cases Hsim_expr 1504 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 /1477 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/ 1505 1478 | 1: #Hexec_ok @SimOk * #val #trace 1506 1479 cases (exec_expr ge en m castee) in Hexec_ok; … … 1512 1485 ] 1513 1486 ] 1514 | 2: normalize @SimFail /2/1487 | 2: @SimFail /2 by refl, ex_intro/ 1515 1488 ] 1516 1489 | 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq … … 1524 1497 | 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false 1525 1498 >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg) 1526 [ 1,2: normalize//1499 [ 1,2: // 1527 1500 | 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??)); 1528 1501 elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq … … 1532 1505 [ 2: #error #_ normalize @I 1533 1506 | 1: * #cond_val #cond_trace #Hcond_sim 1534 >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) 1535 1507 >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) 1536 1508 normalize nodelta 1537 1509 >Htype_cond_eq … … 1634 1606 ] 1635 1607 ] 1636 | 2,4,6: normalize@SimFail /2 by ex_intro/1608 | 2,4,6: @SimFail /2 by ex_intro/ 1637 1609 ] 1638 1610 | 41,42: destruct … … 1668 1640 ] 1669 1641 ] 1670 ]1671 ]1672 | 2,4: normalize@SimFail /2 by ex_intro/1642 ] 1643 ] 1644 | 2,4: @SimFail /2 by ex_intro/ 1673 1645 ] 1674 1646 | 43: destruct … … 1766 1738 | 2: @SimFail /2 by ex_intro/ ] 1767 1739 (* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls 1768 * simplify_expr 2*)1740 * simplify_expr *) 1769 1741 | 47, 48, 49: (* trivial const_int, const_float and var cases *) 1770 1742 try @conj try @conj try @refl … … 2022 1994 | 3: // 2023 1995 ] 2024 ] qed. 2025 2026 2027 (* simplify_expr [e] [ty'] takes an expression e and a desired type ty', and 2028 returns a flag stating whether the desired type was achieved and a simplified 2029 version of e. *) 2030 let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝ 2031 match e with 2032 [ Expr ed ty ⇒ 2033 match ed with 2034 [ Econst_int sz i ⇒ 2035 match ty with 2036 [ Tint ty_sz sg ⇒ 2037 match ty' with 2038 [ Tint sz' sg' ⇒ 2039 (* IG: checking that the displayed type size [ty_sz] and [sz] are equal ... *) 2040 match sz_eq_dec sz ty_sz with 2041 [ inl Heq ⇒ 2042 match simplify_int sz sz' sg sg' i with 2043 [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉 2044 | None ⇒ 〈false, e〉 2045 ] 2046 | inr _ ⇒ 2047 (* The expression is ill-typed. *) 2048 〈false, e〉 2049 ] 2050 | _ ⇒ 〈false, e〉 ] 2051 | _ ⇒ 〈false, e〉 ] 2052 | Ederef e1 ⇒ 2053 let ty1 ≝ typeof e1 in 2054 〈type_eq ty ty',Expr (Ederef (\snd (simplify_expr e1 ty1))) ty〉 2055 | Eaddrof e1 ⇒ 2056 let ty1 ≝ typeof e1 in 2057 〈type_eq ty ty',Expr (Eaddrof (\snd (simplify_expr e1 ty1))) ty〉 2058 | Eunop op e1 ⇒ 2059 let ty1 ≝ typeof e1 in 2060 〈type_eq ty ty',Expr (Eunop op (\snd (simplify_expr e1 ty1))) ty〉 2061 | Ebinop op e1 e2 ⇒ 2062 if binop_simplifiable op then 2063 let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty' in 2064 let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in 2065 if desired_type1 ∧ desired_type2 then 2066 〈true, Expr (Ebinop op e1' e2') ty'〉 2067 else 2068 let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in 2069 let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in 2070 〈false, Expr (Ebinop op e1' e2') ty〉 2071 else 2072 let 〈desired_type1, e1'〉 ≝ simplify_expr e1 (typeof e1) in 2073 let 〈desired_type2, e2'〉 ≝ simplify_expr e2 (typeof e2) in 2074 〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉 2075 | Ecast ty e1 ⇒ 2076 match inttype_compare ty' ty with 2077 [ itc_le ⇒ 2078 let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in 2079 if desired_type then 〈true, e1'〉 else 2080 let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in 2081 if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉 2082 | itc_no ⇒ 2083 let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in 2084 if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉 2085 ] 2086 | Econdition e1 e2 e3 ⇒ 2087 let 〈irrelevant, e1'〉 ≝ simplify_expr e1 (typeof e1) in (* TODO try to reduce size *) 2088 let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in 2089 let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty' in 2090 if desired_type2 ∧ desired_type3 then 2091 〈true, Expr (Econdition e1' e2' e3') ty'〉 2092 else 2093 let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in 2094 let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty in 2095 〈false, Expr (Econdition e1' e2' e3') ty〉 2096 (* Could probably do better with these, too. *) 2097 | Eandbool e1 e2 ⇒ 2098 let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in 2099 let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in 2100 〈type_eq ty ty', Expr (Eandbool e1' e2') ty〉 2101 | Eorbool e1 e2 ⇒ 2102 let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in 2103 let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in 2104 〈type_eq ty ty', Expr (Eorbool e1' e2') ty〉 2105 (* Could also improve Esizeof *) 2106 | Efield e1 f ⇒ 2107 let ty1 ≝ typeof e1 in 2108 〈type_eq ty ty',Expr (Efield (\snd (simplify_expr e1 ty1)) f) ty〉 2109 | Ecost l e1 ⇒ 2110 let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in 2111 〈desired_type, Expr (Ecost l e1') (typeof e1')〉 2112 | _ ⇒ 〈type_eq ty ty',e〉 2113 ] 2114 ]. 2115 2116 definition simplify_e ≝ λe. \snd (simplify_expr e (typeof e)). 1996 ] qed. 1997 1998 (* Propagate cast simplification through statements and programs. *) 1999 2000 definition simplify_e ≝ λe. pi1 … (simplify_inside e). 2117 2001 2118 2002 let rec simplify_statement (s:statement) : statement ≝ … … 2152 2036 λp. transform_program … p simplify_fundef. 2153 2037 2154 2155 (* We have to prove that simplify_expr doesn't alter the semantics. Since expressions are pure, 2156 * we state that expressions before and after conversion should evaluate to the same value, or 2157 * fail in a similar way when placed into a given context. *) 2158 2159 2160 let rec expr_ind2 2161 (P : expr → Prop) (Q : expr_descr → Prop) 2162 (IE : ∀ed. ∀t. Q ed → P (Expr ed t)) 2163 (Iconst_int : ∀sz, i. Q (Econst_int sz i)) 2164 (Iconst_float : ∀f. Q (Econst_float f)) 2165 (Ivar : ∀id. Q (Evar id)) 2166 (Ideref : ∀e. P e → Q (Ederef e)) 2167 (Iaddrof : ∀e. P e → Q (Eaddrof e)) 2168 (Iunop : ∀op,arg. P arg → Q (Eunop op arg)) 2169 (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2)) 2170 (Icast : ∀t. ∀e . P e → Q (Ecast t e)) 2171 (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3)) 2172 (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2)) 2173 (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2)) 2174 (Isizeof : ∀t. Q (Esizeof t)) 2175 (Ifield : ∀e,f. P e → Q (Efield e f)) 2176 (Icost : ∀c,e. P e → Q (Ecost c e)) 2177 (e : expr) on e : P e ≝ 2178 match e with 2179 [ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed) ] 2180 2181 and expr_desc_ind2 2182 (P : expr → Prop) (Q : expr_descr → Prop) 2183 (IE : ∀ed. ∀t. Q ed → P (Expr ed t)) 2184 (Iconst_int : ∀sz, i. Q (Econst_int sz i)) 2185 (Iconst_float : ∀f. Q (Econst_float f)) 2186 (Ivar : ∀id. Q (Evar id)) 2187 (Ideref : ∀e. P e → Q (Ederef e)) 2188 (Iaddrof : ∀e. P e → Q (Eaddrof e)) 2189 (Iunop : ∀op,arg. P arg → Q (Eunop op arg)) 2190 2191 (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2)) 2192 (Icast : ∀t. ∀e . P e → Q (Ecast t e)) 2193 (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3)) 2194 (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2)) 2195 (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2)) 2196 (Isizeof : ∀t. Q (Esizeof t)) 2197 (Ifield : ∀e,f. P e → Q (Efield e f)) 2198 (Icost : ∀c,e. P e → Q (Ecost c e)) 2199 (ed : expr_descr) on ed : Q ed ≝ 2200 match ed with 2201 [ Econst_int sz i ⇒ Iconst_int sz i 2202 | Econst_float f ⇒ Iconst_float f 2203 | Evar id ⇒ Ivar id 2204 | Ederef e ⇒ Ideref e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 2205 | Eaddrof e ⇒ Iaddrof e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 2206 | Eunop op e ⇒ Iunop op e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 2207 | Ebinop op e1 e2 ⇒ Ibinop op e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) 2208 | Ecast t e ⇒ Icast t e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 2209 | Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e3) 2210 | Eandbool e1 e2 ⇒ Iandbool e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) 2211 | Eorbool e1 e2 ⇒ Iorbool e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) 2212 | Esizeof t ⇒ Isizeof t 2213 | Efield e field ⇒ Ifield e field (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) 2214 | Ecost c e ⇒ Icost c e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof 2038 (* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *) 2039 inductive cont_cast : cont → cont → Prop ≝ 2040 | cc_stop : cont_cast Kstop Kstop 2041 | cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k') 2042 | cc_while : ∀e,s,k,k'. 2043 cont_cast k k' → 2044 cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') 2045 | cc_dowhile : ∀e,s,k,k'. 2046 cont_cast k k' → 2047 cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') 2048 | cc_for1 : ∀e,s1,s2,k,k'. 2049 cont_cast k k' → 2050 cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k') 2051 | cc_for2 : ∀e,s1,s2,k,k'. 2052 cont_cast k k' → 2053 cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k') 2054 | cc_for3 : ∀e,s1,s2,k,k'. 2055 cont_cast k k' → 2056 cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k') 2057 | cc_switch : ∀k,k'. 2058 cont_cast k k' → cont_cast (Kswitch k) (Kswitch k') 2059 | cc_call : ∀r,f,en,k,k'. 2060 cont_cast k k' → 2061 cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k'). 2062 (* wtf 2063 | cc_seqls : ∀ls,k,k'. cont_cast k k' → 2064 cont_cast (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (simplify_ls ls)) k'). 2065 *) 2066 2067 lemma call_cont_cast : ∀k,k'. 2068 cont_cast k k' → 2069 cont_cast (call_cont k) (call_cont k'). 2070 #k0 #k0' #K elim K /2/ 2071 qed. 2072 2073 inductive state_cast : state → state → Prop ≝ 2074 | swc_state : ∀f,s,k,k',e,m. 2075 cont_cast k k' → 2076 state_cast (State f s k e m) (State (simplify_function f) (simplify_statement s ) k' e m) 2077 | swc_callstate : ∀fd,args,k,k',m. 2078 cont_cast k k' → state_cast (Callstate fd args k m) (Callstate (simplify_fundef fd) args k' m) 2079 | swc_returnstate : ∀res,k,k',m. 2080 cont_cast k k' → state_cast (Returnstate res k m) (Returnstate res k' m) 2081 | swc_finalstate : ∀r. 2082 state_cast (Finalstate r) (Finalstate r) 2083 . 2084 2085 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { 2086 rg_find_symbol: ∀s. 2087 find_symbol ? ge s = find_symbol ? ge' s; 2088 rg_find_funct: ∀v,f. 2089 find_funct ? ge v = Some ? f → 2090 find_funct ? ge' v = Some ? (t f); 2091 rg_find_funct_ptr: ∀b,f. 2092 find_funct_ptr ? ge b = Some ? f → 2093 find_funct_ptr ? ge' b = Some ? (t f) 2094 }. 2095 2096 (* The return type of any function is invariant under cast simplification *) 2097 lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f. 2098 // qed. 2099 2100 include "CexecSound.ma". 2101 2102 definition expr_lvalue_ind_combined ≝ 2103 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. 2104 conj ?? 2105 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx) 2106 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). 2107 2108 lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulate A r0 r2. 2109 #A #r0 #r1 #r2 * 2110 [ 2: * #error #H >H #_ @SimFail /2 by ex_intro/ 2111 | 1: cases r0 2112 [ 2: #error #_ #_ @SimFail /2 by ex_intro/ 2113 | 1: #elt #Hsim lapply (Hsim elt (refl ? (OK ? elt))) #H >H // ] 2114 ] qed. 2115 2116 lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → 2117 (∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧ 2118 (∀ed, ty. simulate ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)). 2119 #ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined 2120 [ 1: #sz #ty #i @SimOk #a normalize // 2121 | 2: #ty #f @SimOk #a normalize // 2122 | 3: * 2123 [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 2124 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] 2125 #ty #Hsim_lvalue try // 2126 whd in match (Plvalue ???); 2127 whd in match (exec_expr ????); 2128 whd in match (exec_expr ????); 2129 cases Hsim_lvalue 2130 [ 2,4,6: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ 2131 | *: cases (exec_lvalue' ge en m ? ty) 2132 [ 2,4,6: #error #_ @SimFail /2 by ex_intro/ 2133 | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2134 @SimOk // ] 2135 ] 2136 | 4: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); 2137 cases (lookup SymbolTag block en v) normalize nodelta 2138 [ 2: #block @SimOk // 2139 | 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk // 2140 ] 2141 | 5: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); 2142 cases Hsim_expr 2143 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2144 | 1: cases (exec_expr ge en m e) 2145 [ 2: #error #_ @SimFail /2 by ex_intro/ 2146 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2147 @SimOk // ] 2148 ] 2149 | 6: #ty #ed #ty' #Hsim_lvalue 2150 whd in match (exec_expr ????); whd in match (exec_expr ????); 2151 whd in match (exec_lvalue ????); whd in match (exec_lvalue ????); 2152 cases Hsim_lvalue 2153 [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ 2154 | 1: cases (exec_lvalue' ge en m ed ty') 2155 [ 2: #error #_ @SimFail /2 by ex_intro/ 2156 | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2157 @SimOk // ] 2158 ] 2159 | 7: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 2160 cases Hsim 2161 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2162 | 1: cases (exec_expr ge en m e) 2163 [ 2: #error #_ @SimFail /2 by ex_intro/ 2164 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2165 @SimOk // ] 2166 ] 2167 | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 2168 cases Hsim1 2169 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2170 | 1: cases (exec_expr ge en m e1) 2171 [ 2: #error #_ @SimFail /2 by ex_intro/ 2172 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2173 cases Hsim2 2174 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2175 | 1: cases (exec_expr ge en m e2) 2176 [ 2: #error #_ @SimFail /2 by ex_intro/ 2177 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2178 @SimOk // ] 2179 ] 2180 ] 2181 ] 2182 | 9: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 2183 cases Hsim 2184 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2185 | 1: cases (exec_expr ge en m e) 2186 [ 2: #error #_ @SimFail /2 by ex_intro/ 2187 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2188 @SimOk // ] 2189 ] (* mergeable with 7 modulo intros *) 2190 | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 2191 cases Hsim1 2192 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2193 | 1: cases (exec_expr ge en m e1) 2194 [ 2: #error #_ @SimFail /2 by ex_intro/ 2195 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta 2196 cases (exec_bool_of_val (\fst a) (typeof e1)) 2197 [ 2: #error @SimFail /2 by ex_intro/ 2198 | 1: * 2199 [ 1: (* true branch *) cases Hsim2 2200 | 2: (* false branch *) cases Hsim3 ] 2201 [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2202 | 1: cases (exec_expr ge en m e2) | 3: cases (exec_expr ge en m e3) ] 2203 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 2204 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] 2205 ] 2206 ] 2207 ] 2208 | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 2209 cases Hsim1 2210 [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2211 | 1,3: cases (exec_expr ge en m e1) 2212 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 2213 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta 2214 cases (exec_bool_of_val ??) 2215 [ 2,4: #erro @SimFail /2 by ex_intro/ 2216 | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); 2217 [ 2,3: @SimOk // 2218 | 1,4: cases Hsim2 2219 [ 2,4: * #error #Hfail >Hfail normalize nodelta @SimFail /2 by ex_intro/ 2220 | 1,3: cases (exec_expr ge en m e2) 2221 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 2222 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2223 @SimOk // ] 2224 ] 2225 ] 2226 ] 2227 ] 2228 ] 2229 | 13: #ty #sizeof_ty @SimOk normalize // 2230 | 14: #ty #e #ty' #field #Hsim_lvalue 2231 whd in match (exec_lvalue' ? en m (Efield ??) ty); 2232 whd in match (exec_lvalue' ge' en m (Efield ??) ty); 2233 normalize in match (typeof (Expr ??)); 2234 cases ty' in Hsim_lvalue; normalize nodelta 2235 [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain 2236 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ] 2237 #Hsim_lvalue 2238 try (@SimFail /2 by ex_intro/) 2239 normalize in match (exec_lvalue ge en m ?); 2240 normalize in match (exec_lvalue ge' en m ?); 2241 cases Hsim_lvalue 2242 [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2243 | 1,3: cases (exec_lvalue' ge en m e ?) 2244 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 2245 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2246 @SimOk /2 by ex_intro/ ] 2247 ] 2248 | 15: #ty #lab #e #Hsim 2249 whd in match (exec_expr ??? (Expr ??)); 2250 whd in match (exec_expr ??? (Expr ??)); 2251 cases Hsim 2252 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 2253 | 1: cases (exec_expr ge en m e) 2254 [ 2: #error #_ @SimFail /2 by ex_intro/ 2255 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2256 @SimOk // ] 2257 ] (* cf case 7, again *) 2258 | 16: * 2259 [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 2260 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] 2261 #ty normalize in match (is_not_lvalue ?); 2262 [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_ 2263 @SimFail /2 by ex_intro/ 2264 ] qed. 2265 2266 lemma related_globals_expr_simulation : ∀ge,ge',en,m. 2267 related_globals ? simplify_fundef ge ge' → 2268 ∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧ 2269 typeof e = typeof (simplify_e e). 2270 #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); 2271 cases e #ed #ty cases ed 2272 [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 2273 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] 2274 elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) 2275 * * try // 2276 cases (exec_expr ge en m (Expr ??)) 2277 try (#error #_ #_ #_ @SimFail /2 by ex_intro/) 2278 * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq 2279 try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?)) 2280 qed. 2281 2282 lemma related_globals_lvalue_simulation : ∀ge,ge',en,m. 2283 related_globals ? simplify_fundef ge ge' → 2284 ∀e. simulate ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧ 2285 typeof e = typeof (simplify_e e). 2286 #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); 2287 cases e #ed #ty cases ed 2288 [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 2289 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] 2290 elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) 2291 * * try // 2292 cases (exec_lvalue ge en m (Expr ??)) 2293 try (#error #_ #_ #_ @SimFail /2 by ex_intro/) 2294 * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq 2295 (* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *) 2296 cases e' in Hsim_lvalue ⊢ %; #ed' #ty' whd in match (exec_lvalue ????); whd in match (exec_lvalue ????); 2297 lapply (proj2 ?? (sim_related_globals ge ge' en m Hrelated) ed' ty') #Hsim_lvalue2 #Hsim_lvalue1 2298 try @(simulation_transitive ???? Hsim_lvalue1 Hsim_lvalue2) 2299 qed. 2300 2301 lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. 2302 related_globals ? simplify_fundef ge ge' → 2303 ∀args. simulate ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)). 2304 #ge #ge' #en #m #Hrelated #args 2305 elim args 2306 [ 1: /3/ 2307 | 2: #hd #tl #Hind normalize 2308 elim (related_globals_expr_simulation ge ge' en m Hrelated hd) 2309 * 2310 [ 2: * #error #Hfail >Hfail #_ @SimFail /2 by refl, ex_intro/ 2311 | 1: cases (exec_expr ge en m hd) 2312 [ 2: #error #_ #_ @SimFail /2 by refl, ex_intro/ 2313 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq 2314 cases Hind normalize 2315 [ 2: * #error #Hfail >Hfail @SimFail /2 by refl, ex_intro/ 2316 | 1: cases (exec_exprlist ??? tl) 2317 [ 2: #error #_ @SimFail /2 by refl, ex_intro/ 2318 | 1: * #values #trace #Hsim lapply (Hsim 〈values, trace〉 (refl ? (OK ? 〈values, trace〉))) 2319 #Heq >Heq @SimOk // ] 2320 ] 2321 ] 2322 ] 2323 ] qed. 2324 2325 lemma simplify_type_of_fundef_eq : ∀clfd. (type_of_fundef (simplify_fundef clfd)) = (type_of_fundef clfd). 2326 * // qed. 2327 2328 lemma simplify_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. typeof (simplify_e func) = typeof func. 2329 #ge #en #m #func whd in match (simplify_e func); elim (simplify_inside func) 2330 #func' #H lapply (H ge en m) * * #_ #_ // 2331 qed. 2332 2333 lemma simplify_fun_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. fun_typeof (simplify_e func) = fun_typeof func. 2334 #ge #en #m #func whd in match (simplify_e func); whd in match (fun_typeof ?) in ⊢ (??%%); 2335 >simplify_typeof_eq whd in match (simplify_e func); // qed. 2336 2337 lemma simplify_is_not_skip: ∀s.s ≠ Sskip → ∃pf. is_Sskip (simplify_statement s) = inr … pf. 2338 * 2339 [ 1: * #Habsurd elim (Habsurd (refl ? Sskip)) 2340 | *: #a try #b try #c try #d try #e 2341 whd in match (simplify_statement ?); 2342 whd in match (is_Sskip ?); 2343 try /2 by refl, ex_intro/ 2344 ] qed. 2345 2346 lemma call_cont_simplify : ∀k,k'. 2347 cont_cast k k' → 2348 cont_cast (call_cont k) (call_cont k'). 2349 #k0 #k0' #K elim K /2/ 2350 qed. 2351 2352 lemma simplify_ls_commute : ∀l. (simplify_statement (seq_of_labeled_statement l)) = (seq_of_labeled_statement (simplify_ls l)). 2353 #l @(labeled_statements_ind … l) 2354 [ 1: #default_statement // 2355 | 2: #sz #i #s #tl #Hind 2356 whd in match (seq_of_labeled_statement ?) in ⊢ (??%?); 2357 whd in match (simplify_ls ?) in ⊢ (???%); 2358 whd in match (seq_of_labeled_statement ?) in ⊢ (???%); 2359 whd in match (simplify_statement ?) in ⊢ (??%?); 2360 >Hind // 2361 ] qed. 2362 2363 lemma select_switch_commute : ∀sz,i,l. 2364 select_switch sz i (simplify_ls l) = simplify_ls (select_switch sz i l). 2365 #sz #i #l @(labeled_statements_ind … l) 2366 [ 1: #default_statement // 2367 | 2: #sz' #i' #s #tl #Hind 2368 whd in match (simplify_ls ?) in ⊢ (??%?); 2369 whd in match (select_switch ???) in ⊢ (??%%); 2370 cases (sz_eq_dec sz sz') 2371 [ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true 2372 cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta 2373 whd in match (simplify_ls ?) in ⊢ (???%); 2374 [ 1: // | 2: @Hind ] 2375 | 2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq) 2376 @Hind 2377 ] 2378 ] qed. 2379 2380 lemma invoke_cthulhu : 2381 ∀lab. ∀s:statement.∀k,k'. cont_cast k k' → 2382 ∀Hind:(∀k:cont.∀k':cont. 2383 cont_cast k k' → 2384 match find_label lab s k with 2385 [ None ⇒ find_label lab (simplify_statement s) k'=None (statement×cont) 2386 | Some (r:(statement×cont))⇒ 2387 let 〈s',ks〉 ≝r in 2388 ∃ks':cont. find_label lab (simplify_statement s) k' = Some (statement×cont) 〈simplify_statement s',ks'〉 2389 ∧ cont_cast ks ks']). 2390 (find_label lab s k = None ? ∧ find_label lab (simplify_statement s) k' = None ?) ∨ 2391 (∃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'). 2392 #lab #s #k #k' #Hcont_cast #Hind 2393 lapply (Hind k k' Hcont_cast) 2394 cases (find_label lab s k) 2395 [ 1: normalize nodelta #Heq >Heq /3/ 2396 | 2: * #st #kst normalize nodelta * #kst' * #Heq #Hcont_cast' >Heq %2 2397 %{st} %{kst} %{kst'} @conj try @conj // 2398 ] qed. 2399 2400 2401 lemma cast_find_label : ∀lab,s,k,k'. 2402 cont_cast k k' → 2403 match find_label lab s k with 2404 [ Some r ⇒ 2405 let 〈s',ks〉 ≝ r in 2406 ∃ks'. find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement s', ks'〉 2407 ∧ cont_cast ks ks' 2408 | None ⇒ 2409 find_label lab (simplify_statement s) k' = None ? 2410 ]. 2411 #lab #s @(statement_ind2 ? (λls. 2412 ∀k:cont 2413 .∀k':cont 2414 .cont_cast k k' 2415 →match find_label_ls lab ls k with 2416 [None⇒ 2417 find_label_ls lab (simplify_ls ls) k' = None ? 2418 |Some r ⇒ 2419 let 〈s',ks〉 ≝r in 2420 ∃ks':cont 2421 .find_label_ls lab (simplify_ls ls) k' 2422 =Some (statement×cont) 〈simplify_statement s',ks'〉 2423 ∧cont_cast ks ks'] 2424 ) … s) 2425 [ 1: #k #k' #Hcont_cast 2426 whd in match (find_label ? Sskip ?); normalize nodelta @refl 2427 | 2: #e1 #e2 #k #k' #Hcont_cast 2428 whd in match (find_label ? (Sassign e1 e2) ?); normalize nodelta @refl 2429 | 3: #e0 #e #args #k #k' #Hcont_cast 2430 whd in match (find_label ? (Scall e0 e args) ?); normalize nodelta @refl 2431 | 4: #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast 2432 whd in match (find_label ? (Ssequence s1 s2) ?); 2433 whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?); 2434 elim (invoke_cthulhu lab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1) 2435 [ 3: try ( @cc_seq // ) 2436 | 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2437 normalize nodelta %{kst'} /2/ 2438 | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta 2439 elim (invoke_cthulhu lab s2 k k' Hcont_cast Hind_s2) 2440 [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' 2441 normalize nodelta %{kst'} /2/ 2442 | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // 2443 ] ] 2444 | 5: #e #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast 2445 whd in match (find_label ???); 2446 whd in match (find_label ? (simplify_statement ?) ?); 2447 elim (invoke_cthulhu lab s1 k k' Hcont_cast Hind_s1) 2448 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2449 normalize nodelta %{kst'} /2/ 2450 | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta 2451 elim (invoke_cthulhu lab s2 k k' Hcont_cast Hind_s2) 2452 [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' 2453 normalize nodelta %{kst'} /2/ 2454 | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // 2455 ] ] 2456 | 6: #e #s #Hind_s #k #k' #Hcont_cast 2457 whd in match (find_label ???); 2458 whd in match (find_label ? (simplify_statement ?) ?); 2459 elim (invoke_cthulhu lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s) 2460 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2461 normalize nodelta %{kst'} /2/ 2462 | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // 2463 | 3: @cc_while // ] 2464 | 7: #e #s #Hind_s #k #k' #Hcont_cast 2465 whd in match (find_label ???); 2466 whd in match (find_label ? (simplify_statement ?) ?); 2467 elim (invoke_cthulhu lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s) 2468 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2469 normalize nodelta %{kst'} /2/ 2470 | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // 2471 | 3: @cc_dowhile // ] 2472 | 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast 2473 whd in match (find_label ???); 2474 whd in match (find_label ? (simplify_statement ?) ?); 2475 elim (invoke_cthulhu lab s1 2476 (Kseq (Sfor Sskip cond s2 s3) k) 2477 (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k') 2478 ? Hind_s1) 2479 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2480 normalize nodelta %{kst'} /2/ 2481 | 3: @cc_for1 // 2482 | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta 2483 elim (invoke_cthulhu lab s3 2484 (Kfor2 cond s2 s3 k) 2485 (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') 2486 ? Hind_s3) 2487 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2488 normalize nodelta %{kst'} /2/ 2489 | 3: @cc_for2 // 2490 | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta 2491 elim (invoke_cthulhu lab s2 2492 (Kfor3 cond s2 s3 k) 2493 (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') 2494 ? Hind_s2) 2495 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2496 normalize nodelta %{kst'} /2/ 2497 | 3: @cc_for3 // 2498 | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // 2499 ] ] ] 2500 | 9,10: #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta // 2501 | 11: #e #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta // 2502 | 12: #e #ls #Hind #k #k' #Hcont_cast 2503 whd in match (find_label ???); 2504 whd in match (find_label ? (simplify_statement ?) ?); 2505 (* We can't invoke Cthulhu on a list of labeled statements. We must proceed more manually. *) 2506 lapply (Hind (Kswitch k) (Kswitch k') ?) 2507 [ 1: @cc_switch // 2508 | 2: cases (find_label_ls lab ls (Kswitch k)) normalize nodelta 2509 [ 1: // 2510 | 2: * #st #kst normalize nodelta // ] ] 2511 | 13: #lab' #s0 #Hind #k #k' #Hcont_cast 2512 whd in match (find_label ???); 2513 whd in match (find_label ? (simplify_statement ?) ?); 2514 cases (ident_eq lab lab') normalize nodelta 2515 [ 1: #_ %{k'} /2/ 2516 | 2: #_ elim (invoke_cthulhu lab s0 k k' Hcont_cast Hind) 2517 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2518 normalize nodelta %{kst'} /2/ 2519 | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] 2520 ] 2521 | 14: #l #k #k' #Hcont_cast // 2522 | 15: #l #s0 #Hind #k #k' #Hcont_cast 2523 whd in match (find_label ???); 2524 whd in match (find_label ? (simplify_statement ?) ?); 2525 elim (invoke_cthulhu lab s0 k k' Hcont_cast Hind) 2526 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2527 normalize nodelta %{kst'} /2/ 2528 | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] 2529 | 16: #s0 #Hind #k #k' #Hcont_cast 2530 whd in match (find_label ???); 2531 whd in match (find_label ? (simplify_statement ?) ?); 2532 elim (invoke_cthulhu lab s0 k k' Hcont_cast Hind) 2533 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2534 normalize nodelta %{kst'} /2/ 2535 | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] 2536 | 17: #sz #i #s0 #t #Hind_s0 #Hind_ls #k #k' #Hcont_cast 2537 whd in match (simplify_ls ?); 2538 whd in match (find_label_ls ???); 2539 lapply Hind_ls 2540 @(labeled_statements_ind … t) 2541 [ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?); 2542 elim (invoke_cthulhu lab s0 2543 (Kseq default_case k) 2544 (Kseq (simplify_statement default_case) k') ? Hind_s0) 2545 [ 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast' 2546 >Hrewrite >Hrewrite1 2547 normalize nodelta whd in match (find_label_ls ???); 2548 >Hrewrite >Hrewrite1 normalize nodelta 2549 %{kst'} /2/ 2550 | 3: @cc_seq // 2551 | 1: * #Hrewrite #Hrewrite1 >Hrewrite normalize nodelta 2552 lapply (Hind_ls k k' Hcont_cast) 2553 cases (find_label_ls lab (LSdefault default_case) k) 2554 [ 1: normalize nodelta #Heq1 2555 whd in match (simplify_ls ?); 2556 whd in match (find_label_ls lab ??); 2557 whd in match (seq_of_labeled_statement ?); 2558 whd in match (find_label_ls lab ??); 2559 >Hrewrite1 normalize nodelta @Heq1 2560 | 2: * #st #kst normalize nodelta #H 2561 whd in match (find_label_ls lab ??); 2562 whd in match (simplify_ls ?); 2563 whd in match (seq_of_labeled_statement ?); 2564 >Hrewrite1 normalize nodelta @H 2565 ] 2566 ] 2567 | 2: #sz' #i' #s' #tl' #Hind #A 2568 2569 whd in match (seq_of_labeled_statement ?); 2570 elim (invoke_cthulhu lab s0 2571 (Kseq (Ssequence s' (seq_of_labeled_statement tl')) k) 2572 (Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k') 2573 ? 2574 Hind_s0) 2575 [ 3: @cc_seq // 2576 | 1: * #Heq #Heq2 >Heq >Heq2 normalize nodelta 2577 lapply (A k k' Hcont_cast) 2578 cases (find_label_ls lab (LScase sz' i' s' tl') k) normalize nodelta 2579 [ 1: #H whd in match (find_label_ls ???); 2580 <simplify_ls_commute 2581 whd in match (seq_of_labeled_statement ?); 2582 >Heq2 normalize nodelta 2583 assumption 2584 | 2: * #st #kst normalize nodelta #H 2585 whd in match (find_label_ls ???); 2586 <simplify_ls_commute >Heq2 normalize nodelta @H 2587 ] 2588 | 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast' 2589 >Hrewrite normalize nodelta 2590 %{kst'} @conj try // 2591 whd in match (find_label_ls ???); 2592 <simplify_ls_commute >Hrewrite1 // 2593 ] 2594 ] 2595 ] qed. 2596 2597 lemma cast_find_label_fn : ∀lab,f,k,k',s,ks. 2598 cont_cast k k' → 2599 find_label lab (fn_body f) k = Some ? 〈s,ks〉 → 2600 ∃ks'. find_label lab (fn_body (simplify_function f)) k' = Some ? 〈simplify_statement s,ks'〉 2601 ∧ cont_cast ks ks'. 2602 #lab * #rettype #args #vars #body #k #k' #s #ks #Hcont_cast #Hfind_lab 2603 whd in match (simplify_function ?); 2604 lapply (cast_find_label lab body ?? Hcont_cast) 2605 >Hfind_lab normalize nodelta // 2606 qed. 2607 2608 theorem cast_correction : ∀ge, ge'. 2609 related_globals ? simplify_fundef ge ge' → 2610 ∀s1, s1', tr, s2. 2611 state_cast s1 s1' → 2612 exec_step ge s1 = Value … 〈tr,s2〉 → 2613 ∃s2'. exec_step ge' s1' = Value … 〈tr,s2'〉 ∧ 2614 state_cast s2 s2'. 2615 #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hs1_sim_s1' #Houtcome 2616 inversion Hs1_sim_s1' 2617 [ 1: (* regular state *) 2618 #f #stm #k #k' #en #m #Hcont_cast 2619 lapply (related_globals_expr_simulation ge ge' en m Hrelated) #Hsim_related 2620 lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related 2621 cases stm 2622 (* Perform the intros for the statements*) 2623 [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body 2624 | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body 2625 | 14: #lab | 15: #cost #body ] 2626 [ 1: (* Skip *) 2627 #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 2628 whd in match (exec_step ??); whd in match (exec_step ??); 2629 inversion Hcont_cast 2630 [ 1: (* Kstop *) 2631 #Hk #Hk' #_ >fn_return_simplify cases (fn_return f) normalize nodelta 2632 [ 1: >Heq_s1 in Hs1_sim_s1'; >Heq_s1' #Hsim inversion Hsim 2633 [ 1: #f0 #s #k0 #k0' #e #m0 #Hcont_cast0 #Hstate_eq #Hstate_eq' #_ 2634 #Eq whd in match (ret ??) in Eq; destruct (Eq) 2635 %{(Returnstate Vundef Kstop (free_list m (blocks_of_env en)))} @conj 2636 [ 1: // | 2: %3 %1 ] 2637 | 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd) 2638 | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd) 2639 | 4: #r #Habsurd destruct (Habsurd) ] 2640 | 3: #irrelevant #Habsurd destruct 2641 | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct 2642 | *: #irrelevant1 #irrelevant2 #Habsurd destruct ] 2643 | 2: (* Kseq stm' k' *) 2644 #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq 2645 whd in match (ret ??) in Eq; destruct (Eq) 2646 %{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj 2647 [ 1: // | 2: %1 // ] 2648 | 3: (* Kwhile *) 2649 #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq 2650 whd in match (ret ??) in Eq; destruct (Eq) 2651 %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj 2652 [ 1: // | 2: %1 // ] 2653 | 4: (* Kdowhile *) 2654 #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq 2655 elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond 2656 [ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct 2657 | 1: cases (exec_expr ge en m cond) in Eq; 2658 [ 2: #error whd in match (m_bind ?????) in ⊢ (% → ?); #Habsurd destruct 2659 | 1: * #val #trace whd in match (m_bind ?????) in ⊢ (% → ?); <Htype_cond_eq 2660 #Eq #Hsim_cond lapply (Hsim_cond 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) 2661 #Hrewrite_cond >Hrewrite_cond whd in match (m_bind ?????); 2662 (* case analysis on the outcome of the conditional *) 2663 cases (exec_bool_of_val val (typeof cond)) in Eq ⊢ %; 2664 [ 2: (* evaluation of the conditional fails *) 2665 #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2666 | 1: * whd in match (bindIO ??????); 2667 whd in match (bindIO ??????); 2668 #Eq destruct (Eq) 2669 [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)} 2670 @conj [ 1: // | 2: %1 // ] 2671 | 2: %{(State (simplify_function f) Sskip k0' en m)} 2672 @conj [ 1: // | 2: %1 // ] 2673 ] 2674 ] 2675 ] 2676 ] 2677 | 5,6,7: 2678 #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq 2679 whd in match (ret ??) in Eq ⊢ %; destruct (Eq) 2680 [ 1: %{(State (simplify_function f) 2681 (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) 2682 k0' en m)} @conj 2683 [ 1: // | 2: %1 // ] 2684 | 2: %{(State (simplify_function f) 2685 (simplify_statement step) 2686 (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') 2687 en m)} @conj 2688 [ 1: // | 2: %1 @cc_for3 // ] 2689 | 3: %{(State (simplify_function f) 2690 (Sfor Sskip (simplify_e cond) (simplify_statement step) 2691 (simplify_statement body)) 2692 k0' en m)} @conj 2693 [ 1: // | 2: %1 // ] 2694 ] 2695 | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq 2696 whd in match (ret ??) in Eq ⊢ %; destruct (Eq) 2697 %{(State (simplify_function f) Sskip k0' en m)} @conj 2698 [ 1: // | 2: %1 // ] 2699 | 9: (* Call *) 2700 #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ #Eq 2701 >fn_return_simplify cases (fn_return f) in Eq; normalize nodelta 2702 [ 1: #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq) 2703 %{(Returnstate Vundef (Kcall r (simplify_function f0) en0 k0') 2704 (free_list m (blocks_of_env en)))} @conj 2705 [ 1: // | 2: %3 @cc_call // ] 2706 | 3: #irrelevant #Habsurd destruct (Habsurd) 2707 | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct (Habsurd) 2708 | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ] 2709 ] 2710 | 2: (* Assign *) 2711 #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 2712 whd in match (simplify_statement ?); #Heq 2713 whd in match (exec_step ??) in Heq ⊢ %; 2714 (* Begin by making the simplify_e disappear using Hsim_related *) 2715 elim (Hsim_lvalue_related lhs) * 2716 [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd) 2717 | 1: cases (exec_lvalue ge en m lhs) in Heq; 2718 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2719 | 1: * * #block #offset #trace 2720 whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_lhs 2721 lapply (Hsim 〈block, offset, trace〉 (refl ? (OK ? 〈block, offset, trace〉))) 2722 #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????); 2723 (* After [lhs], treat [rhs] *) 2724 elim (Hsim_related rhs) * 2725 [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd) 2726 | 1: cases (exec_expr ge en m rhs) in Heq; 2727 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2728 | 1: * #val #trace 2729 whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_rhs 2730 lapply (Hsim 〈val, trace〉 (refl ? (OK ? 〈val, trace〉))) 2731 #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????); 2732 <Htype_eq_lhs <Htype_eq_rhs 2733 cases (opt_to_io ?????) in Heq; 2734 [ 1: #o #resumption whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2735 | 3: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd) 2736 | 2: #mem whd in match (bindIO ??????); #Heq destruct (Heq) 2737 %{(State (simplify_function f) Sskip k' en mem)} @conj 2738 [ 1: // | 2: %1 // ] 2739 ] 2740 ] 2741 ] 2742 ] 2743 ] 2744 | 3: (* Call *) 2745 #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 2746 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2747 whd in match (exec_step ??) in Heq ⊢ %; 2748 elim (Hsim_related func) in Heq; * 2749 [ 2: * #error #Hfail >Hfail #Htype_eq #Habsurd normalize in Habsurd; destruct (Habsurd) 2750 | 1: cases (exec_expr ??? func) 2751 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2752 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq 2753 whd in match (bindIO ??????) in ⊢ (% → %); 2754 elim (related_globals_exprlist_simulation ge ge' en m Hrelated args) 2755 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 2756 | 1: cases (exec_exprlist ge en m args) 2757 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2758 | 1: #l -Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq 2759 whd in match (bindIO ??????) in ⊢ (% → %); 2760 elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a)) 2761 cases (find_funct clight_fundef ge (\fst a)); 2762 [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2763 | 2: #clfd -Hsim #Hsim lapply (Hsim clfd (refl ? (Some ? clfd))) #Heq >Heq 2764 whd in match (bindIO ??????) in ⊢ (% → %); 2765 >simplify_type_of_fundef_eq >(simplify_fun_typeof_eq ge en m) 2766 cases (assert_type_eq (type_of_fundef clfd) (fun_typeof func)) 2767 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2768 | 1: #Htype_eq cases ret 2769 [ 1: whd in match (bindIO ??????) in ⊢ (% → %); 2770 #Eq destruct (Eq) 2771 %{(Callstate (simplify_fundef clfd) (\fst l) 2772 (Kcall (None (block×offset×type)) (simplify_function f) en k') m)} 2773 @conj 2774 [ 1: // | 2: %2 @cc_call // ] 2775 | 2: #fptr whd in match (bindIO ??????) in ⊢ (% → %); 2776 elim (Hsim_lvalue_related fptr) * 2777 [ 2: * #error #Hfail >Hfail #_ 2778 #Habsurd normalize in Habsurd; destruct (Habsurd) 2779 | 1: cases (exec_lvalue ge en m fptr) 2780 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2781 | 1: #a #Hsim #Htype_eq_fptr >(Hsim a (refl ? (OK ? a))) 2782 whd in match (bindIO ??????) in ⊢ (% → %); 2783 #Heq destruct (Heq) 2784 %{(Callstate (simplify_fundef clfd) (\fst l) 2785 (Kcall (Some (block×offset×type) 〈\fst a,typeof (simplify_e fptr)〉) 2786 (simplify_function f) en k') m)} 2787 @conj [ 1: // | 2: >(simplify_typeof_eq ge en m) %2 @cc_call // ] 2788 ] ] ] ] ] ] ] ] ] 2789 | 4: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2790 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2791 whd in match (exec_step ??) in Heq ⊢ %; 2792 destruct (Heq) 2793 %{(State (simplify_function f) (simplify_statement stm1) (Kseq (simplify_statement stm2) k') en m)} 2794 @conj 2795 [ 1: // | 2: %1 @cc_seq // ] 2796 | 5: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2797 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2798 whd in match (exec_step ??) in Heq ⊢ %; 2799 elim (Hsim_related cond) in Heq; * 2800 [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2801 | 1: cases (exec_expr ge en m cond) 2802 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2803 | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq 2804 #Htype_eq_cond 2805 whd in match (bindIO ??????) in ⊢ (% → %); 2806 >(simplify_typeof_eq ge en m) 2807 cases (exec_bool_of_val condval (typeof cond)) 2808 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2809 | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %; 2810 [ 1: destruct skip (condtrace) 2811 %{(State (simplify_function f) (simplify_statement iftrue) k' en m)} @conj 2812 [ 1: // | 2: <e0 %1 // ] 2813 | 2: destruct skip (condtrace) 2814 %{(State (simplify_function f) (simplify_statement iffalse) k' en m)} @conj 2815 [ 1: // | 2: <e0 %1 // ] 2816 ] ] ] ] 2817 | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2818 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2819 whd in match (exec_step ??) in Heq ⊢ %; 2820 elim (Hsim_related cond) in Heq; * 2821 [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2822 | 1: cases (exec_expr ge en m cond) 2823 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2824 | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq 2825 #Htype_eq_cond 2826 whd in match (bindIO ??????) in ⊢ (% → %); 2827 >(simplify_typeof_eq ge en m) 2828 cases (exec_bool_of_val condval (typeof cond)) 2829 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2830 | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %; 2831 [ 1: destruct skip (condtrace) 2832 %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)} 2833 @conj 2834 [ 1: // | 2: <e0 %1 @cc_while // ] 2835 | 2: destruct skip (condtrace) 2836 %{(State (simplify_function f) Sskip k' en m)} @conj 2837 [ 1: // | 2: <e0 %1 // ] 2838 ] ] ] ] 2839 | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2840 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2841 whd in match (exec_step ??) in Heq ⊢ %; 2842 destruct (Heq) 2843 %{(State (simplify_function f) (simplify_statement body) 2844 (Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj 2845 [ 1: // | 2: %1 @cc_dowhile // ] 2846 | 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2847 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2848 whd in match (exec_step ??) in Heq ⊢ %; 2849 cases (is_Sskip init) in Heq; 2850 [ 2: #Hinit_neq_Sskip elim (simplify_is_not_skip init Hinit_neq_Sskip) #pf #Hrewrite >Hrewrite 2851 normalize nodelta 2852 whd in match (ret ??) in ⊢ (% → %); 2853 #Eq destruct (Eq) 2854 %{(State (simplify_function f) (simplify_statement init) 2855 (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj 2856 [ 1: // | 2: %1 @cc_for1 // ] 2857 | 1: #Hinit_eq_Sskip >Hinit_eq_Sskip 2858 whd in match (simplify_statement ?); 2859 whd in match (is_Sskip ?); 2860 normalize nodelta 2861 elim (Hsim_related cond) * 2862 [ 2: * #error #Hfail #_ >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 2863 | 1: cases (exec_expr ge en m cond) 2864 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2865 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite #Htype_eq_cond >Hrewrite 2866 whd in match (m_bind ?????); whd in match (m_bind ?????); 2867 <Htype_eq_cond 2868 cases (exec_bool_of_val ? (typeof cond)) 2869 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2870 | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????); 2871 normalize nodelta #Heq destruct (Heq) 2872 [ 1: %{(State (simplify_function f) (simplify_statement body) 2873 (Kfor2 (simplify_e cond) (simplify_statement step) (simplify_statement body) k') en m)} 2874 @conj [ 1: // | 2: %1 @cc_for2 // ] 2875 | 2: %{(State (simplify_function f) Sskip k' en m)} @conj 2876 [ 1: // | 2: %1 // ] 2877 ] ] ] ] ] 2878 | 9: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2879 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2880 whd in match (exec_step ??) in Heq ⊢ %; 2881 inversion Hcont_cast in Heq; normalize nodelta 2882 [ 1: #Hk #Hk' #_ 2883 | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 2884 | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 2885 | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 2886 | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 2887 | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 2888 | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] 2889 #H whd in match (ret ??) in H ⊢ %; 2890 destruct (H) 2891 [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ] 2892 | 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ] 2893 | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2894 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2895 whd in match (exec_step ??) in Heq ⊢ %; 2896 inversion Hcont_cast in Heq; normalize nodelta 2897 [ 1: #Hk #Hk' #_ 2898 | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 2899 | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 2900 | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 2901 | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 2902 | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 2903 | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] 2904 #H whd in match (ret ??) in H ⊢ %; 2905 destruct (H) 2906 [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 // 2907 | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} 2908 @conj try // %1 // 2909 | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H; 2910 [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) 2911 | 1: cases (exec_expr ??? cond) 2912 [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2913 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite 2914 whd in match (m_bind ?????) in ⊢ (% → %); 2915 <Htype_cond_eq 2916 cases (exec_bool_of_val ? (typeof cond)) 2917 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 2918 | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????); 2919 normalize nodelta #Heq destruct (Heq) 2920 [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)} 2921 @conj [ 1: // | 2: %1 // ] 2922 | 2: %{(State (simplify_function f) Sskip k0' en m)} 2923 @conj [ 1: // | 2: %1 // ] 2924 ] ] ] ] 2925 | 5: %{(State (simplify_function f) (simplify_statement step) 2926 (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj 2927 [ 1: // | 2: %1 @cc_for3 // ] 2928 ] 2929 | 11: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2930 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2931 whd in match (exec_step ??) in Heq ⊢ %; 2932 cases retval in Heq; normalize nodelta 2933 [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta 2934 whd in match (ret ??) in ⊢ (% → %); 2935 [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty' 2936 | 7: #id #fl | 8: #id #fl | 9: #rg #id ] 2937 #H destruct (H) 2938 %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))} 2939 @conj [ 1: // | 2: %3 @call_cont_simplify // ] 2940 | 2: #e >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta 2941 [ 1: #_ #Habsurd destruct (Habsurd) 2942 | 2: #_ elim (Hsim_related e) * 2943 [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2944 | 1: cases (exec_expr ??? e) 2945 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2946 | 1: #a #Hsim #Htype_eq_e lapply (Hsim a (refl ? (OK ? a))) 2947 #Hrewrite >Hrewrite 2948 whd in match (m_bind ?????); whd in match (m_bind ?????); 2949 #Heq destruct (Heq) 2950 %{(Returnstate (\fst a) (call_cont k') (free_list m (blocks_of_env en)))} 2951 @conj [ 1: // | 2: %3 @call_cont_simplify // ] 2952 ] ] ] ] 2953 | 12: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2954 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2955 whd in match (exec_step ??) in Heq ⊢ %; 2956 elim (Hsim_related cond) in Heq; * 2957 [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2958 | 1: cases (exec_expr ??? cond) 2959 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2960 | 1: #a #Hsim #Htype_eq_cond lapply (Hsim a (refl ? (OK ? a))) 2961 #Hrewrite >Hrewrite 2962 whd in match (bindIO ??????); whd in match (bindIO ??????); 2963 cases (\fst a) normalize nodelta 2964 [ 1,3,4,5: #a destruct (a) #b destruct (b) 2965 | 2: #sz #i whd in match (ret ??) in ⊢ (% → %); #Heq destruct (Heq) 2966 %{(State (simplify_function f) 2967 (seq_of_labeled_statement (select_switch sz i (simplify_ls switchcases))) 2968 (Kswitch k') en m)} @conj 2969 [ 1: // 2970 | 2: @(labeled_statements_ind … switchcases) 2971 [ 1: #default_s 2972 whd in match (simplify_ls ?); 2973 whd in match (select_switch sz i ?) in ⊢ (?%%); 2974 whd in match (seq_of_labeled_statement ?) in ⊢ (?%%); 2975 %1 @cc_switch // 2976 | 2: #sz' #i' #top_case #tail #Hind 2977 cut ((seq_of_labeled_statement (select_switch sz i (simplify_ls (LScase sz' i' top_case tail)))) 2978 = (simplify_statement (seq_of_labeled_statement (select_switch sz i (LScase sz' i' top_case tail))))) 2979 [ 1: >select_switch_commute >simplify_ls_commute @refl 2980 | 2: #Hrewrite >Hrewrite 2981 %1 @cc_switch // 2982 ] ] ] ] ] ] 2983 | 13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2984 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2985 whd in match (exec_step ??) in Heq ⊢ %; 2986 destruct (Heq) 2987 %{(State (simplify_function f) (simplify_statement body) k' en m)} 2988 @conj %1 // 2989 | 14: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2990 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2991 whd in match (exec_step ??) in Heq ⊢ %; 2992 lapply (cast_find_label_fn lab f (call_cont k) (call_cont k')) 2993 cases (find_label lab (fn_body f) (call_cont k)) in Heq; 2994 normalize nodelta 2995 [ 1: #Habsurd destruct (Habsurd) 2996 | 2: * #st #kst normalize nodelta 2997 #Heq whd in match (ret ??) in Heq; 2998 #H lapply (H st kst (call_cont_simplify ???) (refl ? (Some ? 〈st,kst〉))) try // 2999 * #kst' * #Heq2 #Hcont_cast' >Heq2 normalize nodelta 3000 destruct (Heq) 3001 %{(State (simplify_function f) (simplify_statement st) kst' en m)} @conj 3002 [ 1: // | 2: %1 // ] 3003 ] 3004 | 15: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 3005 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 3006 whd in match (exec_step ??) in Heq ⊢ %; 3007 destruct (Heq) 3008 %{(State (simplify_function f) (simplify_statement body) k' en m)} 3009 @conj 3010 [ 1: // | 2: %1 // ] 3011 ] 3012 | 2: (* Call state *) 3013 #fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 3014 whd in match (exec_step ??) in ⊢ (% → %); 3015 elim fd in Heq_s1'; normalize nodelta 3016 [ 1: * #rettype #args #vars #body #Heq_s1' 3017 whd in match (simplify_function ?); 3018 cases (exec_alloc_variables empty_env ??) 3019 #local_env #new_mem normalize nodelta 3020 cases (exec_bind_parameters ????) 3021 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 3022 | 1: #new_mem_init 3023 whd in match (m_bind ?????); whd in match (m_bind ?????); 3024 #Heq destruct (Heq) 3025 %{(State (mk_function rettype args vars (simplify_statement body)) 3026 (simplify_statement body) k' local_env new_mem_init)} @conj 3027 [ 1: // | 2: %1 // ] 3028 ] 3029 | 2: #id #argtypes #rettype #Heq_s1' 3030 cases (check_eventval_list args ?) 3031 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) 3032 | 1: #l whd in match (m_bind ?????); whd in match (m_bind ?????); 3033 #Habsurd destruct (Habsurd) ] 3034 ] 3035 | 3: (* Return state *) 3036 #res #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 3037 whd in match (exec_step ??) in ⊢ (% → %); 3038 inversion Hcont_cast 3039 [ 1: #Hk #Hk' #_ 3040 | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 3041 | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 3042 | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 3043 | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 3044 | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 3045 | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] 3046 normalize nodelta 3047 [ 1: cases res normalize nodelta 3048 [ 2: * normalize nodelta #i 3049 [ 3: #Heq whd in match (ret ??) in Heq; destruct (Heq) 3050 %{(Finalstate i)} @conj [ 1: // | 2: // ] 3051 | * : #Habsurd destruct (Habsurd) ] 3052 | *: #a try #b destruct ] 3053 | 9: elim r normalize nodelta 3054 [ 2: * * #block #offset #typ normalize nodelta 3055 cases (opt_to_io io_out io_in mem ? (store_value_of_type' ????)) 3056 [ 2: #mem whd in match (m_bind ?????); whd in match (m_bind ?????); 3057 #Heq destruct (Heq) 3058 %{(State (simplify_function f0) Sskip k0' en0 mem)} @conj 3059 [ 1: // | 2: %1 // ] 3060 | 1: #output #resumption 3061 whd in match (m_bind ?????); #Habsurd destruct (Habsurd) 3062 | 3: #eror #Habsurd normalize in Habsurd; destruct (Habsurd) ] 3063 | 1: #Heq whd in match (ret ??) in Heq; destruct (Heq) 3064 %{(State (simplify_function f0) Sskip k0' en0 m)} @conj 3065 [ 1: // | 2: %1 // ] 3066 ] 3067 | *: #Habsurd destruct (Habsurd) ] 3068 | 4: (* Final state *) 3069 #r #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 3070 whd in match (exec_step ??) in ⊢ (% → %); 3071 #Habsurd destruct (Habsurd) 3072 ] qed. 3073
Note: See TracChangeset
for help on using the changeset viewer.
