Changeset 2825
 Timestamp:
 Mar 8, 2013, 8:36:08 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r2822 r2825 410 410 cl_env → 411 411 cm_env → 412 var_types → 412 413 (*frame_data cl_f cl_ge cm_ge INV →*) (* data for the current stack frame in CL and CM *) 413 414 option typ → (* optional target type  uniform over a given function *) … … 418 419  ClCm_cont_stop: 419 420 ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type. 420 ∀cl_env, cm_env .421 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type Kstop Kend421 ∀cl_env, cm_env, alloc_type. 422 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type Kstop Kend 422 423 423 424 (* Seq continuation *) … … 437 438 ∀Htranslate_inv. 438 439 translate_statement alloc_type stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 439 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type cl_k' cm_k' →440 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')440 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 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') 441 442 442 443 (* While continuation *) … … 485 486 (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip) 486 487 (St_label exit St_skip)), cm_k'〉, Hinv» → 487 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type cl_k' cm_k' →488 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).488 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 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')). 489 490 490 491 … … 532 533 ∀cm_env, cm_m. 533 534 ∀stackptr, stacksize. 534 (*  relate Clight continuation to Cminor continuation  *)535 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env rettyp cl_k cm_k →536 535 (*  Cminor invariants  *) 537 536 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f). … … 552 551 ∀Htranslate_inv. 553 552 translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 553 (*  relate Clight continuation to Cminor continuation  *) 554 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k → 554 555 (*  state additional invariants  *) 555 556 ∀Em: embedding. … … 577 578 (* call to a function with no return value, or which returns in a local variable in Cminor *) 578 579 ∀cl_ge, cm_ge, cl_f, cm_f. 579 ∀INV: clight_cminor_inv cl_ge cm_ge. 580 ∀ cl_env, cl_m, cm_env, cm_m, stackptr.580 ∀INV: clight_cminor_inv cl_ge cm_ge. 581 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, stackptr. 581 582 (* TODO: put the actual invariants on memory and etc. here *) 582 583 ∀u: universe SymbolTag. … … 592 593 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧ 593 594 translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧ 594 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env rettyp cl_k cm_k595 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k 595 596  CL_External name argtypes rettype ⇒ 596 597 True … … 628 629 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧ 629 630 translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧ 630 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env rettyp cl_k cm_k631 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k 631 632  CL_External name argtypes rettype ⇒ 632 633 True … … 658 659  CMR_while: 659 660 ∀cl_ge,cm_ge,INV,cl_f,cm_f. 660 ∀cl_env, cl_m, cm_env, cm_m, stackptr. 661 ∀cl_env, cl_m, cm_env, cm_m, stackptr, stacksize. 662 ∀alloc_type. 661 663 ∀cl_k, cm_k. 662 664 ∀sz,sg, cl_cond_desc. … … 664 666 ∀entry_label, exit_label. 665 667 ∀cm_cond, cm_body. 666 ∀cm_stack. 668 ∀cm_stack. 667 669 ∀kInv: cont_inv cm_f cm_env cm_k. 668 670 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f). … … 671 673 (St_seq 672 674 (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip) 673 (St_label exit_label St_skip))). 675 (St_label exit_label St_skip))). 676 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbls. 677 (* Invariants *) 678 ∀Em: embedding. 679 tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em → (* locals are properly allocated *) 680 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 → (* specify how alloc_type is built *) 681 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *) 682 memory_inj Em cl_m cm_m → (* memory injection *) 683 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type → (* map CL env to CM env *) 684 (* Expression translation and related hypotheses *) 685 ∀Hcond_tr. (* invariant after converting conditional expr *) 686 translate_expr alloc_type (Expr cl_cond_desc (Tint sz sg)) = OK ? «cm_cond, Hcond_tr » → 687 (* Statement translation *) 688 ∀target_type, Htranslate_inv. 689 translate_statement alloc_type stmt_univ lbl_univ lbls 690 (ConvertTo entry_label exit_label) target_type cl_body 691 = OK ? «〈stmt_univ',lbl_univ',cm_body〉,Htranslate_inv» → 692 (* translate_statement alloc_type *) 674 693 (clight_cminor_rel cl_ge cm_ge INV 675 694 (ClState cl_f (Swhile (Expr cl_cond_desc (Tint sz sg)) cl_body) cl_k cl_env cl_m) … … 679 698 (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip) 680 699 (St_label exit_label St_skip))) 681 cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)). 682 700 cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)). 683 701 684 702 definition clight_normal : Clight_state → bool ≝ … … 1270 1288 #Heq destruct (Heq) 1271 1289 @refl 1272 ] qed. 1290 ] qed. 1291 1292 lemma eval_bool_of_val_to_Cminor : 1293 ∀E. ∀ty. ∀v1,v2. ∀b. 1294 value_eq E v1 v2 → 1295 exec_bool_of_val v1 ty = return b → 1296 eval_bool_of_val v2 = return b. 1297 #E #ty #v1 #v2 #b #Hvalue_eq 1298 whd in ⊢ ((??%%) → (??%%)); 1299 @(value_eq_inversion … Hvalue_eq) normalize nodelta 1300 [ #Habsurd destruct (Habsurd) ] 1301 [ #vsz #vi cases ty 1302 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1303  #structname #fieldspec  #unionname #fieldspec  #id ] normalize nodelta 1304 [ 2:  *: #Habsurd destruct (Habsurd) ] 1305 @(intsize_eq_elim_elim … vsz sz) 1306 [ 1: #H #Habsurd destruct (Habsurd) 1307  2: #Heq destruct (Heq) normalize nodelta #H @H ] 1308  cases ty 1309 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1310  #structname #fieldspec  #unionname #fieldspec  #id ] normalize nodelta 1311 #H destruct (H) @refl 1312  #p1 #p2 #Htranslate 1313 cases ty 1314 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1315  #structname #fieldspec  #unionname #fieldspec  #id ] normalize nodelta 1316 #H destruct (H) @refl 1317 ] qed. 1273 1318 1274 1319 (*  *) … … 1315 1360 [ 3: (* Call *) 1316 1361 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 1317 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #Hcont_rel1362 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize 1318 1363 (* introduce everything *) 1319 1364 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function … … 1322 1367 (* generalize away ugly proof *) 1323 1368 generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly 1324 #Htranslate # Em1369 #Htranslate #Hcont_rel #Em 1325 1370 #Htmp_vars_well_allocated 1326 1371 #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id … … 1549 1594  1: (* Skip *) 1550 1595 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 1551 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #Hcont_rel 1596 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize 1597 (* introduce everything *) 1598 #fInv #sInv #kInv 1599 #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 1600 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 1601 #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved 1602 #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly 1603 whd in ⊢ ((??%?) → ?); #Heq_translate 1604 #Hcont_rel 1605 lapply Heq_translate Heq_translate 1606 lapply Hugly Hugly 1607 lapply Hlabel_wf Hlabel_wf 1608 lapply Hreturn_ok Hreturn_ok 1609 lapply Htmps_preserved Htmps_preserved 1610 lapply Hlabels_translated Hlabels_translated 1611 lapply Hstmt_inv Hstmt_inv 1612 lapply Htranslate_function Htranslate_function 1613 lapply Hfresh_globals Hfresh_globals 1614 lapply Hfresh_function Hfresh_function 1615 lapply Htarget_type Htarget_type 1616 lapply kInv kInv 1617 lapply sInv sInv 1618 lapply fInv fInv 1619 lapply stmt_univ stmt_univ 1620 lapply stmt_univ' stmt_univ' 1552 1621 (* case analysis on continuation *) 1553 1622 inversion Hcont_rel 1554 1623 [ (* Kstop continuation *) 1555 1624 (* simplifying the goal using outcome of the inversion *) 1556 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env 1625 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type 1557 1626 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 1558 1627 destruct (HA HB) … … 1560 1629 destruct (HC HD HE) 1561 1630 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 1562 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ 1563 destruct (HF HG HH HI HJ ) #_1631 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 1632 destruct (HF HG HH HI HJ HK) #_ 1564 1633 (* introduce everything *) 1565 #fInv #sInv #kInv 1566 #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 1567 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 1568 #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved 1569 #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly 1634 #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 1635 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf 1636 #Hugly generalize in match (conj ????); #Hugly' 1570 1637 (* reduce statement translation function *) 1571 whd in ⊢ ((??%?) → ?);1572 1638 #Heq_translate 1573 1639 (* In this simple case, trivial translation *) … … 1596 1662 destruct (HC HD HE) 1597 1663 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI 1598 @(jmeq_absorb ?????) #HJ 1599 destruct (HF HG HH HI HK) #_ 1600 #fInv #sInv #kInv #Hktarget_type 1601 #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 1602 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 1603 #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved 1604 #Hreturn_ok #Hlabel_wf 1605 generalize in match (conj ????); #Hugly 1664 @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 1665 destruct (HF HG HH HI HJ HK) #_ 1666 #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 1667 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf 1668 #Hugly generalize in match (conj ????); #Hugly' 1606 1669 (* In this simple case, trivial translation *) 1607 whd in ⊢ ((??%?) → ?);#Heq_translate destruct (Heq_translate)1670 #Heq_translate destruct (Heq_translate) 1608 1671 #Em 1609 1672 #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id … … 1615 1678 %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl 1616 1679 (* close simulation *) 1617 %1{kINV kHcont_rel ? ? Hfresh_globals Hfresh_function 1618 Htranslate_function kstmt_univ kstmt_univ' klbl_univ klbl_univ' klbls kflag} 1619 (* TODO wrap this up properly *) 1620 try assumption 1680 @(CMR_normal … kHeq_translate … Hinjection … Hmatching) try assumption 1681 (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *) 1621 1682 @cthulhu 1622 1683 (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *) … … 1635 1696 destruct (HC HD HE) 1636 1697 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 1637 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ 1638 destruct (HF HG HH HI HJ) #_ 1639 #fInv #sInv * whd in ⊢ (% → ?); * * 1640 whd in ⊢ (% → ?); * whd in ⊢ (% → ?); #Hlabel_defined * #kInv 1641 #Heq_rettyp 1642 #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 1643 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 1644 #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved 1645 #Hreturn_ok #Hlabel_wf 1646 (* reduce translation function and eliminate result *) 1698 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 1699 destruct (HF HG HH HI HJ HK) #_ 1700 #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals 1701 #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf 1702 #Hugly generalize in match (conj ????); #Hugly' 1647 1703 (* In this simple case, trivial translation *) 1648 whd in ⊢ ((??%?) → ?);#Heq_translate destruct (Heq_translate)1704 #Heq_translate destruct (Heq_translate) 1649 1705 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching 1650 1706 #HEm_fn_id … … 1654 1710 destruct (HC HD HE) #_ #s2 #tr 1655 1711 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 1656 generalize in match (conj ????); #Hnoise'''1657 1712 lapply kHfind_label kHfind_label 1658 1713 generalize in ⊢ ((??(????%????)?) → ?); #Hlabel_exists … … 1667 1722 [ 2: #Habsurd destruct (Habsurd) ] 1668 1723 (* go to a special simulation state for while loops *) 1669 @CMR_while 1724 @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHeq_translate) 1725 try assumption 1726 (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *) 1727 @cthulhu 1728 (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *) 1670 1729 ] 1671 1730  2: (* Assign *) 1672 1731 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 1673 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #Hcont_rel1732 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize 1674 1733 (* introduce everything *) 1675 1734 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function … … 1677 1736 #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved 1678 1737 #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate 1738 #Hcont_rel 1679 1739 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id 1680 1740 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB … … 1866 1926 generalize in match (conj ????); #Hstmt_vars 1867 1927 @(CMR_normal … Halloc_hyp) try assumption 1868 [ 3: @refl  *: ]1928 [ 2: @refl  *: ] 1869 1929 [ (* Need a particular kind of continuation relation *) @cthulhu 1870 1930  (* Lemma on preservation of wellallocatedness through update_present *) @cthulhu … … 1935 1995 ] 1936 1996  *: @cthulhu ] 1937  *: @cthulhu 1938 ] qed. 1997  2: (* Return state *) 1998 @cthulhu 1999  3: (* Call state, nostore *) 2000 @cthulhu 2001  4: (* Call state, store *) 2002 @cthulhu 2003  5: (* Intermediary While state *) 2004 (*  *) 2005 #cl_ge #cm_ge #INV' 2006 #cl_f #cm_f #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #alloc_type 2007 #cl_k #cm_k #sz #sg #cl_cond_desc #cl_body #entry_label #exit_label #cm_cond #cm_body 2008 #cm_stack #kInv #fInv #sInv #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 2009 #Em #Htmp_vars_well_allocated #Halloc_hyp 2010 #Hcl_env_hyp #Hinjection #Hmatching #Hexpr_vars #Htranslate_expr #target_type 2011 #Htranslate_inv #Htranslate_statement 2012 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2013 destruct (HA HB) 2014 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 2015 destruct (HC HD HE) #_ 2016 #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep 2017 (* execute clight condition *) 2018 cases (bindIO_inversion ??????? Hstep) Hstep 2019 * #cl_cond_val #cl_cond_trace * #Hcl_exec_cond #Hstep 2020 cases (bindIO_inversion ??????? Hstep) Hstep 2021 #cl_cond_bool * #Hcl_bool_of_val whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 2022 (* The numbers of steps to execute in Cminor depends on the outcome of the condition 2023 evaluation *) 2024 cases cl_cond_bool in Hcl_bool_of_val; 2025 [ (* cond = true: continue looping *) 2026 #Hcl_bool_of_val 2027 %{4} whd whd in ⊢ (??%?); normalize nodelta 2028 generalize in match (proj1 ???); #Hpresent_ifthenelse 2029 (* Exhibit simulation of condition evaluation *) 2030 lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_ 2031 lapply (Hsim … Hexpr_vars … Htranslate_expr ?? Hpresent_ifthenelse Hcl_exec_cond) 2032 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond 2033 whd in match (m_bind ?????); 2034 >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val) 2035 normalize nodelta whd 2036 generalize in match (proj1 ???); #Hnoise' 2037 generalize in match (conj ????); #Hnoise'' @conj try @conj 2038 [ 3: #Habsurd destruct (Habsurd) 2039  1: normalize >append_nil @refl 2040  2: @cthulhu 2041 (* @(CMR_normal … Htranslate_statement) try assumption *) 2042 (* TODO: new continuation relation 2043 * pump the necessary invariants up in CMR_while so that CMR_normal can complete here *) 2044 ] 2045  (* cond = false: stop looping *) 2046 #Hcl_bool_of_val 2047 %{3} whd whd in ⊢ (??%?); normalize nodelta 2048 generalize in match (proj1 ???); #Hpresent_ifthenelse 2049 (* Exhibit simulation of condition evaluation *) 2050 lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_ 2051 lapply (Hsim … Hexpr_vars … Htranslate_expr ?? Hpresent_ifthenelse Hcl_exec_cond) 2052 * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond 2053 whd in match (m_bind ?????); 2054 >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val) 2055 normalize nodelta whd 2056 generalize in match (proj1 ???); #Hnoise' 2057 generalize in match (proj2 ???); #Hnoise'' 2058 generalize in match (conj ????); #Hnoise''' 2059 @conj try @conj 2060 [ 3: #Habsurd destruct (Habsurd) 2061  1: normalize @refl 2062  2: @cthulhu 2063 (* @(CMR_normal … Htranslate_statement) try assumption *) 2064 (* TODO: new continuation relation 2065 * pump the necessary invariants up in CMR_while so that CMR_normal can complete here *) 2066 ] 2067 ] 2068 2069 ] qed. 1939 2070 1940 2071 (* TODO: adapt the following to the new goal shape. *)
Note: See TracChangeset
for help on using the changeset viewer.