Changeset 2506 for src/correctness.ma
 Timestamp:
 Nov 29, 2012, 6:38:37 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r2475 r2506 39 39 40 40 include "Clight/abstract.ma". 41 include "common/Measurable.ma". 41 42 42 43 definition Clight_stack_T ≝ ∀s:Clight_state. match Clight_classify s with [ cl_call ⇒ True  cl_return ⇒ True  _ ⇒ False ] → nat. 43 44 44 definition execution_prefix : Type[0] ≝ list (trace × Clight_state). 45 let rec split_trace (x:execution Clight_state io_out io_in) (n:nat) on n : option (execution_prefix × (execution Clight_state io_out io_in)) ≝ 46 match n with 47 [ O ⇒ Some ? 〈[ ], x〉 48  S n' ⇒ 49 match x with 50 [ e_step tr s x' ⇒ 51 ! 〈pre,x''〉 ← split_trace x' n'; 52 Some ? 〈〈tr,s〉::pre,x''〉 53  _ ⇒ None ? 54 ] 55 ]. 56 57 definition trace_labelled : execution_prefix → Prop ≝ 58 λx. ∃tr1,s1,x',tr2,s2. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉]) ∧ bool_to_Prop (Clight_labelled s1) ∧ bool_to_Prop (Clight_labelled s2). 59 60 definition measure_stack : Clight_stack_T → execution_prefix → nat × nat ≝ 61 λstack_cost. 62 foldl … (λx, trs. 63 let 〈current,max_stack〉 ≝ x in 64 let 〈tr,s〉 ≝ trs in 65 let new ≝ 66 match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ? with 67 [ cl_call ⇒ λsc. current + sc I 68  cl_return ⇒ λsc. current  sc I 69  _ ⇒ λ_. current 70 ] (stack_cost s) in 71 〈new, max max_stack new〉) 〈0,0〉. 72 73 definition stack_after : Clight_stack_T → execution_prefix → nat ≝ 74 λsc,x. \fst (measure_stack sc x). 75 76 definition max_stack : Clight_stack_T → execution_prefix → nat ≝ 77 λsc,x. \snd (measure_stack sc x). 78 79 let rec will_return_aux (depth:nat) 80 (trace:execution_prefix) on trace : bool ≝ 81 match trace with 82 [ nil ⇒ match depth with [ O ⇒ true  _ ⇒ false ] 83  cons h tl ⇒ 84 let 〈tr,s〉 ≝ h in 85 match Clight_classify s with 86 [ cl_call ⇒ will_return_aux (S depth) tl 87  cl_return ⇒ 88 match depth with 89 [ O ⇒ false 90  S d ⇒ will_return_aux d tl 91 ] 92  _ ⇒ will_return_aux depth tl 93 ] 94 ]. 95 definition will_return' : execution_prefix → bool ≝ will_return_aux O. 96 97 definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝ 98 λp,m,n,stack_cost,max_allowed_stack. ∀prefix,suffix,interesting,remainder. 99 let cl_trace ≝ exec_inf … clight_fullexec p in 100 split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧ 101 split_trace suffix n = Some ? 〈interesting,remainder〉 ∧ 102 trace_labelled interesting ∧ 103 bool_to_Prop (will_return' interesting) ∧ 104 max_stack stack_cost (prefix@interesting) < max_allowed_stack. 45 definition Clight_pcs : preclassified_system ≝ 46 mk_preclassified_system 47 clight_fullexec 48 (λ_.Clight_labelled) 49 (λ_.Clight_classify). 105 50 106 51 (* From measurable on Clight, we will end up with an RTLabs flat trace where … … 114 59 *) 115 60 116 definition observables : clight_program → nat → nat → option ((list trace) × (list trace)) ≝117 λp,m,n.118 let cl_trace ≝ exec_inf … clight_fullexec p in119 match split_trace cl_trace m with120 [ Some x ⇒121 let 〈prefix,suffix〉 ≝ x in122 match split_trace suffix n with123 [ Some y ⇒124 let interesting ≝ \fst y in125 Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉126  _ ⇒ None ?127 ]128  _ ⇒ None ?129 ].130 131 61 axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)). 132 62 133 definition in_execution_prefix : execution_prefix → costlabel → Prop ≝63 definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝ 134 64 λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x. 135 65 … … 155 85 ] qed. 156 86 157 definition measure_clock : ∀x:execution_prefix . ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝87 definition measure_clock : ∀x:execution_prefix Clight_state. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝ 158 88 λx,costmap. foldl_exists … x 159 89 (λclock,trs,H. … … 166 96 λp,n,costmap. 167 97 let x ≝ exec_inf … clight_fullexec p in 168 match split_trace x n with98 match split_trace … x n with 169 99 [ Some traces ⇒ 170 100 Some ? (measure_clock (\fst traces) (λl.costmap «l,?»)) … … 177 107 178 108 definition simulates ≝ 179 λstack_cost ,stack_bound, labelled, object_code, cost_map.109 λstack_cost : Clight_stack_T. λ stack_bound, labelled, object_code, cost_map. 180 110 let initial_status ≝ initial_8051_status (load_code_memory object_code) in 181 ∀m1,m2. measurable labelled m1 m2 stack_cost stack_bound →111 ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound → 182 112 ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 → 183 ∃n1,n2. observables labelled m1 m2 = observables_8051 object_code n1 n2 ∧113 ∃n1,n2. observables clight_fullexec labelled m1 m2 = observables_8051 object_code n1 n2 ∧ 184 114 c2  c1 = clock … (execute n2 ? initial_status)  clock … (execute n1 ? initial_status). 185 115
Note: See TracChangeset
for help on using the changeset viewer.