Ignore:
Timestamp:
Mar 10, 2013, 1:21:00 PM (7 years ago)
Author:
garnier
Message:

Closing some more cases

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2825 r2838  
    487487            (St_label exit St_skip)), cm_k'〉, Hinv» →
    488488  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')).
    490 
     489  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')
     491    (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).
    491492
    492493(* TODO XXX *)
     
    636637 cl_fun_id = cm_fun_id →
    637638 ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval.
    638  ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs. 
     639 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs.
    639640 (* Explain where the lhs of the post-return assign comes from *)
    640641 exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 →
    641  translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») → 
     642 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») →
    642643 (* TODO: Explain that the actual variable used to store the ret val is fresh and has the
    643644  * right type, etc *)
     
    667668 ∀cm_cond, cm_body.
    668669 ∀cm_stack.
     670 ∀rettyp.
    669671 ∀kInv: cont_inv cm_f cm_env cm_k.
    670672 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
     
    673675            (St_seq
    674676             (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
    675              (St_label exit_label St_skip))).             
    676  ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbls.
     677             (St_label exit_label St_skip))).
     678 (* ---- relate return type variable to actual return type ---- *)
     679 rettyp = opttyp_of_type (fn_return cl_f) →
     680 (* ---- relate Clight and Cminor functions ---- *)
     681 ∀func_univ: universe SymbolTag.
     682 ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
     683 ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
     684 translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
     685 (* ---- relate continuations ---- *)
     686 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k →
     687 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbl_univ'',lbls.
    677688 (* Invariants *)
    678689 ∀Em: embedding.
     
    682693 memory_inj Em cl_m cm_m →                                                  (* memory injection *)
    683694 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 *)
     695 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
    684696 (* Expression translation and related hypotheses *)
    685697 ∀Hcond_tr.  (* invariant after converting conditional expr *)
    686698 translate_expr alloc_type (Expr cl_cond_desc (Tint sz sg)) = OK ? «cm_cond, Hcond_tr » →
     699 Exists ? (λl':identifier Label.l'=entry_label) (labels_of (f_body cm_f)) →
     700 Exists ? (λl':identifier Label.l'=exit_label) (labels_of (f_body cm_f)) → 
    687701 (* 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 *)
     702 ∀Htranslate_inv.
     703 mklabels lbl_univ = 〈〈entry_label, exit_label〉, lbl_univ'〉 →
     704 translate_statement alloc_type stmt_univ lbl_univ' lbls
     705   (ConvertTo entry_label exit_label) rettyp cl_body
     706   = OK ? «〈stmt_univ',lbl_univ'',cm_body〉,Htranslate_inv» →
     707 (* 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
     711       (St_seq
     712        (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label))
     713         St_skip)
     714        (St_label exit_label St_skip)),
     715      cm_k〉,
     716   Hinv3» →
    693717 (clight_cminor_rel cl_ge cm_ge INV
    694718  (ClState cl_f (Swhile (Expr cl_cond_desc (Tint sz sg)) cl_body) cl_k cl_env cl_m)
     
    699723     (St_label exit_label St_skip)))
    700724   cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
     725
     726 
    701727
    702728definition clight_normal : Clight_state → bool ≝
     
    17001726      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
    17011727      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
    1702       #Hugly generalize in match (conj ????); #Hugly'
     1728      #Hugly
     1729      generalize in match (conj ????); #Hugly'
    17031730      (* In this simple case, trivial translation *)
    17041731      #Heq_translate destruct (Heq_translate)
     
    17141741      generalize in ⊢ ((???(????%)) → ?); #Hmore_invariant
    17151742      #kHfind_label
     1743      (* Kwhile cont case *)
    17161744      %{2} whd whd in ⊢ (??%?); normalize nodelta generalize in match (proj2 ???); #Hmore_noise
    17171745      generalize in match (proj1 ???); #Hmore_noise'
     
    17221750      [ 2: #Habsurd destruct (Habsurd) ]
    17231751      (* go to a special simulation state for while loops *)
    1724       @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHeq_translate)
     1752      @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHmklabels …  kHeq_translate)
    17251753      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 *)           
     1754      [ 1: @cthulhu
     1755         (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)                 
     1756         (* 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 ]
    17291759    ]
    17301760| 2: (* Assign *)
     
    18501880                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    18511881                 %{1} whd whd in ⊢ (??%?); normalize nodelta
    1852                  whd in match (eval_expr ???????);
     1882                 whd in match (eval_expr ???????); 
    18531883                 whd in match (eval_constant ????);
    18541884                 whd in match (m_bind ?????);
     
    20062036#cl_f #cm_f #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #alloc_type
    20072037#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
     2038#cm_stack #rettyp #kInv #fInv #sInv #Hrettyp_eq #func_univ #Hfresh_globals #Hfresh_function
     2039#Htranslate_function #Hcont_rel
     2040#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #lbls
    20092041#Em #Htmp_vars_well_allocated #Halloc_hyp
    2010 #Hcl_env_hyp #Hinjection #Hmatching #Hexpr_vars #Htranslate_expr #target_type
    2011 #Htranslate_inv #Htranslate_statement
     2042#Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hexpr_vars #Htranslate_expr
     2043#Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
     2044#Hinv1 #Hinv2 #Hinv3 #Hfind_label
    20122045@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    20132046destruct (HA HB)
     
    20352068  normalize nodelta whd
    20362069  generalize in match (proj1 ???); #Hnoise'
    2037   generalize in match (conj ????); #Hnoise'' @conj try @conj 
     2070  generalize in match (conj ????); #Hnoise'' @conj try @conj
    20382071  [ 3: #Habsurd destruct (Habsurd)
    20392072  | 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 *)
     2073  | 2: @(CMR_normal … Htranslate_function … Htranslate_statement) try assumption
     2074       @(ClCm_cont_while … Htranslate_inv … Hmk_labels … Htranslate_statement) try assumption
    20442075  ]
    20452076| (* cond = false: stop looping *)
    20462077  #Hcl_bool_of_val
    2047   %{3} whd whd in ⊢ (??%?); normalize nodelta
     2078  %{5} whd whd in ⊢ (??%?); normalize nodelta
    20482079  generalize in match (proj1 ???); #Hpresent_ifthenelse
    20492080  (* Exhibit simulation of condition evaluation *)
     
    20572088  generalize in match (proj2 ???); #Hnoise''
    20582089  generalize in match (conj ????); #Hnoise'''
    2059   @conj try @conj
     2090  whd @conj try @conj
    20602091  [ 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 *)
     2092  | 1: normalize >append_nil >append_nil @refl
     2093  | 2: @(CMR_normal … DoNotConvert) try assumption
     2094       [ 2: @refl | ]
    20662095  ]
    20672096]
    20682097
    2069 ] qed. 
     2098] qed.
     2099
    20702100
    20712101(* TODO: adapt the following to the new goal shape. *)
Note: See TracChangeset for help on using the changeset viewer.