source: src/common/FEMeasurable.ma @ 2678

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

Switch to single source step simulations for front-end measurable subtraces
results.

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