Changeset 2685
 Timestamp:
 Feb 21, 2013, 11:38:36 AM (6 years ago)
 Location:
 src/common
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r2678 r2685 3 3 include "common/Measurable.ma". 4 4 5 definition normal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝5 definition pnormal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝ 6 6 λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ]. 7 7 8 lemma normal_state_inv : ∀C,g,s.9 normal_state C g s →8 lemma pnormal_state_inv : ∀C,g,s. 9 pnormal_state C g s → 10 10 pcs_classify C g s = cl_other ∨ pcs_classify C g s = cl_jump. 11 11 #C #g #s whd in ⊢ (?% → ?); cases (pcs_classify C g s) /2/ * 12 qed. 13 14 lemma normal_state_p : ∀C,g,s. 15 pnormal_state C g s = normal_state (pcs_to_cs C g) s. 16 // 12 17 qed. 13 18 … … 26 31 ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat); 27 32 ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop; 28 ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (normal_state ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C2 g2 s2); 29 ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (pcs_labelled ms_C2 g2 s2); 33 ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pnormal_state ms_C1 g1 s1 = pnormal_state ms_C2 g2 s2; 34 ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_labelled ms_C1 g1 s1 = pcs_labelled ms_C2 g2 s2; 35 ms_rel_classify : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = pcs_classify ms_C2 g2 s2; 36 ms_rel_callee : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → ∀H,H'. pcs_callee ms_C1 g1 s1 H = pcs_callee ms_C2 g2 s2 H'; 30 37 31 38 (* These hold in (at least) the languages of interest for measurable subtraces *) 32 ms_labelled_normal_1 : ∀g1,s1. bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C1 g1 s1);33 ms_labelled_normal_2 : ∀g2,s2. bool_to_Prop (pcs_labelled ms_C2 g2 s2) ↔ bool_to_Prop (normal_state ms_C2 g2 s2);39 ms_labelled_normal_1 : ∀g1,s1. pcs_labelled ms_C1 g1 s1 → pnormal_state ms_C1 g1 s1; 40 ms_labelled_normal_2 : ∀g2,s2. pcs_labelled ms_C2 g2 s2 → pnormal_state ms_C2 g2 s2; 34 41 ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall; 35 42 … … 44 51 ∀s1,s1'. 45 52 ms_rel g1 g2 INV s1 s1' → 46 normal_state ms_C1 g1 s1 →53 pnormal_state ms_C1 g1 s1 → 47 54 ¬ pcs_labelled ms_C1 g1 s1 → 48 55 ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → 49 ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs. normal_state ms_C2 g2 s) (λtr',s2'.56 ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. 50 57 tr = tr' ∧ 51 58 ms_rel g1 g2 INV s2 s2' ∧ … … 60 67 ¬ pcs_labelled ms_C1 g1 s1 → 61 68 ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → 62 ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs. normal_state ms_C2 g2 s) (λtr',s2'.69 ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. 63 70 tr = tr' ∧ 64 71 ms_rel g1 g2 INV s2 s2' … … 84 91 85 92 (* TODO: obs eq *) 86 93 (* 87 94 lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. 88 95 exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → 89 normal_state C g s1 →96 pnormal_state C g s1 → 90 97 stack_after (pcs_to_cs C g stack) current trace = current. 91 98 #C #g #s1 #trace #s2 #stack #current #EXEC … … 95 102 whd in ⊢ (??%?); generalize in match (cs_stack ??); 96 103 whd in match (cs_classify ??); 97 cases ( normal_state_inv … N)104 cases (pnormal_state_inv … N) 98 105 #CL >CL #f % 99 106 qed. … … 101 108 lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. 102 109 exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → 103 normal_state C g s1 →110 pnormal_state C g s1 → 104 111 max_stack (pcs_to_cs C g stack) current trace = current. 105 112 #C #g #s1 #trace #s2 #stack #current #EXEC … … 109 116 whd in ⊢ (??%?); generalize in match (cs_stack ??); 110 117 whd in match (cs_classify ??); 111 cases ( normal_state_inv … N)118 cases (pnormal_state_inv … N) 112 119 #CL >CL #f % 113 120 qed. … … 161 168 cases (inv s2) // * ] // ] 162 169 qed. 163 170 *) 164 171 (* XXX do I need to do the max_stack reasoning here? perhaps just by preserving 165 172 observables? *) 166 173 174 lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'. 175 exec_steps 1 O I fx g s = OK ? 〈trace,s'〉 → 176 ∃tr. trace = [〈s,tr〉]. 177 #O #I #fx #g #s #trace #s' #EXEC 178 cases (exec_steps_S … EXEC) 179 #nf * #tr * #s'' * #tl * * #E1 #STEP #EXEC' whd in EXEC':(??%%); destruct 180 %{tr} % 181 qed. 182 183 lemma all_1 : ∀A.∀P:A → bool.∀x. 184 P x = all A P [x]. 185 #A #P #x whd in ⊢ (???%); cases (P x) // 186 qed. 167 187 168 188 (* WIP commented out*) … … 171 191 ∀g,g'. 172 192 ∀INV:ms_inv MS g g'. 173 ∀max_allowed_stack.174 193 ∀s1,s1'. 175 194 ms_rel MS g g' INV s1 s1' → … … 178 197 exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 → 179 198 pcs_labelled (ms_C1 MS) g sf → 180 le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack →181 199 182 200 ∃m',prefix',sf'. 183 201 exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧ 184 le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) 0 prefix') max_allowed_stack ∧ 185 202 203 intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧ 186 204 ms_rel MS g g' INV sf sf'. 187 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled # labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init188 #g #g' #INV # max #s1 #s1' #REL205 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init 206 #g #g' #INV #s1 #s1' #REL 189 207 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' 190 generalize in match 0; (* current stack level*)208 generalize in match [ ]; (* current call stack *) 191 209 elim m0 192 210 [ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf 193 #max_ok%{0} %{[]} %{s1'}211 %{0} %{[]} %{s1'} 194 212 % [ % //  // ] 195  #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #MAX_OK213  #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf 196 214 cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2 197 215 cases (true_or_false_Prop … (pcs_labelled … s1)) … … 200 218 #AFTER1' 201 219 cases (after_n_exec_steps … AFTER1') 202 #prefix' * #s2' * #EXEC1' * #Etrace #R2 203 cut (normal_state C1 g s1) [ @(proj1 … (labelled_normal1 …)) assumption ] #N1 204 cut (normal_state C2 g' s1') [ @(proj1 … (labelled_normal2 …)) @(proj1 … (rel_labelled … REL)) assumption ] #N1' 205 cases (IH (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?) 206 [ 2: @(transitive_le … MAX_OK) >E1 cases daemon (* <max_stack_append 207 >(stack_normal_step … EXEC1 N1) 208 >(stack_normal_step … EXEC1' N1') 209 @max_r //*) 210 ] 211 #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R'' 220 #prefix' * #s2' * * #EXEC1' #_ * #Etrace #R2 221 cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 222 cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' 223 cases (IH current_stack … R2 … EXEC2 CSf) 224 #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' 212 225 %{(1+m'')} %{(prefix'@prefix'')} %{sf''} 213 226 % [ % [ @(exec_steps_join … EXEC1') @EXEC'' 214  <max_stack_append @to_max 215 [ >(max_stack_normal_step … EXEC1' N1') 216 lapply MAX_OK >E1 cases daemon (* <max_stack_append 217 >(max_stack_normal_step … EXEC1 N1) 218 #H /2 by le_maxl/*) 219  @MAX'' ] ] 220  @R'' 227  destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // 228 cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct 229 <all_1 assumption 230 ] assumption 221 231 ] 222 232 223 233  #NCS 224 cases (true_or_false_Prop ( normal_state C1 g s1))234 cases (true_or_false_Prop (pnormal_state C1 g s1)) 225 235 [ #NORMAL 226 236 (* XXX should set things up so that notb_Prop isn't needed *) 227 237 cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1) 228 238 #n' #AFTER1' 229 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * * #Etrace #R2 #_ (* measure *) 230 cases (IH (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?) 231 [ 2: cases daemon ] (* XXX *) 232 #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R'' 239 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *) 240 cases (IH current_stack … R2 … EXEC2 CSf) 241 #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' 233 242 %{(n'+m'')} %{(prefix'@prefix'')} %{sf''} 234 243 % [ % [ @(exec_steps_join … EXEC1') @EXEC'' 235  <max_stack_append @to_max 236 [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1') 237 lapply MAX_OK >E1 <max_stack_append 238 >(max_stack_normal_step … EXEC1 N1) 239 #H /2 by le_maxl/*) 240  @MAX'' ] ] 244  destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 245 [ assumption 246  cases prefix' in EXEC1' INV ⊢ %; 247 [ // 248  * #sx #trx #tl #EXEC1' #INV 249 <(exec_steps_first … EXEC1') 250 whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL 251 @INV 252 ] 253  @OBS'' ] ] 241 254  @R'' 242 255 ] 243 256  #CALLRET 244 c ases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)245 [ 2: whd in CALLRET:(?%); whd in match (normal_state ???) in CALLRET;257 cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) 258 [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET; 246 259 lapply (no_tailcalls … s1) 247 260 cases (pcs_classify … s1) in CALLRET ⊢ %; 248 normalize * #H #H' try % try cases (H I) 249 cases H' /2/ ] 261 [ 1,3: #_ #_ /2/ 262  *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??)) 263 ] 264 ] * #CL 265 cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) 266 [2,4: >CL %] 250 267 #m' #AFTER1' 251 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * #Etrace #R2 252 cases (IH (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?) 253 [ 2: cases daemon ] (* XXX *) 254 #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R'' 268 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 269 [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] 270  letin next_stack ≝ (tail … current_stack) 271 ] 272 cases (IH next_stack … R2 … EXEC2 CSf) 273 #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' 255 274 %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} 256 % [ % [ @(exec_steps_join … EXEC1') @EXEC'' 257  <max_stack_append @to_max 258 [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1') 259 lapply MAX_OK >E1 <max_stack_append 260 >(max_stack_normal_step … EXEC1 N1) 261 #H /2 by le_maxl/*) 262  @MAX'' ] ] 263  @R'' 275 % [1,3: % [1,3: @(exec_steps_join … EXEC1') @EXEC'' 276  destruct cases (exec_steps_S … EXEC1') 277 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 278 destruct 279 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 280 [1,3: whd in match (cs_classify ??); >CL % 281 2,4: whd in match (cs_classify ??); <(rel_classify … REL) >CL % 282  @INV 283  assumption 284  @(rel_callee … REL) 285 ] 286  destruct cases (exec_steps_S … EXEC1') 287 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 288 destruct 289 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 290 [ whd in match (cs_classify ??); >CL % 291  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 292  @INV 293  assumption 294 ] 264 295 ] 296  2,4: @R'' 297 ] 265 298 ] 266 299 ] 267 qed.300 ] qed. 268 301 269 302 
src/common/Measurable.ma
r2670 r2685 11 11 cs_labelled : state … cs_exec cs_global → bool; 12 12 cs_classify : state … cs_exec cs_global → status_class; 13 cs_ stack : ∀s. match cs_classify … s with [ cl_call ⇒ True  cl_return ⇒ True  _ ⇒ False ] → nat13 cs_callee : ∀s. match cs_classify … s with [ cl_call ⇒ True  _ ⇒ False ] → ident 14 14 }. 15 15 … … 25 25 λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return. 26 26 27 definition measure_stack_aux ≝ 28 λC. (λx. λstr:cs_state … C × trace. 29 let 〈current,max_stack〉 ≝ x in 30 let 〈s,tr〉 ≝ str in 31 let new ≝ 32 match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ? with 33 [ cl_call ⇒ λsc. current + sc I 34  cl_return ⇒ λsc. current  sc I 35  _ ⇒ λ_. current 36 ] (cs_stack C s) in 37 〈new, max max_stack new〉). 38 39 definition measure_stack : ∀C. nat → list (cs_state … C × trace) → nat × nat ≝ 40 λC,current. 41 foldl … (measure_stack_aux C) 〈current,0〉. 42 43 definition stack_after : ∀C. nat → list (cs_state … C × trace) → nat ≝ 44 λC,current,x. \fst (measure_stack C current x). 45 46 definition max_stack : ∀C. nat → list (cs_state … C × trace) → nat ≝ 47 λC,current,x. \snd (measure_stack C current x). 27 (* For intensional_event; should separate out definition *) 28 include "common/StatusSimulation.ma". 29 30 definition intensional_event_of_event : event → list intensional_event ≝ 31 λev. match ev with 32 [ EVcost l ⇒ [ IEVcost l ] 33  EVextcall _ _ _ ⇒ [ ] (* No equivalent, but there shouldn't be any for now *) 34 ]. 35 36 definition intensional_events_of_events : trace → list intensional_event ≝ 37 λtr. flatten ? (map ?? intensional_event_of_event tr). 38 39 let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝ 40 match trace with 41 [ nil ⇒ 〈callstack, [ ]〉 42  cons str tl ⇒ 43 let 〈s,tr〉 ≝ str in 44 let 〈callstack, call_event〉 ≝ 45 match cs_classify C s return λx. (match x with [ cl_call ⇒ True  _ ⇒ False ] → ident) → list ident × (list intensional_event) with 46 [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉 47  cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉  cons id tl ⇒ 〈tl, [IEVret id]〉 ] 48  _ ⇒ λ_. 〈callstack, [ ]〉 49 ] (cs_callee C s) in 50 let other_events ≝ intensional_events_of_events tr in 51 let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in 52 〈callstack, call_event@other_events@rem〉 53 ]. 54 55 definition normal_state : ∀C:classified_system. cs_state … C → bool ≝ 56 λC,s. match cs_classify C s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ]. 57 58 lemma normal_state_inv : ∀C,s. 59 normal_state C s → 60 cs_classify C s = cl_other ∨ cs_classify C s = cl_jump. 61 #C #s whd in ⊢ (?% → ?); cases (cs_classify C s) /2/ * 62 qed. 63 64 lemma int_trace_of_normal : ∀C,callstack,s,tr,trace. 65 normal_state C s → 66 intensional_trace_of_trace C callstack (〈s,tr〉::trace) = 67 (let 〈stk',tl〉 ≝ intensional_trace_of_trace C callstack trace in 68 〈stk', (intensional_events_of_events tr)@tl〉). 69 #C #callstack #s #tr #trace #NORMAL 70 whd in ⊢ (??%?); 71 generalize in match (cs_callee C s); 72 cases (normal_state_inv … NORMAL) 73 #CL >CL normalize nodelta #_ 74 cases (intensional_trace_of_trace C callstack trace) 75 #callstack' #tl normalize nodelta 76 % 77 qed. 78 79 lemma flatten_append : ∀A,l1,l2. 80 flatten A (l1@l2) = (flatten A l1)@(flatten A l2). 81 #A #l1 #l2 82 elim l1 83 [ % 84  #h #t #IH whd in ⊢ (??%(??%?)); 85 change with (flatten ??) in match (foldr ?????); >IH 86 change with (flatten ??) in match (foldr ?????); 87 >associative_append % 88 ] qed. 89 90 91 lemma int_events_append : ∀tr1,tr2. 92 intensional_events_of_events (tr1@tr2) = (intensional_events_of_events tr1)@(intensional_events_of_events tr2). 93 #tr1 #tr2 94 change with (flatten ??) in ⊢ (??%(??%%)); 95 <map_append >flatten_append % 96 qed. 97 98 99 lemma int_trace_irr : ∀C,callstack,s,trace. 100 normal_state C s → 101 intensional_trace_of_trace C callstack (〈s,E0〉::trace) = intensional_trace_of_trace C callstack trace. 102 #C #callstate #s #trace #NORMAL >(int_trace_of_normal … NORMAL) 103 cases (intensional_trace_of_trace ???) // 104 qed. 105 106 lemma int_trace_append : ∀C,callstack,s,t1,t2,trace. 107 normal_state C s → 108 intensional_trace_of_trace C callstack (〈s,t1@t2〉::trace) = intensional_trace_of_trace C callstack (〈s,t1〉::〈s,t2〉::trace). 109 #C #callstack #s #t1 #t2 #trace #NORMAL 110 >(int_trace_of_normal … NORMAL) 111 >(int_trace_of_normal … NORMAL) 112 >(int_trace_of_normal … NORMAL) 113 cases (intensional_trace_of_trace ???) #callstack' #trace' 114 normalize nodelta 115 >int_events_append 116 >associative_append % 117 qed. 118 119 lemma build_eq_trace : ∀C,C',callstack,s,trace,rem,rem'. 120 normal_state C s → 121 all … (λstr. normal_state C' (\fst str)) trace → 122 intensional_trace_of_trace C callstack rem = intensional_trace_of_trace C' callstack rem' → 123 intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem'). 124 #C #C' #callstack #s #trace #rem #rem' #NORMAL #NORMAL' 125 >(int_trace_of_normal … NORMAL) 126 cases (intensional_trace_of_trace C callstack rem) #callstack' #trace' 127 #REM whd in ⊢ (??%?); 128 elim trace in NORMAL' ⊢ %; 129 [ #_ @REM 130  * #s' #tr' #tl #IH #NORMAL' 131 cases (andb_Prop_true … NORMAL') #NORMALs #NORMALtl 132 >int_trace_of_normal 133 [ <(IH NORMALtl) whd in match (gather_trace ??); whd in ⊢ (???%); 134 >int_events_append >associative_append % 135  @NORMALs 136 ] 137 ] qed. 138 139 lemma int_trace_append' : ∀C,t1,t2,callstack. 140 intensional_trace_of_trace C callstack (t1@t2) = 141 (let 〈cs',t1'〉 ≝ intensional_trace_of_trace C callstack t1 in 142 let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C cs' t2 in 143 〈cs'', t1'@t2'〉). 144 #C #t1 #t2 elim t1 145 [ #callstack whd in match ([ ]@t2); whd in ⊢ (???%); 146 cases (intensional_trace_of_trace ???) #cs' #trace' % 147  * #s #tr #tl #IH 148 #callstack 149 whd in match (intensional_trace_of_trace ???); 150 whd in match (intensional_trace_of_trace ???); 151 generalize in match (cs_callee C s); 152 cases (cs_classify C s) 153 normalize nodelta #callee 154 [ cases callstack [2: #cshd #cdtl] normalize nodelta ] 155 >IH cases (intensional_trace_of_trace C ? tl) #cs' #tl' 156 normalize nodelta 157 cases (intensional_trace_of_trace C ? t2) #cs'' #tl'' 158 normalize nodelta >associative_append >associative_append 159 % 160 ] qed. 161 162 lemma int_trace_normal_cs : ∀C,callstack,trace. 163 all ? (λstr. normal_state C (\fst str)) trace → 164 callstack = \fst (intensional_trace_of_trace C callstack trace). 165 #C #callstack #trace elim trace 166 [ // 167  * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl 168 >(int_trace_of_normal … N1) 169 >(IH Ntl) in ⊢ (??%?); 170 cases (intensional_trace_of_trace ???) /2/ 171 ] qed. 172 173 lemma int_trace_append_normal : ∀C,t1,t2,callstack. 174 all ? (λstr. normal_state C (\fst str)) t1 → 175 intensional_trace_of_trace C callstack (t1@t2) = 176 (let t1' ≝ \snd (intensional_trace_of_trace C callstack t1) in 177 let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C callstack t2 in 178 〈cs'', t1'@t2'〉). 179 #C #t1 #t2 #callstack #NORMAL lapply (int_trace_append' C t1 t2 callstack) 180 lapply (int_trace_normal_cs C callstack t1 NORMAL) 181 cases (intensional_trace_of_trace ?? t1) #cs #tl #E destruct // 182 qed. 183 184 lemma build_return_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem'. 185 cs_classify C s = cl_return → 186 cs_classify C' s' = cl_return → 187 all ? (λstr. normal_state C' (\fst str)) trace' → 188 intensional_trace_of_trace C (tail … callstack) rem = intensional_trace_of_trace C' (tail … callstack) rem' → 189 let trace ≝ 〈s',tr〉::trace' in 190 intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem'). 191 #C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E 192 whd 193 whd in ⊢ (??%%); normalize nodelta 194 generalize in match (cs_callee C s); generalize in match (cs_callee C' s'); 195 >CL >CL' normalize nodelta #_ #_ 196 cases callstack in E ⊢ %; [2: #stkhd #stktl] 197 normalize nodelta 198 cases (intensional_trace_of_trace ?? rem) #cs_rem #ev_rem normalize nodelta 199 >(int_trace_append_normal … NORMAL) normalize nodelta 200 cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E 201 destruct @eq_f @eq_f 202 whd in match (gather_trace ??); >int_events_append 203 >associative_append @eq_f 204 elim trace in NORMAL ⊢ %; 205 [ 1,3: #_ % 206  2,4: 207 * #s1 #tr1 #tl #IH 208 #N cases (andb_Prop_true … N) #N1 #Ntl 209 whd in match (gather_trace ??); >int_events_append 210 >associative_append >(IH Ntl) 211 >(int_trace_of_normal … N1) 212 cases (intensional_trace_of_trace ?? tl) 213 #cs' #tl' >associative_append % 214 ] qed. 215 216 lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop. 217 (∀f. P f (f H)) → 218 P (cs_callee C s) (cs_callee C s H). 219 #C #s #H #P #f @f 220 qed. 221 222 lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'. 223 cs_classify C s = cl_call → 224 cs_classify C' s' = cl_call → 225 all ? (λstr. normal_state C' (\fst str)) trace' → 226 intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' → 227 cs_callee C s H = cs_callee C' s' H' → 228 let trace ≝ 〈s',tr〉::trace' in 229 intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem'). 230 #C #C' #callstack #s #s' #tr #trace #rem #rem' #H #H' #CL #CL' #NORMAL 231 whd in ⊢ (? → ? → %); 232 whd in ⊢ (? → ? → ??%%); normalize nodelta 233 @generalize_callee 234 @generalize_callee 235 >CL in H ⊢ %; * >CL' in H' ⊢ %; * normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE 236 cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta 237 >(int_trace_append_normal … NORMAL) normalize nodelta 238 cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E 239 destruct @eq_f @eq_f 240 whd in match (gather_trace ??); >int_events_append 241 >associative_append @eq_f 242 elim trace in NORMAL ⊢ %; 243 [ 1,3: #_ % 244  2,4: 245 * #s1 #tr1 #tl #IH 246 #N cases (andb_Prop_true … N) #N1 #Ntl 247 whd in match (gather_trace ??); >int_events_append 248 >associative_append >(IH Ntl) 249 >(int_trace_of_normal … N1) 250 cases (intensional_trace_of_trace ?? tl) 251 #cs' #tl' >associative_append % 252 ] qed. 253 254 255 definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝ 256 λcosts,start. 257 foldl ?? (λx. λev. 258 match ev with 259 [ IEVcall id ⇒ 260 let 〈current_stack,max_stack〉 ≝ x in 261 let new_stack ≝ current_stack + costs id in 262 〈new_stack, max new_stack max_stack〉 263  IEVret id ⇒ 264 let 〈current_stack,max_stack〉 ≝ x in 265 〈current_stack  costs id, max_stack〉 266  _ ⇒ x 267 ]) 〈start,start〉. 268 269 definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝ 270 λcosts, start, trace. \snd (measure_stack costs start trace). 48 271 49 272 lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f. … … 55 278  #h #t #IH' #acc #H @IH' @IH @H 56 279 ] qed. 57 280 (* 58 281 lemma max_stack_step : ∀C,a,m,a',m',tr,s. 59 282 measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 → … … 107 330 >IH % 108 331 ] qed. 109 332 *) 110 333 111 334 (* Check that the trace ends with the return from the starting function and one … … 140 363 pcs_labelled : ∀g. state … pcs_exec g → bool; 141 364 pcs_classify : ∀g. state … pcs_exec g → status_class; 142 pcs_ stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True  cl_return ⇒ True  _ ⇒ False ] → nat365 pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True  _ ⇒ False ] → ident 143 366 }. 144 367 145 definition pcs_to_cs : ∀C:preclassified_system. global … C → (ident → nat) →classified_system ≝146 λC,g ,stack_cost.147 mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_ stack C stack_cost?).368 definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝ 369 λC,g. 370 mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?). 148 371 149 372 (* FIXME: this definition is unreasonable because it presumes we can easily … … 158 381 λC,p,m,n,stack_cost,max_allowed_stack. ∃s0,prefix,s1,interesting,s2. 159 382 let g ≝ make_global … (pcs_exec … C) p in 160 let C' ≝ pcs_to_cs C g stack_costin383 let C' ≝ pcs_to_cs C g in 161 384 make_initial_state … p = OK ? s0 ∧ 162 385 exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧ … … 164 387 trace_is_label_to_return C' interesting ∧ 165 388 bool_to_Prop (will_return' C' interesting) ∧ 166 le (max_stack C' 0 (prefix@interesting)) max_allowed_stack.389 le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack. 167 390 168 391 (* TODO: probably ought to be elsewhere; use exec_steps instead 
src/common/SmallstepExec.ma
r2682 r2685 540 540 qed. 541 541 542 lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'. 543 exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 → 544 s = s1. 545 #n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC 546 lapply (exec_steps_length … EXEC) #E normalize in E; destruct 547 cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct 548 % 549 qed. 550 542 551 lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P. 543 552 after_n_steps n O I fx g s inv P → 544 ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'. 553 ∃trace,s'. 554 exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ 555 bool_to_Prop (all ? (λstr. inv (\fst str)) (tail … trace)) ∧ 556 P (gather_trace ? trace) s'. 545 557 #n elim n 546 [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} % {(refl ??)} @AFTER558 [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} % [ %{(refl ??)} %  @AFTER ] 547 559  #m #IH #O #I #fx #g #s #inv #P #AFTER 548 560 cases (after_1_of_n_steps … AFTER) 549 561 #tr1 * #s1 * * * #NF #STEP #INV #AFTER' 550 562 cases (IH … AFTER') 551 #tl * #s' * #STEPS#p563 #tl * #s' * * #STEPS #INV' #p 552 564 %{(〈s,tr1〉::tl)} %{s'} % 553 [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %  // ] 565 [ % 566 [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % 567  cases tl in STEPS INV INV' ⊢ %; [ //  * #sx #trx #t #STEPS #INV #INV' 568 <(exec_steps_first … STEPS) whd in ⊢ (?%); >INV // 569 >(exec_steps_length … STEPS) % 570 ] 571 ] 572  // ] 554 573 ] qed. 555 574 … … 588 607 destruct % 589 608 ] qed. 590 591 lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.592 exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →593 s = s1.594 #n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC595 lapply (exec_steps_length … EXEC) #E normalize in E; destruct596 cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct597 %598 qed.599 609 600 610 (* Show that it corresponds to split_trace … (exec_inf …).
Note: See TracChangeset
for help on using the changeset viewer.