Changeset 3031


Ignore:
Timestamp:
Mar 29, 2013, 12:38:41 PM (4 years ago)
Author:
campbell
Message:

Tidy up RTLabs preclassified_system definitions.

Location:
src/RTLabs
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2948 r3031  
    33include "common/Measurable.ma".
    44include "common/stacksize.ma".
    5 
    6 definition RTLabs_stack_ident :
    7   genv →
    8   ∀s:state.
    9   match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
    10   ident ≝
    11 λge,s.
    12 match s return λs. match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with
    13 [ Callstate id _ _ _ _ _ ⇒ λ_. id
    14 | State f fs m ⇒ λH.⊥
    15 | _ ⇒ λH.⊥
    16 ].
    17 try @H
    18 whd in match (RTLabs_classify ?) in H;
    19 cases (next_instruction f) in H;
    20 normalize //
    21 qed.
    22 
    23 definition RTLabs_pcsys ≝ mk_preclassified_system
    24   RTLabs_fullexec
    25   (λ_.RTLabs_cost)
    26   (λ_.RTLabs_classify)
    27   RTLabs_stack_ident.
     5include "RTLabs/RTLabs_classified_system.ma".
    286
    297definition state_at : ∀C:preclassified_system.
     
    3715  return s1.
    3816
    39 definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝
    40 λge,s.
    41 match eval_statement ge s return λx. (∀s',t. x = Value ??? 〈t,s'〉 → RTLabs_ext_state ge) → ? with
    42 [ Value ts ⇒ λnext. Value ??? 〈\fst ts, next (\snd ts) (\fst ts) ?〉
    43 | Wrong m ⇒ λ_. Wrong ??? m
    44 | Interact o k ⇒ λ_. Wrong … (msg UnexpectedIO)
    45 ] (next_state ge s).
    46 //
    47 qed.
    48 
    49 lemma drop_exec_ext : ∀ge,s,tr,s'.
    50   eval_ext_statement ge s = return 〈tr,s'〉 →
    51   eval_statement ge s = return 〈tr,Ras_state … s'〉.
    52 #ge #s #tr #s'
    53 whd in ⊢ (??%? → ?);
    54 letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
    55 cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
    56 [ // ]
    57 generalize in match f; -f
    58 cases (eval_statement ge s)
    59 [ #o #k #n #N #E whd in E:(??%%); destruct
    60 | * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //
    61 | #m #n #N #E whd in E:(??%%); destruct
    62 ] qed.
    63 
    64 lemma as_eval_ext_statement : ∀ge,s,tr,s'.
    65   eval_ext_statement ge s = Value … 〈tr,s'〉 →
    66   as_execute (RTLabs_status ge) s s'.
    67 #ge #s #tr #s' #EX
    68 whd %{tr} %{(drop_exec_ext … EX)}
    69 whd in EX:(??%?);
    70 letin ns ≝ (next_state ge s) in EX; #EX
    71 change with (ns s' tr ?) in match (next_state ge s s' tr ?);
    72 generalize in match (drop_exec_ext ?????);
    73 #EX'
    74 generalize in match ns in EX ⊢ %; -ns >EX' #ns whd in ⊢ (??%? → %);
    75 #E destruct @e1
    76 qed.
    77 
    78 definition RTLabs_ext_exec : trans_system io_out io_in ≝
    79   mk_trans_system io_out io_in ? RTLabs_ext_state (λ_.RTLabs_is_final) eval_ext_statement.
    80 
    81 definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝
    82 λp.
    83   let ge ≝ make_global p in
    84   do m ← init_mem … (λx.x) p;
    85   let main ≝ prog_main ?? p in
    86   do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
    87   do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
    88   let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
    89   return (mk_RTLabs_ext_state (make_global p) s [b] ?).
    90 % [ % assumption | % ]
    91 qed.
    92 
    93 lemma initial_states_OK : ∀p,s.
    94   make_ext_initial_state p = return s →
    95   make_initial_state p = return (Ras_state … s).
    96 #p #s #E
    97 cases (bind_inversion ????? E) -E #m * #E1 #E
    98 cases (bind_as_inversion ????? E) -E #b * #Eb #E
    99 cases (bind_as_inversion ????? E) -E #f * #Ef #E
    100 whd in ⊢ (??%?); >E1
    101 whd in ⊢ (??%?); >Eb
    102 whd in ⊢ (??%?); >Ef
    103 whd in E:(??%%) ⊢ (??%?); destruct
    104 %
    105 qed.
    106 
    107 lemma initial_states_OK' : ∀p,s.
    108   make_initial_state p = return s →
    109   ∃S,M. make_ext_initial_state p = return (mk_RTLabs_ext_state (make_global p) s S M).
    110 #p #s #E
    111 cases (bind_inversion ????? E) -E #m * #E1 #E
    112 cases (bind_inversion ????? E) -E #b * #Eb #E
    113 cases (bind_inversion ????? E) -E #f * #Ef #E
    114 whd in E:(??%%); destruct
    115 %{[b]} % [ % [ % assumption | % ] ]
    116 whd in ⊢ (??%?); >E1
    117 whd in ⊢ (??%?); generalize in match (refl ??);
    118 >Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb'
    119 whd in ⊢ (??%?); generalize in match (refl ??);
    120 >Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
    121 qed.
    122 
    123 
    124 definition RTLabs_ext_fullexec : fullexec io_out io_in ≝
    125   mk_fullexec … RTLabs_ext_exec make_global make_ext_initial_state.
    126 
    127 definition RTLabs_ext_pcsys ≝ mk_preclassified_system
    128   RTLabs_ext_fullexec
    129   (λg,s. RTLabs_cost (Ras_state … s))
    130   (λg,s. RTLabs_classify (Ras_state … s))
    131   (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H).
    132 
    13317lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX.
    134   will_return_aux (pcs_to_cs … RTLabs_pcsys ge) depth trace →
     18  will_return_aux (pcs_to_cs … RTLabs_pcs ge) depth trace →
    13519  ΣWR:will_return ge depth s (make_flat_trace ge n s trace s' EX).
    13620    will_return_end … WR = ?.
     
    20993
    21094lemma intensional_state_change_State : ∀ge,cs,f,fs,m.
    211   intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (State f fs m) = 〈cs,[ ]〉.
     95  intensional_state_change (pcs_to_cs … RTLabs_pcs ge) cs (State f fs m) = 〈cs,[ ]〉.
    21296#ge #cs #f #fs #m
    21397whd in ⊢ (??%?);
     
    231115  ∃S',M'.
    232116    eval_ext_statement ge s = Value … 〈tr,mk_RTLabs_ext_state … s' S' M'〉 ∧
    233     All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S' (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s')).
     117    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S' (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcs ge) cs s')).
    234118#ge #s #tr #s' #cs #EV #STACK
    235119whd in match (eval_ext_statement ??);
     
    282166
    283167lemma callee_ext : ∀ge,s,S,M.
    284   cs_callee (pcs_to_cs RTLabs_pcsys ge) s = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) (mk_RTLabs_ext_state ge s S M).
     168  cs_callee (pcs_to_cs RTLabs_pcs ge) s = cs_callee (pcs_to_cs RTLabs_ext_pcs ge) (mk_RTLabs_ext_state ge s S M).
    285169#ge * //
    286170qed.
    287171
    288172lemma int_state_change_ext : ∀ge,cs,s,S,M.
    289   intensional_state_change (pcs_to_cs RTLabs_pcsys ge) cs s =
    290   intensional_state_change (pcs_to_cs RTLabs_ext_pcsys ge) cs (mk_RTLabs_ext_state ge s S M).
     173  intensional_state_change (pcs_to_cs RTLabs_pcs ge) cs s =
     174  intensional_state_change (pcs_to_cs RTLabs_ext_pcs ge) cs (mk_RTLabs_ext_state ge s S M).
    291175#ge #cs #s #S #M
    292176whd in ⊢ (??%%);
     
    296180lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs,cs',itrace.
    297181  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
    298   intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs trace = 〈cs',itrace〉 →
    299   All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (Ras_state … s))) →
     182  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ge) cs trace = 〈cs',itrace〉 →
     183  All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcs ge) cs (Ras_state … s))) →
    300184  ∃trace',S,M.
    301185    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
    302     intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs trace' = 〈cs',itrace〉 ∧
    303     All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
     186    intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcs ge) cs trace' = 〈cs',itrace〉 ∧
     187    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcs ge) cs' s')).
    304188#ge #n0 elim n0
    305189[ * #s #S #M #trace #s' #cs #cs' #itrace #E whd in E:(??%%); destruct
     
    333217lemma extend_initial_RTLabs_exec_steps : ∀p. let ge ≝ make_global p in ∀n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs',itrace.
    334218  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
    335   intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) [ ] trace = 〈cs',itrace〉 →
     219  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ge) [ ] trace = 〈cs',itrace〉 →
    336220  make_ext_initial_state p = OK ? s →
    337221  ∃trace',S,M.
    338222    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
    339     intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) [ ] trace' = 〈cs',itrace〉 ∧
    340     All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
     223    intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcs ge) [ ] trace' = 〈cs',itrace〉 ∧
     224    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcs ge) cs' s')).
    341225#p #n #s #trace #s' #cs' #itrace #EXEC #ITOT #INIT
    342226@(extend_RTLabs_exec_steps … EXEC ITOT)
     
    589473
    590474lemma as_call_cs_callee : ∀ge,s,CL,CL'.
    591   as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_pcsys ge) (Ras_state … s) CL'.
     475  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_pcs ge) (Ras_state … s) CL'.
    592476#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
    593477destruct %
     
    610494  as_classifier (RTLabs_status ge) s cl_other →
    611495  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
    612   intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs (〈Ras_state … s,tr〉::rem) = 〈cs',obs〉 →
     496  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ge) cs (〈Ras_state … s,tr〉::rem) = 〈cs',obs〉 →
    613497  ∃obs'.
    614498    obs = (intensional_events_of_events tr) @ obs' ∧
    615     intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs rem = 〈cs',obs'〉.
     499    intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ge) cs rem = 〈cs',obs'〉.
    616500#ge #cs #s #tr #s' #rem #cs #obs #CL #EX
    617501whd in ⊢ (??%? → ?);
    618 whd in match (intensional_state_change (pcs_to_cs RTLabs_pcsys ge) ??);
     502whd in match (intensional_state_change (pcs_to_cs RTLabs_pcs ge) ??);
    619503generalize in match (cs_callee ??) in ⊢ (% → ?);
    620 whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_pcsys ge) ?) in CL:(??%?);
     504whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_pcs ge) ?) in CL:(??%?);
    621505>CL #name whd in ⊢ (??%? → ?);
    622506cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct
     
    629513let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr :
    630514  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',Ras_state … s'〉 →
    631   intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 →
     515  intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace' = 〈cs',obs〉 →
    632516  pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ?
    633517and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll :
    634518  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
    635   intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
     519  intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace1 = 〈cs',obs〉 →
    636520  pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ?
    637521and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal :
    638522  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
    639   intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
     523  intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace1 = 〈cs',obs〉 →
    640524  maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?.
    641525[ cases tlr
     
    655539    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
    656540    whd in EX:(??%?); destruct
    657     whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?);
     541    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcs ge) ?) in CL:(??%?);
    658542    whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
    659543    generalize in match (cs_callee ??) in ⊢ (??%? → ?);
     
    664548    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
    665549    whd in EX:(??%?); destruct
    666     whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?);
     550    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcs ge) ?) in CL:(??%?);
    667551    whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
    668552    generalize in match (cs_callee ??) in ⊢ (??%? → ?);
     
    677561    whd in EX:(??%?); destruct cases (call_ret_event … ST')
    678562    [ #E1 #E2 >E1 >E2 | skip | %1 @CL ] #ITOT
    679     cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ]
     563    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcs ge) ? = ?) in CL; >CL % ]
    680564    #obs' * #E3 #ITOT'
    681565    <(as_exec_eq_step … ST ST') in EX; #EX
     
    690574    cases (call_ret_event … ST')
    691575    [ #E2 #E3 >E2 >E3 | skip | %1 @CL ] #ITOT
    692     cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ]
     576    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcs ge) ? = ?) in CL; >CL % ]
    693577    #obs' * #E4 #ITOT'
    694578    <(as_exec_eq_step … ST ST') in EX; #EX
     
    732616lemma cost_state_intensional_state_change : ∀ge,s,cs.
    733617  RTLabs_cost s →
    734   \fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s) = cs.
     618  \fst (intensional_state_change (pcs_to_cs … RTLabs_pcs ge) cs s) = cs.
    735619#ge *
    736620[ #f #fs #m #cs //
     
    758642theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting.
    759643  well_cost_labelled_program p →
    760   measurable RTLabs_pcsys p m n stack_cost max →
    761   observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 →
     644  measurable RTLabs_pcs p m n stack_cost max →
     645  observables RTLabs_pcs p m n = return 〈prefix,interesting〉 →
    762646  ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
    763   exec_steps_with_obs RTLabs_ext_pcsys p m = return 〈sm, prefix〉 ∧
     647  exec_steps_with_obs RTLabs_ext_pcs p m = return 〈sm, prefix〉 ∧
    764648  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
    765649  le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧
     
    777661whd in ⊢ (??%? → ?);
    778662@pair_elim #cs1 #prefix1 #ITOT1
    779 lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting'))
    780 cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting') in ⊢ (???% → %);
     663lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ?) cs1 interesting'))
     664cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ?) cs1 interesting') in ⊢ (???% → %);
    781665#cs2 #interesting'' #ITOT2
    782666#E whd in E:(??%%); destruct
  • src/RTLabs/RTLabs_abstract.ma

    r2895 r3031  
    323323#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
    324324qed.
     325
     326(* Build a fullexec for the extended semantics, so that we can go on to make
     327   a preclassified system later. *)
     328
     329
     330definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝
     331λge,s.
     332match eval_statement ge s return λx. (∀s',t. x = Value ??? 〈t,s'〉 → RTLabs_ext_state ge) → ? with
     333[ Value ts ⇒ λnext. Value ??? 〈\fst ts, next (\snd ts) (\fst ts) ?〉
     334| Wrong m ⇒ λ_. Wrong ??? m
     335| Interact o k ⇒ λ_. Wrong … (msg UnexpectedIO)
     336] (next_state ge s).
     337//
     338qed.
     339
     340lemma drop_exec_ext : ∀ge,s,tr,s'.
     341  eval_ext_statement ge s = return 〈tr,s'〉 →
     342  eval_statement ge s = return 〈tr,Ras_state … s'〉.
     343#ge #s #tr #s'
     344whd in ⊢ (??%? → ?);
     345letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
     346cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
     347[ // ]
     348generalize in match f; -f
     349cases (eval_statement ge s)
     350[ #o #k #n #N #E whd in E:(??%%); destruct
     351| * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //
     352| #m #n #N #E whd in E:(??%%); destruct
     353] qed.
     354
     355lemma as_eval_ext_statement : ∀ge,s,tr,s'.
     356  eval_ext_statement ge s = Value … 〈tr,s'〉 →
     357  as_execute (RTLabs_status ge) s s'.
     358#ge #s #tr #s' #EX
     359whd %{tr} %{(drop_exec_ext … EX)}
     360whd in EX:(??%?);
     361letin ns ≝ (next_state ge s) in EX; #EX
     362change with (ns s' tr ?) in match (next_state ge s s' tr ?);
     363generalize in match (drop_exec_ext ?????);
     364#EX'
     365generalize in match ns in EX ⊢ %; -ns >EX' #ns whd in ⊢ (??%? → %);
     366#E destruct @e1
     367qed.
     368
     369definition RTLabs_ext_exec : trans_system io_out io_in ≝
     370  mk_trans_system io_out io_in ? RTLabs_ext_state (λ_.RTLabs_is_final) eval_ext_statement.
     371
     372definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝
     373λp.
     374  let ge ≝ make_global p in
     375  do m ← init_mem … (λx.x) p;
     376  let main ≝ prog_main ?? p in
     377  do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
     378  do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
     379  let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
     380  return (mk_RTLabs_ext_state (make_global p) s [b] ?).
     381% [ % assumption | % ]
     382qed.
     383
     384lemma initial_states_OK : ∀p,s.
     385  make_ext_initial_state p = return s →
     386  make_initial_state p = return (Ras_state … s).
     387#p #s #E
     388cases (bind_inversion ????? E) -E #m * #E1 #E
     389cases (bind_as_inversion ????? E) -E #b * #Eb #E
     390cases (bind_as_inversion ????? E) -E #f * #Ef #E
     391whd in ⊢ (??%?); >E1
     392whd in ⊢ (??%?); >Eb
     393whd in ⊢ (??%?); >Ef
     394whd in E:(??%%) ⊢ (??%?); destruct
     395%
     396qed.
     397
     398lemma initial_states_OK' : ∀p,s.
     399  make_initial_state p = return s →
     400  ∃S,M. make_ext_initial_state p = return (mk_RTLabs_ext_state (make_global p) s S M).
     401#p #s #E
     402cases (bind_inversion ????? E) -E #m * #E1 #E
     403cases (bind_inversion ????? E) -E #b * #Eb #E
     404cases (bind_inversion ????? E) -E #f * #Ef #E
     405whd in E:(??%%); destruct
     406%{[b]} % [ % [ % assumption | % ] ]
     407whd in ⊢ (??%?); >E1
     408whd in ⊢ (??%?); generalize in match (refl ??);
     409>Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb'
     410whd in ⊢ (??%?); generalize in match (refl ??);
     411>Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
     412qed.
     413
     414
     415definition RTLabs_ext_fullexec : fullexec io_out io_in ≝
     416  mk_fullexec … RTLabs_ext_exec make_global make_ext_initial_state.
     417
  • src/RTLabs/RTLabs_classified_system.ma

    r2811 r3031  
    1 (**************************************************************************)
    2 (*       ___                                                              *)
    3 (*      ||M||                                                             *)
    4 (*      ||A||       A project by Andrea Asperti                           *)
    5 (*      ||T||                                                             *)
    6 (*      ||I||       Developers:                                           *)
    7 (*      ||T||         The HELM team.                                      *)
    8 (*      ||A||         http://helm.cs.unibo.it                             *)
    9 (*      \   /                                                             *)
    10 (*       \ /        This file is distributed under the terms of the       *)
    11 (*        v         GNU General Public License Version 2                  *)
    12 (*                                                                        *)
    13 (**************************************************************************)
    141
    152include "RTLabs/RTLabs_abstract.ma".
    163include "RTLabs/RTLabs_semantics.ma".
    174include "common/Measurable.ma".
     5
     6(* First, plain RTLabs.  This for for the front-end, the back-end will get a
     7   prefix for its structured trace in terms of the version with the shadow
     8   stack below. *)
    189
    1910definition RTLabs_stack_ident :
     
    3728  (λ_.RTLabs_classify)
    3829  RTLabs_stack_ident.
     30
     31(* Now the version extended with a shadow stack.  This is the one the back-end
     32   will see, because it matches the RTLabs abstract status for the
     33   structured traces. *)
     34
     35definition RTLabs_ext_pcs ≝ mk_preclassified_system
     36  RTLabs_ext_fullexec
     37  (λg,s. RTLabs_cost (Ras_state … s))
     38  (λg,s. RTLabs_classify (Ras_state … s))
     39  (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H).
Note: See TracChangeset for help on using the changeset viewer.