Changeset 1960
 Timestamp:
 May 16, 2012, 5:24:05 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1880 r1960 21 21 ]. 22 22 23 (* We define a straight "is this a cost label" pair of functions, which is 24 convenient for most of our uses here (because we can make a hypothesis of 25 it without naming the label), and a pair which return the label to fit the 26 definition of abstract_status. *) 27 23 28 definition is_cost_label : statement → bool ≝ 24 29 λs. match s with [ St_cost _ _ ⇒ true  _ ⇒ false ]. … … 31 36 ]. 32 37 33 definition RTLabs_status : genv → final_abstract_status ≝ 38 definition cost_label_of : statement → option costlabel ≝ 39 λs. match s with [ St_cost s _ ⇒ Some ? s  _ ⇒ None ? ]. 40 41 definition RTLabs_cost_label : state → option costlabel ≝ 42 λs. match s with 43 [ State f fs m ⇒ 44 cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) 45  _ ⇒ None ? 46 ]. 47 48 (* At the moment we don't need to talk about the program counter, so we just 49 use unit. *) 50 definition unit_deqset ≝ mk_DeqSet unit (λ_.λ_. true) ?. 51 * * % // 52 qed. 53 54 definition RTLabs_status : genv → abstract_status ≝ 34 55 λge. 35 mk_final_abstract_status 36 (mk_abstract_status 56 mk_abstract_status 37 57 state 38 58 (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) 59 unit_deqset 60 (λ_. it) 39 61 (λs,c. RTLabs_classify s = c) 40 (λs. RTLabs_cost s = true)62 RTLabs_cost_label 41 63 (λs,s'. match s with 42 64 [ mk_Sig s p ⇒ … … 51 73  _ ⇒ λH.⊥ 52 74 ] p 53 ]) )75 ]) 54 76 (λs. RTLabs_is_final s ≠ None ?). 55 [ whd in H:(??%?); 77 [ normalize in H; destruct 78  normalize in H; destruct 79  whd in H:(??%?); 56 80 cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H; 57 81 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct 58  normalize in H; destruct 59  normalize in H; destruct 82 ] qed. 83 84 (* Allow us to move between the different notions of when a state is cost 85 labelled. *) 86 87 lemma RTLabs_costed : ∀ge,s. 88 RTLabs_cost s = true → 89 as_costed (RTLabs_status ge) s. 90 #ge * 91 [ * #func #locals #next #nok #b #r #fs #m 92 whd in ⊢ (??%? → %); whd in ⊢ (? → ?(??%?)); 93 cases (lookup_present ?? (f_graph func) ??) normalize 94 #A try #B try #C try #D try #E try #F try #G try #H try #G destruct 95 % #E' destruct 96  normalize #fd #args #r #fs #m #E destruct 97  normalize #A #B #C #D #E destruct 98  normalize #A #B destruct 99 ] qed. 100 101 lemma costed_RTLabs : ∀ge,s. 102 as_costed (RTLabs_status ge) s → 103 RTLabs_cost s = true. 104 #ge 105 cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #H 106 * 107 [ * #func #locals #next #nok #b #r #fs #m 108 whd in ⊢ (% → ??%?); whd in ⊢ (?(??%?) → ?); 109 cases (lookup_present ?? (f_graph func) ??) normalize // 110 #A try #B try #C try #D try #E try #F try #G try #I try #J cases (H ?) // 111  *: normalize #A #B try #C try #D try #E try #F cases (H ?) // 60 112 ] qed. 61 113 … … 63 115 RTLabs_cost s = false → 64 116 ¬ as_costed (RTLabs_status ge) s. 65 #ge #s #E % whd in ⊢ (% → ?); >E #E' destruct 66 qed. 117 #ge * 118 [ * #func #locals #next #nok #b #r #fs #m 119 whd in ⊢ (??%? → ?%); whd in ⊢ (? → ?(?(??%?))); 120 cases (lookup_present ?? (f_graph func) ??) normalize 121 #A try #B try #C try #D try #E try #F try #G try #H try #I destruct 122 % * #J @J @refl 123  *: normalize #A #B try #C try #D try #E try #F % * #G @G @refl 124 ] qed. 67 125 68 126 (* Before attempting to construct a structured trace, let's show that we can … … 550 608 >Estmt #LP whd in ⊢ (??%? → ?); 551 609 (* replace with lemma on successors? *) 552 @bind_ value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct610 @bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct 553 611 lapply (Hbody (next fr) (next_ok fr)) 554 612 generalize in ⊢ (???% → ?); … … 561 619 >Estmt #LP whd in ⊢ (??%? → ?); 562 620 (* replace with lemma on successors? *) 563 @bind_ value #a cases a [  #sz #i  #f  #r  #ptr ] #Ea whd in ⊢ (??%? → ?);621 @bind_res_value #a cases a [  #sz #i  #f  #r  #ptr ] #Ea whd in ⊢ (??%? → ?); 564 622 [ 2: (* later *) 565 623  *: #E destruct … … 598 656 cases fd 599 657 [ #fn whd in ⊢ (??%? → % → ?); 600 @bind_ value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any)658 @bind_res_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any) 601 659 #m' #b whd in ⊢ (??%? → ?); #E' destruct 602 660 * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3 … … 703 761 [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; 704 762 [ normalize #EV destruct  * [ 2: * #r normalize #EV destruct /2/  *: normalize #a try #b destruct ] ] 705  #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_ value #locals #El #EV763  #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_res_value #locals #El #EV 706 764 whd in EV:(??%?); destruct @(sp_finished ? f) // 707 765 cases f // … … 946 1004 let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in 947 1005 replace_sub_trace … r ? 948 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r)1006 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r) 949 1007 950 1008 ] TERMINATES_IN_TIME … … 978 1036 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 979 1037 (* We're about to run into a label. *) 980 [ true ⇒ λCS. 1038 [ true ⇒ λCS. 981 1039 mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ? 982 1040 doesnt_end_with_ret 983 1041 (mk_trace_result ge … next trace' ? 984 (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??)1042 (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) ??) 985 1043 (* An ordinary step, keep going. *) 986 1044  false ⇒ λCS. … … 1006 1064 (mk_trace_result ge … 1007 1065 (tal_base_call (RTLabs_status ge) start next (new_state … r) 1008 ? CL ? (new_trace … r) CS) ??)1066 ? CL ? (new_trace … r) (RTLabs_costed … CS)) ??) 1009 1067 (* otherwise use step case *) 1010 1068  false ⇒ λCS. … … 1041 1099  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ // 1042 1100  @(stack_preserved_join … (stack_ok … r)) // 1043  @( trace_label_label_label … (new_trace … r))1101  @(costed_RTLabs ge) @(trace_label_label_label … (new_trace … r)) 1044 1102  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_ 1045 1103 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) … … 1053 1111  @le_n 1054 1112  // 1113  @RTLabs_costed // 1055 1114  @le_S_S_to_le @TERMINATES_IN_TIME 1056 1115  @(wrl_nonzero … TERMINATES_IN_TIME) … … 1071 1130  %{tr} @EV 1072 1131  %1 whd @CL 1073  @ (well_cost_labelled_jump … EV) //1132  @RTLabs_costed @(well_cost_labelled_jump … EV) // 1074 1133  @(well_cost_labelled_state_step … EV) // 1075 1134  whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} % … … 1236 1295 [ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1237 1296  #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1238  #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //1239  #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //1240  #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_ value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //1241  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_ value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //1242  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_ value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //1243  #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_ value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //1244  #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_ value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //1245  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1}  %{l2} ] % // [ %  %2 %] //1246  #r #ls #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev1297  #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1298  #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1299  #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1300  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1301  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1302  #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1303  #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1304  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1}  %{l2} ] % // [ %  %2 %] // 1305  #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev 1247 1306 cases v [ #E normalize in E; destruct  #sz #i  #f #E normalize in E; destruct  #r #E normalize in E; destruct  #p #E normalize in E; destruct ] 1248 1307 whd in ⊢ (??%? → ?); … … 1252 1311  #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El) 1253 1312 ] 1254  #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl1313  #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl 1255 1314 ] qed. 1256 1315 … … 1328 1387 [ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl 1329 1388  #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl 1330  #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl1331  #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl1332  #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_ value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl1333  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_ value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl1334  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_ value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl1335  #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_ value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl1336  #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_ value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl1337  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl1338  #r #ls #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev1389  #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1390  #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1391  #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1392  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1393  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl 1394  #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl 1395  #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl 1396  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl 1397  #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev 1339 1398 cases v [ #E normalize in E; destruct  #sz #i  #f #E normalize in E; destruct  #r #E normalize in E; destruct  #p #E normalize in E; destruct ] 1340 1399 whd in ⊢ (??%? → ?); … … 1344 1403  #l #El whd in ⊢ (??%? → ?); #E destruct @refl 1345 1404 ] 1346  #LP whd in ⊢ (??%? → ?); @bind_ value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl1405  #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl 1347 1406 ] qed. 1348 1407 … … 1599 1658 match RTLabs_cost next return λx. RTLabs_cost next = x → ? with 1600 1659 [ true ⇒ λCS. 1601 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK'1660 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) trace' TRACE_OK' 1602 1661  false ⇒ λCS. 1603 1662 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in … … 1613 1672 let TRACE_OK' ≝ ? in 1614 1673 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with 1615 [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr) TRACE_OK'1674 [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) (RTLabs_costed … CS)) (remainder … tlr) TRACE_OK' 1616 1675  false ⇒ λCS. 1617 1676 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in … … 1631 1690  @(absurd ?? (ro_no_termination … TRACE_OK)) 1632 1691 %{0} % @wr_base // 1633  @ (well_cost_labelled_jump … EV) /2/1692  @RTLabs_costed @(well_cost_labelled_jump … EV) /2/ 1634 1693  5,6,8,9,10,11: /3/ 1635 1694  % [ @(well_cost_labelled_state_step … EV) /2/ … … 1740 1799 [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL. 1741 1800 let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in 1742 tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T'1801 tld_step (RTLabs_status ge) s s' (tll_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) T' 1743 1802 (* 1744 1803 match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with … … 1748 1807  fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL. 1749 1808 let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in 1750 tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T'1809 tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) ?? T' 1751 1810 (* 1752 1811 match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with … … 1756 1815 ] STATEMENT_COSTLABEL 1757 1816 ]. 1758 [ @( trace_any_label_label … T)1817 [ @(costed_RTLabs ge) @(trace_any_label_label … T) 1759 1818  %{tr} @EV 1760 1819  @(trace_any_call_call … T) … … 1905 1964 1906 1965 (* Extract a flat trace from a structured one. *) 1907 let rec flat ten_trace_label_return ge s s'1966 let rec flat_trace_of_label_return ge s s' 1908 1967 (tr:trace_label_return (RTLabs_status ge) s s') 1909 1968 on tr : 1910 1969 partial_flat_trace io_out io_in ge s s' ≝ 1911 1970 match tr with 1912 [ tlr_base s1 s2 tll ⇒ flat ten_trace_label_label ge ends_with_ret s1 s2 tll1971 [ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll 1913 1972  tlr_step s1 s2 s3 tll tlr ⇒ 1914 1973 append_partial_flat_trace … 1915 (flat ten_trace_label_label ge doesnt_end_with_ret s1 s2 tll)1916 (flat ten_trace_label_return ge s2 s3 tlr)1974 (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll) 1975 (flat_trace_of_label_return ge s2 s3 tlr) 1917 1976 ] 1918 and flat ten_trace_label_label ge ends s s'1977 and flat_trace_of_label_label ge ends s s' 1919 1978 (tr:trace_label_label (RTLabs_status ge) ends s s') 1920 1979 on tr : 1921 1980 partial_flat_trace io_out io_in ge s s' ≝ 1922 1981 match tr with 1923 [ tll_base e s1 s2 tal _ ⇒ flat ten_trace_any_label ge e s1 s2 tal1982 [ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal 1924 1983 ] 1925 and flat ten_trace_any_label ge ends s s'1984 and flat_trace_of_any_label ge ends s s' 1926 1985 (tr:trace_any_label (RTLabs_status ge) ends s s') 1927 1986 on tr : … … 1935 1994 pft_base … EX' ] 1936 1995  tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒ 1937 let suffix' ≝ flat ten_trace_label_return ge ?? tlr in1996 let suffix' ≝ flat_trace_of_label_return ge ?? tlr in 1938 1997 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 1939 1998 pft_step … EX' suffix' ] … … 1942 2001 pft_step … EX' 1943 2002 (append_partial_flat_trace … 1944 (flat ten_trace_label_return ge ?? tlr)1945 (flat ten_trace_any_label ge ??? tal))2003 (flat_trace_of_label_return ge ?? tlr) 2004 (flat_trace_of_any_label ge ??? tal)) 1946 2005 ] 1947 2006  tal_step_default ends s1 s2 s3 EX tal CL CS ⇒ 1948 2007 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 1949 pft_step … EX' (flat ten_trace_any_label ge ??? tal)2008 pft_step … EX' (flat_trace_of_any_label ge ??? tal) 1950 2009 ] 1951 2010 ]. … … 1954 2013 (* We take an extra step so that we can always return a nonempty trace to 1955 2014 satisfy the guardedness condition in the cofixpoint. *) 1956 let rec flat ten_trace_any_call ge s s' s'' et2015 let rec flat_trace_of_any_call ge s s' s'' et 1957 2016 (tr:trace_any_call (RTLabs_status ge) s s') 1958 2017 (EX'':eval_statement ge s' = Value … 〈et,s''〉) … … 1965 2024 pft_step … EX' 1966 2025 (append_partial_flat_trace … 1967 (flat ten_trace_label_return ge ?? tlr)1968 (flat ten_trace_any_call ge … tac EX''))2026 (flat_trace_of_label_return ge ?? tlr) 2027 (flat_trace_of_any_call ge … tac EX'')) 1969 2028 ] 1970 2029  tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''. 1971 2030 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 1972 2031 pft_step … EX' 1973 (flat ten_trace_any_call ge … tal EX'')2032 (flat_trace_of_any_call ge … tal EX'') 1974 2033 ] 1975 2034 ] EX''. 1976 2035 1977 let rec flat ten_trace_label_call ge s s' s'' et2036 let rec flat_trace_of_label_call ge s s' s'' et 1978 2037 (tr:trace_label_call (RTLabs_status ge) s s') 1979 2038 (EX'':eval_statement ge s' = Value … 〈et,s''〉) … … 1981 2040 partial_flat_trace io_out io_in ge s s'' ≝ 1982 2041 match tr with 1983 [ tlc_base s1 s2 tac CS ⇒ flat ten_trace_any_call … tac2042 [ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac 1984 2043 ] EX''. 1985 2044 … … 1987 2046 to take care to satisfy the guardedness condition by witnessing the fact that 1988 2047 the partial traces are nonempty. *) 1989 let corec flat ten_trace_label_diverges ge s2048 let corec flat_trace_of_label_diverges ge s 1990 2049 (tr:trace_label_diverges (RTLabs_status ge) s) 1991 2050 : flat_trace io_out io_in ge s ≝ 1992 2051 match tr with 1993 2052 [ tld_step sx sy tll tld ⇒ 1994 match flat ten_trace_label_label ge … tll with1995 [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat ten_trace_label_diverges ge ? tld)2053 match flat_trace_of_label_label ge … tll with 2054 [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) 1996 2055  pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld) 1997 2056 ] tld 1998 2057  tld_base s1 s2 s3 tlc EX CL tld ⇒ 1999 2058 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2000 match flat ten_trace_label_call … tlc EX' with2001 [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat ten_trace_label_diverges ge ? tld)2059 match flat_trace_of_label_call … tlc EX' with 2060 [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) 2002 2061  pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld) 2003 2062 ] tld … … 2011 2070 : flat_trace io_out io_in ge s ≝ 2012 2071 match ptr with 2013 [ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flat ten_trace_label_diverges ge s' tr)2072 [ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flat_trace_of_label_diverges ge s' tr) 2014 2073  pft_step s1 et s2 s3 EX tr' ⇒ λtr. ft_step … EX (add_partial_flat_trace … tr' tr) 2015 2074 ] tr … … 2072 2131 (str:trace_label_diverges (RTLabs_status ge) s) 2073 2132 (tr:flat_trace io_out io_in ge s) 2074 : equal_flat_traces … (flat ten_trace_label_diverges … str) tr ≝ ?.2133 : equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?. 2075 2134 @flat_traces_are_determined_by_starting_point 2076 2135 qed. 2077 2136 2078 let rec flat ten_trace_whole_program ge s2137 let rec flat_trace_of_whole_program ge s 2079 2138 (tr:trace_whole_program (RTLabs_status ge) s) 2080 2139 on tr : flat_trace io_out io_in ge s ≝ … … 2082 2141 [ twp_terminating s1 s2 sf CL EX tlr F ⇒ 2083 2142 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2084 ft_step … EX' (partial_to_flat_trace … (flat ten_trace_label_return … tlr) (ft_stop … sf F))2143 ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … sf F)) 2085 2144 ] 2086 2145  twp_diverges s1 s2 CL EX tld ⇒ 2087 2146 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2088 ft_step … EX' (flat ten_trace_label_diverges … tld)2147 ft_step … EX' (flat_trace_of_label_diverges … tld) 2089 2148 ] 2090 2149 ]. … … 2093 2152 (str:trace_whole_program (RTLabs_status ge) s) 2094 2153 (tr:flat_trace io_out io_in ge s) 2095 : equal_flat_traces … (flat ten_trace_whole_program … str) tr ≝ ?.2154 : equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?. 2096 2155 @flat_traces_are_determined_by_starting_point 2097 2156 qed.
Note: See TracChangeset
for help on using the changeset viewer.