Changeset 2477
 Timestamp:
 Nov 20, 2012, 1:41:58 PM (7 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/StatusSimulation.ma
r2463 r2477 75 75 λS2 : abstract_status. 76 76 λsim_status_rel : status_rel S1 S2. 77 ∀st1, cl,st1',st2.as_execute S1 st1 st1' →77 ∀st1,st1',st2.as_execute S1 st1 st1' → 78 78 sim_status_rel st1 st2 → 79 ∀prf : as_classifier S1 st1 cl. 80 match cl return λc.as_classifier S1 st1 c → ? with 81 [ cl_call ⇒ λprf. 79 match as_classify … st1 with 80 [ cl_call ⇒ ∀prf. 82 81 (* 83 82 st1' S\ … … 98 97 sim_status_rel st1' st2' ∧ 99 98 label_rel … st1' st2_after_call 100  cl_return ⇒ λ_.99  cl_return ⇒ 101 100 (* 102 101 st1 … … 121 120 ret_rel … sim_status_rel st1' st2_after_ret ∧ 122 121 label_rel … st1' st2' 123  _ ⇒ λ_.124 (*125 122  cl_other ⇒ 123 (* 124 st1 → st1' 126 125  \ 127 126 S S,L … … 132 131 case when both st1 and st1' are labelled (we would be able to collapse 133 132 labels otherwise) 134 also notice that this allows to freely exchange cl_other and cl_jump, 135 but if cl_jump imposed labels before, they will be kept afterwards *) 133 *) 136 134 ∃st2'. 137 135 ∃taa2 : trace_any_any_free … st2 st2'. 138 (* we ensure no labels are collapsed. Technicality? *)139 136 (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ 140 137 sim_status_rel st1' st2' ∧ 141 138 label_rel … st1' st2' 142 ] prf. 139  cl_jump ⇒ 140 (* 141 st1 → st1' st1 → st1'\ 142  /  \ 143 S S,L or S S,L 144  /  \ 145 st2 st2 →collapsable tal→ st2' 146 *) 147 (¬as_costed … st1 (* st1' will necessarily be costed *) ∧ 148 sim_status_rel st1' st2 ∧ label_rel … st1' st2) ∨ 149 (∃st2'.∃tal : trace_any_label … doesnt_end_with_ret st2 st2'. 150 tal_collapsable … tal ∧ 151 sim_status_rel st1' st2' ∧ label_rel … st1' st2') 152 ]. 143 153 144 154 … … 257 267 ]. 258 268 * #S2 #st12 #st22 #H #I #J % %[%{(taa_base ??)} %[%[%[ % 269 qed. 270 271 let rec tal_collapsable_eq_flag S fl st1 st2 272 (tal : trace_any_label S fl st1 st2) on tal : 273 tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝ 274 match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ? 275 with 276 [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl 277  tal_base_not_return _ st2' _ _ K ⇒ λ_.refl … 278  _ ⇒ Ⓧ 279 ]. 280 281 let rec tal_collapsable_split S fl st1 st2 282 (tal : trace_any_label S fl st1 st2) on tal : 283 tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J. 284 tal ≃ taa @ tal_base_not_return … st2 H I J ≝ 285 match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J. 286 tal ≃ taa @ tal_base_not_return … st2_mid ? H I J 287 with 288 [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ? 289  tal_base_not_return st1' st2' H I J ⇒ ? 290  _ ⇒ Ⓧ 291 ]. 292 [ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} % 293  #coll 294 elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J' 295 #EQ %{st2_mid} %{(taa_step … taa)} try assumption 296 %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) tl #tl 297 #EQ >EQ % 298 ] 299 qed. 300 301 lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal. 302 tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J. 303 tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal. 304 #S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J 305 elim (tal_collapsable_split … coll) lapply tal 306 >(tal_collapsable_eq_flag … coll) tal #tal 307 #st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%] 308 %[%[%[%[%[ % ]]]]] 259 309 qed. 260 310 … … 431 481 ] 432 482  (* tal_base_non_return *) whd 433 cases G #G' 434 elim (sim_execute … H st1_R_st2 G') 435 #st2' ** st2 st2' 436 [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *) 437 ** whd in ⊢ (%→?); * 438 [1,3: #ncost #R' #L' %2 /4 by conj/ 439 *: * #ABS elim (ABS K) 483 cases G G #G 484 lapply (sim_execute … H st1_R_st2) 485 (* without try it fails... why? *) 486 try >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); * 487 [ (* jump to none *) 488 ** #K' #st1_R_st2' #st1_L_st2' %2 /4 by conj/ 489  (* jump to some *) 490 * #st2' * #tal2 ** #tal2_coll #st1_R_st2' #st1_L_st2' 491 %1 492 %{st2'} %{tal2} % [ /3 by conj/ ] 493 @tal_collapsable_to_rel_symm assumption 494  (* other *) 495 #st2' ** st2 st2' 496 [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *) 497 ** whd in ⊢ (%→?); * 498 [1,3: #ncost #R' #L' %2 /4 by conj/ 499 *: * #ABS elim (ABS K) 500 ] 501 *: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1 502 %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))} 503 [1,3: whd <st1_L_st2' assumption ] 504 % [1,3: /2 by conj/] 505 % try @refl %{st2_mid} %{taa2} %{H2} %[2,4: %[2,4: %]] 440 506 ] 441 *: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1442 %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))}443 [1,3: whd <st1_L_st2' assumption ]444 % [1,3: /2 by conj/]445 % try @refl %{st2_mid} %{taa2} %{H2} %[2,4: %[2,4: %]]446 507 ] 447 508  (* tal_base_return *) whd 448 elim (sim_execute … H st1_R_st2 G) 509 lapply (sim_execute … H st1_R_st2) 510 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); * 449 511 #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2' 450 512 ***** #ncost #J2 #K2 … … 454 516 %[ %  %[%[%[%[ % ]]]]]]] 455 517  (* tal_base_call *) whd 456 elim (sim_execute … H st1_R_st2 G) 518 lapply (sim_execute … H st1_R_st2) 519 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); 520 #H elim (H G) H 457 521 * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 458 522 #st1_R_st2_mid #st1_L_st2_after_call … … 479 543 ] 480 544  (* tal_step_call *) 481 elim (sim_execute … H st1_R_st2 G) 545 lapply (sim_execute … H st1_R_st2) 546 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); 547 #H elim (H G) H 482 548 * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 483 549 #st1_R_st2_mid #st1_L_st2_after_call … … 524 590 ] 525 591  (* step_default *) 526 elim (sim_execute … H st1_R_st2 G) 592 lapply (sim_execute … H st1_R_st2) 593 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); * 527 594 #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid 528 595 lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid) … … 740 807 *: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl 741 808 (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S 742 elim (sim_execute … ex G' cl) 743 [1,2: (* jump or other *) 809 [ (* jump *) 810 lapply (sim_execute … ex G') 811 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); * 812 [ ** #ncost #G'' #H'' 813 %{st2_mid} %{st2_mid} 814 %[@(ft_extend_taa … taa) 815 assumption] 816 %{(taa_base …)} % [ %{H'' G''} ] 817 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil 818 >ft_extend_taa_obs <L' 819 whd in match (as_label ? st1_mid); 820 >(not_costed_no_label … ncost) >if_eq >S % 821  * #st2' * #tal ** #coll 822 elim (tal_collapsable_split … coll) #st2_mid' * #taa2 823 * #K2 * #J2 *#H2 #EQ #G'' #H'' 824 %{st2'} %{st2'} 825 %[@(ft_advance_flat … K2 J2) 826 @(ft_extend_taa … (taa_append_taa … taa taa2)) 827 assumption] 828 %{(taa_base …)} % [ %{H'' G''} ] 829 >ft_extend_taa_advance_flat_obs 830 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil 831 <S <L' % 832 ] 833  (* other *) 834 lapply (sim_execute … ex G') 835 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); * 744 836 #st2' *#taaf ** #ncost #G'' #H'' 745 837 %{st2'} %{st2'} … … 771 863 ] 772 864 3: (* ret *) 865 lapply (sim_execute … ex G') 866 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); * 773 867 #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2' 774 868 ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'} … … 791 885 >S >L' % 792 886 4: (* call *) 887 lapply (sim_execute … ex G') 888 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); #H elim (H cl) H 793 889 * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2' 794 890 * #taa2 * #taa2' ** #ex' #G'' #H'' 
src/joint/Traces.ma
r2473 r2477 99 99 qed. 100 100 101 definition joint_classify_seq : 102 ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝ 103 λp,st,stmt. 104 match stmt with 105 [ CALL f args dest ⇒ 106 match function_of_call ?? (ev_genv p) st f with 107 [ OK fn ⇒ 108 match description_of_function … fn with 109 [ Internal _ ⇒ cl_call 110  External _ ⇒ cl_other 111 ] 112  Error _ ⇒ cl_other 113 ] 114  _ ⇒ cl_other 115 ]. 116 117 definition joint_classify_step : 118 ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝ 119 λp,st,stmt. 120 match stmt with 121 [ step_seq s ⇒ joint_classify_seq p st s 122  COND _ _ ⇒ cl_jump 123 ]. 124 125 definition joint_classify_final : 126 ∀p : evaluation_params.joint_fin_step p → status_class ≝ 127 λp,stmt. 128 match stmt with 129 [ GOTO _ ⇒ cl_other 130  RETURN ⇒ cl_return 131  TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *) 132 ]. 133 101 134 definition joint_classify : 102 135 ∀p : evaluation_params.state_pc p → status_class ≝ … … 104 137 match fetch_statement ? p … (ev_genv p) (pc … st) with 105 138 [ OK f_s ⇒ 106 let 〈f, s〉 ≝ f_s in 107 match s with 108 [ sequential s _ ⇒ 109 match s with 110 [ step_seq s ⇒ 111 match s with 112 [ CALL f' args dest ⇒ 113 match function_of_call ?? (ev_genv p) st f' with 114 [ OK fn ⇒ 115 match description_of_function … fn with 116 [ Internal _ ⇒ cl_call 117  External _ ⇒ cl_other 118 ] 119  Error _ ⇒ cl_other 120 ] 121  _ ⇒ cl_other 122 ] 123  COND _ _ ⇒ cl_jump 124 ] 125  final s ⇒ 126 match s with 127 [ GOTO _ ⇒ cl_other 128  RETURN ⇒ cl_return 129  TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *) 130 ] 139 match \snd f_s with 140 [ sequential s _ ⇒ joint_classify_step p st s 141  final s ⇒ joint_classify_final p s 131 142 ] 132 143  Error _ ⇒ cl_other … … 142 153 #p #st 143 154 whd in match joint_classify; normalize nodelta 144 lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st))) 145 elim (fetch_statement ?????) in ⊢ (???%→%); 155 inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta 146 156 [ * #f * [ * [ #lbl  #b #f #args ]] 147 157 [ * [ #a #lbl #next ] … … 150 160  #op #a #a'  #op #a #a' #arg  #a #dpl #dph  #dpl #dph #arg 151 161  #ext ] #next 152 [ normalize nodelta 153 lapply (refl … (function_of_call … (ev_genv p) st f')) 154 elim (function_of_call ?????) in ⊢ (???%→%); 155 [ #fn normalize nodelta 156 lapply (refl … (description_of_function … (ev_genv p) fn)) 157 elim (description_of_function ?? fn) in ⊢ (???%→%); #fd 162 [ whd in match joint_classify_step; whd in match joint_classify_seq; 163 normalize nodelta 164 inversion (function_of_call ?????) normalize nodelta 165 [ #fn 166 inversion (description_of_function ?? fn) #fd 158 167 #EQfd 159 168  #e … … 166 175 [*: #ABS normalize in ABS; destruct(ABS) ] 167 176 normalize nodelta #_ 168 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/ 177 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} 178 %{EQfd} %{EQfn} % 169 179 qed. 170 180
Note: See TracChangeset
for help on using the changeset viewer.