Changeset 3031
 Timestamp:
 Mar 29, 2013, 12:38:41 PM (5 years ago)
 Location:
 src/RTLabs
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r2948 r3031 3 3 include "common/Measurable.ma". 4 4 include "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. 5 include "RTLabs/RTLabs_classified_system.ma". 28 6 29 7 definition state_at : ∀C:preclassified_system. … … 37 15 return s1. 38 16 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) → ? with42 [ Value ts ⇒ λnext. Value ??? 〈\fst ts, next (\snd ts) (\fst ts) ?〉43  Wrong m ⇒ λ_. Wrong ??? m44  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; f58 cases (eval_statement ge s)59 [ #o #k #n #N #E whd in E:(??%%); destruct60  * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //61  #m #n #N #E whd in E:(??%%); destruct62 ] 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' #EX68 whd %{tr} %{(drop_exec_ext … EX)}69 whd in EX:(??%?);70 letin ns ≝ (next_state ge s) in EX; #EX71 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 @e176 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 in84 do m ← init_mem … (λx.x) p;85 let main ≝ prog_main ?? p in86 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 in89 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 #E97 cases (bind_inversion ????? E) E #m * #E1 #E98 cases (bind_as_inversion ????? E) E #b * #Eb #E99 cases (bind_as_inversion ????? E) E #f * #Ef #E100 whd in ⊢ (??%?); >E1101 whd in ⊢ (??%?); >Eb102 whd in ⊢ (??%?); >Ef103 whd in E:(??%%) ⊢ (??%?); destruct104 %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 #E111 cases (bind_inversion ????? E) E #m * #E1 #E112 cases (bind_inversion ????? E) E #b * #Eb #E113 cases (bind_inversion ????? E) E #f * #Ef #E114 whd in E:(??%%); destruct115 %{[b]} % [ % [ % assumption  % ] ]116 whd in ⊢ (??%?); >E1117 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_system128 RTLabs_ext_fullexec129 (λ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 133 17 lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX. 134 will_return_aux (pcs_to_cs … RTLabs_pcs ysge) depth trace →18 will_return_aux (pcs_to_cs … RTLabs_pcs ge) depth trace → 135 19 ΣWR:will_return ge depth s (make_flat_trace ge n s trace s' EX). 136 20 will_return_end … WR = ?. … … 209 93 210 94 lemma intensional_state_change_State : ∀ge,cs,f,fs,m. 211 intensional_state_change (pcs_to_cs … RTLabs_pcs ysge) cs (State f fs m) = 〈cs,[ ]〉.95 intensional_state_change (pcs_to_cs … RTLabs_pcs ge) cs (State f fs m) = 〈cs,[ ]〉. 212 96 #ge #cs #f #fs #m 213 97 whd in ⊢ (??%?); … … 231 115 ∃S',M'. 232 116 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_pcs ysge) 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')). 234 118 #ge #s #tr #s' #cs #EV #STACK 235 119 whd in match (eval_ext_statement ??); … … 282 166 283 167 lemma callee_ext : ∀ge,s,S,M. 284 cs_callee (pcs_to_cs RTLabs_pcs ys 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). 285 169 #ge * // 286 170 qed. 287 171 288 172 lemma int_state_change_ext : ∀ge,cs,s,S,M. 289 intensional_state_change (pcs_to_cs RTLabs_pcs ysge) cs s =290 intensional_state_change (pcs_to_cs RTLabs_ext_pcs ysge) 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). 291 175 #ge #cs #s #S #M 292 176 whd in ⊢ (??%%); … … 296 180 lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs,cs',itrace. 297 181 exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 → 298 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ysge) 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_pcs ysge) 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))) → 300 184 ∃trace',S,M. 301 185 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_pcs ysge) cs trace' = 〈cs',itrace〉 ∧303 All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcs ysge) 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')). 304 188 #ge #n0 elim n0 305 189 [ * #s #S #M #trace #s' #cs #cs' #itrace #E whd in E:(??%%); destruct … … 333 217 lemma extend_initial_RTLabs_exec_steps : ∀p. let ge ≝ make_global p in ∀n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs',itrace. 334 218 exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 → 335 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ysge) [ ] trace = 〈cs',itrace〉 →219 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ge) [ ] trace = 〈cs',itrace〉 → 336 220 make_ext_initial_state p = OK ? s → 337 221 ∃trace',S,M. 338 222 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_pcs ysge) [ ] trace' = 〈cs',itrace〉 ∧340 All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcs ysge) 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')). 341 225 #p #n #s #trace #s' #cs' #itrace #EXEC #ITOT #INIT 342 226 @(extend_RTLabs_exec_steps … EXEC ITOT) … … 589 473 590 474 lemma as_call_cs_callee : ∀ge,s,CL,CL'. 591 as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_pcs ysge) (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'. 592 476 #ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E 593 477 destruct % … … 610 494 as_classifier (RTLabs_status ge) s cl_other → 611 495 step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 → 612 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ysge) 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〉 → 613 497 ∃obs'. 614 498 obs = (intensional_events_of_events tr) @ obs' ∧ 615 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ysge) cs rem = 〈cs',obs'〉.499 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcs ge) cs rem = 〈cs',obs'〉. 616 500 #ge #cs #s #tr #s' #rem #cs #obs #CL #EX 617 501 whd in ⊢ (??%? → ?); 618 whd in match (intensional_state_change (pcs_to_cs RTLabs_pcs ysge) ??);502 whd in match (intensional_state_change (pcs_to_cs RTLabs_pcs ge) ??); 619 503 generalize in match (cs_callee ??) in ⊢ (% → ?); 620 whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_pcs ysge) ?) in CL:(??%?);504 whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_pcs ge) ?) in CL:(??%?); 621 505 >CL #name whd in ⊢ (??%? → ?); 622 506 cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct … … 629 513 let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr : 630 514 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_pcs ysge) (fn::cs) trace' = 〈cs',obs〉 →515 intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace' = 〈cs',obs〉 → 632 516 pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ? 633 517 and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll : 634 518 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_pcs ysge) (fn::cs) trace1 = 〈cs',obs〉 →519 intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace1 = 〈cs',obs〉 → 636 520 pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ? 637 521 and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal : 638 522 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_pcs ysge) (fn::cs) trace1 = 〈cs',obs〉 →523 intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace1 = 〈cs',obs〉 → 640 524 maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?. 641 525 [ cases tlr … … 655 539 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX 656 540 whd in EX:(??%?); destruct 657 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcs ysge) ?) in CL:(??%?);541 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcs ge) ?) in CL:(??%?); 658 542 whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???); 659 543 generalize in match (cs_callee ??) in ⊢ (??%? → ?); … … 664 548 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX 665 549 whd in EX:(??%?); destruct 666 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcs ysge) ?) in CL:(??%?);550 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcs ge) ?) in CL:(??%?); 667 551 whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???); 668 552 generalize in match (cs_callee ??) in ⊢ (??%? → ?); … … 677 561 whd in EX:(??%?); destruct cases (call_ret_event … ST') 678 562 [ #E1 #E2 >E1 >E2  skip  %1 @CL ] #ITOT 679 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcs ysge) ? = ?) in CL; >CL % ]563 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcs ge) ? = ?) in CL; >CL % ] 680 564 #obs' * #E3 #ITOT' 681 565 <(as_exec_eq_step … ST ST') in EX; #EX … … 690 574 cases (call_ret_event … ST') 691 575 [ #E2 #E3 >E2 >E3  skip  %1 @CL ] #ITOT 692 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcs ysge) ? = ?) in CL; >CL % ]576 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcs ge) ? = ?) in CL; >CL % ] 693 577 #obs' * #E4 #ITOT' 694 578 <(as_exec_eq_step … ST ST') in EX; #EX … … 732 616 lemma cost_state_intensional_state_change : ∀ge,s,cs. 733 617 RTLabs_cost s → 734 \fst (intensional_state_change (pcs_to_cs … RTLabs_pcs ysge) cs s) = cs.618 \fst (intensional_state_change (pcs_to_cs … RTLabs_pcs ge) cs s) = cs. 735 619 #ge * 736 620 [ #f #fs #m #cs // … … 758 642 theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting. 759 643 well_cost_labelled_program p → 760 measurable RTLabs_pcs ysp m n stack_cost max →761 observables RTLabs_pcs ysp 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〉 → 762 646 ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn. 763 exec_steps_with_obs RTLabs_ext_pcs ysp m = return 〈sm, prefix〉 ∧647 exec_steps_with_obs RTLabs_ext_pcs p m = return 〈sm, prefix〉 ∧ 764 648 tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧ 765 649 le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧ … … 777 661 whd in ⊢ (??%? → ?); 778 662 @pair_elim #cs1 #prefix1 #ITOT1 779 lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ys?) cs1 interesting'))780 cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ys?) cs1 interesting') in ⊢ (???% → %);663 lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ?) cs1 interesting')) 664 cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ?) cs1 interesting') in ⊢ (???% → %); 781 665 #cs2 #interesting'' #ITOT2 782 666 #E whd in E:(??%%); destruct 
src/RTLabs/RTLabs_abstract.ma
r2895 r3031 323 323 #ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct 324 324 qed. 325 326 (* Build a fullexec for the extended semantics, so that we can go on to make 327 a preclassified system later. *) 328 329 330 definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝ 331 λge,s. 332 match 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 // 338 qed. 339 340 lemma 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' 344 whd in ⊢ (??%? → ?); 345 letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *) 346 cut (∀s',t,EV. Ras_state … (f s' t EV) = s') 347 [ // ] 348 generalize in match f; f 349 cases (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 355 lemma 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 359 whd %{tr} %{(drop_exec_ext … EX)} 360 whd in EX:(??%?); 361 letin ns ≝ (next_state ge s) in EX; #EX 362 change with (ns s' tr ?) in match (next_state ge s s' tr ?); 363 generalize in match (drop_exec_ext ?????); 364 #EX' 365 generalize in match ns in EX ⊢ %; ns >EX' #ns whd in ⊢ (??%? → %); 366 #E destruct @e1 367 qed. 368 369 definition 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 372 definition 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  % ] 382 qed. 383 384 lemma 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 388 cases (bind_inversion ????? E) E #m * #E1 #E 389 cases (bind_as_inversion ????? E) E #b * #Eb #E 390 cases (bind_as_inversion ????? E) E #f * #Ef #E 391 whd in ⊢ (??%?); >E1 392 whd in ⊢ (??%?); >Eb 393 whd in ⊢ (??%?); >Ef 394 whd in E:(??%%) ⊢ (??%?); destruct 395 % 396 qed. 397 398 lemma 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 402 cases (bind_inversion ????? E) E #m * #E1 #E 403 cases (bind_inversion ????? E) E #b * #Eb #E 404 cases (bind_inversion ????? E) E #f * #Ef #E 405 whd in E:(??%%); destruct 406 %{[b]} % [ % [ % assumption  % ] ] 407 whd in ⊢ (??%?); >E1 408 whd in ⊢ (??%?); generalize in match (refl ??); 409 >Eb in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)?); #Eb' 410 whd in ⊢ (??%?); generalize in match (refl ??); 411 >Ef in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)?); #Ef' % 412 qed. 413 414 415 definition 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 (**************************************************************************)14 1 15 2 include "RTLabs/RTLabs_abstract.ma". 16 3 include "RTLabs/RTLabs_semantics.ma". 17 4 include "common/Measurable.ma". 5 6 (* First, plain RTLabs. This for for the frontend, the backend will get a 7 prefix for its structured trace in terms of the version with the shadow 8 stack below. *) 18 9 19 10 definition RTLabs_stack_ident : … … 37 28 (λ_.RTLabs_classify) 38 29 RTLabs_stack_ident. 30 31 (* Now the version extended with a shadow stack. This is the one the backend 32 will see, because it matches the RTLabs abstract status for the 33 structured traces. *) 34 35 definition 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.