Changeset 2896 for src/common


Ignore:
Timestamp:
Mar 16, 2013, 9:08:20 PM (7 years ago)
Author:
campbell
Message:

Complete part of measurable to structured subtraces proof that
shows observables are preserved.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2895 r2896  
    458458| % #E destruct
    459459] qed.
     460
     461(* For *functions* the mapping between identifiers and blocks is a bijection,
     462   but to show that we have to keep more invariants about the environment. *)
     463axiom symbol_for_block_fn : ∀F,genv,b,f,id.
     464  find_symbol F genv id = Some ? b →
     465  find_funct_ptr F genv b = Some ? f →
     466  symbol_for_block F genv b = Some ? id.
    460467
    461468(* The mapping of blocks to symbols is total for functions. *)
  • src/common/Measurable.ma

    r2800 r2896  
    4242λtr. flatten ? (map ?? intensional_event_of_event tr).
    4343
     44definition intensional_state_change ≝
     45λC,callstack,s.
     46    match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
     47    [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
     48    | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
     49    | _ ⇒ λ_. 〈callstack, [ ]〉
     50    ] (cs_callee C s).
     51
    4452let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝
    4553match trace with
     
    4755| cons str tl ⇒
    4856  let 〈s,tr〉 ≝ str in
    49   let 〈callstack, call_event〉 ≝
    50     match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
    51     [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
    52     | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
    53     | _ ⇒ λ_. 〈callstack, [ ]〉
    54     ] (cs_callee C s) in
     57  let 〈callstack, call_event〉 ≝ intensional_state_change C callstack s in
    5558  let other_events ≝ intensional_events_of_events tr in
    5659  let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in
     
    7376      〈stk', (intensional_events_of_events tr)@tl〉).
    7477#C #callstack #s #tr #trace #NORMAL
    75 whd in ⊢ (??%?);
     78whd in ⊢ (??%?); whd in match (intensional_state_change ???);
    7679generalize in match (cs_callee C s);
    7780cases (normal_state_inv … NORMAL)
     
    141144| * #s #tr #tl #IH
    142145  #callstack
    143   whd in match (intensional_trace_of_trace ???);
    144   whd in match (intensional_trace_of_trace ???);
     146  whd in match (intensional_trace_of_trace ???); whd in match (intensional_state_change ???);
     147  whd in match (intensional_trace_of_trace ???); whd in match (intensional_state_change ???);
    145148  generalize in match (cs_callee C s);
    146149  cases (cs_classify C s)
     
    185188#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E
    186189whd
    187 whd in ⊢ (??%%); normalize nodelta
     190whd in ⊢ (??%%);
     191whd in match (intensional_state_change ???);
     192whd in match (intensional_state_change C' ??);
     193normalize nodelta
    188194generalize in match (cs_callee C s); generalize in match (cs_callee C' s');
    189195>CL >CL' normalize nodelta #_ #_
     
    223229#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL
    224230whd in ⊢ (? → ? → %);
    225 whd in ⊢ (? → ? → ??%%); normalize nodelta
     231whd in ⊢ (? → ? → ??%%);
     232whd in match (intensional_state_change ???);
     233whd in match (intensional_state_change C' ??);
     234normalize nodelta
    226235@generalize_callee
    227236@generalize_callee
Note: See TracChangeset for help on using the changeset viewer.