Changeset 3115 for src/correctness.ma
 Timestamp:
 Apr 10, 2013, 1:28:46 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r3096 r3115 15 15 and those observables will include the stack space costs. 16 16 *) 17 18 definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝19 λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.20 21 let rec foldl_exists_aux (A,B:Type[0]) (l,l':list B) (f:A → ∀b:B. Exists … (λx.x=b) l → A) (a:A) on l' : (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A ≝22 match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with23 [ nil ⇒ λ_. a24  cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?25 ].26 [ %1 %27  #b #H' @H %2 @H'28 ] qed.29 30 definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝31 λA,B,l,f,a. foldl_exists_aux A B l l f a (λb,H. H).32 33 lemma Exists_lift : ∀A,P,Q,l.34 (∀x. P x → Q x) →35 Exists A P l →36 Exists A Q l.37 #A #P #Q #l elim l38 [ //39  #h #t #IH #H * [ #H' %1 @H @H'  #H' %2 @IH /2/ ]40 ] qed.41 17 42 18 include "RTLabs/MeasurableToStructured.ma". … … 197 173 #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs' 198 174 >OBS ra_meas 175 176 (* So, after the frontend we have for RTLabs: 177 ra_exec_prefix  after [ra_m1] steps we get to [ra_s1] with observables [prefix], 178 ra_tlr  structured trace from [ra_s1] to some [ra_s2], 179 ra_unrepeating  PCs don't repeat locally in [ra_tlr] 180 ra_obs'  the observables from [ra_tlr] are [subtrace] 181 ra_max  the stack bound is respected in [prefix@subtrace] 182 *) 183 199 184 cases (produce_rtlabs_flat_trace … ra_exec_prefix) 200 185 #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs … … 276 261 cut (∀p : rtlabs_program.∀n : ℕ.∀st,tr. 277 262 exec_steps_with_obs RTLabs_ext_pcs p n = return 〈st, tr〉 → 278 279 (* So, we have for RTLabs: 280 ra_exec_prefix  after [ra_m1] steps we get to [ra_s1] with observables [prefix], 281 ra_tlr  structured trace from [ra_s1] to some [ra_s2], 282 ra_unrepeating  PCs don't repeat locally in [ra_tlr] 283 ra_obs'  the observables from [ra_tlr] are [subtrace] 284 ra_max  the stack bound is respected in [prefix@subtrace] 285 *) 286 287 288 (* Old, semiformal cut 289 cut (∀n,s1,s2,obs1,obs2. 290 exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 → 291 ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2. 292 tlr_observables … tlr (function_of … s1) = obs2 → 293 (* maybe instead of function_of the called id can rather be obtained from execution? *) 294 ∃m,p,s_fin. 295 observables (OC_preclassified_system (c_labelled_object_code … p)) 296 (c_labelled_object_code … p) m p = return 〈obs1, obs2〉) 297 *) 263 298 264 299 265
Note: See TracChangeset
for help on using the changeset viewer.