(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) include "joint/linearise.ma". include "common/StatusSimulation.ma". include "joint/Traces.ma". include "joint/semanticsUtils.ma". include "common/ExtraMonads.ma". (* !!!SPOSTATO IN extraGlobalenvs.ma!!!! include alias "common/PositiveMap.ma". lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id. id < (nextfunction ? ge) → lookup_opt … id (functions ? ge) = None ? → lookup_opt … id (functions … (add_functs F ge l)) = None ?. #F #ge #l #id whd in match add_functs; normalize nodelta elim l -l [ #_ normalize //] * #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????); >lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %] #f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1) | cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl)) [elim tl [normalize //] #x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ] #H2 lapply(transitive_le … H H2) @lt_to_not_eq qed. lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l. lookup_opt … id (functions ? (\fst gem)) = None ? → lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?. #F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H] ** #x1 #x2 #x3 #tl whd in match add_globals; normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol; normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %] #f1 #H3 <(drop_fn_lfn … f1 H3) assumption qed. lemma globalenv_no_minus_one : ∀F,V,i,p. find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?. #F #V #i #p whd in match find_funct_ptr; normalize nodelta whd in match globalenv; whd in match globalenv_allocmem; normalize nodelta @add_globals_functions_miss @add_functs_functions_miss normalize // qed. *) (* !!!spostato in semantics.ma ed aggiunto un include a extraGlobalenvs.ma!!! lemma fetch_internal_function_no_minus_one : ∀F,V,i,p,bl. block_id (pi1 … bl) = -1 → fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p) bl = Error … [MSG BadFunction]. #F#V#i#p ** #r #id #EQ1 #EQ2 destruct whd in match fetch_internal_function; whd in match fetch_function; normalize nodelta >globalenv_no_minus_one cases (symbol_for_block ???) normalize // qed. *) (*spostato in ExtraMonads.ma lemma bind_option_inversion_star: ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B. (∀x.f = Some … x → g x = Some … y → P) → (! x ← f ; g x = Some … y) → P. #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed. interpretation "option bind inversion" 'bind_inversion = (bind_option_inversion_star ???????). lemma bind_inversion_star : ∀X,Y.∀P : Prop. ∀m : res X.∀f : X → res Y.∀v : Y. (∀x. m = return x → f x = return v → P) → ! x ← m ; f x = return v → P. #X #Y #P #m #f #v #H #G elim (bind_inversion ????? G) #x * @H qed. interpretation "res bind inversion" 'bind_inversion = (bind_inversion_star ???????). lemma IO_bind_inversion: ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. (∀x.f = return x → g x = return y → P) → (! x ← f ; g x = return y) → P. #O #I #A #B #P #f #g #y cases f normalize [ #o #f #_ #H destruct | #a #G #H @(G ? (refl …) H) | #e #_ #H destruct ] qed. interpretation "IO bind inversion" 'bind_inversion = (IO_bind_inversion ?????????). record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝ { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop) ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf)) ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n. m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) → m_frel ?? Q G (m_bind … m f) (m_bind … n g) ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v }. *) (*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ λO,I.mk_MonadFunctRel ?? (λX,Y,F,m,n.∀x.m = return x → n = return F x) ???. [ #X #Y #F #x #y whd in ⊢ (??%%→?); #EQ destruct(EQ) % | #X #Y #Z #W #F #G * [ #o #f | #u | #e ] #n #H #f #g #K #x whd in ⊢ (??%%→?); #EQ destruct(EQ) >(H ? (refl …)) @K @EQ | #X #Y #P #Q #H #z #w #G #x #EQ >(G … EQ) >H % ] qed.*) (* spostato in ExtraMonads.ma definition res_preserve : MonadFunctRel Res Res ≝ mk_MonadFunctRel ?? (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) ???. [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % | #X #Y #Z #W #P #Q #F #G * [ #u | #e ] #n #H #f #g #K #x whd in ⊢ (??%%→?); #EQ destruct(EQ) cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) | #X #Y #P #F #G #H #u #v #K #x #EQ cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % ] qed. definition opt_preserve : MonadFunctRel Option Option ≝ mk_MonadFunctRel ?? (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) ???. [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % | #X #Y #Z #W #P #Q #F #G * [ | #u ] #n #H #f #g #K #x whd in ⊢ (??%%→?); #EQ destruct(EQ) cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) | #X #Y #P #F #G #H #u #v #K #x #EQ cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % ] qed. definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ λO,I.mk_MonadFunctRel ?? (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) ???. [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % | #X #Y #Z #W #P #Q #F #G * [ #o #f | #u | #e ] #n #H #f #g #K #x whd in ⊢ (??%%→?); #EQ destruct(EQ) cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) | #X #Y #P #F #G #H #u #v #K #x #EQ cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % ] qed. definition preserving ≝ λM1,M2.λFR : MonadFunctRel M1 M2. λX,Y,A,B : Type[0]. λP : X → Prop. λQ : A → Prop. λF : ∀x : X.P x → Y. λG : ∀a : A.Q a → B. λf : X → M1 A. λg : Y → M2 B. ∀x,prf. FR … G (f x) (g (F x prf)). definition preserving2 ≝ λM1,M2.λFR : MonadFunctRel M1 M2. λX,Y,Z,W,A,B : Type[0]. λP : X → Prop. λQ : Y → Prop. λR : A → Prop. λF : ∀x : X.P x → Z. λG : ∀y : Y.Q y → W. λH : ∀a : A.R a → B. λf : X → Y → M1 A. λg : Z → W → M2 B. ∀x,y,prf1,prf2. FR … H (f x y) (g (F x prf1) (G y prf2)). *) definition graph_prog_params ≝ λp,p',prog,stack_sizes. mk_prog_params (make_sem_graph_params p p') prog stack_sizes. definition graph_abstract_status: ∀p:unserialized_params. (∀F.sem_unserialized_params p F) → ∀prog : joint_program (mk_graph_params p). (ident → option ℕ) → abstract_status ≝ λp,p',prog,stack_sizes. joint_abstract_status (graph_prog_params ? p' prog stack_sizes). definition lin_prog_params ≝ λp,p',prog,stack_sizes. mk_prog_params (make_sem_lin_params p p') prog stack_sizes. definition lin_abstract_status: ∀p:unserialized_params. (∀F.sem_unserialized_params p F) → ∀prog : joint_program (mk_lin_params p). (ident → option ℕ) → abstract_status ≝ λp,p',prog,stack_sizes. joint_abstract_status (lin_prog_params ? p' prog stack_sizes). (* axiom P : ∀A,B,prog.A (prog_var_names (λvars.fundef (A vars)) B prog) → Prop. check (λpars.let pars' ≝ make_global pars in λx :joint_closed_internal_function pars' (globals pars'). P … x) (* unification hint 0 ≔ p, prog, stack_sizes ; pars ≟ mk_prog_params p prog stack_sizes , pars' ≟ make_global pars, A ≟ λvars.joint_closed_internal_function p vars, B ≟ ℕ ⊢ A (prog_var_names (λvars.fundef (A vars)) B prog) ≡ joint_closed_internal_function pars' (globals pars'). *) axiom T : ∀A,B,prog.genv_t (fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) B prog))) → Prop. (*axiom Q : ∀A,B,init,prog. T … (globalenv (λvars:list ident.fundef (A vars)) B init prog) → Prop. lemma pippo : ∀p,p',prog,stack_sizes. let pars ≝ graph_prog_params p p' prog stack_sizes in let ge ≝ ev_genv pars in T ?? prog ge → Prop. #H1 #H2 #H3 #H4 #H5 whd in match (ev_genv ?) in H5; whd in match (globalenv_noinit) in H5; normalize nodelta in H5; whd in match (prog ?) in H5; whd in match (joint_function ?) in H5; @(Q … H5) λx:T ??? ge.Q ???? x) *) axiom Q : ∀A,B,init,prog,i. is_internal_function (A (prog_var_names (λvars:list ident.fundef (A vars)) B prog)) (globalenv (λvars:list ident.fundef (A vars)) B init prog) i → Prop. check (λp,p',prog,stack_sizes,i. let pars ≝ graph_prog_params p p' prog stack_sizes in let ge ≝ ev_genv pars in λx:is_internal_function (joint_closed_internal_function pars (globals pars)) ge i.Q ??? prog ? x) *) definition sigma_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p). joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) → label → option ℕ. definition sigma_pc_opt: ∀p,p'.∀graph_prog. sigma_map p graph_prog → program_counter → option program_counter ≝ λp,p',prog,sigma,pc. let pars ≝ make_sem_graph_params p p' in let ge ≝ globalenv_noinit … prog in if eqZb (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *) return pc else ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ; ! lin_point ← sigma fd (point_of_pc pars pc) ; return pc_of_point (make_sem_lin_params ? p') (pc_block pc) lin_point. definition well_formed_pc: ∀p,p',graph_prog. sigma_map p graph_prog → program_counter → Prop ≝ λp,p',prog,sigma,pc. sigma_pc_opt p p' prog sigma pc ≠ None …. definition sigma_beval_opt : ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). sigma_map p graph_prog → beval → option beval ≝ λp,p',graph_prog,sigma,bv. match bv with [ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt | _ ⇒ return bv ]. definition sigma_beval : ∀p,p',graph_prog,sigma,bv. sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝ λp,p',graph_prog,sigma,bv.opt_safe …. definition sigma_is_opt : ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). sigma_map p graph_prog → internal_stack → option internal_stack ≝ λp,p',graph_prog,sigma,is. match is with [ empty_is ⇒ return empty_is | one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv' | both_is bv1 bv2 ⇒ ! bv1' ← sigma_beval_opt p p' … sigma bv1 ; ! bv2' ← sigma_beval_opt p p' … sigma bv2 ; return both_is bv1' bv2' ]. definition sigma_is : ∀p,p',graph_prog,sigma,is. sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝ λp,p',graph_prog,sigma,is.opt_safe …. lemma sigma_is_empty : ∀p,p',graph_prog,sigma. ∀prf.sigma_is p p' graph_prog sigma empty_is prf = empty_is. #p #p' #graph_prog #sigma #prf whd in match sigma_is; normalize nodelta @opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. (* spostato in ExtraMonads.ma lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n. #X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2. ∀X,Y,P,F,v,n. ∀prf.n = return F v prf → FR X Y P F (return v) n. #M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed. lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x. #A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed. *) lemma sigma_is_pop_commute : ∀p,p',graph_prog,sigma,is. ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?. res_preserve … (λpr.sigma_beval_opt p p' graph_prog sigma (\fst pr) ≠ None ? ∧ sigma_is_opt p p' graph_prog sigma (\snd pr) ≠ None ?) (λpr,prf.〈sigma_beval … (proj1 … prf), sigma_is … (proj2 … prf)〉) (is_pop is) (is_pop (sigma_is … prf)). #p #p' #graph_prog #sigma * [|#bv1|#bv1 #bv2] #prf [ @res_preserve_error |*: whd in match sigma_is in ⊢ (?????????%); normalize nodelta @opt_safe_elim #is' #H @('bind_inversion H) -H #bv1' #EQ1 [2: #H @('bind_inversion H) -H #bv2' #EQ2 ] whd in ⊢ (??%%→?); #EQ destruct(EQ) @mfr_return_eq [1,3: @hide_prf %% |*: whd in match sigma_beval; whd in match sigma_is; normalize nodelta @opt_safe_elim #bv1'' @opt_safe_elim #is'' ] [2,4,5,6: whd in match sigma_is_opt; normalize nodelta [1,3: >EQ1 ] whd in ⊢ (??%%→?); #EQ destruct(EQ) ] [1,3: >EQ2 |*: >EQ1 ] #EQ' destruct(EQ') % ] qed. (* lemma opt_to_res_preserve : ∀X,Y.∀P : X → Y → Prop.∀e,u,v. opt_preserve P u v → res_preserve P (opt_to_res … e u) (opt_to_res … e v). #X #Y #P #e #u #v #H #x #EQ lapply (opt_eq_from_res ???? EQ) -EQ #EQ lapply (H … EQ) cases v [ * ] #y #K @K qed. lemma err_eq_from_io : ∀O,I,X,m,v. err_to_io O I X m = return v → m = return v. #O #I #X * #x #v normalize #EQ destruct % qed. lemma res_to_io_preserve : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v. res_preserve P u v → IO_preserve O I P u v. #X #Y #P #O #I #u #v #H #x #EQ lapply (err_eq_from_io ????? EQ) -EQ #EQ lapply (H … EQ) cases v [2: #e * ] #y #K @K qed. lemma preserve_opt_to_res : ∀X,Y.∀P : X → Y → Prop.∀e,u,v. res_preserve P (opt_to_res … e u) (opt_to_res … e v) → opt_preserve P u v. #X #Y #P #e #u #v #H #x #EQ lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [ * ] #y #K @K qed. lemma preserve_res_to_io : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v. IO_preserve O I P (err_to_io … u) (err_to_io … v) → res_preserve P u v. #X #Y #P #O #I #u #v #H #x #EQ lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [2: #e * ] #y #K @K qed. *) definition well_formed_mem : ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). sigma_map p graph_prog → bemem → Prop ≝ λp,p',graph_prog,sigma,m. ∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b → sigma_beval_opt p p' graph_prog sigma (contents (blocks m b) z) ≠ None ?. definition sigma_mem : ∀p,p',graph_prog,sigma,m. well_formed_mem p p' graph_prog sigma m → bemem ≝ λp,p',graph_prog,sigma,m,prf. mk_mem (λb. If Zltb (block_id b) (nextblock m) then with prf' do let l ≝ low_bound m b in let h ≝ high_bound m b in mk_block_contents l h (λz.If Zleb l z ∧ Zltb z h then with prf'' do sigma_beval p p' graph_prog sigma (contents (blocks m b) z) ? else BVundef) else empty_block OZ OZ) (nextblock m) (nextblock_pos m). @hide_prf lapply prf'' lapply prf' -prf' -prf'' @Zltb_elim_Type0 [2: #_ * ] #bid_ok * @Zleb_elim_Type0 [2: #_ * ] @Zltb_elim_Type0 [2: #_ #_ * ] #zh #zl * @(prf … bid_ok zl zh) qed. lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false. ** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed. axiom mem_ext_eq : ∀m1,m2 : mem. (∀b.let bc1 ≝ blocks m1 b in let bc2 ≝ blocks m2 b in low bc1 = low bc2 ∧ high bc1 = high bc2 ∧ ∀z.contents bc1 z = contents bc2 z) → nextblock m1 = nextblock m2 → m1 = m2. (* spostato in ExtraMonads.ma lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n. #X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. *) lemma beloadv_sigma_commute: ∀p,p',graph_prog,sigma,ptr. preserving … opt_preserve … (sigma_mem p p' graph_prog sigma) (sigma_beval p p' graph_prog sigma) (λm.beloadv m ptr) (λm.beloadv m ptr). #p #p' #graph_prog #sigma #ptr #m #prf #bv whd in match beloadv; whd in match do_if_in_bounds; whd in match sigma_mem; normalize nodelta @If_elim #block_ok >block_ok normalize nodelta [2: whd in ⊢ (???%→?); #ABS destruct(ABS) ] @If_elim #H [ elim (andb_true … H) #H1 #H2 whd in match sigma_beval; normalize nodelta @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta whd in ⊢ (???%→?); #EQ' destruct >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe | elim (andb_false … H) -H #H >H [2: >commutative_andb ] normalize nodelta whd in ⊢ (???%→?); #ABS destruct(ABS) ] qed. include alias "common/GenMem.ma". lemma bestorev_sigma_commute : ∀p,p',graph_prog,sigma,ptr. preserving2 ?? opt_preserve … (sigma_mem p p' graph_prog sigma) (sigma_beval p p' graph_prog sigma) (sigma_mem p p' graph_prog sigma) (λm.bestorev m ptr) (λm.bestorev m ptr). #p #p' #graph_prog #sigma #ptr #m #bv #prf1 #prf2 #m' whd in match bestorev; whd in match do_if_in_bounds; whd in match sigma_mem; whd in match update_block; normalize nodelta @If_elim #block_ok >block_ok normalize nodelta [2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)] @Zleb_elim_Type0 #H1 [ @Zltb_elim_Type0 #H2 ] [2,3: #ABS normalize in ABS; destruct(ABS) ] normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ) % [2: whd in ⊢ (???%); @eq_f @mem_ext_eq [2: % ] #b @if_elim [2: #B @If_elim #prf1 @If_elim #prf2 [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ] whd in match low_bound; whd in match high_bound; normalize nodelta cut (Not (bool_to_Prop (eq_block b (pblock ptr)))) [ % #ABS >ABS in B; * ] -B #B % [ >B %% ] #z @If_elim #prf3 @If_elim #prf4 [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ |4: % ] whd in match sigma_beval in ⊢ (??%%); normalize nodelta @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; >EQ2 #EQ destruct(EQ) % | #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ] #EQ destruct(EQ) @If_elim whd in match low_bound; whd in match high_bound; normalize nodelta [2: >block_ok * #ABS elim (ABS I) ] #prf3 % [ >B %% ] #z whd in match update; normalize nodelta @eqZb_elim normalize nodelta #prf4 [2: @If_elim #prf5 @If_elim #prf6 [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ |4: % ] whd in match sigma_beval in ⊢ (??%%); normalize nodelta @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; normalize nodelta >(eqZb_false … prf4) >EQ2 #EQ destruct(EQ) % | @If_elim #prf5 [2: >B in prf5; normalize nodelta >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ] whd in match sigma_beval in ⊢ (??%%); normalize nodelta @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) % ] ] | whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta @eq_block_elim #H normalize nodelta destruct #h2 #h3 whd in match update; normalize nodelta [ @eqZb_elim #H destruct normalize nodelta [ assumption ]] @prf1 assumption ] qed. record good_sem_state_sigma (p : unserialized_params) (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) (sigma : sigma_map p graph_prog) : Type[0] ≝ { well_formed_frames : framesT (make_sem_graph_params p p') → Prop ; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p') ; sigma_empty_frames_commute : ∃prf. empty_framesT (make_sem_lin_params p p') = sigma_frames (empty_framesT (make_sem_graph_params p p')) prf ; well_formed_regs : regsT (make_sem_graph_params p p') → Prop ; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p') ; sigma_empty_regsT_commute : ∀ptr.∃ prf. empty_regsT (make_sem_lin_params p p') ptr = sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf ; sigma_load_sp_commute : preserving … res_preserve … (λ_.True) … sigma_regs (λx.λ_.x) (load_sp (make_sem_graph_params p p')) (load_sp (make_sem_lin_params p p')) ; sigma_save_sp_commute : ∀reg,ptr,prf1. ∃prf2. save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr = sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2 }. definition well_formed_state : ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). ∀sigma. good_sem_state_sigma p p' graph_prog sigma → state (make_sem_graph_params p p') → Prop ≝ λp,p',graph_prog,sigma,gsss,st. well_formed_frames … gsss (st_frms … st) ∧ sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧ well_formed_regs … gsss (regs … st) ∧ well_formed_mem p p' graph_prog sigma (m … st). definition sigma_state : ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). ∀sigma. ∀gsss : good_sem_state_sigma p p' graph_prog sigma. ∀st : state (make_sem_graph_params p p'). well_formed_state … gsss st → state (make_sem_lin_params p p') ≝ λp,p',graph_prog,sigma,gsss,st,prf. mk_state … (sigma_frames p p' graph_prog sigma gsss (st_frms … st) ?) (sigma_is p p' graph_prog sigma (istack … st) ?) (carry … st) (sigma_regs … gsss (regs … st) ?) (sigma_mem p p' graph_prog sigma (m … st) ?). @hide_prf cases prf ** // qed. (* lemma sigma_is_pop_wf : ∀p,p',graph_prog,sigma,is,bv,is'. is_pop is = return 〈bv, is'〉 → sigma_is_opt p p' graph_prog sigma is ≠ None ? → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧ sigma_is_opt p p' graph_prog sigma is' ≠ None ?. cases daemon qed. *) (* lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?. [ #p #s #st #prf whd in match sigma_pc_of_status; normalize nodelta @opt_safe_elim #n lapply (refl … (int_funct_of_block (joint_closed_internal_function p) (globals p) (ev_genv p) (pblock (pc p st)))) elim (int_funct_of_block (joint_closed_internal_function p) (globals p) (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%); [ #_ #ABS normalize in ABS; destruct(ABS) ] #f #EQ >m_return_bind *) (* lemma wf_status_to_wf_pc : ∀p,p',graph_prog,stack_sizes. ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → code_point (mk_graph_params p) → option ℕ). ∀st. well_formed_status p p' graph_prog stack_sizes sigma st → well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st). #p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H qed. *) definition sigma_pc : ∀p,p',graph_prog. ∀sigma. ∀pc. ∀prf : well_formed_pc p p' graph_prog sigma pc. program_counter ≝ λp,p',graph_prog,sigma,st.opt_safe …. lemma sigma_pc_ok: ∀p,p',graph_prog. ∀sigma. ∀pc. ∀prf:well_formed_pc p p' graph_prog sigma pc. sigma_pc_opt p p' graph_prog sigma pc = Some … (sigma_pc p p' graph_prog sigma pc prf). #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed. lemma sigma_pc_irr : ∀p,p',graph_prog,sigma,pc1,pc2,prf1,prf2. pc1 = pc2 → sigma_pc p p' graph_prog sigma pc1 prf1 = sigma_pc p p' graph_prog sigma pc2 prf2. #p #p' #graph_prog #sigma #pc1 #pc2 #prf1 #prf2 #EQ destruct(EQ) % qed. definition well_formed_state_pc : ∀p,p',graph_prog,sigma. good_sem_state_sigma p p' graph_prog sigma → state_pc (make_sem_graph_params p p') → Prop ≝ λp,p',prog,sigma,gsss,st. well_formed_pc p p' prog sigma (last_pop … st) ∧ well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st. definition sigma_state_pc : ∀p. ∀p':∀F.sem_unserialized_params p F. ∀graph_prog. ∀sigma. (* let lin_prog ≝ linearise ? graph_prog in *) ∀gsss : good_sem_state_sigma p p' graph_prog sigma. ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *) well_formed_state_pc p p' graph_prog sigma gsss s → state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) ≝ λp,p',graph_prog,sigma,gsss,s,prf. let last_pop' ≝ sigma_pc … (proj1 … (proj1 … prf)) in let pc' ≝ sigma_pc … (proj2 … (proj1 … prf)) in let st' ≝ sigma_state … (proj2 … prf) in mk_state_pc ? st' pc' last_pop'. (* definition sigma_function_name : ∀p,graph_prog. let lin_prog ≝ linearise p graph_prog in (Σf.is_internal_function_of_program … graph_prog f) → (Σf.is_internal_function_of_program … lin_prog f) ≝ λp,graph_prog,f.«f, if_propagate … (pi2 … f)». *) (* spostato in ExtraMonads.ma lemma m_list_map_All_ok : ∀M : MonadProps.∀X,Y,f,l. All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'. #M #X #Y #f #l elim l -l [ * %{[ ]} % | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ' %{(y :: ys)} change with (! y ← ? ; ? = ?) >EQ >m_return_bind change with (! acc ← m_list_map ????? ; ? = ?) >EQ' @m_return_bind qed. *) definition helper_def_store__commute : ∀p,p',graph_prog,sigma. ∀X : ? → Type[0]. ∀gsss : good_sem_state_sigma p p' graph_prog sigma. ∀store : ∀p,F.∀p' : sem_unserialized_params p F. X p → beval → regsT p' → res (regsT p'). Prop ≝ λp,p',graph_prog,sigma,X,gsss,store. ∀a : X p.preserving2 … res_preserve … (sigma_beval p p' graph_prog sigma) (sigma_regs … gsss) (sigma_regs … gsss) (store … a) (store … a). definition helper_def_retrieve__commute : ∀p,p',graph_prog,sigma. ∀X : ? → Type[0]. ∀gsss : good_sem_state_sigma p p' graph_prog sigma. ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F. regsT p' → X p → res beval. Prop ≝ λp,p',graph_prog,sigma,X,gsss,retrieve. ∀a : X p. preserving … res_preserve … (sigma_regs … gsss) (sigma_beval p p' graph_prog sigma) (λr.retrieve … r a) (λr.retrieve … r a). record good_state_sigma (p : unserialized_params) (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) (sigma : sigma_map p graph_prog) : Type[0] ≝ { gsss :> good_sem_state_sigma p p' graph_prog sigma ; acca_store__commute : helper_def_store__commute … gsss acca_store_ ; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_ ; acca_arg_retrieve_commute : helper_def_retrieve__commute … gsss acca_arg_retrieve_ ; accb_store_commute : helper_def_store__commute … gsss accb_store_ ; accb_retrieve_commute : helper_def_retrieve__commute … gsss accb_retrieve_ ; accb_arg_retrieve_commute : helper_def_retrieve__commute … gsss accb_arg_retrieve_ ; dpl_store_commute : helper_def_store__commute … gsss dpl_store_ ; dpl_retrieve_commute : helper_def_retrieve__commute … gsss dpl_retrieve_ ; dpl_arg_retrieve_commute : helper_def_retrieve__commute … gsss dpl_arg_retrieve_ ; dph_store_commute : helper_def_store__commute … gsss dph_store_ ; dph_retrieve_commute : helper_def_retrieve__commute … gsss dph_retrieve_ ; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_ ; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_ ; pair_reg_move_commute : ∀mv. preserving … res_preserve … (sigma_regs … gsss) (sigma_regs … gsss) (λr.pair_reg_move_ ? ? (p' ?) r mv) (λr.pair_reg_move_ ? ? (p' ?) r mv) ; allocate_locals__commute : ∀loc, r1, prf1. ∃ prf2. allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) = sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2 ; save_frame_commute : ∀dest,fl. preserving … res_preserve … (sigma_state_pc … gsss) (sigma_state … gsss) (save_frame ?? (p' ?) fl dest) (save_frame ?? (p' ?) fl dest) ; eval_ext_seq_commute : let lin_prog ≝ linearise p graph_prog in ∀ stack_sizes. ∀ext,i,fn. preserving … res_preserve … (sigma_state … gsss) (sigma_state … gsss) (eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) ext i fn) (eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) ext i (\fst (linearise_int_fun … fn))) ; setup_call_commute : ∀ n , parsT, call_args. preserving … res_preserve … (sigma_state … gsss) (sigma_state … gsss) (setup_call ?? (p' ?) n parsT call_args) (setup_call ?? (p' ?) n parsT call_args) ; fetch_external_args_commute : (* TO BE CHECKED *) ∀ex_fun,st1,prf1,call_args. fetch_external_args ?? (p' ?) ex_fun st1 call_args = fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args ; set_result_commute : ∀ l , call_dest. preserving … res_preserve … (sigma_state … gsss) (sigma_state … gsss) (set_result ?? (p' ?) l call_dest) (set_result ?? (p' ?) l call_dest) ; read_result_commute : let lin_prog ≝ linearise p graph_prog in ∀stack_sizes. ∀call_dest. preserving … res_preserve … (sigma_state … gsss) (λl,prf.opt_safe ? (m_list_map … (sigma_beval_opt p p' graph_prog sigma) l) prf) (read_result ?? (p' ?) ? (ev_genv (graph_prog_params … graph_prog stack_sizes)) call_dest) (read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) call_dest) ; pop_frame_commute : let lin_prog ≝ linearise p graph_prog in ∀stack_sizes, curr_id , curr_fn. preserving … res_preserve … (sigma_state … gsss) (sigma_state_pc … gsss) (pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) curr_id curr_fn) (pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) curr_id (\fst (linearise_int_fun … curr_fn))) }. lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r. well_formed_state p p' graph_prog sigma gss st → well_formed_regs … gss r → well_formed_state … gss (set_regs … r st). #p #p' #graph_prog #sigma #gss #st #r *** #H1 #H2 #_ #H4 #H3 %{H4} %{H3} %{H2} @H1 qed. lemma allocate_locals_def : ∀p,F,p',loc,locs,st. allocate_locals p F p' (loc::locs) st = (let st' ≝ allocate_locals p F p' locs st in set_regs … (allocate_locals_ p F p' loc (regs … st')) st'). #p #F #p' #loc #locs #st % qed. lemma allocate_locals_commute : ∀p,p',graph_prog,sigma. ∀gss : good_state_sigma p p' graph_prog sigma. ∀locs, st1, prf1. ∃ prf2. allocate_locals ? ? (p' ?) locs (sigma_state … gss st1 prf1) = sigma_state … gss (allocate_locals ? ? (p' ?) locs st1) prf2. #p #p' #gp #sigma #gss #locs elim locs -locs [ #st1 #prf1 %{prf1} % ] #loc #tl #IH #st1 #prf1 letin st2 ≝ (sigma_state … st1 prf1) cases (IH st1 prf1) letin st1' ≝ (allocate_locals ??? tl st1) letin st2' ≝ (allocate_locals ??? tl st2) #prf' #EQ' cases (allocate_locals__commute … gss loc (regs … st1') ?) [2: @hide_prf cases prf' ** // ] #prf'' #EQ'' % [ @hide_prf @wf_set_regs assumption ] change with (set_regs ? (allocate_locals_ ??? loc (regs ? st1')) st1') in match (allocate_locals ??? (loc::tl) st1); change with (set_regs ? (allocate_locals_ ??? loc (regs ? st2')) st2') in match (allocate_locals ??? (loc::tl) st2); >EQ' >EQ'' % qed. lemma store_commute : ∀p,p',graph_prog,sigma. ∀X : ? → Type[0]. ∀store. ∀gsss : good_state_sigma p p' graph_prog sigma. ∀H : helper_def_store__commute … gsss store. ∀a : X p. preserving2 … res_preserve … (sigma_beval p p' graph_prog sigma) (sigma_state … gsss) (sigma_state … gsss) (helper_def_store ? store … a) (helper_def_store ? store … a). #p #p' #graph_prog #sigma #X #store #gsss #H #a #bv #st #prf1 #prf2 @(mfr_bind … (sigma_regs … gsss)) [@H] #r #prf3 @mfr_return cases st in prf2; #frms #is #carry #r' #m *** #H1 #H2 #H3 #H4 %{H4} % [%{H1 H2}] assumption qed. lemma retrieve_commute : ∀p,p',graph_prog,sigma. ∀X : ? → Type[0]. ∀retrieve. ∀gsss : good_sem_state_sigma p p' graph_prog sigma. ∀H : helper_def_retrieve__commute … gsss retrieve. ∀a : X p . preserving … res_preserve … (sigma_state … gsss) (sigma_beval p p' graph_prog sigma) (λst.helper_def_retrieve ? retrieve … st a) (λst.helper_def_retrieve ? retrieve … st a). #p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #prf @H qed. (* definition acca_store_commute : ∀p,p',graph_prog,sigma. ∀gss : good_state_sigma p p' graph_prog sigma. ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'. acca_store … a bv st = return st' → ∃prf2. acca_store … a (sigma_beval p p' graph_prog sigma bv prf1') (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝ λp,p',graph_prog,sigma. λgss : good_state_sigma p p' graph_prog sigma. store_commute … gss (acca_store__commute … gss). *) (* restano: ; setup_call : nat → paramsT … uns_pars → call_args uns_pars → state st_pars → res (state st_pars) ; fetch_external_args: external_function → state st_pars → call_args … uns_pars → res (list val) ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars) (* from now on, parameters that use the type of functions *) ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval) (* change of pc must be left to *_flow execution *) ; pop_frame: ∀globals.∀ge : genv_gen F globals. (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars) *) (* lemma sigma_pc_commute: ∀p,p',graph_prog,sigma,gss,st. ∀prf : well_formed_state_pc p p' graph_prog sigma gss st. sigma_pc … (pc ? st) (proj1 … prf) = pc ? (sigma_state_pc … st prf). // qed. *) (* lemma if_of_function_commute: ∀p. ∀graph_prog : joint_program (mk_graph_params p). ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i. let graph_fd ≝ if_of_function … graph_fun in let lin_fun ≝ sigma_function_name … graph_fun in let lin_fd ≝ if_of_function … lin_fun in lin_fd = \fst (linearise_int_fun ?? graph_fd). #p #graph_prog #graph_fun whd @prog_if_of_function_transform % qed. *) lemma pc_block_sigma_commute : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀sigma,pc. ∀prf : well_formed_pc p p' graph_prog sigma pc. pc_block (sigma_pc ? p' graph_prog sigma pc prf) = pc_block pc. #p #p' #graph_prog #sigma #pc #prf whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta @opt_safe_elim #x @if_elim #_ [2: #H @('bind_inversion H) -H * #i #fn #_ #H @('bind_inversion H) -H #n #_ ] whd in ⊢ (??%?→?); #EQ destruct % qed. (* lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B. (! x ← m ; g x) ≠ None ? → m ≠ None ?. #A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize [ #abs elim abs -abs #abs @abs % | #abs elim abs -abs #abs #v @abs % ] qed. lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A. ∀ b : B .∀ f : A → B. ∀g : B → option C. g (match m with [None ⇒ b | Some x ⇒ f x])≠ None ? → g b = None ? → m ≠ None ?. #A #B #C #m #x #b #f #g #H1 #H2 % #m_eq_none >m_eq_none in H1; normalize #H elim H -H #H @H assumption qed. *) (* lemma funct_of_block_transf : ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. ∀transf : ∀vars. A vars → B vars. ∀bl,f,prf. let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in funct_of_block … (globalenv_noinit … progr) bl = return f → funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf». #A #B #progr #transf #bl #f #prf whd whd in match funct_of_block in ⊢ (%→?); normalize nodelta cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. ∀o.∀prf : Q o. ∀f1,f2. (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) → P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) [ #A #B #Q #P * /2/ ] #aux @aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ] #fd #EQfind whd in ⊢ (??%%→?); generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ) whd in match funct_of_block; normalize nodelta @aux [ # fd' ] [2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ] #prf' cases daemon qed. lemma description_of_function_transf : ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. ∀transf : ∀vars. A vars → B vars. let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in ∀f_out,prf. description_of_function … (globalenv_noinit … progr') f_out = transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr) «pi1 … f_out, prf»). #A #B #progr #transf #f_out #prf whd in match description_of_function in ⊢ (???%); normalize nodelta cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. ∀o.∀prf : Q o. ∀f1,f2. (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) → P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) [ #A #B #Q #P * /2/ ] #aux @aux [ #fd' ] * #fd #EQ destruct (EQ) inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] #bl #EQfind >m_return_bind #EQfindf whd in match description_of_function; normalize nodelta @aux [ #fdo' ] * #fdo #EQ destruct (EQ) >find_symbol_transf >EQfind >m_return_bind >(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) % qed. lemma match_int_fun : ∀A,B : Type[0].∀P : B → Prop. ∀Q : fundef A → Prop. ∀m : fundef A. ∀f1 : ∀fd.Q (Internal \ldots fd) → B. ∀f2 : ∀fd.Q (External … fd) → B. ∀prf : Q m. (∀fd,prf.P (f1 fd prf)) → (∀fd,prf.P (f2 fd prf)) → P (match m return λx.Q x → ? with [ Internal fd ⇒ f1 fd | External fd ⇒ f2 fd ] prf). #A #B #P #Q * // qed. (*) lemma match_int_fun : ∀A,B : Type[0].∀P : B → Prop. ∀m : fundef A. ∀f1 : ∀fd.m = Internal … fd → B. ∀f2 : ∀fd.m = External … fd → B. (∀fd,prf.P (f1 fd prf)) → (∀fd,prf.P (f2 fd prf)) → P (match m return λx.m = x → ? with [ Internal fd ⇒ f1 fd | External fd ⇒ f2 fd ] (refl …)). #A #B #P * // qed. *) (* lemma prova : ∀ A.∀progr : program (λvars. fundef (A vars)) ℕ. ∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)). ∀ f,g,prf1. match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with [Internal fn ⇒ λ prf.return «g,prf1 fn prf» | External fn ⇒ λprf.None ? ] (refl ? M) = return f → ∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf». #H1 #H2 #H3 #H4 #H5 #H6 @match_int_fun #fd #EQ #EQ' whd in EQ' : (??%%); destruct %[|%[| % ]] qed. *) lemma int_funct_of_block_transf: ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ. ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf. let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in int_funct_of_block ? (globalenv_noinit … progr) bl = return f → int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf». #A #B #progr #transf #bl #f #prf whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta @'bind_inversion #x #x_spec @match_int_fun [2: #fd #_ #ABS destruct(ABS) ] #fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ) whd in match int_funct_of_block; normalize nodelta >(funct_of_block_transf … (internal_function_is_function … prf) … x_spec) >m_return_bind @match_int_fun #fd' #prf' [ % ] @⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr >(description_of_function_transf) [2: @x_prf ] >EQdescr whd in ⊢ (??%%→?); #ABS destruct qed. *) lemma symbol_for_block_match: ∀M:matching.∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). ∀MATCH:match_program … M p p'. ∀b: block. symbol_for_block … (globalenv … initW p') b = symbol_for_block … (globalenv … initV p) b. * #A #B #V #W #match_fn #match_var #initV #initW #H #p #p' * #Mvars #Mfn #Mmain #b whd in match symbol_for_block; normalize nodelta whd in match globalenv in ⊢ (???%); normalize nodelta whd in match (globalenv_allocmem ????); change with (add_globals ?????) in match (foldl ?????); >(proj1 … (add_globals_match … initW … Mvars)) [ % |*:] [ * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(H … MVE) ] | @(matching_fns_get_same_blocks … Mfn) #f #g @match_funct_entry_id ] qed. lemma symbol_for_block_transf : ∀A,B,V,init.∀prog_in : program A V. ∀trans : ∀vars.A vars → B vars. let prog_out ≝ transform_program … prog_in trans in ∀bl. symbol_for_block … (globalenv … init prog_out) bl = symbol_for_block … (globalenv … init prog_in) bl. #A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?)) #v0 #w0 * // qed. lemma fetch_function_transf : ∀A,B,V,init.∀prog_in : program A V. ∀trans : ∀vars.A vars → B vars. let prog_out ≝ transform_program … prog_in trans in ∀bl,i,f. fetch_function … (globalenv … init prog_in) bl = return 〈i, f〉 → fetch_function … (globalenv … init prog_out) bl = return 〈i, trans … f〉. #A #B #V #init #prog_in #trans #bl #i #f whd in match fetch_function; normalize nodelta #H lapply (opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #id #eq_symbol_for_block #H @('bind_inversion H) -H #fd #eq_find_funct whd in ⊢ (??%?→?); #EQ destruct(EQ) >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind >(find_funct_ptr_transf A B … eq_find_funct) % qed. lemma fetch_internal_function_transf : ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ. ∀trans : ∀vars.A vars → B vars. let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in ∀bl,i,f. fetch_internal_function … (globalenv_noinit … prog_in) bl = return 〈i, f〉 → fetch_internal_function … (globalenv_noinit … prog_out) bl = return 〈i, trans … f〉. #A #B #prog #trans #bl #i #f whd in match fetch_internal_function; normalize nodelta #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch whd in ⊢ (??%%→?); #EQ destruct(EQ) >(fetch_function_transf … EQfetch) % qed. (* #H elim (bind_opt_inversion ????? H) -H #x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta @match_opt_prf_elim #H #H1 whd in H : (??%?); cases ( find_funct_ptr (fundef (joint_closed_internal_function (graph_prog_params p p' graph_prog (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') (linearise_int_fun p) graph_prog stack_sizes)) (globals (graph_prog_params p p' graph_prog (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') (linearise_int_fun p) graph_prog stack_sizes))))) (ev_genv (graph_prog_params p p' graph_prog (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') (linearise_int_fun p) graph_prog stack_sizes))) (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct normalize nodelta #H #H1 cases ( find_funct_ptr (fundef (joint_closed_internal_function (graph_prog_params p p' graph_prog (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') (linearise_int_fun p) graph_prog stack_sizes)) (globals (graph_prog_params p p' graph_prog (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') (linearise_int_fun p) graph_prog stack_sizes))))) (ev_genv (graph_prog_params p p' graph_prog (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') (linearise_int_fun p) graph_prog stack_sizes))) (pblock (pc (make_sem_graph_params p p') st))) in H; check find_funct_ptr_transf whd in match int_funct_of_block; normalize nodelta #H elim (bind_inversion ????? H) .. sigma_int_funct_of_block whd in match int_funct_of_block; normalize nodelta elim (bind_inversion ????? H) whd in match int_funct_of_block; normalize nodelta #H elim (bind_inversion ????? H) -H #fn * #H lapply (opt_eq_from_res ???? H) -H #H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H) -H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%); destruct // cases daemon qed. *) lemma stmt_at_sigma_commute: ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma. good_local_sigma p globals graph_code entry lin_code sigma → code_closed … lin_code → sigma lbl = return pt → ∀stmt. stmt_at … graph_code lbl = return stmt → All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧ match stmt with [ final s' ⇒ stmt_at … lin_code pt = Some ? (final … s') | sequential s' nxt ⇒ match s' with [ step_seq _ ⇒ (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧ ((sigma nxt = Some ? (S pt)) ∨ (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt) ∧ point_of_label … lin_code nxt = sigma nxt) ) | COND a ltrue ⇒ (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S pt)) ∨ (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt) ∧ point_of_label … lin_code nxt = sigma nxt) ] | FCOND abs _ _ _ ⇒ Ⓧabs ]. #p #globals #graph_code #entry #lin_code #lbl #pt #sigma ** #_ #all_labels_in #lin_stmt_spec #lin_code_closed #prf elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 ** #stmt1_spec #All_succs_in #next_spec #stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ) % [assumption] cases stmt in next_spec; -stmt [ * [ #s | #a #lbl ] #nxt | #s | * ] normalize nodelta [ * #H #G %{H} cases G -G #G [ %1{G} ] | * [ #H %1{H} ] #G | // ] %2 %{G} lapply (refl … (point_of_label … lin_code nxt)) change with (If ? then with prf do ? else ?) in ⊢ (???%→?); @If_elim <(lin_code_has_label … (mk_lin_params p)) [1,3: #_ #EQ >EQ >(all_labels_in … EQ) % ] * #H cases (H ?) -H lapply (lin_code_closed … G) ** [2: #_ * ] // qed. (* >(if_of_function_commute … graph_fun) check opt_Exists check linearise_int_fun check whd in match (stmt_at ????); whd in match (stmt_at ????); cases (linearise_code_spec … p' graph_prog graph_fun (joint_if_entry … graph_fun)) * #lin_code_closed #sigma_entry_is_zero #sigma_spec lapply (sigma_spec (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1))) -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ] -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec; inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_ #related_lin_stm_graph_stm #_ lin_lookup_ok // *) definition good_sigma : ∀p.∀graph_prog : joint_program (mk_graph_params p). (joint_closed_internal_function ? (prog_var_names … graph_prog) → label → option ℕ) → Prop ≝ λp,graph_prog,sigma. ∀fn : joint_closed_internal_function (mk_graph_params p) ?. good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn) (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn). lemma pc_of_label_sigma_commute : ∀p,p',graph_prog,bl,lbl,i,fn. let lin_prog ≝ linearise ? graph_prog in ∀sigma.good_sigma p graph_prog sigma → fetch_internal_function … (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 → let pc' ≝ pc_of_point (make_sem_graph_params p p') … bl lbl in code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl → ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) bl lbl = return sigma_pc p p' graph_prog sigma pc' prf'. #p #p' #graph_prog #bl #lbl #i #fn #sigma #good cases (good fn) -good * #_ #all_labels_in #good #fetchfn >lin_code_has_label #lbl_in whd in match pc_of_label; normalize nodelta > (fetch_internal_function_transf … fetchfn) >m_return_bind inversion (point_of_label ????) [ (* change with (If ? then with prf do ? else ? = ? → ?) @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ] *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS) | #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind % [ @hide_prf whd % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' ] whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #Hbl normalize nodelta [1,3: >(fetch_internal_function_no_minus_one … Hbl) in fetchfn; |*: >fetchfn >m_return_bind >point_of_pc_of_point >EQsigma ] whd in ⊢ (??%%→?); #EQ destruct(EQ) % ] qed. lemma graph_pc_of_label : ∀p,p'.let pars ≝ make_sem_graph_params p p' in ∀globals,ge,bl,i_fn,lbl. fetch_internal_function ? ge bl = return i_fn → pc_of_label pars globals ge bl lbl = OK ? (pc_of_point pars bl lbl). #p #p' #globals #ge #bl #fn #lbl #fetchfn whd in match pc_of_label; normalize nodelta >fetchfn % qed. lemma point_of_pc_sigma_commute : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀sigma,pc,f,fn,n. ∀prf : well_formed_pc p p' graph_prog sigma pc. fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 → sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n → point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n. #p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #Hbl [ >(fetch_internal_function_no_minus_one … Hbl) in EQfetch; whd in ⊢ (???%→?); #ABS destruct(ABS) ] >EQfetch >m_return_bind >EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ) @point_of_offset_of_point qed. lemma graph_succ_pc : ∀p,p'.let pars ≝ make_sem_graph_params p p' in ∀pc,lbl. succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl. normalize // qed. lemma fetch_statement_sigma_commute: ∀p,p',graph_prog,pc,f,fn,stmt. let lin_prog ≝ linearise ? graph_prog in ∀sigma.good_sigma p graph_prog sigma → ∀prf : well_formed_pc p p' graph_prog sigma pc. fetch_statement (make_sem_graph_params p p') … (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl). pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (pc_block pc) lbl = return sigma_pc … prf) (stmt_explicit_labels … stmt) ∧ match stmt with [ sequential s nxt ⇒ match s with [ step_seq x ⇒ fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈f, \fst (linearise_int_fun … fn), sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧ ∃prf'. let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in (nxt_pc = sigma_nxt ∨ (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) nxt_pc = return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 ∧ (pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (pc_block pc) nxt = return sigma_nxt))) | COND a ltrue ⇒ ∃prf'. let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈f, \fst (linearise_int_fun … fn), sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧ nxt_pc = sigma_nxt)) ∨ (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧ pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (pc_block pc) nxt = return sigma_nxt) ] | final z ⇒ fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … z〉 | FCOND abs _ _ _ ⇒ Ⓧabs ]. #p #p' #graph_prog #pc #f #fn #stmt #sigma #good elim (good fn) * #_ #all_labels_in #good_local #wfprf #H elim (fetch_statement_inv … H) #fetchfn #graph_stmt whd in match well_formed_pc in wfprf; normalize nodelta in wfprf; inversion(sigma_pc_opt p p' graph_prog sigma pc) [#ABS @⊥ >ABS in wfprf; * #H @H %] #lin_pc whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta in ⊢ (%→?); @eqZb_elim #Hbl [ >(fetch_internal_function_no_minus_one … Hbl) in fetchfn; #ABS destruct(ABS) ] normalize nodelta >fetchfn >m_return_bind #H @('bind_inversion H) -H #lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ) lapply(stmt_at_sigma_commute ???????? (good fn) ??? graph_stmt) [@lin_pt_spec|@(pi2 … (\fst (linearise_int_fun … fn)))|] * #H1 #H2 % [ cases stmt in H2; [ * [#s|#a#lbl]#nxt | #s | *] normalize nodelta [ * #stmt_at_EQ #_ | ** #stmt_at_EQ #_ | #stmt_at_EQ ] cases (pi2 … (\fst (linearise_int_fun … fn)) … stmt_at_EQ) #H #_ [1,2,4: @(All_mp … H) #lbl @(pc_of_label_sigma_commute … good … fetchfn) |3: cases H -H #H #_ %{I} @(pc_of_label_sigma_commute … good … fetchfn) @H ] ] cases (stmt) in H1 H2; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta #all_labels_spec #H3 whd in match fetch_statement; normalize nodelta >pc_block_sigma_commute >(fetch_internal_function_transf … fetchfn) >m_return_bind >(point_of_pc_sigma_commute … fetchfn lin_pt_spec) [ % [ >(proj1 … H3) % | % [ @hide_prf % | change with (opt_safe ???) in match (sigma_pc ???? (succ_pc ???) ?); @opt_safe_elim #pc1 ] whd in match sigma_pc_opt; normalize nodelta >(eqZb_false … Hbl) >fetchfn >m_return_bind >graph_succ_pc >point_of_pc_of_point cases(proj2 … H3) [1,3: #EQ >EQ |*: * cases all_labels_spec #Z #_ #sn >(opt_to_opt_safe … Z) #EQpoint_of_label ] whd in ⊢ (??%?→?); #EQ destruct(EQ) [ %1 whd in match (point_of_succ ???) ; whd in match point_of_pc; normalize nodelta whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta @opt_safe_elim >(eqZb_false … Hbl) >fetchfn >m_return_bind >lin_pt_spec #pc' whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in match succ_pc; whd in match point_of_pc; normalize nodelta >point_of_offset_of_point % | %2 whd in match (pc_block ?); >pc_block_sigma_commute >(fetch_internal_function_transf … fetchfn) >m_return_bind whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta #pc_lin >fetchfn >m_return_bind >lin_pt_spec >m_return_bind whd in match pc_of_point; normalize nodelta #EQ whd in EQ : (??%?); destruct whd in match point_of_pc; whd in match succ_pc; normalize nodelta whd in match point_of_pc; normalize nodelta >point_of_offset_of_point whd in match pc_of_point; normalize nodelta >point_of_offset_of_point >sn >m_return_bind % [%] whd in match pc_of_label; normalize nodelta >(fetch_internal_function_transf … fetchfn) >m_return_bind >EQpoint_of_label % ] ] | % [ @hide_prf % whd in match sigma_pc_opt; normalize nodelta >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?); >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta whd in match pc_of_point; whd in match point_of_pc; normalize nodelta >point_of_offset_of_point cases all_labels_spec #H >(opt_to_opt_safe … H) #_ >m_return_bind #ABS whd in ABS : (??%?); destruct(ABS)] cases H3 * #nxt_spec #point_of_lab_spec >nxt_spec >m_return_bind [%1 % [%] whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta @opt_safe_elim #lin_pc1 @opt_safe_elim #lin_pc2 >(eqZb_false … Hbl) normalize nodelta >fetchfn >m_return_bind >m_return_bind in ⊢ (? → % → ?); whd in match point_of_pc; whd in match succ_pc; normalize nodelta whd in match pc_of_point; whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >point_of_lab_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) >point_of_offset_of_point % |%2 >m_return_bind >nxt_spec >m_return_bind %[%] whd in match pc_of_label; normalize nodelta >(fetch_internal_function_transf … fetchfn) >m_return_bind >point_of_lab_spec cases all_labels_spec #H #INUTILE >(opt_to_opt_safe … H) in ⊢ (??%?); >m_return_bind normalize in ⊢ (??%?); whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?); >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta whd in match point_of_pc; whd in match pc_of_point; normalize nodelta >point_of_offset_of_point cases (sigma fn nxt) in H; [ * #ABS @⊥ @ABS %] #linear_point * #INUTILE1 #linear_pc >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) normalize nodelta % ] | >H3 >m_return_bind % ] qed. (* spostato in ExtraMonads.ma lemma res_eq_from_opt : ∀A,m,a. res_to_opt A m = return a → m = return a. #A #m #a cases m #x normalize #EQ destruct(EQ) % qed. lemma res_to_opt_preserve : ∀X,Y,P,F,m,n. res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n). #X #Y #P #F #m #n #H #x #EQ cases (H x ?) [ #prf #EQ' %{prf} >EQ' % | cases m in EQ; normalize #x #EQ destruct % ] qed. *) lemma sigma_pc_exit : ∀p,p',graph_prog,sigma,pc,prf. let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in pc = exit → sigma_pc p p' graph_prog sigma pc prf = exit. #p #p' #graph_prog #sigma #pc #prf whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' #EQ1 #EQ2 destruct whd in match sigma_pc_opt in EQ1; whd in EQ1 : (??%?); destruct % qed. (* this should make things easier for ops using memory (where pc cant happen) *) definition bv_no_pc : beval → Prop ≝ λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ]. lemma bv_pc_other : ∀P : beval → Prop. (∀pc,p.P (BVpc pc p)) → (∀bv.bv_no_pc bv → P bv) → ∀bv.P bv. #P #H1 #H2 * /2/ qed. lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf. bv_no_pc bv → sigma_beval p p' graph_prog sigma bv prf = bv. #p #p' #graph_prog #sigma * [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] #prf * whd in match sigma_beval; normalize nodelta @opt_safe_elim #bv' normalize #EQ destruct(EQ) % qed. lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv. bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?. #p #p' #graph_prog #sigma * [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] * % whd in ⊢ (??%?→?); #ABS destruct(ABS) qed. lemma Byte_of_val_inv : ∀bv,e,by.Byte_of_val e bv = return by → bv = BVByte by. * [|| #a #b #c |#p | #p | #p #pa | #p #pa ] #e #by whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. lemma sigma_pc_no_exit : ∀p,p',graph_prog,sigma,pc,prf. let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in pc ≠ exit → sigma_pc p p' graph_prog sigma pc prf ≠ exit. #p #p' #graph_prog #sigma #pc #prf @(eqZb_elim (block_id (pc_block pc)) (-1)) [ #Hbl whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' whd in match sigma_pc_opt; normalize nodelta >Hbl whd in ⊢ (??%?→?); #EQ destruct(EQ) // ] #NEQ #_ inversion (sigma_pc ??????) ** #r #id #EQr #off #EQ lapply (pc_block_sigma_commute …prf) >EQ #EQ' >EQ' % #ABS destruct(ABS) cases NEQ #H @H -H cases (pc_block ?) in e0; * #r #id' #EQ'' >EQ'' #EQ''' destruct(EQ''') % qed. definition linearise_status_rel: ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀stack_sizes. ∀sigma. ∀ gss : good_state_sigma p p' graph_prog sigma. good_sigma p graph_prog sigma → status_rel (graph_abstract_status p p' graph_prog stack_sizes) (lin_abstract_status p p' lin_prog stack_sizes) ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good. mk_status_rel … (* sem_rel ≝ *) (λs1,s2. ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1. s2 = sigma_state_pc … s1 prf) (* call_rel ≝ *) (λs1,s2. ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1. pc ? s2 = sigma_pc … (pc ? s1) (proj2 … (proj1 … prf))) (* sim_final ≝ *) ?. #st1 #st2 * #prf #EQ2 % [2: cases daemon] >EQ2 whd in ⊢ (%→%); #H lapply (opt_to_opt_safe … H) @opt_safe_elim -H #res #_ whd in match is_final; normalize nodelta #H lapply(res_eq_from_opt ??? H) -H #H @('bind_inversion H) -H ** #id #int_f #stmt #stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj2 … (proj1 … prf)) stmt_spec) cases stmt in stmt_spec; -stmt normalize nodelta [1,3: [ #a #b #_| #a #b #c #d #e] #_ #_ #ABS whd in ABS : (???%); destruct(ABS)] * normalize nodelta [1,3: [#l| #a #b #c] #_ #_ #_ #ABS whd in ABS: (???%); destruct(ABS)] #fetch_graph_spec #_ #fetch_lin_spec #H >fetch_lin_spec >m_return_bind normalize nodelta letin graph_ge ≝ (ev_genv (graph_prog_params p p' graph_prog stack_sizes)) letin lin_ge ≝ (ev_genv (lin_prog_params p p' (linearise p graph_prog) stack_sizes)) cut (preserving … res_preserve … (sigma_state … gss) (λl.λ_ : True.l) (λst. do st' ← pop_frame … graph_ge id int_f st; if eq_program_counter (pc … st') exit_pc then do vals ← read_result … graph_ge (joint_if_result … int_f) st ; Word_of_list_beval vals else Error ? [ ]) (λst. do st' ← pop_frame … lin_ge id (\fst (linearise_int_fun … int_f)) st; if eq_program_counter (pc … st') exit_pc then do vals ← read_result … lin_ge (joint_if_result … (\fst (linearise_int_fun … int_f))) st ; Word_of_list_beval vals else Error ? [ ])) [ #st #prf @mfr_bind [3: @pop_frame_commute |*:] #st' #prf' @eq_program_counter_elim [ #EQ_pc normalize nodelta change with (sigma_pc ??????) in match (pc ??); >(sigma_pc_exit … EQ_pc) normalize nodelta @mfr_bind [3: @read_result_commute |*:] #lbv #prf_lbv @opt_safe_elim #lbv' #EQ_lbv' @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) [ | * -lbv -lbv' #by1 #lbv #lbv_prf @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) [ @opt_safe_elim #lbv' #EQ_lbv' |* -lbv #by2 #lbv #lbv_prf @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) [ @opt_safe_elim #lbv' #EQ_lbv' |* -lbv #by3 #lbv #lbv_prf @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) [ @opt_safe_elim #lbv' #EQ_lbv' |* -lbv #by4 * [2: #by5 #tl #lbv_prf @res_preserve_error ] #lbv_prf @mfr_return % ]]]] cases lbv in EQ_lbv'; try (#H @res_preserve_error) -lbv #by1 #lbv #H @('bind_inversion H) -H #by1' #EQby1' #H @('bind_inversion H) -H #tl' #EQtl' whd in ⊢ (??%?→?); #EQ destruct(EQ) @(mfr_bind … (λby.λ_:True.by)) [1,3,5,7: #by #EQ %{I} >(Byte_of_val_inv … EQ) in EQby1'; whd in ⊢ (??%%→?); #EQ destruct(EQ) % |*: #by1 * @mfr_return_eq change with (m_list_map ????? = ?) in EQtl'; [1,3,5,7: % |*: @opt_safe_elim #lbv'' ] >EQtl' #EQ destruct % ] | #_ @res_preserve_error ] ] #PRESERVE cases (PRESERVE … (proj2 … prf) … H) * #EQ >EQ % whd in ⊢ (??%?→?); #ABS destruct(ABS) qed. lemma as_label_sigma_commute : ∀p,p',graph_prog,stack_sizes,sigma,gss.good_sigma p graph_prog sigma → ∀st,prf. as_label (lin_abstract_status p p' (linearise … graph_prog) stack_sizes) (sigma_state_pc p p' graph_prog sigma gss st prf) = as_label (graph_abstract_status p p' graph_prog stack_sizes) st. #p #p' #graph_prog #stack_sizes #sigma #gss #good * #st #pc #popped ** #prf1 #prf2 #prf3 change with (as_label_of_pc ?? = as_label_of_pc ??) change with (sigma_pc ??????) in match (as_pc_of ??); change with pc in match (as_pc_of ??); whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #Hbl normalize nodelta [ whd in ⊢ (??%%→??%%); #EQ destruct(EQ) whd in match fetch_statement; normalize nodelta >(fetch_internal_function_no_minus_one … graph_prog … Hbl) >(fetch_internal_function_no_minus_one … (linearise … graph_prog) … Hbl) % | #H @('bind_inversion H) * #i #f -H inversion (fetch_internal_function … (pc_block pc)) [2: #e #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] * #i' #f' #EQfetch whd in ⊢ (??%%→?); #EQ destruct(EQ) #H @('bind_inversion H) #n #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in ⊢ (??%%); whd in match fetch_statement; normalize nodelta >EQfetch >(fetch_internal_function_transf … graph_prog (λvars,fn.\fst (linearise_int_fun … fn)) … EQfetch) >m_return_bind >m_return_bind cases (good f) * #_ #all_labels_in #spec cases (spec … EQsigma) #s ** cases s -s [ * [#s|#a#lbl]#nxt|#s|*] normalize nodelta #EQstmt_at #_ [ * #EQstmt_at' #_ | * [ * #EQstmt_at' #_ | #EQstmt_at' ] | #EQstmt_at' ] whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >EQstmt_at >EQstmt_at' normalize nodelta % qed. lemma set_istack_sigma_commute : ∀p,p',graph_prog,sigma,gss,st,is,prf1,prf2,prf3. set_istack ? (sigma_is p p' graph_prog sigma is prf1) (sigma_state p p' graph_prog sigma gss st prf2) = sigma_state ???? gss (set_istack ? is st) prf3. #p #p' #graph_prog #sigma #gss * #frms #is' #carry #r #m #is #prf1 #prf2 #prf3 % qed. (* #st #is #sigmais #prf1 #prf2 #H whd in match set_istack; normalize nodelta whd in match sigma_state; normalize nodelta whd in match sigma_is; normalize nodelta @opt_safe_elim #x #H1 cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %] #EQ >EQ // qed.*) lemma is_push_sigma_commute : ∀ p, p', graph_prog,sigma. preserving2 … res_preserve … (sigma_is p p' graph_prog sigma) (sigma_beval p p' graph_prog sigma) (sigma_is p p' graph_prog sigma) is_push is_push. #p #p' #graph_prog #sigma * [ | #bv1 | #bv1 #bv2 ] #val #prf1 #prf2 #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in match sigma_beval; normalize nodelta @opt_safe_elim #val' #EQsigma_val % [1,3: @hide_prf % |*: whd in match sigma_is in ⊢ (???%); normalize nodelta @opt_safe_elim #is'' ] whd in match sigma_is_opt; normalize nodelta [2,4: inversion (sigma_beval_opt ?????) [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1; normalize nodelta * #H @H % ] #bv1' #EQ_bv1' >m_return_bind ] >EQsigma_val whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in match sigma_is; normalize nodelta @opt_safe_elim #is1 whd in match sigma_is_opt; normalize nodelta [ #H @('bind_inversion H) #bv1'' >EQ_bv1' #EQ destruct(EQ) ] whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. lemma Bit_of_val_inv : ∀e,bb,v.Bit_of_val e bb = return v → bb = BBbit v. #e * [ #b || #b #ptr #p #o ] #v whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. lemma beopaccs_sigma_commute : ∀p,p',graph_prog,sigma,op. preserving2 … res_preserve … (sigma_beval p p' graph_prog sigma) (sigma_beval p p' graph_prog sigma) (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf), sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉) (be_opaccs op) (be_opaccs op). #p #p' #graph_prog #sigma #op #bv1 #bv2 #prf1 #prf2 @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ] [2: #by1 * @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ] [2: #by2 * cases (opaccs ????) #by1' #by2' @mfr_return %% whd in ⊢ (??%%→?); #EQ destruct(EQ) ] ] #v #EQ %{I} >sigma_bv_no_pc try assumption >(Byte_of_val_inv … EQ) % qed. lemma beop1_sigma_commute : ∀p,p',graph_prog,sigma,op. preserving … res_preserve … (sigma_beval p p' graph_prog sigma) (sigma_beval p p' graph_prog sigma) (be_op1 op) (be_op1 op). #p #p' #graph_prog #sigma #op #bv #prf @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ] [2: #by * @mfr_return % whd in ⊢ (??%%→?); #EQ destruct(EQ) ] #v #EQ %{I} >sigma_bv_no_pc try assumption >(Byte_of_val_inv … EQ) % qed. lemma sigma_ptr_commute : ∀ p, p', graph_prog , sigma. preserving … res_preserve … (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf), sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉) (λx.λ_ : True.x) pointer_of_address pointer_of_address. #p #p' #graph_prog #sigma * #val1 #val2 * #prf1 #prf2 #ptr whd in ⊢ (??%?→?); cases val1 in prf1; [|| #ptr1 #ptr2 #p | #by | #p | #ptr1 #p1 | #pc #p ] #prf1 whd in ⊢ (??%%→?); #EQ destruct(EQ) cases val2 in prf2 EQ; [|| #ptr1 #ptr2 #p | #by | #p | #ptr2 #p2 | #pc #p ] #prf2 normalize nodelta #EQ destruct(EQ) %{I} >sigma_bv_no_pc [2: %] >sigma_bv_no_pc [2: %] @EQ qed. lemma beop2_sigma_commute : ∀p,p',graph_prog,sigma,carry,op. preserving2 … res_preserve … (sigma_beval p p' graph_prog sigma) (sigma_beval p p' graph_prog sigma) (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) prf, \snd pr〉) (be_op2 carry op) (be_op2 carry op). #p #p' #graph_prog #sigma #carry #op @bv_pc_other [ #pc1 #p1 #bv2 | #bv1 #bv1_no_pc @bv_pc_other [ #pc2 #p2 | #bv2 #bv2_no_pc ] ] #prf1 #prf2 * #res #carry' [1,2: [2: cases bv1 in prf1; [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] #prf1 ] whd in ⊢ (??%%→?); #EQ destruct(EQ) ] #EQ cut (bv_no_pc res) [ -prf1 -prf2 cases bv1 in bv1_no_pc EQ; [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] * cases bv2 in bv2_no_pc; [3,10,17,24,31,38: #ptr21 #ptr22 #p2 |4,11,18,25,32,39: #by2 |5,12,19,26,33,40: #p2 |6,13,20,27,34,41: #ptr2 #p2 |7,14,21,28,35,42: #pc2 #p2 ] * cases op whd in match be_op2; whd in ⊢ (???%→?); normalize nodelta #EQ destruct(EQ) try % try (whd in EQ : (??%?); destruct(EQ) %) lapply EQ -EQ [ @if_elim #_ [ @if_elim #_ ] whd in ⊢ (??%%→?); #EQ destruct(EQ) % |2,12,13,16,18: @if_elim #_ whd in ⊢ (??%%→?); #EQ destruct(EQ) % |3,4,5,6,7,8: #H @('bind_inversion H) #bit #EQ cases (op2 eval bit ???) #res' #bit' whd in ⊢ (??%%→?); #EQ destruct(EQ) % |17: cases (ptype ptr1) normalize nodelta [ @if_elim #_ [ #H @('bind_inversion H) #bit #EQbit cases (op2 eval bit ???) #res' #bit' ] ] whd in ⊢ (??%%→?); #EQ destruct(EQ) % |*: whd in ⊢ (??%?→?); cases (ptype ?) normalize nodelta try (#EQ destruct(EQ) @I) cases (part_no ?) normalize nodelta try (#n lapply (refl ℕ n) #_) try (#EQ destruct(EQ) @I) try (#H @('bind_inversion H) -H * #EQbit whd in ⊢ (??%%→?);) try (#EQ destruct(EQ) @I) [1,2,4,6,7: cases (op2 eval ????) #res' #bit' whd in ⊢ (??%%→?); #EQ destruct(EQ) @I |*: cases carry normalize nodelta try (#b lapply (refl bool b) #_) try (#ptr lapply (refl pointer ptr) #_ #p #o) try (#EQ destruct(EQ) @I) @if_elim #_ try (#EQ destruct(EQ) @I) @If_elim #prf try (#EQ destruct(EQ) @I) cases (op2_bytes ?????) #res' #bit' whd in ⊢ (??%%→?); #EQ destruct(EQ) @I ] ] ] #res_no_pc %{(bv_no_pc_wf … res_no_pc)} >(sigma_bv_no_pc … bv1_no_pc) >(sigma_bv_no_pc … bv2_no_pc) >(sigma_bv_no_pc … res_no_pc) assumption qed. definition combine_strong : ∀A,B,C,D : Type[0]. ∀P : A → Prop.∀Q : C → Prop. (∀x.P x → B) → (∀x.Q x → D) → (∀pr.(P (\fst pr) ∧ Q (\snd pr)) → B × D) ≝ λA,B,C,D,P,Q,f,g,pr,prf.〈f ? (proj1 … prf), g ? (proj2 … prf)〉. lemma wf_set_is : ∀p,p',graph_prog,sigma,gss,st,is. well_formed_state p p' graph_prog sigma gss st → sigma_is_opt p p' graph_prog sigma is ≠ None ? → well_formed_state … gss (set_istack … is st). #p #p' #graph_prog #sigma #gss #st #is *** #H1 #H2 #H3 #H4 #H5 %{H4} %{H3} %{H5} @H1 qed. lemma wf_set_m : ∀p,p',graph_prog,sigma,gss,st,m. well_formed_state p p' graph_prog sigma gss st → well_formed_mem p p' graph_prog sigma m → well_formed_state … gss (set_m … m st). #p #p' #graph_prog #sigma #gss #st #m *** #H1 #H2 #H3 #H4 #H5 %{H5} %{H3} %{H2} @H1 qed. (* spostato in ExtraMonads.ma lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2. opt_preserve X Y P F m n → res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n). #X #Y #P #F #m #n #e1 #e2 #H #v #prf cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'} >EQ % qed. lemma err_eq_from_io : ∀O,I,X,m,v. err_to_io O I X m = return v → m = return v. #O #I #X * #x #v normalize #EQ destruct % qed. lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n. res_preserve X Y P F m n → io_preserve O I X Y P F m n. #O #I #X #Y #P #F #m #n #H #v #prf cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'} >EQ % qed. *) lemma eval_seq_no_pc_sigma_commute : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀stack_sizes. ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. ∀f,fn,stmt. preserving … res_preserve … (sigma_state … gss) (sigma_state … gss) (eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) f fn stmt) (eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes)) f (\fst (linearise_int_fun … fn)) stmt). #p #p' #graph_prog #stack_sizes #sigma #gss #f #fn #stmt whd in match eval_seq_no_pc; cases stmt normalize nodelta [1,2: (* COMMENT, COST_LABEL *) #_ @mfr_return | (* MOVE *) #mv_sig #st #prf' @mfr_bind [3: @pair_reg_move_commute |*:] #r #prf @mfr_return @wf_set_regs assumption | (* POP *) #a #st #prf @(mfr_bind … (combine_strong … (sigma_beval p p' graph_prog sigma) (sigma_state … gss))) [ @(mfr_bind … (sigma_is_pop_commute …)) * #bv #is' * #prf1' #prf2' @mfr_return %{prf1'} @wf_set_is assumption | * #bv #st' * #prf1' #prf2' @mfr_bind [3: @acca_store__commute |*:] #r #prf3' @mfr_return @wf_set_regs assumption ] | (* PUSH *) #a #st #prf @mfr_bind [3: @acca_arg_retrieve_commute |*:] #bv #prf_bv @mfr_bind [3: @is_push_sigma_commute |*:] #is #prf_is @mfr_return @wf_set_is assumption | (*C_ADDRESS*) #sy change with ((member ? ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?) #sy_prf change with ((dpl_reg p) → ?) #dpl change with ((dph_reg p) → ?) #dph #st #prf @(mfr_bind … (sigma_state … gss)) [ @(mfr_bind … (sigma_regs … gss)) [2: #r #prf' @mfr_return @wf_set_regs assumption ] ] @opt_safe_elim #bl #EQbl @opt_safe_elim #bl' >(find_symbol_transf … (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog sy) in ⊢ (%→?); >EQbl in ⊢ (%→?); #EQ destruct(EQ) [ @dpl_store_commute | #st' #st_prf' @mfr_bind [3: @dph_store_commute |*:] [2: #r #prf' @mfr_return @wf_set_regs assumption ] ] @bv_no_pc_wf % | (*C_OPACCS*) #op #a #b #arg1 #arg2 #st #prf @mfr_bind [3: @acca_arg_retrieve_commute |*: ] #bv1 #bv1_prf @mfr_bind [3: @accb_arg_retrieve_commute |*: ] #bv2 #bv2_prf @mfr_bind [3: @beopaccs_sigma_commute |*: ] * #res1 #res2 * #res1_prf #res2_prf @(mfr_bind … (sigma_state … gss)) [ @mfr_bind [3: @acca_store__commute |*: ] #r #r_prf @mfr_return @wf_set_regs assumption ] #st' #st_prf' @mfr_bind [3: @accb_store_commute |*: ] #r #r_prf @mfr_return @wf_set_regs assumption | (*C_OP1*) #op #a #arg #st #prf @mfr_bind [3: @acca_retrieve_commute |*: ] #bv #bv_prf @mfr_bind [3: @beop1_sigma_commute |*: ] #res #res_prf @mfr_bind [3: @acca_store__commute |*: ] #r #r_prf @mfr_return @wf_set_regs assumption | (*C_OP2*) #op #a #arg1 #arg2 #st #prf @mfr_bind [3: @acca_arg_retrieve_commute |*: ] #bv1 #bv1_prf @mfr_bind [3: @snd_arg_retrieve_commute |*: ] #bv2 #bv2_prf @mfr_bind [3: @beop2_sigma_commute |*: ] * #res1 #carry' #res1_prf @(mfr_bind … (sigma_state … gss)) [ @mfr_bind [3: @acca_store__commute |*: ] #r #r_prf @mfr_return @wf_set_regs assumption ] #st' #st_prf' @mfr_return | (*C_CLEAR_CARRY*) #st #prf @mfr_return | (*C_SET_CARRY*) #st #prf @mfr_return | (*C_LOAD*) #a #dpl #dph #st #prf @mfr_bind [3: @dph_arg_retrieve_commute |*:] #bv1 #bv1_prf @mfr_bind [3: @dpl_arg_retrieve_commute |*:] #bv2 #bv2_prf @mfr_bind [3: @sigma_ptr_commute |*:] [ % assumption ] #ptr * @mfr_bind [3: @opt_to_res_preserve @beloadv_sigma_commute |*:] #res #res_prf @mfr_bind [3: @acca_store__commute |*: ] #r #r_prf @mfr_return @wf_set_regs assumption | (*C_STORE*) #dpl #dph #a #st #prf @mfr_bind [3: @dph_arg_retrieve_commute |*:] #bv1 #bv1_prf @mfr_bind [3: @dpl_arg_retrieve_commute |*:] #bv2 #bv2_prf @mfr_bind [3: @sigma_ptr_commute |*:] [ % assumption ] #ptr * @mfr_bind [3: @acca_arg_retrieve_commute |*:] #res #res_prf @mfr_bind [3: @opt_to_res_preserve @bestorev_sigma_commute |*:] #mem #wf_mem @mfr_return @wf_set_m assumption | (*CALL*) #f #args #dest #st #prf @mfr_return | (*C_EXT*) #s_ext #st #prf @eval_ext_seq_commute ] qed. lemma eval_seq_no_call_ok : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀stack_sizes. ∀sigma.good_sigma p graph_prog sigma → ∀gss : good_state_sigma p p' graph_prog sigma. ∀st,st',f,fn,stmt,nxt.no_call ?? stmt → ∀prf : well_formed_state_pc … gss st. fetch_statement (make_sem_graph_params p p') … (globalenv_noinit ? graph_prog) (pc … st) = return 〈f, fn, sequential … (step_seq (mk_graph_params p) … stmt) nxt〉 → eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = return st' → ∃prf'. ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) (sigma_state_pc … gss st prf) (sigma_state_pc … gss st' prf'). bool_to_Prop (taaf_non_empty … taf). #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #stmt #nxt #stmt_no_call #prf #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind whd in match eval_statement_no_pc; whd in match eval_statement_advance; normalize nodelta @'bind_inversion #st_no_pc' #EQeval >no_call_advance [2: assumption] whd in ⊢ (??%%→?); #EQ destruct(EQ) cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) normalize nodelta #_ * #EQfetch' * #prf_nxt #nxt_spec lapply (err_eq_from_io ????? EQeval) -EQeval #EQeval cases (eval_seq_no_pc_sigma_commute … gss … (proj2 … prf) … EQeval) #st_no_pc_prf #EQeval' %{(hide_prf …)} [ %{st_no_pc_prf} %{prf_nxt} cases st in prf; -st #st #pc #popped ** // ] cases nxt_spec -nxt_spec [ #nxt_spec %{(taaf_step … (taa_base …) …) I} | * #nxt_spec #pc_of_label_spec %{(taaf_step … (taa_step … (taa_base …))…) I} ] [1,6: whd whd in ⊢ (??%?); >EQfetch' normalize nodelta whd in match joint_classify_step; normalize nodelta >no_call_other try % assumption |2,5: whd whd in match eval_state; normalize nodelta change with (sigma_pc ??????) in match (pc ??); try >EQfetch' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); whd in match eval_statement_no_pc; normalize nodelta try >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); whd in match eval_statement_advance; normalize nodelta >no_call_advance try assumption whd in match (next ???) in ⊢ (??%?); [ >nxt_spec % | % ] |3: whd whd in ⊢ (??%?); >nxt_spec normalize nodelta % |4: whd whd in match eval_state; normalize nodelta >nxt_spec >m_return_bind >m_return_bind whd in match eval_statement_advance; normalize nodelta whd in match goto; normalize nodelta whd in match (pc_block ?); >pc_block_sigma_commute >pc_of_label_spec % |7: %* #H @H -H whd in ⊢ (??%?); >nxt_spec % |8: ] qed. lemma block_of_call_sigma_commute : ∀p,p',graph_prog,sigma. ∀gss : good_state_sigma p p' graph_prog sigma.∀cl. preserving … res_preserve … (sigma_state p p' graph_prog sigma gss) (λx.λ_ : True .x) (block_of_call (make_sem_graph_params p p') … (globalenv_noinit ? graph_prog) cl) (block_of_call (make_sem_lin_params p p') … (globalenv_noinit ? (linearise ? graph_prog)) cl). #p #p' #graph_prog #sigma #gss #cl #st #prf @mfr_bind [3: cases cl [ #id normalize nodelta @opt_to_res_preserve >(find_symbol_transf … (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog id) #s #EQs %{I} >EQs in ⊢ (??%?); % | * #dpl #dph normalize nodelta @mfr_bind [3: @dpl_arg_retrieve_commute |*:] #bv1 #bv1_prf @mfr_bind [3: @dph_arg_retrieve_commute |*:] #bv2 #bv2_prf @(mfr_bind … (λptr.λ_:True.ptr)) [ change with (pointer_of_address 〈?,?〉) in match (pointer_of_bevals ?); change with (pointer_of_address 〈?,?〉) in match (pointer_of_bevals [sigma_beval ??????;?]); @sigma_ptr_commute % assumption ] #ptr * @if_elim #_ [ @mfr_return | @res_preserve_error ] % ] |4: #bl * @opt_to_res_preserve #x #EQ %{I} @EQ |*: ] qed. lemma fetch_function_no_minus_one : ∀F,V,i,p,bl. block_id (pi1 … bl) = -1 → fetch_function … (globalenv (λvars.fundef (F vars)) V i p) bl = Error … [MSG BadFunction]. #F#V#i#p ** #r #id #EQ1 #EQ2 destruct whd in match fetch_function; normalize nodelta >globalenv_no_minus_one cases (symbol_for_block ???) normalize // qed. lemma entry_sigma_commute: ∀ p,p',graph_prog,sigma.good_sigma p graph_prog sigma → ∀bl,f1,fn1. (fetch_function ? (globalenv_noinit … graph_prog) bl = return 〈f1,Internal ? fn1〉) → ∃prf. sigma_pc p p' graph_prog sigma (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf = pc_of_point (make_sem_lin_params p p') bl 0. #p #p' #graph_prog #sigma #good #bl #f1 #fn1 #fn1_spec cases (good fn1) * #entry_in #_ #_ % [ @hide_prf % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ] whd in match sigma_pc_opt; normalize nodelta >eqZb_false whd in match (pc_block ?); [2,4: % #EQbl >(fetch_function_no_minus_one … graph_prog … EQbl) in fn1_spec; whd in ⊢ (???%→?); #ABS destruct(ABS) ] normalize nodelta whd in match fetch_internal_function; normalize nodelta >fn1_spec >m_return_bind >point_of_pc_of_point >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. lemma eval_call_ok : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀stack_sizes. ∀sigma. good_sigma p graph_prog sigma → ∀gss : good_state_sigma p p' graph_prog sigma. ∀st,st',f,fn,called,args,dest,nxt. ∀prf : well_formed_state_pc … gss st. fetch_statement (make_sem_graph_params p p') … (globalenv_noinit ? graph_prog) (pc … st) = return 〈f, fn, sequential … (CALL (mk_graph_params p) … called args dest ) nxt〉 → eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = return st' → (* let st_pc' ≝ mk_state_pc ? st' (succ_pc (make_sem_graph_params p p') … (pc … st) nxt) in ∀prf'. fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) = return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 → pc_of_label (make_sem_lin_params p p') ? (globalenv_noinit ? (linearise p … graph_prog)) (pc_block (pc … st)) nxt = return sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →*) let st2_pre_call ≝ sigma_state_pc … gss st prf in ∃is_call, is_call'. ∃prf'. let st2_after_call ≝ sigma_state_pc … gss st' prf' in joint_call_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_call'» = joint_call_ident (graph_prog_params … graph_prog stack_sizes) «st, is_call» ∧ eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) st2_pre_call = return st2_after_call. #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st1 #f #fn #called #args #dest #nxt #prf #fetch_spec cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) #_ normalize nodelta * #lin_fetch_spec #_ whd in match eval_state in ⊢ (%→?); normalize nodelta >fetch_spec >m_return_bind >m_return_bind whd in match eval_statement_advance; whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta @('bind_inversion) #bl #H lapply (err_eq_from_io ????? H) -H #bl_spec @('bind_inversion) * #id #int_f #H lapply (err_eq_from_io ????? H) -H cases int_f -int_f [ #fn | #ext_f] #int_f_spec normalize nodelta [2:#H @('bind_inversion H) -H #st' #H #_ @('bind_inversion H) -H #vals #_ @'bind_inversion #vals' #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] #H lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st_no_pc #save_frame_spec >m_bind_bind #H @('bind_inversion H) -H #stack_size #H lapply (opt_eq_from_res ???? H) -H whd in match (stack_sizes ?); #stack_size_spec >m_bind_bind #H @('bind_inversion H) -H #st_no_pc' #set_call_spec >m_return_bind whd in ⊢ (??%%→?); whd in match set_no_pc; normalize nodelta #EQ destruct(EQ) % [ @hide_prf whd in match joint_classify; normalize nodelta >fetch_spec >m_return_bind normalize nodelta whd in match joint_classify_step; whd in match joint_classify_seq; normalize nodelta >bl_spec >m_return_bind >int_f_spec normalize nodelta % | cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? bl_spec) * #lin_bl_spec generalize in match (fetch_function_transf … graph_prog … (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) … int_f_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?; #lin_int_f_spec % [ @hide_prf whd in match joint_classify; normalize nodelta >lin_fetch_spec >m_return_bind normalize nodelta whd in match joint_classify_step; whd in match joint_classify_seq; normalize nodelta >lin_bl_spec >m_return_bind >lin_int_f_spec % | cases (save_frame_commute … gss … save_frame_spec) in ⊢ ?; [2: @hide_prf cases st in prf; // ] #st_no_pc_wf #lin_save_frame_spec cases (setup_call_commute … gss … st_no_pc_wf … set_call_spec) in ⊢ ?; #st_no_pc_wf' #lin_set_call_spec cases (allocate_locals_commute … gss … (joint_if_locals … fn) … st_no_pc_wf') #st_no_pc_wf'' #lin_allocate_locals_spec cases(entry_sigma_commute p p' graph_prog sigma good … int_f_spec) #entry_prf #entry_spec % [ @hide_prf %{st_no_pc_wf''} %{entry_prf} @(proj1 … (proj1 … prf)) ] % [ whd in match joint_call_ident; normalize nodelta >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?); >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]); normalize nodelta >lin_bl_spec >bl_spec >m_return_bind >m_return_bind whd in match fetch_internal_function; normalize nodelta >lin_int_f_spec >int_f_spec % | whd in match eval_state; normalize nodelta >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); whd in match eval_statement_no_pc; normalize nodelta whd in match eval_seq_no_pc; normalize nodelta >m_return_bind in ⊢ (??%?); whd in match eval_statement_advance; whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >lin_int_f_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); normalize nodelta >lin_save_frame_spec >m_return_bind >m_bind_bind whd in match (stack_sizes ?); >stack_size_spec >m_return_bind >lin_set_call_spec >m_return_bind >lin_allocate_locals_spec EQfetch >m_return_bind >m_return_bind whd in match eval_statement_advance; normalize nodelta whd in match goto; normalize nodelta #H lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) #pc' @('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?); #EQ destruct(EQ) >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?); #EQ1 #EQ2 destruct cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) normalize nodelta ** #prf' #EQpc_of_label' * #EQfetch' -H % [ @hide_prf cases st in prf prf'; -st #st #pc #popped ** #H1 #H2 #H3 #H4 %{H3} %{H1 H4} ] %{(taaf_step … (taa_base …) …) I} [ whd whd in ⊢ (??%?); >EQfetch' % | whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind >m_return_bind whd in match eval_statement_advance; whd in match goto; normalize nodelta >pc_block_sigma_commute >EQpc_of_label' >m_return_bind % ] qed. lemma eval_cond_ok : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀stack_sizes. ∀sigma.good_sigma p graph_prog sigma → ∀gss : good_state_sigma p p' graph_prog sigma. ∀st,st',f,fn,a,ltrue,lfalse. ∀prf : well_formed_state_pc … gss st. fetch_statement (make_sem_graph_params p p') … (globalenv_noinit ? graph_prog) (pc … st) = return 〈f, fn, sequential … (COND (mk_graph_params p) … a ltrue) lfalse〉 → eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = return st' → as_costed (joint_abstract_status (graph_prog_params p p' graph_prog stack_sizes)) st' → ∃prf'. ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) (sigma_state_pc … gss st prf) (sigma_state_pc … gss st' prf'). bool_to_Prop (taaf_non_empty … taf). #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #a #ltrue #lfalse #prf #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind >m_return_bind whd in match eval_statement_advance; normalize nodelta #H @('bind_inversion (err_eq_from_io ????? H)) @bv_pc_other [ #pc' #p #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] #bv #bv_no_pc #EQretrieve cut (∃prf'.acca_retrieve ?? (p' ?) (sigma_state_pc p p' graph_prog sigma gss st prf) a = return sigma_beval p p' graph_prog sigma bv prf') [ @acca_retrieve_commute assumption ] * #bv_prf >(sigma_bv_no_pc … bv_no_pc) #EQretrieve' -H #H @('bind_inversion H) * #EQbool normalize nodelta -H [ whd in match goto; normalize nodelta #H @('bind_inversion H) -H #pc' @('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?); #EQ destruct(EQ) >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?); #EQ1 #EQ2 destruct | whd in ⊢ (??%%→?); #EQ destruct(EQ) ] #ncost cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) normalize nodelta ** #prf' #EQpc_of_label' ** #prf'' ** #EQfetch' #nxt_spec % [1,3,5,7: @hide_prf cases st in prf prf' prf''; -st #st #pc #popped ** #H1 #H2 #H3 #H4 #H5 %{H3} %{H1} assumption ] %{(taaf_step_jump … (taa_base …) …) I} [1,4,7,10: whd >(as_label_sigma_commute … good) assumption |2,5,8,11: whd whd in ⊢ (??%?); >EQfetch' % |*: whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind >m_return_bind whd in match eval_statement_advance; normalize nodelta >EQretrieve' >m_return_bind >EQbool >m_return_bind normalize nodelta [1,2: whd in match goto; normalize nodelta >pc_block_sigma_commute >EQpc_of_label' % |3: whd in match next; normalize nodelta >nxt_spec % |4: whd in match goto; normalize nodelta >pc_block_sigma_commute >nxt_spec % ] ] qed. lemma eval_return_ok : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀stack_sizes. ∀sigma.∀good : good_sigma p graph_prog sigma. ∀gss : good_state_sigma p p' graph_prog sigma. ∀st,st',f,fn. ∀prf : well_formed_state_pc … gss st. fetch_statement (make_sem_graph_params p p') … (globalenv_noinit ? graph_prog) (pc … st) = return 〈f, fn, final … (RETURN (mk_graph_params p) … )〉 → eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = return st' → joint_classify (lin_prog_params … (linearise … graph_prog) stack_sizes) (sigma_state_pc … st prf) = Some ? cl_return ∧ ∃prf'. ∃st2_after_ret. ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) st2_after_ret (sigma_state_pc … gss st' prf'). (if taaf_non_empty … taf then ¬as_costed (joint_abstract_status (lin_prog_params p p' (linearise … graph_prog) stack_sizes)) st2_after_ret else True) ∧ eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) (sigma_state_pc … st prf) = return st2_after_ret ∧ ret_rel … (linearise_status_rel … gss good) st' st2_after_ret. #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #prf #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind >m_return_bind whd in match eval_statement_advance; normalize nodelta #H lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1' #EQpop cut (∃prf'. (pop_frame … (ev_genv (lin_prog_params ? p' (linearise ? graph_prog) stack_sizes)) f (\fst (pi1 ?? (linearise_int_fun ?? fn))) (sigma_state … gss st (proj2 … prf))) = return sigma_state_pc … gss st1' prf') [ @pop_frame_commute assumption ] * #prf' #EQpop' >m_bind_bind #H @('bind_inversion H) ** #call_i #call_fn * [ * [ #s | #a #lbl ] #nxt | #s | * ] normalize nodelta #EQfetch_ret -H whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in match (next ???); >graph_succ_pc cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) #_ normalize nodelta #EQfetch' cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf')) … EQfetch_ret) normalize nodelta #all_labels_in * #EQfetch_ret' * #prf'' * [2: * ] #nxt_spec [2:| #EQpc_of_label'] % [1,3: whd in match joint_classify; normalize nodelta >EQfetch' >m_return_bind % ] % [1,3: @hide_prf cases prf' * #_ #H1 #H2 %{H2} %{H1 prf''} ] [ % [2: %{(taaf_base …)} |] % [ %{I} ] [ >EQfetch' >m_return_bind >m_return_bind normalize nodelta whd in match eval_return; normalize nodelta >EQpop' >m_return_bind whd in match next_of_pc; normalize nodelta >EQfetch_ret' >m_return_bind whd in match next; normalize nodelta >nxt_spec % | * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i #calling * #call_spec * #arg * #dest * #nxt * #bl * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called * #s2_pre #s2_call whd in ⊢ (%→?); >EQfetch_call * #EQ #_ * #s1_pre_prf #EQpc_s2_pre whd >EQpc_s2_pre <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ] >EQfetch_ret' % [ % | >nxt_spec % ] ] | % [2: %{(taaf_step … (taa_base …) …)} |*:] [3: % [ % normalize nodelta ] [2: >EQfetch' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >m_return_bind in ⊢ (??%?); normalize nodelta whd in match eval_return; normalize nodelta >EQpop' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); whd in match next_of_pc; normalize nodelta >EQfetch_ret' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); whd in match next; normalize nodelta % |1: normalize nodelta %* #H @H -H whd in ⊢ (??%?); >nxt_spec % |3: * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i #calling * #call_spec * #arg * #dest * #nxt' * #bl * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called * #s2_pre #s2_call whd in ⊢ (%→?); >EQfetch_call * #EQ #_ * #s1_pre_prf #EQpc_s2_pre whd >EQpc_s2_pre <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ] >EQfetch_ret' %% ] |1: whd whd in ⊢ (??%?); >nxt_spec % |2: whd whd in match eval_state; normalize nodelta >nxt_spec >m_return_bind >m_return_bind whd in match eval_statement_advance; whd in match goto; normalize nodelta whd in match (pc_block ?); >pc_block_sigma_commute >EQpc_of_label' >m_return_bind % whd in match (set_pc ???); % |*: ] ] qed. lemma eval_tailcall_ok : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀stack_sizes. ∀sigma.good_sigma p graph_prog sigma → ∀gss : good_state_sigma p p' graph_prog sigma. ∀st,st',f,fn,fl,called,args. ∀prf : well_formed_state_pc … gss st. fetch_statement (make_sem_graph_params p p') … (globalenv_noinit ? graph_prog) (pc … st) = return 〈f, fn, final … (TAILCALL (mk_graph_params p) … fl called args)〉 → eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = return st' → let st2_pre_call ≝ sigma_state_pc … gss st prf in ∃is_tailcall, is_tailcall'. ∃prf'. let st2_after_call ≝ sigma_state_pc … gss st' prf' in joint_tailcall_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_tailcall'» = joint_tailcall_ident (graph_prog_params … graph_prog stack_sizes) «st, is_tailcall» ∧ eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) st2_pre_call = return st2_after_call. #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #fl #called #args #prf #fetch_spec cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) * normalize nodelta #lin_fetch_spec whd in match eval_state; normalize nodelta >fetch_spec >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta @('bind_inversion) #bl #bl_spec lapply (err_eq_from_io ????? bl_spec) -bl_spec whd in match set_no_pc; normalize nodelta #bl_spec cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? bl_spec) * #lin_bl_spec @('bind_inversion) * #f1 #fn1 cases fn1 normalize nodelta -fn1 [2: #ext_f #_ whd in match eval_external_call; normalize nodelta @('bind_inversion) #st @('bind_inversion) #list_val #_ @('bind_inversion) #le #_ whd in ⊢ (??%% → ?); #ABS destruct(ABS)] #fn1 #fn1_spec lapply(err_eq_from_io ????? fn1_spec) -fn1_spec #fn1_spec generalize in match (fetch_function_transf … graph_prog … (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) … fn1_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?; #lin_fn1_spec whd in match eval_internal_call; normalize nodelta #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1 #H @('bind_inversion H) -H #dim_s #dim_s_spec #H @('bind_inversion H) -H #st2 #st2_spec whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct % [ @hide_prf | % [@hide_prf]] [1,2: whd in match joint_classify; normalize nodelta [>fetch_spec | >lin_fetch_spec] >m_return_bind normalize nodelta whd in match joint_classify_final; normalize nodelta [>bl_spec|>lin_bl_spec] >m_return_bind [>fn1_spec|>lin_fn1_spec] % | cases (setup_call_commute … gss … (proj2 … prf) … st2_spec) #wf_st2 #lin_st2_spec cases (allocate_locals_commute … gss … (joint_if_locals … fn1) ? wf_st2) #wf_all_st2 #all_st2_spec cases(entry_sigma_commute p p' graph_prog sigma good … fn1_spec) #wf_pc #pc_spec % [ @hide_prf % [ % [@(proj1 … (proj1 … prf)) | @(wf_pc)] | @(wf_all_st2) ] | % [ whd in match joint_tailcall_ident; normalize nodelta >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?); >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]); normalize nodelta >lin_bl_spec >bl_spec >m_return_bind >m_return_bind whd in match fetch_internal_function; normalize nodelta >fn1_spec >lin_fn1_spec % | >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); normalize nodelta >m_return_bind in ⊢ (??%?); >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >lin_fn1_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); normalize nodelta >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >lin_st2_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >all_st2_spec in ⊢ (??%?); whd in ⊢ (??%%); @eq_f @eq_f2 [2: %] >pc_spec % ] ] ] qed. inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ ex1_intro: ∀ x:A. P x → ex_Type1 A P. (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) lemma linearise_ok: ∀p,p',graph_prog. let lin_prog ≝ linearise ? graph_prog in ∀stack_sizes. (∀sigma.good_state_sigma p p' graph_prog sigma) → ex_Type1 … (λR. status_simulation (graph_abstract_status p p' graph_prog stack_sizes) (lin_abstract_status p p' lin_prog stack_sizes) R). #p #p' #graph_prog letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog) cut (∀fn.good_local_sigma … (sigma fn)) [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:] #good #stack_sizes #gss lapply (gss sigma) -gss #gss %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)} whd in match graph_abstract_status; whd in match lin_abstract_status; whd in match graph_prog_params; whd in match lin_prog_params; normalize nodelta whd whd in ⊢ (%→%→%→?); whd in ⊢ (?(?%)→?(?%)→?(?%)→?); whd in ⊢ (?%→?%→?%→?); #st1 #st1' #st2 whd in ⊢ (%→?); change with (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?) #EQeval @('bind_inversion EQeval) ** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch #_ * #prf #EQst2 cases stmt in EQfetch; -stmt [ @cond_call_other [ #a #ltrue | #f #args #dest | #s #s_no_call ] #nxt | #s | * ] normalize nodelta #EQfetch change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); [ (* COND *) whd in match joint_classify; normalize nodelta; >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta #ncost cases (eval_cond_ok … good … prf EQfetch EQeval ncost) #prf' * #taf #taf_ne destruct(EQst2) % [2: %{taf} |*:] >taf_ne normalize nodelta % [ %{I} %{prf'} % ] whd >(as_label_sigma_commute … good) % | (* CALL *) cases (eval_call_ok … good … prf EQfetch EQeval) #is_call * #is_call' * #prf' * #eq_call #EQeval' destruct(EQst2) >is_call in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta #ignore %{«?, is_call'»} % [ %{eq_call} %{prf} % ] % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:] whd >(as_label_sigma_commute … good) % | (* SEQ *) whd in match joint_classify; normalize nodelta; >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta whd in match joint_classify_step; normalize nodelta >no_call_other [2: assumption ] normalize nodelta cases (eval_seq_no_call_ok … good … prf EQfetch EQeval) [2: assumption ] #prf' * #taf #taf_ne destruct(EQst2) % [2: %{taf} |*:] >taf_ne normalize nodelta % [ %{I} ] [ %{prf'} % | whd >(as_label_sigma_commute … good) % ] | (* FIN *) cases s in EQfetch; [ (* GOTO *) #lbl #EQfetch whd in match joint_classify; normalize nodelta; >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta cases (eval_goto_ok … good … prf EQfetch EQeval) #prf' * #taf #taf_ne destruct(EQst2) % [2: %{taf} |*:] >taf_ne normalize nodelta % [ %{I} ] [ %{prf'} % | whd >(as_label_sigma_commute … good) % ] | (* RETURN *) #EQfetch whd in match joint_classify; normalize nodelta; >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta cases (eval_return_ok … good … prf EQfetch EQeval) #is_ret' * #prf' * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf destruct(EQst2) % [2: % [2: % [2: %{(taa_base …)} %{taf} ]] |*:] % [2: whd >(as_label_sigma_commute … good) % ] %{ret_prf} % [2: %{prf'} % ] %{EQeval'} %{taf_prf is_ret'} | (* TAILCALL *) #fl #called #args #EQfetch cases (eval_tailcall_ok … good … prf EQfetch EQeval) #is_tailcall * #is_tailcall' * #prf' * #eq_call #EQeval' destruct(EQst2) >is_tailcall in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta #ignore %{«?, is_tailcall'»} %{eq_call} % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:] whd >(as_label_sigma_commute … good) % ] ] qed.