source: src/common/FEMeasurable.ma @ 2768

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

Remove a couple of redundant hypotheses.
File size: 26.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  sim_call_return :
63    ∀g1,g2.
64    ∀INV:ms_inv g1 g2.
65    ∀s1,s1'.
66    ms_rel g1 g2 INV s1 s1' →
67    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
68    ¬ pcs_labelled ms_C1 g1 s1 →
69    (* NB: calls and returns don't emit timing cost labels; otherwise we would
70       have to worry about whether the cost labels seen at the final return of
71       the measured trace might appear in the target in subsequent steps that
72       are *after* the new measurable subtrace.  Also note that extra steps are
73       introduced in the front-end: to perform variable saves on entry and to
74       write back the result *after* exit.  The latter do not get included in
75       the measurable subtrace because it stops at the return, and they are the
76       caller's responsibility. *)
77    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
78    ∃m. tr = E0 ∧
79      after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
80      E0 = tr' ∧
81      ms_rel g1 g2 INV s2 s2'
82    );
83  sim_cost :
84    ∀g1,g2.
85    ∀INV:ms_inv g1 g2.
86    ∀s1,s1',s2,tr.
87    ms_rel g1 g2 INV s1 s1' →
88    pcs_labelled ms_C1 g1 s1 →
89    step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
90    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
91      tr = tr' ∧
92      ms_rel g1 g2 INV s2 s2'
93    );
94  sim_init :
95    ∀p1,p2,s.
96    ms_compiled p1 p2 →
97    make_initial_state ?? ms_C1 p1 = OK ? s →
98    ∃s'. make_initial_state ?? ms_C2 p2 = OK ? s' ∧
99    ∃INV. ms_rel ?? INV s s'
100}.
101
102
103(*
104lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
105  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
106  pnormal_state C g s1 →
107  stack_after (pcs_to_cs C g stack) current trace = current.
108#C #g #s1 #trace #s2 #stack #current #EXEC
109cases (exec_steps_S … EXEC)
110#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
111#N
112whd in ⊢ (??%?); generalize in match (cs_stack ??);
113whd in match (cs_classify ??);
114cases (pnormal_state_inv … N)
115#CL >CL #f %
116qed.
117
118lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
119  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
120  pnormal_state C g s1 →
121  max_stack (pcs_to_cs C g stack) current trace = current.
122#C #g #s1 #trace #s2 #stack #current #EXEC
123cases (exec_steps_S … EXEC)
124#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
125#N
126whd in ⊢ (??%?); generalize in match (cs_stack ??);
127whd in match (cs_classify ??);
128cases (pnormal_state_inv … N)
129#CL >CL #f %
130qed.
131
132lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf.
133  exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
134  ¬pcs_labelled C g s1 →
135  pcs_labelled C g sf →
136  ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) →
137  ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P →
138  ∃p,trace1,s2,trace2.
139    exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
140    P (gather_trace … trace1) s2 ∧
141    exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧
142    m = n + p.
143#C #g #m elim m -m
144[ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct
145  #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS
146| #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H *
147  [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ % | @AFTER ] | @EXEC1 ]| % ]
148  | #n #P #AFTER
149    cases (exec_steps_S … EXEC1)
150    #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2
151    cases (after_1_of_n_steps … AFTER)
152    #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2
153    >STEP in STEP'; #E destruct
154    cases (IH … EXEC2 … AFTER2)
155    [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E
156      %{p} % [2: %{s2} %{trace2} % [ % [ %
157       [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); % | skip ]
158      | @P2 ]| @EXEC2 ]| >E % ] | skip ]
159    | @H assumption
160    | assumption
161    | assumption
162    ]
163  ]
164] qed.
165
166lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf.
167  exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
168  ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P →
169  ∃trace1,s2,trace2.
170    exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
171    P (gather_trace … trace1) s2 ∧
172    exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉.
173#C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1
174cases (exec_steps_S … EXEC1)
175#NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2
176%{[〈s1,tr〉]} %{s2} %{tl} % [ %
177 [ whd in ⊢ (??%?); >NF1 >STEP % | whd in AFTER1; >NF1 in AFTER1; >STEP normalize
178 cases (inv s2) // * ]| // ]
179qed.
180*)
181(* XXX do I need to do the max_stack reasoning here?  perhaps just by preserving
182   observables? *)
183
184lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'.
185  exec_steps 1 O I fx g s = OK ? 〈trace,s'〉 →
186  ∃tr. trace = [〈s,tr〉].
187#O #I #fx #g #s #trace #s' #EXEC
188cases (exec_steps_S … EXEC)
189#nf * #tr * #s'' * #tl * * #E1 #STEP #EXEC' whd in EXEC':(??%%); destruct
190%{tr} %
191qed.
192
193lemma all_1 : ∀A.∀P:A → bool.∀x.
194  P x = all A P [x].
195#A #P #x whd in ⊢ (???%); cases (P x) //
196qed.
197
198
199lemma prefix_preserved :
200  ∀MS:meas_sim.
201  ∀g,g'.
202  ∀INV:ms_inv MS g g'.
203  ∀s1,s1'.
204  ms_rel MS g g' INV s1 s1' →
205
206  ∀m,prefix,sf.
207  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
208  pcs_labelled (ms_C1 MS) g sf →
209
210  ∃m',prefix',sf'.
211    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
212
213    intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧
214    ms_rel MS g g' INV sf sf'.
215* #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init
216#g #g' #INV #s1 #s1' #REL
217#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
218generalize in match [ ]; (* current call stack *)
219elim m0
220[ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
221  %{0} %{[]} %{s1'}
222  % [ % // | // ]
223| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf
224  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
225  cases (true_or_false_Prop … (pcs_labelled … s1))
226  [ #CS
227    lapply (sim_cost … REL CS STEP1)
228    #AFTER1'
229    cases (after_n_exec_steps … AFTER1')
230    #prefix' * #s2' * * #EXEC1' #_ * #Etrace #R2
231    cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
232    cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
233    cases (IH current_stack … R2 … EXEC2 CSf)
234    #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
235    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
236    % [ % [ @(exec_steps_join … EXEC1') @EXEC''
237      | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
238        cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
239        <all_1 assumption
240      ]| assumption
241      ]
242 
243  | #NCS
244    cases (true_or_false_Prop (pnormal_state C1 g s1))
245    [ #NORMAL
246      (* XXX should set things up so that notb_Prop isn't needed *)
247      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
248      #n' #AFTER1'
249      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
250      cases (IH current_stack … R2 … EXEC2 CSf)
251      #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
252      %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
253      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
254        | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
255          [ assumption
256          | cases prefix' in EXEC1' INV ⊢ %;
257            [ //
258            | * #sx #trx #tl #EXEC1' #INV
259              <(exec_steps_first … EXEC1')
260              whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
261              @INV
262            ]
263          | @OBS'' ] ]
264        | @R''
265        ]
266    | #CALLRET
267      cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
268      [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
269        lapply (no_tailcalls … s1)
270        cases (pcs_classify … s1) in CALLRET ⊢ %;
271        [ 1,3: #_ #_ /2/
272        | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??))
273        ]
274      ] * #CL
275      cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
276      [2,4: >CL %]
277      #m' * #Etr #AFTER1'
278      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
279      [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
280      | letin next_stack ≝ (tail … current_stack)
281      ]
282      cases (IH next_stack … R2 … EXEC2 CSf)
283      #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
284      %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
285      % [1,3: % [1,3: @(exec_steps_join … EXEC1') @EXEC''
286        | destruct cases (exec_steps_S … EXEC1')
287          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
288          destruct >Etrace
289          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
290          [ whd in match (cs_classify ??); >CL %
291          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
292          | @INV
293          | assumption
294          | @(rel_callee … REL)
295          ]
296        | destruct cases (exec_steps_S … EXEC1')
297          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
298          destruct >Etrace
299          @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
300          [ whd in match (cs_classify ??); >CL %
301          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
302          | @INV
303          | assumption
304          ]
305        ]
306      | 2,4: @R''
307      ]
308    ]
309  ]
310] qed.
311
312definition ends_at_return : ∀C:preclassified_system. ∀g. list (state … C g × trace) → Prop ≝
313λC,g,x. ∃x',tr2,s2. x = x'@[〈s2,tr2〉] ∧ pcs_classify C g s2 = cl_return.
314
315lemma ends_at_return_append : ∀C,g,t1,t2.
316  ends_at_return C g t2 →
317  ends_at_return C g (t1@t2).
318#C #g #t1 #t2 * #x * #tr * #s * #E >E #CL
319%{(t1@x)} %{tr} %{s} % /2/
320qed.
321
322lemma will_return_aux_normal : ∀C,depth,t1,t2.
323  all … (λstr. normal_state C (\fst str)) t1 →
324  will_return_aux C depth (t1@t2) = will_return_aux C depth t2.
325#C #depth #t1 #t2 elim t1
326[ #_ %
327| * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl
328  whd in ⊢ (??%?);
329  cases (normal_state_inv … N1) #CL >CL
330  @IH @Ntl
331] qed.
332
333lemma measurable_subtrace_preserved :
334  ∀MS:meas_sim.
335  ∀g,g'.
336  ∀INV:ms_inv MS g g'.
337  ∀s1,s1',depth,callstack.
338  ms_rel MS g g' INV s1 s1' →
339 
340  let C ≝ pcs_to_cs (ms_C1 MS) g in
341  let C' ≝ pcs_to_cs (ms_C2 MS) g' in
342
343  ∀m,interesting,sf.
344  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈interesting,sf〉 →
345  ends_at_return (ms_C1 MS) g interesting →
346  will_return_aux C depth interesting →
347
348  ∃m',interesting',sf'.
349    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈interesting',sf'〉 ∧
350    (* The obs trace equality almost gives this, but doesn't ensure the
351       cost/return are exactly at the ends *)
352    ends_at_return (ms_C2 MS) g' interesting' ∧
353    bool_to_Prop (will_return_aux C' depth interesting') ∧
354   
355    intensional_trace_of_trace C callstack interesting = intensional_trace_of_trace C' callstack interesting'.
356    (* Seems a shame to leave this out "∧ ms_rel MS g g' INV sf sf'", but it
357       isn't true if the final return step is expanded into the caller, e.g.,
358       in Clight → Cminor we added an instruction to callers if they need to
359       store the result in memory.  This extra step doesn't form part of the
360       measurable trace, so the end is no longer in the relation. ☹ *)
361   
362* #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init
363#g #g' #INV #s1 #s1' #depth #callstack #REL
364#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
365generalize in match callstack; generalize in match depth; -callstack -depth
366elim m0
367[ (* "fake" base case - we can never have zero steps *)
368  #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC
369  whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct
370| #m #IH #depth #current_stack #s1 #s1' #REL #prefix #sf #EXEC #END #RETURNS
371  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
372  cases (true_or_false_Prop … (pcs_labelled … s1))
373  [ #CS
374    lapply (sim_cost … REL CS STEP1)
375    #AFTER1'
376    cases (after_n_exec_steps … AFTER1')
377    #interesting' * #s2' * * #EXEC1' #_ * #Etrace #R2
378    cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
379    cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
380    cases (IH depth current_stack … R2 … EXEC2 ??)
381    [ (* End must be later, and still a return *)
382      2: destruct cases END *
383      [ * #trE * #sE * #E whd in E:(???%); destruct
384        #CL cases (pnormal_state_inv … N1) >CL #E destruct
385      | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
386        %{t} %{trE} %{sE} /2/
387      ]
388    | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
389      cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS
390    ]
391    #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
392    %{(1+m'')} %{(interesting'@interesting'')} %{sf''}
393    % [ % [ %
394    [  @(exec_steps_join … EXEC1') @EXEC''
395    |  @ends_at_return_append assumption
396    ]| cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
397       whd in ⊢ (?%); whd in match (cs_classify ??); <(rel_classify … REL)
398       cases (pnormal_state_inv … N1) #CL >CL @RETURNS''
399    ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
400       cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
401       <all_1 assumption
402    ]
403 
404  | #NCS
405    cases (true_or_false_Prop (pnormal_state C1 g s1))
406    [ #NORMAL
407      (* XXX should set things up so that notb_Prop isn't needed *)
408      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
409      #n' #AFTER1'
410      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
411      cases (IH depth current_stack … R2 … EXEC2 ??)
412      [ (* End must be later, and still a return *)
413        2: destruct cases END *
414        [ * #trE * #sE * #E whd in E:(???%); destruct
415          #CL cases (pnormal_state_inv … NORMAL) >CL #E destruct
416        | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
417          %{t} %{trE} %{sE} /2/
418        ]
419      | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;
420        cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS
421      ]
422      #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
423      %{(n'+m'')} %{(interesting'@interesting'')} %{sf''}
424      % [ % [ %
425      [  @(exec_steps_join … EXEC1') @EXEC''
426      |  @ends_at_return_append assumption
427      ]| >will_return_aux_normal
428         [ @RETURNS''
429         | cases n' in EXEC1';
430           [ #EXEC >(lenght_to_nil (*sic*) … interesting') // >(exec_steps_length … EXEC) %
431           | #n'' #EXEC cases (exec_steps_S … EXEC)
432             #_ * #tr1' * #s2' * #tl * * #E #STEP1' #EXEC2' destruct
433             @andb_Prop [ <normal_state_p <(rel_normal … REL) @NORMAL | @INV ]
434           ]
435         ]
436      ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
437          [ assumption
438          | cases interesting' in EXEC1' INV ⊢ %;
439            [ //
440            | * #sx #trx #tl #EXEC1' #INV
441              <(exec_steps_first … EXEC1')
442              whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
443              @INV
444            ]
445          | @OBS''
446          ]
447      ]
448
449    | #CALLRET
450      cases trace2 in E1 EXEC2;
451        (* For a return we might hit the end - this is the real base case. *)
452      [ #E1 #EXEC2 destruct cases END #tl * #tr * #s1x * #E1 #CL
453        cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ]
454        #E1 normalize in E1; destruct
455        cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
456        [2: >CL %]
457        #m' * #Etr #AFTER1' destruct
458        cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2'
459        cut (tr1' = E0) [
460          cases (after_n_exec_steps … AFTER2') #trace * #sf' * * #_ #_ * #H #_
461          cases (Eapp_E0_inv … (sym_eq … H)) //
462        ] #E1 destruct
463        %{1} %{[〈s1',E0〉]} %{s2'}
464        % [ % [ %
465        [  whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); %
466        |  %{[ ]} %{E0} %{s1'} %{(refl ??)} <(rel_classify … REL) assumption
467        ]| whd in RETURNS:(?%) ⊢ (?%);
468           whd in match (cs_classify ??) in RETURNS;
469           whd in match (cs_classify ??); <(rel_classify … REL)
470           >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%);
471           cases depth [ // | #d * ]
472        ]| <(append_nil … [〈s1',E0〉])
473           change with (gather_trace … [〈s1',E0〉]) in match E0 in ⊢ (??%?);
474           @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
475           [ @CL
476           | whd in ⊢ (??%?); <(rel_classify … REL) @CL
477           | %
478           | %
479           ]
480        ]
481      ] * #s2x #tr2 #trace3 #E1 #EXEC2
482      cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
483      [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
484        lapply (no_tailcalls … s1)
485        cases (pcs_classify … s1) in CALLRET ⊢ %;
486        [ 1,3: #_ #_ /2/
487        | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??))
488        ]
489      ] * #CL
490      cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
491      [2,4: >CL %]
492      #m' * #Etr #AFTER1'
493      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
494      [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
495        letin next_depth ≝ (S depth)
496      | letin next_stack ≝ (tail … current_stack)
497        letin next_depth ≝ (pred depth)
498      ]
499      cases (IH next_depth next_stack … R2 … EXEC2 ??)
500      [(* End must be later, and still a return *)
501        2,5: destruct cases END *
502        [1,3: * #trE * #sE * #E whd in E:(???%); destruct
503        |*: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL
504          %{t} %{trE} %{sE} /2/
505        ]
506      | 3: destruct whd in RETURNS:(?%);
507           whd in match (cs_classify ??) in RETURNS;
508           >CL in RETURNS; //
509      | 6: destruct whd in RETURNS:(?%);
510           whd in match (cs_classify ??) in RETURNS;
511           >CL in RETURNS; whd in ⊢ (?% → ?);
512           whd in match next_depth; cases depth
513           [ * | #d' // ]
514      ]
515      #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS''
516      %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''}
517      % [1,3: % [1,3: %
518      [1,3: @(exec_steps_join … EXEC1') @EXEC''
519      |2,4: @ends_at_return_append assumption
520      ]|    cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
521            destruct whd in ⊢ (?%); whd in match (cs_classify ??);
522            <(rel_classify … REL) >CL whd in ⊢ (?%);
523            >will_return_aux_normal //
524       |    cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'
525            destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %;
526            <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%);
527            whd in match next_depth in RETURNS'';
528            cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_
529            whd in ⊢ (?%);
530            >will_return_aux_normal [ @RETURNS'' | @INV ]
531      ]|  destruct cases (exec_steps_S … EXEC1')
532          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
533          destruct >Etrace
534          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
535          [ whd in match (cs_classify ??); >CL %
536          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
537          | @INV
538          | assumption
539          | @(rel_callee … REL)
540          ]
541       |  destruct cases (exec_steps_S … EXEC1')
542          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
543          destruct >Etrace
544          @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
545          [ whd in match (cs_classify ??); >CL %
546          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
547          | @INV
548          | assumption
549          ]
550       ]
551    ]
552  ]
553] qed.
554
555lemma label_to_ret_inv : ∀C,m,g,s,trace,s'.
556  exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 →
557  trace_is_label_to_return (pcs_to_cs … C g) trace →
558  bool_to_Prop (pcs_labelled C g s) ∧ ends_at_return C g trace.
559#C #m #g #s #trace #s' #EXEC
560* #tr * #s1 * #tl * #tr2 * #s2 * * #E #CS #CL destruct
561>(exec_steps_first … EXEC)
562%
563[ @CS
564| %{(〈s1,tr〉::tl)} %{tr2} %{s2} %{(refl ??)} @CL
565] qed.
566
567lemma build_label_to_ret : ∀C,m,g,s,trace,s'.
568  (∀s. pcs_labelled C g s → pnormal_state C g s) →
569  exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 →
570  pcs_labelled C g s →
571  ends_at_return C g trace →
572  trace_is_label_to_return (pcs_to_cs … C g) trace.
573#C #m #g #s #trace #s' #LABELLED_NORMAL #EXEC #CS * #trace' * #tr2 * #s2 * #E #CL
574destruct
575cases trace' in EXEC ⊢ %;
576[ #EXEC >(exec_steps_first … EXEC) in CS; #CS
577  cases (pnormal_state_inv … (LABELLED_NORMAL … CS)) >CL #E destruct
578| * #s1 #tr1 #trace1 #EXEC
579  %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ % | <(exec_steps_first … EXEC) @CS ] | @CL ]
580] qed.
581
582
583theorem measured_subtrace_preserved :
584  ∀MS:meas_sim.
585  ∀p1,p2,m,n,stack_cost,max.
586  ms_compiled MS p1 p2 →
587  measurable (ms_C1 MS) p1 m n stack_cost max →
588  ∃m',n'.
589    measurable (ms_C2 MS) p2 m' n' stack_cost max ∧
590    observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'.
591#MS #p1 #p2 #m #n #stack_cost #max #compiled
592* #s0 * #prefix * #s1 * #interesting * #s2
593whd in ⊢ (? → ??(λ_.??(λ_.(?%(??%%)))));
594letin g ≝ (make_global … (pcs_exec … ) p1)
595letin g' ≝ (make_global … (pcs_exec … ) p2)
596letin C ≝ (pcs_to_cs ? g)
597letin C' ≝ (pcs_to_cs ? g')
598* * * * * #INIT #EXEC0 #EXEC1 #TLR #RETURNS #MAX
599
600cases (sim_init … compiled INIT) #s0' * #INIT' * #INV #R0
601cases (label_to_ret_inv … EXEC1 TLR)
602#CS1 #ENDS
603
604cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1)
605#m' * #prefix' * #s1' * * #EXEC0' #OBS0 #R1
606
607cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] prefix)) R1 … EXEC1 ENDS RETURNS)
608#n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS'
609
610cut (intensional_trace_of_trace C [ ] (prefix@interesting) =
611     intensional_trace_of_trace C' [ ] (prefix'@interesting'))
612[ >int_trace_append' >int_trace_append'
613  <OBS0 @breakup_pair @breakup_pair @breakup_pair @breakup_pair
614  <OBS' %
615] #Eobs
616
617%{m'} %{n'} %
618[ %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'}
619  % [ % [ % [ % [ %
620  [  assumption
621  |  assumption
622  ]| assumption
623  ]| @(build_label_to_ret … EXEC1' ? ENDS')
624     [ #s #CS @(ms_labelled_normal_2 … CS)
625     | <(ms_rel_labelled … R1) @CS1
626     ]
627  ]| @RETURNS'
628  ]| <Eobs @MAX
629  ]
630| >INIT >INIT'
631  whd in ⊢ (??%%); >EXEC0 >EXEC0'
632  whd in ⊢ (??%%); >EXEC1 >EXEC1'
633  whd in ⊢ (??%%); <OBS0 cases (intensional_trace_of_trace C [ ] prefix) in OBS' ⊢ %;
634  #cs #prefixtr #OBS' whd in ⊢ (??%%); >OBS' %
635] qed.
Note: See TracBrowser for help on using the repository browser.