Changeset 1586
 Timestamp:
 Dec 5, 2011, 1:11:50 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1583 r1586 20 20 ]. 21 21 22 definition is_cost_label : statement → bool ≝ 23 λs. match s with [ St_cost _ _ ⇒ true  _ ⇒ false ]. 24 22 25 definition RTLabs_cost : state → bool ≝ 23 26 λs. match s with 24 27 [ State f fs m ⇒ 25 match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with 26 [ St_cost c l ⇒ true 27  _ ⇒ false 28 ] 28 is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) 29 29  _ ⇒ false 30 30 ]. … … 301 301 between labels to catch loops for soundness (is this sufficient?). *) 302 302 303 definition is_cost_label : statement → Prop ≝304 λs. match s with [ St_cost _ _ ⇒ True  _ ⇒ False ].305 306 let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝307 match l return λl.All A P l → Prop with308 [ nil ⇒ λ_. True309  cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H)310 ] H.311 312 303 definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝ 313 304 λf,s. match s return λs. labels_present ? s → Prop with 314 305 [ St_cond _ l1 l2 ⇒ λH. 315 is_cost_label (lookup_present … (f_graph f) l1 ?) ∧316 is_cost_label (lookup_present … (f_graph f) l2 ?) 306 is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧ 307 is_cost_label (lookup_present … (f_graph f) l2 ?) = true 317 308  St_jumptable _ ls ⇒ λH. 318 All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H 309 (* I did have a dependent version of All here, but it's a pain. *) 310 All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls 319 311  _ ⇒ λ_. True 320 312 ]. whd in H; … … 324 316 325 317 definition well_cost_labelled_fn : internal_function → Prop ≝ 326 λf. (∀l ,s. ∀H:lookup … (f_graph f) l = Some ? s.327 well_cost_labelled_statement f s (f_closed f…)) ∧328 is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) .329 [ 2: @H  skip cases (f_entry f) // ] qed.318 λf. (∀l. ∀H:present … (f_graph f) l. 319 well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧ 320 is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true. 321 [ @lookup_lookup_present  cases (f_entry f) // ] qed. 330 322 331 323 (* We need to ensure that any code we come across is wellcostlabelled. We may … … 356 348  #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % // 357 349 ] qed. 350 351 lemma rtlabs_jump_inv : ∀s. 352 RTLabs_classify s = cl_jump → 353 ∃f,fs,m. s = State f fs m ∧ 354 let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in 355 (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls). 356 * 357 [ #f #fs #m #E 358 %{f} %{fs} %{m} % 359 [ @refl 360  whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %; 361 try (normalize try #A try #B try #C try #D try #F try #G try #H destruct) 362 [ %1 %{A} %{B} %{C} @refl 363  %2 %{A} %{B} @refl 364 ] 365 ] 366  normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct 367  normalize #H8 #H9 #H10 #H11 #H12 destruct 368 ] qed. 369 370 lemma well_cost_labelled_jump : ∀ge,s,tr,s'. 371 eval_statement ge s = Value ??? 〈tr,s'〉 → 372 well_cost_labelled_state s → 373 RTLabs_classify s = cl_jump → 374 RTLabs_cost s' = true. 375 #ge #s #tr #s' #EV #H #CL 376 cases (rtlabs_jump_inv s CL) 377 #fr * #fs * #m * #Es * 378 [ * #r * #l1 * #l2 #Estmt 379 >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs 380 >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 381 >Estmt #LP whd in ⊢ (??%? → ?); 382 (* replace with lemma on successors? *) 383 @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct 384 lapply (Hbody (next fr) (next_ok fr)) 385 generalize in ⊢ (???% → ?); 386 >Estmt #LP' 387 whd in ⊢ (% → ?); 388 * #H1 #H2 [ @H1  @H2 ] 389  * #r * #ls #Estmt 390 >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs 391 >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 392 >Estmt #LP whd in ⊢ (??%? → ?); 393 (* replace with lemma on successors? *) 394 @bindIO_value #a cases a [  #sz #i  #f  #r  #ptr ] #Ea whd in ⊢ (??%? → ?); 395 [ 2: (* later *) 396  *: #E destruct 397 ] 398 lapply (Hbody (next fr) (next_ok fr)) 399 generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP 400 generalize in ⊢ (??(?%)? → ?); 401 cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)? → ?); 402 [ #E1 #E2 whd in E2:(??%?); destruct 403  #l' #E1 #E2 whd in E2:(??%?); destruct 404 cases (All_nth ???? CP ? E1) 405 #H1 #H2 @H2 406 ] 407 ] qed. 408 358 409 359 410 (* Don't need to know that labels break loops because we have termination. *) … … 437 488 ] 438 489 ] (refl ??) 439  cl_jump ⇒ λCL. ? 490  cl_jump ⇒ λCL. 491 mk_make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends start s') next (pred n) trace' ?? (dp ?? doesnt_end_with_ret (tal_base_not_return (RTLabs_status ge) start next ???)) 440 492  cl_call ⇒ λCL. ? 441 493  cl_return ⇒ λCL. ? … … 456 508  457 509  458  510  @(nth_is_return_notfn … TERMINATES) %2 @CL 511  @(well_cost_labelled_state_step … EV) // 512  %{tr} @EV 513  % whd in ⊢ (% → ?); >CL #E destruct 514  @(well_cost_labelled_jump … EV) // 459 515  460 516  @(nth_is_return_notfn … TERMINATES) %1 @CL 461 517  @(well_cost_labelled_state_step … EV) // 462 518  %{tr} @EV 463  519  % whd in ⊢ (% → ?); >CL #E destruct 464 520  @CS 465 521  %{tr} @EV
Note: See TracChangeset
for help on using the changeset viewer.