Changeset 2313 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Aug 31, 2012, 2:39:49 PM (8 years ago)
Author:
campbell
Message:

RTLabs cost checker correct.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2307 r2313  
    22include "RTLabs/semantics.ma".
    33include "RTLabs/CostSpec.ma".
     4include "RTLabs/CostMisc.ma".
    45include "common/StructuredTraces.ma".
    56include "common/Executions.ma".
     
    24062407] qed.
    24072408
    2408 (* We aim to extract a loop without a cost label to contradict the reappearance
    2409    of a pc within a trace_any_label.  This data structure represents the tail
    2410    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 head
    2414 | 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 
    24202409(* We need to link the pcs, states of the semantics with the labels and graphs
    24212410   of the syntax. *)
     
    25822571] qed.
    25832572
    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. *)
    26712576
    26722577lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_state ge. ∀fl,tal.
     
    27062611    cases (bound_step1 … BOUND1 … SC1)
    27072612    #bound2 #BOUND2 @(absurd … BOUND2)
    2708     @(loop_soundness_contradiction … BLL … BLL)
     2613    @(loop_soundness_contradiction … BLL)
    27092614    [ @(next_ok f)
    27102615    | @SC1
Note: See TracChangeset for help on using the changeset viewer.