Changeset 2883 for src/ERTL


Ignore:
Timestamp:
Mar 15, 2013, 6:33:18 PM (7 years ago)
Author:
piccolo
Message:

partial commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2843 r2883  
    157157#EQt_fn >EQt_fn >m_return_bind >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_stmt;
    158158#EQt_stmt >EQt_stmt %
     159qed.
     160
     161include "joint/StatusSimulationHelper.ma".
     162
     163lemma make_ERTL_To_ERTLptr_good_state_relation :
     164∀prog : ertl_program.
     165let p_out ≝ ertl_to_ertlptr prog in
     166∀stack_sizes.
     167∃init_regs : block → list register.
     168∃f_lbls : block → label → list label.
     169∃f_regs : block → label → list register.
     170∃good : b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
     171        (λglobals,fn.«translate_data globals fn,(refl …)»)
     172        prog init_regs f_lbls f_regs.
     173good_state_relation ERTL_semantics ERTLptr_semantics prog stack_sizes
     174 (λglobals,fn.«translate_data globals fn,(refl …)»)
     175 (sem_rel … (ERTLptrStatusSimulation prog … good)).
     176#prog #stack_sizes
     177cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
     178          (λglobals,fn.«translate_data globals fn,(refl …)») prog)
     179#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
     180%
     181[#s1 #s2 #f #fn #stmt whd in ⊢ (% → ?); #EQ destruct(EQ) @fetch_stmt_ok_sigma_pc_ok
     182| #st1 #st2 #f #fn #stmt #EQfetch whd in ⊢ (% → ?); #EQ destruct(EQ)
     183  lapply(as_label_ok … good st2 … EQfetch) #EQ <EQ in ⊢ (??%?); %
     184| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn
     185  #a #ltrue #lfalse #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     186   whd in match eval_state; whd in match eval_statement_no_pc;
     187  normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
     188  whd in match eval_statement_advance; normalize nodelta
     189  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     190  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     191  #bv whd in match set_no_pc; normalize nodelta #EQbv
     192   #H @('bind_inversion H) -H * #EQbool normalize nodelta
     193   [whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
     194    >m_return_bind] whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     195  whd in ⊢ (% → ?); #EQ destruct(EQ) >(fetch_stmt_ok_sigma_state_ok … EQfetch) in EQbv;
     196  whd in match sigma_state; normalize nodelta #EQbv
     197  cases(ps_reg_retrieve_ok ?????? EQbv) #bv1 * #EQbv1 #EQ destruct(EQ)
     198  cases(bool_of_beval_ok … EQbool) #b * #EQb #EQ destruct(EQ) #t_fn #EQt_fn
     199  whd %{(refl …)} #mid #EQt_stmt %{(st_no_pc … st2)} %{(refl …)}
     200  % [1,3: %{(refl …)} %]
     201  %{(set_pc ? (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2)}
     202  [@ltrue |3: @lfalse] whd in match fetch_statement; normalize nodelta
     203  >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt >m_return_bind
     204  normalize nodelta >m_return_bind
     205  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     206  >EQbv1 >m_return_bind >EQb >m_return_bind normalize nodelta
     207  [ >(pc_of_label_eq … EQt_fn) >m_return_bind] %{(refl …)}
     208  whd whd in match sigma_state_pc; normalize nodelta
     209  change with (pc_block (pc … st2)) in match (pc_block ?);
     210  <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQfn %
     211]
    159212qed.
    160213
Note: See TracChangeset for help on using the changeset viewer.