Ignore:
Timestamp:
Mar 8, 2013, 8:36:08 PM (7 years ago)
Author:
garnier
Message:

Progress, Clight to Cminor

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2822 r2825  
    410410  cl_env →
    411411  cm_env →
     412  var_types →
    412413  (*frame_data cl_f cl_ge cm_ge INV →*)         (* data for the current stack frame in CL and CM *)
    413414  option typ →                              (* optional target type - uniform over a given function *)
     
    418419| ClCm_cont_stop:
    419420  ∀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 Kend
     421  ∀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
    422423
    423424(* Seq continuation *)
     
    437438  ∀Htranslate_inv.
    438439  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')
    441442
    442443(* While continuation *) 
     
    485486            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
    486487            (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')).
    489490
    490491
     
    532533  ∀cm_env, cm_m.
    533534  ∀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 →
    536535  (* ---- Cminor invariants ---- *)
    537536  ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
     
    552551  ∀Htranslate_inv.
    553552  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 →
    554555  (* ---- state additional invariants ---- *) 
    555556  ∀Em: embedding.
     
    577578 (* call to a function with no return value, or which returns in a local variable in Cminor *)
    578579 ∀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.
    581582 (* TODO: put the actual invariants on memory and etc. here *)
    582583 ∀u: universe SymbolTag.
     
    592593    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
    593594    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_k
     595    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k
    595596 | CL_External name argtypes rettype ⇒
    596597   True
     
    628629    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
    629630    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_k
     631    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k
    631632 | CL_External name argtypes rettype ⇒
    632633   True
     
    658659| CMR_while:
    659660 ∀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.
    661663 ∀cl_k, cm_k. 
    662664 ∀sz,sg, cl_cond_desc.
     
    664666 ∀entry_label, exit_label.
    665667 ∀cm_cond, cm_body.
    666  ∀cm_stack. 
     668 ∀cm_stack.
    667669 ∀kInv: cont_inv cm_f cm_env cm_k.
    668670 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
     
    671673            (St_seq
    672674             (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 *)
    674693 (clight_cminor_rel cl_ge cm_ge INV
    675694  (ClState cl_f (Swhile (Expr cl_cond_desc (Tint sz sg)) cl_body) cl_k cl_env cl_m)
     
    679698     (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
    680699     (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)).
    683701
    684702definition clight_normal : Clight_state → bool ≝
     
    12701288  #Heq destruct (Heq)
    12711289  @refl
    1272 ] qed.
     1290] qed.
     1291
     1292lemma 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
     1298whd 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.
    12731318
    12741319(* --------------------------------------------------------------------------- *)
     
    13151360[ 3: (* Call *)
    13161361     #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_rel
     1362     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
    13181363     (* introduce everything *)
    13191364     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     
    13221367     (* generalize away ugly proof *)
    13231368     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
    1324      #Htranslate #Em
     1369     #Htranslate #Hcont_rel #Em
    13251370     #Htmp_vars_well_allocated
    13261371     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     
    15491594| 1: (* Skip *)
    15501595    #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'
    15521621    (* case analysis on continuation *)
    15531622    inversion Hcont_rel
    15541623    [ (* Kstop continuation *)
    15551624      (* 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
    15571626      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    15581627      destruct (HA HB)
     
    15601629      destruct (HC HD HE)
    15611630      @(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) #_
    15641633      (* 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'
    15701637      (* reduce statement translation function *)
    1571       whd in ⊢ ((??%?) → ?);
    15721638      #Heq_translate
    15731639      (* In this simple case, trivial translation *)
     
    15961662      destruct (HC HD HE)
    15971663      @(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'
    16061669      (* In this simple case, trivial translation *)
    1607       whd in ⊢ ((??%?) → ?); #Heq_translate destruct (Heq_translate)
     1670      #Heq_translate destruct (Heq_translate)
    16081671      #Em
    16091672      #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     
    16151678      %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl
    16161679      (* 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 *)
    16211682      @cthulhu
    16221683      (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)
     
    16351696      destruct (HC HD HE)
    16361697      @(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'
    16471703      (* In this simple case, trivial translation *)
    1648       whd in ⊢ ((??%?) → ?); #Heq_translate destruct (Heq_translate)
     1704      #Heq_translate destruct (Heq_translate)
    16491705      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
    16501706      #HEm_fn_id
     
    16541710      destruct (HC HD HE) #_ #s2 #tr
    16551711      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    1656       generalize in match (conj ????); #Hnoise'''
    16571712      lapply kHfind_label -kHfind_label
    16581713      generalize in ⊢ ((??(????%????)?) → ?); #Hlabel_exists
     
    16671722      [ 2: #Habsurd destruct (Habsurd) ]
    16681723      (* 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 *)           
    16701729    ]
    16711730| 2: (* Assign *)
    16721731     #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_rel
     1732     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
    16741733     (* introduce everything *)
    16751734     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     
    16771736     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
    16781737     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
     1738     #Hcont_rel
    16791739     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
    16801740     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     
    18661926                 generalize in match (conj ????); #Hstmt_vars
    18671927                 @(CMR_normal … Halloc_hyp) try assumption
    1868                  [ 3: @refl | *: ]
     1928                 [ 2: @refl | *: ]
    18691929                 [ (* Need a particular kind of continuation relation *) @cthulhu
    18701930                 | (* Lemma on preservation of well-allocatedness through update_present *) @cthulhu
     
    19351995     ]
    19361996| *: @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
     2013destruct (HA HB)
     2014@(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     2015destruct (HC HD HE) #_
     2016#s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
     2017(* execute clight condition *)
     2018cases (bindIO_inversion ??????? Hstep) -Hstep
     2019* #cl_cond_val #cl_cond_trace * #Hcl_exec_cond #Hstep
     2020cases (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 *)
     2024cases 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. 
    19392070
    19402071(* TODO: adapt the following to the new goal shape. *)
Note: See TracChangeset for help on using the changeset viewer.