Changeset 2850
 Timestamp:
 Mar 12, 2013, 3:54:19 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r2838 r2850 402 402 }. 403 403 404 definition CMcast : ∀t,t'. CMexpr t → t = t' → CMexpr t'. 405 #t #t' #e #H destruct (H) @e 406 qed. 407 408 lemma CMcast_identity : ∀t. ∀e: CMexpr t. CMcast t t e (refl ??) = e. 409 #H1 #H2 @refl qed. 410 411 404 412 (* relate Clight continuations and Cminor ones. *) 405 413 inductive clight_cminor_cont_rel : … … 438 446 ∀Htranslate_inv. 439 447 translate_statement alloc_type stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 448 (*  invariant on label existence  *) 449 lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) → 440 450 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' → 441 451 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') … … 456 466 (* elements of the source while statement *) 457 467 ∀sz,sg. 468 ∀cl_ty. 458 469 ∀cl_cond_desc. 459 470 ∀cl_body. 471 ∀Heq: ASTint sz sg = typ_of_type cl_ty. 460 472 461 473 (* elements of the converted while statement *) … … 472 484 (* relate CL and CM expressions *) 473 485 ∀Hexpr_vars. 474 translate_expr alloc_type (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →486 translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? («CMcast ?? cm_cond Heq, Hexpr_vars») → 475 487 476 488 (* Parameters and results to find_label_always *) 477 489 ∀sInv: stmt_inv cm_f cm_env (f_body cm_f). 490 ∀Hlabel_declared: Exists (identifier Label) (λl'.l'=entry) (labels_of (f_body cm_f)). 478 491 ∀Hinv. 479 492 … … 481 494 mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 → 482 495 translate_statement alloc_type stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» → 483 find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f cm_env sInv I = 484 «〈St_label entry 496 (* Invariant on label existence *) 497 lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) → 498 find_label_always entry (f_body cm_f) Kend Hlabel_declared cm_f cm_env sInv I = 499 «〈(*St_label entry*) 485 500 (St_seq 486 501 (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip) … … 488 503 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' → 489 504 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type ( 490 Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k')505 Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k') 491 506 (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')). 492 507 … … 551 566 ∀flag : convert_flag. 552 567 ∀Htranslate_inv. 553 translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 568 translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 569 (*  invariant on label existence  *) 570 lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) → 554 571 (*  relate Clight continuation to Cminor continuation  *) 555 572 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k → 556 (*  state additional invariants  *)573 (*  state invariants for memory and environments  *) 557 574 ∀Em: embedding. 558 575 tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em → (* locals are properly allocated *) … … 663 680 ∀alloc_type. 664 681 ∀cl_k, cm_k. 665 ∀sz,sg, cl_ cond_desc.682 ∀sz,sg, cl_ty, cl_cond_desc. 666 683 ∀cl_body. 667 684 ∀entry_label, exit_label. 668 ∀cm_cond, cm_body. 685 ∀cm_cond: CMexpr (ASTint sz sg). 686 ∀cm_body. 669 687 ∀cm_stack. 670 688 ∀rettyp. … … 672 690 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f). 673 691 ∀sInv: stmt_inv cm_f cm_env 674 ( St_label entry_label692 ((*St_label entry_label*) 675 693 (St_seq 676 694 (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip) 677 695 (St_label exit_label St_skip))). 696 (* Constrain the CL type *) 697 ∀Heq_ty: ASTint sz sg = typ_of_type cl_ty. 678 698 (*  relate return type variable to actual return type  *) 679 699 rettyp = opttyp_of_type (fn_return cl_f) → … … 696 716 (* Expression translation and related hypotheses *) 697 717 ∀Hcond_tr. (* invariant after converting conditional expr *) 698 translate_expr alloc_type (Expr cl_cond_desc (Tint sz sg)) = OK ? «cm_cond, Hcond_tr » → 718 translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? «CMcast ?? cm_cond Heq_ty, Hcond_tr » → 719 (* Label consistency *) 699 720 Exists ? (λl':identifier Label.l'=entry_label) (labels_of (f_body cm_f)) → 700 721 Exists ? (λl':identifier Label.l'=exit_label) (labels_of (f_body cm_f)) → … … 705 726 (ConvertTo entry_label exit_label) rettyp cl_body 706 727 = OK ? «〈stmt_univ',lbl_univ'',cm_body〉,Htranslate_inv» → 728 (*  invariant on label existence  *) 729 lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) → 707 730 (* Express the fact that the label points where it ought to *) 708 ∀Hinv1, Hinv2, Hinv3. 709 find_label_always entry_label (f_body cm_f) Kend Hinv1 cm_f cm_env fInv Hinv2 710 = «〈St_label entry_label 731 ∀Hlabel_exists. 732 ∀Hinv1, Hinv2. 733 find_label_always entry_label (f_body cm_f) Kend Hlabel_exists cm_f cm_env fInv Hinv1 734 = «〈(*St_label entry_label*) 711 735 (St_seq 712 736 (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) … … 714 738 (St_label exit_label St_skip)), 715 739 cm_k〉, 716 Hinv 3» →740 Hinv2» → 717 741 (clight_cminor_rel cl_ge cm_ge INV 718 (ClState cl_f (Swhile (Expr cl_cond_desc (Tint sz sg)) cl_body) cl_k cl_env cl_m)742 (ClState cl_f (Swhile (Expr cl_cond_desc cl_ty) cl_body) cl_k cl_env cl_m) 719 743 (CmState cm_f 720 ( St_label entry_label744 ( (*St_label entry_label*) 721 745 (St_seq 722 746 (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip) … … 850 874 (* Note: duplicate in switchRemoval.ma *) 851 875 lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed. 876 877 lemma fresh_elim_lab : ∀u. ∃fv',u'. fresh Label u = 〈fv', u'〉. #u /3 by ex_intro/ qed. 878 852 879 853 880 lemma breakup_dependent_match_on_pairs : … … 1343 1370 ] qed. 1344 1371 1372 lemma let_prod_as_inversion : 1373 ∀A,B,C: Type[0]. 1374 ∀expr: A × B. 1375 ∀body: ∀a:A. ∀b:B. 〈a,b〉 = expr → res C. 1376 ∀result: C. 1377 (let 〈a,b〉 as E ≝ expr in body a b E) = return result → 1378 ∃x,y. ∃E. 〈x,y〉 = expr ∧ 1379 body x y E = return result. 1380 #A #B #C * #a #b #body #res normalize nodelta #Heq 1381 %{a} %{b} %{(refl ??)} @conj try @refl @Heq 1382 qed. 1383 1384 (* move this to frontend_misc *) 1385 lemma lset_inclusion_Exists : ∀A, l1, l2, P. 1386 Exists A P l1 → lset_inclusion A l1 l2 → Exists A P l2. 1387 #A #l1 #l2 #P #Hexists whd in ⊢ (% → ?); 1388 lapply Hexists 1389 generalize in match l2; 1390 elim l1 1391 [ #l2 @False_ind 1392  #hd #tl #Hind #l2 * 1393 [ 2: #HA * #Hhd #Htl @Hind try assumption 1394  1: #H * #Hmem #_ elim l2 in Hmem; 1395 [ @False_ind 1396  #hd2 #tl2 #Hind * 1397 [ #Heq destruct (Heq) %1 @H 1398  #Hneq %2 @Hind @Hneq ] 1399 ] 1400 ] 1401 ] qed. 1402 1345 1403 (*  *) 1346 1404 (* Main simulation results *) 1347 (*   *)1405 (* ; *) 1348 1406 1349 1407 (* Conjectured simulation results … … 1384 1442  7: #cond #body  8: #init #cond #step #body  9,10:  11: #retval  12: #cond #switchcases  13: #lab #body 1385 1443  14: #lab  15: #cost #body ] 1386 [ 3: (* Call *) 1444 [ 6: (* While *) 1445 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 1446 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize 1447 (* introduce everything *) 1448 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 1449 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 1450 #flag * * * * #Hstmt_inv_cm cases cond #cond_desc #cond_ty 1451 (* early case analysis to avoid dependency hell *) 1452 cases cond_ty 1453 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1454  #structname #fieldspec  #unionname #fieldspec  #id ] 1455 #Hlabels_translated #Htmps_preserved 1456 #Hreturn_ok #Hlabel_wf #Htranslate #Hlabel_inclusion 1457 #Hcont_rel 1458 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id 1459 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1460 destruct (HA HB) 1461 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_ 1462 destruct (HC HD HE) 1463 lapply Htranslate Htranslate 1464 [ 1: generalize in match (conj ????); #Hugly_inv 1465  2: generalize in match (conj ????); #Hugly_inv 1466  3: generalize in match (conj ????); #Hugly_inv 1467  4: generalize in match (conj ????); #Hugly_inv 1468  5: generalize in match (conj ????); #Hugly_inv 1469  6: generalize in match (conj ????); #Hugly_inv 1470  7: generalize in match (conj ????); #Hugly_inv 1471  8: generalize in match (conj ????); #Hugly_inv ] 1472 #Htranslate 1473 cases (bind_inversion ????? Htranslate) Htranslate 1474 whd in match (typeof ?); whd in match (typ_of_type ?); * 1475 #cm_cond #Hexpr_vars_cond * #Htranslate_cond normalize nodelta 1476 [ 3,4,5,8: whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ] 1477 #Htranslate normalize nodelta 1478 lapply (let_prod_as_inversion ?????? Htranslate) Htranslate 1479 * * #entry_label #exit_label * #lbl_univ0 * #Hmk_label_eq * 1480 #Hmk_label_eq_bis normalize nodelta #Htranslate 1481 cases (bind_inversion ????? Htranslate) Htranslate 1482 * * * #stmt_univ0 #lbl_univ1 #cm_body 1483 #Htrans_inv * #Htrans_body normalize nodelta 1484 [ generalize in ⊢ ((??(??(????%))?) → ?); 1485 #Htrans_inv' 1486  generalize in ⊢ ((??(??(????%))?) → ?); 1487 #Htrans_inv' 1488  generalize in ⊢ ((??(??(????%))?) → ?); 1489 #Htrans_inv' 1490  generalize in ⊢ ((??(??(????%))?) → ?); 1491 #Htrans_inv' ] 1492 whd in ⊢ ((???%) → ?); 1493 #Heq destruct (Heq) 1494 #s2 #tr whd in ⊢ ((??%?) → ?); 1495 #Hstep 1496 cases (bindIO_inversion ??????? Hstep) Hstep * #cond_val #cond_trace 1497 * #Hcl_exec_cond #Hstep 1498 cases (bindIO_inversion ??????? Hstep) Hstep 1499 #cl_cond_bool * #Hcl_bool_of_val whd in ⊢ ((??%%) → ?); 1500 cases cl_cond_bool in Hcl_bool_of_val; 1501 [ 1,3,5,7: (* cond = true: continue looping *) 1502 #Hcl_bool_of_val normalize nodelta 1503 #Heq destruct (Heq) 1504 %{4} whd whd in ⊢ (??%?); normalize nodelta 1505 [ generalize in match (proj1 ???); #Hpresent_ifthenelse 1506  generalize in match (proj1 ???); #Hpresent_ifthenelse 1507  generalize in match (proj1 ???); #Hpresent_ifthenelse 1508  generalize in match (proj1 ???); #Hpresent_ifthenelse ] 1509 (* Exhibit simulation of condition evaluation *) 1510 lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_ 1511 [ lapply (Hsim (Expr cond_desc Tvoid) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) 1512  lapply (Hsim (Expr cond_desc (Tint sz sg)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) 1513  lapply (Hsim (Expr cond_desc (Tstruct structname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) 1514  lapply (Hsim (Expr cond_desc (Tunion unionname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) ] 1515 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond 1516 whd in match (m_bind ?????); 1517 >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val) 1518 normalize nodelta whd 1519 [ generalize in match (proj1 ???); #Hnoise' 1520 generalize in match (conj ????); #Hnoise'' 1521  generalize in match (proj1 ???); #Hnoise' 1522 generalize in match (conj ????); #Hnoise'' 1523  generalize in match (proj1 ???); #Hnoise' 1524 generalize in match (conj ????); #Hnoise'' 1525  generalize in match (proj1 ???); #Hnoise' 1526 generalize in match (conj ????); #Hnoise'' ] 1527 @conj try @conj 1528 [ 3,6,9,12: #Habsurd destruct (Habsurd) 1529  1,4,7,10: normalize >append_nil @refl 1530  2,5,8,11: 1531 cut (lset_inclusion (identifier Label) (labels_of cm_body) (labels_of (f_body cm_f))) 1532 [ 1,3,5,7: 1533 lapply Hlabel_inclusion 1534 @transitive_lset_inclusion 1535 @cons_preserves_inclusion 1536 @lset_inclusion_union %1 1537 @lset_inclusion_union %1 1538 @lset_inclusion_union %1 1539 @reflexive_lset_inclusion ] 1540 #Hlabels_of_body 1541 cut (Exists (identifier Label) (λl'.l'=entry_label) (labels_of (f_body cm_f))) 1542 [ 1,3,5,7: @(lset_inclusion_Exists ????? Hlabel_inclusion) 1543 %1 @refl ] 1544 #Hentry_exists 1545 cut (Exists (identifier Label) (λl'.l'=exit_label) (labels_of (f_body cm_f))) 1546 [ 1,3,5,7: @(lset_inclusion_Exists ????? Hlabel_inclusion) 1547 %2 @Exists_append_r %1 @refl ] 1548 #Hexit_exists 1549 @(CMR_normal … Htrans_body) try assumption 1550 @(ClCm_cont_while … (sym_eq … Hmk_label_eq) … Htrans_body) try assumption 1551 [ 1,6,11,16: 1552 @refl 1553  2,3,7,8,12,13,17,18: 1554 >CMcast_identity try assumption 1555  4,9,14,19: 1556 @conj try assumption @conj @conj try assumption @conj @conj try assumption 1557 try @conj try assumption try @conj try assumption 1558 try @conj try assumption try @conj try assumption 1559  5,10,15,20: (* find_label_always *) 1560 (* TODO /!\ we need to find a clever way to prove this. *) 1561 @cthulhu 1562 ] 1563 ] 1564  2,4,6,8: (* cond = false: stop looping *) 1565 #Hcl_bool_of_val normalize nodelta #Heq destruct (Heq) 1566 %{5} whd whd in ⊢ (??%?); normalize nodelta 1567 [ generalize in match (proj1 ???); #Hpresent_ifthenelse 1568  generalize in match (proj1 ???); #Hpresent_ifthenelse 1569  generalize in match (proj1 ???); #Hpresent_ifthenelse 1570  generalize in match (proj1 ???); #Hpresent_ifthenelse ] 1571 (* Exhibit simulation of condition evaluation *) 1572 lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_ 1573 [ lapply (Hsim (Expr cond_desc Tvoid) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) 1574  lapply (Hsim (Expr cond_desc (Tint sz sg)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) 1575  lapply (Hsim (Expr cond_desc (Tstruct structname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) 1576  lapply (Hsim (Expr cond_desc (Tunion unionname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) ] 1577 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond 1578 whd in match (m_bind ?????); 1579 >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val) normalize nodelta whd 1580 [ generalize in match (proj2 ???); #Hnoise' 1581 generalize in match (proj2 ???); #Hnoise'' 1582  generalize in match (proj2 ???); #Hnoise' 1583 generalize in match (proj2 ???); #Hnoise'' 1584  generalize in match (proj2 ???); #Hnoise' 1585 generalize in match (proj2 ???); #Hnoise'' 1586  generalize in match (proj2 ???); #Hnoise' 1587 generalize in match (proj2 ???); #Hnoise'' ] 1588 @conj try @conj try @conj 1589 [ 1,4,7,10: normalize >append_nil >append_nil @refl 1590  2,5,8,11: 1591 @(CMR_normal … Htranslate_function … DoNotConvert … Hcont_rel) try assumption 1592 [ 2,4,6,8: @refl  *: ] 1593  *: #Habsurd destruct (Habsurd) ] 1594 ] 1595  3: (* Call *) 1387 1596 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 1388 1597 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize … … 1393 1602 (* generalize away ugly proof *) 1394 1603 generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly 1395 #Htranslate #H cont_rel #Em1604 #Htranslate #Hlabel_inclusion #Hcont_rel #Em 1396 1605 #Htmp_vars_well_allocated 1397 1606 #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id … … 1627 1836 #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved 1628 1837 #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly 1629 whd in ⊢ ((??%?) → ?); #Heq_translate 1838 whd in ⊢ ((??%?) → ?); #Heq_translate #Hlabel_inclusion 1630 1839 #Hcont_rel 1631 1840 lapply Heq_translate Heq_translate … … 1645 1854 lapply stmt_univ stmt_univ 1646 1855 lapply stmt_univ' stmt_univ' 1856 lapply Hlabel_inclusion Hlabel_inclusion 1647 1857 (* case analysis on continuation *) 1648 1858 inversion Hcont_rel … … 1657 1867 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 1658 1868 destruct (HF HG HH HI HJ HK) #_ 1659 (* introduce everything *) 1869 (* reintroduce everything *) 1870 #Hlabel_inclusion 1660 1871 #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 1661 1872 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf … … 1679 1890 [ 2: #Habsurd destruct (Habsurd) ] 1680 1891 @CMR_return 1681  #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kalloc_type #kcl_s #kcm_s 1892  (* Kseq *) 1893 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kalloc_type #kcl_s #kcm_s 1682 1894 #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag 1683 1895 * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved 1684 #kHreturn_ok #kHlabel_wf #kHeq_translate #kH cont_rel #_1896 #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_ 1685 1897 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1686 1898 destruct (HA HB) … … 1690 1902 @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 1691 1903 destruct (HF HG HH HI HJ HK) #_ 1904 #Hlabel_inclusion 1692 1905 #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 1693 1906 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf 1694 1907 #Hugly generalize in match (conj ????); #Hugly' 1695 1908 (* In this simple case, trivial translation *) 1696 #Heq_translate destruct (Heq_translate) 1697 #Em 1909 #Heq_translate destruct (Heq_translate) #Em 1698 1910 #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id 1699 1911 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB … … 1710 1922  (* Kwhile continuation *) 1711 1923 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kalloc_type #kcl_env #kcm_env 1712 #kcl_k' #kcm_k' #ksz #ksg #kcl_ cond_desc #kcl_body #kcm_cond #kcm_body1924 #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body 1713 1925 #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ'' 1714 #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv 1926 #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared 1927 #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label 1928 (* 1715 1929 * * * * #kHentry_declared * * * * 1716 1930 * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise'' 1717 1931 #kHcont_inv #kHmklabels #kHeq_translate 1718 #kHfind_label #kHcont_rel #_1932 #kHfind_label *) #kHcont_rel #_ 1719 1933 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1720 1934 destruct (HA HB) … … 1724 1938 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 1725 1939 destruct (HF HG HH HI HJ HK) #_ 1940 #Hlabel_inclusion 1726 1941 #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 1727 1942 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf 1728 #Hugly 1943 #Hugly 1729 1944 generalize in match (conj ????); #Hugly' 1730 1945 (* In this simple case, trivial translation *) … … 1742 1957 #kHfind_label 1743 1958 (* Kwhile cont case *) 1744 %{2} whd whd in ⊢ (??%?); normalize nodelta generalize in match (proj2 ???); #Hmore_noise 1959 %{2} whd whd in ⊢ (??%?); normalize nodelta 1960 generalize in match (proj2 ???); #Hmore_noise 1745 1961 generalize in match (proj1 ???); #Hmore_noise' 1746 1962 >kHfind_label normalize nodelta … … 1755 1971 (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *) 1756 1972 (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *) 1757  2: cases Hmore_invariant * * * #_ * * * * * * *1758 #_ #_ #_ * * #_ #H #_ #_ @H ]1973  2: cases Hmore_invariant * * #_ * * * * #_ #_ * #_ #_ * * #_ #H 1974 #_ #_ @H ] 1759 1975 ] 1760 1976  2: (* Assign *) … … 1766 1982 #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved 1767 1983 #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate 1768 #H cont_rel1984 #Hlabel_inclusion #Hcont_rel 1769 1985 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id 1770 1986 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB … … 2024 2240  2: (* memory matching *) @cthulhu ] 2025 2241 ] 2242  4: (* Seq *) 2243 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 2244 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize 2245 (* introduce everything *) 2246 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 2247 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 2248 #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved 2249 #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate #Hlabel_inclusion 2250 #Hcont_rel 2251 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id 2252 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2253 destruct (HA HB) 2254 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_ 2255 destruct (HC HD HE) 2256 cases (bind_inversion ????? Htranslate) Htranslate 2257 * * * #tmp_gen #labgen #cm_s1 #Htrans_inv * #Htrans_stm1 normalize nodelta 2258 #Htranslate cases (bind_inversion ????? Htranslate) Htranslate 2259 * * * #tmp_gen' #labgen' #cm_s2 #Htrans_inv' * #Htrans_stm2 normalize nodelta 2260 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 2261 #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 2262 %{1} whd @conj try @conj try @refl 2263 [ 2: #Habsurd destruct (Habsurd) ] 2264 @(CMR_normal … Htrans_stm1) try assumption 2265 [ 1: lapply Hlabel_inclusion 2266 @transitive_lset_inclusion @lset_inclusion_union %1 2267 @reflexive_lset_inclusion 2268  2: @(ClCm_cont_seq … Htrans_stm2) 2269 [ 1: lapply Hlabel_inclusion @transitive_lset_inclusion @lset_inclusion_union %2 2270 @reflexive_lset_inclusion 2271  2: assumption ] 2272  3: @cthulhu ] 2026 2273  *: @cthulhu ] 2027 2274  2: (* Return state *) … … 2035 2282 #cl_ge #cm_ge #INV' 2036 2283 #cl_f #cm_f #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #alloc_type 2037 #cl_k #cm_k #sz #sg #cl_cond_ desc #cl_body #entry_label #exit_label #cm_cond #cm_body2038 #cm_stack #rettyp #kInv #fInv #sInv #H rettyp_eq #func_univ #Hfresh_globals #Hfresh_function2284 #cl_k #cm_k #sz #sg #cl_cond_ty #cl_cond_desc #cl_body #entry_label #exit_label #cm_cond #cm_body 2285 #cm_stack #rettyp #kInv #fInv #sInv #Heq_ty #Hrettyp_eq #func_univ #Hfresh_globals #Hfresh_function 2039 2286 #Htranslate_function #Hcont_rel 2040 2287 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #lbls … … 2042 2289 #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hexpr_vars #Htranslate_expr 2043 2290 #Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement 2044 #H inv1 #Hinv2 #Hinv3#Hfind_label2291 #Hlabel_inclusion #Hlabel_exists #Hinv1 #Hinv2 #Hfind_label 2045 2292 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2046 2293 destruct (HA HB) … … 2058 2305 [ (* cond = true: continue looping *) 2059 2306 #Hcl_bool_of_val 2060 %{ 4} whd whd in ⊢ (??%?); normalize nodelta2307 %{3} whd whd in ⊢ (??%?); normalize nodelta 2061 2308 generalize in match (proj1 ???); #Hpresent_ifthenelse 2062 2309 (* Exhibit simulation of condition evaluation *) 2063 2310 lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_ 2064 lapply (Hsim … Hexpr_vars … Htranslate_expr ?? Hpresent_ifthenelse Hcl_exec_cond) 2065 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond 2311 lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?)) 2312 [ >Heq_ty @refl ] Hsim #Hsim 2313 lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond) 2314 [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ] 2315 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq Hsim 2316 cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉) 2317 [ lapply Hpresent_ifthenelse 2318 <(CMcast_identity (ASTint sz sg) cm_cond) #foo 2319 lapply Hcm_eval_cond whd in match (eq_ind_r ??????); normalize nodelta cases Heq_ty 2320 #H @H ] 2321 #Heval >Heval 2066 2322 whd in match (m_bind ?????); 2067 2323 >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val) … … 2076 2332  (* cond = false: stop looping *) 2077 2333 #Hcl_bool_of_val 2078 %{ 5} whd whd in ⊢ (??%?); normalize nodelta2334 %{4} whd whd in ⊢ (??%?); normalize nodelta 2079 2335 generalize in match (proj1 ???); #Hpresent_ifthenelse 2080 2336 (* Exhibit simulation of condition evaluation *) 2081 2337 lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_ 2082 lapply (Hsim … Hexpr_vars … Htranslate_expr ?? Hpresent_ifthenelse Hcl_exec_cond) 2083 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond 2338 lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?)) 2339 [ >Heq_ty @refl ] Hsim #Hsim 2340 lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond) 2341 [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ] 2342 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq Hsim 2343 cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉) 2344 [ lapply Hpresent_ifthenelse 2345 <(CMcast_identity (ASTint sz sg) cm_cond) #foo 2346 lapply Hcm_eval_cond whd in match (eq_ind_r ??????); normalize nodelta cases Heq_ty 2347 #H @H ] 2348 #Heval >Heval 2084 2349 whd in match (m_bind ?????); 2085 2350 >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
Note: See TracChangeset
for help on using the changeset viewer.