Changeset 3115


Ignore:
Timestamp:
Apr 10, 2013, 1:28:46 PM (4 years ago)
Author:
campbell
Message:

Clean up some left-over lemmas and move comment back into place.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r3096 r3115  
    1515   and those observables will include the stack space costs.
    1616 *)
    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 with
    23 [ nil ⇒ λ_. a
    24 | 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 l
    38 [ //
    39 | #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
    40 ] qed.
    4117
    4218include "RTLabs/MeasurableToStructured.ma".
     
    197173  #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
    198174  >OBS -ra_meas
     175   
     176  (* So, after the front-end 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
    199184  cases (produce_rtlabs_flat_trace … ra_exec_prefix)
    200185  #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
     
    276261  cut (∀p : rtlabs_program.∀n : ℕ.∀st,tr.
    277262    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
    298264     
    299265             
Note: See TracChangeset for help on using the changeset viewer.