 Timestamp:
 Feb 16, 2012, 6:05:57 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1706 r1707 77 77  ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s 78 78  ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s. 79 80 coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝ 81  nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H) 82  nw_step : ∀s,tr,s',H,tr'. not_wrong o i ge s' tr' → not_wrong o i ge s (ft_step o i ge s tr s' H tr'). 83 84 lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'. 85 not_wrong o i ge s (ft_step o i ge s tr s' H tr') → 86 not_wrong o i ge s' tr'. 87 #o #i #ge #s #tr #s' #H #tr' #NW inversion NW 88 [ #H105 #H106 #H107 #H108 #H109 destruct 89  #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct // 90 ] qed. 79 91 80 92 let corec make_flat_trace ge s … … 984 996 λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1  St_call_ptr _ _ _ _ ⇒ 1  St_return ⇒ 1  _ ⇒ 0 ]). 985 997 986 inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝ 987  stlb_step : ∀l,n,H. 998 inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝ 999  bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n 1000  bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n 1001 with bound_on_steps_to_cost1 : label → nat → Prop ≝ 1002  bostc_step : ∀l,n,H. 988 1003 let stmt ≝ lookup_present … g l H in 989 1004 (∀l'. Exists label (λl0. l0 = l') (successors stmt) → 990 (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨991 steps_to_label_bound g l' n) →992 steps_to_label_bound g l (steps_for_statement stmt + n). 993 1005 bound_on_steps_to_cost g l' n) → 1006 bound_on_steps_to_cost1 g l (steps_for_statement stmt + n). 1007 1008 (* 994 1009 lemma steps_to_label_bound_inv : ∀g,l,n. 995 1010 steps_to_label_bound g l n → … … 1002 1017 % [2: % [ @refl  #l' #EX cases (IH l' EX) /2/ ]  skip ] 1003 1018 qed. 1004 1019 *) 1005 1020 discriminator nat. 1006 1021 (* 1007 1022 definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n. 1008 1023 … … 1020 1035  Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False  cons f _ ⇒ soundly_labelled_frame f ] 1021 1036 ]. 1022 1023 definition frame_steps_to_label_bound : frame → nat → Prop ≝ 1024 λf. steps_to_label_bound (f_graph (func f)) (next f). 1025 1026 inductive state_steps_to_label_bound : state → nat → Prop ≝ 1027  sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) n 1028  sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S n) 1029  sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S n) 1037 *) 1038 definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝ 1039 λf. bound_on_steps_to_cost (f_graph (func f)) (next f). 1040 definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝ 1041 λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f). 1042 1043 inductive state_bound_on_steps_to_cost : state → nat → Prop ≝ 1044  sbostc_state : ∀f,fs,m,n. frame_bound_on_steps_to_cost1 f n → state_bound_on_steps_to_cost (State f fs m) n 1045  sbostc_call : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate fd args dst (f::fs) m) (S n) 1046  sbostc_ret : ∀rtv,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Returnstate rtv dst (f::fs) m) (S n) 1030 1047 . 1031 1048 1032 lemma state_ steps_to_label_bound_zero : ∀s.1033 ¬ state_ steps_to_label_bounds O.1049 lemma state_bound_on_steps_to_cost_zero : ∀s. 1050 ¬ state_bound_on_steps_to_cost s O. 1034 1051 #s % #H inversion H 1035 [ #H4 8 #H49 #H50 #H51 #H52 #H53 #H54 #H55destruct1036 inversion H521037 #H 68 #H69 #H70 #H71 #H72 #H73 #H74 normalize in H73; destruct1052 [ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct 1053 whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*) 1054 #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct 1038 1055  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct 1039 1056  #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct … … 1068 1085 ] qed. 1069 1086 1070 lemma state_steps_to_label_bound_step : ∀ge,s,tr,s',n.1071 state_ steps_to_label_bounds (S n) →1087 lemma bound_after_step : ∀ge,s,tr,s',n. 1088 state_bound_on_steps_to_cost s (S n) → 1072 1089 eval_statement ge s = Value ??? 〈tr, s'〉 → 1073 1090 RTLabs_cost s' = false → 1074 1091 (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨ 1075 state_ steps_to_label_bounds' n.1076 #ge #s #tr #s' #n # STEPS inversion STEPS1092 state_bound_on_steps_to_cost s' n. 1093 #ge #s #tr #s' #n #BOUND1 inversion BOUND1 1077 1094 [ #f #fs #m #m #FS #E1 #E2 #_ destruct 1078 1095 #EVAL cases (eval_successor … EVAL) 1079 1096 [ /3/ 1080 1097  * #l * #S1 #S2 #NC %2 1081 cases (steps_to_label_bound_inv … FS ?) [2: @(next_ok f) ] 1082 #n' 1098 (* 1099 cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ] 1100 *) 1101 @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct 1083 1102 inversion (eval_perserves … EVAL) 1084 [ #ge0 #f0 #f' #fs' #m0 #m' #F #E1 #E2 #E3 #_ destruct 1085 >(eval_steps … EVAL) * #En normalize in En; 1086 #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct 1087 whd in S1:(??%?); destruct 1088 %1 cases (H l S2) 1089 [ * #LP 1090 change with (RTLabs_cost (State (mk_frame H1 H7 l H9 H5 H6) fs' m')) in ⊢ (?% → ?); 1091 >NC * 1092  // 1103 [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct 1104 >(eval_steps … EVAL) in E2; #En normalize in En; 1105 inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct 1106 %1 inversion (IH … S2) 1107 [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct 1108 change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%); 1109 whd in S1:(??%?); destruct >NC in CSx; * 1110  whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73 1093 1111 ] 1094  #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct 1095 >(eval_steps … EVAL) * #En normalize in En; 1096 #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct 1097 %2 whd lapply (H l S2) 1098 @FS // 1099  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 1112  #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct 1113 >(eval_steps … EVAL) in E2; #En normalize in En; 1114 inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct 1115 %2 @IH normalize in S1; destruct @S2 1116  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 1100 1117 destruct 1101  #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42destruct1118  #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct 1102 1119 normalize in S1; destruct 1103  #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56destruct1120  #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct 1104 1121 ] 1105 1122 ] … … 1118 1135 inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct  #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct  #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ] 1119 1136 inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct 1120 @FS 1137 inversion FS 1138 [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct 1139 change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%); 1140 >NC in CSx; * 1141  #lx #nx #H #E1x #E2x #_ destruct @H 1142 ] 1121 1143 ] 1122 1144 ] qed. 1123 1145 1124 1125 (*1126 lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'.1127 state_steps_to_label_bound (State f fs m) (S (S n)) →1128 ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) →1129 eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →1130 state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n  _ ⇒ S n ]).1131 #ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H1132 [ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct1133 cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct  #n' #H1 #E2 normalize in E2; destruct ]1134 #NC whd in ⊢ (??%? → ?);1135 generalize in ⊢ (??(?%)? → ?);1136 lapply (steps_to_label_bound_inv_step … H1 next_ok NC)1137 cases (lookup_present ??? next next_ok)1138 [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl1139  #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl1140  #r #cs #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #E3 @bind_ok #locals' #E4 whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl1141  #t1 #t2 #op #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl1142  #op #r1 #r2 #r3 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl1143  #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl1144  #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl1145  #id #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl1146  #r #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl1147  #id #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl1148  #r #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b  @Efn ]   cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]1149  #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %1150  #r #ls #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct  #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct  #l' #e #E whd in E:(??%?); destruct % % ]  *: #vl #E whd in E:(??%?); destruct ]1151  #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %51152 ]1153 *)1154 1146 (* When constructing an infinite trace, we need to be able to grab the finite 1155 1147 portion of the trace for the next [trace_label_diverges] constructor. We … … 1208 1200 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 1209 1201 (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace))) 1210 (LABEL_LIMIT: state_steps_to_label_bound s n) 1202 (NOT_UNDEFINED: not_wrong … trace) 1203 (LABEL_LIMIT: state_bound_on_steps_to_cost s n) 1211 1204 on n : finite_prefix ge s ≝ 1212 match n return λn. state_ steps_to_label_bounds n → finite_prefix ge s with1205 match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with 1213 1206 [ O ⇒ λLABEL_LIMIT. ⊥ 1214 1207  S n' ⇒ 1215 match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_steps_to_label_bounds (S n') → finite_prefix ge s with1216 [ ft_stop st FINAL ⇒ λ STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥1217  ft_step start tr next EV trace' ⇒ λ STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.1208 match trace return λs,trace. not_wrong ??? s trace → well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with 1209 [ ft_stop st FINAL ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ 1210  ft_step start tr next EV trace' ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. 1218 1211 match RTLabs_classify start return λx. RTLabs_classify start = x → ? with 1219 1212 [ cl_other ⇒ λCL. … … 1222 1215 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' 1223 1216  false ⇒ λCS. 1224 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ??? in1217 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ???? in 1225 1218 fp_add_default ge ?? CL fs ? CS 1226 1219 ] (refl ??) 1227 1220  cl_jump ⇒ λCL. 1228 1221 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' 1229  cl_call ⇒ λCL. ?(*1222  cl_call ⇒ λCL. 1230 1223 match ORACLE ge O next trace' return λ_. finite_prefix ge start with 1231 1224 [ or_introl TERMINATES ⇒ … … 1234 1227 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with 1235 1228 [ 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) 1236  false ⇒ λCS. ? (* broken  we don't know the new value of n *)1237 (*let fs ≝ finite_segment ge (new_status … tlr) ??????????????1238 fp_add_terminating_call … (new_trace … tlr) ? CS*)1229  false ⇒ λCS. 1230 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ???? in 1231 fp_add_terminating_call … fs (new_trace … tlr) ? CS 1239 1232 ] (refl ??) 1240 1233 ] 1241 1234  or_intror NO_TERMINATION ⇒ 1242 1235 fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace') 1243 ] *)1236 ] 1244 1237  cl_return ⇒ λCL. ⊥ 1245 1238 ] (refl ??) 1246  ft_wrong start m EV ⇒ λ STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥1247 ] STATE_COSTLABELLED NO_TERMINATION1239  ft_wrong start m EV ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ 1240 ] NOT_UNDEFINED STATE_COSTLABELLED NO_TERMINATION 1248 1241 ] LABEL_LIMIT. 1249 [ cases (state_ steps_to_label_bound_zero s) /2/1242 [ cases (state_bound_on_steps_to_cost_zero s) /2/ 1250 1243  (* TODO: how do we know that we're not at the final state? *) 1251 1244  @(absurd ?? NO_TERMINATION) 1252 1245 %{0} % @wr_base // 1253 1246  @(well_cost_labelled_jump … EV) // 1254  5,6,8,9,10: /2/ 1255  1247  5,6,7,8,9,10: /2/ 1248  /2/ 1249  // 1250  (* FIXME: postcall nontermination *) 1251  (* FIXME: postcall notwrong *) 1252  (* FIXME: bound on steps after call *) 1253  @(well_cost_labelled_state_step … EV) // 1254  @(well_cost_labelled_call … EV) // 1255  18,19,20: /2/ 1256 1256  @(well_cost_labelled_state_step … EV) // 1257 1257  @(not_to_not … NO_TERMINATION) 1258 1258 * #depth * #TERM %{depth} % @wr_step /2/ 1259  cases (state_steps_to_label_bound_step … LABEL_LIMIT EV ?) 1260 1261 @(well_cost_labelled_call … EV) // 1262  1263 2,14: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct 1264  5,6,8: /2/ 1265  1266 *) 1267  12,13,14: /2/ 1268  @(well_cost_labelled_state_step … EV) // 1269  @(not_to_not … NO_TERMINATION) 1270 * #depth * #TERM %{depth} % @wr_step /2/ 1259  @(still_not_wrong … NOT_UNDEFINED) 1260  cases (bound_after_step … LABEL_LIMIT EV ?) 1261 [ * [ #TERMINATES @⊥ @(absurd ?? NO_TERMINATION) %{0} % @wr_step [ %1 //  1262 inversion trace' 1263 [ cases daemon (* TODO again *)  #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct 1264 @wr_base // 1265  #H99 #H100 #H101 #H102 #H103 destruct 1266 inversion NOT_UNDEFINED 1267 [ #H137 #H138 #H139 #H140 #H141 destruct 1268  #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 destruct 1269 inversion H148 1270 [ #H153 #H154 #H155 #H156 #H157 destruct 1271  #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct 1272 ] 1273 ] 1274 ] 1275 ] 1276  >CL #E destruct 1277 ] 1278  // 1279  // 1280 ] 1281  inversion NOT_UNDEFINED 1282 [ #H169 #H170 #H171 #H172 #H173 destruct 1283  #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct 1284 ] 1271 1285 ] cases daemon qed. 1272 1286
Note: See TracChangeset
for help on using the changeset viewer.