Changeset 2939
- Timestamp:
- Mar 22, 2013, 10:11:53 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/StatusSimulationHelper.ma
r2898 r2939 47 47 48 48 definition 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. 50 50 51 51 definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop. … … 98 98 fetch_internal_function ? (globalenv_noinit … prog) 99 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) 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) 101 103 ; fetch_ok_pc_ok : 102 104 ∀st1,st2,f,fn.st_rel st1 st2 → … … 112 114 ∀st1,st2,pc,lp1,lp2,f,fn. 113 115 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 → 115 118 lp1 = sigma_stored_pc P_in P_out prog f_lbls lp2 → 116 119 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 118 122 ∀st1,st2,f,fn,stmt. 119 123 fetch_statement ? (prog_var_names … prog) … … 146 150 (st_no_pc ? st2) 147 151 = 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) ∧ 149 154 joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) 150 155 ((\snd (\fst blp)) mid) = cl_jump ∧ … … 182 187 repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f 183 188 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 185 192 ) (f_step … data (point_of_pc P_in (pc … st1)) seq) 186 193 ) (init ? fn) … … 199 206 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 200 207 return 〈f,fn,stmt〉 → 201 st_no_pc_rel (pc_block (pc … st1)) ( st_no_pc … st1) (st_no_pc … st2).208 st_no_pc_rel (pc_block (pc … st1)) (point_of_pc P_in … (pc … st1)) (st_no_pc … st1) (st_no_pc … st2). 202 209 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel 203 210 #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch … … 264 271 qed. 265 272 *) 266 273 274 (*CSC: Isn't this already proved somewhere else??? *) 275 lemma 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 * // 281 qed. 267 282 268 283 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. … … 334 349 [1,3: @(st_rel_def … goodR … f fn ?) 335 350 [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption 336 |2,5: assumption351 |2,5: >point_of_pc_pc_of_point assumption 337 352 |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption 338 353 ]
Note: See TracChangeset
for help on using the changeset viewer.