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/joint/StatusSimulationHelper.ma

    r2863 r2883  
    4444 @Hr
    4545]
    46 qed.
    47 
    48 check joint_classify
    49 check as_label
     46qed.
     47
     48
     49definition step_to_seq : ∀p : prog_params.∀stmt : joint_step p (globals p).
     50joint_classify_step p stmt = cl_other →
     51(∀c.stmt ≠ COST_LABEL ?? c) → Σ seq.stmt = step_seq ?? seq ≝
     52λp,stmt,CL_OTHER,COST.
     53(match stmt return λx.x = stmt → ? with
     54[ COST_LABEL c ⇒ λprf.⊥
     55| CALL id args dest ⇒ λprf.⊥
     56| COND r lab ⇒ λprf.⊥
     57| step_seq seq ⇒ λprf.«seq,?»
     58])(refl …).
     59@hide_prf
     60[ lapply(COST c) * #H @H >prf %
     61|2,3: <prf in CL_OTHER; whd in match (joint_classify_step ??); #EQ destruct(EQ)
     62| >prf %
     63]
     64qed.
     65 
    5066
    5167record good_state_relation (P_in : sem_graph_params)
     
    5975                                stack_sizes)
    6076        → Prop) : Prop ≝
    61 { pc_eq_sigma_commute : ∀st1,st2.R st1 st2 → pc … st1 = pc … st2
     77{ pc_eq_sigma_commute : ∀st1,st2,f,fn,stmt.R st1 st2 →
     78                 fetch_statement ? (prog_var_names … prog)
     79                     (globalenv_noinit … prog) (pc … st1)  = return 〈f,fn,stmt〉 →
     80                 pc … st1 = pc … st2
    6281; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes).
    6382                ∀st2 : joint_abstract_status ?.
     
    7089    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    7190    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    72     ∀f,fn,a,ltrue,lfalse.
    73     eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
    74     st1 = return st1' →
     91    ∀f,fn,a,ltrue,lfalse.
    7592    let cond ≝ (COND P_in ? a ltrue) in
    7693    fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
    77     return 〈f, fn,  sequential … cond lfalse〉 →
     94    return 〈f, fn,  sequential … cond lfalse〉 → 
     95    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
     96    st1 = return st1' →
    7897    R st1 st2 →
    7998    ∀t_fn.
     
    82101    bind_new_P' ??
    83102     (λregs1.λdata.bind_new_P' ??
    84      (λregs2.λblp.
    85         ∀mid,nxt1.
     103     (λregs2.λblp.(\snd blp) = [ ] ∧
     104        ∀mid.
    86105          stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
    87           = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1
     106          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse
    88107         ∃st2_pre_mid_no_pc.
    89108            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid)
     
    95114                                ((\snd (\fst blp)) mid)  = cl_jump ∧
    96115            cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
    97                                (sequential P_out ? ((\snd (\fst blp)) mid) nxt1) = None ? ∧
    98             (\snd blp) = [ ] ∧
     116                               (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
    99117            ∃st2_mid .
    100118                eval_state P_out (prog_var_names … trans_prog)
     
    103121   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
    104122  ) (init ? fn)
     123; seq_commutation :
     124  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     125  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     126  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
     127  ∀f,fn,stmt,nxt.
     128  let seq ≝ (step_seq P_in ? stmt) in
     129  fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
     130  return 〈f, fn,  sequential … seq nxt〉 → 
     131  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
     132  st1 = return st1' →
     133  R st1 st2 →
     134  ∀t_fn.
     135  fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
     136  return 〈f,t_fn〉 →
     137  bind_new_P' ??
     138     (λregs1.λdata.bind_new_P' ??
     139     (λregs2.λblp.
     140           ∀mid,mid1.
     141            stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
     142            = return sequential P_out ? ((\snd (\fst blp)) mid) mid1→
     143            ∃CL_OTHER : joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
     144                          ((\snd (\fst blp)) mid)  = cl_other.
     145            ∃COST : cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
     146                         (sequential P_out ? ((\snd (\fst blp)) mid) mid1) = None ?.
     147            ∃st2_fin_no_pc.
     148            let pre ≝ (map_eval ?? (\fst (\fst blp)) mid) in
     149            let middle ≝ [pi1 ?? (step_to_seq (mk_prog_params P_out trans_prog stack_sizes)
     150                                  ((\snd (\fst blp)) mid) CL_OTHER ?)] in
     151           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
     152              (pre@ middle @ (\snd blp))  (st_no_pc … st2)= return st2_fin_no_pc ∧
     153           let st2_fin ≝
     154           mk_state_pc ? st2_fin_no_pc
     155                         (pc_of_point P_out (pc_block(pc … st2)) nxt)
     156                         (last_pop … st2) in
     157           R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
     158      ) (init ? fn)         
    105159}.
    106 
     160@hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     161qed.
    107162
    108163lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     
    135190#f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed
    136191cases(b_graph_transform_program_fetch_statement … good … EQfetch)
    137 #init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2)
     192#init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
    138193#EQt_fn1 whd in ⊢ (% → ?); #Hinit
    139194* #labs * #regs
     
    142197[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
    143198  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
    144   * #_ >(pc_eq_sigma_commute … goodR … Rst1st2) whd in match point_of_pc;
     199  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
    145200  normalize nodelta whd in match (point_of_offset ??); <ABS
    146201  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
    147202]
    148 #_ <(pc_eq_sigma_commute … goodR … Rst1st2) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1
     203#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1
    149204* #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
    150205* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    151 cases(bind_new_bind_new_instantiates … EQbl
    152             (bind_new_bind_new_instantiates … Hinit
    153                (cond_commutation … goodR … EQeval EQfetch Rst1st2 t_fn1 EQt_fn1))
    154             … EQmid)   
    155 #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *** #CL_JUMP #COST #EQ destruct(EQ) *
    156 #st2_mid * #EQst2mid #Hst2_mid whd in ⊢(% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    157 %{st2_mid} %{Hst2_mid}
    158 >(pc_eq_sigma_commute … goodR … Rst1st2) in seq_pre_l; #seq_pre_l
     206cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
     207               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
     208#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
     209cases(APP … EQmid) -APP
     210#st_pre_mid_no_pc * #EQst_pre_mid_no_pc ** #CL_JUMP #COST *
     211#st2_mid * #EQst2mid #Hst2_mid %{st2_mid} %{Hst2_mid}
     212>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
    159213lapply(taaf_to_taa ???
    160214           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
     
    174228qed.
    175229
     230(*
     231let rec taa_to_taaf  S st1 st2 (taa : trace_any_any S st1 st2) on taa :
     232trace_any_any_free S st1 st2 ≝
     233(match taa in trace_any_any return λs1,s2.λx.st1 = s1 → st2 = s2 → taa ≃ x → trace_any_any_free S s1 s2 with
     234[taa_base st1' ⇒ λprf.?
     235|taa_step st1' st2' st3' H I J tl ⇒ λprf.?
     236]) (refl … st1) (refl … st2) (refl_jmeq ? taa).
     237*)
     238
     239lemma general_eval_seq_no_call_ok : ∀ P_in , P_out: sem_graph_params.
     240∀prog : joint_program P_in.
     241∀stack_sizes.
     242∀ f_lbls,f_regs.∀f_bl_r.∀init.
     243∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     244let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     245let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     246let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     247∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
     248good_state_relation P_in P_out prog stack_sizes init R →
     249∀st1,st1' : joint_abstract_status prog_pars_in.
     250∀st2 : joint_abstract_status prog_pars_out.
     251∀f.
     252∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
     253∀stmt,nxt.
     254R st1 st2 →
     255    let seq ≝ (step_seq P_in ? stmt) in
     256 fetch_statement P_in …
     257  (globalenv_noinit ? prog) (pc … st1) =
     258    return 〈f, fn,  sequential ?? seq nxt〉 →
     259 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
     260            st1 = return st1' →
     261∃st2'. R st1' st2' ∧           
     262∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
     263 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
     264(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
     265 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
     266#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1'
     267#st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
     268cases(b_graph_transform_program_fetch_statement … good … EQfetch)
     269#init_data * #t_fn ** >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
     270#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta ***
     271#blp #blm #bls * @if_elim
     272[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
     273  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
     274  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
     275  normalize nodelta whd in match (point_of_offset ??); <ABS
     276  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
     277]
     278#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl
     279>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC lapply SBiC
     280whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
     281#_ whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
     282#_
     283cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
     284               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
     285[4: @EQmid |*:] #COST * #CL_OTHER * #st2_fin_no_pc normalize nodelta cases(step_to_seq ????)
     286    #seq_mid cases daemon (*TODO*)
     287    qed.
     288   
     289(*   
     290    cases(blm mid1) in
     291#stmt_at_middle #EQstmt_at_middle normalize nodelta * >EQstmt_at_middle in SBiC;  destruct(EQ) whd in ⊢ (??%% → ?);#EQ destruct(EQ)
     292
     293
     294* #EQst2_pre_mid_no_pc
     295* #st2_mid * #EQst2_mid * #st2_fin_no_pc * #EQst2_fin_no_pc #Hfin
     296%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
     297%{Hfin}
     298lapply(taaf_to_taa ???
     299           (produce_trace_any_any_free ? st2 f t_fn ??? st2_pre_mid_no_pc EQt_fn
     300                                       seq_pre_l EQst2_pre_mid_no_pc) ?)
     301[ @if_elim #_ [2: @I] % whd in match as_costed; normalize nodelta
     302  whd in match (as_label ??); whd in match fetch_statement; normalize nodelta
     303  >EQt_fn >m_return_bind whd in match (as_pc_of ??); whd in match point_of_pc;
     304  normalize nodelta >point_of_offset_of_point >EQmid >m_return_bind
     305  normalize nodelta >COST * #H @H %]
     306#taa1
     307letin st2_mid_pc ≝ (mk_state_pc ? st2_mid
     308                                (pc_of_point P_out (pc_block (pc … st2)) mid2)
     309                                (last_pop … st2))
     310<(point_of_pc_of_point P_out (pc_block (pc … st2)) mid2) in seq_post_l;
     311#seq_post_l
     312lapply (produce_trace_any_any_free (mk_prog_params P_out ? stack_sizes)
     313                     st2_mid_pc f t_fn ??? st2_fin_no_pc EQt_fn
     314                                       (seq_post_l) EQst2_fin_no_pc)
     315* #taaf2 * #taaf2_prf1 #taaf2_prf2
     316%{(taaf_append_taaf ???? (taaf_step ???? taa1 ??) taaf2 ?)}
     317[ @hide_prf @if_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H #_
     318  % whd in match (as_costed ??); whd in match (as_label ??);
     319  whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
     320  >EQt_fn >m_return_bind whd in match point_of_pc; normalize nodelta
     321  >point_of_offset_of_point lapply(taaf2_prf2 H) lapply seq_post_l cases bls
     322  [ #_ *] #stmt1 #tl * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQstmt1
     323  >point_of_pc_of_point change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #_ #_
     324  >point_of_pc_of_point in EQstmt1; #EQstmt1 >EQstmt1 >m_return_bind normalize nodelta
     325  * #H @H %
     326| @hide_prf whd whd in match eval_state; normalize nodelta whd in match fetch_statement;
     327  normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid
     328  >m_return_bind >EQst2_mid >m_return_bind whd in match eval_statement_advance;
     329  normalize nodelta lapply COST lapply CL_OTHER lapply EQmid cases(blm mid1)
     330  normalize nodelta
     331  [ #c #_ #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
     332  | #id #args #dest #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
     333  | #r #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
     334  | #jseq #EQjseq #_ #_ %
     335  ]
     336| @hide_prf whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn
     337  >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind assumption
     338| @if_elim #_ [%] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
     339]
     340qed.
     341*)
Note: See TracChangeset for help on using the changeset viewer.