 Timestamp:
 Mar 15, 2013, 6:33:18 PM (7 years ago)
 Location:
 src/joint
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/StatusSimulationHelper.ma
r2863 r2883 44 44 @Hr 45 45 ] 46 qed. 47 48 check joint_classify 49 check as_label 46 qed. 47 48 49 definition step_to_seq : ∀p : prog_params.∀stmt : joint_step p (globals p). 50 joint_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 ] 64 qed. 65 50 66 51 67 record good_state_relation (P_in : sem_graph_params) … … 59 75 stack_sizes) 60 76 → 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 62 81 ; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes). 63 82 ∀st2 : joint_abstract_status ?. … … 70 89 ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 71 90 ∀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. 75 92 let cond ≝ (COND P_in ? a ltrue) in 76 93 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' → 78 97 R st1 st2 → 79 98 ∀t_fn. … … 82 101 bind_new_P' ?? 83 102 (λregs1.λdata.bind_new_P' ?? 84 (λregs2.λblp. 85 ∀mid ,nxt1.103 (λregs2.λblp.(\snd blp) = [ ] ∧ 104 ∀mid. 86 105 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→ 88 107 ∃st2_pre_mid_no_pc. 89 108 repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid) … … 95 114 ((\snd (\fst blp)) mid) = cl_jump ∧ 96 115 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 ? ∧ 99 117 ∃st2_mid . 100 118 eval_state P_out (prog_var_names … trans_prog) … … 103 121 ) (f_step … data (point_of_pc P_in (pc … st1)) cond) 104 122 ) (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) 105 159 }. 106 160 @hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ) 161 qed. 107 162 108 163 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. … … 135 190 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed 136 191 cases(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) 138 193 #EQt_fn1 whd in ⊢ (% → ?); #Hinit 139 194 * #labs * #regs … … 142 197 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta 143 198 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; 145 200 normalize nodelta whd in match (point_of_offset ??); <ABS 146 201 cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1) 147 202 ] 148 #_ <(pc_eq_sigma_commute … goodR … Rst1st2 ) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1203 #_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1 149 204 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1 150 205 * #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 206 cases(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) 209 cases(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 159 213 lapply(taaf_to_taa ??? 160 214 (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1 … … 174 228 qed. 175 229 230 (* 231 let rec taa_to_taaf S st1 st2 (taa : trace_any_any S st1 st2) on taa : 232 trace_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 239 lemma 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. 244 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 245 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 246 let 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. 248 good_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. 254 R 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 268 cases(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 280 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); 281 #_ whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 282 #_ 283 cases(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} 298 lapply(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 307 letin 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 312 lapply (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 ] 340 qed. 341 *) 
src/joint/semantics_blocks.ma
r2879 r2883 146 146 seq_list_in_code … (joint_if_code … curr_fn) src b l dst → 147 147 repeat_eval_seq_no_pc p curr_id b st = return st' → 148 trace_any_any_free (joint_abstract_status p) st 149 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝ 148 Σtaaf :trace_any_any_free (joint_abstract_status p) st 149 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)). 150 (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝ 150 151 λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3. 151 152 produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3. … … 175 176 #H #G 176 177 %2{(taa_base …)} assumption 177  #hd #tl #_ #EQ <EQ hd tl @produce_trace_any_any_freeassumption178  #hd #tl #_ #EQ <EQ hd tl #H1 #H2 @(produce_trace_any_any_free …) assumption 178 179 ] 179 180 qed.
Note: See TracChangeset
for help on using the changeset viewer.