Changeset 2074


Ignore:
Timestamp:
Jun 14, 2012, 10:23:08 AM (5 years ago)
Author:
garnier
Message:

Prophylactic renaming of a relation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2032 r2074  
    211211
    212212(* Simulation relation used for expression evaluation. *)
    213 inductive simulate (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
    214 | SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → simulate A r1 r2
    215 | SimFail : (∃err. r1 = Error ? err) → simulate A r1 r2.
     213inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
     214| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2
     215| SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.
    216216
    217217(* Invariant of simplify_expr *)
     
    221221     result_flag = false →
    222222     typeof e1 = typeof e2 →
    223      simulate ? (exec_expr ge en m e1) (exec_expr ge en m e2) →
    224      simulate ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) →     
     223     res_sim ? (exec_expr ge en m e1) (exec_expr ge en m e2) →
     224     res_sim ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) →     
    225225     simplify_inv ge en m e1 e2 target_sz target_sg result_flag
    226226(* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *)
     
    233233(* Invariant of simplify_inside *)     
    234234definition conservation ≝ λe,result:expr.
    235 ∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
    236                                                     ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
     235∀ge,en,m. res_sim ? (exec_expr ge en m e) (exec_expr ge en m result)
     236                                                    ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
    237237                                                    ∧ typeof e = typeof result.
    238238
     
    20772077 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
    20782078 
    2079 lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulate A r0 r2.
     2079lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2.
    20802080#A #r0 #r1 #r2 *
    20812081[ 2: * #error #H >H #_ @SimFail /2 by ex_intro/
     
    20862086
    20872087lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' →
    2088   (∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
    2089   (∀ed, ty. simulate ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
     2088  (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
     2089  (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
    20902090#ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined
    20912091[ 1: #sz #ty #i @SimOk #a normalize //
     
    22372237lemma related_globals_expr_simulation : ∀ge,ge',en,m.
    22382238  related_globals ? simplify_fundef ge ge' →
    2239   ∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧
     2239  ∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧
    22402240      typeof e = typeof (simplify_e e).
    22412241#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
     
    22532253lemma related_globals_lvalue_simulation : ∀ge,ge',en,m.
    22542254  related_globals ? simplify_fundef ge ge' →
    2255   ∀e. simulate ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧
     2255  ∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧
    22562256      typeof e = typeof (simplify_e e).
    22572257#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
     
    22722272lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
    22732273related_globals ? simplify_fundef ge ge' →
    2274 ∀args. simulate ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).
     2274∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).
    22752275#ge #ge' #en #m #Hrelated #args
    22762276elim args
Note: See TracChangeset for help on using the changeset viewer.