Changeset 2313 for src/RTLabs/Traces.ma
 Timestamp:
 Aug 31, 2012, 2:39:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.