Changeset 2800
 Timestamp:
 Mar 7, 2013, 1:07:31 PM (7 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Measurable.ma
r2795 r2800 24 24 definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝ 25 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. 26 27 (* Construction of the trace of intensional events. 28 29 It might be possible to merge these with the plain events, but for now we 30 combine those with call/return information taken from the states. 31 32 The build_* results help with the proof that measurable subtraces are 33 preserved in the frontend. *) 26 34 27 35 definition intensional_event_of_event : event → list intensional_event ≝ … … 73 81 % 74 82 qed. 75 76 lemma flatten_append : ∀A,l1,l2.77 flatten A (l1@l2) = (flatten A l1)@(flatten A l2).78 #A #l1 #l279 elim l180 [ %81  #h #t #IH whd in ⊢ (??%(??%?));82 change with (flatten ??) in match (foldr ?????); >IH83 change with (flatten ??) in match (foldr ?????);84 >associative_append %85 ] qed.86 83 87 84 … … 211 208 ] qed. 212 209 210 (* I had a little trouble doing this directly. *) 213 211 lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop. 214 212 (∀f. P f (f H)) → … … 247 245 #cs' #tl' >associative_append % 248 246 ] qed. 249 247 248 (* Measuring stack usage. TODO: I think there's another version of this from 249 the backend that should be merged. *) 250 250 251 251 definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝ … … 366 366 mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?). 367 367 368 (* FIXME: this definition is unreasonable because it presumes we can easily 369 identify the change in stack usage from return states, but that information 370 is rather implicit (we only really record the function called in the 371 extended RTLabs states when building the structured traces). *) 368 372 369 373 370 definition measurable : ∀C:preclassified_system. … … 385 382 le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack. 386 383 387 (* TODO: probably ought to be elsewhere; use exec_steps instead 388 389 Note that this does not include stack space 390 *) 384 391 385 392 386 definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝ 
src/utilities/lists.ma
r2443 r2800 244 244 ] 245 245 qed. 246 247 248 249 lemma flatten_append : ∀A,l1,l2. 250 flatten A (l1@l2) = (flatten A l1)@(flatten A l2). 251 #A #l1 #l2 252 elim l1 253 [ % 254  #h #t #IH whd in ⊢ (??%(??%?)); 255 change with (flatten ??) in match (foldr ?????); >IH 256 change with (flatten ??) in match (foldr ?????); 257 >associative_append % 258 ] qed. 246 259 247 260 … … 352 365 353 366 354 (* Not terribly efficient sort for testing purposes *)367 (* A not terribly efficient sort for testing purposes *) 355 368 356 369 let rec ordered_insert (A:Type[0]) (lt:A → A → bool) (a:A) (l:list A) on l : list A ≝
Note: See TracChangeset
for help on using the changeset viewer.