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/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 ≝
Note: See TracChangeset for help on using the changeset viewer.