source: src/common/FEMeasurable.ma @ 2989

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

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

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