Changeset 2939


Ignore:
Timestamp:
Mar 22, 2013, 10:11:53 AM (4 years ago)
Author:
sacerdot
Message:

Major problem: in order to accomodate the ERTLptrToLTL proof pass, the
relation between states must be parameterized over the current label.

This makes the previous proof fail:

if s1 == s2 then it is not automatically true that s1' == s2'

because the relation at s1' is no longer constrained to have any
relationship with the one at s1. More conditions are required, but
which ones?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/StatusSimulationHelper.ma

    r2898 r2939  
    4747
    4848definition joint_state_relation ≝
    49 λP_in,P_out.(Σb:block.block_region b=Code) → state P_in → state P_out → Prop.
     49λP_in,P_out.(Σb:block.block_region b=Code) → label → state P_in → state P_out → Prop.
    5050
    5151definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
     
    9898    fetch_internal_function ? (globalenv_noinit … prog)
    9999     (pc_block (pc … st1))  = return 〈f,fn〉 →
    100      st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1) (st_no_pc … st2)
     100     st_no_pc_rel (pc_block(pc … st1))
     101     (point_of_pc P_in (pc … st1))
     102     (st_no_pc … st1) (st_no_pc … st2)
    101103; fetch_ok_pc_ok :
    102104  ∀st1,st2,f,fn.st_rel st1 st2 →
     
    112114  ∀st1,st2,pc,lp1,lp2,f,fn.
    113115  fetch_internal_function ? (globalenv_noinit … prog)
    114    (pc_block pc) = return 〈f,fn〉 → st_no_pc_rel (pc_block pc) st1 st2 →
     116   (pc_block pc) = return 〈f,fn〉 →
     117   st_no_pc_rel (pc_block pc) (point_of_pc P_in pc) st1 st2 →
    115118   lp1 = sigma_stored_pc P_in P_out prog f_lbls lp2 →
    116119  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
     120; as_label_ok :
     121  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    118122  ∀st1,st2,f,fn,stmt.
    119123   fetch_statement ? (prog_var_names … prog)
     
    146150                                   (st_no_pc ? st2)
    147151            = return st2_pre_mid_no_pc ∧
    148             st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
     152            st_no_pc_rel (pc_block(pc … st1))
     153             (point_of_pc P_in … (pc … st1)) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
    149154            joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
    150155                                ((\snd (\fst blp)) mid)  = cl_jump ∧
     
    182187           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
    183188              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
    184            st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1') st2_fin_no_pc
     189           st_no_pc_rel (pc_block (pc … st1))
     190            (point_of_pc P_in … (pc … st1))
     191            (st_no_pc … st1') st2_fin_no_pc
    185192      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
    186193     ) (init ? fn)
     
    199206fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
    200207 return 〈f,fn,stmt〉 →
    201 st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1) (st_no_pc … st2).
     208st_no_pc_rel (pc_block (pc … st1)) (point_of_pc P_in … (pc … st1)) (st_no_pc … st1) (st_no_pc … st2).
    202209#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
    203210#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
     
    264271qed.
    265272*)
    266  
     273
     274(*CSC: Isn't this already proved somewhere else??? *)
     275lemma point_of_pc_pc_of_point:
     276 ∀P_in: sem_graph_params.∀l,st.
     277   point_of_pc P_in
     278    (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in))
     279     (pc_block (pc P_in st)) l) = l.
     280 #P * //
     281qed.
    267282
    268283lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     
    334349[1,3: @(st_rel_def … goodR … f fn ?)
    335350      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
    336       |2,5: assumption
     351      |2,5: >point_of_pc_pc_of_point assumption
    337352      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
    338353      ]
Note: See TracChangeset for help on using the changeset viewer.