source: src/common/FEMeasurable.ma @ 3044

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

Remind myself why ms_rel_normal is reasonable.

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