source: src/common/FEMeasurable.ma @ 2990

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

Replace dodgy hypothesis by nice ones, clean up a little.

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