Changeset 2863


Ignore:
Timestamp:
Mar 13, 2013, 2:22:29 PM (4 years ago)
Author:
piccolo
Message:

Added new invariant to good_if
Generalized version of cond case for the correctness proof of each translate step

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2855 r2863  
    184184include "joint/semantics_blocks.ma".
    185185include "ASM/Util.ma".
    186 include "joint/StatusSimulationHelper.ma".
    187186
    188187lemma eval_cond_ok :
     
    210209bool_to_Prop (taaf_non_empty … taf).
    211210#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
    212 #ltrue #lfalse #Rst1st2 #EQfetch #EQeval
    213 @(general_eval_cond_ok … good … Rst1st2 … EQfetch EQeval)
    214 whd #lbl whd #mid1 normalize nodelta
    215 letin LTL_prog_params ≝ (mk_prog_params LTL_semantics ??)
    216 
    217 
    218  whd in match eval_state; normalize nodelta
     211#ltrue #lfalse #Rst1st2 #EQfetch
     212whd in match eval_state; normalize nodelta
    219213>EQfetch >m_return_bind
    220214whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
  • src/joint/Joint.ma

    r2843 r2863  
    520520
    521521include alias "basics/logic.ma".
    522 
     522check stmt_at
    523523record good_if
    524524(p : params) (globals : list ident) (def : joint_internal_function p globals)
     
    539539; regs_are_in_univers :
    540540  regs_in_universe … (joint_if_code … def) (joint_if_runiverse … def)
     541; entry_is_cost :
     542  ∃nxt,c.
     543  stmt_at p globals (joint_if_code … def) (joint_if_entry … def) =
     544  Some ? (sequential p ? (COST_LABEL ?? c) nxt)
    541545}.
    542546 
  • src/joint/StatusSimulationHelper.ma

    r2855 r2863  
    4646qed.
    4747
     48check joint_classify
     49check as_label
     50
     51record good_state_relation (P_in : sem_graph_params)
     52   (P_out : sem_graph_params) (prog : joint_program P_in)
     53   (stack_sizes : ident → option ℕ)
     54   (init : ∀globals.joint_closed_internal_function P_in globals
     55         →bound_b_graph_translate_data P_in P_out globals)
     56   (R : joint_abstract_status (mk_prog_params P_in prog stack_sizes) →
     57        joint_abstract_status (mk_prog_params P_out
     58                                (b_graph_transform_program P_in P_out init prog)
     59                                stack_sizes)
     60        → Prop) : Prop ≝
     61{ pc_eq_sigma_commute : ∀st1,st2.R st1 st2 → 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
     68; cond_commutation :
     69    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     70    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     71    ∀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' →
     75    let cond ≝ (COND P_in ? a ltrue) in
     76    fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
     77    return 〈f, fn,  sequential … cond lfalse〉 →
     78    R st1 st2 →
     79    ∀t_fn.
     80    fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
     81    return 〈f,t_fn〉 →
     82    bind_new_P' ??
     83     (λregs1.λdata.bind_new_P' ??
     84     (λregs2.λblp.
     85        ∀mid,nxt1.
     86          stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
     87          = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1→
     88         ∃st2_pre_mid_no_pc.
     89            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid)
     90                                   (st_no_pc ? st2)
     91            = 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
     94            joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
     95                                ((\snd (\fst blp)) mid)  = cl_jump ∧
     96            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) = [ ] ∧
     99            ∃st2_mid .
     100                eval_state P_out (prog_var_names … trans_prog)
     101                (ev_genv (mk_prog_params P_out trans_prog stack_sizes)) st2_pre_mid =
     102                return st2_mid ∧ R st1' st2_mid
     103   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
     104  ) (init ? fn)
     105}.
     106
    48107
    49108lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     
    51110∀stack_sizes.
    52111∀ f_lbls,f_regs.∀f_bl_r.∀init.
    53 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 
     112∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
    54113let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
    55114let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
    56115let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     116∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
     117good_state_relation P_in P_out prog stack_sizes init R →
    57118∀st1,st1' : joint_abstract_status prog_pars_in.
    58119∀st2 : joint_abstract_status prog_pars_out.
    59 ∀f,fn,a,ltrue,lfalse.
    60 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
     120∀f.
     121∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
     122∀a,ltrue,lfalse.
    61123R st1 st2 →
    62 let step ≝ (COND P_in ? a ltrue) in
    63 bind_new_P' ??
    64  (λregs1.λdata.∀lbl.bind_new_P' ??
    65   (λregs2.λblp.
    66    (∀mid1.∃st2'.
    67      repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? (\fst (\fst blp)) mid1) (st_no_pc … st2)
    68      = return (st_no_pc … st2') ∧
    69      pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
    70      last_pop … st2' = last_pop … st2)
    71    ) (f_step ??? data lbl step)   
    72   ) (init ? fn) →
     124    let cond ≝ (COND P_in ? a ltrue) in
    73125 fetch_statement P_in …
    74   (globalenv_noinit ? prog) (pc … st1) =
    75     return 〈f, fn,  sequential … step lfalse〉 →
     126  (globalenv_noinit ? prog) (pc … st1) = 
     127    return 〈f, fn,  sequential … cond lfalse〉 →
    76128 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
    77129            st1 = return st1' →
     
    80132∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
    81133bool_to_Prop (taaf_non_empty … taf).
    82 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st1 #st1' #st2
    83 #f #fn #a #ltrue #lfalse #R #Rst1st2 #Hb_graph #EQfetch whd in match eval_state; normalize nodelta
    84 >EQfetch >m_return_bind
    85 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
    86 whd in match eval_statement_advance; normalize nodelta
    87 #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
    88 #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
    89 lapply(fetch_statement_inv … EQfetch) * #EQfn #_
    90 [ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
    91 | whd in match next; normalize nodelta
    92 ]
    93 whd in ⊢ (??%% → ?); #EQ destruct(EQ) #n_cost
     134#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' #st2
     135#f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed
    94136cases(b_graph_transform_program_fetch_statement … good … EQfetch)
    95 #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); #Hinit (*cases (f_bl_r ?) normalize nodelta
    96 [2,4: #r #tl] whd in ⊢ (%→?); #EQ >EQ -init_data
    97 >if_merge_right in ⊢ (% → ?); [2,4: %] *)
     137#init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2)
     138#EQt_fn1 whd in ⊢ (% → ?); #Hinit
    98139* #labs * #regs
    99 (*[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *]*)
    100140** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls *
    101 whd in ⊢ (% → ?); #EQbl
    102 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
    103 #seq_pre_l
    104 letin trans_prog  ≝ (b_graph_transform_program P_in P_out init prog)
    105 letin prog_pars_out ≝ (mk_prog_params P_out trans_prog stack_sizes)
    106 cases(? : ∃st2'.
    107            repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? blp mid1) (st_no_pc … st2)
    108            = return (st_no_pc … st2') ∧
    109            pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
    110            last_pop … st2' = last_pop … st2)
    111    [2,4: assumption ]
    112 #st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
    113 >(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
    114 >(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
    115 whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
    116 >EQ in EQmid ⊢ %; -nxt1 #EQmid
     141whd in ⊢ (% → ?); @if_elim
     142[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
     143  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;
     145  normalize nodelta whd in match (point_of_offset ??); <ABS
     146  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
     147]
     148#_ <(pc_eq_sigma_commute … goodR … Rst1st2) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1
     149* #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
     150* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
     151cases(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
    117159lapply(taaf_to_taa ???
    118            (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
    119                                        seq_pre_l res_st2_pre_mid) ?)
    120 [1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
    121       whd in match (as_label ??); whd in match (as_pc_of ??);
    122       whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
    123       >m_return_bind whd in match point_of_pc; normalize nodelta
    124       >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
    125       cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
    126 #taa_pre_mid whd in ⊢ (% → ?);
    127 cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
    128                      return st2_cond )
    129 [2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
    130 #st2_mid #EQst2_mid
    131 cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
    132 [1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
    133 * #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
    134 letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
    135 cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
    136 %{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
    137 [1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
    138      cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
    139 |*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
     160           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
     161                                       seq_pre_l EQst_pre_mid_no_pc) ?)
     162[ @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
     163  whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
     164  whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
     165  >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
     166  #H @H %
     167] #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
     168[ whd <(as_label_ok … goodR … Hst2_mid) [assumption] cases daemon (*TODO: general lemma!*)
     169| whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
     170  >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
     171  assumption
     172| assumption
    140173]
    141 qed.*)
     174qed.
     175
Note: See TracChangeset for help on using the changeset viewer.