include "Clight/Cexec.ma". include "Clight/CexecInd.ma". lemma exec_bool_of_val_sound: ∀v,ty,r. exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). #v #ty #r cases v; [ | #sz #i (*| #f*) | | #ptr ] cases ty; [ 2,10,18,26: #sz' #sg | 3,11,19,27: #ty' | 4,12,20,28: (*#r*) #ty #n | 5,13,21,29: #args #rty | 6,7,14,15,22,23,30,31: #id #fs | 8,16,24,32: (*#r*) #id ] whd in ⊢ (??%? → ?); [ 2: @intsize_eq_elim_elim [ #NE #H destruct | *; whd @eq_bv_elim [ #E1 #E2 destruct @bool_of_val_false @is_false_int | #E1 #E2 destruct @bool_of_val_true @is_true_int_int @E1 ] ] (*| 8: #H cases (eq_dec f Fzero) [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float | #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne ]*) | 7: #H destruct @bool_of_val_false @is_false_pointer | 8: #H destruct @bool_of_val_true @is_true_pointer_pointer | *: #H destruct ] qed. lemma bool_val_distinct: Vtrue ≠ Vfalse. % normalize #H destruct qed. lemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) → if b then is_true v ty else is_false v ty. #v #ty #b cases b; #H inversion H; #v' #ty' #H' #ev #et #ev' //; @⊥ cases (bool_val_distinct) #X @X [2: @sym_eq] @ev' qed. lemma try_cast_null_sound: ∀m,sz,i,ty,ty',v'. try_cast_null m sz i ty ty' = OK ? v' → cast m (Vint sz i) ty ty' v'. #m #sz #i #ty #ty' #v' whd in ⊢ (??%? → ?); @eq_bv_elim [ #e >e cases ty; [ | #sz' #sg (* | #fs *) | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ] whd in ⊢ (??%? → ?); #H [ 2: | *: destruct ] cases ty' in H ⊢ %; [ | #sz'' #sg (* | #fs*) | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ] try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z // | #_ whd in ⊢ (??%? → ?); #H destruct ] qed. lemma exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'. #m #v #ty #ty' #v' cases v; [ #H whd in H:(??%?); destruct; | #sz #i cases ty; [ #H whd in H:(??%?); destruct; (* | 3: #a #H whd in H:(??%?); destruct; *) | 6,7,8: #a [ 1,2: #b ] #H whd in H:(??%?); destruct; | #sz1 #si1 cases ty'; [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim [ #NE #H destruct | *; whd #H whd in H:(??%?); destruct; ] (* | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim [ #E #H whd in H:(??%?); destruct | *; whd #H whd in H:(??%?); destruct; @cast_if ] *) | 2,6,7,8: #a [1,2,3: #b] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim [ 1,3,5,7: #NE #H destruct | *: *; whd #H whd in H:(??%?); destruct; // ] | 3,4,5: [ #ty'' letin t ≝ (Tpointer ty'') | #ty'' #n letin t ≝ (Tarray ty'' n) | #args #rty letin t ≝ (Tfunction args rty) ] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim [ 1,3,5: #NE #H destruct | *: *; whd lapply (try_cast_null_sound m sz i (Tint sz si1) t v'); cases (try_cast_null m sz i (Tint sz si1) t); [ 1,3,5: #v'' #H' #e @H' @e | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H); ] ] ] | *: [ #ty'' letin t ≝ (Tpointer ty'') | #ty'' #n letin t ≝ (Tarray ty'' n) | #args #rty letin t ≝ (Tfunction args rty) ] whd in ⊢ (??%? → ?); lapply (try_cast_null_sound m sz i t ty' v'); cases (try_cast_null m sz i t ty'); [ 1,3,5: #v'' #H' #e @H' @e | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H); ] ] (*| #f cases ty; [ 3,4,9: #x | 2,5,6,7,8: #x #y ] [ cases ty'; [ #e | 3,4,9: #a #e | 2,6,7,8: #a #b #e | #a #b #e ] whd in e:(??%?); destruct; //; | *: #e whd in e:(??%?); destruct ] *) | cases ty; [ 3,8: #x | 2,4,5,6,7: #x #y ] whd in ⊢ (??%? → ?); #H destruct cases ty' in H; normalize; try #a try #b try #c try #d destruct; @cast_pp_z //; (* | #ptr whd in ⊢ (??%? → ?); #e elim (bind_inversion ????? e) #s * #es #e' elim (bind_inversion ????? e') #u * #eu #e'' -e'; elim (bind_inversion ????? e'') #s' * #es' #e'''; -e''; cut (type_region ty s); [ cases ty in es:(??%?) ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ] whd in e:(??%%); destruct; //; | #Hty cut (type_region ty' s'); [ cases ty' in es' ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ] whd in e:(??%%); destruct; //; | #Hty' cut (s = ptype ptr). elim (eq_region_dec (ptype ptr) s) in eu; //; normalize; #_ #e destruct. #e >e in Hty; #Hty cases (pointer_compat_dec (pblock ptr) s') in e'''; #Hcompat #e''' whd in e''':(??%%); destruct /2 by cast_pp/ ] ] *) | #ptr cases ty; [ 3,8: #x | 2,4,5,6,7: #x #y ] #E whd in E:(??%?); destruct cases ty' in E ⊢ %; normalize #A try #B try #C try #D destruct /2/ ] qed. theorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr. (P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)). #ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e) [ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%); @eq_intsize_elim #E try @I H in He'; #He' @He' | #v #ty whd in ⊢ (???%); lapply (refl ? (lookup SymbolTag block en v)) cases (lookup SymbolTag block en v) in ⊢ (???% → %); [ #eget @opt_bind_OK #sploc cases sploc; #sp (* #loc *) #efind whd; @(eval_Evar_global … eget efind) | #loc #eget @(eval_Evar_local … eget) ] | #ty #e #He whd in ⊢ (???%); @bind2_OK #v cases v / by / * #l #ofs #tr #Hv whd >Hv in He; #He @eval_Ederef @He | #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H cases ty try (try #a try #b try #c @I) #ty' whd @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He'' | #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1 @opt_bind_OK #v #ev @(eval_Eunop … ev) >Hv1 in He1; #He1 @He1 | #ty #op #e1 #e2 #He1 #He2 @bind2_OK #v1 #tr1 #ev1 >ev1 in He1; #He1 @bind2_OK #v2 #tr2 #ev2 >ev2 in He2; #He2 @opt_bind_OK #v #ev whd in He1 He2; whd; @(eval_Ebinop … He1 He2 ev) | #ty #ty' #e' #He' @bind2_OK #v #tr #Hv >Hv in He'; #He' @bind_OK #v' #ev' @(eval_Ecast … He' ?) (* XXX /2/; *) @(exec_cast_sound … ev') | #ty #e1 #e2 #e3 #He1 #He2 #He3 @bind2_OK #vb #tr1 #Hvb >Hvb in He1; #He1 @bind_OK #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb @bind2_OK #v #tr #Hv whd in Hv:(??%?); [ >Hv in He2; #He2 whd in He2 Hv:(??%?) ⊢%; @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb) | >Hv in He3; #He3 whd in He3 Hv:(??%?) ⊢%; @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb) ] | #ty #e1 #e2 #He1 #He2 @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1 @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1 normalize nodelta [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2 @bind_OK #b2 #eb2 whd in match (cast_bool_to_target ??); cases ty [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ] try @I normalize nodelta @(eval_Eandbool_2 … (of_bool b2) … He1 … He2) [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) | @refl ] | cases ty [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ] try @I @(eval_Eandbool_1 … He1) [ @(bool_of … Hb1) | @refl ] ] | #ty #e1 #e2 #He1 #He2 @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1 @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1 normalize nodelta [ cases ty [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ] try @I @(eval_Eorbool_1 … He1) [ @(bool_of … Hb1) | @refl ] | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2 @bind_OK #b2 #eb2 cases ty [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ] try @I @(eval_Eorbool_2 … (of_bool b2) … He1 … He2) [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) | @refl ] ] | #ty #ty' cases ty try #sz try #sg try #x // | #ty #e' #ty' #i cases ty'; //; [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H @bind_OK #delta #Hdelta whd in H:(??%?); >H in He'; #He' @(eval_Efield_struct … He' (refl ??) Hdelta) | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?); >H in He'; #He' @(eval_Efield_union … He' (refl ??)) ] | #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He'; #He' @(eval_Ecost … He') (* exec_lvalue fails on non-lvalues. *) | #e' #ty cases e'; [ 2,4,11: #a #H try @I @(False_ind … H) | 3: #a * | 12,13: #a #b * | 1,5,7,9,10: #a #b #H @I | 6,8: #a #b #c #H @I ] try @I ] qed. lemma addrof_eval_lvalue: ∀ge,en,m,e,loc,off,tr,ty. eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer loc off)) tr → eval_lvalue ge en m e loc off tr. #ge #en #m #e #loc #off #tr #ty #H inversion H; [ 1,4: #a #b #c #H @False_ind destruct (H); | #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3

H whd in ⊢ (??%?); (* cases r *) @refl qed. theorem exec_lvalue_sound: ∀ge,en,m,e. P_res ? (λr.eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e). #ge #en #m #e lapply (refl ? (exec_lvalue ge en m e)); cases (exec_lvalue ge en m e) in ⊢ (???% → %); [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #loci #H (* #locr #loci #H *) @(addrof_eval_lvalue … (Tpointer Tvoid)) lapply (addrof_exec_lvalue … H) #H' lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer Tvoid))) >H' #H'' @H'' | #msg #_ whd @I ] qed. (* Plain equality versions of the above *) definition exec_expr_sound' ≝ λge,en,m,e,v. λH:exec_expr ge en m e = OK ? v. P_res_to_P ???? (exec_expr_sound ge en m e) H. definition exec_lvalue_sound' ≝ λge,en,m,e,loc,off,tr. λH:exec_lvalue ge en m e = OK ? 〈〈loc,off〉,tr〉. P_res_to_P ???? (exec_lvalue_sound ge en m e) H. lemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l). #ge #e #m #l elim l; whd [ % | #e1 #es #IH @bind2_OK #v #tr1 #Hv @bind2_OK #vs #tr2 #Hvs whd; @eval_Econs [ @(P_res_to_P … (exec_expr_sound ge e m e1) Hv) | @(P_res_to_P … IH Hvs) ] ] qed. lemma exec_alloc_variables_sound : ∀l,en,m,en',m'. exec_alloc_variables en m l = 〈en',m'〉 → alloc_variables en m l en' m'. #l elim l [ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct % | * #id #ty #t #IH #en #m #en' #m' lapply (refl ? (alloc m O (sizeof ty) (*XData*))) whd in ⊢ (? → ??%? → ?); cases (alloc ??? (*?*)) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC @(alloc_variables_cons … ALLOC) @IH @EXEC qed. lemma exec_bind_parameters_sound : ∀ps,vs,en,m. P_res ? (λm'. bind_parameters en m ps vs m') (exec_bind_parameters en m ps vs). #ps elim ps [ * // | * #id #ty #ps' #IH * [ // | #v #vs #en #m @opt_bind_OK #b #GET @opt_bind_OK #m' #STORE lapply (refl ? (exec_bind_parameters en m' ps' vs)) cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %); [2: #msg #_ %] #m'' #BIND @(bind_parameters_cons … GET STORE) lapply (IH vs en m') whd in ⊢ (% → ?); >BIND // ] ] qed. lemma check_eventval_list_sound : ∀vs,tys. P_res ? (λevs. eventval_list_match evs tys vs) (check_eventval_list vs tys). #vs0 elim vs0 [ * // | #v #vs #IH * [ // | #ty #tys whd in ⊢ (???%); cases ty [ #sz #sg | ] cases v // #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?); @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct @bind_OK #evs #CHECKevs @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECKevs)) // ] ] qed. theorem exec_step_sound: ∀ge,st. P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st). #ge #st cases st; [ #f #s #k #e #m cases s; [ cases k; [ whd in ⊢ (?????%); lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H whd; @step_skip_call //; | #s' #k' whd; // | #ex #s' #k' @step_skip_or_continue_while % //; | #ex #s' #k' @res_bindIO2_OK #v #tr #Hv letin bexpr ≝ (exec_bool_of_val v (typeof ex)); lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); [ #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb whd in ⊢ (?????%); [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv)) [ % // | @(bool_of … Hb) ] | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv)) [ % // | @(bool_of … Hb) ] ] | #msg #_ //; ] | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //; | #ex #s1 #s2 #k' @step_skip_for3 | #k' @step_skip_break_switch % //; | #r #f' #e' #k' whd in ⊢ (?????%); lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H whd; @step_skip_call //; ] | #ex1 #ex2 @res_bindIO2_OK #x cases x; (*#y cases y; *) #pcl (* #loc *) #ofs #tr1 #Hlval @res_bindIO2_OK #v2 #tr2 #Hv2 @opt_bindIO_OK #m' #em' whd; @(step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em') | #lex #fex #args @res_bindIO2_OK #vf #tr1 #Hvf0 lapply (exec_expr_sound' … Hvf0); #Hvf @res_bindIO2_OK #vargs #tr2 #Hvargs0 lapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs @opt_bindIO_OK #fd #efd @bindIO_OK #ety cases lex; whd; [ @(step_call_none … Hvf Hvargs efd ety) | #lhs' @res_bindIO2_OK #x cases x; (* #y cases y; *) #pcl (* #loc *) #ofs #tr3 #Hlocofs whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety) ] | #s1 #s2 // | #ex #s1 #s2 @res_bindIO2_OK #v #tr #Hv letin bexpr ≝ (exec_bool_of_val v (typeof ex)); lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //; #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb [ @(step_ifthenelse_true … (exec_expr_sound' … Hv)) @(bool_of … Hb) | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb) ] | #ex #s' @res_bindIO2_OK #v #tr #Hv letin bexpr ≝ (exec_bool_of_val v (typeof ex)); lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //; #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb [ @(step_while_true … (exec_expr_sound' … Hv)) @(bool_of … Hb) | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb) ] | #ex #s' // | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%); [ >Hs1 @res_bindIO2_OK #v #tr #Hv letin bexpr ≝ (exec_bool_of_val v (typeof ex)); lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //; #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb [ @(step_for_true … (exec_expr_sound' … Hv)) @(bool_of … Hb) | @(step_for_false … (exec_expr_sound' … Hv)) @(bool_of … Hb) ] | @step_for_start //; ] | whd in ⊢ (?????%); cases k; // #k' @step_skip_break_switch %2 // | whd in ⊢ (?????%); cases k; //; [ #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //; | #ex #s' #k' whd; @res_bindIO2_OK #v #tr #Hv letin bexpr ≝ (exec_bool_of_val v (typeof ex)); lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //; #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv)) [ %2 ; // | @(bool_of … Hb) ] | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv)) [ %2 ; // | @(bool_of … Hb) ] ] | #ex #s1 #s2 #k' whd; @step_skip_or_continue_for2 %2 ; // ] | #r whd in ⊢ (?????%); cases r; [ whd; lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H @step_return_0 @H | #ex cases (type_eq_dec (fn_return f) Tvoid); //; whd in ⊢ (% → ?????%); #Hnotvoid @res_bindIO2_OK #v #tr #Hv whd; @(step_return_1 … Hnotvoid (exec_expr_sound' … Hv)) ] | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv lapply (refl ? (typeof ex)) cases (typeof ex) in ⊢ (???% → %); // #sz' #sg #TY whd in ⊢ (?????%); cases (sz_eq_dec sz sz') // #SZ destruct (SZ) whd in ⊢ (?????%); @opt_bindIO_OK #ls' #LS @(step_switch … TY LS) @(exec_expr_sound' … Hv) | #l #s' // | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k))); cases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //; #sk cases sk; #s' #k' #H @(step_goto … H) | #l #s' // ] | #f0 #vargs #k #m whd in ⊢ (?????%); cases f0; [ #fn whd in ⊢ (?????%); lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn))) cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %); #en' #m' #ALLOC whd in ⊢ (?????%); @res_bindIO_OK #m2 #BIND whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC)) @(P_res_to_P … (exec_bind_parameters_sound …) BIND) | #id #argtys #rty @res_bindIO_OK #evs #Hevs #v' @bindIO_OK #eres whd @step_external_function % [ @(P_res_to_P … (check_eventval_list_sound …) Hevs) | @mk_val_correct ] ] | #v #k' #m' whd in ⊢ (?????%); cases k'; //; [ whd in ⊢ (?????%); cases v // * // | #r #f #e #k whd in ⊢ (?????%); cases r // * * #b #ofs #ty @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); // ] | // ] qed. lemma make_initial_state_sound : ∀p. P_res ? (initial_state p) (make_initial_state p). #p cases p; #fns #main #vars whd in ⊢ (???%); @bind_OK #m #Em @opt_bind_OK #x cases x; #sp #esb (* #b #esb *) @opt_bind_OK #f #ef @(initial_state_intro … Em esb ef) @refl qed. theorem exec_steps_sound: ∀ge,n,st. P_io ??? (λts:trace×state. star (mk_transrel ?? step) ge st (\fst ts) (\snd ts)) (exec_steps n ge st). #ge #n elim n; [ #st whd in ⊢ (?????%); elim (is_final_state st); #H whd; % | #n' #IH #st whd in ⊢ (?????%); elim (is_final_state st); #H [ whd; % | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s'; [ #f #s #k #e #m | #fd #args #k #m | #r #k #m | #r ] normalize [ 1,2,3: cases m; #mc #mn #mp ] #Hstep normalize @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps whd; @(star_step ????????? Hsteps) [ 2,5,8,11: @Hstep | 3,6,9,12: // ] ] qed. lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r. * [ 4: #r #r' normalize #E destruct % | *: normalize #x1 #x2 #x3 #x4 #x5 try #x6 try #x7 destruct ] qed.