Changeset 2722 for src/correctness.ma
 Timestamp:
 Feb 23, 2013, 5:05:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r2677 r2722 47 47 definition stack_cost_T ≝ ident → nat. 48 48 49 (* Again, in principle we can use the fact that the state must be a call and 50 also show some relevant invariants about call states, but we go with the 51 easier option of returning zero elsewhere. *) 52 definition Clight_stack_cost : 53 stack_cost_T → 49 definition Clight_stack_ident : 54 50 cl_genv → 55 51 ∀s:Clight_state. 56 52 match Clight_classify s with [ cl_call ⇒ True  _ ⇒ False ] → 57 nat ≝ 58 λcost,ge,s,H. 59 match s with 60 [ Callstate v _ _ _ _ ⇒ 61 match v with [ Vptr p ⇒ match symbol_for_block … ge (pblock p) with [ Some id ⇒ cost id  _ ⇒ 0 ]  _ ⇒ 0 ] 62  _ ⇒ 0 53 ident ≝ 54 λge,s. 55 match s return λs. match Clight_classify s with [ cl_call ⇒ True  _ ⇒ False ] → ident with 56 [ Callstate id _ _ _ _ ⇒ λ_. id 57  _ ⇒ λH.⊥ 63 58 ]. 59 @H 60 qed. 64 61 65 62 definition Clight_pcs : preclassified_system ≝ … … 68 65 (λ_.Clight_labelled) 69 66 (λ_.Clight_classify) 70 Clight_stack_ cost.67 Clight_stack_ident. 71 68 72 69 (* From measurable on Clight, we will end up with an RTLabs flat trace where … … 80 77 *) 81 78 82 axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).79 axiom observables_8051 : object_code → nat → nat → res ((list intensional_event) × (list intensional_event)). 83 80 84 81 definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝ … … 132 129 ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound → 133 130 ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 → 134 ∃n1,n2. observables clight_fullexeclabelled m1 m2 = observables_8051 object_code n1 n2 ∧131 ∃n1,n2. observables Clight_pcs labelled m1 m2 = observables_8051 object_code n1 n2 ∧ 135 132 c2  c1 = clock … (execute n2 ? initial_status)  clock … (execute n1 ? initial_status). 136 133
Note: See TracChangeset
for help on using the changeset viewer.