Changeset 3021
 Timestamp:
 Mar 28, 2013, 7:11:09 PM (7 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/label.ma
r2588 r3021 56 56 λp. Σl. in_clight_program p l. 57 57 58 (* Providing these proofs isn't easy, and doesn't seem to have any benefit, so 59 let's stick with a simpler form. 58 60 definition clight_cost_map ≝ 59 61 λp. (in_clight_label p) → ℕ. 62 *) 63 64 definition clight_cost_map ≝ costlabel → ℕ. 60 65 61 66 definition clight_label_free : clight_program → bool ≝ 
src/compiler.ma
r3018 r3021 128 128 include "ASM/ASMCosts.ma". 129 129 130 definition lift_out_of_sigma : 131 ∀A,B : Type[0].∀P_out : A → Prop.B → 132 (∀a.P_out a + ¬ P_out a) → 133 ((Σa.P_out a) → B) → A → B ≝ λA,B,P_out,dflt,dec,m,a_sig. 134 match dec a_sig with 135 [ inl prf ⇒ m «a_sig, prf» 136  inr _ ⇒ dflt (* labels not present in out code get 0 *) 137 ]. 138 130 139 definition lift_cost_map_back_to_front : 131 ∀ clight,oc.140 ∀oc. 132 141 let abstat ≝ OC_abstract_status oc in 133 as_cost_map abstat → clight_cost_map clight≝134 λ clight,oc,k,asm_cost_map.135 lift_ sigma_map_id… 0 (* labels not present in out code get 0 *)136 (strong_decidable_in_codomain …) kasm_cost_map.142 as_cost_map abstat → clight_cost_map ≝ 143 λoc,asm_cost_map. 144 lift_out_of_sigma … 0 (* labels not present in out code get 0 *) 145 (strong_decidable_in_codomain …) asm_cost_map. 137 146 138 147 (* Cost model computation *) … … 144 153 ; c_max_stack: nat 145 154 ; c_labelled_clight: clight_program 146 ; c_clight_cost_map: clight_cost_map c_labelled_clight155 ; c_clight_cost_map: clight_cost_map 147 156 }. 148 157 … … 154 163 let k ≝ ASM_cost_map p in 155 164 let k' ≝ 156 lift_cost_map_back_to_front p ' pk in165 lift_cost_map_back_to_front p k in 157 166 return mk_compiler_output p stack_cost max_stack p' k'. 
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.