[2486] | 1 | include "common/Executions.ma". |
---|
| 2 | include "common/StructuredTraces.ma". (* just for status_class *) |
---|
| 3 | |
---|
[2618] | 4 | (* A small-step executable semantics, together with some kind of global |
---|
| 5 | environment, notion of cost labelled state, classification function and |
---|
| 6 | stack costs. *) |
---|
| 7 | |
---|
[2486] | 8 | record classified_system : Type[2] ≝ { |
---|
| 9 | cs_exec :> fullexec io_out io_in; |
---|
| 10 | cs_global : global … cs_exec; |
---|
| 11 | cs_labelled : state … cs_exec cs_global → bool; |
---|
| 12 | cs_classify : state … cs_exec cs_global → status_class; |
---|
[2685] | 13 | cs_callee : ∀s. match cs_classify … s with [ cl_call ⇒ True | _ ⇒ False ] → ident |
---|
[2486] | 14 | }. |
---|
| 15 | |
---|
| 16 | definition cs_state : classified_system → Type[0] ≝ |
---|
| 17 | λC. state … C (cs_global … C). |
---|
| 18 | |
---|
[2534] | 19 | (* Ideally we would also allow measurable traces to be from one cost label to |
---|
| 20 | another (in the same function call), but due to time constraints we'll stick |
---|
| 21 | to ending measurable traces at the end of the function only. |
---|
| 22 | *) |
---|
[2486] | 23 | |
---|
[2669] | 24 | definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝ |
---|
| 25 | λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return. |
---|
[2534] | 26 | |
---|
[2685] | 27 | (* For intensional_event; should separate out definition *) |
---|
| 28 | include "common/StatusSimulation.ma". |
---|
[2486] | 29 | |
---|
[2685] | 30 | definition intensional_event_of_event : event → list intensional_event ≝ |
---|
| 31 | λev. match ev with |
---|
| 32 | [ EVcost l ⇒ [ IEVcost l ] |
---|
| 33 | | EVextcall _ _ _ ⇒ [ ] (* No equivalent, but there shouldn't be any for now *) |
---|
| 34 | ]. |
---|
[2486] | 35 | |
---|
[2685] | 36 | definition intensional_events_of_events : trace → list intensional_event ≝ |
---|
| 37 | λtr. flatten ? (map ?? intensional_event_of_event tr). |
---|
[2486] | 38 | |
---|
[2685] | 39 | let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝ |
---|
| 40 | match trace with |
---|
| 41 | [ nil ⇒ 〈callstack, [ ]〉 |
---|
| 42 | | cons str tl ⇒ |
---|
| 43 | let 〈s,tr〉 ≝ str in |
---|
| 44 | let 〈callstack, call_event〉 ≝ |
---|
| 45 | match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with |
---|
| 46 | [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉 |
---|
| 47 | | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ] |
---|
| 48 | | _ ⇒ λ_. 〈callstack, [ ]〉 |
---|
| 49 | ] (cs_callee C s) in |
---|
| 50 | let other_events ≝ intensional_events_of_events tr in |
---|
| 51 | let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in |
---|
| 52 | 〈callstack, call_event@other_events@rem〉 |
---|
| 53 | ]. |
---|
[2668] | 54 | |
---|
[2685] | 55 | definition normal_state : ∀C:classified_system. cs_state … C → bool ≝ |
---|
| 56 | λC,s. match cs_classify C s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
| 57 | |
---|
| 58 | lemma normal_state_inv : ∀C,s. |
---|
| 59 | normal_state C s → |
---|
| 60 | cs_classify C s = cl_other ∨ cs_classify C s = cl_jump. |
---|
| 61 | #C #s whd in ⊢ (?% → ?); cases (cs_classify C s) /2/ * |
---|
| 62 | qed. |
---|
| 63 | |
---|
| 64 | lemma int_trace_of_normal : ∀C,callstack,s,tr,trace. |
---|
| 65 | normal_state C s → |
---|
| 66 | intensional_trace_of_trace C callstack (〈s,tr〉::trace) = |
---|
| 67 | (let 〈stk',tl〉 ≝ intensional_trace_of_trace C callstack trace in |
---|
| 68 | 〈stk', (intensional_events_of_events tr)@tl〉). |
---|
| 69 | #C #callstack #s #tr #trace #NORMAL |
---|
| 70 | whd in ⊢ (??%?); |
---|
| 71 | generalize in match (cs_callee C s); |
---|
| 72 | cases (normal_state_inv … NORMAL) |
---|
| 73 | #CL >CL normalize nodelta #_ |
---|
| 74 | cases (intensional_trace_of_trace C callstack trace) |
---|
| 75 | #callstack' #tl normalize nodelta |
---|
| 76 | % |
---|
| 77 | qed. |
---|
| 78 | |
---|
| 79 | lemma flatten_append : ∀A,l1,l2. |
---|
| 80 | flatten A (l1@l2) = (flatten A l1)@(flatten A l2). |
---|
| 81 | #A #l1 #l2 |
---|
| 82 | elim l1 |
---|
| 83 | [ % |
---|
| 84 | | #h #t #IH whd in ⊢ (??%(??%?)); |
---|
| 85 | change with (flatten ??) in match (foldr ?????); >IH |
---|
| 86 | change with (flatten ??) in match (foldr ?????); |
---|
| 87 | >associative_append % |
---|
| 88 | ] qed. |
---|
| 89 | |
---|
| 90 | |
---|
| 91 | lemma int_events_append : ∀tr1,tr2. |
---|
| 92 | intensional_events_of_events (tr1@tr2) = (intensional_events_of_events tr1)@(intensional_events_of_events tr2). |
---|
| 93 | #tr1 #tr2 |
---|
| 94 | change with (flatten ??) in ⊢ (??%(??%%)); |
---|
| 95 | <map_append >flatten_append % |
---|
| 96 | qed. |
---|
| 97 | |
---|
| 98 | |
---|
| 99 | lemma int_trace_irr : ∀C,callstack,s,trace. |
---|
| 100 | normal_state C s → |
---|
| 101 | intensional_trace_of_trace C callstack (〈s,E0〉::trace) = intensional_trace_of_trace C callstack trace. |
---|
| 102 | #C #callstate #s #trace #NORMAL >(int_trace_of_normal … NORMAL) |
---|
| 103 | cases (intensional_trace_of_trace ???) // |
---|
| 104 | qed. |
---|
| 105 | |
---|
| 106 | lemma int_trace_append : ∀C,callstack,s,t1,t2,trace. |
---|
| 107 | normal_state C s → |
---|
| 108 | intensional_trace_of_trace C callstack (〈s,t1@t2〉::trace) = intensional_trace_of_trace C callstack (〈s,t1〉::〈s,t2〉::trace). |
---|
| 109 | #C #callstack #s #t1 #t2 #trace #NORMAL |
---|
| 110 | >(int_trace_of_normal … NORMAL) |
---|
| 111 | >(int_trace_of_normal … NORMAL) |
---|
| 112 | >(int_trace_of_normal … NORMAL) |
---|
| 113 | cases (intensional_trace_of_trace ???) #callstack' #trace' |
---|
| 114 | normalize nodelta |
---|
| 115 | >int_events_append |
---|
| 116 | >associative_append % |
---|
| 117 | qed. |
---|
| 118 | |
---|
| 119 | lemma build_eq_trace : ∀C,C',callstack,s,trace,rem,rem'. |
---|
| 120 | normal_state C s → |
---|
| 121 | all … (λstr. normal_state C' (\fst str)) trace → |
---|
| 122 | intensional_trace_of_trace C callstack rem = intensional_trace_of_trace C' callstack rem' → |
---|
| 123 | intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem'). |
---|
| 124 | #C #C' #callstack #s #trace #rem #rem' #NORMAL #NORMAL' |
---|
| 125 | >(int_trace_of_normal … NORMAL) |
---|
| 126 | cases (intensional_trace_of_trace C callstack rem) #callstack' #trace' |
---|
| 127 | #REM whd in ⊢ (??%?); |
---|
| 128 | elim trace in NORMAL' ⊢ %; |
---|
| 129 | [ #_ @REM |
---|
| 130 | | * #s' #tr' #tl #IH #NORMAL' |
---|
| 131 | cases (andb_Prop_true … NORMAL') #NORMALs #NORMALtl |
---|
| 132 | >int_trace_of_normal |
---|
| 133 | [ <(IH NORMALtl) whd in match (gather_trace ??); whd in ⊢ (???%); |
---|
| 134 | >int_events_append >associative_append % |
---|
| 135 | | @NORMALs |
---|
| 136 | ] |
---|
| 137 | ] qed. |
---|
| 138 | |
---|
| 139 | lemma int_trace_append' : ∀C,t1,t2,callstack. |
---|
| 140 | intensional_trace_of_trace C callstack (t1@t2) = |
---|
| 141 | (let 〈cs',t1'〉 ≝ intensional_trace_of_trace C callstack t1 in |
---|
| 142 | let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C cs' t2 in |
---|
| 143 | 〈cs'', t1'@t2'〉). |
---|
| 144 | #C #t1 #t2 elim t1 |
---|
| 145 | [ #callstack whd in match ([ ]@t2); whd in ⊢ (???%); |
---|
| 146 | cases (intensional_trace_of_trace ???) #cs' #trace' % |
---|
| 147 | | * #s #tr #tl #IH |
---|
| 148 | #callstack |
---|
| 149 | whd in match (intensional_trace_of_trace ???); |
---|
| 150 | whd in match (intensional_trace_of_trace ???); |
---|
| 151 | generalize in match (cs_callee C s); |
---|
| 152 | cases (cs_classify C s) |
---|
| 153 | normalize nodelta #callee |
---|
| 154 | [ cases callstack [2: #cshd #cdtl] normalize nodelta ] |
---|
| 155 | >IH cases (intensional_trace_of_trace C ? tl) #cs' #tl' |
---|
| 156 | normalize nodelta |
---|
| 157 | cases (intensional_trace_of_trace C ? t2) #cs'' #tl'' |
---|
| 158 | normalize nodelta >associative_append >associative_append |
---|
| 159 | % |
---|
| 160 | ] qed. |
---|
| 161 | |
---|
| 162 | lemma int_trace_normal_cs : ∀C,callstack,trace. |
---|
| 163 | all ? (λstr. normal_state C (\fst str)) trace → |
---|
| 164 | callstack = \fst (intensional_trace_of_trace C callstack trace). |
---|
| 165 | #C #callstack #trace elim trace |
---|
| 166 | [ // |
---|
| 167 | | * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl |
---|
| 168 | >(int_trace_of_normal … N1) |
---|
| 169 | >(IH Ntl) in ⊢ (??%?); |
---|
| 170 | cases (intensional_trace_of_trace ???) /2/ |
---|
| 171 | ] qed. |
---|
| 172 | |
---|
| 173 | lemma int_trace_append_normal : ∀C,t1,t2,callstack. |
---|
| 174 | all ? (λstr. normal_state C (\fst str)) t1 → |
---|
| 175 | intensional_trace_of_trace C callstack (t1@t2) = |
---|
| 176 | (let t1' ≝ \snd (intensional_trace_of_trace C callstack t1) in |
---|
| 177 | let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C callstack t2 in |
---|
| 178 | 〈cs'', t1'@t2'〉). |
---|
| 179 | #C #t1 #t2 #callstack #NORMAL lapply (int_trace_append' C t1 t2 callstack) |
---|
| 180 | lapply (int_trace_normal_cs C callstack t1 NORMAL) |
---|
| 181 | cases (intensional_trace_of_trace ?? t1) #cs #tl #E destruct // |
---|
| 182 | qed. |
---|
| 183 | |
---|
| 184 | lemma build_return_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem'. |
---|
| 185 | cs_classify C s = cl_return → |
---|
| 186 | cs_classify C' s' = cl_return → |
---|
| 187 | all ? (λstr. normal_state C' (\fst str)) trace' → |
---|
| 188 | intensional_trace_of_trace C (tail … callstack) rem = intensional_trace_of_trace C' (tail … callstack) rem' → |
---|
| 189 | let trace ≝ 〈s',tr〉::trace' in |
---|
| 190 | intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem'). |
---|
| 191 | #C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E |
---|
| 192 | whd |
---|
| 193 | whd in ⊢ (??%%); normalize nodelta |
---|
| 194 | generalize in match (cs_callee C s); generalize in match (cs_callee C' s'); |
---|
| 195 | >CL >CL' normalize nodelta #_ #_ |
---|
| 196 | cases callstack in E ⊢ %; [2: #stkhd #stktl] |
---|
| 197 | normalize nodelta |
---|
| 198 | cases (intensional_trace_of_trace ?? rem) #cs_rem #ev_rem normalize nodelta |
---|
| 199 | >(int_trace_append_normal … NORMAL) normalize nodelta |
---|
| 200 | cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E |
---|
| 201 | destruct @eq_f @eq_f |
---|
| 202 | whd in match (gather_trace ??); >int_events_append |
---|
| 203 | >associative_append @eq_f |
---|
| 204 | elim trace in NORMAL ⊢ %; |
---|
| 205 | [ 1,3: #_ % |
---|
| 206 | | 2,4: |
---|
| 207 | * #s1 #tr1 #tl #IH |
---|
| 208 | #N cases (andb_Prop_true … N) #N1 #Ntl |
---|
| 209 | whd in match (gather_trace ??); >int_events_append |
---|
| 210 | >associative_append >(IH Ntl) |
---|
| 211 | >(int_trace_of_normal … N1) |
---|
| 212 | cases (intensional_trace_of_trace ?? tl) |
---|
| 213 | #cs' #tl' >associative_append % |
---|
| 214 | ] qed. |
---|
| 215 | |
---|
| 216 | lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop. |
---|
| 217 | (∀f. P f (f H)) → |
---|
| 218 | P (cs_callee C s) (cs_callee C s H). |
---|
| 219 | #C #s #H #P #f @f |
---|
| 220 | qed. |
---|
| 221 | |
---|
| 222 | lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'. |
---|
| 223 | cs_classify C s = cl_call → |
---|
| 224 | cs_classify C' s' = cl_call → |
---|
| 225 | all ? (λstr. normal_state C' (\fst str)) trace' → |
---|
| 226 | intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' → |
---|
| 227 | cs_callee C s H = cs_callee C' s' H' → |
---|
| 228 | let trace ≝ 〈s',tr〉::trace' in |
---|
| 229 | intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem'). |
---|
| 230 | #C #C' #callstack #s #s' #tr #trace #rem #rem' #H #H' #CL #CL' #NORMAL |
---|
| 231 | whd in ⊢ (? → ? → %); |
---|
| 232 | whd in ⊢ (? → ? → ??%%); normalize nodelta |
---|
| 233 | @generalize_callee |
---|
| 234 | @generalize_callee |
---|
| 235 | >CL in H ⊢ %; * >CL' in H' ⊢ %; * normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE |
---|
| 236 | cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta |
---|
| 237 | >(int_trace_append_normal … NORMAL) normalize nodelta |
---|
| 238 | cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E |
---|
| 239 | destruct @eq_f @eq_f |
---|
| 240 | whd in match (gather_trace ??); >int_events_append |
---|
| 241 | >associative_append @eq_f |
---|
| 242 | elim trace in NORMAL ⊢ %; |
---|
| 243 | [ 1,3: #_ % |
---|
| 244 | | 2,4: |
---|
| 245 | * #s1 #tr1 #tl #IH |
---|
| 246 | #N cases (andb_Prop_true … N) #N1 #Ntl |
---|
| 247 | whd in match (gather_trace ??); >int_events_append |
---|
| 248 | >associative_append >(IH Ntl) |
---|
| 249 | >(int_trace_of_normal … N1) |
---|
| 250 | cases (intensional_trace_of_trace ?? tl) |
---|
| 251 | #cs' #tl' >associative_append % |
---|
| 252 | ] qed. |
---|
| 253 | |
---|
| 254 | |
---|
| 255 | definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝ |
---|
| 256 | λcosts,start. |
---|
| 257 | foldl ?? (λx. λev. |
---|
| 258 | match ev with |
---|
| 259 | [ IEVcall id ⇒ |
---|
| 260 | let 〈current_stack,max_stack〉 ≝ x in |
---|
| 261 | let new_stack ≝ current_stack + costs id in |
---|
| 262 | 〈new_stack, max new_stack max_stack〉 |
---|
| 263 | | IEVret id ⇒ |
---|
| 264 | let 〈current_stack,max_stack〉 ≝ x in |
---|
| 265 | 〈current_stack - costs id, max_stack〉 |
---|
| 266 | | _ ⇒ x |
---|
| 267 | ]) 〈start,start〉. |
---|
| 268 | |
---|
| 269 | definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝ |
---|
| 270 | λcosts, start, trace. \snd (measure_stack costs start trace). |
---|
| 271 | |
---|
[2668] | 272 | lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f. |
---|
| 273 | (∀acc,el. P acc → P (f acc el)) → |
---|
| 274 | ∀l,acc. P acc → |
---|
| 275 | P (foldl A B f acc l). |
---|
| 276 | #A #B #P #f #IH #l elim l |
---|
| 277 | [ // |
---|
| 278 | | #h #t #IH' #acc #H @IH' @IH @H |
---|
| 279 | ] qed. |
---|
[2685] | 280 | (* |
---|
[2668] | 281 | lemma max_stack_step : ∀C,a,m,a',m',tr,s. |
---|
[2669] | 282 | measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 → |
---|
[2668] | 283 | m' = max m a'. |
---|
| 284 | #C #a #m #a' #m' #tr #s |
---|
| 285 | whd in match (measure_stack_aux ???); |
---|
| 286 | generalize in match (cs_stack C s); cases (cs_classify C s) #f |
---|
| 287 | normalize nodelta #E destruct // |
---|
| 288 | qed. |
---|
| 289 | |
---|
[2669] | 290 | lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str. |
---|
| 291 | measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 → |
---|
| 292 | measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 → |
---|
[2668] | 293 | a1' = a2'. |
---|
[2669] | 294 | #C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr |
---|
[2668] | 295 | whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???); |
---|
| 296 | generalize in match (cs_stack C s); cases (cs_classify C s) #f |
---|
| 297 | normalize nodelta |
---|
| 298 | #E1 #E2 destruct |
---|
| 299 | % |
---|
| 300 | qed. |
---|
| 301 | |
---|
| 302 | |
---|
| 303 | lemma max_stack_steps : ∀C,trace,a,m. |
---|
| 304 | \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) = |
---|
| 305 | max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)). |
---|
| 306 | #C #trace elim trace |
---|
| 307 | [ #a #m >max_n_O % |
---|
| 308 | | * #tr #s #tl #IH #a #m |
---|
| 309 | whd in match (foldl ?????); |
---|
| 310 | letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M |
---|
| 311 | whd in match (foldl ??? 〈a,O〉 ?); |
---|
| 312 | letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M' |
---|
| 313 | >(IH a'') >IH |
---|
| 314 | >(max_stack_step … M) |
---|
| 315 | >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max % |
---|
| 316 | ] qed. |
---|
| 317 | |
---|
| 318 | lemma max_stack_append : ∀C,c1,ex1,ex2. |
---|
| 319 | max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2). |
---|
| 320 | #C #c1 #ex1 #ex2 |
---|
| 321 | whd in match (max_stack ???); whd in match (stack_after ???); |
---|
| 322 | whd in match (max_stack ?? (ex1@ex2)); |
---|
| 323 | whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2)); |
---|
| 324 | generalize in match O; generalize in match c1; elim ex1 |
---|
| 325 | [ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps % |
---|
| 326 | | * #tr #s #tl #IH #c #m |
---|
| 327 | whd in match (foldl ?????); whd in ⊢ (???(???%)); |
---|
| 328 | lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉)) |
---|
| 329 | cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M |
---|
| 330 | >IH % |
---|
| 331 | ] qed. |
---|
[2685] | 332 | *) |
---|
[2668] | 333 | |
---|
[2534] | 334 | (* Check that the trace ends with the return from the starting function and one |
---|
| 335 | further state. *) |
---|
| 336 | |
---|
[2486] | 337 | let rec will_return_aux C (depth:nat) |
---|
[2669] | 338 | (trace:list (cs_state … C × trace)) on trace : bool ≝ |
---|
[2486] | 339 | match trace with |
---|
[2534] | 340 | [ nil ⇒ false |
---|
[2486] | 341 | | cons h tl ⇒ |
---|
[2669] | 342 | let 〈s,tr〉 ≝ h in |
---|
[2486] | 343 | match cs_classify C s with |
---|
| 344 | [ cl_call ⇒ will_return_aux C (S depth) tl |
---|
| 345 | | cl_return ⇒ |
---|
| 346 | match depth with |
---|
[2669] | 347 | (* The state after the return will appear in the structured trace, but |
---|
| 348 | not here because it is the second part of the pair returned by |
---|
| 349 | exec_steps. *) |
---|
| 350 | [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ] |
---|
[2486] | 351 | | S d ⇒ will_return_aux C d tl |
---|
| 352 | ] |
---|
| 353 | | _ ⇒ will_return_aux C depth tl |
---|
| 354 | ] |
---|
| 355 | ]. |
---|
[2669] | 356 | definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O. |
---|
[2486] | 357 | |
---|
[2618] | 358 | (* Like classified_system, but we don't fix the global environment so that we |
---|
| 359 | talk about the program separately. *) |
---|
| 360 | |
---|
[2486] | 361 | record preclassified_system : Type[2] ≝ { |
---|
| 362 | pcs_exec :> fullexec io_out io_in; |
---|
| 363 | pcs_labelled : ∀g. state … pcs_exec g → bool; |
---|
[2596] | 364 | pcs_classify : ∀g. state … pcs_exec g → status_class; |
---|
[2685] | 365 | pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | _ ⇒ False ] → ident |
---|
[2486] | 366 | }. |
---|
| 367 | |
---|
[2685] | 368 | definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝ |
---|
| 369 | λC,g. |
---|
| 370 | mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?). |
---|
[2618] | 371 | |
---|
[2511] | 372 | (* FIXME: this definition is unreasonable because it presumes we can easily |
---|
| 373 | identify the change in stack usage from return states, but that information |
---|
| 374 | is rather implicit (we only really record the function called in the |
---|
| 375 | extended RTLabs states when building the structured traces). *) |
---|
| 376 | |
---|
[2486] | 377 | definition measurable : ∀C:preclassified_system. |
---|
| 378 | ∀p:program ?? C. nat → nat → |
---|
[2596] | 379 | (ident → nat) (* stack cost *) → |
---|
[2486] | 380 | nat → Prop ≝ |
---|
[2668] | 381 | λC,p,m,n,stack_cost,max_allowed_stack. ∃s0,prefix,s1,interesting,s2. |
---|
| 382 | let g ≝ make_global … (pcs_exec … C) p in |
---|
[2685] | 383 | let C' ≝ pcs_to_cs C g in |
---|
[2668] | 384 | make_initial_state … p = OK ? s0 ∧ |
---|
| 385 | exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧ |
---|
| 386 | exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧ |
---|
[2534] | 387 | trace_is_label_to_return C' interesting ∧ |
---|
[2486] | 388 | bool_to_Prop (will_return' C' interesting) ∧ |
---|
[2685] | 389 | le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack. |
---|
[2502] | 390 | |
---|
[2668] | 391 | (* TODO: probably ought to be elsewhere; use exec_steps instead |
---|
[2502] | 392 | |
---|
| 393 | Note that this does not include stack space |
---|
| 394 | *) |
---|
| 395 | |
---|
| 396 | definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝ |
---|
| 397 | λFE,p,m,n. |
---|
| 398 | let trace ≝ exec_inf … FE p in |
---|
[2618] | 399 | match split_trace … trace m with |
---|
[2502] | 400 | [ Some x ⇒ |
---|
| 401 | let 〈prefix,suffix〉 ≝ x in |
---|
[2618] | 402 | match split_trace … suffix n with |
---|
[2502] | 403 | [ Some y ⇒ |
---|
| 404 | let interesting ≝ \fst y in |
---|
| 405 | Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉 |
---|
| 406 | | _ ⇒ None ? |
---|
| 407 | ] |
---|
| 408 | | _ ⇒ None ? |
---|
| 409 | ]. |
---|
| 410 | |
---|
| 411 | definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝ |
---|
| 412 | λFE,p,m. |
---|
| 413 | let trace ≝ exec_inf … FE p in |
---|
[2618] | 414 | match split_trace … trace m with |
---|
[2502] | 415 | [ Some x ⇒ |
---|
| 416 | match \snd x with |
---|
| 417 | [ e_step _ s _ ⇒ Some ? s |
---|
| 418 | | e_stop _ _ s ⇒ Some ? s |
---|
| 419 | | _ ⇒ None ? |
---|
| 420 | ] |
---|
| 421 | | _ ⇒ None ? |
---|
| 422 | ]. |
---|