source: src/common/FEMeasurable.ma @ 3081

Last change on this file since 3081 was 3081, checked in by campbell, 7 years ago

Tidy up recent work a little.

File size: 39.6 KB
Line 
1(* Show that measurable subtraces are preserved in the front-end. *)
2
3include "common/Measurable.ma".
4
5definition pnormal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝
6λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
7
8lemma pnormal_state_inv : ∀C,g,s.
9  pnormal_state C g s →
10  pcs_classify C g s = cl_other ∨ pcs_classify C g s = cl_jump.
11#C #g #s whd in ⊢ (?% → ?); cases (pcs_classify C g s) /2/ *
12qed.
13
14lemma normal_state_p : ∀C,g,s.
15  pnormal_state C g s = normal_state (pcs_to_cs C g) s.
16//
17qed.
18
19(* A record giving the languages and simulation results necessary to show that
20   measurability is preserved.
21   
22   Note: as we're interested in measurable subtraces, we don't have to worry
23   about the execution "going wrong."
24   
25   For call and return states we only allow the addition of extra steps *after*
26   the corresponding call or return state (i.e., the simulation must always
27   start with it).  This is true in the front-end: Callstate and Returnstate
28   are the second half of calls and returns, the first is the instruction for
29   the call or return which is translated as a "normal" step, where any extra
30   instructions for before the action are added.
31    *)
32
33record meas_sim : Type[2] ≝ {
34  ms_C1 : preclassified_system;
35  ms_C2 : preclassified_system;
36  ms_compiled : program … ms_C1 → program … ms_C2 → Prop;
37  ms_inv : ? → ? → Type[0];
38  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
39  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;
40  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;
41  (* It's tempting to have a general result that states in the relation always
42     have the same classification, but this may not be true when the step for
43     s1 "disappears" in s2.  The best we can do is match calls, returns and
44     "normal" steps (above), because while we may switch cl_other and cl_jump,
45     nothing ever collapses into a cl_call or cl_return because they are always
46     preceeded by the corresponding instruction. *)
47  ms_rel_classify_call : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = cl_call → pcs_classify ms_C2 g2 s2 = cl_call;
48  ms_rel_classify_return : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = cl_return → pcs_classify ms_C2 g2 s2 = cl_return;
49  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';
50
51  (* These hold in (at least) the languages of interest for measurable subtraces *)
52  ms_labelled_normal_1 : ∀g1,s1. pcs_labelled ms_C1 g1 s1 → pnormal_state ms_C1 g1 s1;
53  ms_labelled_normal_2 : ∀g2,s2. pcs_labelled ms_C2 g2 s2 → pnormal_state ms_C2 g2 s2;
54  ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall;
55
56  (* Measure on source states; only needed for showing preservation of
57     non-termination.  Should not be necessary for showing that the measurable
58     traces are preserved.
59     
60     Commented out because we're not using it for now.
61  ms_measure1 : ∀g1. state … ms_C1 g1 → nat;
62  *)
63
64  sim_normal :
65    ∀g1,g2.
66    ∀INV:ms_inv g1 g2.
67    ∀s1,s1'.
68    ms_rel g1 g2 INV s1 s1' →
69    pnormal_state ms_C1 g1 s1 →
70    ¬ pcs_labelled ms_C1 g1 s1 →
71    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
72    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
73      tr = tr' ∧
74      ms_rel g1 g2 INV s2 s2' (*∧
75      (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))*)
76    );
77  (* Naughty code without a cost label will end up being rejected, but we don't
78     have local information about that. *)
79  sim_call_nolabel :
80    ∀g1,g2.
81    ∀INV:ms_inv g1 g2.
82    ∀s1,s1'.
83    ms_rel g1 g2 INV s1 s1' →
84    pcs_classify ms_C1 g1 s1 = cl_call →
85    ¬ pcs_labelled ms_C1 g1 s1 →
86    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
87    ¬ pcs_labelled ms_C1 g1 s2 →
88    ∃m.
89      after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
90      tr = tr' ∧
91      ms_rel g1 g2 INV s2 s2'
92    );
93  (* Note that extra steps are introduced in the front-end to perform variable
94     saves on entry.  If there's a cost label (and there ought to be!) then we
95     move it forward, so have to include it in the simulation.  Unfortunately
96     that's a little messy. *)
97  sim_call_label :
98    ∀g1,g2.
99    ∀INV:ms_inv g1 g2.
100    ∀s1,s1'.
101    ms_rel g1 g2 INV s1 s1' →
102    pcs_classify ms_C1 g1 s1 = cl_call →
103    ¬ pcs_labelled ms_C1 g1 s1 →
104    ∀s2,tr2,s3,tr3.
105    step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr2,s2〉 →
106    pcs_labelled ms_C1 g1 s2 →
107    step … (pcs_exec ms_C1) g1 s2 = Value … 〈tr3,s3〉 →
108    ∃m.
109      after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
110        tr2 = tr' ∧
111        bool_to_Prop (pcs_labelled ms_C2 g2 s2') ∧
112        (after_n_steps m … (pcs_exec ms_C2) g2 s2' (λs.pnormal_state ms_C2 g2 s) (λtr'',s3'.
113         tr'' = tr3 ∧
114         ms_rel g1 g2 INV s3 s3'))
115    );
116  sim_return :
117    ∀g1,g2.
118    ∀INV:ms_inv g1 g2.
119    ∀s1,s1'.
120    ms_rel g1 g2 INV s1 s1' →
121    pcs_classify ms_C1 g1 s1 = cl_return →
122    ¬ pcs_labelled ms_C1 g1 s1 →
123    (* NB: calls and returns don't emit timing cost labels; otherwise we would
124       have to worry about whether the cost labels seen at the final return of
125       the measured trace might appear in the target in subsequent steps that
126       are *after* the new measurable subtrace.  Also note that extra steps are
127       introduced in the front-end: to perform variable saves on entry and to
128       write back the result *after* exit.  The latter do not get included in
129       the measurable subtrace because it stops at the return, and they are the
130       caller's responsibility. *)
131    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
132    ∃m. tr = E0 ∧
133      after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
134      E0 = tr' ∧
135      ms_rel g1 g2 INV s2 s2'
136    );
137  sim_cost :
138    ∀g1,g2.
139    ∀INV:ms_inv g1 g2.
140    ∀s1,s1',s2,tr.
141    ms_rel g1 g2 INV s1 s1' →
142    pcs_labelled ms_C1 g1 s1 →
143    step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
144    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
145      tr = tr' ∧
146      ms_rel g1 g2 INV s2 s2'
147    );
148  sim_init :
149    ∀p1,p2,s.
150    ms_compiled p1 p2 →
151    make_initial_state ?? ms_C1 p1 = OK ? s →
152    ∃s'. make_initial_state ?? ms_C2 p2 = OK ? s' ∧
153    ∃INV. ms_rel ?? INV s s'
154}.
155
156
157
158lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'.
159  exec_steps 1 O I fx g s = OK ? 〈trace,s'〉 →
160  ∃tr. trace = [〈s,tr〉].
161#O #I #fx #g #s #trace #s' #EXEC
162cases (exec_steps_S … EXEC)
163#nf * #tr * #s'' * #tl * * #E1 #STEP #EXEC' whd in EXEC':(??%%); destruct
164%{tr} %
165qed.
166
167lemma all_1 : ∀A.∀P:A → bool.∀x.
168  P x = all A P [x].
169#A #P #x whd in ⊢ (???%); cases (P x) //
170qed.
171
172(* First show that the trace up to the start of the measurable subtrace (i.e.,
173   the prefix of the execution) is preserved using the simulation results in
174   the meas_sim record.  Note that this doesn't end cleanly - the first states
175   in the measurable subtrace may not be in the simulation relation, see the
176   comment below. *)
177
178lemma prefix_preserved :
179  ∀MS:meas_sim.
180  ∀g,g'.
181  ∀INV:ms_inv MS g g'.
182  ∀s1,s1'.
183  ms_rel MS g g' INV s1 s1' →
184
185  ∀m,prefix,sf.
186  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
187  pcs_labelled (ms_C1 MS) g sf →
188
189  (* Needed to ensure we can get back into the relation after a call *)
190  (∃ex,sx. exec_steps 1 … (pcs_exec … (ms_C1 MS)) g sf = OK ? 〈ex,sx〉) →
191
192  ∃m',prefix',sf'.
193    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
194    bool_to_Prop (pcs_labelled (ms_C2 MS) g' sf') ∧
195    intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧
196
197
198    (* We may need to make extra steps to get back into the relation.  In
199       particular, the Clight to Cminor stage adds stores to the stack after
200       the function call, but must preserve the position of the cost label at
201       the head of the function, so we may need to move past these stores. *)
202    ∃r,r',ex,ex',sr,sr'.
203      exec_steps r … (pcs_exec … (ms_C1 MS)) g sf = OK … 〈ex,sr〉 ∧
204      bool_to_Prop (all … (λst.pnormal_state (ms_C1 MS) g (\fst st)) ex) ∧
205      exec_steps r' … (pcs_exec … (ms_C2 MS)) g' sf' = OK … 〈ex',sr'〉 ∧
206      bool_to_Prop (all … (λst.pnormal_state (ms_C2 MS) g' (\fst st)) ex') ∧
207      (∀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') ∧
208      ms_rel MS g g' INV sr sr'.
209
210* #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls (*#measure1*) #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
211#g #g' #INV #s1 #s1' #REL
212#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
213generalize in match [ ]; (* current call stack *)
214@(nat_elim1 m0) *
215[ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf #_
216  %{0} %{[]} %{s1'}
217  % [ % [ % [ // | <(rel_labelled … REL) // ] | // ] | %{0} %{0} %{[ ]} %{[ ]} %{sf} %{s1'} /6/ ]
218| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #EXTRA_STEP
219  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
220  cases (true_or_false_Prop … (pcs_labelled … s1))
221  [ #CS
222    lapply (sim_cost … REL CS STEP1)
223    #AFTER1'
224    cases (after_n_exec_steps … AFTER1')
225    #prefix' * #s2' * * #EXEC1' #_ * #Etrace #R2
226    cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
227    cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
228    cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
229    #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R''
230    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
231    % [ % [ %
232    [  @(exec_steps_join … EXEC1') @EXEC''
233    |  @CS''
234    ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
235       cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
236       <all_1 assumption
237    ]| assumption
238    ]
239 
240  | #NCS
241    cases (true_or_false_Prop (pnormal_state C1 g s1))
242    [ #NORMAL
243      (* XXX should set things up so that notb_Prop isn't needed *)
244      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
245      #n' #AFTER1'
246      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
247      cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
248      #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R''
249      %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
250      % [ % [ %
251      [  @(exec_steps_join … EXEC1') @EXEC''
252      |  @CS''
253      ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
254         [ assumption
255         | cases prefix' in EXEC1' INV ⊢ %;
256           [ //
257           | * #sx #trx #tl #EXEC1' #INV
258             <(exec_steps_first … EXEC1')
259             whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
260             @INV
261           ]
262         | @OBS''
263         ]
264      ]| @R''
265      ]
266
267    | #CALLRET
268      cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
269      [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
270        lapply (no_tailcalls … s1)
271        cases (pcs_classify … s1) in CALLRET ⊢ %;
272        [ 1,3: #_ #_ /2/
273        | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??))
274        ]
275      ] * #CL
276      [ cases (true_or_false_Prop … (pcs_labelled … s2))
277        [ #CS2
278          (* Can we execute another step now, or shall we wait for later? *)
279          cases m in IH EXEC2;
280          [ #_ (* Nope, use extra step to get back into relation *)
281            #EXEC2 whd in EXEC2:(??%%); destruct
282            cases EXTRA_STEP #trx * #sx #EXTRA -EXTRA_STEP
283            cases (exec_steps_S … EXTRA) #NFf * #trx' * #sx' * #tlx * * #Ex #EXTRA_STEP #EX' whd in EX':(??%?); destruct
284            cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 EXTRA_STEP)
285            #m' #AFTER1'
286            cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace #CS2' #AFTER2'
287            cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2 #R3
288            %{1} %{prefix1'} %{s2'}
289            % [ % [ %
290            [  @EXEC1'
291            |  @CS2'
292            ]| destruct cases (exec_steps_S … EXEC1')
293               #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
294               destruct <(append_nil … (?::prefix2)) in ⊢ (???%);
295               @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
296               [ whd in match (cs_classify ??); >CL %
297               | whd in match (cs_classify ??); >(rel_classify_call … REL CL) %
298               | @INV1
299               | %
300               | @(rel_callee … REL)
301               ]
302            ]| %{1} %{m'} %{[〈sf,trx'〉]} %{prefix2'} %{sx} %{s3'}
303               cut (all ? (λst.pnormal_state C2 g' (\fst st)) prefix2')
304               [ cases prefix2' in EXEC2' INV2 ⊢ %;
305                  [ //
306                  | * #sp #trp #tlp #EXEC2' #INV2
307                    whd in ⊢ (?%); <(exec_steps_first … EXEC2')
308                    >labelled_normal2 //
309                  ]
310               ] #Np2'
311               % [ % [ % [ % [ %
312               [  @EXTRA
313               |  whd in ⊢ (?%); >labelled_normal1 //
314               ]| @EXEC2'
315               ]| @Np2'
316               ]| #cs <(append_nil … prefix2') <Etrace2
317                  @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
318                  [ <normal_state_p @labelled_normal1 //
319                  | @Np2'
320                  | //
321                  ]
322               ]| @R3
323               ]
324            ]
325          (* We can execute the cost label, too. *)
326          | #m1 #IH #EXEC2
327            cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3
328            cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2)
329            #m' #AFTER1'
330            cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2'
331            cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3
332            letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
333            cases (IH m1 ? next_stack … R3 … EXEC3 CSf EXTRA_STEP) [2: // ]
334            #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R''
335            %{(S m' + m'')} %{(prefix1'@prefix2'@prefix'')} %{sf''}
336            % [ % [ %
337            [  @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC''
338            |  @CSf''
339            ]| destruct cases (exec_steps_S … EXEC1')
340               #NF1' * #tr1' * #s2'' * #prefix2'' * * #E #STEP1' #EXEC2''
341               whd in EXEC2'':(??%%);
342               destruct
343               @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
344               [ whd in match (cs_classify ??); >CL %
345               | whd in match (cs_classify ??); >(rel_classify_call … REL CL) %
346               | %
347               | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
348                 [ <normal_state_p @labelled_normal1 @CS2
349                 | cases prefix2' in EXEC2' INV2 ⊢ %;
350                   [ //
351                   | * #sy #try #tly #EXEC2' #INV2
352                     <(exec_steps_first … EXEC2')
353                     whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 //
354                   ]
355                 | assumption
356                 ]
357               | @(rel_callee … REL)
358               ]
359            ]| @R''
360            ]
361          ]
362
363        | #NCS2
364          cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1)
365          [2: >CL % | 3: @notb_Prop @NCS2 ]
366          #m' #AFTER1'
367          cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
368          letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
369          cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
370          #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R''
371          %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
372          % [ % [ %
373          [  @(exec_steps_join … EXEC1') @EXEC''
374          |  @CSf''
375          ]| destruct cases (exec_steps_S … EXEC1')
376             #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
377             destruct
378             @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
379             [ whd in match (cs_classify ??); >CL %
380             | whd in match (cs_classify ??); >(rel_classify_call … REL CL) %
381             | @INV
382             | assumption
383             | @(rel_callee … REL)
384             ]
385          ]| @R''
386          ]
387        ]
388
389      | cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %]
390        #m' * #Etr #AFTER1'
391        cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
392        letin next_stack ≝ (tail … current_stack)
393        cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: //]
394        #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R''
395        %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
396        % [ % [ %
397        [  @(exec_steps_join … EXEC1') @EXEC''
398        |  @CSf''
399        ]| destruct cases (exec_steps_S … EXEC1')
400           #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
401           destruct >Etrace
402           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
403           [ whd in match (cs_classify ??); >CL % 
404           | whd in match (cs_classify ??); @(rel_classify_return … REL CL)
405           | @INV
406           | assumption
407           ]
408        ]| @R''
409        ]
410      ]
411    ]
412  ]
413] qed.
414
415definition ends_at_return : ∀C:preclassified_system. ∀g. list (state … C g × trace) → Prop ≝
416λC,g,x. ∃x',tr2,s2. x = x'@[〈s2,tr2〉] ∧ pcs_classify C g s2 = cl_return.
417
418lemma ends_at_return_append : ∀C,g,t1,t2.
419  ends_at_return C g t2 →
420  ends_at_return C g (t1@t2).
421#C #g #t1 #t2 * #x * #tr * #s * #E >E #CL
422%{(t1@x)} %{tr} %{s} % /2/
423qed.
424
425lemma will_return_aux_normal : ∀C,depth,t1,t2.
426  all … (λstr. normal_state C (\fst str)) t1 →
427  will_return_aux C depth (t1@t2) = will_return_aux C depth t2.
428#C #depth #t1 #t2 elim t1
429[ #_ %
430| * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl
431  whd in ⊢ (??%?);
432  cases (normal_state_inv … N1) #CL >CL
433  @IH @Ntl
434] qed.
435
436(* Now show the preservation of parts of the measurable subtrace from states in
437   simulation to the end.  (We'll deal with any extra steps at the start from
438   the prefix lemma in the theorem below.)  The basic idea here is that having
439   broken up the simulation results into normal, call, return and cost lemmas,
440   we can match up the structure of the two executions, and in particular
441   prove the will_return_aux predicate for the target execution. *)
442
443lemma measurable_subtrace_preserved :
444  ∀MS:meas_sim.
445  ∀g,g'.
446  ∀INV:ms_inv MS g g'.
447  ∀s1,s1',depth,callstack.
448  ms_rel MS g g' INV s1 s1' →
449 
450  let C ≝ pcs_to_cs (ms_C1 MS) g in
451  let C' ≝ pcs_to_cs (ms_C2 MS) g' in
452
453  ∀m,interesting,sf.
454  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈interesting,sf〉 →
455  ends_at_return (ms_C1 MS) g interesting →
456  will_return_aux C depth interesting →
457
458  ∃m',interesting',sf'.
459    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈interesting',sf'〉 ∧
460    (* The obs trace equality almost gives this, but doesn't ensure the
461       cost/return are exactly at the ends *)
462    ends_at_return (ms_C2 MS) g' interesting' ∧
463    bool_to_Prop (will_return_aux C' depth interesting') ∧
464   
465    intensional_trace_of_trace C callstack interesting = intensional_trace_of_trace C' callstack interesting'.
466    (* Seems a shame to leave this out "∧ ms_rel MS g g' INV sf sf'", but it
467       isn't true if the final return step is expanded into the caller, e.g.,
468       in Clight → Cminor we added an instruction to callers if they need to
469       store the result in memory.  This extra step doesn't form part of the
470       measurable trace, so the end is no longer in the relation. ☹ *)
471   
472* #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls (*#measure1*) #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
473#g #g' #INV #s1 #s1' #depth #callstack #REL
474#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
475generalize in match callstack; generalize in match depth; -callstack -depth
476@(nat_elim1 m0) *
477[ #_ (* "fake" base case - we can never have zero steps *)
478  #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC
479  whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct
480| #m #IH #depth #current_stack #s1 #s1' #REL #prefix #sf #EXEC #END #RETURNS
481  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
482  cases (true_or_false_Prop … (pcs_labelled … s1))
483  [ #CS
484    lapply (sim_cost … REL CS STEP1)
485    #AFTER1'
486    cases (after_n_exec_steps … AFTER1')
487    #interesting' * #s2' * * #EXEC1' #_ * #Etrace #R2
488    cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
489    cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
490    cases (IH m ? depth current_stack … R2 … EXEC2 ??)
491    [ 2: //
492    | (* End must be later, and still a return *)
493      3: destruct cases END *
494      [ * #trE * #sE * #E whd in E:(???%); destruct
495        #CL cases (pnormal_state_inv … N1) >CL #E destruct
496      | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
497        %{t} %{trE} %{sE} /2/
498      ]
499    | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
500      cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS
501    ]
502    #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
503    %{(1+m'')} %{(interesting'@interesting'')} %{sf''}
504    % [ % [ %
505    [  @(exec_steps_join … EXEC1') @EXEC''
506    |  @ends_at_return_append assumption
507    ]| cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
508       >will_return_aux_normal
509       [ @RETURNS''
510       | whd in ⊢ (?%); <normal_state_p >N1' %
511       ]
512    ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
513       cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
514       <all_1 assumption
515    ]
516 
517  | #NCS
518    cases (true_or_false_Prop (pnormal_state C1 g s1))
519    [ #NORMAL
520      (* XXX should set things up so that notb_Prop isn't needed *)
521      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
522      #n' #AFTER1'
523      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
524      cases (IH m ? depth current_stack … R2 … EXEC2 ??)
525      [ 2: //
526      | (* End must be later, and still a return *)
527        3: destruct cases END *
528        [ * #trE * #sE * #E whd in E:(???%); destruct
529          #CL cases (pnormal_state_inv … NORMAL) >CL #E destruct
530        | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
531          %{t} %{trE} %{sE} /2/
532        ]
533      | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
534        cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS
535      ]
536      #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
537      %{(n'+m'')} %{(interesting'@interesting'')} %{sf''}
538      % [ % [ %
539      [  @(exec_steps_join … EXEC1') @EXEC''
540      |  @ends_at_return_append assumption
541      ]| >will_return_aux_normal
542         [ @RETURNS''
543         | cases n' in EXEC1';
544           [ #EXEC >(lenght_to_nil (*sic*) … interesting') // >(exec_steps_length … EXEC) %
545           | #n'' #EXEC cases (exec_steps_S … EXEC)
546             #_ * #tr1' * #s2' * #tl * * #E #STEP1' #EXEC2' destruct
547             @andb_Prop [ <normal_state_p <(rel_normal … REL) @NORMAL | @INV ]
548           ]
549         ]
550      ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
551          [ assumption
552          | cases interesting' in EXEC1' INV ⊢ %;
553            [ //
554            | * #sx #trx #tl #EXEC1' #INV
555              <(exec_steps_first … EXEC1')
556              whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
557              @INV
558            ]
559          | @OBS''
560          ]
561      ]
562
563    | #CALLRET
564      cases trace2 in E1 EXEC2;
565        (* For a return we might hit the end - this is the real base case. *)
566      [ #E1 #EXEC2 destruct cases END #tl * #tr * #s1x * #E1 #CL
567        cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ]
568        #E1 normalize in E1; destruct
569        cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %]
570        #m' * #Etr #AFTER1' destruct
571        cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2'
572        cut (tr1' = E0) [
573          cases (after_n_exec_steps … AFTER2') #trace * #sf' * * #_ #_ * #H #_
574          cases (Eapp_E0_inv … (sym_eq … H)) //
575        ] #E1 destruct
576        %{1} %{[〈s1',E0〉]} %{s2'}
577        % [ % [ %
578        [  whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); %
579        |  %{[ ]} %{E0} %{s1'} %{(refl ??)} @(rel_classify_return … REL) assumption
580        ]| whd in RETURNS:(?%) ⊢ (?%);
581           whd in match (cs_classify ??) in RETURNS;
582           whd in match (cs_classify ??); >(rel_classify_return … REL CL)
583           >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%);
584           cases depth [ // | #d * ]
585        ]| <(append_nil … [〈s1',E0〉])
586           change with (gather_trace … [〈s1',E0〉]) in match E0 in ⊢ (??%?);
587           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
588           [ @CL
589           | whd in ⊢ (??%?); @(rel_classify_return … REL CL)
590           | %
591           | %
592           ]
593        ]
594      ]
595      (* Not at the end *)
596      * #s2x #tr2 #trace3 #E1 #EXEC2
597      cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
598      [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
599        lapply (no_tailcalls … s1)
600        cases (pcs_classify … s1) in CALLRET ⊢ %;
601        [ 1,3: #_ #_ /2/
602        | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??))
603        ]
604      ] * #CL
605     
606      [ cases (true_or_false_Prop … (pcs_labelled … s2))
607        [ #CS2
608          (* We can't stop here *)
609          cases m in IH EXEC2;
610          [ #_ #EXEC2 whd in EXEC2:(??%%); destruct ]
611          #m1 #IH #EXEC2
612          cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3
613          cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2)
614          #m' #AFTER1'
615          cases (after_n_exec_steps … AFTER1') #interesting1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2'
616          cases (after_n_exec_steps … AFTER2') #interesting2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3
617          letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
618          letin next_depth ≝ (S depth)
619          cut (pnormal_state C1 g s2) [ @labelled_normal1 assumption ] #N2
620          cases (IH m1 ? next_depth next_stack … R3 … EXEC3 ??)
621          [ 2: //
622          | (* End must be later, and still a return *)
623            3: destruct cases END *
624            [ * #trE * #sE * #E whd in E:(???%); destruct
625            | *: #h1 *
626              [ * #trE * #sE * #E normalize in E:(???%); destruct
627                #CL cases (pnormal_state_inv … N2) >CL #E destruct
628              | #h2 #t * #trE * #sE * #E normalize in E:(???%); destruct #CL
629                 %{t} %{trE} %{sE} /2/
630              ]
631            ]
632          | 4: destruct whd in RETURNS:(?%);
633            whd in match (cs_classify ??) in RETURNS;
634            >CL in RETURNS; whd in ⊢ (?% → ?);
635            cases (pnormal_state_inv … N2) #CL2
636            whd in match (cs_classify ??); >CL2 //
637          ]
638          #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
639          %{(S m' + m'')} %{(interesting1'@interesting2'@interesting'')} %{sf''}
640          % [ % [ %
641          [ @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC''
642          | @ends_at_return_append @ends_at_return_append assumption
643         ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2''
644            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
645            >(rel_classify_call … REL CL) whd in ⊢ (?%); whd in INV1:(?(???%));
646            >will_return_aux_normal [2: @INV1 ]
647            >will_return_aux_normal
648            [ //
649            | cases interesting2' in EXEC2' INV2 ⊢ %;
650              [ //
651              | * #s2'' #tr2'' #tl2'' #E2'' <(exec_steps_first … E2'') #TL
652                whd in ⊢ (?%); <normal_state_p >(labelled_normal2 … CS2') @TL
653              ]
654            ]
655         ]| destruct cases (exec_steps_S … EXEC1')
656            #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2''
657            destruct
658            @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
659            [ whd in match (cs_classify ??); >CL %
660            | whd in match (cs_classify ??); >(rel_classify_call … REL CL) %
661            | @INV1
662            | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
663              (* Repeats bits of proof above, could compress *)
664              [ <normal_state_p @labelled_normal1 @CS2
665              | cases interesting2' in EXEC2' INV2 ⊢ %;
666                [ //
667                | * #sy #try #tly #EXEC2' #INV2
668                  <(exec_steps_first … EXEC2')
669                  whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 //
670                ]
671              | assumption
672              ]
673            | @(rel_callee … REL)
674            ]
675          ]
676
677        | #NCS2
678          cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1)
679          [2: >CL % | 3: @notb_Prop @NCS2 ]
680          #m' #AFTER1'
681          cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
682          letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
683          letin next_depth ≝ (S depth)
684          cases (IH m ? next_depth next_stack … R2 … EXEC2 ??)
685          [ 2: //
686          | (* End must be later, and still a return *)
687            3: destruct cases END *
688            [ * #trE * #sE * #E whd in E:(???%); destruct
689            | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
690              %{t} %{trE} %{sE} /2/
691            ]
692          | 4: destruct whd in RETURNS:(?%);
693               whd in match (cs_classify ??) in RETURNS;
694               >CL in RETURNS; //
695          ]
696          #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
697          %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''}
698          % [ % [ %
699          [ @(exec_steps_join … EXEC1') @EXEC''
700          | @ends_at_return_append assumption
701         ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
702            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
703            >(rel_classify_call … REL CL) whd in ⊢ (?%);
704            >will_return_aux_normal //
705         ]| destruct cases (exec_steps_S … EXEC1')
706            #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
707            destruct
708            @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
709            [ whd in match (cs_classify ??); >CL %
710            | whd in match (cs_classify ??); >(rel_classify_call … REL CL) %
711            | @INV
712            | assumption
713            | @(rel_callee … REL)
714            ]
715          ]
716       ]
717     |
718
719      cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %]
720      #m' * #Etr #AFTER1'
721      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
722      letin next_stack ≝ (tail … current_stack)
723      letin next_depth ≝ (pred depth)
724      cases (IH m ? next_depth next_stack … R2 … EXEC2 ??)
725      [ 2: //
726      | (* End must be later, and still a return *)
727        3: destruct cases END *
728        [ * #trE * #sE * #E whd in E:(???%); destruct
729        | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
730          %{t} %{trE} %{sE} /2/
731        ]
732      | 4: destruct whd in RETURNS:(?%);
733           whd in match (cs_classify ??) in RETURNS;
734           >CL in RETURNS; whd in ⊢ (?% → ?);
735           whd in match next_depth; cases depth
736           [ * | #d' // ]
737      ]
738      #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
739      %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''}
740      % [ % [ %
741      [ @(exec_steps_join … EXEC1') @EXEC''
742      | @ends_at_return_append assumption
743     ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
744        destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %;
745        >(rel_classify_return … REL CL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%);
746        whd in match next_depth in RETURNS'';
747        cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_
748        whd in ⊢ (?%);
749        >will_return_aux_normal [ @RETURNS'' | @INV ]
750     ]| destruct cases (exec_steps_S … EXEC1')
751        #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
752        destruct >Etrace
753        @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
754        [ whd in match (cs_classify ??); >CL %
755        | whd in match (cs_classify ??); @(rel_classify_return … REL CL)
756        | @INV
757        | assumption
758        ]
759    ]
760  ]
761] qed.
762
763lemma label_to_ret_inv : ∀C,m,g,s,trace,s'.
764  exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 →
765  trace_is_label_to_return (pcs_to_cs … C g) trace →
766  bool_to_Prop (pcs_labelled C g s) ∧ ends_at_return C g trace.
767#C #m #g #s #trace #s' #EXEC
768* #tr * #s1 * #tl * #tr2 * #s2 * * #E #CS #CL destruct
769>(exec_steps_first … EXEC)
770%
771[ @CS
772| %{(〈s1,tr〉::tl)} %{tr2} %{s2} %{(refl ??)} @CL
773] qed.
774
775lemma build_label_to_ret : ∀C,m,g,s,trace,s'.
776  (∀s. pcs_labelled C g s → pnormal_state C g s) →
777  exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 →
778  pcs_labelled C g s →
779  ends_at_return C g trace →
780  trace_is_label_to_return (pcs_to_cs … C g) trace.
781#C #m #g #s #trace #s' #LABELLED_NORMAL #EXEC #CS * #trace' * #tr2 * #s2 * #E #CL
782destruct
783cases trace' in EXEC ⊢ %;
784[ #EXEC >(exec_steps_first … EXEC) in CS; #CS
785  cases (pnormal_state_inv … (LABELLED_NORMAL … CS)) >CL #E destruct
786| * #s1 #tr1 #trace1 #EXEC
787  %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ % | <(exec_steps_first … EXEC) @CS ] | @CL ]
788] qed.
789
790
791lemma ends_at_return_normal : ∀C,g,t1,t2.
792  ends_at_return C g (t1@t2) →
793  all … (λst. pnormal_state C g (\fst st)) t1 →
794  ends_at_return C g t2.
795#C #g #t1 elim t1
796[ //
797| * #s #tr #tl #IH #t2 * #tr1 * #tr2 * #s2 * cases tr1
798  [ #E normalize in E; destruct #CL whd in ⊢ (?% → ?);
799    lapply (pnormal_state_inv … s2)
800    cases (pnormal_state … s2)
801    [ #H cases (H I) >CL #E' destruct
802    | #_ *
803    ]
804  | * #s' #tr' #tl' #E whd in E:(??%%); destruct #CL #ALL
805    @IH
806    [ %{tl'} %{tr2} %{s2} >e0 % //
807    | whd in ALL:(?%); cases (pnormal_state … s') in ALL;
808      [ // | * ]
809    ]
810  ]
811] qed.
812
813
814(* Now put the two main lemmas above together to show that the target has a
815   [measurable] subtrace, and that the observables are the same.
816
817   To deal with the extra steps from the prefix lemma, note that they are
818   "normal" steps, and so cannot interfere with the structure. *)
819
820theorem measured_subtrace_preserved :
821  ∀MS:meas_sim.
822  ∀p1,p2,m,n,stack_cost,max.
823  ms_compiled MS p1 p2 →
824  measurable (ms_C1 MS) p1 m n stack_cost max →
825  ∃m',n'.
826    measurable (ms_C2 MS) p2 m' n' stack_cost max ∧
827    observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'.
828#MS #p1 #p2 #m #n #stack_cost #max #compiled
829* #s0 * #prefix * #s1 * #interesting * #s2
830whd in ⊢ (? → ??(λ_.??(λ_.(?%(??%%)))));
831letin g ≝ (make_global … (pcs_exec … ) p1)
832letin g' ≝ (make_global … (pcs_exec … ) p2)
833letin C ≝ (pcs_to_cs ? g)
834letin C' ≝ (pcs_to_cs ? g')
835* * * * * #INIT #EXEC0 #EXEC1 #TLR #RETURNS #MAX
836
837cases (sim_init … compiled INIT) #s0' * #INIT' * #INV #R0
838cases (label_to_ret_inv … EXEC1 TLR)
839#CS1 #ENDS
840
841cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1)
842(* Need an extra step from the source in case we end up at a label after a
843   function call. *)
844[2: cases n in EXEC1;
845  [ #E whd in E:(??%?); destruct cases RETURNS
846  | #n1 #EXEC1 cases (exec_steps_split 1 … EXEC1) #ex * #ex2 * #sx * * #EX1 #_ #_
847    %{ex} %{sx} @EX1
848  ]
849]
850#m' * #prefix' * #s1' * * * #EXEC0' #CS1' #OBS0
851* #r * #r' * #interesting1 * #interesting1' * #sr * #sr' * * * * * #EXECr #Nr #EXECr' #Nr' #OBS1 #R1
852
853(* Show that the extra r steps we need to get back into the relation are a
854   prefix of the measurable subtrace. *)
855cut (∃nr,interesting2. n = r + nr ∧
856  exec_steps nr … C g sr = OK … 〈interesting2,s2〉 ∧
857  interesting = interesting1 @ interesting2)
858[ cases (plus_split n r) #nr *
859  [ #En %{nr} >En in EXEC1; #EXEC1
860    cases (exec_steps_split … EXEC1)
861    #interesting1x * #interesting2 * #srx * * #EXEC1x #EXECrx #E
862    >EXECr in EXEC1x; #E1x destruct
863    %{interesting2} % [ % [ % | assumption ] | % ]
864  | #En @⊥
865    >En in EXECr; #EXECr cases (exec_steps_split … EXECr)
866    #ex1 * #ex2 * #sx * * #EX1 #EXx #E >E in Nr; >EXEC1 in EX1; #E' destruct
867    #Nr cases (andb_Prop_true … (all_append … Nr)) #N1 #N2
868    cases ENDS #le * #tre * #se * #Ee #CLe destruct
869    cases (andb_Prop_true … (all_append … N1)) #_ whd in ⊢ (?% → ?);
870    lapply (pnormal_state_inv … se) cases (pnormal_state … se)
871    [ #H cases (H I) >CLe #E destruct
872    | #_ *
873    ]
874  ]
875]
876* #nr * #interesting2 * * #En #EXECr2 #Ei destruct
877
878whd in RETURNS:(?%);
879>will_return_aux_normal in RETURNS;
880[2: @Nr] #RETURNS
881
882lapply (ends_at_return_normal … ENDS Nr)
883#ENDS2
884
885cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] (prefix@interesting1))) R1 … EXECr2 ENDS2 RETURNS)
886#n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS'
887
888cut (intensional_trace_of_trace C [ ] (prefix@interesting1) =
889     intensional_trace_of_trace C' [ ] (prefix'@interesting1'))
890[ >int_trace_append' >(int_trace_append' C')
891  <OBS0 @breakup_pair @breakup_pair @breakup_pair @breakup_pair
892  <OBS1 %
893] #OBS01
894
895cut (intensional_trace_of_trace C [ ] (prefix@interesting1@interesting2) =
896     intensional_trace_of_trace C' [ ] (prefix'@interesting1'@interesting'))
897[ <associative_append <associative_append
898  >int_trace_append' >(int_trace_append' C')
899  <OBS01
900  @breakup_pair @breakup_pair @breakup_pair @breakup_pair
901  <OBS' %
902] #Eobs
903
904lapply (exec_steps_join … EXECr' EXEC1')
905#EXECr''
906
907%{m'} %{(r' + n')} %
908[ %{s0'} %{prefix'} %{s1'} %{(interesting1'@interesting')} %{s2'}
909  % [ % [ % [ % [ %
910  [  assumption
911  |  assumption
912  ]| assumption
913  ]| @(build_label_to_ret … EXECr'' ? (ends_at_return_append … ENDS'))
914     [ #s #CS @(ms_labelled_normal_2 … CS)
915     | <(ms_rel_labelled … R1) @CS1'
916     ]
917  ]| whd in ⊢ (?%); >will_return_aux_normal [2: @Nr'] @RETURNS'
918  ]| <Eobs @MAX
919  ]
920| >INIT >INIT'
921  whd in ⊢ (??%%); >EXEC0 >EXEC0'
922  whd in ⊢ (??%%); >EXEC1 >EXECr''
923  whd in ⊢ (??%%); >int_trace_append' in OBS'; <OBS0
924  cases (intensional_trace_of_trace C [ ] prefix)
925  #cs #prefixtr whd in ⊢ (??(??(???%)?)(??(???%)?) → ??%%);
926  >int_trace_append' >int_trace_append' <OBS1
927  @breakup_pair @breakup_pair @breakup_pair @breakup_pair @breakup_pair
928  #OBS' <OBS' %
929] qed.
Note: See TracBrowser for help on using the repository browser.