source: src/common/FEMeasurable.ma @ 3007

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

Sketch out how Cminor to RTLabs correctness would fit into the
front-end measurable traces proof.

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