Ignore:
Timestamp:
Apr 1, 2013, 7:04:56 PM (7 years ago)
Author:
campbell
Message:

Put missing typ check in; adjust proof because I did it a little
differently to Ilias.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r3036 r3054  
    11521152(* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
    11531153lemma translate_dest_id_inversion :
    1154   ∀var_types, e, var_id, ty,H.
    1155    translate_dest var_types e = return IdDest var_types var_id ty H →
     1154  ∀var_types, e, var_id, H.
     1155   translate_dest var_types e = return IdDest var_types ? var_id H →
    11561156   e = Expr (Evar var_id) (typeof e).
    11571157@cthulhu
     
    12511251  ∀cl_block, cl_offset, trace.
    12521252  ∀Hyp_present. 
    1253      translate_dest alloc_type cl_expr = OK ? (MemDest ? cm_expr) →
     1253     translate_dest alloc_type cl_expr = OK ? (MemDest cm_expr) →
    12541254     exec_lvalue cl_ge cl_env cl_m cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
    12551255     ∃cm_val. eval_expr cm_ge ASTptr cm_expr cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
     
    12731273[ #r | #n | ]
    12741274* #cl_type * #Heq_lookup normalize nodelta
    1275 [ 3: cases (type_eq_dec ??) normalize nodelta #H
    1276   [ 2: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
    1277 | *: ]
    1278 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1275whd in ⊢ ((??%%) → ?); [3: cases (typ_eq ??) #Htyp whd in ⊢ (??%% → ?); ] #Heq destruct (Heq)
    12791276whd in ⊢ ((??%?) → ?);
    12801277@(match lookup SymbolTag block cl_env id
     
    14971494    translate_dest vars (Expr ed ty) =
    14981495    (do e1' ← translate_addr vars (Expr ed ty);
    1499      OK ? (MemDest ? e1')).
     1496     OK ? (MemDest e1')).
    15001497#vars *
    15011498[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     
    17541751   memory_matching Em cl_ge cm_ge cl_m' cm_m cl_env
    17551752    (update_present SymbolTag val cm_env var_id Hpresent cm_value) INV stackptr alloc_type.
    1756  
    1757 lemma translate_dest_conservation :
    1758   ∀vars, e1.
    1759   ∀id, t, H.
    1760   translate_dest vars e1 = OK ? (IdDest vars id t H) →
    1761   typeof e1 = t.
    1762 #vars #e1 #id #t #H #Htranslate lapply (translate_dest_id_inversion … Htranslate)
    1763 #Heq >Heq in Htranslate;
    1764 whd in ⊢ ((??%?) → ?);
    1765 generalize in match (refl ??);
    1766 generalize in ⊢ ((???%) → (??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)?) → ?); *
    1767 normalize nodelta
    1768 [ 2: #er #_ #Habsurd destruct (Habsurd) ]
    1769 * * normalize nodelta
    1770 [ #a #b #c #Habsurd
    1771 | #n #t #H #Habsurd
    1772 | #ty #H ]
    1773 [ 1,2: destruct (Habsurd) ]
    1774 cases (type_eq_dec ??) normalize nodelta
    1775 #Hty #Heq destruct (Heq) >Hty @refl
    1776 qed.
    17771753
    17781754lemma alloc_tmp_monotonic :
     
    22352211       #Hdest cases (bind_inversion ????? Hdest) -Hdest #dest *
    22362212       inversion dest normalize nodelta
    2237        [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
     2213       [ (* register dest *) #var_id #His_local @(jmeq_absorb ?????) #Hdest
    22382214         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    22392215         (* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
     
    24552431             #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef
    24562432             whd nodelta in match (typeof ?);
    2457              [ <(translate_dest_conservation … Htranslate_dest)
    2458                @ClCm_cont_call_nostore normalize nodelta
     2433             [ @ClCm_cont_call_nostore normalize nodelta
    24592434               %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id}
    24602435               @conj @refl
     
    27972772          | 3: (* Local *)
    27982773               #Hlookup_var_success
    2799                cases (type_eq_dec ??) normalize nodelta #Htype_eq_dec
     2774               cases (typ_eq ??) normalize nodelta #Htyp_eq
    28002775               whd in ⊢ ((???%) → ?);
    28012776               #Heq destruct (Heq) normalize nodelta -Htranslate_statement
     
    28042779               * #cm_expr #Hexpr_vars * #Htyp_should_eq
    28052780               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    2806                cases (typ_should_eq_inversion (typ_of_type (typeof rhs)) (typ_of_type type_of_var) … Htyp_should_eq)
     2781               cases (typ_should_eq_inversion (typ_of_type (typeof rhs)) (typ_of_type lhs_ty) … Htyp_should_eq)
    28072782               -Htyp_should_eq #Htyp_eq lapply Hexpr_vars_rhs lapply Hexpr_vars
    28082783               -Hlabel_wf -Hreturn_ok -Hlabels_translated -Hstmt_inv_cm lapply sInv               
Note: See TracChangeset for help on using the changeset viewer.