source: src/common/FEMeasurable.ma @ 2970

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

Fix silly label handling bug I realised was there during my talk...

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