Changeset 2399 for src/correctness.ma
 Timestamp:
 Oct 17, 2012, 6:45:20 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r2325 r2399 12 12 13 13 ∀object_code,costlabel_map,labelled,cost_map. 14 compile input_program = OK ? 〈〈object_code,costlabel_map〉, labelled,cost_map〉 →14 compile input_program = OK ? 〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉 → 15 15 16 16 not_wrong … (exec_inf … clight_fullexec input_program) → … … 41 41 42 42 definition execution_prefix : Type[0] ≝ list (trace × Clight_state). 43 axiom split_trace : execution Clight_state io_out io_in → nat → option (execution_prefix × (execution Clight_state io_out io_in)). 44 axiom stack_after : execution_prefix → nat. 43 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)) ≝ 44 match n with 45 [ O ⇒ Some ? 〈[ ], x〉 46  S n' ⇒ 47 match x with 48 [ e_step tr s x' ⇒ 49 ! 〈pre,x''〉 ← split_trace x' n'; 50 Some ? 〈〈tr,s〉::pre,x''〉 51  _ ⇒ None ? 52 ] 53 ]. 54 55 definition trace_labelled : execution_prefix → Prop ≝ 56 λx. ∃tr1,s1,x',tr2,s2. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉]) ∧ bool_to_Prop (Clight_labelled s1) ∧ bool_to_Prop (Clight_labelled s2). 57 58 definition measure_stack : Clight_stack_T → execution_prefix → nat × nat ≝ 59 λstack_cost. 60 foldl … (λx, trs. 61 let 〈current,max_stack〉 ≝ x in 62 let 〈tr,s〉 ≝ trs in 63 let new ≝ 64 match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ? with 65 [ cl_call ⇒ λsc. current + sc I 66  cl_return ⇒ λsc. current  sc I 67  _ ⇒ λ_. current 68 ] (stack_cost s) in 69 〈new, max max_stack new〉) 〈0,0〉. 70 71 definition stack_after : Clight_stack_T → execution_prefix → nat ≝ 72 λsc,x. \fst (measure_stack sc x). 73 74 definition max_stack : Clight_stack_T → execution_prefix → nat ≝ 75 λsc,x. \snd (measure_stack sc x). 45 76 46 77 (* TODO: cost labels *) … … 72 103 split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧ 73 104 split_trace suffix n = Some ? 〈interesting,remainder〉 ∧ 74 will_return' stack_cost (stack_after prefix) interesting = Some ? max_stack ∧ 105 trace_labelled interesting → 106 will_return' stack_cost (stack_after stack_cost prefix) interesting = Some ? max_stack ∧ 75 107 max_stack < max_allowed_stack. 76 108 … … 85 117 *) 86 118 87 axiom observables : clight_program → nat → nat → option ((list trace) × (list trace)). 119 definition observables : clight_program → nat → nat → option ((list trace) × (list trace)) ≝ 120 λp,m,n. 121 let cl_trace ≝ exec_inf … clight_fullexec p in 122 match split_trace cl_trace m with 123 [ Some x ⇒ 124 let 〈prefix,suffix〉 ≝ x in 125 match split_trace suffix n with 126 [ Some y ⇒ 127 let interesting ≝ \fst y in 128 Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉 129  _ ⇒ None ? 130 ] 131  _ ⇒ None ? 132 ]. 133 88 134 axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)). 89 axiom clight_clock_after : clight_program → nat → option nat. 135 136 definition in_execution_prefix : execution_prefix → costlabel → Prop ≝ 137 λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x. 138 139 let rec foldl_exists_aux (A,B:Type[0]) (l,l':list B) (f:A → ∀b:B. Exists … (λx.x=b) l → A) (a:A) on l' : (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A ≝ 140 match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with 141 [ nil ⇒ λ_. a 142  cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ? 143 ]. 144 [ %1 % 145  #b #H' @H %2 @H' 146 ] qed. 147 148 definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝ 149 λA,B,l,f,a. foldl_exists_aux A B l l f a (λb,H. H). 150 151 lemma Exists_lift : ∀A,P,Q,l. 152 (∀x. P x → Q x) → 153 Exists A P l → 154 Exists A Q l. 155 #A #P #Q #l elim l 156 [ // 157  #h #t #IH #H * [ #H' %1 @H @H'  #H' %2 @IH /2/ ] 158 ] qed. 159 160 definition measure_clock : ∀x:execution_prefix. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝ 161 λx,costmap. foldl_exists … x 162 (λclock,trs,H. 163 foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?»  _ ⇒ λ_. clock ]) clock) 164 0. 165 whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E 166 qed. 167 168 definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝ 169 λp,n,costmap. 170 let x ≝ exec_inf … clight_fullexec p in 171 match split_trace x n with 172 [ Some traces ⇒ 173 Some ? (measure_clock (\fst traces) (λl.costmap «l,?»)) 174  None ⇒ None ? 175 ]. 176 cases daemon 177 qed. 178 90 179 axiom initial_8051_status : ∀oc. Status oc. 91 180 92 181 definition simulates ≝ 93 λstack_cost, stack_bound, labelled, object_code .182 λstack_cost, stack_bound, labelled, object_code, cost_map. 94 183 let initial_status ≝ initial_8051_status (load_code_memory object_code) in 95 184 ∀m1,m2. measurable labelled m1 m2 stack_cost stack_bound → 96 ∀c1,c2. clight_clock_after labelled m1 = Some ? c1 → clight_clock_after labelled m2= Some ? c2 →185 ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 → 97 186 ∃n1,n2. observables labelled m1 m2 = observables_8051 object_code n1 n2 ∧ 98 187 c2  c1 = clock … (execute n2 ? initial_status)  clock … (execute n1 ? initial_status). 99 188 100 axiom compile' : clight_program → res (object_code × costlabel_map × clight_program101 × ((Σl:costlabel.in_clight_program l)→ℕ) × Clight_stack_T × nat).189 axiom compile' : clight_program → res (object_code × costlabel_map × 190 (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled l)→ℕ)) × Clight_stack_T × nat). 102 191 103 192 theorem correct' : … … 107 196 108 197 ∀object_code,costlabel_map,labelled,cost_map,stack_cost,stack_bound. 109 compile' input_program = OK ? 〈〈〈 〈object_code,costlabel_map〉,labelled〉,cost_map〉,stack_cost,stack_bound〉 →198 compile' input_program = OK ? 〈〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉,stack_cost,stack_bound〉 → 110 199 111 200 sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled) 112 201 ∧ 113 202 114 simulates stack_cost stack_bound labelled object_code .203 simulates stack_cost stack_bound labelled object_code cost_map. 115 204 116 205
Note: See TracChangeset
for help on using the changeset viewer.