Changeset 2898 for src/ERTL


Ignore:
Timestamp:
Mar 18, 2013, 10:03:37 AM (7 years ago)
Author:
piccolo
Message:

1) simplification of cond and seq case for StatusSimulationHelper? which has
been tested correct in ERTL to ERTlptr correctness proof.

2) the cond case for ERTLptr to LTL correctenss proof has been adapted to the
new specification

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2891 r2898  
    1414(**************************************************************************)
    1515
     16
     17include "joint/StatusSimulationHelper.ma".
    1618include "ERTL/ERTLtoERTLptrUtils.ma".
    1719
     
    159161qed.
    160162
    161 include "joint/StatusSimulationHelper.ma".
    162163include alias "basics/lists/listb.ma".
    163164
     165definition state_rel ≝ λprog : ertl_program.λf_lbls.
     166λf_regs : (block → label → list register).
     167λbl,st1,st2.∃f,fn.
     168fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
     169let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in
     170st1 = (sigma_state prog f_lbls f_regs added st2).
     171 
    164172lemma make_ERTL_To_ERTLptr_good_state_relation :
    165173∀prog : ertl_program.
     
    173181        prog init_regs f_lbls f_regs.
    174182good_state_relation ERTL_semantics ERTLptr_semantics prog stack_sizes
    175  (λglobals,fn.«translate_data globals fn,(refl …)»)
    176  (sem_rel … (ERTLptrStatusSimulation prog … good)).
     183 (λglobals,fn.«translate_data globals fn,(refl …)») init_regs f_lbls f_regs
     184 good (state_rel prog f_lbls f_regs)
     185 (sem_rel … (ERTLptrStatusSimulation prog … stack_sizes … good)).
    177186#prog #stack_sizes
    178187cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
     
    180189#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
    181190%
    182 [#s1 #s2 #f #fn #stmt whd in ⊢ (% → ?); #EQ destruct(EQ) @fetch_stmt_ok_sigma_pc_ok
     191[ #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn whd %{f} %{fn}
     192  >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta
     193  lapply EQfn >(fetch_ok_sigma_pc_ok … EQfn) #EQfn1 >EQfn1 %
     194| #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn @fetch_ok_sigma_pc_ok
     195  assumption
     196| #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn
     197  >(fetch_ok_sigma_last_pop_ok … f fn st2 EQfn) %
     198| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
     199  #EQ destruct(EQ) normalize nodelta #EQ destruct(EQ) #EQ destruct(EQ) whd
     200  whd in match sigma_state_pc; normalize nodelta >EQfn %
    183201| #st1 #st2 #f #fn #stmt #EQfetch whd in ⊢ (% → ?); #EQ destruct(EQ)
    184   lapply(as_label_ok … good st2 … EQfetch) #EQ <EQ in ⊢ (??%?); %
     202  lapply(as_label_ok … stack_sizes … good st2 … EQfetch) #EQ <EQ in ⊢ (??%?); %
    185203| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn
    186204  #a #ltrue #lfalse #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     
    194212   [whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
    195213    >m_return_bind] whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    196   whd in ⊢ (% → ?); #EQ destruct(EQ) >(fetch_stmt_ok_sigma_state_ok … EQfetch) in EQbv;
     214  whd in ⊢ (% → ?); #EQ destruct(EQ)
     215  >(fetch_stmt_ok_sigma_state_ok … EQfetch) in EQbv;
    197216  whd in match sigma_state; normalize nodelta #EQbv
    198217  cases(ps_reg_retrieve_ok ?????? EQbv) #bv1 * #EQbv1 #EQ destruct(EQ)
    199218  cases(bool_of_beval_ok … EQbool) #b * #EQb #EQ destruct(EQ) #t_fn #EQt_fn
    200   whd %{(refl …)} #mid #EQt_stmt %{(st_no_pc … st2)} %{(refl …)}
    201   % [1,3: %{(refl …)} %]
    202   %{(set_pc ? (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2)}
    203   [@ltrue |3: @lfalse] whd in match fetch_statement; normalize nodelta
    204   >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt >m_return_bind
    205   normalize nodelta >m_return_bind
    206   change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
    207   >EQbv1 >m_return_bind >EQb >m_return_bind normalize nodelta
    208   [ >(pc_of_label_eq … EQt_fn) >m_return_bind] %{(refl …)}
    209   whd whd in match sigma_state_pc; normalize nodelta
    210   change with (pc_block (pc … st2)) in match (pc_block ?);
    211   <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQfn %
     219  whd %{(refl …)} #mid #EQt_stmt %{(st_no_pc … st2)} %
     220  [1,3: %
     221       [1,3: %
     222             [1,3: %{(refl …)}
     223             |*: %
     224             ]
     225       |*: %
     226       ]
     227  |*: normalize nodelta 
     228      change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     229      >EQbv1 >m_return_bind >EQb >m_return_bind normalize nodelta
     230      [ >(pc_of_label_eq … EQt_fn) >m_return_bind]
     231      >(fetch_stmt_ok_sigma_pc_ok … EQfetch) %
     232   ]
     233  whd %{f} %{fn} >EQfn %{(refl …)} >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     234  cases st2 * #frms #is #b #regs #m #pc2 #lp2 %
    212235| #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state;
    213236  whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
     
    220243  -EQst1_no_pc' #EQst1_no_pc'
    221244  cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc')
    222   [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ)
    223   %{(mk_state_pc ? st2_no_pc'
    224      (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt)
    225      (last_pop … st2))} %
    226      [ whd in ⊢ (??%?); >EQst2_no_pc' %
    227      | whd whd in match sigma_state_pc; normalize nodelta >EQfn %
    228      ]
     245  [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ) %{st2_no_pc'} %
     246    [ whd in ⊢ (??%?); >EQst2_no_pc' %
     247    | whd %{f} %{fn} >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta
     248      >EQfn %
     249    ]
    229250  |  #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta
    230251  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_
Note: See TracChangeset for help on using the changeset viewer.