Changeset 3021 for src/correctness.ma
 Timestamp:
 Mar 28, 2013, 7:11:09 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r3003 r3021 72 72 ] qed. 73 73 74 definition measure_clock : ∀x:execution_prefix Clight_state. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝ 75 λx,costmap. foldl_exists … x 76 (λclock,trs,H. 77 foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?»  _ ⇒ λ_. clock ]) clock) 78 0. 79 whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E 80 qed. 81 82 definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝ 74 include "RTLabs/MeasurableToStructured.ma". 75 76 definition clight_clock_after : ∀p:clight_program. nat → (costlabel→ℕ) → res nat ≝ 83 77 λp,n,costmap. 84 let x ≝ exec_inf … clight_fullexec p in 85 match split_trace … x n with 86 [ Some traces ⇒ 87 Some ? (measure_clock (\fst traces) (λl.costmap «l,?»)) 88  None ⇒ None ? 89 ]. 90 cases daemon 91 qed. 78 ! 〈s,itrace〉 ← exec_steps_with_obs Clight_pcs p n; 79 let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl  _ ⇒ None ? ]) itrace in 80 return Σ_{l ∈ ctrace}(costmap l). 92 81 93 82 include "common/AssocList.ma". … … 104 93 (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) → 105 94 ∀c1,c2. 106 clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = Some ?c1 →107 clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = Some ?c2 →95 clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 → 96 clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = OK … c2 → 108 97 ∃n1,n2. 109 98 observables Clight_pcs (c_labelled_clight … p) m1 m2 =
Note: See TracChangeset
for help on using the changeset viewer.