Changeset 2898 for src


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

Location:
src
Files:
3 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 #_

  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2889 r2898  
    2121λprog : ltl_program.λstack_sizes.
    2222joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
    23 
    24 axiom sigma_stored_pc : ertlptr_program → (block → label → list label) → 
    25 program_counter → program_counter.
    26 
    2723
    2824definition clear_sb_type ≝ label → decision → bool.
    … …  
    8177  ].
    8278
     79include "joint/StatusSimulationHelper.ma".
     80
    8381definition sigma_sb_state_pc :fixpoint_computer → coloured_graph_computer → 
    8482ertlptr_program → (block → label → list label) →
    … …  
    9290     let coloured_graph ≝ build … (\snd y) after in
    9391     mk_state_pc ? (sigma_sb_state prog f_lbls f_regs
    94                           (to_be_cleared_sb after coloured_graph) st) (pc … st) 
    95                           (sigma_stored_pc prog f_lbls (last_pop … st))
     92                       (to_be_cleared_sb after coloured_graph) st) (pc … st) 
     93                   (sigma_stored_pc ERTLptr_semantics LTL_semantics
     94                                    prog f_lbls (last_pop … st))
    9695  | Error e ⇒ dummy_state_pc
    9796  ].
     97
     98definition state_rel : fixpoint_computer → coloured_graph_computer →
     99ertlptr_program → (block → label → list label) → (block → label → list register) →
     100(Σb:block.block_region b = Code) → state ERTL_state → state LTL_LIN_state → Prop ≝
     101λfix_comp,build,prog,f_lbls,f_regs,bl,st1,st2.
     102∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
     103let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     104let coloured_graph ≝ build … fn after in
     105(sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb after) st1) =
     106(sigma_sb_state prog f_lbls f_regs
     107                       (to_be_cleared_sb after coloured_graph) st2).
    98108
    99109axiom write_decision : decision → beval → state LTL_LIN_state →
    … …  
    132142       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
    133143          .λs2:Σs:LTL_status ??.as_classifier ? s cl_call
    134            .pc ? s1 =sigma_stored_pc prog f_lbls (pc ? s2))
     144           .pc ? s1 =sigma_stored_pc ERTLptr_semantics LTL_semantics
     145                                                          prog f_lbls (pc ? s2))
    135146    (* sim_final ≝ *) ?.
    136147cases daemon
    … …  
    167178
    168179
    169 lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.
    170  #T #x #y #EQ destruct %
    171 qed.
    172 
    173180
    174181axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
    … …  
    186193∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    187194     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    188 ∀st1,st2,f,fn,stmt.
    189 fetch_statement ERTLptr_semantics (prog_var_names … prog) (globalenv_noinit … prog)
    190                 (pc … st1) = return 〈f,fn,stmt〉 →
     195∀st1,st2,f,fn.
     196fetch_internal_function ? (globalenv_noinit … prog)
     197                (pc_block (pc … st1)) = return 〈f,fn〉 →
    191198let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
    192199R st1 st2 →
    193200(pc … st1) = (pc … st2).
    194201
    195 
     202(*
    196203axiom change_pc_sigma_commute : ∀fix_comp,colour.
    197204∀prog.∀ f_lbls,f_regs.∀f_bl_r.
    … …  
    203210∀pc1,pc2.pc1 = pc2 →
    204211R (set_pc … pc1 st1) (set_pc … pc2 st2).
    205 (*
     212
    206213axiom globals_commute : ∀fix_comp,colour.
    207214∀prog.
    208215∀p_out,m,n.
    209216∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
    210 prog_var_names … prog = prog_var_names … p_out.*)
     217prog_var_names … prog = prog_var_names … p_out.
    211218
    212219lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C.
    213220〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3).
    214221#H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] //
    215 qed.
     222qed.*)
    216223
    217224include "joint/semantics_blocks.ma".
    218225include "ASM/Util.ma".
    219 include "joint/StatusSimulationHelper.ma".
    220 
    221226
    222227axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.
    … …  
    350355good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
    351356 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
     357 init_regs f_lbls f_regs good (state_rel fix_comp colour prog f_lbls f_regs)
    352358 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
    353359#fix_comp #colour #prog
    … …  
    356362#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
    357363%
    358 [ #st1 #st2 #f #fn #stmt #Rst1st2 #EQstmt >(pc_eq_sigma_commute … good … EQstmt Rst1st2) %
     364[ #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
     365  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
     366  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn
     367  normalize nodelta #H cases(state_pc_eq … H) * #H1 #_ #_ whd %{f} %{fn} %{EQfn}
     368  assumption
     369| #st1 #st2 #f #fn #Rst1st2 #EQfetcn >(pc_eq_sigma_commute … good … EQfetcn Rst1st2) %
     370| #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
     371  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
     372  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn normalize nodelta
     373   #H cases(state_pc_eq … H) * #_ #_ //
     374| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
     375  #EQ destruct(EQ) normalize nodelta #state_rel #EQ destruct(EQ) whd
     376  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
     377  >EQfn >EQfn normalize nodelta //
    359378| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
    360379| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
    361380  #EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc;
    362   normalize nodelta
    363   >EQfetch >m_return_bind normalize nodelta >m_return_bind
     381  normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
    364382  whd in match eval_statement_advance; normalize nodelta
    365383  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
    … …  
    385403  %{st2_pre_mid_no_pc}
    386404  %
    387   [1,3: >map_eval_add_dummy_variance_id @move_spec]
    388   % [1,3: % %] %{(mk_state_pc ? st2_pre_mid_no_pc
    389                        (pc_of_point LTL_semantics (pc_block (pc … st2)) ?)
    390                         (last_pop … st2))} [@ltrue |3: @lfalse]
    391   change with prog_pars_out in match (mk_prog_params ???); %
    392   [1,3: whd in match eval_state; whd in match eval_statement_no_pc;
    393         whd in match fetch_statement; normalize nodelta
    394        >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
    395         normalize nodelta >m_return_bind
    396         change with prog_pars_out in match (mk_prog_params ???);
    397         whd in match eval_statement_advance; normalize nodelta
    398         change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
    399         whd in match set_no_pc; normalize nodelta
    400         >hw_reg_retrieve_write_decision_hit >m_return_bind
    401         cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog … good fn … Rst1st2 … EQbv)
     405  [1,3: >map_eval_add_dummy_variance_id %
     406       [1,3: %
     407            [1,3: %
     408                 [1,3: @move_spec
     409                 |*: lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
     410                     whd in match sigma_sb_state_pc; normalize nodelta >EQfn
     411                     <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
     412                     normalize nodelta #EQ cases(state_pc_eq … EQ) *
     413                     #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn}
     414                     <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
     415                                          (point_of_pc ERTLptr_semantics (pc … st2)))
     416                     [2,4: @dead_registers_in_dead @acc_is_dead ]
     417                     assumption
     418                 ]
     419            |*: %
     420            ]
     421       |*: %
     422       ]
     423  |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
     424      >hw_reg_retrieve_write_decision_hit >m_return_bind
     425      cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog …
     426                                                        good fn … Rst1st2 … EQbv)
    402427        [2,4: @(all_used_are_live_before … EQstmt)
    403428            [1,3: @set_member_singl |*: % ] ] #bv' * #EQbv' #EQbv1
    … …  
    405430        >EQbv' in EQbool; #EQbool
    406431        >(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind
    407         normalize nodelta [2: %] whd in match goto; normalize nodelta
    408         >(pc_of_label_eq … EQt_fn1) %
    409   |2,4: whd whd in match sigma_fb_state_pc; normalize nodelta
    410         whd in match sigma_sb_state_pc; normalize nodelta
    411         change with (pc_block (pc … st1)) in match (pc_block ?);
    412         cases(fetch_statement_inv … EQfetch) #EQfn #_ >EQfn
    413         normalize nodelta <(pc_eq_sigma_commute … good … EQfetch Rst1st2)
    414         change with (pc_block (pc … st1)) in ⊢ (???match (???%) with [_⇒ ? | _ ⇒ ?]);
    415         >EQfn normalize nodelta
    416         lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
    417          whd in match sigma_sb_state_pc; normalize nodelta >EQfn
    418          <(pc_eq_sigma_commute … good … EQfetch Rst1st2) >EQfn normalize nodelta
    419          #EQ cases(state_pc_eq … EQ) * #EQst1st2 #EQpc #EQlp @eq_f3
    420         [3,6:  assumption
    421         |2,5: %
    422         |*: <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
    423                (point_of_pc ERTLptr_semantics (pc … st2)))
    424             [2,4: @dead_registers_in_dead @acc_is_dead ]
    425             assumption
    426         ]
     432        normalize nodelta
     433        [2: <(pc_eq_sigma_commute … good … EQfn Rst1st2) %]
     434        whd in match goto; normalize nodelta
     435        >(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) %
    427436  ]
    428 | letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
     437| xxxxxxxxxxxx
     438 letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
    429439  letin p_out ≝ (mk_prog_params LTL_semantics ??)
    430440  letin trans_prog ≝ (b_graph_transform_program ????)

  • src/joint/StatusSimulationHelper.ma

    r2891 r2898  
    4646qed.
    4747
     48definition joint_state_relation ≝
     49λP_in,P_out.(Σb:block.block_region b=Code) → state P_in → state P_out → Prop.
     50
     51definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
     52
     53definition sigma_map ≝  block → label → option label.
     54definition lbl_funct ≝  block → label → (list label).
     55definition regs_funct ≝ block → label → (list register).
     56
     57definition get_sigma : ∀p : sem_graph_params.
     58joint_program p → lbl_funct → sigma_map ≝
     59λp,prog,f_lbls.λbl,searched.
     60let globals ≝ prog_var_names … prog in
     61let ge ≝ globalenv_noinit … prog in
     62! bl ← code_block_of_block bl ;
     63! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
     64!〈res,s〉 ← find ?? (joint_if_code  ?? fn)
     65                (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with
     66                          [None ⇒ eq_identifier … searched lbl
     67                          |Some x ⇒ eq_identifier … searched (\snd x)
     68                          ]);
     69return res.
     70
     71definition sigma_pc_opt :  ∀p_in,p_out : sem_graph_params.
     72joint_program p_in →  lbl_funct →
     73program_counter → option program_counter ≝
     74λp_in,p_out,prog,f_lbls,pc.
     75  let sigma ≝ get_sigma p_in prog f_lbls in
     76  let ertl_ptr_point ≝ point_of_pc p_out pc in
     77  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
     78    return pc
     79  else
     80       ! point ← sigma (pc_block pc) ertl_ptr_point;
     81       return pc_of_point p_in (pc_block pc) point.
     82
     83definition sigma_stored_pc ≝
     84λp_in,p_out,prog,f_lbls,pc. match sigma_pc_opt p_in p_out prog f_lbls pc with
     85      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
     86
    4887record good_state_relation (P_in : sem_graph_params)
    4988   (P_out : sem_graph_params) (prog : joint_program P_in)
    5089   (stack_sizes : ident → option ℕ)
    5190   (init : ∀globals.joint_closed_internal_function P_in globals
    52          →bound_b_graph_translate_data P_in P_out globals)
    53    (R : joint_abstract_status (mk_prog_params P_in prog stack_sizes) →
    54         joint_abstract_status (mk_prog_params P_out
    55                                 (b_graph_transform_program P_in P_out init prog)
    56                                 stack_sizes)
    57         → Prop) : Prop ≝
    58 { pc_eq_sigma_commute : ∀st1,st2,f,fn,stmt.R st1 st2 →
    59                  fetch_statement ? (prog_var_names … prog)
    60                      (globalenv_noinit … prog) (pc … st1)  = return 〈f,fn,stmt〉 →
    61                  pc … st1 = pc … st2
    62 ; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes).
    63                 ∀st2 : joint_abstract_status ?.
    64                 ∀f,fn,stmt.
    65                   fetch_statement ? (prog_var_names … prog)
    66                   (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 →
    67                   R st1 st2 → as_label ? st1 = as_label ? st2
     91         →bound_b_graph_translate_data P_in P_out globals)
     92   (f_bl_r : block → list register) (f_lbls : lbl_funct) (f_regs : regs_funct)
     93   (good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs)
     94   (st_no_pc_rel : joint_state_relation P_in P_out)
     95   (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝
     96{ fetch_ok_sigma_state_ok :
     97   ∀st1,st2,f,fn. st_rel st1 st2 →
     98    fetch_internal_function ? (globalenv_noinit … prog)
     99     (pc_block (pc … st1))  = return 〈f,fn〉 →
     100     st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1) (st_no_pc … st2)
     101; fetch_ok_pc_ok :
     102  ∀st1,st2,f,fn.st_rel st1 st2 →
     103   fetch_internal_function ? (globalenv_noinit … prog)
     104  (pc_block (pc … st1))  = return 〈f,fn〉 →
     105   pc … st1 = pc … st2
     106; fetch_ok_sigma_last_pop_ok :
     107  ∀st1,st2,f,fn.st_rel st1 st2 →
     108   fetch_internal_function ? (globalenv_noinit … prog)
     109    (pc_block (pc … st1))  = return 〈f,fn〉 →
     110   (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2)
     111; st_rel_def :
     112  ∀st1,st2,pc,lp1,lp2,f,fn.
     113  fetch_internal_function ? (globalenv_noinit … prog)
     114   (pc_block pc) = return 〈f,fn〉 → st_no_pc_rel (pc_block pc) st1 st2 →
     115   lp1 = sigma_stored_pc P_in P_out prog f_lbls lp2 →
     116  st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
     117; as_label_ok :     let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     118  ∀st1,st2,f,fn,stmt.
     119   fetch_statement ? (prog_var_names … prog)
     120   (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 →
     121   st_rel st1 st2 →
     122   as_label (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 =
     123    as_label (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) st2
    68124; cond_commutation :
    69125    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    … …  
    76132    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
    77133    st1 = return st1' →
    78     R st1 st2 →
     134    st_rel st1 st2 →
    79135    ∀t_fn.
    80136    fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
    … …  
    90146                                   (st_no_pc ? st2)
    91147            = return st2_pre_mid_no_pc ∧
    92             let st2_pre_mid ≝ mk_state_pc ? st2_pre_mid_no_pc (pc_of_point P_out (pc_block (pc … st2)) mid)
    93                                             (last_pop … st2) in
     148            st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
    94149            joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
    95150                                ((\snd (\fst blp)) mid)  = cl_jump ∧
    96151            cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
    97152                               (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
    98             ∃st2_mid .
    99                 eval_state P_out (prog_var_names … trans_prog)
    100                 (ev_genv (mk_prog_params P_out trans_prog stack_sizes)) st2_pre_mid =
    101                 return st2_mid ∧ R st1' st2_mid
     153            let st2_pre_mid ≝  mk_state_pc P_out st2_pre_mid_no_pc
     154                               (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in
     155            let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in
     156            eval_statement_advance P_out (prog_var_names … trans_prog)
     157             (ev_genv … (mk_prog_params P_out trans_prog stack_sizes)) f t_fn
     158             (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'
    102159   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
    103   ) (init ? fn)
     160  ) (init ? fn) 
    104161; seq_commutation :
    105162  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    … …  
    112169  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
    113170  st1 = return st1' →
    114   R st1 st2 →
     171  st_rel st1 st2 →
    115172  ∀t_fn.
    116173  fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
    … …  
    118175  bind_new_P' ??
    119176     (λregs1.λdata.bind_new_P' ??
    120      (λregs2.λblp.
     177      (λregs2.λblp.
    121178       ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes)
    122179                            (globals (mk_prog_params P_out trans_prog stack_sizes))).
    … …  
    125182           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
    126183              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
    127            let st2_fin ≝
    128            mk_state_pc ? st2_fin_no_pc
    129                          (pc_of_point P_out (pc_block(pc … st2)) nxt)
    130                          (last_pop … st2) in
    131            R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
    132       ) (init ? fn)         
     184           st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1') st2_fin_no_pc
     185      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
     186     ) (init ? fn)
    133187}.
    134188
     189lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
     190∀prog : joint_program P_in.
     191∀stack_sizes.
     192∀ f_lbls,f_regs.∀f_bl_r.∀init.
     193∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     194∀st_no_pc_rel,st_rel.
     195∀f,fn,stmt,st1,st2.
     196good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
     197                    st_no_pc_rel st_rel →
     198st_rel st1 st2 →
     199fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
     200 return 〈f,fn,stmt〉 →
     201st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1) (st_no_pc … st2).
     202#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
     203#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
     204cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     205@(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
     206qed.
     207
     208lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
     209∀prog : joint_program P_in.
     210∀stack_sizes.
     211∀ f_lbls,f_regs.∀f_bl_r.∀init.
     212∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     213∀st_no_pc_rel,st_rel.
     214∀f,fn,stmt,st1,st2.
     215good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
     216                    st_no_pc_rel st_rel →
     217st_rel st1 st2 →
     218fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
     219 return 〈f,fn,stmt〉 →
     220pc … st1 = pc … st2.
     221#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
     222#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
     223cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     224@(fetch_ok_pc_ok … goodR … EQfn) assumption
     225qed.
     226
     227lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
     228∀prog : joint_program P_in.
     229∀stack_sizes.
     230∀ f_lbls,f_regs.∀f_bl_r.∀init.
     231∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     232∀st_no_pc_rel,st_rel.
     233∀f,fn,stmt,st1,st2.
     234good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
     235                    st_no_pc_rel st_rel →
     236st_rel st1 st2 →
     237fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
     238 return 〈f,fn,stmt〉 →
     239(last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2).
     240#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
     241#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
     242cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     243@(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption
     244qed.
     245
     246(*
     247lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params.
     248∀prog : joint_program P_in.
     249∀stack_sizes.
     250∀ f_lbls,f_regs.∀f_bl_r.∀init.
     251∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     252∀st_no_pc_rel,st_rel.
     253∀f,fn,stmt,st1,st2.
     254good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
     255                    st_no_pc_rel st_rel →
     256st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) →
     257(last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) →
     258fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
     259 return 〈f,fn,stmt〉 → st_rel st1 st2.
     260#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel
     261#st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ)
     262#EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     263@(st_rel_def … goodR … EQfn) assumption
     264qed.
     265*)
     266 
     267
    135268lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
    136269∀prog : joint_program P_in.
    … …  
    138271∀ f_lbls,f_regs.∀f_bl_r.∀init.
    139272∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     273∀st_no_pc_rel,st_rel.
    140274let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
    141275let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
    142276let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
    143 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
    144 good_state_relation P_in P_out prog stack_sizes init R →
     277good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
     278                    st_no_pc_rel st_rel →
    145279∀st1,st1' : joint_abstract_status prog_pars_in.
    146280∀st2 : joint_abstract_status prog_pars_out.
    … …  
    148282∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
    149283∀a,ltrue,lfalse.
    150 R st1 st2 →
     284st_rel st1 st2 →
    151285    let cond ≝ (COND P_in ? a ltrue) in
    152286 fetch_statement P_in …
    … …  
    156290            st1 = return st1' →
    157291as_costed (joint_abstract_status prog_pars_in) st1' →
    158 ∃ st2'. R st1' st2' ∧
     292∃ st2'. st_rel st1' st2' ∧
    159293∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
    160294bool_to_Prop (taaf_non_empty … taf).
    161 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' #st2
    162 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed
     295#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel
     296#goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval
     297@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     298whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     299#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
     300#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
     301cases(fetch_statement_inv … EQfetch) #EQfn #_
     302[ >(pc_of_label_eq … EQfn)
     303  normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
     304| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
     305]
     306#EQ destruct(EQ) #n_costed
    163307cases(b_graph_transform_program_fetch_statement … good … EQfetch)
    164 #init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
     308#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    165309#EQt_fn1 whd in ⊢ (% → ?); #Hinit
    166 * #labs * #regs
    167 ** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls *
     310* #labs * #regs ** #EQlabs #EQf_regs normalize nodelta *** #blp #blm #bls *
    168311whd in ⊢ (% → ?); @if_elim
    169 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
     312[1,3: @eq_identifier_elim [2,4: #_ *] whd in match point_of_pc; normalize nodelta
    170313  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
    171   * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
     314  * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
    172315  normalize nodelta whd in match (point_of_offset ??); <ABS
    173316  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
    174317]
    175 #_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1
    176 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
     318#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
     319#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
    177320* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    178321cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
    179322               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
    180323#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    181 cases(APP … EQmid) -APP
    182 #st_pre_mid_no_pc * #EQst_pre_mid_no_pc ** #CL_JUMP #COST *
    183 #st2_mid * #EQst2mid #Hst2_mid %{st2_mid} %{Hst2_mid}
    184 >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
     324cases(APP … EQmid) -APP #st_pre_mid_no_pc **** whd in match set_no_pc; normalize nodelta
     325#EQst_pre_mid_no_pc #Hsem #CL_JUMP #COST #Hst2_mid
     326[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
     327     (last_pop … st2))}
     328| %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse)
     329     (last_pop … st2))}
     330]
     331letin st1' ≝ (mk_state_pc P_in ???)
     332letin st2' ≝ (mk_state_pc P_out ???)
     333cut(st_rel st1' st2')
     334[1,3: @(st_rel_def … goodR … f fn ?)
     335      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
     336      |2,5: assumption
     337      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
     338      ]
     339]
     340#H_fin
     341%
     342[1,3: assumption]
     343>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
    185344lapply(taaf_to_taa ???
    186345           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
    187346                                       seq_pre_l EQst_pre_mid_no_pc) ?)
    188 [ @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
    189   whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
    190   whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
    191   >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
    192   #H @H %
    193 ] #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
    194 [ whd <(as_label_ok … goodR … Hst2_mid) [assumption] cases daemon (*TODO: general lemma!*)
    195 | whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
    196   >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
    197   assumption
    198 | assumption
     347[1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
     348      whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
     349      whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
     350      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
     351      #H @H %
     352]
     353#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
     354[1,4: whd <(as_label_ok ??????????? goodR st1' st2' f fn ?? H_fin) [1,4: assumption]
     355      cases daemon (*TODO: general lemma!*)
     356|2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
     357      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
     358      assumption
     359|*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
     360    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
     361    cases(blm mid1) in CL_JUMP COST Hst2_mid;
     362    [1,5: #c #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     363    |2,4,6,8: [1,3: #c_id #args #dest |*: #seq] whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     364    ]
     365    #r #ltrue #_ #_ #Hst2_mid whd in match eval_statement_no_pc; normalize nodelta
     366    >m_return_bind assumption
    199367]
    200368qed.
    … …  
    209377*)
    210378
    211 lemma general_eval_seq_no_call_ok : ∀ P_in , P_out: sem_graph_params.
    212 ∀prog : joint_program P_in.
    213 ∀stack_sizes.
    214 ∀ f_lbls,f_regs.∀f_bl_r.∀init.
    215 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     379lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
     380∀prog : joint_program P_in.
     381∀stack_sizes.
     382∀ f_lbls,f_regs.∀f_bl_r.∀init.
     383∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     384∀st_no_pc_rel,st_rel.
    216385let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
    217386let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
    218387let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
    219 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
    220 good_state_relation P_in P_out prog stack_sizes init R →
     388good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
     389                    st_no_pc_rel st_rel →
    221390∀st1,st1' : joint_abstract_status prog_pars_in.
    222391∀st2 : joint_abstract_status prog_pars_out.
    223 ∀f.
    224 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
     392∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
    225393∀stmt,nxt.
    226 R st1 st2 →
     394st_rel st1 st2 →
    227395    let seq ≝ (step_seq P_in ? stmt) in
    228396 fetch_statement P_in …
    … …  
    231399 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
    232400            st1 = return st1' →
    233 ∃st2'. R st1' st2' ∧           
     401∃st2'. st_rel st1' st2' ∧           
    234402∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
    235403 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
    236404(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
    237405 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
    238 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1'
    239 #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
     406#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel
     407#goodR #st1 #st1' #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
     408@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     409#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
     410#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
     411whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
    240412cases(b_graph_transform_program_fetch_statement … good … EQfetch)
    241 #init_data * #t_fn ** >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
     413#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    242414#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim
    243415[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
    244416  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
    245   * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
     417  * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
    246418  normalize nodelta whd in match (point_of_offset ??); <ABS
    247419  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
    248420]
    249 #_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl
    250 >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC
     421#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
     422>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
    251423cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
    252424               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
    253425#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
    254426%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
    255 %{Rsem} 
     427cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
     428#EQfn #_
     429%
     430[ @(st_rel_def ??????????? goodR … f fn)
     431      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
     432      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
     433      | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
     434      ]
     435]
    256436%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
    257437                                      SBiC EQst2_fin_no_pc)}
    258438@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
    259439qed.
     440
     441(*
     442lemma eval_cost_ok :
     443∀ P_in , P_out: sem_graph_params.
     444∀prog : joint_program P_in.
     445∀stack_sizes.
     446∀ f_lbls,f_regs.∀f_bl_r.∀init.
     447∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     448let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     449let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     450let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     451∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
     452∀st1,st1' : joint_abstract_status prog_pars_in.
     453∀st2 : joint_abstract_status prog_pars_out.
     454∀f.
     455∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt.
     456R st1 st2 →
     457let cost ≝ COST_LABEL P_in ? c in
     458 fetch_statement P_in …
     459  (globalenv_noinit ? prog) (pc … st1) =
     460    return 〈f, fn,  sequential ?? cost nxt〉 →
     461 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
     462            st1 = return st1' →
     463∃ st2'. R st1' st2' ∧
     464∃taf : trace_any_any_free
     465        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
     466        st2 st2'.
     467bool_to_Prop (taaf_non_empty … taf).
     468#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #good #R #st1 #st1'
     469#st2 #f #fn #c #nxt #Rst1st2 normalize nodelta #EQfetch whd in match eval_state;
     470whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
     471normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     472*)
Note: See TracChangeset for help on using the changeset viewer.