source: src/common/FEMeasurable.ma @ 2670

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

Clean up from recent commits.

File size: 11.3 KB
Line 
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
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
14(* A record giving the languages and simulation results necessary to show that
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    *)
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;
25  ms_inv : ? → ? → Type[0];
26  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
27  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
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);
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
36  sim_normal :
37    ∀g1,g2.
38    ∀INV:ms_inv g1 g2.
39    ∀s1,s1'.
40    ms_rel g1 g2 INV s1 s1' →
41    normal_state ms_C1 g1 s1 →
42    ¬ pcs_labelled ms_C1 g1 s1 →
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〉) ∧
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.
51    ∀s1,s1'.
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 →
55    ∃s2,tr. after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) ∧
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
81lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
82  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
83  normal_state C g s1 →
84  stack_after (pcs_to_cs C g stack) current trace = current.
85#C #g #s1 #trace #s2 #stack #current #EXEC
86cases (exec_steps_S … EXEC)
87#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
88#N
89whd in ⊢ (??%?); generalize in match (cs_stack ??);
90whd in match (cs_classify ??);
91cases (normal_state_inv … N)
92#CL >CL #f %
93qed.
94
95lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
96  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
97  normal_state C g s1 →
98  max_stack (pcs_to_cs C g stack) current trace = current.
99#C #g #s1 #trace #s2 #stack #current #EXEC
100cases (exec_steps_S … EXEC)
101#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
102#N
103whd in ⊢ (??%?); generalize in match (cs_stack ??);
104whd in match (cs_classify ??);
105cases (normal_state_inv … N)
106#CL >CL #f %
107qed.
108
109lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf.
110  exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
111  ¬pcs_labelled C g s1 →
112  pcs_labelled C g sf →
113  ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) →
114  ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P →
115  ∃p,trace1,s2,trace2.
116    exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
117    P (gather_trace … trace1) s2 ∧
118    exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧
119    m = n + p.
120#C #g #m elim m -m
121[ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct
122  #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS
123| #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H *
124  [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ % | @AFTER ] | @EXEC1 ]| % ]
125  | #n #P #AFTER
126    cases (exec_steps_S … EXEC1)
127    #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2
128    cases (after_1_of_n_steps … AFTER)
129    #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2
130    >STEP in STEP'; #E destruct
131    cases (IH … EXEC2 … AFTER2)
132    [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E
133      %{p} % [2: %{s2} %{trace2} % [ % [ %
134       [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); % | skip ]
135      | @P2 ]| @EXEC2 ]| >E % ] | skip ]
136    | @H assumption
137    | assumption
138    | assumption
139    ]
140  ]
141] qed.
142
143lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf.
144  exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
145  ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P →
146  ∃trace1,s2,trace2.
147    exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
148    P (gather_trace … trace1) s2 ∧
149    exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉.
150#C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1
151cases (exec_steps_S … EXEC1)
152#NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2
153%{[〈s1,tr〉]} %{s2} %{tl} % [ %
154 [ whd in ⊢ (??%?); >NF1 >STEP % | whd in AFTER1; >NF1 in AFTER1; >STEP normalize
155 cases (inv s2) // * ]| // ]
156qed.
157
158(* XXX do I need to do the max_stack reasoning here?  perhaps just by preserving
159   observables? *)
160
161
162(* WIP commented out*)
163lemma prefix_preserved :
164  ∀MS:meas_sim.
165  ∀g,g'.
166  ∀INV:ms_inv MS g g'.
167  ∀max_allowed_stack.
168  ∀s1,s1'.
169  ms_rel MS g g' INV s1 s1' →
170
171  ∀m,prefix,sf.
172  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
173  pcs_labelled (ms_C1 MS) g sf →
174  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack →
175
176  ∃m',prefix',sf'.
177    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
178    le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) 0 prefix') max_allowed_stack ∧
179 
180    ms_rel MS g g' INV sf sf'.
181* #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
182#g #g' #INV #max #s1 #s1' #REL
183#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
184generalize in match 0; (* current stack level *)
185@(nat_elim1 m0)
186*
187[ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
188  #max_ok %{0} %{[]} %{s1'}
189  % [ % // | // ]
190| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #MAX_OK
191  cases (true_or_false_Prop … (pcs_labelled … s1))
192  [ #CS
193    cases (exec_steps_split 1 … EXEC) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1
194    lapply (sim_cost … s2 ? REL CS ?)
195    [ @(exec_steps_after_n_noinv … EXEC1) % | skip ]
196    #AFTER'
197    cases (after_n_exec_steps … AFTER')
198    #prefix' * #s2' * #EXEC1' * #Etrace #R2
199    cut (normal_state C1 g s1) [ @(proj1 … (labelled_normal1 …)) assumption ] #N1
200    cut (normal_state C2 g' s1') [ @(proj1 … (labelled_normal2 …)) @(proj1 … (rel_labelled … REL)) assumption ] #N1'
201    cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
202    [ 2: // | 3: @(transitive_le … MAX_OK) >E1 <max_stack_append
203      >(stack_normal_step … EXEC1 N1)
204      >(stack_normal_step … EXEC1' N1')
205      @max_r //
206    ]
207    #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
208    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
209    % [ % [ @(exec_steps_join … EXEC1') @EXEC''
210      | <max_stack_append @to_max
211        [ >(max_stack_normal_step … EXEC1' N1')
212          lapply MAX_OK >E1 <max_stack_append
213          >(max_stack_normal_step … EXEC1 N1)
214          #H /2 by le_maxl/
215        | @MAX'' ] ]
216      | @R''
217      ]
218 
219  | #NCS
220    cases (true_or_false_Prop (normal_state C1 g s1))
221    [ #NORMAL
222      (* XXX should set things up so that notb_Prop isn't needed *)
223      cases (sim_normal … REL NORMAL (notb_Prop … NCS))
224      #n * #s2x * #tr * #AFTER * #n' #AFTER'
225      cases (exec_split … EXEC (notb_Prop … NCS) CSf … AFTER)
226      [ 2: #s #H cases (andb_Prop_true … H) // ]
227      #p * #trace1 * #s2 * #trace2 * * * #EXEC1 #E2 #EXEC2 #Esplit destruct
228      cases (after_n_exec_steps … AFTER') #prefix' * #s2' * #EXEC1' * #Etrace #R2
229      cases (IH p ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
230      [ 2: /2/ | 3: cases daemon ] (* XXX *)
231      #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
232      %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
233      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
234        | <max_stack_append @to_max
235          [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1')
236            lapply MAX_OK >E1 <max_stack_append
237            >(max_stack_normal_step … EXEC1 N1)
238            #H /2 by le_maxl/*)
239          | @MAX'' ] ]
240        | @R''
241        ]
242    | #CALLRET
243      cases (sim_call_return … REL … (notb_Prop … NCS))
244      [ 2: whd in CALLRET:(?%); whd in match (normal_state ???) in CALLRET;
245        lapply (no_tailcalls … s1)
246        cases (pcs_classify … s1) in CALLRET ⊢ %;
247        normalize * #H #H' try % try cases (H I)
248        cases H' /2/ ]
249      #s2 * #tr2 * #AFTER1 * #m' #AFTER1'
250      cases (exec_split1 … EXEC … AFTER1)
251      #trace1 * #s2x * #trace2 * * #EXEC1 #E2 #EXEC2 destruct
252      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * #Etrace #R2
253      cases (IH ?? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
254      [ 2: /2/ | 3: cases daemon ] (* XXX *)
255      #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
256      %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
257      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
258        | <max_stack_append @to_max
259          [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1')
260            lapply MAX_OK >E1 <max_stack_append
261            >(max_stack_normal_step … EXEC1 N1)
262            #H /2 by le_maxl/*)
263          | @MAX'' ] ]
264        | @R''
265        ]
266    ]
267  ]
268qed.
269       
270     
271
272theorem measured_subtrace_preserved :
273  ∀MS:meas_sim.
274  ∀p1,p2,m,n,stack_cost,max.
275  ms_compiled MS p1 p2 →
276  measurable (ms_C1 MS) p1 m n stack_cost max →
277  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
278
Note: See TracBrowser for help on using the repository browser.