(**************************************************************************) (* ___ *) (* ||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". 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). ((Σi.is_internal_function_of_program … prog i) → ℕ) → 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). ((Σi.is_internal_function_of_program … prog i) → ℕ) → 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_pc_opt: ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). ((Σi.is_internal_function_of_program … graph_prog i) → code_point (mk_graph_params p) → option ℕ) → 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 ! f ← int_funct_of_block ? ge (pc_block pc) ; ! lin_point ← sigma f (point_of_pc ? pars pc) ; return pc_of_point ? (make_sem_lin_params ? p') pc lin_point. definition well_formed_pc: ∀p,p',graph_prog. ((Σi.is_internal_function_of_program … graph_prog i) → label → option ℕ) → 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). ((Σi.is_internal_function_of_program … graph_prog i) → code_point (mk_graph_params p) → option ℕ) → 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 …. (* 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 : ((Σi.is_internal_function_of_program … graph_prog i) → label → option ℕ). ∀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. 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)». record good_sigma_state (p : unserialized_params) (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p)) graph_prog i) → label → option ℕ) : Type[0] ≝ { well_formed_state : state (make_sem_graph_params p p') → Prop ; sigma_state : ∀st.well_formed_state st → state (make_sem_lin_params p p') ; acca_store_ok : ∀a,bv,bv',st,st',prf1,prf2. sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → acca_store ?? (p' ?) a bv st = return st' → acca_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 ; acca_store_wf : ∀a,bv,bv',st,st'. sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → acca_store ?? (p' ?) a bv st = return st' → well_formed_state st → well_formed_state st' ; acca_retrieve_ok : ∀a,st,bv,prf1,prf2. acca_retrieve ?? (p' ?) st a = return bv → acca_retrieve ?? (p' ?) (sigma_state st prf1) a = return sigma_beval p p' graph_prog sigma bv prf2 ; acca_retrieve_wf : ∀a,st,bv. acca_retrieve ?? (p' ?) st a = return bv → well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ; acca_arg_retrieve_ok : ∀a,st,bv,prf1,prf2. acca_arg_retrieve ?? (p' ?) st a = return bv → acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = return sigma_beval p p' graph_prog sigma bv prf2 ; acca_arg_retrieve_wf : ∀a,st,bv. acca_arg_retrieve ?? (p' ?) st a = return bv → well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ; accb_store_ok : ∀a,bv,bv',st,st',prf1,prf2. sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → accb_store ?? (p' ?) a bv st = return st' → accb_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 ; accb_store_wf : ∀a,bv,bv',st,st'. sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → accb_store ?? (p' ?) a bv st = return st' → well_formed_state st → well_formed_state st' ; accb_retrieve_ok : ∀a,st,bv,prf1,prf2. accb_retrieve ?? (p' ?) st a = return bv → accb_retrieve ?? (p' ?) (sigma_state st prf1) a = return sigma_beval p p' graph_prog sigma bv prf2 ; accb_retrieve_wf : ∀a,st,bv. accb_retrieve ?? (p' ?) st a = return bv → well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ; accb_arg_retrieve_ok : ∀a,st,bv,prf1,prf2. acca_arg_retrieve ?? (p' ?) st a = return bv → acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = return sigma_beval p p' graph_prog sigma bv prf2 ; accb_arg_retrieve_wf : ∀a,st,bv. accb_arg_retrieve ?? (p' ?) st a = return bv → well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ; dpl_store_ok : ∀a,bv,bv',st,st',prf1,prf2. sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → dpl_store ?? (p' ?) a bv st = return st' → dpl_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 ; dpl_store_wf : ∀a,bv,bv',st,st'. sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → dpl_store ?? (p' ?) a bv st = return st' → well_formed_state st → well_formed_state st' ; dpl_retrieve_ok : ∀a,st,bv,prf1,prf2. dpl_retrieve ?? (p' ?) st a = return bv → dpl_retrieve ?? (p' ?) (sigma_state st prf1) a = return sigma_beval p p' graph_prog sigma bv prf2 ; dpl_retrieve_wf : ∀a,st,bv. dpl_retrieve ?? (p' ?) st a = return bv → well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ; dpl_arg_retrieve_ok : ∀a,st,bv,prf1,prf2. acca_arg_retrieve ?? (p' ?) st a = return bv → acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = return sigma_beval p p' graph_prog sigma bv prf2 ; dpl_arg_retrieve_wf : ∀a,st,bv. dpl_arg_retrieve ?? (p' ?) st a = return bv → well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ; dph_store_ok : ∀a,bv,bv',st,st',prf1,prf2. sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → dph_store ?? (p' ?) a bv st = return st' → dph_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 ; dph_store_wf : ∀a,bv,bv',st,st'. sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → dph_store ?? (p' ?) a bv st = return st' → well_formed_state st → well_formed_state st' ; dph_retrieve_ok : ∀a,st,bv,prf1,prf2. dph_retrieve ?? (p' ?) st a = return bv → dph_retrieve ?? (p' ?) (sigma_state st prf1) a = return sigma_beval p p' graph_prog sigma bv prf2 ; dph_retrieve_wf : ∀a,st,bv. dph_retrieve ?? (p' ?) st a = return bv → well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ; dph_arg_retrieve_ok : ∀a,st,bv,prf1,prf2. acca_arg_retrieve ?? (p' ?) st a = return bv → acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = return sigma_beval p p' graph_prog sigma bv prf2 ; dph_arg_retrieve_wf : ∀a,st,bv. dph_arg_retrieve ?? (p' ?) st a = return bv → well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ; snd_arg_retrieve_ok : ∀a,st,bv,prf1,prf2. snd_arg_retrieve ?? (p' ?) st a = return bv → snd_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = return sigma_beval p p' graph_prog sigma bv prf2 ; snd_arg_retrieve_wf : ∀a,st,bv. snd_arg_retrieve ?? (p' ?) st a = return bv → well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ; pair_reg_move_ok : ∀mv,st1,st2,prf1,prf2. pair_reg_move ?? (p' ?) st1 mv = return st2 → pair_reg_move ?? (p' ?) (sigma_state st1 prf1) mv = return sigma_state st2 prf2 ; pair_reg_move_wf : ∀mv,st1,st2. pair_reg_move ?? (p' ?) st1 mv = return st2 → well_formed_state st1 → well_formed_state st2 ; allocate_locals_ok : ∀l,st1,prf1,prf2. allocate_locals ?? (p' ?) l (sigma_state st1 prf1) = sigma_state (allocate_locals ?? (p' ?) l st1) prf2 ; allocate_locals_wf : ∀l,st1. well_formed_state st1 → well_formed_state (allocate_locals ?? (p' ?) l st1) ; save_frame_ok : ∀dest,st1,st2,prf1,prf2. save_frame ?? (p' ?) dest st1 = return st2 → let st1' ≝ mk_state_pc … (sigma_state st1 (proj2 … prf1)) (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in save_frame ?? (p' ?) dest st1' = return sigma_state st2 prf2 ; save_frame_wf : ∀dest,st1,st2. save_frame ?? (p' ?) dest st1 = return st2 → (well_formed_pc p p' graph_prog sigma (pc … st1) ∧ well_formed_state st1) → well_formed_state st2 ; eval_ext_seq_ok : let lin_prog ≝ linearise p graph_prog in ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. let stack_sizes' ≝ stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') ? graph_prog stack_sizes in ∀ext,fn,st1,st2,prf1,prf2. eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) ext fn st1 = return st2 → eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) ext (sigma_function_name … fn) (sigma_state st1 prf1) = return sigma_state st2 prf2 ; eval_ext_seq_wf : let lin_prog ≝ linearise p graph_prog in ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. let stack_sizes' ≝ stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') ? graph_prog stack_sizes in ∀ext,fn,st1,st2. eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) ext fn st1 = return st2 → well_formed_state st1 → well_formed_state st2 }. (* 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) *) definition well_formed_state_pc : ∀p,p',graph_prog,sigma. good_sigma_state p p' graph_prog sigma → state_pc (make_sem_graph_params p p') → Prop ≝ λp,p',prog,sigma,gss,st. well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gss st. definition sigma_state_pc : ∀p. ∀p':∀F.sem_unserialized_params p F. ∀graph_prog. ∀sigma. (* let lin_prog ≝ linearise ? graph_prog in *) ∀gss : good_sigma_state 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 gss s → state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) ≝ λp,p',graph_prog,sigma,gss,s,prf. let pc' ≝ sigma_pc … (proj1 … prf) in let st' ≝ sigma_state … (proj2 … prf) in mk_state_pc ? st' pc'. (* 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 res_eq_from_opt : ∀A,m,v.res_to_opt A m = return v → m = return v. #A * #x #v normalize #EQ destruct % 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 bind_opt_inversion: ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B. (! x ← f ; g x = Some … y) → ∃x. (f = Some … x) ∧ (g x = Some … y). #A #B #f #g #y cases f normalize [ #H destruct (H) | #a #e %{a} /2 by conj/ ] qed. lemma sigma_pblock_eq_lemma : ∀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; normalize nodelta @opt_safe_elim #x #x_spec whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec; normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H #offset * #_ 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 #H elim (bind_opt_inversion ??? ?? H) -H #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 fetch_function_sigma_commute : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀sigma,pc_st,f. ∀prf : well_formed_pc p p' graph_prog sigma pc_st. fetch_function … (globalenv_noinit … graph_prog) pc_st = return f → fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) = return sigma_function_name … f. #p #p' #graph_prog #sigma #st #f #prf whd in match fetch_function; normalize nodelta >(sigma_pblock_eq_lemma … prf) #H lapply (opt_eq_from_res ???? H) -H #H >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H) // 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 opt_Exists_elim: ∀A:Type[0].∀P:A → Prop. ∀o:option A. opt_Exists A P o → ∃v:A. o = Some … v ∧ P v. #A #P * normalize /3/ * qed. lemma stmt_at_sigma_commute: ∀p,graph_prog,graph_fun,lbl,pt. let lin_prog ≝ linearise ? graph_prog in let lin_fun ≝ sigma_function_name p graph_prog graph_fun in ∀sigma.good_sigma p graph_prog sigma → sigma graph_fun lbl = return pt → ∀stmt. stmt_at … (joint_if_code ?? (if_of_function ?? graph_fun)) lbl = return stmt → stmt_at ?? (joint_if_code ?? (if_of_function ?? lin_fun)) pt = return (graph_to_lin_statement … stmt). #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun))) #sigma_entry_is_zero #lin_stmt_spec lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 * #EQlookup_stmt1 #H elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt * #EQnth_opt_graph_stmt normalize nodelta * #optEQlbl_optlbl_graph_stmt #next_spec whd in match (stmt_at ????) in ⊢ (% → ?); normalize nodelta >EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ) whd in match (stmt_at ????); > EQnth_opt_graph_stmt normalize nodelta elim optEQlbl_optlbl_graph_stmt #_ #EQ >EQ // 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 // *) lemma fetch_statement_sigma_commute: ∀p,p',graph_prog,pc,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 〈fn,stmt〉 → fetch_statement ? (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉. #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf whd in match fetch_statement; normalize nodelta #H cases (bind_inversion ????? H) #id * -H #fetchfn >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind #H cases (bind_inversion ????? H) #fstmt * -H #H lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct >(stmt_at_sigma_commute … good … H) [%] whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' #H cases (bind_opt_inversion ????? H) #i * #EQ1 -H #H cases (bind_opt_inversion ????? H) #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2 qed. lemma point_of_pc_sigma_commute : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀sigma,pc,fn,n. ∀prf : well_formed_pc p p' graph_prog sigma pc. int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return 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 #fn #n #prf #EQfetch #EQsigma whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' whd in match sigma_pc_opt; normalize nodelta >EQfetch >m_return_bind >EQsigma >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ) change with (point_of_offset ??? = ?) @point_of_offset_of_point qed. definition linearise_status_rel: ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. let stack_sizes' ≝ stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') ? graph_prog stack_sizes in ∀sigma,gss. 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) (proj1 … prf)) (* sim_final ≝ *) ?. #st1 #st2 * #prf #EQ2 % whd in ⊢ (%→%); #H lapply (opt_to_opt_safe … H) @opt_safe_elim -H #res #_ #H lapply (res_eq_from_opt ??? H) -H cases daemon (*#H elim (bind_inversion ????? H) in ⊢ ?; * #f #stmt * whd in ⊢ (??%?→?);*) qed. lemma IO_bind_inversion: ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. (! x ← f ; g x = return y) → ∃x. (f = return x) ∧ (g x = return y). #O #I #A #B #f #g #y cases f normalize [ #o #f #H destruct | #a #e %{a} /2 by conj/ | #m #H destruct (H) ] 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 eval_seq_no_pc_sigma_commute : ∀p,p',graph_prog. let lin_prog ≝ linearise p graph_prog in ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. let stack_sizes' ≝ stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') ? graph_prog stack_sizes in ∀sigma.∀gss : good_sigma_state … graph_prog sigma. ∀fn,st,stmt,st'. ∀prf : well_formed_state … gss st.∀prf'. eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes')) fn st stmt = return st' → eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes)) (sigma_function_name … fn) (sigma_state … gss st prf) stmt = return sigma_state … gss st' prf'. #p #p' #graph_prog #stack_sizes #sigma #gss #fn #st #stmt #st' #prf #prf' cases daemon (* whd in match eval_seq_no_pc; cases stmt normalize nodelta [1,2: #_ #EQ whd in EQ : (??%%); destruct(EQ) // | #mv_sig whd in match pair_reg_move in ⊢ (%→?); normalize nodelta #H ] *) 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 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. let graph_stack_sizes ≝ stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') ? graph_prog lin_stack_sizes in (∀sigma.good_sigma_state p p' graph_prog sigma) → ex_Type1 … (λR. status_simulation (graph_abstract_status p p' graph_prog graph_stack_sizes) (lin_abstract_status p p' lin_prog lin_stack_sizes) R). #p #p' #graph_prog cases (linearise_spec … graph_prog) #sigma #good #lin_stack_sizes #gss lapply (gss sigma) -gss #gss %{(linearise_status_rel p p' graph_prog lin_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 ???) ?? = ? → ?) whd in match eval_state in ⊢ (%→?); normalize nodelta change with (Σi.is_internal_function_of_program ? graph_prog i) in match (Sig ??) in ⊢ (%→?); letin globals ≝ (prog_var_names ?? graph_prog) change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in match (fetch_statement ?????) in ⊢ (%→?); #ex cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex #EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch #EQfetch cases (bind_inversion ????? EQfetch) #f_id * #H lapply (opt_eq_from_res ???? H) -H #EQfunc_of_block #H elim (bind_inversion ????? H) -H #stmt' * #H lapply (opt_eq_from_res ???? H) -H #EQstmt_at whd in ⊢ (??%%→?); #EQ destruct(EQ) #EQeval cases (good fn (pi2 … (sigma_function_name p graph_prog fn))) letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at #entry_0 #good_local * * #wf_pc #wf_state #EQst2 generalize in match wf_pc in ⊢ ?; whd in ⊢ (%→?); inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ] #lin_pc whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta >EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?); #H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt * #EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_ elim (good_local … EQsigma) -good_local #stmt' * change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?) >EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ) #H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta >(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ] change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?); letin lin_fun ≝ (\fst  (linearise_int_fun p globals graph_fun)) change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?); * #EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec letin lin_prog ≝ (linearise … graph_prog) lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2)) destruct(EQst2) whd in match eval_state in ⊢ (???%→?); normalize nodelta letin st2 ≝ (sigma_state_pc ????? st1 ?) >(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?); >m_return_bind in ⊢ (%→?); #ex' (* resolve classifier *) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); normalize nodelta cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex'; [ * [ #stmt #nxt whd in match eval_statement in ⊢ (?→%→?); normalize nodelta #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec whd in match (graph_to_lin_statement ???) in ⊢ (%→?); whd in match eval_statement in ⊢ (%→?); normalize nodelta elim (IO_bind_inversion ??????? EQeval) #st1_no_pc * #EQeval_no_pc #EQeval_pc >(eval_seq_no_pc_sigma_commute … EQeval_no_pc) [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ] >m_return_bind cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec; [14: #f #args #dest | #c | #lbl | #move_sig | #a | #a | #sy #sy_prf #dpl #dph | #op #a #b #arg1 #arg2 | #op #a #arg | #op #a #arg1 #arg2 || | #a #dpl #dph | #dpl #dph #a | #s_ext ] [ (* CALL *) |(*:*) normalize nodelta #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec whd in match eval_seq_pc; normalize nodelta #ex1 cases next_spec [ #EQnext_sigma %[2: %{(taaf_step … (taa_base …) ex1 ?)} [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|] normalize nodelta cut (? : Prop) [3: #R' % [ %{I R'} ] |*:] [ cases daemon (* TODO lemma joint_label_sigma_commute *) | % [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon | whd in match eval_seq_pc in EQeval_pc; whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?); destruct (EQeval_pc) whd in ⊢ (??%%); change with (sigma_pc ??????) in match (pc ? (sigma_state_pc ???????)); whd in match (succ_pc ????) in ⊢ (??%%); whd in match (point_of_succ ???) in ⊢ (??%%); >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma) whd in match sigma_pc in ⊢ (???%); whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta @opt_safe_elim #pc' >EQfunc_of_block >m_return_bind whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >EQnext_sigma whd in ⊢ (??%?→?); whd in match pc_of_point; normalize nodelta #EQ destruct(EQ) >sigma_pblock_eq_lemma % ] ] | -next_spec #next_spec % whd in ⊢ (?→???%→?); generalize in ⊢ (??%? → ???(????%) → ?); |*: skip] | #a #lbltrue #next ] #next change with label in next; | * [ #lbl | | #fl #f #args ] ] whd in match eval_statement in ⊢ (?→%→?); normalize nodelta #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec normalize nodelta whd in match (graph_to_lin_statement ???) in ⊢ (%→?); whd in match eval_statement in ⊢ (%→?); normalize nodelta [ >m_return_bind in ⊢ (%→?); >m_return_bind in EQeval; (* common for all non-call seq *) >m_return_bind in ⊢ (%→?); whd in ⊢ (??%%→?); #EQ destruct(EQ) >m_return_bind in ⊢ (%→?); #ex1 lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2)) whd in match (point_of_pc ???); whd in match (point_of_succ ???); whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim #pc' #H elim (bind_opt_inversion ????? H) #fn * #EQbl -H #H elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) whd in match (succ_pc ????); whd in match (point_of_succ ???); change with (point_of_offset ???) in match (point_of_pc ???); >point_of_offset_of_point whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' whd in match sigma_pc_opt; normalize nodelta whd in match (succ_pc ????); change with next in match (offset_of_point ???) in ⊢ (???%); whd in fetch_statement_spec : (??()%); cases cl in classified_st1_cl; -cl #classified_st1_cl whd [4: >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog) cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ] #sigma_entry_is_zero #sigma_spec lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1))) -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ] -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec cases (opt_Exists_elim … sigma_spec) in ⊢ ?; * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved #related_lin_stm_graph_stm inversion (stmt_implicit_label ???) [ whd in match (opt_All ???); #stmt_implicit_spec #_ letin st2_opt' ≝ (eval_state … (ev_genv (lin_prog_params … lin_prog lin_stack_sizes)) (sigma_state_pc … wf_st1)) cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2') [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec' normalize nodelta in st2_spec'; -st2_opt' %{st2'} %{(taaf_step … (taa_base …) …)} [ cases daemon (* TODO, together with the previous one? *) | @st2_spec' ] %[%] [%] [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec'; >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec'; >m_return_bind (* Case analysis over the possible statements *) inversion graph_stmt in stmt_implicit_spec; normalize nodelta [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ] XXXXXXXXXX siamo qua, caso GOTO e RETURN | cases daemon (* TODO, after the definition of label_rel, trivial *) ] ] | .... qed. [ * [ * [ letin C_COMMENT ≝ 0 in ⊢ ?; #c | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl | letin C_MOVE ≝ 0 in ⊢ ?; #move_sig | letin C_POP ≝ 0 in ⊢ ?; #a | letin C_PUSH ≝ 0 in ⊢ ?; #a | letin C_ADDRESS ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph | letin C_OPACCS ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2 | letin C_OP1 ≝ 0 in ⊢ ?; #op #a #arg | letin C_OP2 ≝ 0 in ⊢ ?; #op #a #arg1 #arg2 | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?; | letin C_SET_CARRY ≝ 0 in ⊢ ?; | letin C_LOAD ≝ 0 in ⊢ ?; #a #dpl #dph | letin C_STORE ≝ 0 in ⊢ ?; #dpl #dph #a | letin C_CALL ≝ 0 in ⊢ ?; #f #args #dest | letin C_EXT ≝ 0 in ⊢ ?; #s_ext ] | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue ] #next change with label in next; | * [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl | letin C_RETURN ≝ 0 in ⊢ ?; | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args ] ]