Changeset 2850


Ignore:
Timestamp:
Mar 12, 2013, 3:54:19 PM (4 years ago)
Author:
garnier
Message:

Progress on CL to CM. Some more cases closed modulo some critical lemmas. Some invariants were wrong.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2838 r2850  
    402402}.
    403403
     404definition CMcast : ∀t,t'. CMexpr t → t = t' → CMexpr t'.
     405#t #t' #e #H destruct (H) @e
     406qed.
     407
     408lemma CMcast_identity : ∀t. ∀e: CMexpr t. CMcast t t e (refl ??) = e.
     409#H1 #H2 @refl qed.
     410
     411
    404412(* relate Clight continuations and Cminor ones. *)
    405413inductive clight_cminor_cont_rel :
     
    438446  ∀Htranslate_inv.
    439447  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)) →
    440450  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' →
    441451  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')
     
    456466  (* elements of the source while statement *)
    457467  ∀sz,sg.
     468  ∀cl_ty.
    458469  ∀cl_cond_desc.
    459470  ∀cl_body.
     471  ∀Heq: ASTint sz sg = typ_of_type cl_ty.
    460472
    461473  (* elements of the converted while statement *)
     
    472484  (* relate CL and CM expressions *)
    473485  ∀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») →
    475487
    476488  (* Parameters and results to find_label_always *)
    477489  ∀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)).
    478491  ∀Hinv.
    479492
     
    481494  mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
    482495  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*)
    485500          (St_seq
    486501            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
     
    488503  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' →
    489504  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')
    491506    (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).
    492507
     
    551566  ∀flag                 : convert_flag.
    552567  ∀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)) →
    554571  (* ---- relate Clight continuation to Cminor continuation ---- *)
    555572  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 ---- *) 
    557574  ∀Em: embedding.
    558575  tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
     
    663680 ∀alloc_type.
    664681 ∀cl_k, cm_k. 
    665  ∀sz,sg, cl_cond_desc.
     682 ∀sz,sg, cl_ty, cl_cond_desc.
    666683 ∀cl_body.
    667684 ∀entry_label, exit_label.
    668  ∀cm_cond, cm_body.
     685 ∀cm_cond: CMexpr (ASTint sz sg).
     686 ∀cm_body.
    669687 ∀cm_stack.
    670688 ∀rettyp.
     
    672690 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
    673691 ∀sInv: stmt_inv cm_f cm_env
    674            (St_label entry_label
     692           ((*St_label entry_label*)
    675693            (St_seq
    676694             (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
    677695             (St_label exit_label St_skip))).
     696 (* Constrain the CL type *)             
     697 ∀Heq_ty: ASTint sz sg = typ_of_type cl_ty.           
    678698 (* ---- relate return type variable to actual return type ---- *)
    679699 rettyp = opttyp_of_type (fn_return cl_f) →
     
    696716 (* Expression translation and related hypotheses *)
    697717 ∀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 *)
    699720 Exists ? (λl':identifier Label.l'=entry_label) (labels_of (f_body cm_f)) →
    700721 Exists ? (λl':identifier Label.l'=exit_label) (labels_of (f_body cm_f)) → 
     
    705726   (ConvertTo entry_label exit_label) rettyp cl_body
    706727   = 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)) → 
    707730 (* 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*)
    711735       (St_seq
    712736        (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label))
     
    714738        (St_label exit_label St_skip)),
    715739      cm_k〉,
    716    Hinv3» →
     740   Hinv2» →
    717741 (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)
    719743  (CmState cm_f
    720    (St_label entry_label
     744   ( (*St_label entry_label*)
    721745    (St_seq
    722746     (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
     
    850874(* Note: duplicate in switchRemoval.ma *)
    851875lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
     876
     877lemma fresh_elim_lab : ∀u. ∃fv',u'. fresh Label u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
     878
    852879
    853880lemma breakup_dependent_match_on_pairs :
     
    13431370] qed.
    13441371
     1372lemma 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
     1382qed.
     1383
     1384(* move this to frontend_misc *)
     1385lemma 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 ⊢ (% → ?);
     1388lapply Hexists
     1389generalize in match l2;
     1390elim 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
    13451403(* --------------------------------------------------------------------------- *)
    13461404(* Main simulation results                                                     *)
    1347 (* --------------------------------------------------------------------------- *)
     1405(* -------------------------------------------------------------------;-------- *)
    13481406
    13491407(* Conjectured simulation results
     
    13841442| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
    13851443| 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 *)
    13871596     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
    13881597     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
     
    13931602     (* generalize away ugly proof *)
    13941603     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
    1395      #Htranslate #Hcont_rel #Em
     1604     #Htranslate #Hlabel_inclusion #Hcont_rel #Em
    13961605     #Htmp_vars_well_allocated
    13971606     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     
    16271836    #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
    16281837    #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly
    1629     whd in ⊢ ((??%?) → ?); #Heq_translate    
     1838    whd in ⊢ ((??%?) → ?); #Heq_translate #Hlabel_inclusion
    16301839    #Hcont_rel
    16311840    lapply Heq_translate -Heq_translate
     
    16451854    lapply stmt_univ -stmt_univ
    16461855    lapply stmt_univ' -stmt_univ'
     1856    lapply Hlabel_inclusion -Hlabel_inclusion
    16471857    (* case analysis on continuation *)
    16481858    inversion Hcont_rel
     
    16571867      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
    16581868      destruct (HF HG HH HI HJ HK) #_
    1659       (* introduce everything *)
     1869      (* re-introduce everything *)
     1870      #Hlabel_inclusion
    16601871      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
    16611872      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
     
    16791890      [ 2: #Habsurd destruct (Habsurd) ]
    16801891      @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
    16821894      #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
    16831895      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
    1684       #kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_
     1896      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_
    16851897      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    16861898      destruct (HA HB)
     
    16901902      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
    16911903      destruct (HF HG HH HI HJ HK) #_
     1904      #Hlabel_inclusion
    16921905      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
    16931906      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
    16941907      #Hugly generalize in match (conj ????); #Hugly'
    16951908      (* In this simple case, trivial translation *)
    1696       #Heq_translate destruct (Heq_translate)
    1697       #Em
     1909      #Heq_translate destruct (Heq_translate) #Em
    16981910      #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
    16991911      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     
    17101922    | (* Kwhile continuation *)
    17111923      #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_body
     1924      #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
    17131925      #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      (*     
    17151929      * * * * #kHentry_declared * * * *
    17161930      * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise''
    17171931      #kHcont_inv #kHmklabels #kHeq_translate
    1718       #kHfind_label #kHcont_rel #_
     1932      #kHfind_label *) #kHcont_rel #_
    17191933      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    17201934      destruct (HA HB)
     
    17241938      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
    17251939      destruct (HF HG HH HI HJ HK) #_
     1940      #Hlabel_inclusion
    17261941      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
    17271942      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
    1728       #Hugly 
     1943      #Hugly
    17291944      generalize in match (conj ????); #Hugly'
    17301945      (* In this simple case, trivial translation *)
     
    17421957      #kHfind_label
    17431958      (* 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
    17451961      generalize in match (proj1 ???); #Hmore_noise'
    17461962      >kHfind_label normalize nodelta
     
    17551971         (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)                 
    17561972         (* 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 ]                 
    17591975    ]
    17601976| 2: (* Assign *)
     
    17661982     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
    17671983     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
    1768      #Hcont_rel
     1984     #Hlabel_inclusion #Hcont_rel
    17691985     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
    17701986     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     
    20242240          | 2: (* memory matching *) @cthulhu ]
    20252241     ]
     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 ]
    20262273| *: @cthulhu ]
    20272274| 2: (* Return state *)
     
    20352282#cl_ge #cm_ge #INV'
    20362283#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_body
    2038 #cm_stack #rettyp #kInv #fInv #sInv #Hrettyp_eq #func_univ #Hfresh_globals #Hfresh_function
     2284#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
    20392286#Htranslate_function #Hcont_rel
    20402287#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #lbls
     
    20422289#Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hexpr_vars #Htranslate_expr
    20432290#Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
    2044 #Hinv1 #Hinv2 #Hinv3 #Hfind_label
     2291#Hlabel_inclusion #Hlabel_exists #Hinv1 #Hinv2 #Hfind_label
    20452292@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    20462293destruct (HA HB)
     
    20582305[ (* cond = true: continue looping *)
    20592306  #Hcl_bool_of_val
    2060   %{4} whd whd in ⊢ (??%?); normalize nodelta
     2307  %{3} whd whd in ⊢ (??%?); normalize nodelta
    20612308  generalize in match (proj1 ???); #Hpresent_ifthenelse
    20622309  (* Exhibit simulation of condition evaluation *)
    20632310  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
    20662322  whd in match (m_bind ?????);
    20672323  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
     
    20762332| (* cond = false: stop looping *)
    20772333  #Hcl_bool_of_val
    2078   %{5} whd whd in ⊢ (??%?); normalize nodelta
     2334  %{4} whd whd in ⊢ (??%?); normalize nodelta
    20792335  generalize in match (proj1 ???); #Hpresent_ifthenelse
    20802336  (* Exhibit simulation of condition evaluation *)
    20812337  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
    20842349  whd in match (m_bind ?????);
    20852350  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
Note: See TracChangeset for help on using the changeset viewer.