Changeset 2669 for src/common/FEMeasurable.ma
 Timestamp:
 Feb 15, 2013, 11:27:58 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r2668 r2669 6 6 λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ]. 7 7 8 lemma 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/ * 12 qed. 13 8 14 (* A record giving the languages and simulation results necessary to show that 9 measurability is preserved. *) 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 *) 10 20 11 21 record meas_sim : Type[2] ≝ { … … 18 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); 19 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 20 36 sim_normal : 21 37 ∀g1,g2. 22 38 ∀INV:ms_inv g1 g2. 23 ∀s1,s1' ,s2,tr.39 ∀s1,s1'. 24 40 ms_rel g1 g2 INV s1 s1' → 25 41 normal_state ms_C1 g1 s1 → 26 42 ¬ pcs_labelled ms_C1 g1 s1 → 27 ∃n . 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〉) →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〉) ∧ 28 44 ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'. 29 45 tr = tr' ∧ … … 33 49 ∀g1,g2. 34 50 ∀INV:ms_inv g1 g2. 35 ∀s1,s1' ,s2,tr.51 ∀s1,s1'. 36 52 ms_rel g1 g2 INV s1 s1' → 37 53 match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true  cl_return ⇒ true  _ ⇒ false] → 38 54 ¬ pcs_labelled ms_C1 g1 s1 → 39 after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →55 ∃s2,tr. after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) ∧ 40 56 ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'. 41 57 tr = tr' ∧ … … 131 147 ] qed. 132 148 133 lemma stack_ labelled_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.149 lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. 134 150 exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → 135 pcs_labelledC g s1 →151 normal_state C g s1 → 136 152 stack_after (pcs_to_cs C g stack) current trace = current. 137 153 #C #g #s1 #trace #s2 #stack #current #EXEC 138 154 cases (exec_steps_S … EXEC) 139 155 #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct 140 #CS 141 whd in ⊢ (??%?); whd in match (cs_classify ??); >CS 156 #N 157 whd in ⊢ (??%?); generalize in match (cs_stack ??); 158 whd in match (cs_classify ??); 159 cases (normal_state_inv … N) 160 #CL >CL #f % 161 qed. 162 163 lemma 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 168 cases (exec_steps_S … EXEC) 169 #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct 170 #N 171 whd in ⊢ (??%?); generalize in match (cs_stack ??); 172 whd in match (cs_classify ??); 173 cases (normal_state_inv … N) 174 #CL >CL #f % 175 qed. 176 177 lemma 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 211 lemma 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 219 cases (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) // * ] // ] 224 qed. 225 226 (* XXX do I need to do the max_stack reasoning here? perhaps just by preserving 227 observables? *) 142 228 143 229 … … 153 239 ∀m,prefix,sf. 154 240 exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 → 241 pcs_labelled (ms_C1 MS) g sf → 155 242 le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack → 156 243 … … 160 247 161 248 ms_rel MS g g' INV sf sf'. 162 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled # sim_normal #sim_call_return #sim_cost #sim_init249 * #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 163 250 #g #g' #INV #max #s1 #s1' #REL 164 251 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' … … 166 253 @(nat_elim1 m0) 167 254 * 168 [ #_ #current_stack #s1 #s1' #REL #prefix #sf # exec whd in exec:(??%?); destruct255 [ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf 169 256 #max_ok %{0} %{[]} %{s1'} 170 257 % [ % //  // ] 171  #m #IH #current_stack #s1 #s1' #REL #prefix #sf # exec #max_ok258  #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #MAX_OK 172 259 cases (true_or_false_Prop … (pcs_labelled … s1)) 173 260 [ #CS 174 cases (exec_steps_split 1 … exec) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1261 cases (exec_steps_split 1 … EXEC) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1 175 262 lapply (sim_cost … s2 ? REL CS ?) 176 263 [ @(exec_steps_after_n_noinv … EXEC1) %  skip ] … … 178 265 cases (after_n_exec_steps … AFTER') 179 266 #prefix' * #s2' * #EXEC1' * #Etrace #R2 180 cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 ?) 181 [ 2: //  3: @(transitive_le … max_ok) >E1 <max_stack_append 182 183 @le_maxr 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 ] 184 275 #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R'' 185 276 %{(1+m'')} %{(prefix'@prefix'')} %{sf''} 186 % [ % [ @(exec_steps_join … EXEC1') @EXEC''  cases daemon ]  @R2 187  188 %{trace1 } 189 190 cases (exec_steps_S … exec) #notfinal * #tr' * #s' * #tl * * #E #STEP #EXEC' 191 cases (true_or_false_Prop … (pcs_labelled … s1)) 192 [ #CS lapply (sim_cost … s' tr' REL CS ?) 193 [ @(exec_steps_after_n_noinv … whd >notfinal whd >STEP whd % ] 194 #AFTER %{1} 195 [ 3: whd in match (after_n_steps ????? s1 ??); 196 >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?); 197 lapply (refl ? (pcs_classify … s1)) cases (pcs_classify … s1) in ⊢ (???% → ?); 198 [ 199  #CL 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 ] 336 qed. 337 338 200 339 201 340 theorem measured_subtrace_preserved :
Note: See TracChangeset
for help on using the changeset viewer.