source: src/common/FEMeasurable.ma @ 2669

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

Tweak exec_steps output; show that simulations extend to measurable
subtrace prefixes.

File size: 14.5 KB
RevLine 
[2597]1(* Show that measurable subtraces are preserved in the front-end. *)
2
3include "common/Measurable.ma".
4
5definition normal_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
[2669]8lemma normal_state_inv : ∀C,g,s.
9  normal_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
[2597]14(* A record giving the languages and simulation results necessary to show that
[2669]15   measurability is preserved.
16   
17   Note: as we're interested in measurable subtraces, we don't have to worry
18   about the execution "going wrong."
19    *)
[2597]20
21record meas_sim : Type[2] ≝ {
22  ms_C1 : preclassified_system;
23  ms_C2 : preclassified_system;
24  ms_compiled : program … ms_C1 → program … ms_C2 → Prop;
[2618]25  ms_inv : ? → ? → Type[0];
26  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
[2597]27  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
[2668]28  ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (normal_state ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C2 g2 s2);
29  ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (pcs_labelled ms_C2 g2 s2);
[2669]30
31  (* These hold in (at least) the languages of interest for measurable subtraces *)
32  ms_labelled_normal_1 : ∀g1,s1. bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C1 g1 s1);
33  ms_labelled_normal_2 : ∀g2,s2. bool_to_Prop (pcs_labelled ms_C2 g2 s2) ↔ bool_to_Prop (normal_state ms_C2 g2 s2);
34  ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall;
35
[2597]36  sim_normal :
37    ∀g1,g2.
38    ∀INV:ms_inv g1 g2.
[2669]39    ∀s1,s1'.
[2597]40    ms_rel g1 g2 INV s1 s1' →
41    normal_state ms_C1 g1 s1 →
42    ¬ pcs_labelled ms_C1 g1 s1 →
[2669]43    ∃n,s2,tr. after_n_steps (S n) … (pcs_exec ms_C1) g1 s1 (λs.normal_state ms_C1 g1 s ∧ ¬ pcs_labelled ms_C1 g1 s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) ∧
[2597]44    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
45      tr = tr' ∧
46      ms_rel g1 g2 INV s2 s2'
47    );
48  sim_call_return :
49    ∀g1,g2.
50    ∀INV:ms_inv g1 g2.
[2669]51    ∀s1,s1'.
[2597]52    ms_rel g1 g2 INV s1 s1' →
53    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
54    ¬ pcs_labelled ms_C1 g1 s1 →
[2669]55    ∃s2,tr. after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) ∧
[2597]56    ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
57      tr = tr' ∧
58      ms_rel g1 g2 INV s2 s2'
59    );
60  sim_cost :
61    ∀g1,g2.
62    ∀INV:ms_inv g1 g2.
63    ∀s1,s1',s2,tr.
64    ms_rel g1 g2 INV s1 s1' →
65    pcs_labelled ms_C1 g1 s1 →
66    after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
67    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
68      tr = tr' ∧
69      ms_rel g1 g2 INV s2 s2'
70    );
71  sim_init :
72    ∀p1,p2,s,s'.
73    ms_compiled p1 p2 →
74    make_initial_state ?? ms_C1 p1 = OK ? s →
75    make_initial_state ?? ms_C2 p2 = OK ? s' →
76    ∃INV. ms_rel ?? INV s s'
77}.
78
79(* TODO: obs eq *)
80
81definition trace_starts : ∀S. execution S io_out io_in → S → Prop ≝
82λS,t,s. match t with [ e_step _ s' _ ⇒ s = s' | _ ⇒ False ].
83
[2644]84(* TODO: too many of these lemmas, slim it down*)
85
86lemma split_trace_S : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
87  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S n) = Some ? 〈a,b〉 →
88  ∃a'. a = 〈tr,s〉::a' ∧
89  ((is_final … fx g s = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s)) n = Some ? 〈a',b〉) ∨
90  (∃r. is_final … fx g s = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s)).
91#fx #g #tr #s #n #a #b
92>exec_inf_aux_unfold whd in ⊢ (??(????%?)? → ?);
93cases (is_final … s)
94[ whd in ⊢ (??%? → ?); cases (split_trace ?????)
95  [ #E whd in E:(??%%); destruct
96  | * #a' #b' #E whd in E:(??%%); destruct
97    %{a'} %{(refl ??)} %1 %{(refl ??)} %
98  ]
99| #r cases n [2:#n'] whd in ⊢ (??%? → ?); #E destruct
100  %{[ ]} %{(refl ??)} %2 %{r} /4/
101] qed.
102
103lemma split_trace_S' : ∀fx:trans_system io_out io_in. ∀g,s,n,a,b.
104  split_trace … (exec_inf_aux ?? fx g (step … fx g s)) (S n) = Some ? 〈a,b〉 →
105  ∃tr,s'. step … fx g s = Value … 〈tr,s'〉 ∧
106  ∃a'. a = 〈tr,s'〉::a' ∧
107  ((is_final … fx g s' = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s')) n = Some ? 〈a',b〉) ∨
108  (∃r. is_final … fx g s' = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s')).
109#fx #g #s #n #a #b
110cases (step … fx g s)
111[ #o #i whd in ⊢ (??%? → ?); #E destruct
112| * #tr #s' #split %{tr} %{s'} %{(refl …)} @split_trace_S @split
113| #err #E whd in E:(??%%); destruct
114] qed.
115
116lemma split_trace_1 : ∀fx:trans_system io_out io_in. ∀g,tr,s,a,b.
117  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) 1 = Some ? 〈a,b〉 →
118  a = [〈tr,s〉] ∧
119  ((is_final … fx g s = None ? ∧ b = exec_inf_aux ?? fx g (step … fx g s)) ∨
120  (∃r. is_final … fx g s = Some ? r ∧ b = e_stop … tr r s)).
121#fx #g #tr #s #a #b #split
122cases (split_trace_S … split)
123#a' * #E1 *
124[ * #notfinal #split' whd in split':(??%?); destruct %{(refl ??)}
125  %1 %{notfinal} %
126| * #r * * * #final #_ #E2 #E3 destruct %{(refl ??)}
127  %2 %{r} %{final} %
128] qed.
129 
130
131lemma split_trace_SS : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
132  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S (S n)) = Some ? 〈a,b〉 →
133  ∃a'. a = 〈tr,s〉::a' ∧
134  is_final … fx g s = None ? ∧
135  ∃tr',s'. step … fx g s = Value … 〈tr',s'〉 ∧
136  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr',s'〉)) (S n) = Some ? 〈a',b〉.
137#fx #g #tr #s #n #a #b #splitSS
138cases (split_trace_S … splitSS)
139#a' * #E1 *
140[ * #notfinal #splitS %{a'} % [ %{E1} @notfinal ]
141  cases (step … s) in splitS ⊢ %;
142  [ #o #i #E whd in E:(??%%); destruct
143  | * #tr' #s' #splitS %{tr'} %{s'} %{(refl ??)} @splitS
144  | #m  #E whd in E:(??%%); destruct
145  ]
146| * #r * * * #final #En #Ea #Eb destruct
147] qed.
148
[2669]149lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
[2668]150  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
[2669]151  normal_state C g s1 →
[2668]152  stack_after (pcs_to_cs C g stack) current trace = current.
153#C #g #s1 #trace #s2 #stack #current #EXEC
154cases (exec_steps_S … EXEC)
155#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
[2669]156#N
157whd in ⊢ (??%?); generalize in match (cs_stack ??);
158whd in match (cs_classify ??);
159cases (normal_state_inv … N)
160#CL >CL #f %
161qed.
[2668]162
[2669]163lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
164  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
165  normal_state C g s1 →
166  max_stack (pcs_to_cs C g stack) current trace = current.
167#C #g #s1 #trace #s2 #stack #current #EXEC
168cases (exec_steps_S … EXEC)
169#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
170#N
171whd in ⊢ (??%?); generalize in match (cs_stack ??);
172whd in match (cs_classify ??);
173cases (normal_state_inv … N)
174#CL >CL #f %
175qed.
[2668]176
[2669]177lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf.
178  exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
179  ¬pcs_labelled C g s1 →
180  pcs_labelled C g sf →
181  ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) →
182  ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P →
183  ∃p,trace1,s2,trace2.
184    exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
185    P (gather_trace … trace1) s2 ∧
186    exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧
187    m = n + p.
188#C #g #m elim m -m
189[ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct
190  #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS
191| #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H *
192  [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ % | @AFTER ] | @EXEC1 ]| % ]
193  | #n #P #AFTER
194    cases (exec_steps_S … EXEC1)
195    #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2
196    cases (after_1_of_n_steps … AFTER)
197    #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2
198    >STEP in STEP'; #E destruct
199    cases (IH … EXEC2 … AFTER2)
200    [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E
201      %{p} % [2: %{s2} %{trace2} % [ % [ %
202       [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); % | skip ]
203      | @P2 ]| @EXEC2 ]| >E % ] | skip ]
204    | @H assumption
205    | assumption
206    | assumption
207    ]
208  ]
209] qed.
210
211lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf.
212  exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
213  ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P →
214  ∃trace1,s2,trace2.
215    exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
216    P (gather_trace … trace1) s2 ∧
217    exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉.
218#C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1
219cases (exec_steps_S … EXEC1)
220#NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2
221%{[〈s1,tr〉]} %{s2} %{tl} % [ %
222 [ whd in ⊢ (??%?); >NF1 >STEP % | whd in AFTER1; >NF1 in AFTER1; >STEP normalize
223 cases (inv s2) // * ]| // ]
224qed.
225
226(* XXX do I need to do the max_stack reasoning here?  perhaps just by preserving
227   observables? *)
228
229
[2668]230(* WIP commented out*)
[2597]231lemma prefix_preserved :
232  ∀MS:meas_sim.
[2668]233  ∀g,g'.
234  ∀INV:ms_inv MS g g'.
[2597]235  ∀max_allowed_stack.
[2668]236  ∀s1,s1'.
237  ms_rel MS g g' INV s1 s1' →
[2644]238
[2668]239  ∀m,prefix,sf.
240  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
[2669]241  pcs_labelled (ms_C1 MS) g sf →
[2668]242  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack →
243
244  ∃m',prefix',sf'.
245    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
246    le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) 0 prefix') max_allowed_stack ∧
[2644]247 
[2668]248    ms_rel MS g g' INV sf sf'.
[2669]249* #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #labelled_normal1 #labelled_normal2 #no_tailcalls #sim_normal #sim_call_return #sim_cost #sim_init
[2668]250#g #g' #INV #max #s1 #s1' #REL
251#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
252generalize in match 0; (* current stack level *)
[2644]253@(nat_elim1 m0)
254*
[2669]255[ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
[2668]256  #max_ok %{0} %{[]} %{s1'}
257  % [ % // | // ]
[2669]258| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #MAX_OK
[2644]259  cases (true_or_false_Prop … (pcs_labelled … s1))
[2668]260  [ #CS
[2669]261    cases (exec_steps_split 1 … EXEC) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1
[2668]262    lapply (sim_cost … s2 ? REL CS ?)
263    [ @(exec_steps_after_n_noinv … EXEC1) % | skip ]
264    #AFTER'
265    cases (after_n_exec_steps … AFTER')
266    #prefix' * #s2' * #EXEC1' * #Etrace #R2
[2669]267    cut (normal_state C1 g s1) [ @(proj1 … (labelled_normal1 …)) assumption ] #N1
268    cut (normal_state C2 g' s1') [ @(proj1 … (labelled_normal2 …)) @(proj1 … (rel_labelled … REL)) assumption ] #N1'
269    cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
270    [ 2: // | 3: @(transitive_le … MAX_OK) >E1 <max_stack_append
271      >(stack_normal_step … EXEC1 N1)
272      >(stack_normal_step … EXEC1' N1')
273      @max_r //
274    ]
[2668]275    #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
276    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
[2669]277    % [ % [ @(exec_steps_join … EXEC1') @EXEC''
278      | <max_stack_append @to_max
279        [ >(max_stack_normal_step … EXEC1' N1')
280          lapply MAX_OK >E1 <max_stack_append
281          >(max_stack_normal_step … EXEC1 N1)
282          #H /2 by le_maxl/
283        | @MAX'' ] ]
284      | @R''
285      ]
286 
287  | #NCS
288    cases (true_or_false_Prop (normal_state C1 g s1))
289    [ #NORMAL
290      (* XXX should set things up so that notb_Prop isn't needed *)
291      cases (sim_normal … REL NORMAL (notb_Prop … NCS))
292      #n * #s2x * #tr * #AFTER * #n' #AFTER'
293      cases (exec_split … EXEC (notb_Prop … NCS) CSf … AFTER)
294      [ 2: #s #H cases (andb_Prop_true … H) // ]
295      #p * #trace1 * #s2 * #trace2 * * * #EXEC1 #E2 #EXEC2 #Esplit destruct
296      cases (after_n_exec_steps … AFTER') #prefix' * #s2' * #EXEC1' * #Etrace #R2
297      cases (IH p ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
298      [ 2: /2/ | 3: cases daemon ] (* XXX *)
299      #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
300      %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
301      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
302        | <max_stack_append @to_max
303          [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1')
304            lapply MAX_OK >E1 <max_stack_append
305            >(max_stack_normal_step … EXEC1 N1)
306            #H /2 by le_maxl/*)
307          | @MAX'' ] ]
308        | @R''
309        ]
310    | #CALLRET
311      cases (sim_call_return … REL … (notb_Prop … NCS))
312      [ 2: whd in CALLRET:(?%); whd in match (normal_state ???) in CALLRET;
313        lapply (no_tailcalls … s1)
314        cases (pcs_classify … s1) in CALLRET ⊢ %;
315        normalize * #H #H' try % try cases (H I)
316        cases H' /2/ ]
317      #s2 * #tr2 * #AFTER1 * #m' #AFTER1'
318      cases (exec_split1 … EXEC … AFTER1)
319      #trace1 * #s2x * #trace2 * * #EXEC1 #E2 #EXEC2 destruct
320      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * #Etrace #R2
321      cases (IH ?? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
322      [ 2: /2/ | 3: cases daemon ] (* XXX *)
323      #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
324      %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
325      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
326        | <max_stack_append @to_max
327          [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1')
328            lapply MAX_OK >E1 <max_stack_append
329            >(max_stack_normal_step … EXEC1 N1)
330            #H /2 by le_maxl/*)
331          | @MAX'' ] ]
332        | @R''
333        ]
334    ]
335  ]
336qed.
337       
338     
[2668]339
[2597]340theorem measured_subtrace_preserved :
341  ∀MS:meas_sim.
342  ∀p1,p2,m,n,stack_cost,max.
343  ms_compiled MS p1 p2 →
344  measurable (ms_C1 MS) p1 m n stack_cost max →
345  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
346* #C1 #C2 #compiled #inv #rel #sim_normal #sim_call_return #sim_cost #sim_init
347#p1 #p2 #m #n #stack_cost #max #compiled
348whd in ⊢ (% → ?); letin C1' ≝ (mk_classified_system C1 ????) letin g1 ≝ (make_global ?? C1 ?)
349* #prefix * #suffix * #subtrace * #remainder
350* * * * #split1 #split2 #subtrace_ok #terminates #max_ok
351
[2644]352*)
Note: See TracBrowser for help on using the repository browser.