Changeset 2989


Ignore:
Timestamp:
Mar 27, 2013, 7:00:14 PM (4 years ago)
Author:
campbell
Message:

Make front-end measurability preservation proof cope with moving the cost
label to the front of the function.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2953 r2989  
    6060      (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))
    6161    );
    62   sim_call :
     62  (* Naughty code without a cost label will end up being rejected, but we don't
     63     have local information about that. *)
     64  sim_call_nolabel :
    6365    ∀g1,g2.
    6466    ∀INV:ms_inv g1 g2.
     
    6769    pcs_classify ms_C1 g1 s1 = cl_call →
    6870    ¬ 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. *)
    77     ∀s2,tr.
    78       if pcs_labelled ms_C1 g1 s2 then
    79         (∃si,tri1,tri2. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tri1,si〉 ∧
    80           bool_to_Prop (pcs_labelled ms_C1 g1 si) ∧
    81           step … (pcs_exec ms_C1) g1 si = Value … 〈tri1,s2〉 ∧
    82           tr = tri1 ⧺ tri2)
    83       else
    84         (step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉)
    85       →
     71    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
     72    ¬ pcs_labelled ms_C1 g1 s2 →
    8673    ∃m.
    8774      after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
    8875      tr = tr' ∧
    8976      ms_rel g1 g2 INV s2 s2'
     77    );
     78  (* Note that extra steps are introduced in the front-end to perform variable
     79     saves on entry.  If there's a cost label (and there ought to be!) then we
     80     move it forward, so have to include it in the simulation.  Unfortunately
     81     that's a little messy. *)
     82  sim_call_label :
     83    ∀g1,g2.
     84    ∀INV:ms_inv g1 g2.
     85    ∀s1,s1'.
     86    ms_rel g1 g2 INV s1 s1' →
     87    pcs_classify ms_C1 g1 s1 = cl_call →
     88    ¬ pcs_labelled ms_C1 g1 s1 →
     89    ∀s2,tr2,s3,tr3.
     90    step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr2,s2〉 →
     91    pcs_labelled ms_C1 g1 s2 →
     92    step … (pcs_exec ms_C1) g1 s2 = Value … 〈tr3,s3〉 →
     93    ∃m.
     94      after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
     95        tr2 = tr' ∧
     96        bool_to_Prop (pcs_labelled ms_C2 g2 s2') ∧
     97        (after_n_steps m … (pcs_exec ms_C2) g2 s2' (λs.pnormal_state ms_C2 g2 s) (λtr'',s3'.
     98         tr'' = tr3 ∧
     99         ms_rel g1 g2 INV s3 s3'))
    90100    );
    91101  sim_return :
     
    226236
    227237
    228 (* TODO repair proof
    229238
    230239lemma prefix_preserved :
     
    239248  pcs_labelled (ms_C1 MS) g sf →
    240249
     250  (* Needed to ensure we can get back into the relation after a call *)
     251  (∃ex,sx. exec_steps 1 … (pcs_exec … (ms_C1 MS)) g sf = OK ? 〈ex,sx〉) →
     252
    241253  ∃m',prefix',sf'.
    242254    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
    243 
     255    bool_to_Prop (pcs_labelled (ms_C2 MS) g' sf') ∧
    244256    intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧
    245     ms_rel MS g g' INV sf sf'.
    246 * #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
     257
     258
     259    (* We may need to make extra steps to get back into the relation.  In
     260       particular, the Clight to Cminor stage adds stores to the stack after
     261       the function call, but must preserve the position of the cost label at
     262       the head of the function, so we may need to move past these stores. *)
     263    ∃r,r',ex,ex',sr,sr'.
     264      exec_steps r … (pcs_exec … (ms_C1 MS)) g sf = OK … 〈ex,sr〉 ∧
     265      bool_to_Prop (all … (λst.pnormal_state (ms_C1 MS) g (\fst st)) ex) ∧
     266      exec_steps r' … (pcs_exec … (ms_C2 MS)) g' sf' = OK … 〈ex',sr'〉 ∧
     267      bool_to_Prop (all … (λst.pnormal_state (ms_C2 MS) g' (\fst st)) ex') ∧
     268      (∀cs. intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) cs ex = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') cs ex') ∧
     269      ms_rel MS g g' INV sr sr'.
     270
     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
    247272#g #g' #INV #s1 #s1' #REL
    248273#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
    249274generalize in match [ ]; (* current call stack *)
    250 elim m0
    251 [ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
     275@(nat_elim1 m0) *
     276[ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf #_
    252277  %{0} %{[]} %{s1'}
    253   % [ % // | // ]
    254 | #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf
     278  % [ % [ % [ // | <(rel_labelled … REL) // ] | // ] | %{0} %{0} %{[ ]} %{[ ]} %{sf} %{s1'} /6/ ]
     279| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #EXTRA_STEP
    255280  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
    256281  cases (true_or_false_Prop … (pcs_labelled … s1))
     
    262287    cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
    263288    cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
    264     cases (IH current_stack … R2 … EXEC2 CSf)
    265     #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
     289    cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
     290    #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R''
    266291    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
    267     % [ % [ @(exec_steps_join … EXEC1') @EXEC''
    268       | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
    269         cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
    270         <all_1 assumption
    271       ]| assumption
    272       ]
     292    % [ % [ %
     293    [  @(exec_steps_join … EXEC1') @EXEC''
     294    |  @CS''
     295    ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
     296       cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
     297       <all_1 assumption
     298    ]| assumption
     299    ]
    273300 
    274301  | #NCS
     
    279306      #n' #AFTER1'
    280307      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
    281       cases (IH current_stack … R2 … EXEC2 CSf)
    282       #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
     308      cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
     309      #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R''
    283310      %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
    284       % [ % [ @(exec_steps_join … EXEC1') @EXEC''
    285         | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    286           [ assumption
    287           | cases prefix' in EXEC1' INV ⊢ %;
    288             [ //
    289             | * #sx #trx #tl #EXEC1' #INV
    290               <(exec_steps_first … EXEC1')
    291               whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
    292               @INV
    293             ]
    294           | @OBS'' ] ]
    295         | @R''
    296         ]
     311      % [ % [ %
     312      [  @(exec_steps_join … EXEC1') @EXEC''
     313      |  @CS''
     314      ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     315         [ assumption
     316         | cases prefix' in EXEC1' INV ⊢ %;
     317           [ //
     318           | * #sx #trx #tl #EXEC1' #INV
     319             <(exec_steps_first … EXEC1')
     320             whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
     321             @INV
     322           ]
     323         | @OBS''
     324         ]
     325      ]| @R''
     326      ]
     327
    297328    | #CALLRET
    298329      cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
     
    304335        ]
    305336      ] * #CL
    306       cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
    307       [2,4: >CL %]
    308       #m' * #Etr #AFTER1'
    309       cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
    310       [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
    311       | letin next_stack ≝ (tail … current_stack)
    312       ]
    313       cases (IH next_stack … R2 … EXEC2 CSf)
    314       #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
    315       %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
    316       % [1,3: % [1,3: @(exec_steps_join … EXEC1') @EXEC''
    317         | destruct cases (exec_steps_S … EXEC1')
    318           #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
    319           destruct >Etrace
    320           @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    321           [ whd in match (cs_classify ??); >CL %
    322           | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
    323           | @INV
    324           | assumption
    325           | @(rel_callee … REL)
     337      [ cases (true_or_false_Prop … (pcs_labelled … s2))
     338        [ #CS2
     339          (* Can we execute another step now, or shall we wait for later? *)
     340          cases m in IH EXEC2;
     341          [ #_ (* Nope, use extra step to get back into relation *)
     342            #EXEC2 whd in EXEC2:(??%%); destruct
     343            cases EXTRA_STEP #trx * #sx #EXTRA -EXTRA_STEP
     344            cases (exec_steps_S … EXTRA) #NFf * #trx' * #sx' * #tlx * * #Ex #EXTRA_STEP #EX' whd in EX':(??%?); destruct
     345            cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 EXTRA_STEP)
     346            #m' #AFTER1'
     347            cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace #CS2' #AFTER2'
     348            cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2 #R3
     349            %{1} %{prefix1'} %{s2'}
     350            % [ % [ %
     351            [  @EXEC1'
     352            |  @CS2'
     353            ]| destruct cases (exec_steps_S … EXEC1')
     354               #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
     355               destruct <(append_nil … (?::prefix2)) in ⊢ (???%);
     356               @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     357               [ whd in match (cs_classify ??); >CL %
     358               | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     359               | @INV1
     360               | %
     361               | @(rel_callee … REL)
     362               ]
     363            ]| %{1} %{m'} %{[〈sf,trx'〉]} %{prefix2'} %{sx} %{s3'}
     364               cut (all ? (λst.pnormal_state C2 g' (\fst st)) prefix2')
     365               [ cases prefix2' in EXEC2' INV2 ⊢ %;
     366                  [ //
     367                  | * #sp #trp #tlp #EXEC2' #INV2
     368                    whd in ⊢ (?%); <(exec_steps_first … EXEC2')
     369                    >labelled_normal2 //
     370                  ]
     371               ] #Np2'
     372               % [ % [ % [ % [ %
     373               [  @EXTRA
     374               |  whd in ⊢ (?%); >labelled_normal1 //
     375               ]| @EXEC2'
     376               ]| @Np2'
     377               ]| #cs <(append_nil … prefix2') <Etrace2
     378                  @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     379                  [ <normal_state_p @labelled_normal1 //
     380                  | @Np2'
     381                  | //
     382                  ]
     383               ]| @R3
     384               ]
     385            ]
     386          (* We can execute the cost label, too. *)
     387          | #m1 #IH #EXEC2
     388            cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3
     389            cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2)
     390            #m' #AFTER1'
     391            cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2'
     392            cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3
     393            letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
     394            cases (IH m1 ? next_stack … R3 … EXEC3 CSf EXTRA_STEP) [2: // ]
     395            #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R''
     396            %{(S m' + m'')} %{(prefix1'@prefix2'@prefix'')} %{sf''}
     397            % [ % [ %
     398            [  @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC''
     399            |  @CSf''
     400            ]| destruct cases (exec_steps_S … EXEC1')
     401               #NF1' * #tr1' * #s2'' * #prefix2'' * * #E #STEP1' #EXEC2''
     402               whd in EXEC2'':(??%%);
     403               destruct
     404               @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     405               [ whd in match (cs_classify ??); >CL %
     406               | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     407               | %
     408               | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     409                 [ <normal_state_p @labelled_normal1 @CS2
     410                 | cases prefix2' in EXEC2' INV2 ⊢ %;
     411                   [ //
     412                   | * #sy #try #tly #EXEC2' #INV2
     413                     <(exec_steps_first … EXEC2')
     414                     whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 //
     415                   ]
     416                 | assumption
     417                 ]
     418               | @(rel_callee … REL)
     419               ]
     420            ]| @R''
     421            ]
    326422          ]
    327         | destruct cases (exec_steps_S … EXEC1')
    328           #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
    329           destruct >Etrace
    330           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    331           [ whd in match (cs_classify ??); >CL %
    332           | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
    333           | @INV
    334           | assumption
     423
     424        | #NCS2
     425          cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1)
     426          [2: >CL % | 3: @notb_Prop @NCS2 ]
     427          #m' #AFTER1'
     428          cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
     429          letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
     430          cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
     431          #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R''
     432          %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
     433          % [ % [ %
     434          [  @(exec_steps_join … EXEC1') @EXEC''
     435          |  @CSf''
     436          ]| destruct cases (exec_steps_S … EXEC1')
     437             #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
     438             destruct
     439             @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     440             [ whd in match (cs_classify ??); >CL %
     441             | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     442             | @INV
     443             | assumption
     444             | @(rel_callee … REL)
     445             ]
     446          ]| @R''
    335447          ]
    336448        ]
    337       | 2,4: @R''
     449
     450      | cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %]
     451        #m' * #Etr #AFTER1'
     452        cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
     453        letin next_stack ≝ (tail … current_stack)
     454        cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: //]
     455        #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R''
     456        %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
     457        % [ % [ %
     458        [  @(exec_steps_join … EXEC1') @EXEC''
     459        |  @CSf''
     460        ]| destruct cases (exec_steps_S … EXEC1')
     461           #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
     462           destruct >Etrace
     463           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     464           [ whd in match (cs_classify ??); >CL % 
     465           | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     466           | @INV
     467           | assumption
     468           ]
     469        ]| @R''
     470        ]
    338471      ]
    339472    ]
     
    391524       measurable trace, so the end is no longer in the relation. ☹ *)
    392525   
    393 * #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
     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
    394527#g #g' #INV #s1 #s1' #depth #callstack #REL
    395528#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
    396529generalize in match callstack; generalize in match depth; -callstack -depth
    397 elim m0
    398 [ (* "fake" base case - we can never have zero steps *)
     530@(nat_elim1 m0) *
     531[ #_ (* "fake" base case - we can never have zero steps *)
    399532  #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC
    400533  whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct
     
    409542    cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
    410543    cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
    411     cases (IH depth current_stack … R2 … EXEC2 ??)
    412     [ (* End must be later, and still a return *)
    413       2: destruct cases END *
     544    cases (IH m ? depth current_stack … R2 … EXEC2 ??)
     545    [ 2: //
     546    | (* End must be later, and still a return *)
     547      3: destruct cases END *
    414548      [ * #trE * #sE * #E whd in E:(???%); destruct
    415549        #CL cases (pnormal_state_inv … N1) >CL #E destruct
     
    417551        %{t} %{trE} %{sE} /2/
    418552      ]
    419     | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
     553    | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
    420554      cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS
    421555    ]
     
    440574      #n' #AFTER1'
    441575      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
    442       cases (IH depth current_stack … R2 … EXEC2 ??)
    443       [ (* End must be later, and still a return *)
    444         2: destruct cases END *
     576      cases (IH m ? depth current_stack … R2 … EXEC2 ??)
     577      [ 2: //
     578      | (* End must be later, and still a return *)
     579        3: destruct cases END *
    445580        [ * #trE * #sE * #E whd in E:(???%); destruct
    446581          #CL cases (pnormal_state_inv … NORMAL) >CL #E destruct
     
    448583          %{t} %{trE} %{sE} /2/
    449584        ]
    450       | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
     585      | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
    451586        cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS
    452587      ]
     
    484619        cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ]
    485620        #E1 normalize in E1; destruct
    486         cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
    487         [2: >CL %]
     621        cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %]
    488622        #m' * #Etr #AFTER1' destruct
    489623        cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2'
     
    510644           ]
    511645        ]
    512       ] * #s2x #tr2 #trace3 #E1 #EXEC2
     646      ]
     647      (* Not at the end *)
     648      * #s2x #tr2 #trace3 #E1 #EXEC2
    513649      cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
    514650      [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
     
    519655        ]
    520656      ] * #CL
    521       cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
    522       [2,4: >CL %]
     657     
     658      [ cases (true_or_false_Prop … (pcs_labelled … s2))
     659        [ #CS2
     660          (* We can't stop here *)
     661          cases m in IH EXEC2;
     662          [ #_ #EXEC2 whd in EXEC2:(??%%); destruct ]
     663          #m1 #IH #EXEC2
     664          cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3
     665          cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2)
     666          #m' #AFTER1'
     667          cases (after_n_exec_steps … AFTER1') #interesting1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2'
     668          cases (after_n_exec_steps … AFTER2') #interesting2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3
     669          letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
     670          letin next_depth ≝ (S depth)
     671          cut (pnormal_state C1 g s2) [ @labelled_normal1 assumption ] #N2
     672          cases (IH m1 ? next_depth next_stack … R3 … EXEC3 ??)
     673          [ 2: //
     674          | (* End must be later, and still a return *)
     675            3: destruct cases END *
     676            [ * #trE * #sE * #E whd in E:(???%); destruct
     677            | *: #h1 *
     678              [ * #trE * #sE * #E normalize in E:(???%); destruct
     679                #CL cases (pnormal_state_inv … N2) >CL #E destruct
     680              | #h2 #t * #trE * #sE * #E normalize in E:(???%); destruct #CL
     681                 %{t} %{trE} %{sE} /2/
     682              ]
     683            ]
     684          | 4: destruct whd in RETURNS:(?%);
     685            whd in match (cs_classify ??) in RETURNS;
     686            >CL in RETURNS; whd in ⊢ (?% → ?);
     687            cases (pnormal_state_inv … N2) #CL2
     688            whd in match (cs_classify ??); >CL2 //
     689          ]
     690          #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
     691          %{(S m' + m'')} %{(interesting1'@interesting2'@interesting'')} %{sf''}
     692          % [ % [ %
     693          [ @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC''
     694          | @ends_at_return_append @ends_at_return_append assumption
     695         ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2''
     696            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
     697            <(rel_classify … REL) >CL whd in ⊢ (?%); whd in INV1:(?(???%));
     698            >will_return_aux_normal [2: @INV1 ]
     699            >will_return_aux_normal
     700            [ //
     701            | cases interesting2' in EXEC2' INV2 ⊢ %;
     702              [ //
     703              | * #s2'' #tr2'' #tl2'' #E2'' <(exec_steps_first … E2'') #TL
     704                whd in ⊢ (?%); <normal_state_p >(labelled_normal2 … CS2') @TL
     705              ]
     706            ]
     707         ]| destruct cases (exec_steps_S … EXEC1')
     708            #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2''
     709            destruct
     710            @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     711            [ whd in match (cs_classify ??); >CL %
     712            | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     713            | @INV1
     714            | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     715              (* Repeats bits of proof above, could compress *)
     716              [ <normal_state_p @labelled_normal1 @CS2
     717              | cases interesting2' in EXEC2' INV2 ⊢ %;
     718                [ //
     719                | * #sy #try #tly #EXEC2' #INV2
     720                  <(exec_steps_first … EXEC2')
     721                  whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 //
     722                ]
     723              | assumption
     724              ]
     725            | @(rel_callee … REL)
     726            ]
     727          ]
     728
     729        | #NCS2
     730          cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1)
     731          [2: >CL % | 3: @notb_Prop @NCS2 ]
     732          #m' #AFTER1'
     733          cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
     734          letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
     735          letin next_depth ≝ (S depth)
     736          cases (IH m ? next_depth next_stack … R2 … EXEC2 ??)
     737          [ 2: //
     738          | (* End must be later, and still a return *)
     739            3: destruct cases END *
     740            [ * #trE * #sE * #E whd in E:(???%); destruct
     741            | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
     742              %{t} %{trE} %{sE} /2/
     743            ]
     744          | 4: destruct whd in RETURNS:(?%);
     745               whd in match (cs_classify ??) in RETURNS;
     746               >CL in RETURNS; //
     747          ]
     748          #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
     749          %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''}
     750          % [ % [ %
     751          [ @(exec_steps_join … EXEC1') @EXEC''
     752          | @ends_at_return_append assumption
     753         ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
     754            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
     755            <(rel_classify … REL) >CL whd in ⊢ (?%);
     756            >will_return_aux_normal //
     757         ]| destruct cases (exec_steps_S … EXEC1')
     758            #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
     759            destruct
     760            @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     761            [ whd in match (cs_classify ??); >CL %
     762            | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     763            | @INV
     764            | assumption
     765            | @(rel_callee … REL)
     766            ]
     767          ]
     768       ]
     769     |
     770
     771      cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %]
    523772      #m' * #Etr #AFTER1'
    524773      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
    525       [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
    526         letin next_depth ≝ (S depth)
    527       | letin next_stack ≝ (tail … current_stack)
    528         letin next_depth ≝ (pred depth)
    529       ]
    530       cases (IH next_depth next_stack … R2 … EXEC2 ??)
    531       [(* End must be later, and still a return *)
    532         2,5: destruct cases END *
    533         [1,3: * #trE * #sE * #E whd in E:(???%); destruct
    534         |*: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
     774      letin next_stack ≝ (tail … current_stack)
     775      letin next_depth ≝ (pred depth)
     776      cases (IH m ? next_depth next_stack … R2 … EXEC2 ??)
     777      [ 2: //
     778      | (* End must be later, and still a return *)
     779        3: destruct cases END *
     780        [ * #trE * #sE * #E whd in E:(???%); destruct
     781        | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
    535782          %{t} %{trE} %{sE} /2/
    536783        ]
    537       | 3: destruct whd in RETURNS:(?%);
    538            whd in match (cs_classify ??) in RETURNS;
    539            >CL in RETURNS; //
    540       | 6: destruct whd in RETURNS:(?%);
     784      | 4: destruct whd in RETURNS:(?%);
    541785           whd in match (cs_classify ??) in RETURNS;
    542786           >CL in RETURNS; whd in ⊢ (?% → ?);
     
    546790      #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
    547791      %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''}
    548       % [1,3: % [1,3: %
    549       [1,3: @(exec_steps_join … EXEC1') @EXEC''
    550       |2,4: @ends_at_return_append assumption
    551       ]|    cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
    552             destruct whd in ⊢ (?%); whd in match (cs_classify ??);
    553             <(rel_classify … REL) >CL whd in ⊢ (?%);
    554             >will_return_aux_normal //
    555        |    cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
    556             destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %;
    557             <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%);
    558             whd in match next_depth in RETURNS'';
    559             cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_
    560             whd in ⊢ (?%);
    561             >will_return_aux_normal [ @RETURNS'' | @INV ]
    562       ]|  destruct cases (exec_steps_S … EXEC1')
    563           #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
    564           destruct >Etrace
    565           @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    566           [ whd in match (cs_classify ??); >CL %
    567           | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
    568           | @INV
    569           | assumption
    570           | @(rel_callee … REL)
    571           ]
    572        |  destruct cases (exec_steps_S … EXEC1')
    573           #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
    574           destruct >Etrace
    575           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    576           [ whd in match (cs_classify ??); >CL %
    577           | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
    578           | @INV
    579           | assumption
    580           ]
    581        ]
     792      % [ % [ %
     793      [ @(exec_steps_join … EXEC1') @EXEC''
     794      | @ends_at_return_append assumption
     795     ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
     796        destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %;
     797        <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%);
     798        whd in match next_depth in RETURNS'';
     799        cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_
     800        whd in ⊢ (?%);
     801        >will_return_aux_normal [ @RETURNS'' | @INV ]
     802     ]| destruct cases (exec_steps_S … EXEC1')
     803        #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
     804        destruct >Etrace
     805        @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
     806        [ whd in match (cs_classify ??); >CL %
     807        | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     808        | @INV
     809        | assumption
     810        ]
    582811    ]
    583812  ]
     
    610839  %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ % | <(exec_steps_first … EXEC) @CS ] | @CL ]
    611840] qed.
     841
     842(* TODO: move*)
     843lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.
     844#x0 elim x0
     845[ #y %{y} %2 %
     846| #x #IH *
     847  [ %{(S x)} %1 %
     848  | #y cases (IH y) #z *
     849    [ #H %{z} %1 >H //
     850    | #H %{z} %2 >H //
     851    ]
     852  ]
     853] qed.
     854
     855lemma all_append : ∀A,p,l1,l2.
     856  all A p (l1@l2) →
     857  all A p l1 ∧ all A p l2.
     858#A #p #l1 elim l1
     859[ //
     860| #h #t #IH #l2
     861  whd in ⊢ (?% → ?(?%?));
     862  cases (p h) //
     863  @IH
     864] qed.
     865
     866
     867lemma ends_at_return_normal : ∀C,g,t1,t2.
     868  ends_at_return C g (t1@t2) →
     869  all … (λst. pnormal_state C g (\fst st)) t1 →
     870  ends_at_return C g t2.
     871#C #g #t1 elim t1
     872[ //
     873| * #s #tr #tl #IH #t2 * #tr1 * #tr2 * #s2 * cases tr1
     874  [ #E normalize in E; destruct #CL whd in ⊢ (?% → ?);
     875    lapply (pnormal_state_inv … s2)
     876    cases (pnormal_state … s2)
     877    [ #H cases (H I) >CL #E' destruct
     878    | #_ *
     879    ]
     880  | * #s' #tr' #tl' #E whd in E:(??%%); destruct #CL #ALL
     881    @IH
     882    [ %{tl'} %{tr2} %{s2} >e0 % //
     883    | whd in ALL:(?%); cases (pnormal_state … s') in ALL;
     884      [ // | * ]
     885    ]
     886  ]
     887] qed.
     888
    612889
    613890
     
    634911
    635912cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1)
    636 #m' * #prefix' * #s1' * * #EXEC0' #OBS0 #R1
    637 
    638 cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] prefix)) R1 … EXEC1 ENDS RETURNS)
     913(* Need an extra step from the source in case we end up at a label after a
     914   function call. *)
     915[2: cases n in EXEC1;
     916  [ #E whd in E:(??%?); destruct cases RETURNS
     917  | #n1 #EXEC1 cases (exec_steps_split 1 … EXEC1) #ex * #ex2 * #sx * * #EX1 #_ #_
     918    %{ex} %{sx} @EX1
     919  ]
     920]
     921#m' * #prefix' * #s1' * * * #EXEC0' #CS1' #OBS0
     922* #r * #r' * #interesting1 * #interesting1' * #sr * #sr' * * * * * #EXECr #Nr #EXECr' #Nr' #OBS1 #R1
     923
     924(* Show that the extra r steps we need to get back into the relation are a
     925   prefix of the measurable subtrace. *)
     926cut (∃nr,interesting2. n = r + nr ∧
     927  exec_steps nr … C g sr = OK … 〈interesting2,s2〉 ∧
     928  interesting = interesting1 @ interesting2)
     929[ cases (plus_split n r) #nr *
     930  [ #En %{nr} >En in EXEC1; #EXEC1
     931    cases (exec_steps_split … EXEC1)
     932    #interesting1x * #interesting2 * #srx * * #EXEC1x #EXECrx #E
     933    >EXECr in EXEC1x; #E1x destruct
     934    %{interesting2} % [ % [ % | assumption ] | % ]
     935  | #En @⊥
     936    >En in EXECr; #EXECr cases (exec_steps_split … EXECr)
     937    #ex1 * #ex2 * #sx * * #EX1 #EXx #E >E in Nr; >EXEC1 in EX1; #E' destruct
     938    #Nr cases (andb_Prop_true … (all_append … Nr)) #N1 #N2
     939    cases ENDS #le * #tre * #se * #Ee #CLe destruct
     940    cases (andb_Prop_true … (all_append … N1)) #_ whd in ⊢ (?% → ?);
     941    lapply (pnormal_state_inv … se) cases (pnormal_state … se)
     942    [ #H cases (H I) >CLe #E destruct
     943    | #_ *
     944    ]
     945  ]
     946]
     947* #nr * #interesting2 * * #En #EXECr2 #Ei destruct
     948
     949whd in RETURNS:(?%);
     950>will_return_aux_normal in RETURNS;
     951[2: @Nr] #RETURNS
     952
     953lapply (ends_at_return_normal … ENDS Nr)
     954#ENDS2
     955
     956cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] (prefix@interesting1))) R1 … EXECr2 ENDS2 RETURNS)
    639957#n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS'
    640958
    641 cut (intensional_trace_of_trace C [ ] (prefix@interesting) =
    642      intensional_trace_of_trace C' [ ] (prefix'@interesting'))
    643 [ >int_trace_append' >int_trace_append'
     959cut (intensional_trace_of_trace C [ ] (prefix@interesting1) =
     960     intensional_trace_of_trace C' [ ] (prefix'@interesting1'))
     961[ >int_trace_append' >(int_trace_append' C')
    644962  <OBS0 @breakup_pair @breakup_pair @breakup_pair @breakup_pair
     963  <OBS1 %
     964] #OBS01
     965
     966cut (intensional_trace_of_trace C [ ] (prefix@interesting1@interesting2) =
     967     intensional_trace_of_trace C' [ ] (prefix'@interesting1'@interesting'))
     968[ <associative_append <associative_append
     969  >int_trace_append' >(int_trace_append' C')
     970  <OBS01
     971  @breakup_pair @breakup_pair @breakup_pair @breakup_pair
    645972  <OBS' %
    646973] #Eobs
    647974
    648 %{m'} %{n'} %
    649 [ %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'}
     975lapply (exec_steps_join … EXECr' EXEC1')
     976#EXECr''
     977
     978%{m'} %{(r' + n')} %
     979[ %{s0'} %{prefix'} %{s1'} %{(interesting1'@interesting')} %{s2'}
    650980  % [ % [ % [ % [ %
    651981  [  assumption
    652982  |  assumption
    653983  ]| assumption
    654   ]| @(build_label_to_ret … EXEC1' ? ENDS')
     984  ]| @(build_label_to_ret … EXECr'' ? (ends_at_return_append … ENDS'))
    655985     [ #s #CS @(ms_labelled_normal_2 … CS)
    656      | <(ms_rel_labelled … R1) @CS1
     986     | <(ms_rel_labelled … R1) @CS1'
    657987     ]
    658   ]| @RETURNS'
     988  ]| whd in ⊢ (?%); >will_return_aux_normal [2: @Nr'] @RETURNS'
    659989  ]| <Eobs @MAX
    660990  ]
    661991| >INIT >INIT'
    662992  whd in ⊢ (??%%); >EXEC0 >EXEC0'
    663   whd in ⊢ (??%%); >EXEC1 >EXEC1'
    664   whd in ⊢ (??%%); <OBS0 cases (intensional_trace_of_trace C [ ] prefix) in OBS' ⊢ %;
    665   #cs #prefixtr #OBS' whd in ⊢ (??%%); >OBS' %
     993  whd in ⊢ (??%%); >EXEC1 >EXECr''
     994  whd in ⊢ (??%%); >int_trace_append' in OBS'; <OBS0
     995  cases (intensional_trace_of_trace C [ ] prefix)
     996  #cs #prefixtr whd in ⊢ (??(??(???%)?)(??(???%)?) → ??%%);
     997  >int_trace_append' >int_trace_append' <OBS1
     998  @breakup_pair @breakup_pair @breakup_pair @breakup_pair @breakup_pair
     999  #OBS' <OBS' %
    6661000] qed.
    667 *)
Note: See TracChangeset for help on using the changeset viewer.