Changeset 2554 for src/Clight/toCminorCorrectness.ma
 Timestamp:
 Dec 13, 2012, 5:22:51 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r2545 r2554 471 471 qed. 472 472 473 (* TODO convert Clight unary ops to frontend ops ops, then prove correspondence for operators (with equal values). *) 474 473 lemma typ_eq_elim : 474 ∀t1,t2. 475 ∀(P: (t1=t2)+(t1≠t2) → Prop). 476 (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2). 477 #t1 #t2 #P #Hl #Hr 478 @(match typ_eq t1 t2 479 with 480 [ inl H ⇒ Hl H 481  inr H ⇒ Hr H ]) 482 qed. 483 484 485 lemma translate_notbool_to_cminor : 486 ∀t,sg,arg. 487 ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop → 488 ∀res. sem_unary_operation Onotbool arg t = Some ? res → 489 eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res. 490 * 491 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 492  #structname #fieldspec  #unionname #fieldspec  #id ] 493 normalize in match (typ_of_type ?); 494 #sg #arg #cmop 495 whd in ⊢ (??%% → ?); #Heq destruct (Heq) 496 cases arg 497 [  #vsz #vi   #vp 498   #vsz #vi   #vp 499   #vsz #vi   #vp 500   #vsz #vi   #vp 501   #vsz #vi   #vp 502   #vsz #vi   #vp 503   #vsz #vi   #vp 504   #vsz #vi   #vp ] 505 #res 506 whd in ⊢ ((??%?) → ?); 507 #Heq 508 [ 6,11,12:  *: destruct (Heq) ] 509 [ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl 510  1: lapply Heq Heq @(eq_intsize_elim … sz vsz) 511 #H normalize nodelta #Heq destruct 512 whd in match (eval_unop ????); 513 cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl 514 ] qed. 515 516 lemma translate_notint_to_cminor : 517 ∀t,t',arg. 518 ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop → 519 ∀res. sem_unary_operation Onotint arg t = Some ? res → 520 eval_unop (typ_of_type t) t' cmop arg = Some ? res. 521 #ty * 522 [ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ] 523 #sz #sg #arg #cmop 524 whd in match (translate_unop ???); 525 @(match typ_eq (ASTint sz sg) (typ_of_type ty) 526 with 527 [ inl H ⇒ ? 528  inr H ⇒ ? ]) 529 normalize nodelta 530 [ 2: #Heq destruct ] 531 lapply H H 532 lapply cmop cmop 533 cases ty 534 [  #sz' #sg'  #ptr_ty  #array_ty #array_sz  #domain #codomain 535  #structname #fieldspec  #unionname #fieldspec  #id ] 536 normalize nodelta 537 #cmop normalize in match (typ_of_type ?); #H destruct 538 #H' normalize in H'; 539 destruct (H') 540 #res 541 whd in match (sem_unary_operation ???); 542 cases arg 543 [  #vsz #vi   #vp 544   #vsz #vi   #vp 545   #vsz #vi   #vp 546   #vsz #vi   #vp ] 547 whd in match (sem_notint ?); 548 #H destruct (H) @refl 549 qed. 550 551 552 lemma translate_negint_to_cminor : 553 ∀t,t',arg. 554 ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop → 555 ∀res. sem_unary_operation Oneg arg t = Some ? res → 556 eval_unop (typ_of_type t) t' cmop arg = Some ? res. 557 #ty * 558 [ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ] 559 #sz #sg #arg #cmop 560 whd in match (translate_unop ???); 561 @(match typ_eq (ASTint sz sg) (typ_of_type ty) 562 with 563 [ inl H ⇒ ? 564  inr H ⇒ ? ]) 565 normalize nodelta 566 [ 2: #Heq destruct ] 567 lapply H H 568 lapply cmop cmop 569 cases ty 570 [  #sz' #sg'  #ptr_ty  #array_ty #array_sz  #domain #codomain 571  #structname #fieldspec  #unionname #fieldspec  #id ] 572 normalize nodelta 573 #cmop normalize in match (typ_of_type ?); #H destruct 574 #H' normalize in H'; 575 destruct (H') 576 #res 577 whd in match (sem_unary_operation ???); 578 cases arg 579 [  #vsz #vi   #vp 580   #vsz #vi   #vp 581   #vsz #vi   #vp 582   #vsz #vi   #vp ] 583 whd in match (sem_neg ??); 584 #H destruct (H) 585 whd in match (eval_unop ????); 586 cases (eq_intsize sz' vsz) in H; normalize nodelta 587 #H destruct @refl 588 qed. 589 590 591 lemma translate_unop : 592 ∀ty,sg,op,cmop. 593 translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop → 594 ∀arg,res. sem_unary_operation op arg ty = Some ? res → 595 eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res. 596 #ty #sg * #cmop #Htranslate #arg 597 [ @translate_notbool_to_cminor assumption 598  @translate_notint_to_cminor assumption 599  @translate_negint_to_cminor assumption ] 600 qed. 601 602 lemma classify_add_inversion : 603 ∀ty1,ty2. 604 (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨ 605 (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨ 606 (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨ 607 (classify_add ty1 ty2 = add_default ty1 ty2). 608 #ty1 #ty2 609 cases (classify_add ty1 ty2) 610 [ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq 611  #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq 612  #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq 613  #tya #tyb %2 @refl ] 614 qed. 615 616 lemma typ_should_eq_inversion : ∀ty1,ty2,P,a,x. typ_should_eq ty1 ty2 P a = OK ? x → ty1 = ty2. 617 * [ #sz #sg ] * [ 1,3: #sz2 #sg2 ] 618 [ 4: #P #a #x normalize #H destruct (H) @refl 619  3: cases sz cases sg #P #A #x normalize #H destruct 620  2: cases sz2 cases sg2 #P #a #x normalize #H destruct ] 621 cases sz cases sz2 cases sg cases sg2 622 #P #a #x #H normalize in H:(??%?); destruct (H) 623 try @refl 624 qed. 625 626 lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t). 627 * 628 [ * * normalize @refl 629  @refl ] 630 qed. 631 632 lemma intsize_eq_elim_inversion : 633 ∀A:Type[0]. 634 ∀sz1,sz2. 635 ∀elt1,f,errmsg,res. 636 intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res → 637 ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)). 638 #A * * #elt1 #f #errmsg #res normalize #H destruct (H) 639 %{(refl ??)} normalize nodelta >H @refl 640 qed. 475 641 476 642 lemma eval_expr_sim : … … 954 1120 %{cm_val} @conj try @refl assumption 955 1121  6: 1122 #ty * 1123 [ cases ty 1124 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1125  #structname #fieldspec  #unionname #fieldspec  #id ] 1126 #e #Hind 1127 whd in match (typeof ?); 1128 #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?); 1129 #Htranslate 1130 [ 3,4,5,8: destruct (Htranslate) 1131  2: lapply Htranslate Htranslate lapply Hexpr_vars Hexpr_vars lapply e' e' 1132 cases sz normalize nodelta 1133 #e' #Hexpr_vars #Htranslate 1134 [ 1, 2: destruct (Htranslate) ] ] 1135 #cl_val #trace #Hyp_present #Hexec_expr 1136 cases (bind_inversion ????? Htranslate) Htranslate 1137 #cmop * #Htranslate_unop #Hexec_arg 1138 cases (bind_inversion ????? Hexec_arg) Hexec_arg 1139 * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1140 cases (bind_inversion ????? Hexec_expr) Hexec_expr 1141 * #cl_arg #cl_trace * #Hexec_cl 1142 whd in ⊢ ((???%) → ?); #Hexec_unop 1143 cases (bind_inversion ????? Hexec_unop) Hexec_unop 1144 #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1145 lapply (opt_to_res_inversion ???? Hopt) Hopt 1146 #Hsem_cl whd in match (eval_expr ???????); 1147 cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl) 1148 #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta 1149 lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl) 1150 * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption 1151 whd in match (typ_of_type Tvoid); 1152 lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop) 1153 #H >H @refl 1154  *: 1155 cases ty 1156 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain  #structname #fieldspec  #unionname #fieldspec  #id 1157   #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain  #structname #fieldspec  #unionname #fieldspec  #id ] 1158 #e #Hind whd in match (typeof ?); whd in match (typ_of_type ?); 1159 #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec 1160 whd in Htranslate:(??%?); 1161 [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ] 1162 cases (bind_inversion ????? Htranslate) Htranslate 1163 #cmop * #Htranslate_unop #Hexec_arg 1164 cases (bind_inversion ????? Hexec_arg) Hexec_arg 1165 * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1166 cases (bind_inversion ????? Hexec) Hexec 1167 * #cl_arg #cl_trace * #Hexec_cl 1168 whd in ⊢ ((???%) → ?); #Hexec_unop 1169 cases (bind_inversion ????? Hexec_unop) Hexec_unop 1170 #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1171 lapply (opt_to_res_inversion ???? Hopt) Hopt 1172 #Hcl_unop whd in match (eval_expr ???????); 1173 cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl) 1174 #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta 1175 lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop) 1176 * #op_res * #Hcl_sem #Hvalue_eq 1177 [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem) 1178 %{op_res} @conj try @refl assumption 1179  5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem) 1180 %{op_res} @conj try @refl assumption 1181 ] 1182 ] 1183  7: (* binary ops *) 1184 #ty 1185 letin s ≝ (typ_of_type ty) 1186 #op #e1 #e2 1187 #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate 1188 cases (bind_inversion ????? Htranslate) Htranslate 1189 * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate 1190 cases (bind_inversion ????? Htranslate) Htranslate 1191 * #rhs #Hexpr_vars_rhs * #Htranslate_rhs 1192 whd in ⊢ ((??%?) → ?); 1193 cases op whd in match (translate_binop ??????); 1194 @cthulhu (* PITA *) 1195  8: #ty #ty' * #ed #ety 1196 cases ety 1197 [  #esz #esg  #eptr_ty  #earray_ty #earray_sz  #edomain #ecodomain 1198  #estructname #efieldspec  #eunionname #efieldspec  #eid ] 1199 whd in match (typeof ?); whd in match (typ_of_type ?); 1200 #Hind whd in match (typeof ?); 1201 #cm_expr #Hexpr_vars #Htranslate 1202 cases (bind_inversion ????? Htranslate) Htranslate 1203 * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate 1204 cases (bind_inversion ????? Htranslate) Htranslate 1205 * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate 1206 [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ] 1207 cases (bind_inversion ????? Htranslate) Htranslate 1208 * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?); 1209 #Heq destruct (Heq) 1210 #cl_val #trace #Hyp_present #Hexec_cm 1211 cases (bind_inversion ????? Hexec_cm) Hexec_cm 1212 * #cm_val #trace0 * #Hexec_cm #Hexec_cast 1213 cases (bind_inversion ????? Hexec_cast) Hexec_cast 1214 #cast_val * #Hexec_cast 1215 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 1216 lapply (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) #Htype_eq 1217 lapply Hexec_cast Hexec_cast 1218 lapply Htyp_should_eq Htyp_should_eq 1219 lapply Htranslate_cast Htranslate_cast 1220 lapply Hexpr_vars_cast Hexpr_vars_cast 1221 lapply cm_cast cm_cast 1222 lapply Hyp_present Hyp_present 1223 lapply Hexpr_vars Hexpr_vars 1224 lapply cm_expr cm_expr 1225 <Htype_eq Htype_eq 1226 whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?); >typ_eq_refl normalize nodelta 1227 cases ty' 1228 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain'  #structname' #fieldspec'  #unionname' #fieldspec'  #id' 1229   #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain'  #structname' #fieldspec'  #unionname' #fieldspec'  #id' 1230   #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain'  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1231 #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast 1232 whd in match (typ_of_type ?) in cm_castee cm_expr Hexpr_vars_castee; 1233 whd in match (typeof ?) in Htranslate_cast Hexec_cast; 1234 #Heq destruct (Heq) 1235 whd in Htranslate_cast:(??%%); 1236 whd in Hexpr_vars; 1237 destruct (Htranslate_cast) 1238 [ 1,2,3,4,7: 1239 lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm) 1240 * #cm_val' * #Heval_castee #Hvalue_eq #Hexec_cast 1241 lapply Hvalue_eq Hvalue_eq lapply Hexec_cm Hexec_cm 1242 whd in Hexec_cast:(??%%); 1243 cases cm_val in Hexec_cast; normalize nodelta 1244 [  #vsz #vi   #vp 1245   #vsz #vi   #vp 1246   #vsz #vi   #vp 1247   #vsz #vi   #vp 1248   #vsz #vi   #vp ] 1249 [ 2,6,10,14,18: 1250  *: #Habsurd destruct (Habsurd) ] 1251 #Hexec_cast #Hexec_cm #Hvalue_eq 1252 [ 1,2,3: 1253 cases (intsize_eq_elim_inversion ??????? Hexec_cast) Hexec_cast 1254 #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ] 1255 [ 2,3: lapply (sym_eq ??? Hcl_val_eq) Hcl_val_eq #Hexec_cast ] 1256 [ 1,2,4,5: 1257 cases (bind_inversion ????? Hexec_cast) 1258 whd in match (typeof ?); 1259 #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta 1260 whd in match (eq_rect_r ??????); 1261 [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ] 1262 @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta 1263 [ 2,4: #foo #Habsurd destruct (Habsurd) ] 1264 #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq) 1265 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 1266 whd in match (typ_of_type ?); whd in match (eval_expr ???????); 1267 >Heval_castee normalize nodelta whd in match (eval_unop ????); 1268 >(value_eq_int_inversion … Hvalue_eq) normalize nodelta 1269 >Heq_vi >eq_bv_true normalize 1270 %{Vnull} @conj try @refl %3 1271  3: destruct (Hcl_val_eq) 1272 whd in match (eval_expr ???????); 1273 >Heval_castee normalize nodelta 1274 whd in match (eval_unop ????); 1275 cases esg normalize nodelta 1276 whd in match (opt_to_res ???); whd in match (m_bind ?????); 1277 [ %{(sign_ext sz' cm_val')}  %{(zero_ext sz' cm_val')} ] @conj try @refl 1278 whd in match (eq_rect_r ??????); 1279 Hexpr_vars Hyp_present Hind Hexec_cm cm_castee 1280 (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for 1281 this reason. *) 1282 lapply Hvalue_eq Hvalue_eq lapply vi vi 1283 cases esz normalize nodelta 1284 #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq) 1285 whd in match (sign_ext ??); whd in match (zero_ext ??); 1286 %2 1287 ] 1288  *: 1289 lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm) 1290 * #cm_val' * #Heval_expr #Hvalue_eq #Hexec_cast >Heval_expr 1291 %{cm_val'} @conj try @refl 1292 lapply Hexec_cast Hexec_cast lapply Hvalue_eq Hvalue_eq 1293 Hind Hexpr_vars Hyp_present lapply Hexec_cm Hexec_cm 1294 cases cm_val 1295 [  #vsz #vi   #vp 1296   #vsz #vi   #vp 1297   #vsz #vi   #vp 1298   #vsz #vi   #vp ] 1299 #Hexec_cm #Hvalue_eq #Hexec_cast 1300 whd in Hexec_cast:(??%%); 1301 [ 1,5,9,13: destruct (Hexec_cast) ] 1302 [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ] 1303 lapply Hexec_cast Hexec_cast 1304 normalize cases (eq_v ?????) normalize 1305 #Habsurd destruct (Habsurd) 1306 ] 1307  9: (* Econdition *) 1308 #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?); 1309 #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present 1310 #Hexec_cm 1311 cases (bind_inversion ????? Hexec_cm) Hexec_cm 1312 * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm 1313 cases (bind_inversion ????? Hexec_cm) Hexec_cm 1314 #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm 1315 cases (bind_inversion ????? Hexec_cm) Hexec_cm 1316 * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse 1317 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1318 cases (bind_inversion ????? Htranslate) Htranslate 1319 * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate 1320 cases (bind_inversion ????? Htranslate) Htranslate 1321 * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate 1322 cases (bind_inversion ????? Htranslate) Htranslate 1323 * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck 1324 lapply (type_should_eq_inversion (typeof e2) ty … Htypecheck) Htypecheck 1325 * #Htypeof_e2_eq_ty 1326 lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) Hind2 1327 lapply Hexpr_vars_e2 Hexpr_vars_e2 lapply cm_expr_e2 cm_expr_e2 1328 >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2 1329 #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) Hjm_type_eq 1330 #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate 1331 cases (bind_inversion ????? Htranslate) Htranslate 1332 * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate 1333 cases (bind_inversion ????? Htranslate) Htranslate 1334 * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck 1335 lapply (type_should_eq_inversion (typeof e3) ty … Htypecheck) Htypecheck 1336 * #Htypeof_e3_eq_ty 1337 lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) Hind3 1338 lapply Hexpr_vars_e3 Hexpr_vars_e3 lapply cm_expr_e3 cm_expr_e3 1339 >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3 1340 #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) Hjm_type_eq 1341 #Hcmexpr_eq3 destruct (Hcm_expr_eq2) 1342 lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) Hind1 1343 lapply Hexpr_vars_e1 Hexpr_vars_e1 lapply cm_expr_e1 cm_expr_e1 1344 lapply Hexec_bool_of_val Hexec_bool_of_val 1345 cases (typeof e1) normalize nodelta 1346 [  #esz #esg  #eptr_ty  #earray_ty #earray_sz  #edomain #ecodomain 1347  #estructname #efieldspec  #eunionname #efieldspec  #eid ] 1348 #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq 1349 whd in Heq:(???%); destruct (Heq) 1350 whd in match (eval_expr ???????); 1351 whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 Hyp_present 1352 lapply (Hind1 … Hyp1 Hexec_cond) Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1 1353 >Heval_e1 normalize nodelta 1354 lapply Hcm_ifthenelse Hcm_ifthenelse 1355 lapply Hexec_cond Hexec_cond 1356 lapply Hexec_bool_of_val Hexec_bool_of_val 1357 lapply Hvalue_eq1 Hvalue_eq1 1358 cases cm_cond_val 1359 [  #vsz #vi   #vp 1360   #vsz #vi   #vp 1361   #vsz #vi   #vp 1362   #vsz #vi   #vp ] 1363 whd in ⊢ (? → (??%%) → ?); 1364 [ 6: 1365  *: #_ #Habsurd destruct (Habsurd) ] 1366 #Hvalue_eq1 #Hsz_check 1367 lapply (intsize_eq_elim_inversion ??????? Hsz_check) Hsz_check 1368 * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????); 1369 #Heq destruct (Heq) 1370 #Hexec_expr_e1 1371 @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) 1372 return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ? 1373 with 1374 [ true ⇒ λHeq. ? 1375  false ⇒ λHeq. ? 1376 ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))))) 1377 normalize nodelta 1378 >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body 1379 whd in match (eval_bool_of_val ?); whd in match (m_bind ?????); 1380 >Heq normalize nodelta 1381 [ Heq Hexec_expr_e1 Hvalue_eq1 Heval_e1 cm_val_e1 Hexpr_vars_e1 destruct (Hcmexpr_eq3) 1382 cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq 1383 normalize %{cm_val3} @conj try @refl assumption 1384  Heq Hexec_expr_e1 Hvalue_eq1 Heval_e1 cm_val_e1 Hexpr_vars_e1 destruct (Hcmexpr_eq2) 1385 cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq 1386 normalize %{cm_val2} @conj try @refl assumption ] 1387  10: (* andbool *) 956 1388 #ty cases ty 957 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1389 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 958 1390  #structname #fieldspec  #unionname #fieldspec  #id ] 959 whd in match (typeof ?); 960 #op #e #Hind 961 whd in match (typeof ?); whd in match (typ_of_type ?); 962 #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec 1391 #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?); 1392 #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr 1393 (* decompose first slice of clight execution *) 1394 cases (bind_inversion ????? Hexec_expr) Hexec_expr 1395 * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr 1396 cases (bind_inversion ????? Hexec_expr) Hexec_expr 1397 #b * #Hexec_bool_of_val #Hexec_expr 1398 (* decompose translation to Cminor *) 1399 cases (bind_inversion ????? Htranslate) Htranslate normalize nodelta 1400 * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate 963 1401 cases (bind_inversion ????? Htranslate) Htranslate 964 #op * #Htranslate_unop #Hexec_arg 965 cases (bind_inversion ????? Hexec_arg) Hexec_arg 966 * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 967 cases (bind_inversion ????? Hexec) Hexec 968 * #cl_val #cl_trace * #Hexec_cl 969 whd in ⊢ ((???%) → ?); #Hexec_unop 970 cases (bind_inversion ????? Hexec_unop) Hexec_unop 971 #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 972 lapply (opt_to_res_inversion ???? Hopt) Hopt 973 #Hsem_cl whd in match (eval_expr ???????); 974 cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl) 975 #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta 976 lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl) 1402 * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?); 1403 [ 2:  *: #Heq destruct (Heq) ] 1404 (* discriminate I16 and I8 cases *) 1405 (* lapply Hyp_present Hyp_present 1406 lapply Hexpr_vars Hexpr_vars 1407 lapply cm_expr cm_expr cases sz 1408 #cm_expr #Hexpr_vars #Hyp_present normalize nodelta 1409 [ 1,2: #Habsurd destruct (Habsurd) ] *) 1410 (* go on with decomposition *) 1411 #Htranslate cases (bind_inversion ????? Htranslate) Htranslate 1412 * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck 1413 (* cleanup the type coercion *) 1414 lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) Htypecheck 1415 * #Htypeof_e2_eq_ty 1416 lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) Hind2 1417 lapply Hexpr_vars_e2_wt Hexpr_vars_e2_wt 1418 lapply cm_expr_e2_welltyped cm_expr_e2_welltyped whd in match (typ_of_type ?); 1419 lapply Hexpr_vars_e2 Hexpr_vars_e2 1420 lapply cm_expr_e2 cm_expr_e2 1421 lapply Hexec_expr Hexec_expr 1422 >Htypeof_e2_eq_ty normalize nodelta Htypeof_e2_eq_ty 1423 #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2 1424 #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) Heq_e2_wt #Heq destruct (Heq) 1425 (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order 1426 * to proceed in decomposing translation. *) 1427 lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) Hind1 1428 lapply Hexpr_vars_e1 Hexpr_vars_e1 1429 lapply cm_expr_e1 cm_expr_e1 1430 lapply Hexec_bool_of_val Hexec_bool_of_val 1431 cases (typeof e1) 1432 [  #sz1 #sg1  #ptr_ty1  #array_ty1 #array_sz1  #domain1 #codomain1 1433  #structname1 #fieldspec1  #unionname1 #fieldspec1  #id1 ] 1434 #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 1435 normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 1436 (* translation decomposition terminated. Reduce goal *) 1437 whd in match (eval_expr ???????); 1438 (* We need Hind1. *) 1439 cases Hyp_present Hyp_present * #Hyp1 #Hyp2 #Hyp 1440 lapply (Hind1 … Hyp1 Hexec_e1) Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq 1441 normalize nodelta 1442 (* peform case analysis to further reduce the goal. *) 1443 lapply Hvalue_eq Hvalue_eq 1444 lapply Hexec_bool_of_val Hexec_bool_of_val 1445 whd in match (proj2 ???); 1446 cases cl_val_e1 1447 [  #vsz #vi   #vp 1448   #vsz #vi   #vp 1449   #vsz #vi   #vp 1450   #vsz #vi   #vp ] 1451 whd in ⊢ ((??%%) → ?); 1452 [ 6: 1453  *: #Heq destruct (Heq) ] 1454 #Hsz_check #Hvalue_eq 1455 lapply (intsize_eq_elim_inversion ??????? Hsz_check) Hsz_check 1456 * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????); 1457 (* preparing case analysis on b *) 1458 lapply Hexec_expr Hexec_expr 1459 cases b normalize nodelta 1460 [ 2: (* early exit *) 1461 #Heq_early whd in Heq_early:(??%%); destruct (Heq_early) 1462 #Heq_outcome destruct (Heq_outcome) Heq_outcome 1463 >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?); 1464 <e0 whd in match (m_bind ?????); 1465 @cthulhu 1466 (* Pb: incompatible semantics for cl and cm. 1467 * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if 1468 first operand is false (for andbool) 1469 . solution 1 : change semantics to return actual value instead of Vfalse 1470 . solution 2 : change toCminor to introduce another test in the program, 1471 returning Vfalse in case of failure instead of actual value 1472 *) ] 1473 #Hexec_expr #Heq_outcome 1474 cases (bind_inversion ????? Hexec_expr) Hexec_expr 1475 * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr 1476 cases (bind_inversion ????? Hexec_expr) Hexec_expr 1477 #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?); 1478 #Heq destruct (Heq) 1479 >(value_eq_int_inversion … Hvalue_eq) 1480 whd in match (eval_bool_of_val ?); 1481 destruct (Heq_outcome) <e0 whd in match (m_bind ?????); 1482 normalize nodelta 1483 cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2 1484 >Heval_expr normalize nodelta 1485 %{cm_val_e2} @conj try @refl 1486 whd in Hexec_bool_outcome:(??%%); 1487 normalize nodelta in Hexec_bool_outcome:(??%%); 1488 lapply Hvalue_eq2 Hvalue_eq2 1489 Heval_expr 1490 lapply Hexec_bool_outcome Hexec_bool_outcome 1491 cases cl_val_e2 1492 [  #vsz2 #vi2   #vp2 ] normalize nodelta 1493 #Heq destruct (Heq) 1494 cases (intsize_eq_elim_inversion ??????? Heq) 1495 #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????); 1496 cases outcome_bool normalize nodelta 1497 (* Problem. cf prev case. *) 977 1498 @cthulhu 978  *: @cthulhu 1499  11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *) 1500  12: (* sizeof *) 1501 #ty cases ty 1502 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1503  #structname #fieldspec  #unionname #fieldspec  #id ] 1504 #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr 1505 whd in Hexec_expr:(??%?); destruct (Hexec_expr) 1506 normalize in match (typ_of_type ?); 1507 whd in Htranslate:(??%?); destruct (Htranslate) 1508 whd in match (eval_expr ???????); 1509 %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2 1510  13: 1511 #ty #ed #ty' cases ty' 1512 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1513  #structname #fieldspec  #unionname #fieldspec  #id ] 1514 #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present 1515 #Hexec_lvalue 1516 whd in Hexec_lvalue:(??%?); destruct 1517 [ whd in Htranslate_addr:(??%?); 1518 cases (bind_inversion ????? Htranslate_addr) Htranslate_addr 1519 * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr 1520 cases (bind_inversion ????? Htranslate_addr) Htranslate_addr 1521 #field_off * #Hfield_off whd in ⊢ ((???%) → ?); 1522 #Heq destruct (Heq) 1523 cases Hyp_present Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst 1524 ] 1525 cases (bind_inversion ????? Hexec_lvalue) Hexec_lvalue 1526 * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue 1527 [ 1: cases (bind_inversion ????? Hexec_lvalue) Hexec_lvalue #field_off' * 1528 #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H) 1529 cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind) 1530 #cm_val_field * #Heval_cm #Hvalue_eq 1531 whd in match (eval_expr ???????); 1532 >Heval_cm normalize nodelta 1533 whd in match (eval_expr ???????); whd in match (m_bind ?????); 1534 whd in match (eval_binop ???????); normalize nodelta 1535 cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr 1536 normalize nodelta #Hptr_translate 1537 %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))} 1538 @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl 1539 %4 whd in Hptr_translate:(??%?) ⊢ (??%?); 1540 cases (E cl_blo) in Hptr_translate; normalize nodelta 1541 [ #H destruct (H) ] 1542 * #BL #OFF normalize nodelta #Heq destruct (Heq) 1543 >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?); 1544 #H destruct (H) 1545 (* again, mismatch in the size of the integers *) 1546 @cthulhu 1547  2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue) 1548 cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind) 1549 #cm_val * #Heval_expr >Heval_expr #Hvalue_eq 1550 cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq 1551 #Hpointer_translation 1552 %{cm_val} @conj try assumption 1553 destruct @refl 1554 ] 1555  14: (* cost label *) 1556 #ty (* cases ty 1557 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1558  #structname #fieldspec  #unionname #fieldspec  #id ] *) 1559 #l * #ed #ety 1560 whd in match (typeof ?); whd in match (typeof ?); 1561 #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr 1562 cases (bind_inversion ????? Htranslate) Htranslate * #cm_expr 1563 #Hexpr_vars * #Htranslate_ind #Htranslate 1564 cases (bind_inversion ????? Htranslate) Htranslate * #cm_costexpr #Hexpr_vars_costexpr 1565 * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq 1566 whd in match (typeof ?) in Htyp_should_eq:(??%?); 1567 lapply (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq) 1568 #Htyp_eq 1569 lapply Htyp_should_eq Htyp_should_eq 1570 lapply Htranslate_ind Htranslate_ind 1571 lapply Hexpr_vars_costexpr Hexpr_vars_costexpr 1572 lapply Hexec_expr Hexec_expr lapply Hyp_present Hyp_present 1573 lapply Hexpr_vars Hexpr_vars lapply e' e' 1574 lapply Hind Hind lapply cm_expr cm_expr whd in match (typeof ?); 1575 <(Htyp_eq) 1576 #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr 1577 #Htranslate_ind 1578 whd in ⊢ ((??%?) → ?); >typ_eq_refl normalize nodelta 1579 whd in ⊢ ((??%%) → ?); #H destruct (H) whd in match (eval_expr ???????); 1580 cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind 1581 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1582 cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind) 1583 #cm_val' * #Heval_expr' #Hvalue_eq 1584 >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption 1585 (* Inconsistency in clight and cminor executable semantics for expressions~: 1586 placement of the label is either before or after current trace. 1587 To be resolved. 1588 *) 1589 @cthulhu 1590  15: * 1591 [ #sz #i  #var_id  #e1  #e1  #op #e1  #op #e1 #e2  #cast_ty #e1 1592  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ] 1593 #ty normalize in ⊢ (% → ?); 1594 [ 2,3,12: @False_ind 1595  *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present 1596 normalize #Habsurd destruct (Habsurd) ] 979 1597 ] qed. 980 981 982 983 1598 984 1599
Note: See TracChangeset
for help on using the changeset viewer.