Changeset 2990
 Timestamp:
 Mar 27, 2013, 7:49:32 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r2989 r2990 33 33 ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pnormal_state ms_C1 g1 s1 = pnormal_state ms_C2 g2 s2; 34 34 ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_labelled ms_C1 g1 s1 = pcs_labelled ms_C2 g2 s2; 35 (* FIXME: this is almost certainly too strong if the step from s1 "disappears" in s2. *) 36 ms_rel_classify : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = pcs_classify ms_C2 g2 s2; 35 (* It's tempting to have a general result that states in the relation always 36 have the same classification, but this may not be true when the step for 37 s1 "disappears" in s2. *) 38 ms_rel_classify_call : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = cl_call → pcs_classify ms_C2 g2 s2 = cl_call; 39 ms_rel_classify_return : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = cl_return → pcs_classify ms_C2 g2 s2 = cl_return; 37 40 ms_rel_callee : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → ∀H,H'. pcs_callee ms_C1 g1 s1 H = pcs_callee ms_C2 g2 s2 H'; 38 41 … … 140 143 141 144 142 (*143 lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.144 exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →145 pnormal_state C g s1 →146 stack_after (pcs_to_cs C g stack) current trace = current.147 #C #g #s1 #trace #s2 #stack #current #EXEC148 cases (exec_steps_S … EXEC)149 #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct150 #N151 whd in ⊢ (??%?); generalize in match (cs_stack ??);152 whd in match (cs_classify ??);153 cases (pnormal_state_inv … N)154 #CL >CL #f %155 qed.156 157 lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.158 exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →159 pnormal_state C g s1 →160 max_stack (pcs_to_cs C g stack) current trace = current.161 #C #g #s1 #trace #s2 #stack #current #EXEC162 cases (exec_steps_S … EXEC)163 #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct164 #N165 whd in ⊢ (??%?); generalize in match (cs_stack ??);166 whd in match (cs_classify ??);167 cases (pnormal_state_inv … N)168 #CL >CL #f %169 qed.170 171 lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf.172 exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →173 ¬pcs_labelled C g s1 →174 pcs_labelled C g sf →175 ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) →176 ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P →177 ∃p,trace1,s2,trace2.178 exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧179 P (gather_trace … trace1) s2 ∧180 exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧181 m = n + p.182 #C #g #m elim m m183 [ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct184 #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS185  #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H *186 [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ %  @AFTER ]  @EXEC1 ] % ]187  #n #P #AFTER188 cases (exec_steps_S … EXEC1)189 #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2190 cases (after_1_of_n_steps … AFTER)191 #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2192 >STEP in STEP'; #E destruct193 cases (IH … EXEC2 … AFTER2)194 [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E195 %{p} % [2: %{s2} %{trace2} % [ % [ %196 [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); %  skip ]197  @P2 ] @EXEC2 ] >E % ]  skip ]198  @H assumption199  assumption200  assumption201 ]202 ]203 ] qed.204 205 lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf.206 exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →207 ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P →208 ∃trace1,s2,trace2.209 exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧210 P (gather_trace … trace1) s2 ∧211 exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉.212 #C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1213 cases (exec_steps_S … EXEC1)214 #NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2215 %{[〈s1,tr〉]} %{s2} %{tl} % [ %216 [ whd in ⊢ (??%?); >NF1 >STEP %  whd in AFTER1; >NF1 in AFTER1; >STEP normalize217 cases (inv s2) // * ] // ]218 qed.219 *)220 (* XXX do I need to do the max_stack reasoning here? perhaps just by preserving221 observables? *)222 145 223 146 lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'. … … 269 192 ms_rel MS g g' INV sr sr'. 270 193 271 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init194 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init 272 195 #g #g' #INV #s1 #s1' #REL 273 196 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' … … 356 279 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 357 280 [ whd in match (cs_classify ??); >CL % 358  whd in match (cs_classify ??); <(rel_classify … REL) >CL%281  whd in match (cs_classify ??); >(rel_classify_call … REL CL) % 359 282  @INV1 360 283  % … … 404 327 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 405 328 [ whd in match (cs_classify ??); >CL % 406  whd in match (cs_classify ??); <(rel_classify … REL) >CL%329  whd in match (cs_classify ??); >(rel_classify_call … REL CL) % 407 330  % 408 331  @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) … … 439 362 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 440 363 [ whd in match (cs_classify ??); >CL % 441  whd in match (cs_classify ??); <(rel_classify … REL) >CL%364  whd in match (cs_classify ??); >(rel_classify_call … REL CL) % 442 365  @INV 443 366  assumption … … 463 386 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 464 387 [ whd in match (cs_classify ??); >CL % 465  whd in match (cs_classify ??); <(rel_classify … REL) >CL %388  whd in match (cs_classify ??); @(rel_classify_return … REL CL) 466 389  @INV 467 390  assumption … … 524 447 measurable trace, so the end is no longer in the relation. ☹ *) 525 448 526 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init449 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init 527 450 #g #g' #INV #s1 #s1' #depth #callstack #REL 528 451 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' … … 560 483  @ends_at_return_append assumption 561 484 ] cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct 562 whd in ⊢ (?%); whd in match (cs_classify ??); <(rel_classify … REL) 563 cases (pnormal_state_inv … N1) #CL >CL @RETURNS'' 485 >will_return_aux_normal 486 [ @RETURNS'' 487  whd in ⊢ (?%); <normal_state_p >N1' % 488 ] 564 489 ] destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // 565 490 cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct … … 629 554 % [ % [ % 630 555 [ whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); % 631  %{[ ]} %{E0} %{s1'} %{(refl ??)} <(rel_classify… REL) assumption556  %{[ ]} %{E0} %{s1'} %{(refl ??)} @(rel_classify_return … REL) assumption 632 557 ] whd in RETURNS:(?%) ⊢ (?%); 633 558 whd in match (cs_classify ??) in RETURNS; 634 whd in match (cs_classify ??); <(rel_classify … REL)559 whd in match (cs_classify ??); >(rel_classify_return … REL CL) 635 560 >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%); 636 561 cases depth [ //  #d * ] … … 639 564 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 640 565 [ @CL 641  whd in ⊢ (??%?); <(rel_classify … REL) @CL566  whd in ⊢ (??%?); @(rel_classify_return … REL CL) 642 567  % 643 568  % … … 695 620 ] cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'' 696 621 destruct whd in ⊢ (?%); whd in match (cs_classify ??); 697 <(rel_classify … REL) >CLwhd in ⊢ (?%); whd in INV1:(?(???%));622 >(rel_classify_call … REL CL) whd in ⊢ (?%); whd in INV1:(?(???%)); 698 623 >will_return_aux_normal [2: @INV1 ] 699 624 >will_return_aux_normal … … 710 635 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 711 636 [ whd in match (cs_classify ??); >CL % 712  whd in match (cs_classify ??); <(rel_classify … REL) >CL%637  whd in match (cs_classify ??); >(rel_classify_call … REL CL) % 713 638  @INV1 714 639  @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) … … 753 678 ] cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' 754 679 destruct whd in ⊢ (?%); whd in match (cs_classify ??); 755 <(rel_classify … REL) >CLwhd in ⊢ (?%);680 >(rel_classify_call … REL CL) whd in ⊢ (?%); 756 681 >will_return_aux_normal // 757 682 ] destruct cases (exec_steps_S … EXEC1') … … 760 685 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 761 686 [ whd in match (cs_classify ??); >CL % 762  whd in match (cs_classify ??); <(rel_classify … REL) >CL%687  whd in match (cs_classify ??); >(rel_classify_call … REL CL) % 763 688  @INV 764 689  assumption … … 795 720 ] cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' 796 721 destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %; 797 <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%);722 >(rel_classify_return … REL CL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%); 798 723 whd in match next_depth in RETURNS''; 799 724 cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_ … … 805 730 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 806 731 [ whd in match (cs_classify ??); >CL % 807  whd in match (cs_classify ??); <(rel_classify … REL) >CL %732  whd in match (cs_classify ??); @(rel_classify_return … REL CL) 808 733  @INV 809 734  assumption
Note: See TracChangeset
for help on using the changeset viewer.