Changeset 2313
 Timestamp:
 Aug 31, 2012, 2:39:49 PM (7 years ago)
 Location:
 src/RTLabs
 Files:

 1 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostCheck.ma
r2308 r2313 385 385 ] qed. 386 386 387 (* TODO: share with Traces.ma. *) 388 inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝ 389  gl_end : bad_label_list g head head 390  gl_step : ∀l1,l2,H. 391 l2 ∈ successors (lookup_present … g l1 H) → 392 ¬ is_cost_label (lookup_present … g l1 H) → 393 bad_label_list g head l2 → 394 bad_label_list g head l1. 395 (* 396 inductive checked_label_costs (g:graph statement) : list label → label → Prop ≝ 397  clc_start : ∀l. checked_label_costs g [ ] l 398  clc_two : ∀l,H,l'. ¬ is_cost_label (lookup_present … g l H) → checked_label_costs g [l'] l 399  clc_many : ∀h,t,l,H. ¬ is_cost_label (lookup_present … g h H) → checked_label_costs g t l → checked_label_costs g (h::t) l. 400 *) 387 include "RTLabs/CostMisc.ma". 388 401 389 lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM. 402 390 (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) → 403 391 check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? → 404 392 ∃head,PR'. bool_to_Prop (¬ is_cost_label (lookup_present … g head PR')) ∧ 405 (bad_label_list g head head ∨ 406 (bool_to_Prop (head ∈ checking::checking_tail) ∧ bad_label_list g head checking)). 393 ((∃l. Exists ? (λl'.l'=l) (successors (lookup_present … g head PR')) ∧ 394 bad_label_list g head l) ∨ 395 (bool_to_Prop (head ∈ checking_tail) ∧ bad_label_list g head checking)). 407 396 #g #CL #term_check elim term_check 408 397 [ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct … … 417 406 cases (try_remove ????) 418 407 [ #H whd in ⊢ (??%? → ?); @if_elim 419 (* base case  we've found the head of the list *) 420 [ #IN #_ %{h} % [ @PR' @eq_true_to_b @memb_hd ] % [ @NCS ] %2 % 421 [ cases (orb_Prop_true … IN) /2/ 422  @(gl_step … (gl_end …)) 408 (* base case  we've found the head of the list *) 409 [ #IN #_ cases (orb_Prop_true … IN) 410 [ (* selfloop *) #E >(proj1 ?? (eqb_true …) E) in SUCC PR' NCS; #SUCC #PR' #NCS %{checking} %{PR} 411 %{NCS} %1 %{checking} % [ >SUCC % %  // ] 412  #IN' %{h} % [ @PR' @eq_true_to_b @memb_hd ] %{NCS} %2 %{IN'} 413 @(gl_step … (gl_end …)) 423 414 [ @PR 424 415  >SUCC @eq_true_to_b @memb_hd … … 437 428 [ #BLL %{head} %{PRhead} % /2/ 438 429  * whd in ⊢ (?% → ?); @if_elim 439 [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead ⊢ %; #PRh #BLL %{h} %{PRh} %{NCS} %1 @BLL 430 [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead NCShead ⊢ %; #PRh #NCSh #BLL %{checking} %{PRh} %{NCSh} 431 %1 %{h} >SUCC % [ % %  @BLL ] 440 432  #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % // 441 433 @(gl_step … BLL) … … 443 435  >SUCC @eq_true_to_b @memb_hd 444 436  cases checking_tail in PRECS INtl; 445 [ #_ #INc <(memb_single … INc) in PR ⊢ %; //437 [ #_ * 446 438  #h #t #H #_ @H % #E destruct 447 439 ] … … 550 542 ] qed. 551 543 544 lemma check_graph_bounded_bad : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM. 545 check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = false → 546 ∃l. present ?? g l ∧ ∀n. ¬ bound_on_instrs_to_cost g l n. 547 #g #CL #term_check elim term_check 548 [ #a #b #c #d #e #f #TERM @⊥ inversion TERM #A try #B try #C try #D destruct 549  #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM 550 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 551 cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)? → ?); 552 [ #CHECK_LABEL whd in ⊢ (??%? → ?); #_ 553 cases (check_label_bounded_bad … CHECK_LABEL) 554 [ #head * #PR_head * #NCS_head * 555 [ * #next * #NEXT #BLL 556 %{head} %{PR_head} #n % #BOUND 557 cases (bound_step1 … BOUND … NEXT) #m #BOUND' 558 @(absurd ? BOUND' (loop_soundness_contradiction … NEXT NCS_head BLL m)) 559  * * 560 ] 561  * #H cases (H (refl ??)) 562 ] 563  #to_check' #CHECK_LABEL whd in ⊢ (??%? → ?); 564 generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?); 565 cases (choose LabelTag unit to_check') 566 [ #H1 #H2 #H3 whd in ⊢ (??%? → ?); #E destruct 567  * * #next * #to_check'' #H2 #H3 #H4 whd in ⊢ (??%? → ?); 568 @IH 569 ] 570 ] 571 ] qed. 572 573 552 574 (* TODO: move *) 553 575 definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝ … … 598 620 ] qed. 599 621 600 axiomcheck_sound_cost_fn_ok : ∀fn.622 lemma check_sound_cost_fn_ok : ∀fn. 601 623 well_cost_labelled_fn fn → 602 624 bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn. 603 (*604 625 #fn #WCL % 605 626 [ whd in ⊢ (?% → %); … … 624 645 ] 625 646 ] 626  TODO 627 *) 647  whd in ⊢ (% → %); #SOUND 648 lapply (refl ? (check_sound_cost_fn fn)) 649 cases (check_sound_cost_fn fn) in ⊢ (???% → %); 650 [ // 651  whd in ⊢ (??%? → %); 652 generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?); 653 cases (try_remove ????) 654 [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E 655 lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?); 656 >(E (refl ??)) * /3/ 657  * * #to_check #H1 #H2 #H3 658 whd in ⊢ (??%? → ?); #CHECK 659 lapply (check_graph_bounded_bad … CHECK) CHECK H1 H2 H3 660 * #l * #PR #NOT cases (SOUND l PR) #n #B 661 @(absurd ? B) @NOT 662 ] 663 ] 664 ] qed. 665 628 666 629 667 definition check_cost_program : RTLabs_program → bool ≝ 
src/RTLabs/Traces.ma
r2307 r2313 2 2 include "RTLabs/semantics.ma". 3 3 include "RTLabs/CostSpec.ma". 4 include "RTLabs/CostMisc.ma". 4 5 include "common/StructuredTraces.ma". 5 6 include "common/Executions.ma". … … 2406 2407 ] qed. 2407 2408 2408 (* We aim to extract a loop without a cost label to contradict the reappearance2409 of a pc within a trace_any_label. This data structure represents the tail2410 of a loop purely in terms of the RTLabs function body graph. *)2411 2412 inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝2413  gl_end : bad_label_list g head head2414  gl_step : ∀l1,l2,H.2415 l2 ∈ successors (lookup_present … g l1 H) →2416 ¬ is_cost_label (lookup_present … g l1 H) →2417 bad_label_list g head l2 →2418 bad_label_list g head l1.2419 2420 2409 (* We need to link the pcs, states of the semantics with the labels and graphs 2421 2410 of the syntax. *) … … 2582 2571 ] qed. 2583 2572 2584 (* Some inversion lemmas on the bounds. 2585 2586 For the first step just get a bound after the step; we don't care what it is, 2587 just that it exists. *) 2588 2589 lemma bound_step1 : ∀g,l1,n. 2590 bound_on_instrs_to_cost g l1 n → 2591 ∀l2,H. Exists ? (λl.l = l2) (successors (lookup_present … g l1 H)) → 2592 ∃m. bound_on_instrs_to_cost' g l2 m. 2593 #g #l1X #nX * #l #n #H #EX #l2 #H' #EX' %{n} @EX @EX' 2594 qed. 2595 2596 lemma bound_zero1 : ∀g,l. 2597 ¬ bound_on_instrs_to_cost g l 0. 2598 #g #l % #B lapply (refl ? O) cases B in ⊢ (???% → ?); 2599 #l' #n #H #_ whd in ⊢ (???% → ?); #E destruct 2600 qed. 2601 2602 lemma bound_zero : ∀g,l. 2603 bound_on_instrs_to_cost' g l 0 → 2604 ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)). 2605 #g #l #B 2606 @(match B return λl,n,B. n = O → ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)) with 2607 [ boitc_here l n H CS ⇒ ? 2608  boitc_later _ _ _ _ B' ⇒ ? 2609 ] (refl ? O)) 2610 [ #E >E %{H} @CS 2611  #E >E in B'; #B' @⊥ @(absurd … B' (bound_zero1 …)) 2612 ] qed. 2613 2614 lemma bound_step : ∀g,l,n. 2615 bound_on_instrs_to_cost' g l (S n) → 2616 ∃H. (bool_to_Prop (is_cost_label (lookup_present … g l H)) ∨ 2617 (let stmt ≝ lookup_present … g l H in 2618 ∀l'. Exists label (λl0. l0 = l') (successors stmt) → 2619 bound_on_instrs_to_cost' g l' n)). 2620 #g #lX #n #B lapply (refl ? (S n)) cases B in ⊢ (???% → %); 2621 [ #l #n #H #CS #E %{H} %1 @CS 2622  #l #m #H #CS * 2623 #l' #n' #H' #EX #E destruct %{H'} %2 2624 #l'' #EX' @EX @EX' 2625 ] qed. 2626 2627 lemma bad_label_list_no_cost : ∀g,l1,l2. 2628 bad_label_list g l1 l2 → 2629 ∀H1. ¬ is_cost_label (lookup_present … g l1 H1) → 2630 ∃H2. bool_to_Prop (¬ is_cost_label (lookup_present … g l2 H2)). 2631 #g #l1 #l2 * /2/ 2632 qed. 2633 2634 (* Show that a bad_label_list is incompatible with a bound on the number of 2635 instructions to a cost label, by induction on the bound and the invariant 2636 that none of the instructions involved are a cost label. *) 2637 2638 lemma loop_soundness_contradiction : ∀g,l1,l2,H1. 2639 Exists ? (λl.l = l2) (successors (lookup_present … g l1 H1)) → 2640 ¬ is_cost_label (lookup_present … g l1 H1) → 2641 bad_label_list g l1 l2 → 2642 ∀n,l'. 2643 bad_label_list g l1 l' → 2644 ¬ bound_on_instrs_to_cost' g l' n. 2645 #g #l1 #l2 #H1 #SC1 #NCS1 #BLL2 2646 #n elim n 2647 [ #l #BLL % #BOUND 2648 cases (bound_zero … BOUND) #H' #ICS 2649 cases (bad_label_list_no_cost … BLL H1 NCS1) #H'' 2650 >ICS * 2651  #m #IH #l #BLL % #BOUND 2652 cases (bound_step … BOUND) #H' * 2653 [ #ICS cases (bad_label_list_no_cost … BLL H1 NCS1) #H'' >ICS * 2654  #EX_BOUND inversion BLL 2655 [ #E1 #E2 destruct 2656 lapply (IH l2 BLL2) 2657 lapply (EX_BOUND … SC1) 2658 @absurd 2659  #l3 #l4 #H3 #SC2 #NCS3 #BLL4 #_ #E1 #E2 destruct 2660 lapply (IH l4 BLL4) 2661 cut (Exists ? (λl.l=l4) (successors (lookup_present … H3))) 2662 [ cases (memb_exists … SC2) #left * #right #E >E @Exists_mid % ] 2663 #SC2' lapply (EX_BOUND … SC2') 2664 @absurd 2665 ] 2666 ] 2667 ] qed. 2668 2669 (* Combine the above results to show that the pc of a normal instruction 2670 execution state can't be repeated within a trace_any_label. *) 2573 (* Combine the above result with the result on bad loops in CostMisc.ma to show 2574 that the pc of a normal instruction execution state can't be repeated within 2575 a trace_any_label. *) 2671 2576 2672 2577 lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_state ge. ∀fl,tal. … … 2706 2611 cases (bound_step1 … BOUND1 … SC1) 2707 2612 #bound2 #BOUND2 @(absurd … BOUND2) 2708 @(loop_soundness_contradiction … BLL … BLL)2613 @(loop_soundness_contradiction … BLL) 2709 2614 [ @(next_ok f) 2710 2615  @SC1
Note: See TracChangeset
for help on using the changeset viewer.