Changeset 2313


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

RTLabs cost checker correct.

Location:
src/RTLabs
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2308 r2313  
    385385] qed.
    386386
    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 *)
     387include "RTLabs/CostMisc.ma".
     388
    401389lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM.
    402390  (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) →
    403391  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? →
    404392  ∃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)).
    407396#g #CL #term_check elim term_check
    408397[ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct
     
    417406  cases (try_remove ????)
    418407  [ #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      [ (* self-loop *) #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 …))
    423414        [ @PR
    424415        | >SUCC @eq_true_to_b @memb_hd
     
    437428      [ #BLL %{head} %{PRhead} % /2/
    438429      | * 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 ]
    440432        | #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % //
    441433          @(gl_step … BLL)
     
    443435          | >SUCC @eq_true_to_b @memb_hd
    444436          | cases checking_tail in PRECS INtl;
    445             [ #_ #INc <(memb_single … INc) in PR ⊢ %; //
     437            [ #_ *
    446438            | #h #t #H #_ @H % #E destruct
    447439            ]
     
    550542] qed.
    551543
     544lemma 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 
    552574(* TODO: move *)
    553575definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
     
    598620] qed.
    599621
    600 axiom check_sound_cost_fn_ok : ∀fn.
     622lemma check_sound_cost_fn_ok : ∀fn.
    601623  well_cost_labelled_fn fn →
    602624  bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
    603 (*
    604625#fn #WCL %
    605626[ whd in ⊢ (?% → %);
     
    624645    ]
    625646  ]
    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
    628666
    629667definition check_cost_program : RTLabs_program → bool ≝
  • 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.