 Timestamp:
 Mar 16, 2013, 10:42:43 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/StatusSimulationHelper.ma
r2886 r2891 45 45 ] 46 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 → ? with54 [ 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_prf60 [ 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 66 check ensure_step_block67 47 68 48 record good_state_relation (P_in : sem_graph_params) … … 141 121 ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes) 142 122 (globals (mk_prog_params P_out trans_prog stack_sizes))). 143 blp = (ensure_step_block ?? l) ∧ True 144 (* 145 TUTTO IL RESTO PARLA DI R 146 147 ∀mid,mid1. 148 stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid 149 = return sequential P_out ? ((\snd (\fst blp)) mid) mid1→ 150 ∃CL_OTHER : joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) 151 ((\snd (\fst blp)) mid) = cl_other. 152 ∃COST : cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes) 153 (sequential P_out ? ((\snd (\fst blp)) mid) mid1) = None ?. 154 ∃st2_fin_no_pc. 155 let pre ≝ (map_eval ?? (\fst (\fst blp)) mid) in 156 let middle ≝ [pi1 ?? (step_to_seq (mk_prog_params P_out trans_prog stack_sizes) 157 ((\snd (\fst blp)) mid) CL_OTHER ?)] in 123 blp = (ensure_step_block ?? l) ∧ 124 ∃st2_fin_no_pc. 158 125 repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f 159 (pre@ middle @ (\snd blp))(st_no_pc … st2)= return st2_fin_no_pc ∧126 l (st_no_pc … st2)= return st2_fin_no_pc ∧ 160 127 let st2_fin ≝ 161 128 mk_state_pc ? st2_fin_no_pc 162 129 (pc_of_point P_out (pc_block(pc … st2)) nxt) 163 130 (last_pop … st2) in 164 R st1' st2_fin *)) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)131 R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq) 165 132 ) (init ? fn) 166 133 }. 167 (*@hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ)168 qed.*)169 134 170 135 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. … … 270 235 if taaf_non_empty … taf then True else (*IT CAN BE SIMPLIFIED *) 271 236 (¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨ 272 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1'). 273 cases daemon qed. 274 275 (* 237 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1'). 276 238 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' 277 239 #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval 278 240 cases(b_graph_transform_program_fetch_statement … good … EQfetch) 279 241 #init_data * #t_fn ** >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) 280 #EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta *** 281 #blp #blm #bls * @if_elim 242 #EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim 282 243 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta 283 244 whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) … … 287 248 ] 288 249 #_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl 289 >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC lapply SBiC 290 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); 291 #_ whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 292 #_ 250 >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC 293 251 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit 294 252 (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn))) 295 [4: @EQmid *:] #COST * #CL_OTHER * #st2_fin_no_pc normalize nodelta cases(step_to_seq ????) 296 #seq_mid cases daemon (*TODO*) 297 qed. 298 299 cases(blm mid1) in 300 #stmt_at_middle #EQstmt_at_middle normalize nodelta * >EQstmt_at_middle in SBiC; destruct(EQ) whd in ⊢ (??%% → ?);#EQ destruct(EQ) 301 302 303 * #EQst2_pre_mid_no_pc 304 * #st2_mid * #EQst2_mid * #st2_fin_no_pc * #EQst2_fin_no_pc #Hfin 253 #l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem 305 254 %{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))} 306 %{Hfin} 307 lapply(taaf_to_taa ??? 308 (produce_trace_any_any_free ? st2 f t_fn ??? st2_pre_mid_no_pc EQt_fn 309 seq_pre_l EQst2_pre_mid_no_pc) ?) 310 [ @if_elim #_ [2: @I] % whd in match as_costed; normalize nodelta 311 whd in match (as_label ??); whd in match fetch_statement; normalize nodelta 312 >EQt_fn >m_return_bind whd in match (as_pc_of ??); whd in match point_of_pc; 313 normalize nodelta >point_of_offset_of_point >EQmid >m_return_bind 314 normalize nodelta >COST * #H @H %] 315 #taa1 316 letin st2_mid_pc ≝ (mk_state_pc ? st2_mid 317 (pc_of_point P_out (pc_block (pc … st2)) mid2) 318 (last_pop … st2)) 319 <(point_of_pc_of_point P_out (pc_block (pc … st2)) mid2) in seq_post_l; 320 #seq_post_l 321 lapply (produce_trace_any_any_free (mk_prog_params P_out ? stack_sizes) 322 st2_mid_pc f t_fn ??? st2_fin_no_pc EQt_fn 323 (seq_post_l) EQst2_fin_no_pc) 324 * #taaf2 * #taaf2_prf1 #taaf2_prf2 325 %{(taaf_append_taaf ???? (taaf_step ???? taa1 ??) taaf2 ?)} 326 [ @hide_prf @if_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H #_ 327 % whd in match (as_costed ??); whd in match (as_label ??); 328 whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta 329 >EQt_fn >m_return_bind whd in match point_of_pc; normalize nodelta 330 >point_of_offset_of_point lapply(taaf2_prf2 H) lapply seq_post_l cases bls 331 [ #_ *] #stmt1 #tl * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQstmt1 332 >point_of_pc_of_point change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #_ #_ 333 >point_of_pc_of_point in EQstmt1; #EQstmt1 >EQstmt1 >m_return_bind normalize nodelta 334 * #H @H % 335  @hide_prf whd whd in match eval_state; normalize nodelta whd in match fetch_statement; 336 normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid 337 >m_return_bind >EQst2_mid >m_return_bind whd in match eval_statement_advance; 338 normalize nodelta lapply COST lapply CL_OTHER lapply EQmid cases(blm mid1) 339 normalize nodelta 340 [ #c #_ #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ) 341  #id #args #dest #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ) 342  #r #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ) 343  #jseq #EQjseq #_ #_ % 344 ] 345  @hide_prf whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn 346 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind assumption 347  @if_elim #_ [%] % % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); >EQfetch % 348 ] 349 qed. 350 *) 255 %{Rsem} 256 %{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn 257 SBiC EQst2_fin_no_pc)} 258 @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); >EQfetch % 259 qed.
Note: See TracChangeset
for help on using the changeset viewer.