source: src/common/FEMeasurable.ma @ 2685

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

Progress on measurable trace preservation: prefix preserves observable
intensional events (costs and calls).

File size: 12.0 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  ms_rel_classify : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = pcs_classify ms_C2 g2 s2;
36  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';
37
38  (* These hold in (at least) the languages of interest for measurable subtraces *)
39  ms_labelled_normal_1 : ∀g1,s1. pcs_labelled ms_C1 g1 s1 → pnormal_state ms_C1 g1 s1;
40  ms_labelled_normal_2 : ∀g2,s2. pcs_labelled ms_C2 g2 s2 → pnormal_state ms_C2 g2 s2;
41  ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall;
42
43  (* Measure on source states; only needed for showing preservation of
44     non-termination.  Should not be necessary for showing that the measurable
45     traces are preserved. *)
46  ms_measure1 : ∀g1. state … ms_C1 g1 → nat;
47
48  sim_normal :
49    ∀g1,g2.
50    ∀INV:ms_inv g1 g2.
51    ∀s1,s1'.
52    ms_rel g1 g2 INV s1 s1' →
53    pnormal_state ms_C1 g1 s1 →
54    ¬ pcs_labelled ms_C1 g1 s1 →
55    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
56    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
57      tr = tr' ∧
58      ms_rel g1 g2 INV s2 s2' ∧
59      (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))
60    );
61  sim_call_return :
62    ∀g1,g2.
63    ∀INV:ms_inv g1 g2.
64    ∀s1,s1'.
65    ms_rel g1 g2 INV s1 s1' →
66    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
67    ¬ pcs_labelled ms_C1 g1 s1 →
68    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
69    ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
70      tr = tr' ∧
71      ms_rel g1 g2 INV s2 s2'
72    );
73  sim_cost :
74    ∀g1,g2.
75    ∀INV:ms_inv g1 g2.
76    ∀s1,s1',s2,tr.
77    ms_rel g1 g2 INV s1 s1' →
78    pcs_labelled ms_C1 g1 s1 →
79    step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
80    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
81      tr = tr' ∧
82      ms_rel g1 g2 INV s2 s2'
83    );
84  sim_init :
85    ∀p1,p2,s,s'.
86    ms_compiled p1 p2 →
87    make_initial_state ?? ms_C1 p1 = OK ? s →
88    make_initial_state ?? ms_C2 p2 = OK ? s' →
89    ∃INV. ms_rel ?? INV s s'
90}.
91
92(* TODO: obs eq *)
93(*
94lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
95  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
96  pnormal_state C g s1 →
97  stack_after (pcs_to_cs C g stack) current trace = current.
98#C #g #s1 #trace #s2 #stack #current #EXEC
99cases (exec_steps_S … EXEC)
100#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
101#N
102whd in ⊢ (??%?); generalize in match (cs_stack ??);
103whd in match (cs_classify ??);
104cases (pnormal_state_inv … N)
105#CL >CL #f %
106qed.
107
108lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
109  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
110  pnormal_state C g s1 →
111  max_stack (pcs_to_cs C g stack) current trace = current.
112#C #g #s1 #trace #s2 #stack #current #EXEC
113cases (exec_steps_S … EXEC)
114#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
115#N
116whd in ⊢ (??%?); generalize in match (cs_stack ??);
117whd in match (cs_classify ??);
118cases (pnormal_state_inv … N)
119#CL >CL #f %
120qed.
121
122lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf.
123  exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
124  ¬pcs_labelled C g s1 →
125  pcs_labelled C g sf →
126  ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) →
127  ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P →
128  ∃p,trace1,s2,trace2.
129    exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
130    P (gather_trace … trace1) s2 ∧
131    exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧
132    m = n + p.
133#C #g #m elim m -m
134[ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct
135  #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS
136| #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H *
137  [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ % | @AFTER ] | @EXEC1 ]| % ]
138  | #n #P #AFTER
139    cases (exec_steps_S … EXEC1)
140    #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2
141    cases (after_1_of_n_steps … AFTER)
142    #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2
143    >STEP in STEP'; #E destruct
144    cases (IH … EXEC2 … AFTER2)
145    [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E
146      %{p} % [2: %{s2} %{trace2} % [ % [ %
147       [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); % | skip ]
148      | @P2 ]| @EXEC2 ]| >E % ] | skip ]
149    | @H assumption
150    | assumption
151    | assumption
152    ]
153  ]
154] qed.
155
156lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf.
157  exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
158  ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P →
159  ∃trace1,s2,trace2.
160    exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
161    P (gather_trace … trace1) s2 ∧
162    exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉.
163#C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1
164cases (exec_steps_S … EXEC1)
165#NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2
166%{[〈s1,tr〉]} %{s2} %{tl} % [ %
167 [ whd in ⊢ (??%?); >NF1 >STEP % | whd in AFTER1; >NF1 in AFTER1; >STEP normalize
168 cases (inv s2) // * ]| // ]
169qed.
170*)
171(* XXX do I need to do the max_stack reasoning here?  perhaps just by preserving
172   observables? *)
173
174lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'.
175  exec_steps 1 O I fx g s = OK ? 〈trace,s'〉 →
176  ∃tr. trace = [〈s,tr〉].
177#O #I #fx #g #s #trace #s' #EXEC
178cases (exec_steps_S … EXEC)
179#nf * #tr * #s'' * #tl * * #E1 #STEP #EXEC' whd in EXEC':(??%%); destruct
180%{tr} %
181qed.
182
183lemma all_1 : ∀A.∀P:A → bool.∀x.
184  P x = all A P [x].
185#A #P #x whd in ⊢ (???%); cases (P x) //
186qed.
187
188(* WIP commented out*)
189lemma prefix_preserved :
190  ∀MS:meas_sim.
191  ∀g,g'.
192  ∀INV:ms_inv MS g g'.
193  ∀s1,s1'.
194  ms_rel MS g g' INV s1 s1' →
195
196  ∀m,prefix,sf.
197  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
198  pcs_labelled (ms_C1 MS) g sf →
199
200  ∃m',prefix',sf'.
201    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
202
203    intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧
204    ms_rel MS g g' INV sf sf'.
205* #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init
206#g #g' #INV #s1 #s1' #REL
207#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
208generalize in match [ ]; (* current call stack *)
209elim m0
210[ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
211  %{0} %{[]} %{s1'}
212  % [ % // | // ]
213| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf
214  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
215  cases (true_or_false_Prop … (pcs_labelled … s1))
216  [ #CS
217    lapply (sim_cost … REL CS STEP1)
218    #AFTER1'
219    cases (after_n_exec_steps … AFTER1')
220    #prefix' * #s2' * * #EXEC1' #_ * #Etrace #R2
221    cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1
222    cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1'
223    cases (IH current_stack … R2 … EXEC2 CSf)
224    #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
225    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
226    % [ % [ @(exec_steps_join … EXEC1') @EXEC''
227      | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) //
228        cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct
229        <all_1 assumption
230      ]| assumption
231      ]
232 
233  | #NCS
234    cases (true_or_false_Prop (pnormal_state C1 g s1))
235    [ #NORMAL
236      (* XXX should set things up so that notb_Prop isn't needed *)
237      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
238      #n' #AFTER1'
239      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
240      cases (IH current_stack … R2 … EXEC2 CSf)
241      #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
242      %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
243      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
244        | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
245          [ assumption
246          | cases prefix' in EXEC1' INV ⊢ %;
247            [ //
248            | * #sx #trx #tl #EXEC1' #INV
249              <(exec_steps_first … EXEC1')
250              whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL
251              @INV
252            ]
253          | @OBS'' ] ]
254        | @R''
255        ]
256    | #CALLRET
257      cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return)
258      [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET;
259        lapply (no_tailcalls … s1)
260        cases (pcs_classify … s1) in CALLRET ⊢ %;
261        [ 1,3: #_ #_ /2/
262        | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??))
263        ]
264      ] * #CL
265      cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
266      [2,4: >CL %]
267      #m' #AFTER1'
268      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
269      [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %]
270      | letin next_stack ≝ (tail … current_stack)
271      ]
272      cases (IH next_stack … R2 … EXEC2 CSf)
273      #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''
274      %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
275      % [1,3: % [1,3: @(exec_steps_join … EXEC1') @EXEC''
276        | destruct cases (exec_steps_S … EXEC1')
277          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
278          destruct
279          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
280          [1,3: whd in match (cs_classify ??); >CL %
281          |2,4: whd in match (cs_classify ??); <(rel_classify … REL) >CL %
282          | @INV
283          | assumption
284          | @(rel_callee … REL)
285          ]
286        | destruct cases (exec_steps_S … EXEC1')
287          #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'
288          destruct
289          @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
290          [ whd in match (cs_classify ??); >CL %
291          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
292          | @INV
293          | assumption
294          ]
295        ]
296      | 2,4: @R''
297      ]
298    ]
299  ]
300] qed.
301       
302     
303
304theorem measured_subtrace_preserved :
305  ∀MS:meas_sim.
306  ∀p1,p2,m,n,stack_cost,max.
307  ms_compiled MS p1 p2 →
308  measurable (ms_C1 MS) p1 m n stack_cost max →
309  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
310
Note: See TracBrowser for help on using the repository browser.