Changeset 2989

Timestamp:

Mar 27, 2013, 7:00:14 PM (6 years ago)

Author:

campbell

Message:

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

File:

• src/common/FEMeasurable.ma (modified) (18 diffs)

src/common/FEMeasurable.ma

@@ -60 +60 @@
       (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))
     );
-  sim_call :
+  (* Naughty code without a cost label will end up being rejected, but we don't
+     have local information about that. *)
+  sim_call_nolabel :
     ∀g1,g2.
     ∀INV:ms_inv g1 g2.
@@ -67 +69 @@
     pcs_classify ms_C1 g1 s1 = cl_call →
     ¬ pcs_labelled ms_C1 g1 s1 →
-    (* NB: calls and returns don't emit timing cost labels; otherwise we would
-       have to worry about whether the cost labels seen at the final return of
-       the measured trace might appear in the target in subsequent steps that
-       are *after* the new measurable subtrace.  Also note that extra steps are
-       introduced in the front-end: to perform variable saves on entry and to
-       write back the result *after* exit.  The latter do not get included in
-       the measurable subtrace because it stops at the return, and they are the
-       caller's responsibility. *)
-    ∀s2,tr.
-      if pcs_labelled ms_C1 g1 s2 then
-        (∃si,tri1,tri2. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tri1,si〉 ∧
-          bool_to_Prop (pcs_labelled ms_C1 g1 si) ∧
-          step … (pcs_exec ms_C1) g1 si = Value … 〈tri1,s2〉 ∧
-          tr = tri1 ⧺ tri2)
-      else
-        (step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉)
-      →
+    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
+    ¬ pcs_labelled ms_C1 g1 s2 →
     ∃m.
       after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
       tr = tr' ∧
       ms_rel g1 g2 INV s2 s2'
+    );
+  (* Note that extra steps are introduced in the front-end to perform variable
+     saves on entry.  If there's a cost label (and there ought to be!) then we
+     move it forward, so have to include it in the simulation.  Unfortunately
+     that's a little messy. *)
+  sim_call_label :
+    ∀g1,g2.
+    ∀INV:ms_inv g1 g2.
+    ∀s1,s1'.
+    ms_rel g1 g2 INV s1 s1' →
+    pcs_classify ms_C1 g1 s1 = cl_call →
+    ¬ pcs_labelled ms_C1 g1 s1 →
+    ∀s2,tr2,s3,tr3.
+    step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr2,s2〉 →
+    pcs_labelled ms_C1 g1 s2 →
+    step … (pcs_exec ms_C1) g1 s2 = Value … 〈tr3,s3〉 →
+    ∃m.
+      after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
+        tr2 = tr' ∧
+        bool_to_Prop (pcs_labelled ms_C2 g2 s2') ∧
+        (after_n_steps m … (pcs_exec ms_C2) g2 s2' (λs.pnormal_state ms_C2 g2 s) (λtr'',s3'.
+         tr'' = tr3 ∧
+         ms_rel g1 g2 INV s3 s3'))
     );
   sim_return :
@@ -226 +236 @@
 
 
-(* TODO repair proof
 
 lemma prefix_preserved :
@@ -239 +248 @@
   pcs_labelled (ms_C1 MS) g sf →
 
+  (* Needed to ensure we can get back into the relation after a call *)
+  (∃ex,sx. exec_steps 1 … (pcs_exec … (ms_C1 MS)) g sf = OK ? 〈ex,sx〉) →
+
   ∃m',prefix',sf'.
     exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
-
+    bool_to_Prop (pcs_labelled (ms_C2 MS) g' sf') ∧
     intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧
-    ms_rel MS g g' INV sf sf'.
-* #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
+
+
+    (* We may need to make extra steps to get back into the relation.  In
+       particular, the Clight to Cminor stage adds stores to the stack after
+       the function call, but must preserve the position of the cost label at
+       the head of the function, so we may need to move past these stores. *)
+    ∃r,r',ex,ex',sr,sr'.
+      exec_steps r … (pcs_exec … (ms_C1 MS)) g sf = OK … 〈ex,sr〉 ∧
+      bool_to_Prop (all … (λst.pnormal_state (ms_C1 MS) g (\fst st)) ex) ∧
+      exec_steps r' … (pcs_exec … (ms_C2 MS)) g' sf' = OK … 〈ex',sr'〉 ∧
+      bool_to_Prop (all … (λst.pnormal_state (ms_C2 MS) g' (\fst st)) ex') ∧
+      (∀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') ∧
+      ms_rel MS g g' INV sr sr'.
+
+* #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
 #g #g' #INV #s1 #s1' #REL
 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
 generalize in match [ ]; (* current call stack *)
-elim m0
-[ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
+@(nat_elim1 m0) *
+[ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf #_
   %{0} %{[]} %{s1'}
-  % [ % // | // ]
-| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf
+  % [ % [ % [ // | <(rel_labelled … REL) // ] | // ] | %{0} %{0} %{[ ]} %{[ ]} %{sf} %{s1'} /6/ ]
+| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #EXTRA_STEP
   cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
   cases (true_or_false_Prop … (pcs_labelled … s1))
@@ -262 +287 @@
     cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
     cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
-    cases (IH current_stack … R2 … EXEC2 CSf)
-    #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' 
+    cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
+    #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R'' 
     %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
-    % [ % [ @(exec_steps_join … EXEC1') @EXEC''
-      | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
-        cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
-        <all_1 assumption
-      ]| assumption
-      ]
+    % [ % [ %
+    [  @(exec_steps_join … EXEC1') @EXEC''
+    |  @CS''
+    ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
+       cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
+       <all_1 assumption
+    ]| assumption
+    ]
   
   | #NCS
@@ -279 +306 @@
       #n' #AFTER1'
       cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
-      cases (IH current_stack … R2 … EXEC2 CSf)
-      #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' 
+      cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
+      #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R'' 
       %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
-      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
-        | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
-          [ assumption
-          | cases prefix' in EXEC1' INV ⊢ %;
-            [ //
-            | * #sx #trx #tl #EXEC1' #INV
-              <(exec_steps_first … EXEC1')
-              whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
-              @INV
-            ]
-          | @OBS'' ] ]
-        | @R''
-        ]
+      % [ % [ %
+      [  @(exec_steps_join … EXEC1') @EXEC''
+      |  @CS''
+      ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+         [ assumption
+         | cases prefix' in EXEC1' INV ⊢ %;
+           [ //
+           | * #sx #trx #tl #EXEC1' #INV
+             <(exec_steps_first … EXEC1')
+             whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
+             @INV
+           ]
+         | @OBS''
+         ]
+      ]| @R''
+      ]
+
     | #CALLRET
       cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
@@ -304 +335 @@
         ]
       ] * #CL
-      cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
-      [2,4: >CL %]
-      #m' * #Etr #AFTER1'
-      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
-      [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
-      | letin next_stack ≝ (tail … current_stack)
-      ]
-      cases (IH next_stack … R2 … EXEC2 CSf)
-      #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' 
-      %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
-      % [1,3: % [1,3: @(exec_steps_join … EXEC1') @EXEC''
-        | destruct cases (exec_steps_S … EXEC1')
-          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
-          destruct >Etrace
-          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
-          [ whd in match (cs_classify ??); >CL % 
-          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
-          | @INV
-          | assumption
-          | @(rel_callee … REL)
+      [ cases (true_or_false_Prop … (pcs_labelled … s2))
+        [ #CS2
+          (* Can we execute another step now, or shall we wait for later? *)
+          cases m in IH EXEC2;
+          [ #_ (* Nope, use extra step to get back into relation *)
+            #EXEC2 whd in EXEC2:(??%%); destruct
+            cases EXTRA_STEP #trx * #sx #EXTRA -EXTRA_STEP
+            cases (exec_steps_S … EXTRA) #NFf * #trx' * #sx' * #tlx * * #Ex #EXTRA_STEP #EX' whd in EX':(??%?); destruct
+            cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 EXTRA_STEP)
+            #m' #AFTER1'
+            cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace #CS2' #AFTER2'
+            cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2 #R3
+            %{1} %{prefix1'} %{s2'}
+            % [ % [ %
+            [  @EXEC1'
+            |  @CS2'
+            ]| destruct cases (exec_steps_S … EXEC1')
+               #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
+               destruct <(append_nil … (?::prefix2)) in ⊢ (???%);
+               @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+               [ whd in match (cs_classify ??); >CL % 
+               | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
+               | @INV1
+               | %
+               | @(rel_callee … REL)
+               ]
+            ]| %{1} %{m'} %{[〈sf,trx'〉]} %{prefix2'} %{sx} %{s3'}
+               cut (all ? (λst.pnormal_state C2 g' (\fst st)) prefix2')
+               [ cases prefix2' in EXEC2' INV2 ⊢ %;
+                  [ //
+                  | * #sp #trp #tlp #EXEC2' #INV2
+                    whd in ⊢ (?%); <(exec_steps_first … EXEC2')
+                    >labelled_normal2 //
+                  ]
+               ] #Np2'
+               % [ % [ % [ % [ %
+               [  @EXTRA
+               |  whd in ⊢ (?%); >labelled_normal1 //
+               ]| @EXEC2'
+               ]| @Np2'
+               ]| #cs <(append_nil … prefix2') <Etrace2
+                  @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+                  [ <normal_state_p @labelled_normal1 //
+                  | @Np2'
+                  | //
+                  ]
+               ]| @R3
+               ]
+            ]
+          (* We can execute the cost label, too. *)
+          | #m1 #IH #EXEC2
+            cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3
+            cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2)
+            #m' #AFTER1'
+            cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2'
+            cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3
+            letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
+            cases (IH m1 ? next_stack … R3 … EXEC3 CSf EXTRA_STEP) [2: // ]
+            #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' 
+            %{(S m' + m'')} %{(prefix1'@prefix2'@prefix'')} %{sf''}
+            % [ % [ %
+            [  @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC''
+            |  @CSf''
+            ]| destruct cases (exec_steps_S … EXEC1')
+               #NF1' * #tr1' * #s2'' * #prefix2'' * * #E #STEP1' #EXEC2''
+               whd in EXEC2'':(??%%);
+               destruct
+               @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+               [ whd in match (cs_classify ??); >CL %
+               | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
+               | %
+               | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+                 [ <normal_state_p @labelled_normal1 @CS2
+                 | cases prefix2' in EXEC2' INV2 ⊢ %;
+                   [ //
+                   | * #sy #try #tly #EXEC2' #INV2
+                     <(exec_steps_first … EXEC2')
+                     whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 //
+                   ]
+                 | assumption
+                 ]
+               | @(rel_callee … REL)
+               ]
+            ]| @R''
+            ]
           ]
-        | destruct cases (exec_steps_S … EXEC1')
-          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
-          destruct >Etrace
-          @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
-          [ whd in match (cs_classify ??); >CL % 
-          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
-          | @INV
-          | assumption
+
+        | #NCS2
+          cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1)
+          [2: >CL % | 3: @notb_Prop @NCS2 ]
+          #m' #AFTER1'
+          cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
+          letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
+          cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
+          #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' 
+          %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
+          % [ % [ %
+          [  @(exec_steps_join … EXEC1') @EXEC''
+          |  @CSf''
+          ]| destruct cases (exec_steps_S … EXEC1')
+             #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
+             destruct
+             @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+             [ whd in match (cs_classify ??); >CL %
+             | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
+             | @INV
+             | assumption
+             | @(rel_callee … REL)
+             ]
+          ]| @R''
           ]
         ]
-      | 2,4: @R''
+
+      | cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %]
+        #m' * #Etr #AFTER1'
+        cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
+        letin next_stack ≝ (tail … current_stack)
+        cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: //]
+        #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' 
+        %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
+        % [ % [ %
+        [  @(exec_steps_join … EXEC1') @EXEC''
+        |  @CSf''
+        ]| destruct cases (exec_steps_S … EXEC1')
+           #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
+           destruct >Etrace
+           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+           [ whd in match (cs_classify ??); >CL %  
+           | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
+           | @INV
+           | assumption
+           ]
+        ]| @R''
+        ]
       ]
     ]
@@ -391 +524 @@
        measurable trace, so the end is no longer in the relation. ☹ *)
     
-* #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
+* #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
 #g #g' #INV #s1 #s1' #depth #callstack #REL
 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
 generalize in match callstack; generalize in match depth; -callstack -depth
-elim m0
-[ (* "fake" base case - we can never have zero steps *)
+@(nat_elim1 m0) *
+[ #_ (* "fake" base case - we can never have zero steps *)
   #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC
   whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct
@@ -409 +542 @@
     cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
     cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
-    cases (IH depth current_stack … R2 … EXEC2 ??)
-    [ (* End must be later, and still a return *)
-      2: destruct cases END *
+    cases (IH m ? depth current_stack … R2 … EXEC2 ??)
+    [ 2: //
+    | (* End must be later, and still a return *)
+      3: destruct cases END *
       [ * #trE * #sE * #E whd in E:(???%); destruct
         #CL cases (pnormal_state_inv … N1) >CL #E destruct
@@ -417 +551 @@
         %{t} %{trE} %{sE} /2/
       ]
-    | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
+    | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
       cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS
     ]
@@ -440 +574 @@
       #n' #AFTER1'
       cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
-      cases (IH depth current_stack … R2 … EXEC2 ??)
-      [ (* End must be later, and still a return *)
-        2: destruct cases END *
+      cases (IH m ? depth current_stack … R2 … EXEC2 ??)
+      [ 2: //
+      | (* End must be later, and still a return *)
+        3: destruct cases END *
         [ * #trE * #sE * #E whd in E:(???%); destruct
           #CL cases (pnormal_state_inv … NORMAL) >CL #E destruct
@@ -448 +583 @@
           %{t} %{trE} %{sE} /2/
         ]
-      | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
+      | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
         cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS
       ]
@@ -484 +619 @@
         cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ]
         #E1 normalize in E1; destruct
-        cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) 
-        [2: >CL %]
+        cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %]
         #m' * #Etr #AFTER1' destruct
         cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2'
@@ -510 +644 @@
            ]
         ]
-      ] * #s2x #tr2 #trace3 #E1 #EXEC2
+      ]
+      (* Not at the end *)
+      * #s2x #tr2 #trace3 #E1 #EXEC2
       cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
       [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
@@ -519 +655 @@
         ]
       ] * #CL
-      cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
-      [2,4: >CL %]
+      
+      [ cases (true_or_false_Prop … (pcs_labelled … s2))
+        [ #CS2
+          (* We can't stop here *)
+          cases m in IH EXEC2;
+          [ #_ #EXEC2 whd in EXEC2:(??%%); destruct ]
+          #m1 #IH #EXEC2
+          cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3
+          cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2)
+          #m' #AFTER1'
+          cases (after_n_exec_steps … AFTER1') #interesting1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2'
+          cases (after_n_exec_steps … AFTER2') #interesting2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3
+          letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
+          letin next_depth ≝ (S depth)
+          cut (pnormal_state C1 g s2) [ @labelled_normal1 assumption ] #N2
+          cases (IH m1 ? next_depth next_stack … R3 … EXEC3 ??)
+          [ 2: //
+          | (* End must be later, and still a return *)
+            3: destruct cases END *
+            [ * #trE * #sE * #E whd in E:(???%); destruct
+            | *: #h1 *
+              [ * #trE * #sE * #E normalize in E:(???%); destruct
+                #CL cases (pnormal_state_inv … N2) >CL #E destruct
+              | #h2 #t * #trE * #sE * #E normalize in E:(???%); destruct #CL
+                 %{t} %{trE} %{sE} /2/
+              ]
+            ]
+          | 4: destruct whd in RETURNS:(?%);
+            whd in match (cs_classify ??) in RETURNS;
+            >CL in RETURNS; whd in ⊢ (?% → ?);
+            cases (pnormal_state_inv … N2) #CL2
+            whd in match (cs_classify ??); >CL2 //
+          ]
+          #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
+          %{(S m' + m'')} %{(interesting1'@interesting2'@interesting'')} %{sf''}
+          % [ % [ %
+          [ @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC''
+          | @ends_at_return_append @ends_at_return_append assumption
+         ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2''
+            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
+            <(rel_classify … REL) >CL whd in ⊢ (?%); whd in INV1:(?(???%));
+            >will_return_aux_normal [2: @INV1 ]
+            >will_return_aux_normal
+            [ //
+            | cases interesting2' in EXEC2' INV2 ⊢ %;
+              [ //
+              | * #s2'' #tr2'' #tl2'' #E2'' <(exec_steps_first … E2'') #TL
+                whd in ⊢ (?%); <normal_state_p >(labelled_normal2 … CS2') @TL
+              ]
+            ]
+         ]| destruct cases (exec_steps_S … EXEC1')
+            #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2''
+            destruct
+            @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+            [ whd in match (cs_classify ??); >CL % 
+            | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
+            | @INV1
+            | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+              (* Repeats bits of proof above, could compress *)
+              [ <normal_state_p @labelled_normal1 @CS2
+              | cases interesting2' in EXEC2' INV2 ⊢ %;
+                [ //
+                | * #sy #try #tly #EXEC2' #INV2
+                  <(exec_steps_first … EXEC2')
+                  whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 //
+                ]
+              | assumption
+              ]
+            | @(rel_callee … REL)
+            ]
+          ]
+
+        | #NCS2
+          cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1)
+          [2: >CL % | 3: @notb_Prop @NCS2 ]
+          #m' #AFTER1'
+          cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
+          letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
+          letin next_depth ≝ (S depth)
+          cases (IH m ? next_depth next_stack … R2 … EXEC2 ??)
+          [ 2: //
+          | (* End must be later, and still a return *)
+            3: destruct cases END *
+            [ * #trE * #sE * #E whd in E:(???%); destruct
+            | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
+              %{t} %{trE} %{sE} /2/
+            ]
+          | 4: destruct whd in RETURNS:(?%);
+               whd in match (cs_classify ??) in RETURNS;
+               >CL in RETURNS; //
+          ]
+          #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
+          %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''}
+          % [ % [ %
+          [ @(exec_steps_join … EXEC1') @EXEC''
+          | @ends_at_return_append assumption
+         ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
+            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
+            <(rel_classify … REL) >CL whd in ⊢ (?%);
+            >will_return_aux_normal //
+         ]| destruct cases (exec_steps_S … EXEC1')
+            #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
+            destruct
+            @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+            [ whd in match (cs_classify ??); >CL % 
+            | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
+            | @INV
+            | assumption
+            | @(rel_callee … REL)
+            ]
+          ]
+       ]
+     |
+
+      cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %]
       #m' * #Etr #AFTER1'
       cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
-      [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
-        letin next_depth ≝ (S depth)
-      | letin next_stack ≝ (tail … current_stack)
-        letin next_depth ≝ (pred depth)
-      ]
-      cases (IH next_depth next_stack … R2 … EXEC2 ??)
-      [(* End must be later, and still a return *)
-        2,5: destruct cases END *
-        [1,3: * #trE * #sE * #E whd in E:(???%); destruct
-        |*: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
+      letin next_stack ≝ (tail … current_stack)
+      letin next_depth ≝ (pred depth)
+      cases (IH m ? next_depth next_stack … R2 … EXEC2 ??)
+      [ 2: //
+      | (* End must be later, and still a return *)
+        3: destruct cases END *
+        [ * #trE * #sE * #E whd in E:(???%); destruct
+        | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
           %{t} %{trE} %{sE} /2/
         ]
-      | 3: destruct whd in RETURNS:(?%);
-           whd in match (cs_classify ??) in RETURNS;
-           >CL in RETURNS; //
-      | 6: destruct whd in RETURNS:(?%);
+      | 4: destruct whd in RETURNS:(?%);
            whd in match (cs_classify ??) in RETURNS;
            >CL in RETURNS; whd in ⊢ (?% → ?);
@@ -546 +790 @@
       #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
       %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''}
-      % [1,3: % [1,3: %
-      [1,3: @(exec_steps_join … EXEC1') @EXEC''
-      |2,4: @ends_at_return_append assumption
-      ]|    cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
-            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
-            <(rel_classify … REL) >CL whd in ⊢ (?%);
-            >will_return_aux_normal //
-       |    cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
-            destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %;
-            <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%);
-            whd in match next_depth in RETURNS'';
-            cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_
-            whd in ⊢ (?%);
-            >will_return_aux_normal [ @RETURNS'' | @INV ]
-      ]|  destruct cases (exec_steps_S … EXEC1')
-          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
-          destruct >Etrace
-          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
-          [ whd in match (cs_classify ??); >CL % 
-          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
-          | @INV
-          | assumption
-          | @(rel_callee … REL)
-          ]
-       |  destruct cases (exec_steps_S … EXEC1')
-          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
-          destruct >Etrace
-          @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
-          [ whd in match (cs_classify ??); >CL % 
-          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
-          | @INV
-          | assumption
-          ]
-       ]
+      % [ % [ %
+      [ @(exec_steps_join … EXEC1') @EXEC''
+      | @ends_at_return_append assumption
+     ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
+        destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %;
+        <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%);
+        whd in match next_depth in RETURNS'';
+        cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_
+        whd in ⊢ (?%);
+        >will_return_aux_normal [ @RETURNS'' | @INV ]
+     ]| destruct cases (exec_steps_S … EXEC1')
+        #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
+        destruct >Etrace
+        @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
+        [ whd in match (cs_classify ??); >CL % 
+        | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
+        | @INV
+        | assumption
+        ]
     ]
   ]
@@ -610 +839 @@
   %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ % | <(exec_steps_first … EXEC) @CS ] | @CL ]
 ] qed.
+
+(* TODO: move*)
+lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.
+#x0 elim x0
+[ #y %{y} %2 %
+| #x #IH *
+  [ %{(S x)} %1 %
+  | #y cases (IH y) #z *
+    [ #H %{z} %1 >H //
+    | #H %{z} %2 >H //
+    ]
+  ]
+] qed.
+
+lemma all_append : ∀A,p,l1,l2.
+  all A p (l1@l2) →
+  all A p l1 ∧ all A p l2.
+#A #p #l1 elim l1
+[ //
+| #h #t #IH #l2
+  whd in ⊢ (?% → ?(?%?));
+  cases (p h) //
+  @IH
+] qed.
+
+
+lemma ends_at_return_normal : ∀C,g,t1,t2.
+  ends_at_return C g (t1@t2) →
+  all … (λst. pnormal_state C g (\fst st)) t1 →
+  ends_at_return C g t2.
+#C #g #t1 elim t1
+[ //
+| * #s #tr #tl #IH #t2 * #tr1 * #tr2 * #s2 * cases tr1
+  [ #E normalize in E; destruct #CL whd in ⊢ (?% → ?);
+    lapply (pnormal_state_inv … s2)
+    cases (pnormal_state … s2)
+    [ #H cases (H I) >CL #E' destruct
+    | #_ *
+    ]
+  | * #s' #tr' #tl' #E whd in E:(??%%); destruct #CL #ALL
+    @IH
+    [ %{tl'} %{tr2} %{s2} >e0 % //
+    | whd in ALL:(?%); cases (pnormal_state … s') in ALL;
+      [ // | * ]
+    ]
+  ]
+] qed.
+
 
 
@@ -634 +911 @@
 
 cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1)
-#m' * #prefix' * #s1' * * #EXEC0' #OBS0 #R1
-
-cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] prefix)) R1 … EXEC1 ENDS RETURNS)
+(* Need an extra step from the source in case we end up at a label after a
+   function call. *)
+[2: cases n in EXEC1;
+  [ #E whd in E:(??%?); destruct cases RETURNS
+  | #n1 #EXEC1 cases (exec_steps_split 1 … EXEC1) #ex * #ex2 * #sx * * #EX1 #_ #_
+    %{ex} %{sx} @EX1
+  ]
+]
+#m' * #prefix' * #s1' * * * #EXEC0' #CS1' #OBS0
+* #r * #r' * #interesting1 * #interesting1' * #sr * #sr' * * * * * #EXECr #Nr #EXECr' #Nr' #OBS1 #R1
+
+(* Show that the extra r steps we need to get back into the relation are a
+   prefix of the measurable subtrace. *)
+cut (∃nr,interesting2. n = r + nr ∧
+  exec_steps nr … C g sr = OK … 〈interesting2,s2〉 ∧
+  interesting = interesting1 @ interesting2)
+[ cases (plus_split n r) #nr *
+  [ #En %{nr} >En in EXEC1; #EXEC1
+    cases (exec_steps_split … EXEC1)
+    #interesting1x * #interesting2 * #srx * * #EXEC1x #EXECrx #E
+    >EXECr in EXEC1x; #E1x destruct
+    %{interesting2} % [ % [ % | assumption ] | % ]
+  | #En @⊥
+    >En in EXECr; #EXECr cases (exec_steps_split … EXECr)
+    #ex1 * #ex2 * #sx * * #EX1 #EXx #E >E in Nr; >EXEC1 in EX1; #E' destruct
+    #Nr cases (andb_Prop_true … (all_append … Nr)) #N1 #N2
+    cases ENDS #le * #tre * #se * #Ee #CLe destruct
+    cases (andb_Prop_true … (all_append … N1)) #_ whd in ⊢ (?% → ?);
+    lapply (pnormal_state_inv … se) cases (pnormal_state … se)
+    [ #H cases (H I) >CLe #E destruct
+    | #_ *
+    ]
+  ]
+]
+* #nr * #interesting2 * * #En #EXECr2 #Ei destruct
+
+whd in RETURNS:(?%);
+>will_return_aux_normal in RETURNS;
+[2: @Nr] #RETURNS
+
+lapply (ends_at_return_normal … ENDS Nr)
+#ENDS2
+
+cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] (prefix@interesting1))) R1 … EXECr2 ENDS2 RETURNS)
 #n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS'
 
-cut (intensional_trace_of_trace C [ ] (prefix@interesting) =
-     intensional_trace_of_trace C' [ ] (prefix'@interesting'))
-[ >int_trace_append' >int_trace_append'
+cut (intensional_trace_of_trace C [ ] (prefix@interesting1) =
+     intensional_trace_of_trace C' [ ] (prefix'@interesting1'))
+[ >int_trace_append' >(int_trace_append' C')
   <OBS0 @breakup_pair @breakup_pair @breakup_pair @breakup_pair
+  <OBS1 %
+] #OBS01 
+
+cut (intensional_trace_of_trace C [ ] (prefix@interesting1@interesting2) =
+     intensional_trace_of_trace C' [ ] (prefix'@interesting1'@interesting'))
+[ <associative_append <associative_append
+  >int_trace_append' >(int_trace_append' C')
+  <OBS01
+  @breakup_pair @breakup_pair @breakup_pair @breakup_pair
   <OBS' %
 ] #Eobs
 
-%{m'} %{n'} %
-[ %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'}
+lapply (exec_steps_join … EXECr' EXEC1')
+#EXECr''
+
+%{m'} %{(r' + n')} %
+[ %{s0'} %{prefix'} %{s1'} %{(interesting1'@interesting')} %{s2'}
   % [ % [ % [ % [ %
   [  assumption
   |  assumption
   ]| assumption
-  ]| @(build_label_to_ret … EXEC1' ? ENDS')
+  ]| @(build_label_to_ret … EXECr'' ? (ends_at_return_append … ENDS'))
      [ #s #CS @(ms_labelled_normal_2 … CS)
-     | <(ms_rel_labelled … R1) @CS1
+     | <(ms_rel_labelled … R1) @CS1'
      ]
-  ]| @RETURNS'
+  ]| whd in ⊢ (?%); >will_return_aux_normal [2: @Nr'] @RETURNS'
   ]| <Eobs @MAX
   ]
 | >INIT >INIT'
   whd in ⊢ (??%%); >EXEC0 >EXEC0'
-  whd in ⊢ (??%%); >EXEC1 >EXEC1'
-  whd in ⊢ (??%%); <OBS0 cases (intensional_trace_of_trace C [ ] prefix) in OBS' ⊢ %;
-  #cs #prefixtr #OBS' whd in ⊢ (??%%); >OBS' % 
+  whd in ⊢ (??%%); >EXEC1 >EXECr''
+  whd in ⊢ (??%%); >int_trace_append' in OBS'; <OBS0
+  cases (intensional_trace_of_trace C [ ] prefix)
+  #cs #prefixtr whd in ⊢ (??(??(???%)?)(??(???%)?) → ??%%);
+  >int_trace_append' >int_trace_append' <OBS1
+  @breakup_pair @breakup_pair @breakup_pair @breakup_pair @breakup_pair
+  #OBS' <OBS' % 
 ] qed.
-*)