Changeset 2690 for src/common


Ignore:
Timestamp:
Feb 21, 2013, 7:24:11 PM (7 years ago)
Author:
campbell
Message:

Most of the measurable subtrace preservation proof done.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2685 r2690  
    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. *)
    3536  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;
    3637  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';
     
    6667    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
    6768    ¬ pcs_labelled ms_C1 g1 s1 →
     69    (* NB: calls and returns don't emit timing cost labels; otherwise we would
     70       have to worry about whether the cost labels seen at the final return of
     71       the measured trace might appear in the target in subsequent steps that
     72       are *after* the new measurable subtrace.  Also note that extra steps are
     73       introduced in the front-end: to perform variable saves on entry and to
     74       write back the result *after* exit.  The latter do not get included in
     75       the measurable subtrace because it stops at the return, and they are the
     76       caller's responsibility. *)
    6877    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
    69     ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
    70       tr = tr' ∧
     78    ∃m. tr = E0 ∧
     79      after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
     80      E0 = tr' ∧
    7181      ms_rel g1 g2 INV s2 s2'
    7282    );
     
    8393    );
    8494  sim_init :
    85     ∀p1,p2,s,s'.
     95    ∀p1,p2,s.
    8696    ms_compiled p1 p2 →
    8797    make_initial_state ?? ms_C1 p1 = OK ? s →
    88     make_initial_state ?? ms_C2 p2 = OK ? s' →
     98    ∃s'. make_initial_state ?? ms_C2 p2 = OK ? s' ∧
    8999    ∃INV. ms_rel ?? INV s s'
    90100}.
    91101
    92 (* TODO: obs eq *)
     102
    93103(*
    94104lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
     
    186196qed.
    187197
    188 (* WIP commented out*)
     198
    189199lemma prefix_preserved :
    190200  ∀MS:meas_sim.
     
    265275      cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
    266276      [2,4: >CL %]
    267       #m' #AFTER1'
     277      #m' * #Etr #AFTER1'
    268278      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
    269279      [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
     
    276286        | destruct cases (exec_steps_S … EXEC1')
    277287          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
    278           destruct
     288          destruct >Etrace
    279289          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    280290          [1,3: whd in match (cs_classify ??); >CL %
     
    286296        | destruct cases (exec_steps_S … EXEC1')
    287297          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
    288           destruct
     298          destruct >Etrace
    289299          @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    290300          [ whd in match (cs_classify ??); >CL %
     
    299309  ]
    300310] qed.
    301        
    302      
    303 
     311
     312definition ends_at_return : ∀C:preclassified_system. ∀g. list (state … C g × trace) → Prop ≝
     313λC,g,x. ∃x',tr2,s2. x = x'@[〈s2,tr2〉] ∧ pcs_classify C g s2 = cl_return.
     314
     315lemma ends_at_return_append : ∀C,g,t1,t2.
     316  ends_at_return C g t2 →
     317  ends_at_return C g (t1@t2).
     318#C #g #t1 #t2 * #x * #tr * #s * #E >E #CL
     319%{(t1@x)} %{tr} %{s} % /2/
     320qed.
     321
     322lemma will_return_aux_normal : ∀C,depth,t1,t2.
     323  all … (λstr. normal_state C (\fst str)) t1 →
     324  will_return_aux C depth (t1@t2) = will_return_aux C depth t2.
     325#C #depth #t1 #t2 elim t1
     326[ #_ %
     327| * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl
     328  whd in ⊢ (??%?);
     329  cases (normal_state_inv … N1) #CL >CL
     330  @IH @Ntl
     331] qed.
     332
     333lemma measurable_subtrace_preserved :
     334  ∀MS:meas_sim.
     335  ∀g,g'.
     336  ∀INV:ms_inv MS g g'.
     337  ∀s1,s1',depth,callstack.
     338  ms_rel MS g g' INV s1 s1' →
     339 
     340  let C ≝ pcs_to_cs (ms_C1 MS) g in
     341  let C' ≝ pcs_to_cs (ms_C2 MS) g' in
     342
     343  ∀m,interesting,sf.
     344  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈interesting,sf〉 →
     345  ends_at_return (ms_C1 MS) g interesting →
     346  will_return_aux C depth interesting →
     347
     348  ∃m',interesting',sf'.
     349    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈interesting',sf'〉 ∧
     350    (* The obs trace equality almost gives this, but doesn't ensure the
     351       cost/return are exactly at the ends *)
     352    ends_at_return (ms_C2 MS) g' interesting' ∧
     353    bool_to_Prop (will_return_aux C' depth interesting') ∧
     354   
     355    intensional_trace_of_trace C callstack interesting = intensional_trace_of_trace C' callstack interesting'.
     356    (* Seems a shame to leave this out "∧ ms_rel MS g g' INV sf sf'", but it
     357       isn't true if the final return step is expanded into the caller, e.g.,
     358       in Clight → Cminor we added an instruction to callers if they need to
     359       store the result in memory.  This extra step doesn't form part of the
     360       measurable trace, so the end is no longer in the relation. ☹ *)
     361   
     362* #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_return #sim_cost #sim_init
     363#g #g' #INV #s1 #s1' #depth #callstack #REL
     364#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
     365generalize in match callstack; generalize in match depth; -callstack -depth
     366elim m0
     367[ (* "fake" base case - we can never have zero steps *)
     368  #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC
     369  whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct
     370| #m #IH #depth #current_stack #s1 #s1' #REL #prefix #sf #EXEC #END #RETURNS
     371  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
     372  cases (true_or_false_Prop … (pcs_labelled … s1))
     373  [ #CS
     374    lapply (sim_cost … REL CS STEP1)
     375    #AFTER1'
     376    cases (after_n_exec_steps … AFTER1')
     377    #interesting' * #s2' * * #EXEC1' #_ * #Etrace #R2
     378    cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
     379    cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
     380    cases (IH depth current_stack … R2 … EXEC2 ??)
     381    [ (* End must be later, and still a return *)
     382      2: destruct cases END *
     383      [ * #trE * #sE * #E whd in E:(???%); destruct
     384        #CL cases (pnormal_state_inv … N1) >CL #E destruct
     385      | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
     386        %{t} %{trE} %{sE} /2/
     387      ]
     388    | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
     389      cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS
     390    ]
     391    #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
     392    %{(1+m'')} %{(interesting'@interesting'')} %{sf''}
     393    % [ % [ %
     394    [  @(exec_steps_join … EXEC1') @EXEC''
     395    |  @ends_at_return_append assumption
     396    ]| cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
     397       whd in ⊢ (?%); whd in match (cs_classify ??); <(rel_classify … REL)
     398       cases (pnormal_state_inv … N1) #CL >CL @RETURNS''
     399    ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
     400       cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
     401       <all_1 assumption
     402    ]
     403 
     404  | #NCS
     405    cases (true_or_false_Prop (pnormal_state C1 g s1))
     406    [ #NORMAL
     407      (* XXX should set things up so that notb_Prop isn't needed *)
     408      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
     409      #n' #AFTER1'
     410      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
     411      cases (IH depth current_stack … R2 … EXEC2 ??)
     412      [ (* End must be later, and still a return *)
     413        2: destruct cases END *
     414        [ * #trE * #sE * #E whd in E:(???%); destruct
     415          #CL cases (pnormal_state_inv … NORMAL) >CL #E destruct
     416        | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
     417          %{t} %{trE} %{sE} /2/
     418        ]
     419      | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
     420        cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS
     421      ]
     422      #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
     423      %{(n'+m'')} %{(interesting'@interesting'')} %{sf''}
     424      % [ % [ %
     425      [  @(exec_steps_join … EXEC1') @EXEC''
     426      |  @ends_at_return_append assumption
     427      ]| >will_return_aux_normal
     428         [ @RETURNS''
     429         | cases n' in EXEC1';
     430           [ #EXEC >(lenght_to_nil (*sic*) … interesting') // >(exec_steps_length … EXEC) %
     431           | #n'' #EXEC cases (exec_steps_S … EXEC)
     432             #_ * #tr1' * #s2' * #tl * * #E #STEP1' #EXEC2' destruct
     433             @andb_Prop [ <normal_state_p <(rel_normal … REL) @NORMAL | @INV ]
     434           ]
     435         ]
     436      ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     437          [ assumption
     438          | cases interesting' in EXEC1' INV ⊢ %;
     439            [ //
     440            | * #sx #trx #tl #EXEC1' #INV
     441              <(exec_steps_first … EXEC1')
     442              whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
     443              @INV
     444            ]
     445          | @OBS''
     446          ]
     447      ]
     448
     449    | #CALLRET
     450      cases trace2 in E1 EXEC2;
     451        (* For a return we might hit the end - this is the real base case. *)
     452      [ #E1 #EXEC2 destruct cases END #tl * #tr * #s1x * #E1 #CL
     453        cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ]
     454        #E1 normalize in E1; destruct
     455        cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
     456        [2: >CL %]
     457        #m' * #Etr #AFTER1' destruct
     458        cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2'
     459        cut (tr1' = E0) [
     460          cases (after_n_exec_steps … AFTER2') #trace * #sf' * * #_ #_ * #H #_
     461          cases (Eapp_E0_inv … (sym_eq … H)) //
     462        ] #E1 destruct
     463        %{1} %{[〈s1',E0〉]} %{s2'}
     464        % [ % [ %
     465        [  whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); %
     466        |  %{[ ]} %{E0} %{s1'} %{(refl ??)} <(rel_classify … REL) assumption
     467        ]| whd in RETURNS:(?%) ⊢ (?%);
     468           whd in match (cs_classify ??) in RETURNS;
     469           whd in match (cs_classify ??); <(rel_classify … REL)
     470           >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%);
     471           cases depth [ // | #d * ]
     472        ]| <(append_nil … [〈s1',E0〉])
     473           change with (gather_trace … [〈s1',E0〉]) in match E0 in ⊢ (??%?);
     474           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     475           [ @CL
     476           | whd in ⊢ (??%?); <(rel_classify … REL) @CL
     477           | %
     478           | %
     479           ]
     480        ]
     481      ] * #s2x #tr2 #trace3 #E1 #EXEC2
     482      cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
     483      [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
     484        lapply (no_tailcalls … s1)
     485        cases (pcs_classify … s1) in CALLRET ⊢ %;
     486        [ 1,3: #_ #_ /2/
     487        | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??))
     488        ]
     489      ] * #CL
     490      cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
     491      [2,4: >CL %]
     492      #m' * #Etr #AFTER1'
     493      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
     494      [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
     495        letin next_depth ≝ (S depth)
     496      | letin next_stack ≝ (tail … current_stack)
     497        letin next_depth ≝ (pred depth)
     498      ]
     499      cases (IH next_depth next_stack … R2 … EXEC2 ??)
     500      [(* End must be later, and still a return *)
     501        2,5: destruct cases END *
     502        [1,3: * #trE * #sE * #E whd in E:(???%); destruct
     503        |*: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
     504          %{t} %{trE} %{sE} /2/
     505        ]
     506      | 3: destruct whd in RETURNS:(?%);
     507           whd in match (cs_classify ??) in RETURNS;
     508           >CL in RETURNS; //
     509      | 6: destruct whd in RETURNS:(?%);
     510           whd in match (cs_classify ??) in RETURNS;
     511           >CL in RETURNS; whd in ⊢ (?% → ?);
     512           whd in match next_depth; cases depth
     513           [ * | #d' // ]
     514      ]
     515      #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
     516      %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''}
     517      % [1,3: % [1,3: %
     518      [1,3: @(exec_steps_join … EXEC1') @EXEC''
     519      |2,4: @ends_at_return_append assumption
     520      ]|    cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
     521            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
     522            <(rel_classify … REL) >CL whd in ⊢ (?%);
     523            >will_return_aux_normal //
     524       |    cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
     525            destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %;
     526            <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%);
     527            whd in match next_depth in RETURNS'';
     528            cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_
     529            whd in ⊢ (?%);
     530            >will_return_aux_normal [ @RETURNS'' | @INV ]
     531      ]|  destruct cases (exec_steps_S … EXEC1')
     532          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
     533          destruct >Etrace
     534          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     535          [1,3: whd in match (cs_classify ??); >CL %
     536          |2,4: whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     537          | @INV
     538          | assumption
     539          | @(rel_callee … REL)
     540          ]
     541       |  destruct cases (exec_steps_S … EXEC1')
     542          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
     543          destruct >Etrace
     544          @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     545          [ whd in match (cs_classify ??); >CL %
     546          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     547          | @INV
     548          | assumption
     549          ]
     550       ]
     551    ]
     552  ]
     553] qed.
     554
     555lemma label_to_ret_inv : ∀C,m,g,s,trace,s'.
     556  exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 →
     557  trace_is_label_to_return (pcs_to_cs … C g) trace →
     558  bool_to_Prop (pcs_labelled C g s) ∧ ends_at_return C g trace.
     559#C #m #g #s #trace #s' #EXEC
     560* #tr * #s1 * #tl * #tr2 * #s2 * * #E #CS #CL destruct
     561>(exec_steps_first … EXEC)
     562%
     563[ @CS
     564| %{(〈s1,tr〉::tl)} %{tr2} %{s2} %{(refl ??)} @CL
     565] qed.
     566
     567lemma build_label_to_ret : ∀C,m,g,s,trace,s'.
     568  (∀s. pcs_labelled C g s → pnormal_state C g s) →
     569  exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 →
     570  pcs_labelled C g s →
     571  ends_at_return C g trace →
     572  trace_is_label_to_return (pcs_to_cs … C g) trace.
     573#C #m #g #s #trace #s' #LABELLED_NORMAL #EXEC #CS * #trace' * #tr2 * #s2 * #E #CL
     574destruct
     575cases trace' in EXEC ⊢ %;
     576[ #EXEC >(exec_steps_first … EXEC) in CS; #CS
     577  cases (pnormal_state_inv … (LABELLED_NORMAL … CS)) >CL #E destruct
     578| * #s1 #tr1 #trace1 #EXEC
     579  %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ % | <(exec_steps_first … EXEC) @CS ] | @CL ]
     580] qed.
     581
     582(* TODO: explicitly mention observables *)
    304583theorem measured_subtrace_preserved :
    305584  ∀MS:meas_sim.
     
    308587  measurable (ms_C1 MS) p1 m n stack_cost max →
    309588  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
    310 
     589#MS #p1 #p2 #m #n #stack_cost #max #compiled
     590* #s0 * #prefix * #s1 * #interesting * #s2
     591whd in ⊢ (? → ??(λ_.??(λ_.%)));
     592letin g ≝ (make_global … (pcs_exec … ) p1)
     593letin g' ≝ (make_global … (pcs_exec … ) p2)
     594letin C ≝ (pcs_to_cs ? g)
     595letin C' ≝ (pcs_to_cs ? g')
     596* * * * * #INIT #EXEC0 #EXEC1 #TLR #RETURNS #MAX
     597
     598cases (sim_init … compiled INIT) #s0' * #INIT' * #INV #R0
     599cases (label_to_ret_inv … EXEC1 TLR)
     600#CS1 #ENDS
     601
     602cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1)
     603#m' * #prefix' * #s1' * * #EXEC0' #OBS0 #R1
     604
     605cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] prefix)) R1 … EXEC1 ENDS RETURNS)
     606#n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS'
     607
     608%{m'} %{n'} %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'}
     609% [ % [ % [ % [ %
     610[  assumption
     611|  assumption
     612]| assumption
     613]| @(build_label_to_ret … EXEC1' ? ENDS')
     614   [ #s #CS @(ms_labelled_normal_2 … CS)
     615   | <(ms_rel_labelled … R1) @CS1
     616   ]
     617]| @RETURNS'
     618]| cases daemon (* TODO! *)
     619] qed.
Note: See TracChangeset for help on using the changeset viewer.