(* Show that measurable subtraces are preserved in the front-end. *)

include "common/Measurable.ma".

definition pnormal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝
λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].

lemma pnormal_state_inv : ∀C,g,s.
  pnormal_state C g s →
  pcs_classify C g s = cl_other ∨ pcs_classify C g s = cl_jump.
#C #g #s whd in ⊢ (?% → ?); cases (pcs_classify C g s) /2/ *
qed.

lemma normal_state_p : ∀C,g,s.
  pnormal_state C g s = normal_state (pcs_to_cs C g) s.
//
qed.

(* A record giving the languages and simulation results necessary to show that
   measurability is preserved.
   
   Note: as we're interested in measurable subtraces, we don't have to worry
   about the execution "going wrong."
    *)

record meas_sim : Type[2] ≝ {
  ms_C1 : preclassified_system;
  ms_C2 : preclassified_system;
  ms_compiled : program … ms_C1 → program … ms_C2 → Prop;
  ms_inv : ? → ? → Type[0];
  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
  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;
  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;
  (* FIXME: this is almost certainly too strong if the step from s1 "disappears" in s2. *)
  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;
  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';

  (* These hold in (at least) the languages of interest for measurable subtraces *)
  ms_labelled_normal_1 : ∀g1,s1. pcs_labelled ms_C1 g1 s1 → pnormal_state ms_C1 g1 s1;
  ms_labelled_normal_2 : ∀g2,s2. pcs_labelled ms_C2 g2 s2 → pnormal_state ms_C2 g2 s2;
  ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall;

  (* Measure on source states; only needed for showing preservation of
     non-termination.  Should not be necessary for showing that the measurable
     traces are preserved. *)
  ms_measure1 : ∀g1. state … ms_C1 g1 → nat;

  sim_normal :
    ∀g1,g2.
    ∀INV:ms_inv g1 g2.
    ∀s1,s1'.
    ms_rel g1 g2 INV s1 s1' →
    pnormal_state ms_C1 g1 s1 →
    ¬ pcs_labelled ms_C1 g1 s1 →
    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
    ∃m. after_n_steps 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' ∧
      (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))
    );
  (* 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.
    ∀s1,s1'.
    ms_rel g1 g2 INV s1 s1' →
    pcs_classify ms_C1 g1 s1 = cl_call →
    ¬ pcs_labelled ms_C1 g1 s1 →
    ∀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 :
    ∀g1,g2.
    ∀INV:ms_inv g1 g2.
    ∀s1,s1'.
    ms_rel g1 g2 INV s1 s1' →
    pcs_classify ms_C1 g1 s1 = cl_return →
    ¬ 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. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
    ∃m. tr = E0 ∧
      after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
      E0 = tr' ∧
      ms_rel g1 g2 INV s2 s2'
    );
  sim_cost :
    ∀g1,g2.
    ∀INV:ms_inv g1 g2.
    ∀s1,s1',s2,tr.
    ms_rel g1 g2 INV s1 s1' →
    pcs_labelled ms_C1 g1 s1 →
    step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
      tr = tr' ∧
      ms_rel g1 g2 INV s2 s2'
    );
  sim_init :
    ∀p1,p2,s.
    ms_compiled p1 p2 →
    make_initial_state ?? ms_C1 p1 = OK ? s →
    ∃s'. make_initial_state ?? ms_C2 p2 = OK ? s' ∧
    ∃INV. ms_rel ?? INV s s'
}.


(*
lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
  pnormal_state C g s1 →
  stack_after (pcs_to_cs C g stack) current trace = current.
#C #g #s1 #trace #s2 #stack #current #EXEC
cases (exec_steps_S … EXEC)
#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
#N
whd in ⊢ (??%?); generalize in match (cs_stack ??);
whd in match (cs_classify ??);
cases (pnormal_state_inv … N)
#CL >CL #f %
qed.

lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
  pnormal_state C g s1 →
  max_stack (pcs_to_cs C g stack) current trace = current.
#C #g #s1 #trace #s2 #stack #current #EXEC
cases (exec_steps_S … EXEC)
#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
#N
whd in ⊢ (??%?); generalize in match (cs_stack ??);
whd in match (cs_classify ??);
cases (pnormal_state_inv … N)
#CL >CL #f %
qed.

lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf.
  exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
  ¬pcs_labelled C g s1 →
  pcs_labelled C g sf →
  ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) →
  ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P →
  ∃p,trace1,s2,trace2.
    exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
    P (gather_trace … trace1) s2 ∧
    exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧
    m = n + p.
#C #g #m elim m -m
[ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct
  #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS
| #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H *
  [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ % | @AFTER ] | @EXEC1 ]| % ]
  | #n #P #AFTER
    cases (exec_steps_S … EXEC1)
    #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2
    cases (after_1_of_n_steps … AFTER)
    #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2
    >STEP in STEP'; #E destruct
    cases (IH … EXEC2 … AFTER2)
    [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E
      %{p} % [2: %{s2} %{trace2} % [ % [ %
       [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); % | skip ]
      | @P2 ]| @EXEC2 ]| >E % ] | skip ]
    | @H assumption
    | assumption
    | assumption
    ]
  ]
] qed.

lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf.
  exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
  ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P →
  ∃trace1,s2,trace2.
    exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
    P (gather_trace … trace1) s2 ∧
    exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉.
#C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1
cases (exec_steps_S … EXEC1)
#NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2
%{[〈s1,tr〉]} %{s2} %{tl} % [ %
 [ whd in ⊢ (??%?); >NF1 >STEP % | whd in AFTER1; >NF1 in AFTER1; >STEP normalize
 cases (inv s2) // * ]| // ]
qed.
*)
(* XXX do I need to do the max_stack reasoning here?  perhaps just by preserving
   observables? *)

lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'.
  exec_steps 1 O I fx g s = OK ? 〈trace,s'〉 →
  ∃tr. trace = [〈s,tr〉].
#O #I #fx #g #s #trace #s' #EXEC
cases (exec_steps_S … EXEC)
#nf * #tr * #s'' * #tl * * #E1 #STEP #EXEC' whd in EXEC':(??%%); destruct
%{tr} %
qed.

lemma all_1 : ∀A.∀P:A → bool.∀x.
  P x = all A P [x].
#A #P #x whd in ⊢ (???%); cases (P x) //
qed.



lemma prefix_preserved :
  ∀MS:meas_sim.
  ∀g,g'.
  ∀INV:ms_inv MS g g'.
  ∀s1,s1'.
  ms_rel MS g g' INV s1 s1' →

  ∀m,prefix,sf.
  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
  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' ∧


    (* 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 *)
@(nat_elim1 m0) *
[ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf #_
  %{0} %{[]} %{s1'}
  % [ % [ % [ // | <(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))
  [ #CS
    lapply (sim_cost … REL CS STEP1)
    #AFTER1'
    cases (after_n_exec_steps … AFTER1')
    #prefix' * #s2' * * #EXEC1' #_ * #Etrace #R2
    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 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''
    |  @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
    cases (true_or_false_Prop (pnormal_state C1 g s1))
    [ #NORMAL
      (* XXX should set things up so that notb_Prop isn't needed *)
      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
      #n' #AFTER1'
      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
      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''
      |  @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)
      [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
        lapply (no_tailcalls … s1)
        cases (pcs_classify … s1) in CALLRET ⊢ %;
        [ 1,3: #_ #_ /2/
        | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??))
        ]
      ] * #CL
      [ 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''
            ]
          ]

        | #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''
          ]
        ]

      | 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''
        ]
      ]
    ]
  ]
] qed.

definition ends_at_return : ∀C:preclassified_system. ∀g. list (state … C g × trace) → Prop ≝
λC,g,x. ∃x',tr2,s2. x = x'@[〈s2,tr2〉] ∧ pcs_classify C g s2 = cl_return.

lemma ends_at_return_append : ∀C,g,t1,t2.
  ends_at_return C g t2 →
  ends_at_return C g (t1@t2).
#C #g #t1 #t2 * #x * #tr * #s * #E >E #CL
%{(t1@x)} %{tr} %{s} % /2/
qed.

lemma will_return_aux_normal : ∀C,depth,t1,t2.
  all … (λstr. normal_state C (\fst str)) t1 →
  will_return_aux C depth (t1@t2) = will_return_aux C depth t2.
#C #depth #t1 #t2 elim t1
[ #_ %
| * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl
  whd in ⊢ (??%?);
  cases (normal_state_inv … N1) #CL >CL
  @IH @Ntl
] qed.

lemma measurable_subtrace_preserved :
  ∀MS:meas_sim.
  ∀g,g'.
  ∀INV:ms_inv MS g g'.
  ∀s1,s1',depth,callstack.
  ms_rel MS g g' INV s1 s1' →
  
  let C ≝ pcs_to_cs (ms_C1 MS) g in
  let C' ≝ pcs_to_cs (ms_C2 MS) g' in

  ∀m,interesting,sf.
  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈interesting,sf〉 →
  ends_at_return (ms_C1 MS) g interesting →
  will_return_aux C depth interesting →

  ∃m',interesting',sf'.
    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈interesting',sf'〉 ∧
    (* The obs trace equality almost gives this, but doesn't ensure the
       cost/return are exactly at the ends *)
    ends_at_return (ms_C2 MS) g' interesting' ∧
    bool_to_Prop (will_return_aux C' depth interesting') ∧
    
    intensional_trace_of_trace C callstack interesting = intensional_trace_of_trace C' callstack interesting'.
    (* Seems a shame to leave this out "∧ ms_rel MS g g' INV sf sf'", but it
       isn't true if the final return step is expanded into the caller, e.g.,
       in Clight → Cminor we added an instruction to callers if they need to
       store the result in memory.  This extra step doesn't form part of the
       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_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
@(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
| #m #IH #depth #current_stack #s1 #s1' #REL #prefix #sf #EXEC #END #RETURNS
  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
  cases (true_or_false_Prop … (pcs_labelled … s1))
  [ #CS
    lapply (sim_cost … REL CS STEP1)
    #AFTER1'
    cases (after_n_exec_steps … AFTER1')
    #interesting' * #s2' * * #EXEC1' #_ * #Etrace #R2
    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 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
      | #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;
      cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS
    ]
    #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
    %{(1+m'')} %{(interesting'@interesting'')} %{sf''}
    % [ % [ %
    [  @(exec_steps_join … EXEC1') @EXEC''
    |  @ends_at_return_append assumption
    ]| cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
       whd in ⊢ (?%); whd in match (cs_classify ??); <(rel_classify … REL)
       cases (pnormal_state_inv … N1) #CL >CL @RETURNS''
    ]| 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
    ]
  
  | #NCS
    cases (true_or_false_Prop (pnormal_state C1 g s1))
    [ #NORMAL
      (* XXX should set things up so that notb_Prop isn't needed *)
      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
      #n' #AFTER1'
      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
      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
        | #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;
        cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS
      ]
      #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
      %{(n'+m'')} %{(interesting'@interesting'')} %{sf''}
      % [ % [ %
      [  @(exec_steps_join … EXEC1') @EXEC''
      |  @ends_at_return_append assumption
      ]| >will_return_aux_normal
         [ @RETURNS''
         | cases n' in EXEC1';
           [ #EXEC >(lenght_to_nil (*sic*) … interesting') // >(exec_steps_length … EXEC) %
           | #n'' #EXEC cases (exec_steps_S … EXEC)
             #_ * #tr1' * #s2' * #tl * * #E #STEP1' #EXEC2' destruct
             @andb_Prop [ <normal_state_p <(rel_normal … REL) @NORMAL | @INV ]
           ]
         ]
      ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
          [ assumption
          | cases interesting' in EXEC1' INV ⊢ %;
            [ //
            | * #sx #trx #tl #EXEC1' #INV
              <(exec_steps_first … EXEC1')
              whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
              @INV
            ]
          | @OBS''
          ]
      ]

    | #CALLRET
      cases trace2 in E1 EXEC2;
        (* For a return we might hit the end - this is the real base case. *)
      [ #E1 #EXEC2 destruct cases END #tl * #tr * #s1x * #E1 #CL
        cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ]
        #E1 normalize in E1; destruct
        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'
        cut (tr1' = E0) [
          cases (after_n_exec_steps … AFTER2') #trace * #sf' * * #_ #_ * #H #_
          cases (Eapp_E0_inv … (sym_eq … H)) //
        ] #E1 destruct
        %{1} %{[〈s1',E0〉]} %{s2'}
        % [ % [ %
        [  whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); %
        |  %{[ ]} %{E0} %{s1'} %{(refl ??)} <(rel_classify … REL) assumption
        ]| whd in RETURNS:(?%) ⊢ (?%);
           whd in match (cs_classify ??) in RETURNS;
           whd in match (cs_classify ??); <(rel_classify … REL)
           >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%);
           cases depth [ // | #d * ]
        ]| <(append_nil … [〈s1',E0〉])
           change with (gather_trace … [〈s1',E0〉]) in match E0 in ⊢ (??%?);
           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
           [ @CL
           | whd in ⊢ (??%?); <(rel_classify … REL) @CL
           | %
           | %
           ]
        ]
      ]
      (* 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;
        lapply (no_tailcalls … s1)
        cases (pcs_classify … s1) in CALLRET ⊢ %;
        [ 1,3: #_ #_ /2/
        | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??))
        ]
      ] * #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 ≝ (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/
        ]
      | 4: destruct whd in RETURNS:(?%);
           whd in match (cs_classify ??) in RETURNS;
           >CL in RETURNS; whd in ⊢ (?% → ?);
           whd in match next_depth; cases depth
           [ * | #d' // ]
      ]
      #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 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
        ]
    ]
  ]
] qed.

lemma label_to_ret_inv : ∀C,m,g,s,trace,s'.
  exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 →
  trace_is_label_to_return (pcs_to_cs … C g) trace →
  bool_to_Prop (pcs_labelled C g s) ∧ ends_at_return C g trace.
#C #m #g #s #trace #s' #EXEC
* #tr * #s1 * #tl * #tr2 * #s2 * * #E #CS #CL destruct
>(exec_steps_first … EXEC)
%
[ @CS
| %{(〈s1,tr〉::tl)} %{tr2} %{s2} %{(refl ??)} @CL
] qed.

lemma build_label_to_ret : ∀C,m,g,s,trace,s'.
  (∀s. pcs_labelled C g s → pnormal_state C g s) →
  exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 →
  pcs_labelled C g s →
  ends_at_return C g trace →
  trace_is_label_to_return (pcs_to_cs … C g) trace.
#C #m #g #s #trace #s' #LABELLED_NORMAL #EXEC #CS * #trace' * #tr2 * #s2 * #E #CL
destruct
cases trace' in EXEC ⊢ %;
[ #EXEC >(exec_steps_first … EXEC) in CS; #CS
  cases (pnormal_state_inv … (LABELLED_NORMAL … CS)) >CL #E destruct
| * #s1 #tr1 #trace1 #EXEC
  %{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.



theorem measured_subtrace_preserved :
  ∀MS:meas_sim.
  ∀p1,p2,m,n,stack_cost,max.
  ms_compiled MS p1 p2 →
  measurable (ms_C1 MS) p1 m n stack_cost max →
  ∃m',n'.
    measurable (ms_C2 MS) p2 m' n' stack_cost max ∧
    observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'.
#MS #p1 #p2 #m #n #stack_cost #max #compiled
* #s0 * #prefix * #s1 * #interesting * #s2
whd in ⊢ (? → ??(λ_.??(λ_.(?%(??%%)))));
letin g ≝ (make_global … (pcs_exec … ) p1)
letin g' ≝ (make_global … (pcs_exec … ) p2)
letin C ≝ (pcs_to_cs ? g)
letin C' ≝ (pcs_to_cs ? g')
* * * * * #INIT #EXEC0 #EXEC1 #TLR #RETURNS #MAX

cases (sim_init … compiled INIT) #s0' * #INIT' * #INV #R0
cases (label_to_ret_inv … EXEC1 TLR)
#CS1 #ENDS

cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1)
(* 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@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

lapply (exec_steps_join … EXECr' EXEC1')
#EXECr''

%{m'} %{(r' + n')} %
[ %{s0'} %{prefix'} %{s1'} %{(interesting1'@interesting')} %{s2'}
  % [ % [ % [ % [ %
  [  assumption
  |  assumption
  ]| assumption
  ]| @(build_label_to_ret … EXECr'' ? (ends_at_return_append … ENDS'))
     [ #s #CS @(ms_labelled_normal_2 … CS)
     | <(ms_rel_labelled … R1) @CS1'
     ]
  ]| whd in ⊢ (?%); >will_return_aux_normal [2: @Nr'] @RETURNS'
  ]| <Eobs @MAX
  ]
| >INIT >INIT'
  whd in ⊢ (??%%); >EXEC0 >EXEC0'
  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.