Changeset 2009


Ignore:
Timestamp:
May 30, 2012, 9:34:19 PM (5 years ago)
Author:
garnier
Message:

Proof of simulation completed for singe-step executions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r1974 r2009  
    2020 *)
    2121
    22 
    23 
    2422(* Attempt to squeeze integer constant into a given type.
    2523
    2624   This might be too conservative --- if we're going to cast it anyway, can't
    27    I just ignore the fact that the integer doesn't fit?
     25   I just ignore the fact that the integer doesn't fit?let (++)
    2826*)
    2927
     
    103101(* /!\ This lemma uses the "uniqueness of identity proofs" K axiom. I've tried doing a proper
    104102 * induction on t but it turns out to be a non-well-founded pandora box. /!\ *)
     103(* Finally useless
    105104lemma type_eq_dec_identity : ∀t. type_eq_dec t t = inl ?? (refl ? t).
    106105#t elim (type_eq_dec t t)
    107106[ 1: @streicherK //
    108107| 2: #H elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.
    109 
    110 
     108*)
     109
     110(* Useless
    111111lemma sign_eq_dec : ∀s1,s2:signedness. (s1 = s2) ∨ (s1 ≠ s2).
    112112* * /2/ %2 % #H destruct
    113113qed.
     114*)
    114115
    115116lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
     
    131132| 2: #Hneq' normalize // ] qed.
    132133
     134(* Useless
    133135lemma type_eq_eq : ∀t1, t2. type_eq t1 t2 = true → t1 = t2.
    134136#t1 #t2 whd in match (type_eq ??); cases (type_eq_dec t1 t2) normalize
    135137[ 1: // | 2: #_ #H destruct ] qed.
     138*)
    136139
    137140definition size_le ≝ λsz1,sz2.
     
    173176#H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed.
    174177 
    175 
    176178(* This defines necessary conditions for [src_expr] to be coerced to "target_ty".
    177179 * Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *)
     
    191193
    192194(* Used to inject boolean functions in invariants. *)
     195(* Useless
    193196definition is_true : bool → Prop ≝ λb.
    194197match b with
    195198[ true ⇒ True
    196199| false ⇒ False ].
     200*)
    197201
    198202(* An useful lemma to cull out recursive calls: the guard forces the target type to be different from the origin type. *)
    199203
    200204(* aux lemma *)
     205(* Useless
    201206lemma size_lt_dec_not_refl : ∀sz. ∃H. size_lt_dec sz sz = inr ??H.
    202207* normalize @(ex_intro … (nmk False (λauto:False.auto))) // qed.
    203 
    204 
    205 
     208*)
     209
     210(* Inversion on necessary_conditions *)
    206211lemma necessary_conditions_spec :
    207212  ∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) →
     
    219224     ]
    220225] qed.     
    221 
    222226
    223227
     
    255259].
    256260
     261(* Inversion on smaller_integer_val *)
    257262lemma smaller_integer_val_spec : ∀src_sz,dst_sz,sg,val1,val2,tr1,tr2.
    258263    smaller_integer_val src_sz dst_sz sg (OK ? 〈val1, tr1〉) (OK ? 〈val2, tr2〉) →
     
    274279          ]
    275280     ]
    276 ] qed.   
    277    
    278 definition is_integer_type ≝ λty.
    279 match ty with
    280 [ Tint _ _ ⇒ True
    281 | _ ⇒ False
    282 ].
    283 
    284 
    285 
     281] qed.
     282
     283(* Simulation relation used for expression evaluation. *)
    286284inductive simulate (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
    287285| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → simulate A r1 r2
    288286| SimFail : (∃err. r1 = Error ? err) → simulate A r1 r2.
    289287
     288(* Invariant of simplify_expr *)
    290289inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝
     290(* Inv_eq states a standard simulation result. We enforce some needed equations on types to prove the cast cases. *)
    291291| Inv_eq : ∀result_flag.
    292292     result_flag = false →
     
    295295     simulate ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) →     
    296296     simplify_inv ge en m e1 e2 target_sz target_sg result_flag
     297(* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *)
    297298| Inv_coerce_ok : ∀src_sz,src_sg.
    298299     (typeof e1) = (Tint src_sz src_sg) →
     
    300301     (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) →
    301302     simplify_inv ge en m e1 e2 target_sz target_sg true.
    302    
    303 
    304 (* This lemma proves that simplify_int actually implements an integer cast. This is central to the proof of correctness. *)
    305 (* The case 4 can be merged with cases 7 and 8.  *)
     303     
     304definition conservation ≝ λe,result:expr.
     305∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
     306                                                    ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
     307                                                    ∧ typeof e = typeof result.
     308
     309(* This lemma proves that simplify_int actually implements an integer cast. *)
     310(* The case 4 can be merged with cases 7 and 8. *)
     311
    306312lemma simplify_int_implements_cast : ∀sz,sz'.∀sg,sg'.∀i,i'. simplify_int sz sz' sg sg' i = Some ? i' → i' = cast_int_int sz sg sz' i.
    307313* *
     
    380386qed.
    381387
    382 lemma prod_eq_left:
    383   ∀A: Type[0].
    384   ∀p, q, r: A.
    385     p = q → 〈p, r〉 = 〈q, r〉.
    386   #A #p #q #r #hyp
    387   >hyp %
    388 qed.
    389 
    390 lemma prod_eq_right:
    391   ∀A: Type[0].
    392   ∀p, q, r: A.
    393     p = q → 〈r, p〉 = 〈r, q〉.
    394   #A #p #q #r #hyp
    395   >hyp %
    396 qed.
    397 
    398388corollary prod_vector_zero_eq_left:
    399389  ∀A, n.
     
    589579    //
    590580  ]
    591 qed.
    592 
    593 lemma tail_eat_cons : ∀A. ∀n. ∀hd:A. ∀v:Vector A n. tail A n (hd ::: v) = v.
    594 #A #n #hd #v normalize //
    595 qed.
    596 
    597 lemma tail_eat_pad : ∀A. ∀padelt. ∀padlen, veclen. ∀v:Vector A veclen.
    598   tail A ? (pad_vector A padelt (S padlen) veclen v) = pad_vector A padelt padlen veclen v.
    599 # A #padelt #padlen #veclen #v
    600 normalize //
    601581qed.
    602582
     
    914894 * more or less "modular", case-by-case wise.
    915895 *)
    916 let rec simplify_expr2 (e:expr) (target_sz:intsize) (target_sg:signedness)
     896let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness)
    917897  : Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝
    918898match e return λx. x = e → ? with
     
    961941            match assert_type_eq (typeof lhs) (typeof rhs) with
    962942            [ OK Htylhs_eq_tyrhs ⇒
    963                 let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr2 lhs target_sz target_sg in
    964                 let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr2 rhs target_sz target_sg in
     943                let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr lhs target_sz target_sg in
     944                let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr rhs target_sz target_sg in
    965945                match desired_type_lhs ∧ desired_type_rhs
    966946                return  λx. (desired_type_lhs ∧ desired_type_rhs) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
     
    997977          with
    998978          [ true ⇒ λHconditions.
    999               let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr2 castee target_sz target_sg in
     979              let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr castee target_sz target_sg in
    1000980              match desired_type return λx. desired_type = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))
    1001981              with
     
    1003983                «〈true, castee1〉, ?»
    1004984              | false ⇒ λHdesired_eq.
    1005                 let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr2 castee cast_sz cast_sg in
     985                let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in
    1006986                match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))
    1007987                with
     
    1013993              ] (refl ? desired_type)
    1014994          | false ⇒ λHconditions.
    1015               let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr2 castee cast_sz cast_sg in
     995              let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in
    1016996              match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))
    1017997              with
     
    10371017          match assert_type_eq (typeof iftrue) (typeof iffalse) with
    10381018          [ OK Hiftrue_eq_iffalse ⇒
    1039               let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue      ≝ simplify_expr2 iftrue target_sz target_sg in
    1040               let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr2 iffalse target_sz target_sg in         
     1019              let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue      ≝ simplify_expr iftrue target_sz target_sg in
     1020              let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr iffalse target_sz target_sg in         
    10411021              match desired_true ∧ desired_false
    10421022              return  λx. (desired_true ∧ desired_false) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
     
    10771057      match type_eq_dec ty (typeof e1) with
    10781058      [ inl Heq ⇒
    1079         let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr2 e1 target_sz target_sg in
     1059        let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr e1 target_sz target_sg in
    10801060        «〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?»
    1081       | inr Heq ⇒
     1061      | inr Hneq ⇒
    10821062        let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in
    10831063        «〈false, Expr (Ecost l e2) ty〉, ?»
     
    10891069] (refl ? e)
    10901070
    1091 and simplify_inside (e:expr) : Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
    1092                                                     ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
    1093                                                     ∧ typeof e = typeof result) ≝
     1071and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝
    10941072match e return λx. x = e → ? with
    10951073[ Expr ed ty ⇒ λHexpr_eq.
     
    11111089    match type_eq_dec ty cast_ty with
    11121090    [ inl Hcast_eq ⇒
    1113        match cast_ty return λx. x = cast_ty → Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
    1114                                                      ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
    1115                                                      ∧ typeof e = typeof result)
     1091       match cast_ty return λx. x = cast_ty → Σresult:expr. conservation e result
    11161092       with
    11171093       [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq.
    1118           let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr2 castee cast_sz cast_sg in
    1119           match success return λx. x = success → Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
    1120                                                        ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
    1121                                                        ∧ typeof e = typeof result)
     1094          let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr castee cast_sz cast_sg in
     1095          match success return λx. x = success → Σresult:expr. conservation e result
    11221096         with
    11231097         [ true ⇒ λHsuccess_eq.
     
    11561130] (refl ? e).
    11571131#ge #en #m
    1158 [ 1,3,5,6,7,8,9,10,11,12: %1 //
     1132[ 1,3,5,6,7,8,9,10,11,12: %1 try @refl
    11591133     cases (exec_expr ge en m e) #res
    11601134     try (@(SimOk ???) //)
    11611135| 13,14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
    11621136     try (@(SimOk ???) //)
    1163 | 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct //
     1137| 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/
    11641138     whd in match (exec_expr ????); >eq_intsize_identity whd
    1165      >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ]     
    1166 | 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) //
     1139     >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ]
     1140| 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/
    11671141     whd in match (exec_expr ????);
    11681142     whd in match (exec_expr ????);
    11691143     >eq_intsize_identity >eq_intsize_identity whd
    1170      >sz_eq_identity >sz_eq_identity whd @conj try @conj //     
     1144     >sz_eq_identity >sz_eq_identity whd @conj try @conj try @refl     
    11711145     [ 1: @(simplify_int_implements_cast … Hsimpl_eq)
    11721146     | 2: @(simplify_int_success_lt … Hsimpl_eq) ]
    1173 | 15: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
     1147| 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    11741148    [ 1: (* Proving preservation of the semantics for expressions. *)
    11751149      cases Hexpr_sim
    11761150      [ 2: (* Case where the evaluation of e1 as an expression fails *)     
    1177         normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2/
     1151        normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/
    11781152      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
    11791153        #Hsim %1 * #val #trace normalize #Hstep
     
    12051179      cases Hexpr_sim
    12061180      [ 2: (* Case where the evaluation of e1 as an lvalue fails *)
    1207         normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2/
     1181        normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/
    12081182      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
    12091183        #Hsim %1 * * #block #offset #trace normalize #Hstep       
     
    12281202     ]
    12291203   ]
    1230 | 16: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
     1204| 16: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    12311205    [ 1: (* Proving preservation of the semantics for expressions. *)
    12321206      cases Hlvalue_sim
    12331207      [ 2: (* Case where the evaluation of e1 as an expression fails *)     
    1234         * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2/
     1208        * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2 by ex_intro/
    12351209      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
    12361210        #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep
     
    12541228        | 2: * #block * #offset * #region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat #Hty_eq #Hval_eq
    12551229             whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta
    1256              >Hptr_compat normalize nodelta //
     1230             >Hptr_compat //
    12571231        ]
    12581232     ]
    1259    | 2: (* Proving preservation of the semantics of lvalues. *)
    1260       normalize @SimFail /2/
    1261    ]
    1262 | 17: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
     1233    | 2: (* Proving preservation of the semantics of lvalues. *)
     1234         @SimFail /2 by ex_intro/
     1235    ]
     1236| 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    12631237      [ 1: whd in match (exec_expr ge en m (Expr ??));
    12641238           whd in match (exec_expr ge en m (Expr ??));
    12651239           cases Hexpr_sim           
    1266            [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2/
     1240           [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2 by ex_intro/
    12671241           | 1: cases (exec_expr ge en m e1)
    1268                 [ 2: #error #Hexec normalize nodelta @SimFail /2/
     1242                [ 2: #error #Hexec normalize nodelta @SimFail /2 by ex_intro/
    12691243                | 1: * #val #trace #Hexec
    12701244                     >(Hexec ? (refl ? (OK ? 〈val,trace〉)))
     
    12721246                ]
    12731247           ]
    1274       | 2: normalize @SimFail /2/
    1275       ]   
     1248      | 2: @SimFail /2 by ex_intro/
     1249      ]
    12761250| 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq
    12771251      inversion (Hinv_lhs ge en m)
     
    12901264                     (* Enumerate all the cases for the evaluation of the source expressions ... *)
    12911265                     cases (exec_expr ge en m lhs) in Hsmaller_lhs;
    1292                      [ 2: #error normalize //
     1266                     [ 2: #error //
    12931267                     | 1: * #val_lhs #trace_lhs normalize nodelta cases (exec_expr ge en m lhs1)
    1294                           [ 2: #error normalize #H @(False_ind … H)
     1268                          [ 2: #error #H @(False_ind … H)
    12951269                          | 1: * #val_lhs1 #trace_lhs1 #Hsmaller_lhs
    12961270                               elim (smaller_integer_val_spec … Hsmaller_lhs)
    12971271                               #lhs_int * #lhs1_int * * * * #Hval_lhs #Hval_lhs1 #Hlhs_cast #Hlhs_trace #Hlhs_size
    12981272                               cases (exec_expr ge en m rhs) in Hsmaller_rhs;
    1299                                [ 2: #error normalize //
     1273                               [ 2: #error //
    13001274                               | 1: * #val_rhs #trace_rhs normalize nodelta cases (exec_expr ge en m rhs1)
    1301                                     [ 2: #error normalize #H @(False_ind … H)
     1275                                    [ 2: #error #H @(False_ind … H)
    13021276                                    | 1: * #val_rhs1 #trace_rhs1 #Hsmaller_rhs
    13031277                                         elim (smaller_integer_val_spec … Hsmaller_rhs)
     
    13241298                                             >sz_eq_identity >sz_eq_identity normalize nodelta
    13251299                                             try @conj try @conj try //
    1326                                              >integer_add_cast_le //                                            
     1300                                             >integer_add_cast_le //                                     
    13271301                                         | 2: #_ (* subtraction case *)
    13281302                                             >Hval_lhs >Hval_rhs destruct       
     
    13441318                 ]
    13451319             ]
    1346 | 19,20,21,22: destruct %1 //
     1320| 19,20,21,22: destruct %1 try @refl
    13471321   elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs
    13481322   elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs
     
    13521326      [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
    13531327      | *: cases (exec_expr ge en m lhs)
    1354            [ 2,4,6,8: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
    1355            | *: * #lval #ltrace #Hsim_lhs normalize nodelta          
     1328           [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/
     1329           | *: * #lval #ltrace #Hsim_lhs normalize nodelta         
    13561330                cases Hexpr_sim_rhs
    13571331                [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
    13581332                | *: cases (exec_expr ge en m rhs)
    1359                      [ 2,4,6,8: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
     1333                     [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/
    13601334                     | *: * #rval #rtrace #Hsim_rhs
    13611335                          whd in match (exec_expr ??? (Expr (Ebinop ???) ?));
     
    13691343           ]
    13701344      ]
    1371    | *: normalize @SimFail /2 by refl, ex_intro/ 
     1345   | *: @SimFail /2 by refl, ex_intro/ 
    13721346   ]
    13731347(* Jump to the cast cases *)   
     
    14001374            ]   
    14011375      ]
    1402   | 2,4,6,8,10,12,14,16: destruct normalize @SimFail /2/
     1376  | 2,4,6,8,10,12,14,16: destruct  @SimFail /2 by refl, ex_intro/
    14031377  ]
    14041378| 24: destruct inversion (Hcastee_inv ge en m)
     
    14121386            (* Simplify the goal by culling impossible cases, using Hsmaller_val *)
    14131387            cases (exec_expr ge en m castee) in Hsmaller_eval;
    1414             [ 2: #error normalize //
     1388            [ 2: #error //
    14151389            | 1: * #castee_val #castee_trace cases (exec_expr ge en m castee1)
    1416               [ 2: #error normalize #Hcontr @(False_ind … Hcontr)
     1390              [ 2: #error #Hcontr @(False_ind … Hcontr)
    14171391              | 1: * #castee1_val #castee1_trace #Hsmaller
    14181392                   elim (smaller_integer_val_spec … Hsmaller)
     
    14431417           #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq
    14441418           @(Inv_eq ???????) //
    1445            [ 1,4: >Htype_castee2 normalize //
     1419           [ 1,4: >Htype_castee2 //
    14461420           | 2,5: (* Prove simulation for exec_expr *)
    14471421               whd in match (exec_expr ??? (Expr ??));
    14481422               cases (exec_expr ge en m castee) in Hsmaller_eval;
    14491423               [ 2,4: (* erroneous evaluation of the original expression *)
    1450                      #error #Hsmaller_eval @SimFail @(ex_intro … error)
    1451                      normalize nodelta //
     1424                     #error #Hsmaller_eval @SimFail @(ex_intro … error) //
    14521425               | 1,3: * #val #trace
    14531426                    cases (exec_expr ge en m castee2)
     
    14671440                    ]
    14681441              ]
    1469          | 3,6: normalize @SimFail /2/
     1442         | 3,6:  @SimFail /2 by refl, ex_intro/
    14701443         ]
    14711444    ]
     
    14941467                      ]
    14951468                 ]
    1496             | 2,4: normalize @SimFail /2/
     1469            | 2,4: @SimFail /2 by refl, ex_intro/
    14971470            ]
    14981471      ]
     
    15021475      whd in match (exec_expr ??? (Expr ??));
    15031476      [ 1: cases Hsim_expr
    1504            [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2/
     1477           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/
    15051478           | 1: #Hexec_ok @SimOk * #val #trace
    15061479                cases (exec_expr ge en m castee) in Hexec_ok;
     
    15121485                ]
    15131486           ]
    1514       | 2: normalize @SimFail /2/
     1487      | 2: @SimFail /2 by refl, ex_intro/
    15151488      ]
    15161489| 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq
     
    15241497           | 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false
    15251498                >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg)
    1526                 [ 1,2: normalize //
     1499                [ 1,2: //
    15271500                | 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??));
    15281501                     elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq
     
    15321505                          [ 2: #error #_ normalize @I
    15331506                          | 1: * #cond_val #cond_trace #Hcond_sim
    1534                                >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
    1535                                
     1507                               >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))                               
    15361508                               normalize nodelta
    15371509                               >Htype_cond_eq
     
    16341606                ]
    16351607            ]
    1636    | 2,4,6: normalize @SimFail /2 by ex_intro/           
     1608   | 2,4,6: @SimFail /2 by ex_intro/           
    16371609   ]
    16381610| 41,42: destruct
     
    16681640                         ]
    16691641                      ]
    1670             ]
    1671          ]
    1672    | 2,4: normalize @SimFail /2 by ex_intro/
     1642              ]
     1643          ]
     1644   | 2,4: @SimFail /2 by ex_intro/
    16731645   ]
    16741646| 43: destruct
     
    17661738      | 2: @SimFail /2 by ex_intro/ ]
    17671739(* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls
    1768  * simplify_expr2 *)     
     1740 * simplify_expr *)     
    17691741| 47, 48, 49: (* trivial const_int, const_float and var cases *)
    17701742  try @conj try @conj try @refl
     
    20221994   | 3: //
    20231995   ]
    2024 ] qed.   
    2025 
    2026 
    2027 (* simplify_expr [e] [ty'] takes an expression e and a desired type ty', and
    2028    returns a flag stating whether the desired type was achieved and a simplified
    2029    version of e. *)
    2030 let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝
    2031 match e with
    2032 [ Expr ed ty ⇒
    2033   match ed with
    2034   [ Econst_int sz i ⇒
    2035     match ty with
    2036     [ Tint ty_sz sg ⇒
    2037       match ty' with
    2038       [ Tint sz' sg' ⇒
    2039         (* IG: checking that the displayed type size [ty_sz] and [sz] are equal ... *)
    2040         match sz_eq_dec sz ty_sz with
    2041         [ inl Heq ⇒
    2042           match simplify_int sz sz' sg sg' i with
    2043           [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉
    2044           | None ⇒ 〈false, e〉
    2045           ]
    2046         | inr _ ⇒
    2047           (* The expression is ill-typed. *)
    2048           〈false, e〉
    2049         ]
    2050       | _ ⇒ 〈false, e〉 ]
    2051     | _ ⇒ 〈false, e〉 ]
    2052   | Ederef e1 ⇒
    2053       let ty1 ≝ typeof e1 in
    2054       〈type_eq ty ty',Expr (Ederef (\snd (simplify_expr e1 ty1))) ty〉
    2055   | Eaddrof e1 ⇒
    2056       let ty1 ≝ typeof e1 in
    2057       〈type_eq ty ty',Expr (Eaddrof (\snd (simplify_expr e1 ty1))) ty〉
    2058   | Eunop op e1 ⇒
    2059       let ty1 ≝ typeof e1 in
    2060       〈type_eq ty ty',Expr (Eunop op (\snd (simplify_expr e1 ty1))) ty〉
    2061   | Ebinop op e1 e2 ⇒
    2062       if binop_simplifiable op then
    2063         let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty' in
    2064         let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in
    2065         if desired_type1 ∧ desired_type2 then
    2066           〈true, Expr (Ebinop op e1' e2') ty'〉
    2067         else
    2068           let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
    2069           let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
    2070             〈false, Expr (Ebinop op e1' e2') ty〉
    2071       else
    2072         let 〈desired_type1, e1'〉 ≝ simplify_expr e1 (typeof e1) in
    2073         let 〈desired_type2, e2'〉 ≝ simplify_expr e2 (typeof e2) in
    2074           〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉
    2075   | Ecast ty e1 ⇒
    2076       match inttype_compare ty' ty with
    2077       [ itc_le ⇒
    2078         let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in
    2079         if desired_type then 〈true, e1'〉 else
    2080           let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in
    2081           if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉
    2082       | itc_no ⇒
    2083         let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in
    2084         if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉
    2085       ]
    2086   | Econdition e1 e2 e3 ⇒
    2087       let 〈irrelevant, e1'〉 ≝ simplify_expr e1 (typeof e1) in (* TODO try to reduce size *)
    2088       let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in
    2089       let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty' in
    2090       if desired_type2 ∧ desired_type3 then
    2091         〈true, Expr (Econdition e1' e2' e3') ty'〉
    2092       else
    2093         let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
    2094         let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty in
    2095           〈false, Expr (Econdition e1' e2' e3') ty〉
    2096     (* Could probably do better with these, too. *)
    2097   | Eandbool e1 e2 ⇒
    2098       let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
    2099       let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
    2100         〈type_eq ty ty', Expr (Eandbool e1' e2') ty〉
    2101   | Eorbool e1 e2 ⇒
    2102       let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
    2103       let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
    2104         〈type_eq ty ty', Expr (Eorbool e1' e2') ty〉
    2105   (* Could also improve Esizeof *)
    2106   | Efield e1 f ⇒
    2107       let ty1 ≝ typeof e1 in
    2108       〈type_eq ty ty',Expr (Efield (\snd (simplify_expr e1 ty1)) f) ty〉
    2109   | Ecost l e1 ⇒
    2110       let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in
    2111         〈desired_type, Expr (Ecost l e1') (typeof e1')〉
    2112   | _ ⇒ 〈type_eq ty ty',e〉
    2113   ]
    2114 ].
    2115 
    2116 definition simplify_e ≝ λe. \snd (simplify_expr e (typeof e)).
     1996] qed.
     1997
     1998(* Propagate cast simplification through statements and programs. *)
     1999
     2000definition simplify_e ≝ λe. pi1 … (simplify_inside e).
    21172001
    21182002let rec simplify_statement (s:statement) : statement ≝
     
    21522036λp. transform_program … p simplify_fundef.
    21532037
    2154 
    2155 (* We have to prove that simplify_expr doesn't alter the semantics. Since expressions are pure,
    2156  * we state that expressions before and after conversion should evaluate to the same value, or
    2157  * fail in a similar way when placed into a given context. *)
    2158 
    2159 
    2160 let rec expr_ind2
    2161     (P : expr → Prop) (Q : expr_descr → Prop)
    2162     (IE : ∀ed. ∀t. Q ed → P (Expr ed t))
    2163     (Iconst_int : ∀sz, i. Q (Econst_int sz i))
    2164     (Iconst_float : ∀f. Q (Econst_float f))
    2165     (Ivar : ∀id. Q (Evar id))
    2166     (Ideref : ∀e. P e → Q (Ederef e))
    2167     (Iaddrof : ∀e. P e → Q (Eaddrof e))
    2168     (Iunop : ∀op,arg. P arg → Q (Eunop op arg))
    2169     (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2))
    2170     (Icast : ∀t. ∀e . P e →  Q (Ecast t e))
    2171     (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3))
    2172     (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2))
    2173     (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2))
    2174     (Isizeof : ∀t. Q (Esizeof t))
    2175     (Ifield : ∀e,f. P e → Q (Efield e f))
    2176     (Icost : ∀c,e. P e → Q (Ecost c e))
    2177     (e : expr) on e : P e ≝
    2178 match e with
    2179 [ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed) ]
    2180 
    2181 and expr_desc_ind2
    2182     (P : expr → Prop) (Q : expr_descr → Prop)
    2183     (IE : ∀ed. ∀t. Q ed → P (Expr ed t))
    2184     (Iconst_int : ∀sz, i. Q (Econst_int sz i))
    2185     (Iconst_float : ∀f. Q (Econst_float f))
    2186     (Ivar : ∀id. Q (Evar id))
    2187     (Ideref : ∀e. P e → Q (Ederef e))
    2188     (Iaddrof : ∀e. P e → Q (Eaddrof e))
    2189     (Iunop : ∀op,arg. P arg → Q (Eunop op arg))
    2190    
    2191     (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2))
    2192     (Icast : ∀t. ∀e . P e →  Q (Ecast t e))
    2193     (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3))
    2194     (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2))
    2195     (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2))
    2196     (Isizeof : ∀t. Q (Esizeof t))
    2197     (Ifield : ∀e,f. P e → Q (Efield e f))
    2198     (Icost : ∀c,e. P e → Q (Ecost c e))
    2199     (ed : expr_descr) on ed : Q ed ≝
    2200 match ed with
    2201 [ Econst_int sz i ⇒ Iconst_int sz i
    2202 | Econst_float f ⇒ Iconst_float f
    2203 | Evar id ⇒ Ivar id
    2204 | Ederef e ⇒ Ideref e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    2205 | Eaddrof e ⇒ Iaddrof e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    2206 | Eunop op e ⇒ Iunop op e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    2207 | Ebinop op e1 e2 ⇒ Ibinop op e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
    2208 | Ecast t e ⇒ Icast t e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    2209 | Econdition e1 e2 e3 ⇒ Icond e1 e2 e3  (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e3)
    2210 | Eandbool e1 e2 ⇒ Iandbool e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
    2211 | Eorbool e1 e2 ⇒ Iorbool e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
    2212 | Esizeof t ⇒ Isizeof t
    2213 | Efield e field ⇒ Ifield e field (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    2214 | Ecost c e ⇒ Icost c e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof
     2038(* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *)
     2039inductive cont_cast : cont → cont → Prop ≝
     2040| cc_stop : cont_cast Kstop Kstop
     2041| cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k')
     2042| cc_while : ∀e,s,k,k'.
     2043    cont_cast k k' →
     2044    cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k')
     2045| cc_dowhile : ∀e,s,k,k'.
     2046    cont_cast k k' →
     2047    cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k')
     2048| cc_for1 : ∀e,s1,s2,k,k'.
     2049    cont_cast k k' →
     2050    cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k')
     2051| cc_for2 : ∀e,s1,s2,k,k'.
     2052    cont_cast k k' →
     2053    cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
     2054| cc_for3 : ∀e,s1,s2,k,k'.
     2055    cont_cast k k' →
     2056    cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
     2057| cc_switch : ∀k,k'.
     2058    cont_cast k k' → cont_cast (Kswitch k) (Kswitch k')
     2059| cc_call : ∀r,f,en,k,k'.
     2060    cont_cast k k' →
     2061    cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k').
     2062(* wtf
     2063| cc_seqls : ∀ls,k,k'. cont_cast k k' →
     2064    cont_cast (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (simplify_ls ls)) k').
     2065*)
     2066
     2067lemma call_cont_cast : ∀k,k'.
     2068  cont_cast k k' →
     2069  cont_cast (call_cont k) (call_cont k').
     2070#k0 #k0' #K elim K /2/
     2071qed.
     2072
     2073inductive state_cast : state → state → Prop ≝
     2074| swc_state : ∀f,s,k,k',e,m.
     2075  cont_cast k k' →
     2076  state_cast (State f s k e m) (State (simplify_function f) (simplify_statement s ) k' e m)
     2077| swc_callstate : ∀fd,args,k,k',m.
     2078  cont_cast k k' → state_cast (Callstate fd args k m) (Callstate (simplify_fundef fd) args k' m)
     2079| swc_returnstate : ∀res,k,k',m.
     2080  cont_cast k k' → state_cast (Returnstate res k m) (Returnstate res k' m)
     2081| swc_finalstate : ∀r.
     2082  state_cast (Finalstate r) (Finalstate r)
     2083.
     2084
     2085record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
     2086  rg_find_symbol: ∀s.
     2087    find_symbol ? ge s = find_symbol ? ge' s;
     2088  rg_find_funct: ∀v,f.
     2089    find_funct ? ge v = Some ? f →
     2090    find_funct ? ge' v = Some ? (t f);
     2091  rg_find_funct_ptr: ∀b,f.
     2092    find_funct_ptr ? ge b = Some ? f →
     2093    find_funct_ptr ? ge' b = Some ? (t f)
     2094}.
     2095
     2096(* The return type of any function is invariant under cast simplification *)
     2097lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f.
     2098// qed.
     2099
     2100include "CexecSound.ma".
     2101
     2102definition expr_lvalue_ind_combined ≝
     2103λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
     2104conj ??
     2105 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
     2106 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
     2107 
     2108lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulate A r0 r2.
     2109#A #r0 #r1 #r2 *
     2110[ 2: * #error #H >H #_ @SimFail /2 by ex_intro/
     2111| 1: cases r0
     2112     [ 2: #error #_ #_ @SimFail /2 by ex_intro/
     2113     | 1: #elt #Hsim lapply (Hsim elt (refl ? (OK ? elt))) #H >H // ]
     2114] qed.
     2115
     2116lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' →
     2117  (∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
     2118  (∀ed, ty. simulate ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
     2119#ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined
     2120[ 1: #sz #ty #i @SimOk #a normalize //
     2121| 2: #ty #f @SimOk #a normalize //
     2122| 3: *
     2123    [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
     2124    | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2125    #ty #Hsim_lvalue try //
     2126    whd in match (Plvalue ???);
     2127    whd in match (exec_expr ????);
     2128    whd in match (exec_expr ????);
     2129    cases Hsim_lvalue
     2130    [ 2,4,6: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
     2131    | *: cases (exec_lvalue' ge en m ? ty)
     2132         [ 2,4,6: #error #_ @SimFail /2 by ex_intro/
     2133         | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2134              @SimOk // ]
     2135    ]
     2136| 4: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
     2137     cases (lookup SymbolTag block en v) normalize nodelta
     2138     [ 2: #block @SimOk //
     2139     | 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk //
     2140     ]
     2141| 5: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
     2142     cases Hsim_expr
     2143     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2144     | 1: cases (exec_expr ge en m e)
     2145          [ 2: #error #_ @SimFail /2 by ex_intro/
     2146          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2147                @SimOk // ]
     2148     ]
     2149| 6: #ty #ed #ty' #Hsim_lvalue
     2150     whd in match (exec_expr ????); whd in match (exec_expr ????);
     2151     whd in match (exec_lvalue ????); whd in match (exec_lvalue ????);
     2152     cases Hsim_lvalue
     2153     [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
     2154     | 1: cases (exec_lvalue' ge en m ed ty')
     2155         [ 2: #error #_ @SimFail /2 by ex_intro/
     2156         | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2157              @SimOk // ]
     2158    ]
     2159| 7: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     2160     cases Hsim
     2161     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2162     | 1: cases (exec_expr ge en m e)
     2163          [ 2: #error #_ @SimFail /2 by ex_intro/
     2164          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2165               @SimOk // ]
     2166     ]
     2167| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     2168     cases Hsim1
     2169     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2170     | 1: cases (exec_expr ge en m e1)
     2171          [ 2: #error #_ @SimFail /2 by ex_intro/
     2172          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2173               cases Hsim2
     2174               [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2175               | 1: cases (exec_expr ge en m e2)
     2176                    [ 2: #error #_ @SimFail /2 by ex_intro/
     2177                    | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2178                         @SimOk // ]
     2179               ]
     2180          ]
     2181     ]
     2182| 9: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     2183     cases Hsim
     2184     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2185     | 1: cases (exec_expr ge en m e)
     2186          [ 2: #error #_ @SimFail /2 by ex_intro/
     2187          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2188               @SimOk // ]
     2189     ] (* mergeable with 7 modulo intros *)
     2190| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     2191     cases Hsim1
     2192     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2193     | 1: cases (exec_expr ge en m e1)
     2194          [ 2: #error #_ @SimFail /2 by ex_intro/
     2195          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta
     2196               cases (exec_bool_of_val (\fst a) (typeof e1))
     2197               [ 2: #error @SimFail /2 by ex_intro/
     2198               | 1: *
     2199                    [ 1: (* true branch *) cases Hsim2
     2200                    | 2: (* false branch *) cases Hsim3 ]
     2201                    [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2202                    | 1: cases (exec_expr ge en m e2) | 3: cases (exec_expr ge en m e3) ]
     2203                    [ 2,4: #error #_ @SimFail /2 by ex_intro/
     2204                    | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ]
     2205              ]
     2206          ]
     2207     ]
     2208| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     2209     cases Hsim1
     2210     [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2211     | 1,3: cases (exec_expr ge en m e1)
     2212          [ 2,4: #error #_ @SimFail /2 by ex_intro/
     2213          | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta
     2214                 cases (exec_bool_of_val ??)
     2215                 [ 2,4: #erro @SimFail /2 by ex_intro/
     2216                 | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????);
     2217                        [ 2,3: @SimOk //
     2218                        | 1,4: cases Hsim2
     2219                               [ 2,4: * #error #Hfail >Hfail normalize nodelta @SimFail /2 by ex_intro/
     2220                               | 1,3: cases (exec_expr ge en m e2)
     2221                                      [ 2,4: #error #_ @SimFail /2 by ex_intro/
     2222                                      | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2223                                           @SimOk // ]
     2224                               ]
     2225                        ]
     2226                ]
     2227          ]
     2228     ]
     2229| 13: #ty #sizeof_ty @SimOk normalize //
     2230| 14: #ty #e #ty' #field #Hsim_lvalue
     2231      whd in match (exec_lvalue' ? en m (Efield ??) ty);
     2232      whd in match (exec_lvalue' ge' en m (Efield ??) ty);
     2233      normalize in match (typeof (Expr ??));
     2234      cases ty' in Hsim_lvalue; normalize nodelta
     2235      [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
     2236      | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
     2237      #Hsim_lvalue
     2238      try (@SimFail /2 by ex_intro/)
     2239      normalize in match (exec_lvalue ge en m ?);
     2240      normalize in match (exec_lvalue ge' en m ?);
     2241      cases Hsim_lvalue
     2242      [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2243      | 1,3: cases (exec_lvalue' ge en m e ?)
     2244             [ 2,4: #error #_ @SimFail /2 by ex_intro/
     2245             | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2246                    @SimOk /2 by ex_intro/ ]
     2247      ]
     2248| 15: #ty #lab #e #Hsim
     2249      whd in match (exec_expr ??? (Expr ??));
     2250      whd in match (exec_expr ??? (Expr ??));
     2251      cases Hsim
     2252     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2253     | 1: cases (exec_expr ge en m e)
     2254          [ 2: #error #_ @SimFail /2 by ex_intro/
     2255          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2256               @SimOk // ]
     2257     ] (* cf case 7, again *)
     2258| 16: *
     2259      [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
     2260      | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2261      #ty normalize in match (is_not_lvalue ?);
     2262      [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_
     2263      @SimFail /2 by ex_intro/
     2264] qed.
     2265
     2266lemma related_globals_expr_simulation : ∀ge,ge',en,m.
     2267  related_globals ? simplify_fundef ge ge' →
     2268  ∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧
     2269      typeof e = typeof (simplify_e e).
     2270#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
     2271cases e #ed #ty cases ed
     2272[ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
     2273| 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2274elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
     2275* * try //
     2276cases (exec_expr ge en m (Expr ??))
     2277try (#error #_ #_ #_ @SimFail /2 by ex_intro/)
     2278* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
     2279try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?))
     2280qed.
     2281
     2282lemma related_globals_lvalue_simulation : ∀ge,ge',en,m.
     2283  related_globals ? simplify_fundef ge ge' →
     2284  ∀e. simulate ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧
     2285      typeof e = typeof (simplify_e e).
     2286#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
     2287cases e #ed #ty cases ed
     2288[ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
     2289| 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2290elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
     2291* * try //
     2292cases (exec_lvalue ge en m (Expr ??))
     2293try (#error #_ #_ #_ @SimFail /2 by ex_intro/)
     2294* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
     2295(* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *)
     2296cases e' in Hsim_lvalue ⊢ %; #ed' #ty' whd in match (exec_lvalue ????); whd in match (exec_lvalue ????);
     2297lapply (proj2 ?? (sim_related_globals ge ge' en m Hrelated) ed' ty') #Hsim_lvalue2 #Hsim_lvalue1
     2298try @(simulation_transitive ???? Hsim_lvalue1 Hsim_lvalue2)
     2299qed.
     2300
     2301lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
     2302related_globals ? simplify_fundef ge ge' →
     2303∀args. simulate ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).
     2304#ge #ge' #en #m #Hrelated #args
     2305elim args
     2306[ 1: /3/
     2307| 2: #hd #tl #Hind normalize
     2308     elim (related_globals_expr_simulation ge ge' en m Hrelated hd)
     2309     *
     2310     [ 2: * #error #Hfail >Hfail #_ @SimFail /2 by refl, ex_intro/
     2311     | 1: cases (exec_expr ge en m hd)
     2312          [ 2: #error #_ #_ @SimFail /2 by refl, ex_intro/
     2313          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq
     2314               cases Hind normalize
     2315               [ 2: * #error #Hfail >Hfail @SimFail /2 by refl, ex_intro/
     2316               | 1: cases (exec_exprlist ??? tl)
     2317                    [ 2: #error #_ @SimFail /2 by refl, ex_intro/
     2318                    | 1: * #values #trace #Hsim lapply (Hsim 〈values, trace〉 (refl ? (OK ? 〈values, trace〉)))
     2319                         #Heq >Heq @SimOk // ]
     2320               ]
     2321          ]
     2322     ]
     2323] qed.
     2324
     2325lemma simplify_type_of_fundef_eq : ∀clfd. (type_of_fundef (simplify_fundef clfd)) = (type_of_fundef clfd).
     2326* // qed.
     2327
     2328lemma simplify_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. typeof (simplify_e func) = typeof func.
     2329#ge #en #m #func whd in match (simplify_e func); elim (simplify_inside func)
     2330#func' #H lapply (H ge en m) * * #_ #_ //
     2331qed.
     2332
     2333lemma simplify_fun_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. fun_typeof (simplify_e func) = fun_typeof func.
     2334#ge #en #m #func whd in match (simplify_e func); whd in match (fun_typeof ?) in ⊢ (??%%);
     2335>simplify_typeof_eq whd in match (simplify_e func); // qed.
     2336
     2337lemma simplify_is_not_skip: ∀s.s ≠ Sskip → ∃pf. is_Sskip (simplify_statement s) = inr … pf.
     2338*
     2339[ 1: * #Habsurd elim (Habsurd (refl ? Sskip))
     2340| *: #a try #b try #c try #d try #e
     2341     whd in match (simplify_statement ?);
     2342     whd in match (is_Sskip ?);
     2343     try /2 by refl, ex_intro/
     2344] qed.
     2345
     2346lemma call_cont_simplify : ∀k,k'.
     2347  cont_cast k k' →
     2348  cont_cast (call_cont k) (call_cont k').
     2349#k0 #k0' #K elim K /2/
     2350qed.
     2351
     2352lemma simplify_ls_commute : ∀l. (simplify_statement (seq_of_labeled_statement l)) = (seq_of_labeled_statement (simplify_ls l)).
     2353#l @(labeled_statements_ind … l)
     2354[ 1: #default_statement //
     2355| 2: #sz #i #s #tl #Hind
     2356     whd in match (seq_of_labeled_statement ?) in ⊢ (??%?);
     2357     whd in match (simplify_ls ?) in ⊢ (???%);
     2358     whd in match (seq_of_labeled_statement ?) in ⊢ (???%);
     2359     whd in match (simplify_statement ?) in ⊢ (??%?);
     2360     >Hind //
     2361] qed.
     2362
     2363lemma select_switch_commute : ∀sz,i,l.
     2364 select_switch sz i (simplify_ls l) = simplify_ls (select_switch sz i l).
     2365#sz #i #l @(labeled_statements_ind … l)
     2366[ 1: #default_statement //
     2367| 2: #sz' #i' #s #tl #Hind
     2368     whd in match (simplify_ls ?) in ⊢ (??%?);
     2369     whd in match (select_switch ???) in ⊢ (??%%);
     2370     cases (sz_eq_dec sz sz')
     2371     [ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true
     2372           cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta
     2373           whd in match (simplify_ls ?) in ⊢ (???%);
     2374           [ 1: // | 2: @Hind ]
     2375     | 2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq)
     2376          @Hind
     2377     ]
     2378] qed.
     2379
     2380lemma invoke_cthulhu :
     2381  ∀lab. ∀s:statement.∀k,k'. cont_cast k k' →
     2382  ∀Hind:(∀k:cont.∀k':cont.
     2383          cont_cast k k' →
     2384          match find_label lab s k with 
     2385          [ None ⇒ find_label lab (simplify_statement s) k'=None (statement×cont)
     2386          | Some (r:(statement×cont))⇒
     2387            let 〈s',ks〉 ≝r in 
     2388            ∃ks':cont. find_label lab (simplify_statement s) k' = Some (statement×cont) 〈simplify_statement s',ks'〉
     2389                        ∧ cont_cast ks ks']).
     2390  (find_label lab s k = None ? ∧ find_label lab (simplify_statement s) k' = None ?) ∨
     2391  (∃st,kst,kst'. find_label lab s k = Some ? 〈st,kst〉 ∧ find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement st,kst'〉 ∧ cont_cast kst kst').
     2392#lab #s #k #k' #Hcont_cast #Hind
     2393lapply (Hind k k' Hcont_cast)
     2394cases (find_label lab s k)
     2395[ 1: normalize nodelta #Heq >Heq /3/
     2396| 2: * #st #kst normalize nodelta * #kst' * #Heq #Hcont_cast' >Heq %2
     2397     %{st} %{kst} %{kst'} @conj try @conj //
     2398] qed.
     2399
     2400
     2401lemma cast_find_label : ∀lab,s,k,k'.
     2402  cont_cast k k' →
     2403  match find_label lab s k with
     2404  [ Some r ⇒
     2405    let 〈s',ks〉 ≝ r in
     2406    ∃ks'. find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement s', ks'〉
     2407    ∧ cont_cast ks ks'
     2408  | None ⇒
     2409    find_label lab (simplify_statement s) k' = None ?
     2410  ].
     2411#lab #s @(statement_ind2 ? (λls.
     2412    ∀k:cont
     2413    .∀k':cont
     2414     .cont_cast k k'
     2415      →match find_label_ls lab ls k with 
     2416       [None⇒
     2417        find_label_ls lab (simplify_ls ls) k' = None ?
     2418       |Some r ⇒
     2419        let 〈s',ks〉 ≝r in 
     2420        ∃ks':cont
     2421        .find_label_ls lab (simplify_ls ls) k'
     2422         =Some (statement×cont) 〈simplify_statement s',ks'〉
     2423         ∧cont_cast ks ks']
     2424) … s)
     2425[ 1: #k #k' #Hcont_cast
     2426     whd in match (find_label ? Sskip ?); normalize nodelta @refl
     2427| 2: #e1 #e2 #k #k' #Hcont_cast
     2428     whd in match (find_label ? (Sassign e1 e2) ?); normalize nodelta @refl
     2429| 3: #e0 #e #args #k #k' #Hcont_cast
     2430     whd in match (find_label ? (Scall e0 e args) ?); normalize nodelta @refl
     2431| 4: #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast
     2432     whd in match (find_label ? (Ssequence s1 s2) ?);
     2433     whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?);
     2434     elim (invoke_cthulhu lab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1)
     2435     [ 3: try ( @cc_seq // )
     2436     | 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2437          normalize nodelta %{kst'} /2/
     2438     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
     2439          elim (invoke_cthulhu lab s2 k k' Hcont_cast Hind_s2)
     2440          [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
     2441               normalize nodelta %{kst'} /2/
     2442          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     2443     ] ] 
     2444| 5: #e #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast
     2445     whd in match (find_label ???);
     2446     whd in match (find_label ? (simplify_statement ?) ?);
     2447     elim (invoke_cthulhu lab s1 k k' Hcont_cast Hind_s1)
     2448     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2449          normalize nodelta %{kst'} /2/
     2450     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
     2451          elim (invoke_cthulhu lab s2 k k' Hcont_cast Hind_s2)
     2452          [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
     2453               normalize nodelta %{kst'} /2/
     2454          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     2455     ] ]
     2456| 6: #e #s #Hind_s #k #k' #Hcont_cast
     2457     whd in match (find_label ???);
     2458     whd in match (find_label ? (simplify_statement ?) ?);
     2459     elim (invoke_cthulhu lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
     2460     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2461          normalize nodelta %{kst'} /2/
     2462     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     2463     | 3: @cc_while // ]
     2464| 7: #e #s #Hind_s #k #k' #Hcont_cast
     2465     whd in match (find_label ???);
     2466     whd in match (find_label ? (simplify_statement ?) ?);
     2467     elim (invoke_cthulhu lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
     2468     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2469          normalize nodelta %{kst'} /2/
     2470     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     2471     | 3: @cc_dowhile // ]
     2472| 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast     
     2473     whd in match (find_label ???);
     2474     whd in match (find_label ? (simplify_statement ?) ?);
     2475     elim (invoke_cthulhu lab s1
     2476               (Kseq (Sfor Sskip cond s2 s3) k)
     2477               (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k')
     2478               ? Hind_s1)
     2479     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2480          normalize nodelta %{kst'} /2/
     2481     | 3: @cc_for1 //
     2482     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
     2483          elim (invoke_cthulhu lab s3
     2484                    (Kfor2 cond s2 s3 k)
     2485                    (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
     2486                      ? Hind_s3)
     2487          [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2488                normalize nodelta %{kst'} /2/
     2489          | 3: @cc_for2 //
     2490          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
     2491               elim (invoke_cthulhu lab s2
     2492                         (Kfor3 cond s2 s3 k)
     2493                         (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
     2494                           ? Hind_s2)
     2495               [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2496                    normalize nodelta %{kst'} /2/
     2497               | 3: @cc_for3 //
     2498               | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     2499    ] ] ]
     2500| 9,10: #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta //
     2501| 11: #e #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta //
     2502| 12: #e #ls #Hind #k #k' #Hcont_cast
     2503     whd in match (find_label ???);
     2504     whd in match (find_label ? (simplify_statement ?) ?);
     2505     (* We can't invoke Cthulhu on a list of labeled statements. We must proceed more manually. *)
     2506     lapply (Hind (Kswitch k) (Kswitch k') ?)
     2507     [ 1: @cc_switch //
     2508     | 2: cases (find_label_ls lab ls (Kswitch k)) normalize nodelta
     2509          [ 1: //
     2510          | 2: * #st #kst normalize nodelta // ] ]
     2511| 13: #lab' #s0 #Hind #k #k' #Hcont_cast
     2512     whd in match (find_label ???);
     2513     whd in match (find_label ? (simplify_statement ?) ?);
     2514     cases (ident_eq lab lab') normalize nodelta
     2515     [ 1: #_ %{k'} /2/
     2516     | 2: #_ elim (invoke_cthulhu lab s0 k k' Hcont_cast Hind)
     2517          [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2518                normalize nodelta %{kst'} /2/
     2519          | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
     2520     ]
     2521| 14: #l #k #k' #Hcont_cast //
     2522| 15: #l #s0 #Hind #k #k' #Hcont_cast
     2523     whd in match (find_label ???);
     2524     whd in match (find_label ? (simplify_statement ?) ?);
     2525     elim (invoke_cthulhu lab s0 k k' Hcont_cast Hind)
     2526     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2527          normalize nodelta %{kst'} /2/
     2528     | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
     2529| 16: #s0 #Hind #k #k' #Hcont_cast
     2530     whd in match (find_label ???);
     2531     whd in match (find_label ? (simplify_statement ?) ?);
     2532     elim (invoke_cthulhu lab s0 k k' Hcont_cast Hind)
     2533     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
     2534          normalize nodelta %{kst'} /2/
     2535     | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
     2536| 17: #sz #i #s0 #t #Hind_s0 #Hind_ls #k #k' #Hcont_cast
     2537     whd in match (simplify_ls ?);
     2538     whd in match (find_label_ls ???);
     2539     lapply Hind_ls
     2540     @(labeled_statements_ind … t)
     2541     [ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?);
     2542          elim (invoke_cthulhu lab s0
     2543                  (Kseq default_case k)
     2544                  (Kseq (simplify_statement default_case) k') ? Hind_s0)
     2545         [ 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast'
     2546              >Hrewrite >Hrewrite1         
     2547              normalize nodelta whd in match (find_label_ls ???);
     2548              >Hrewrite >Hrewrite1 normalize nodelta
     2549              %{kst'} /2/
     2550         | 3: @cc_seq //
     2551         | 1: * #Hrewrite #Hrewrite1 >Hrewrite normalize nodelta
     2552              lapply (Hind_ls k k' Hcont_cast)
     2553              cases (find_label_ls lab (LSdefault default_case) k)
     2554              [ 1: normalize nodelta #Heq1
     2555                   whd in match (simplify_ls ?);
     2556                   whd in match (find_label_ls lab ??);
     2557                   whd in match (seq_of_labeled_statement ?);
     2558                   whd in match (find_label_ls lab ??);
     2559                   >Hrewrite1 normalize nodelta @Heq1
     2560              | 2: * #st #kst normalize nodelta #H
     2561                   whd in match (find_label_ls lab ??);
     2562                   whd in match (simplify_ls ?);
     2563                   whd in match (seq_of_labeled_statement ?);
     2564                   >Hrewrite1 normalize nodelta @H
     2565              ]
     2566         ]
     2567     | 2: #sz' #i' #s' #tl' #Hind #A
     2568     
     2569          whd in match (seq_of_labeled_statement ?);
     2570          elim (invoke_cthulhu lab s0
     2571                   (Kseq (Ssequence s' (seq_of_labeled_statement tl')) k)
     2572                   (Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k')
     2573                   ?
     2574                   Hind_s0)
     2575          [ 3: @cc_seq //
     2576          | 1: * #Heq #Heq2 >Heq >Heq2 normalize nodelta
     2577               lapply (A k k' Hcont_cast)
     2578               cases (find_label_ls lab (LScase sz' i' s' tl') k) normalize nodelta
     2579               [ 1: #H whd in match (find_label_ls ???);
     2580                    <simplify_ls_commute
     2581                    whd in match (seq_of_labeled_statement ?);
     2582                    >Heq2 normalize nodelta
     2583                    assumption
     2584               | 2: * #st #kst normalize nodelta #H
     2585                    whd in match (find_label_ls ???);
     2586                    <simplify_ls_commute >Heq2 normalize nodelta @H
     2587               ]
     2588          | 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast'
     2589               >Hrewrite normalize nodelta
     2590               %{kst'} @conj try //
     2591               whd in match (find_label_ls ???);
     2592               <simplify_ls_commute >Hrewrite1 //
     2593          ]
     2594    ]
     2595] qed.   
     2596                   
     2597lemma cast_find_label_fn : ∀lab,f,k,k',s,ks.
     2598  cont_cast k k' →
     2599  find_label lab (fn_body f) k = Some ? 〈s,ks〉 →
     2600  ∃ks'. find_label lab (fn_body (simplify_function f)) k' = Some ? 〈simplify_statement s,ks'〉
     2601        ∧ cont_cast ks ks'.
     2602#lab * #rettype #args #vars #body #k #k' #s #ks #Hcont_cast #Hfind_lab
     2603whd in match (simplify_function ?);
     2604lapply (cast_find_label lab body ?? Hcont_cast)
     2605>Hfind_lab normalize nodelta //
     2606qed.
     2607
     2608theorem cast_correction : ∀ge, ge'.
     2609  related_globals ? simplify_fundef ge ge' →
     2610  ∀s1, s1', tr, s2.
     2611  state_cast s1 s1' →
     2612  exec_step ge s1 = Value … 〈tr,s2〉 →
     2613  ∃s2'. exec_step ge' s1' = Value … 〈tr,s2'〉 ∧
     2614        state_cast s2 s2'.
     2615#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hs1_sim_s1' #Houtcome
     2616inversion Hs1_sim_s1'
     2617[ 1: (* regular state *)
     2618     #f #stm #k #k' #en #m #Hcont_cast
     2619     lapply (related_globals_expr_simulation ge ge' en m Hrelated) #Hsim_related
     2620     lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related
     2621     cases stm
     2622     (* Perform the intros for the statements*)
     2623     [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
     2624     | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
     2625     | 14: #lab | 15: #cost #body ]
     2626     [ 1: (* Skip *)
     2627          #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
     2628          whd in match (exec_step ??); whd in match (exec_step ??);
     2629          inversion Hcont_cast
     2630          [ 1: (* Kstop *)
     2631               #Hk #Hk' #_ >fn_return_simplify cases (fn_return f) normalize nodelta
     2632               [ 1: >Heq_s1 in Hs1_sim_s1'; >Heq_s1' #Hsim inversion Hsim
     2633                    [ 1: #f0 #s #k0 #k0' #e #m0 #Hcont_cast0 #Hstate_eq #Hstate_eq' #_
     2634                         #Eq whd in match (ret ??) in Eq; destruct (Eq)
     2635                         %{(Returnstate Vundef Kstop (free_list m (blocks_of_env en)))} @conj
     2636                         [ 1: // | 2: %3 %1 ]
     2637                    | 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd)
     2638                    | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd)
     2639                    | 4: #r #Habsurd destruct (Habsurd) ]                   
     2640               | 3: #irrelevant #Habsurd destruct
     2641               | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct
     2642               | *: #irrelevant1 #irrelevant2 #Habsurd destruct ]
     2643          | 2: (* Kseq stm' k' *)
     2644               #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2645               whd in match (ret ??) in Eq; destruct (Eq)
     2646               %{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj
     2647               [ 1: // | 2: %1 // ]               
     2648          | 3: (* Kwhile *)
     2649               #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2650               whd in match (ret ??) in Eq; destruct (Eq)               
     2651               %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj
     2652               [ 1: // | 2: %1 // ]
     2653          | 4: (* Kdowhile *)
     2654               #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2655               elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond
     2656               [ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct
     2657               | 1: cases (exec_expr ge en m cond) in Eq;
     2658                    [ 2: #error whd in match (m_bind ?????) in ⊢ (% → ?); #Habsurd destruct
     2659                    | 1: * #val #trace whd in match (m_bind ?????) in ⊢ (% → ?); <Htype_cond_eq
     2660                         #Eq #Hsim_cond lapply (Hsim_cond 〈val,trace〉 (refl ? (OK ? 〈val,trace〉)))
     2661                         #Hrewrite_cond >Hrewrite_cond whd in match (m_bind ?????);
     2662                         (* case analysis on the outcome of the conditional *)
     2663                         cases (exec_bool_of_val val (typeof cond)) in Eq ⊢ %;
     2664                         [ 2: (* evaluation of the conditional fails *)
     2665                              #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
     2666                         | 1: * whd in match (bindIO ??????);
     2667                                whd in match (bindIO ??????);
     2668                                #Eq destruct (Eq)
     2669                              [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
     2670                                   @conj [ 1: // | 2: %1 // ]
     2671                              | 2: %{(State (simplify_function f) Sskip k0' en m)}
     2672                                   @conj [ 1: // | 2: %1 // ]
     2673                              ]
     2674                         ]
     2675                    ]
     2676               ]
     2677           | 5,6,7:
     2678                #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2679                whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
     2680                [ 1: %{(State (simplify_function f)
     2681                              (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body))
     2682                               k0' en m)} @conj
     2683                     [ 1: // | 2: %1 // ]
     2684                | 2: %{(State (simplify_function f)
     2685                              (simplify_statement step)
     2686                              (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0')
     2687                              en m)} @conj
     2688                     [ 1: // | 2: %1 @cc_for3 // ]
     2689                | 3: %{(State (simplify_function f)
     2690                              (Sfor Sskip (simplify_e cond) (simplify_statement step)
     2691                              (simplify_statement body))
     2692                              k0' en m)} @conj
     2693                     [ 1: // | 2: %1 // ]
     2694                ]
     2695           | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2696                whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
     2697                %{(State (simplify_function f) Sskip k0' en m)} @conj
     2698                [ 1: // | 2: %1 // ]
     2699           | 9: (* Call *)
     2700                #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ #Eq
     2701                >fn_return_simplify cases (fn_return f) in Eq; normalize nodelta
     2702               [ 1: #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
     2703                    %{(Returnstate Vundef (Kcall r (simplify_function f0) en0 k0')
     2704                                  (free_list m (blocks_of_env en)))} @conj
     2705                    [ 1: // | 2: %3 @cc_call // ]                                 
     2706               | 3: #irrelevant #Habsurd destruct (Habsurd)
     2707               | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct (Habsurd)
     2708               | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ]
     2709           ]
     2710     | 2: (* Assign *)
     2711          #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
     2712          whd in match (simplify_statement ?); #Heq
     2713          whd in match (exec_step ??) in Heq ⊢ %;
     2714          (* Begin by making the simplify_e disappear using Hsim_related *)
     2715          elim (Hsim_lvalue_related lhs) *
     2716          [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd)
     2717          | 1: cases (exec_lvalue ge en m lhs) in Heq;
     2718               [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     2719               | 1: * * #block #offset #trace
     2720                    whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_lhs
     2721                    lapply (Hsim 〈block, offset, trace〉 (refl ? (OK ? 〈block, offset, trace〉)))
     2722                    #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????);
     2723                    (* After [lhs], treat [rhs] *)
     2724                    elim (Hsim_related rhs) *
     2725                    [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd)
     2726                    | 1: cases (exec_expr ge en m rhs) in Heq;
     2727                         [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     2728                         | 1: * #val #trace
     2729                              whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_rhs
     2730                              lapply (Hsim 〈val, trace〉 (refl ? (OK ? 〈val, trace〉)))
     2731                              #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????);
     2732                              <Htype_eq_lhs <Htype_eq_rhs
     2733                              cases (opt_to_io ?????) in Heq;
     2734                              [ 1: #o #resumption whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
     2735                              | 3: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
     2736                              | 2: #mem whd in match (bindIO ??????); #Heq destruct (Heq)
     2737                                   %{(State (simplify_function f) Sskip k' en mem)} @conj
     2738                                   [ 1: // | 2: %1 // ]
     2739                              ]
     2740                         ]
     2741                    ]
     2742               ]
     2743         ]
     2744    | 3: (* Call *)
     2745         #Heq_s1 #Heq_s1' #_  lapply Houtcome >Heq_s1
     2746         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2747         whd in match (exec_step ??) in Heq ⊢ %;
     2748         elim (Hsim_related func) in Heq; *
     2749         [ 2: * #error #Hfail >Hfail #Htype_eq #Habsurd normalize in Habsurd; destruct (Habsurd)
     2750         | 1: cases (exec_expr ??? func)
     2751              [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2752              | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq
     2753                   whd in match (bindIO ??????) in ⊢ (% → %);
     2754                   elim (related_globals_exprlist_simulation ge ge' en m Hrelated args)
     2755                   [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
     2756                   | 1: cases (exec_exprlist ge en m args)
     2757                        [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2758                        | 1: #l -Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq
     2759                             whd in match (bindIO ??????) in ⊢ (% → %);
     2760                             elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a))
     2761                             cases (find_funct clight_fundef ge (\fst a));
     2762                             [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2763                             | 2: #clfd -Hsim #Hsim lapply (Hsim clfd (refl ? (Some ? clfd))) #Heq >Heq
     2764                                  whd in match (bindIO ??????) in ⊢ (% → %);
     2765                                  >simplify_type_of_fundef_eq >(simplify_fun_typeof_eq ge en m)
     2766                                  cases (assert_type_eq (type_of_fundef clfd) (fun_typeof func))
     2767                                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     2768                                  | 1: #Htype_eq cases ret                                     
     2769                                       [ 1: whd in match (bindIO ??????) in ⊢ (% → %);
     2770                                            #Eq destruct (Eq)
     2771                                            %{(Callstate (simplify_fundef clfd) (\fst  l)
     2772                                                         (Kcall (None (block×offset×type)) (simplify_function f) en k') m)}
     2773                                            @conj
     2774                                            [ 1: // | 2: %2 @cc_call // ]
     2775                                       | 2: #fptr whd in match (bindIO ??????) in ⊢ (% → %);
     2776                                            elim (Hsim_lvalue_related fptr) *
     2777                                            [ 2: * #error #Hfail >Hfail #_
     2778                                                 #Habsurd normalize in Habsurd; destruct (Habsurd)
     2779                                            | 1: cases (exec_lvalue ge en m fptr)
     2780                                                 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2781                                                 | 1: #a #Hsim #Htype_eq_fptr >(Hsim a (refl ? (OK ? a)))
     2782                                                      whd in match (bindIO ??????) in ⊢ (% → %);
     2783                                                      #Heq destruct (Heq)
     2784                                                      %{(Callstate (simplify_fundef clfd) (\fst  l)
     2785                                                                   (Kcall (Some (block×offset×type) 〈\fst  a,typeof (simplify_e fptr)〉)
     2786                                                                   (simplify_function f) en k') m)}
     2787                                                      @conj [ 1: // | 2: >(simplify_typeof_eq ge en m) %2 @cc_call // ]
     2788        ] ] ] ] ] ] ] ] ]
     2789    | 4: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2790         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2791         whd in match (exec_step ??) in Heq ⊢ %;
     2792         destruct (Heq)
     2793         %{(State (simplify_function f) (simplify_statement stm1) (Kseq (simplify_statement stm2) k') en m)}
     2794         @conj
     2795         [ 1: // | 2: %1 @cc_seq // ]
     2796    | 5: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2797         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2798         whd in match (exec_step ??) in Heq ⊢ %;
     2799         elim (Hsim_related cond) in Heq; *
     2800         [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2801         | 1: cases (exec_expr ge en m cond)
     2802              [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2803              | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq
     2804                   #Htype_eq_cond
     2805                   whd in match (bindIO ??????) in ⊢ (% → %);
     2806                   >(simplify_typeof_eq ge en m)
     2807                   cases (exec_bool_of_val condval (typeof cond))
     2808                   [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     2809                   | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
     2810                        [ 1: destruct skip (condtrace)
     2811                             %{(State (simplify_function f) (simplify_statement iftrue) k' en m)} @conj
     2812                             [ 1: // | 2: <e0 %1 // ]
     2813                        | 2: destruct skip (condtrace)
     2814                             %{(State (simplify_function f) (simplify_statement iffalse) k' en m)} @conj
     2815                             [ 1: // | 2: <e0 %1 // ]
     2816                        ] ] ] ]
     2817    | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2818         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2819         whd in match (exec_step ??) in Heq ⊢ %;
     2820         elim (Hsim_related cond) in Heq; *
     2821         [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2822         | 1: cases (exec_expr ge en m cond)
     2823              [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2824              | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq
     2825                   #Htype_eq_cond
     2826                   whd in match (bindIO ??????) in ⊢ (% → %);
     2827                   >(simplify_typeof_eq ge en m)
     2828                   cases (exec_bool_of_val condval (typeof cond))
     2829                   [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     2830                   | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
     2831                        [ 1: destruct skip (condtrace)
     2832                             %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)}
     2833                             @conj
     2834                             [ 1: // | 2: <e0 %1 @cc_while // ]
     2835                        | 2: destruct skip (condtrace)
     2836                             %{(State (simplify_function f) Sskip k' en m)} @conj
     2837                             [ 1: // | 2: <e0 %1 // ]
     2838                        ] ] ] ]
     2839    | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2840         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2841         whd in match (exec_step ??) in Heq ⊢ %;
     2842         destruct (Heq)
     2843         %{(State (simplify_function f) (simplify_statement body)
     2844                  (Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj
     2845         [ 1: // | 2: %1 @cc_dowhile // ]
     2846    | 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2847         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2848         whd in match (exec_step ??) in Heq ⊢ %;
     2849         cases (is_Sskip init) in Heq;
     2850         [ 2: #Hinit_neq_Sskip elim (simplify_is_not_skip init Hinit_neq_Sskip) #pf #Hrewrite >Hrewrite
     2851              normalize nodelta
     2852              whd in match (ret ??) in ⊢ (% → %);
     2853              #Eq destruct (Eq)
     2854              %{(State (simplify_function f) (simplify_statement init)
     2855                       (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj
     2856              [ 1: // | 2: %1 @cc_for1 // ]   
     2857         | 1: #Hinit_eq_Sskip >Hinit_eq_Sskip
     2858              whd in match (simplify_statement ?);
     2859              whd in match (is_Sskip ?);
     2860              normalize nodelta
     2861              elim (Hsim_related cond) *
     2862              [ 2: * #error #Hfail #_ >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
     2863              | 1: cases (exec_expr ge en m cond)
     2864                   [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2865                   | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite #Htype_eq_cond >Hrewrite
     2866                        whd in match (m_bind ?????); whd in match (m_bind ?????);
     2867                        <Htype_eq_cond
     2868                        cases (exec_bool_of_val ? (typeof cond))
     2869                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     2870                        | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
     2871                             normalize nodelta #Heq destruct (Heq)
     2872                             [ 1: %{(State (simplify_function f) (simplify_statement body)
     2873                                           (Kfor2 (simplify_e cond) (simplify_statement step) (simplify_statement body) k') en m)}
     2874                                   @conj [ 1: // | 2: %1 @cc_for2 // ]
     2875                             | 2: %{(State (simplify_function f) Sskip k' en m)} @conj
     2876                                  [ 1: // | 2: %1 // ]
     2877         ] ] ] ] ]
     2878    | 9: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2879         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2880         whd in match (exec_step ??) in Heq ⊢ %;
     2881         inversion Hcont_cast in Heq; normalize nodelta
     2882         [ 1: #Hk #Hk' #_
     2883         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2884         | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2885         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2886         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2887         | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2888         | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
     2889         #H whd in match (ret ??) in H ⊢ %;
     2890         destruct (H)
     2891         [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ]
     2892         | 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
     2893    | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2894         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2895         whd in match (exec_step ??) in Heq ⊢ %;
     2896         inversion Hcont_cast in Heq; normalize nodelta
     2897         [ 1: #Hk #Hk' #_
     2898         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2899         | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2900         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2901         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2902         | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     2903         | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
     2904         #H whd in match (ret ??) in H ⊢ %;
     2905         destruct (H)
     2906         [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 //
     2907         | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)}
     2908              @conj try // %1 //
     2909         | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H;
     2910              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
     2911              | 1: cases (exec_expr ??? cond)
     2912                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2913                   | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
     2914                        whd in match (m_bind ?????) in ⊢ (% → %);
     2915                        <Htype_cond_eq
     2916                        cases (exec_bool_of_val ? (typeof cond))
     2917                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     2918                        | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
     2919                             normalize nodelta #Heq destruct (Heq)
     2920                             [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
     2921                                  @conj [ 1: // | 2: %1 // ]
     2922                             | 2: %{(State (simplify_function f) Sskip k0' en m)}
     2923                                  @conj [ 1: // | 2: %1 // ]
     2924             ] ] ] ]
     2925         | 5: %{(State (simplify_function f) (simplify_statement step)
     2926                       (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj
     2927              [ 1: // | 2: %1 @cc_for3 // ]
     2928         ]
     2929    | 11: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2930          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2931          whd in match (exec_step ??) in Heq ⊢ %;
     2932          cases retval in Heq; normalize nodelta
     2933          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
     2934               whd in match (ret ??) in ⊢ (% → %);
     2935               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
     2936               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
     2937               #H destruct (H)
     2938               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))}
     2939               @conj [ 1: // | 2: %3 @call_cont_simplify // ]
     2940          | 2: #e >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
     2941               [ 1: #_ #Habsurd destruct (Habsurd)
     2942               | 2: #_ elim (Hsim_related e) *
     2943                    [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2944                    | 1: cases (exec_expr ??? e)
     2945                         [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2946                         | 1: #a #Hsim #Htype_eq_e lapply (Hsim a (refl ? (OK ? a)))
     2947                              #Hrewrite >Hrewrite
     2948                              whd in match (m_bind ?????); whd in match (m_bind ?????);
     2949                              #Heq destruct (Heq)
     2950                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env en)))}
     2951                              @conj [ 1: // | 2: %3 @call_cont_simplify // ]
     2952         ] ] ] ]
     2953    | 12: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2954          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2955          whd in match (exec_step ??) in Heq ⊢ %;
     2956          elim (Hsim_related cond) in Heq; *
     2957          [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2958          | 1: cases (exec_expr ??? cond)
     2959               [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     2960               | 1: #a #Hsim #Htype_eq_cond lapply (Hsim a (refl ? (OK ? a)))
     2961                    #Hrewrite >Hrewrite
     2962                    whd in match (bindIO ??????); whd in match (bindIO ??????);
     2963                    cases (\fst a) normalize nodelta
     2964                    [ 1,3,4,5: #a destruct (a) #b destruct (b)
     2965                    | 2: #sz #i whd in match (ret ??) in ⊢ (% → %); #Heq destruct (Heq)
     2966                         %{(State (simplify_function f)
     2967                                  (seq_of_labeled_statement (select_switch sz i (simplify_ls switchcases)))
     2968                                  (Kswitch k') en m)} @conj
     2969                         [ 1: //
     2970                         | 2: @(labeled_statements_ind … switchcases)
     2971                              [ 1: #default_s
     2972                                   whd in match (simplify_ls ?);
     2973                                   whd in match (select_switch sz i ?) in ⊢ (?%%);
     2974                                   whd in match (seq_of_labeled_statement ?) in ⊢ (?%%);
     2975                                   %1 @cc_switch //
     2976                              | 2: #sz' #i' #top_case #tail #Hind
     2977                                   cut ((seq_of_labeled_statement (select_switch sz i (simplify_ls (LScase sz' i' top_case tail))))
     2978                                         = (simplify_statement (seq_of_labeled_statement (select_switch sz i (LScase sz' i' top_case tail)))))
     2979                                   [ 1: >select_switch_commute >simplify_ls_commute @refl
     2980                                   | 2: #Hrewrite >Hrewrite
     2981                                        %1 @cc_switch //
     2982         ] ] ] ] ] ]
     2983    | 13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2984          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2985          whd in match (exec_step ??) in Heq ⊢ %;
     2986          destruct (Heq)
     2987          %{(State (simplify_function f) (simplify_statement body) k' en m)}
     2988          @conj %1 //
     2989   | 14: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2990          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     2991          whd in match (exec_step ??) in Heq ⊢ %;
     2992          lapply (cast_find_label_fn lab f (call_cont k) (call_cont k'))
     2993          cases (find_label lab (fn_body f) (call_cont k)) in Heq;
     2994          normalize nodelta
     2995          [ 1: #Habsurd destruct (Habsurd)
     2996          | 2: * #st #kst normalize nodelta
     2997               #Heq whd in match (ret ??) in Heq;
     2998               #H lapply (H st kst (call_cont_simplify ???) (refl ? (Some ? 〈st,kst〉))) try //
     2999               * #kst' * #Heq2 #Hcont_cast' >Heq2 normalize nodelta
     3000               destruct (Heq)
     3001               %{(State (simplify_function f) (simplify_statement st) kst' en m)} @conj
     3002               [ 1: // | 2: %1 // ]
     3003          ]
     3004   | 15: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     3005          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     3006          whd in match (exec_step ??) in Heq ⊢ %;
     3007          destruct (Heq)                   
     3008          %{(State (simplify_function f) (simplify_statement body) k' en m)}
     3009          @conj
     3010          [ 1: // | 2: %1 // ]
     3011   ]
     3012| 2: (* Call state *)
     3013     #fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     3014     whd in match (exec_step ??) in ⊢ (% → %);
     3015     elim fd in Heq_s1'; normalize nodelta
     3016     [ 1: * #rettype #args #vars #body #Heq_s1'
     3017          whd in match (simplify_function ?);
     3018          cases (exec_alloc_variables empty_env ??)
     3019          #local_env #new_mem normalize nodelta
     3020          cases (exec_bind_parameters ????)
     3021          [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     3022          | 1: #new_mem_init
     3023               whd in match (m_bind ?????); whd in match (m_bind ?????);
     3024                #Heq destruct (Heq)               
     3025                %{(State (mk_function rettype args vars (simplify_statement body))
     3026                         (simplify_statement body) k' local_env new_mem_init)} @conj
     3027                [ 1: // | 2: %1 // ]
     3028          ]
     3029     | 2: #id #argtypes #rettype #Heq_s1'
     3030          cases (check_eventval_list args ?)
     3031          [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
     3032          | 1: #l whd in match (m_bind ?????); whd in match (m_bind ?????);
     3033          #Habsurd destruct (Habsurd) ]
     3034     ]
     3035| 3: (* Return state *)             
     3036     #res #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     3037     whd in match (exec_step ??) in ⊢ (% → %);
     3038     inversion Hcont_cast
     3039     [ 1: #Hk #Hk' #_
     3040     | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     3041     | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     3042     | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     3043     | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     3044     | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     3045     | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
     3046     normalize nodelta
     3047     [ 1: cases res normalize nodelta
     3048          [ 2: * normalize nodelta #i
     3049               [ 3: #Heq whd in match (ret ??) in Heq; destruct (Heq)
     3050                    %{(Finalstate i)} @conj [ 1: // | 2: // ]
     3051               | * : #Habsurd destruct (Habsurd) ]
     3052          | *: #a try #b destruct ]
     3053     | 9: elim r normalize nodelta
     3054          [ 2: * * #block #offset #typ normalize nodelta
     3055               cases (opt_to_io io_out io_in mem ? (store_value_of_type' ????))
     3056               [ 2: #mem whd in match (m_bind ?????); whd in match (m_bind ?????);
     3057                    #Heq destruct (Heq)
     3058                    %{(State (simplify_function f0) Sskip k0' en0 mem)} @conj
     3059                    [ 1: // | 2: %1 // ]
     3060               | 1: #output #resumption
     3061                    whd in match (m_bind ?????); #Habsurd destruct (Habsurd)
     3062               | 3: #eror #Habsurd normalize in Habsurd; destruct (Habsurd) ]
     3063          | 1: #Heq whd in match (ret ??) in Heq; destruct (Heq)
     3064               %{(State (simplify_function f0) Sskip k0' en0 m)} @conj
     3065               [ 1: // | 2: %1 // ]
     3066          ]
     3067     | *: #Habsurd destruct (Habsurd) ]
     3068| 4: (* Final state *)
     3069     #r #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     3070     whd in match (exec_step ??) in ⊢ (% → %);
     3071     #Habsurd destruct (Habsurd)
     3072] qed.
     3073
Note: See TracChangeset for help on using the changeset viewer.