source: src/common/FEMeasurable.ma @ 3063

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

Remove measure function from FEMeasurable because we're not using it and
it would need to be generalised for clight to cminor. Sketch out rest
of clight to cminor meas_sim record.

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