Changeset 2990 for src/common


Ignore:
Timestamp:
Mar 27, 2013, 7:49:32 PM (7 years ago)
Author:
campbell
Message:

Replace dodgy hypothesis by nice ones, clean up a little.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/common/FEMeasurable.ma

    r2989 r2990  
    3333  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;
    3434  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;
    3740  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';
    3841
    … …  
    140143
    141144
    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 #EXEC
    148 cases (exec_steps_S … EXEC)
    149 #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
    150 #N
    151 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 #EXEC
    162 cases (exec_steps_S … EXEC)
    163 #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
    164 #N
    165 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 -m
    183 [ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct
    184   #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS
    185 | #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H *
    186   [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ % | @AFTER ] | @EXEC1 ]| % ]
    187   | #n #P #AFTER
    188     cases (exec_steps_S … EXEC1)
    189     #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2
    190     cases (after_1_of_n_steps … AFTER)
    191     #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2
    192     >STEP in STEP'; #E destruct
    193     cases (IH … EXEC2 … AFTER2)
    194     [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E
    195       %{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 assumption
    199     | assumption
    200     | assumption
    201     ]
    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 #AFTER1
    213 cases (exec_steps_S … EXEC1)
    214 #NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2
    215 %{[〈s1,tr〉]} %{s2} %{tl} % [ %
    216  [ whd in ⊢ (??%?); >NF1 >STEP % | whd in AFTER1; >NF1 in AFTER1; >STEP normalize
    217  cases (inv s2) // * ]| // ]
    218 qed.
    219 *)
    220 (* XXX do I need to do the max_stack reasoning here?  perhaps just by preserving
    221    observables? *)
    222145
    223146lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'.
    … …  
    269192      ms_rel MS g g' INV sr sr'.
    270193
    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_init
     194* #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
    272195#g #g' #INV #s1 #s1' #REL
    273196#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
    … …  
    356279               @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    357280               [ 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) %
    359282               | @INV1
    360283               | %
    … …  
    404327               @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    405328               [ 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) %
    407330               | %
    408331               | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    … …  
    439362             @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    440363             [ 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) %
    442365             | @INV
    443366             | assumption
    … …  
    463386           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    464387           [ 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)
    466389           | @INV
    467390           | assumption
    … …  
    524447       measurable trace, so the end is no longer in the relation. ☹ *)
    525448   
    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_init
     449* #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
    527450#g #g' #INV #s1 #s1' #depth #callstack #REL
    528451#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
    … …  
    560483    |  @ends_at_return_append assumption
    561484    ]| 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       ]
    564489    ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
    565490       cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
    … …  
    629554        % [ % [ %
    630555        [  whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); %
    631         |  %{[ ]} %{E0} %{s1'} %{(refl ??)} <(rel_classify … REL) assumption
     556        |  %{[ ]} %{E0} %{s1'} %{(refl ??)} @(rel_classify_return … REL) assumption
    632557        ]| whd in RETURNS:(?%) ⊢ (?%);
    633558           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)
    635560           >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%);
    636561           cases depth [ // | #d * ]
    … …  
    639564           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    640565           [ @CL
    641            | whd in ⊢ (??%?); <(rel_classify … REL) @CL
     566           | whd in ⊢ (??%?); @(rel_classify_return … REL CL)
    642567           | %
    643568           | %
    … …  
    695620         ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2''
    696621            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
    697             <(rel_classify … REL) >CL whd in ⊢ (?%); whd in INV1:(?(???%));
     622            >(rel_classify_call … REL CL) whd in ⊢ (?%); whd in INV1:(?(???%));
    698623            >will_return_aux_normal [2: @INV1 ]
    699624            >will_return_aux_normal
    … …  
    710635            @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    711636            [ 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) %
    713638            | @INV1
    714639            | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    … …  
    753678         ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
    754679            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
    755             <(rel_classify … REL) >CL whd in ⊢ (?%);
     680            >(rel_classify_call … REL CL) whd in ⊢ (?%);
    756681            >will_return_aux_normal //
    757682         ]| destruct cases (exec_steps_S … EXEC1')
    … …  
    760685            @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    761686            [ 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) %
    763688            | @INV
    764689            | assumption
    … …  
    795720     ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
    796721        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 ⊢ (?% → ?%);
    798723        whd in match next_depth in RETURNS'';
    799724        cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_
    … …  
    805730        @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    806731        [ 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)
    808733        | @INV
    809734        | assumption
Note: See TracChangeset for help on using the changeset viewer.