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/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.