include "RTLabs/CostSpec.ma".
include "utilities/bool.ma".
include "utilities/listb.ma".
include "RTLabs/CostMisc.ma".

definition check_well_cost_fn : internal_function → bool ≝
λf.
  idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement (f_graph f) s (f_closed f l s PR)) ∧
  is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
cases (f_entry f) //
qed.

lemma check_well_cost_fn_ok : ∀fn. bool_to_Prop (check_well_cost_fn fn) ↔ well_cost_labelled_fn fn.
#fn %
[ #H cases (andb_Prop_true … H) #ST #EN
  % [ lapply (proj1 … (idmap_all_ok …) ST) // | @EN ]
| * #ST #EN @andb_Prop
  [ @(proj2 … (idmap_all_ok …)) #l #st #L
    cut (present ?? (f_graph fn) l) [ whd >L % #E destruct ] #PR
    lapply (ST l PR) generalize in ⊢ (?(???%) → ?);
    >(lookup_present_eq ????? L PR) //
  | @eq_true_to_b @EN
  ]
] qed.

include alias "utilities/deqsets.ma".

lemma successors_present : ∀g,st.
  labels_present g st →
  ∀l. l ∈ successors st →
  present ?? g l.
#g *
[ #l1 #PR #l2 #IN >(memb_single … IN) @PR
| #cs #l1 #PR #l2 #IN >(memb_single … IN) @PR
| #ty #r #c #l1 #PR #l2 #IN >(memb_single … IN) @PR
| #ty1 #ty2 #op #r1 #r2  #l1 #PR #l2 #IN >(memb_single … IN) @PR
| #ty1 #ty2 #ty3 #op #r1 #r2 #r3 #l1 #PR #l2 #IN >(memb_single … IN) @PR
| #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR
| #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR
| #id #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR
| #r #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR
| #r #l1 #l2 * #PR1 #PR2 #l3 whd in ⊢ (?% → ?); @eqb_elim [ // | #_ #IN >(memb_single … IN) // ]
| #_ #l *
] qed.

include alias "common/Identifiers.ma".

(* Check that from [checking] we reach a cost label without going through
   [checking_tail], which would form a loop in the CFG.  We also have a set of
   labels that we have still [to_check], and return an updated set of labels
   to check if the check for the current label is successful. *)
let rec check_label_bounded
  (g : graph statement)
  (CL : graph_closed g)
  (checking : label)
  (PR : present ?? g checking)
  (checking_tail : list label)
  (to_check : identifier_set LabelTag)
  (term_check : nat)
on term_check : gt term_check (id_map_size … to_check) → option (identifier_set LabelTag) ≝
let stop_now ≝ Some ? to_check in
match term_check return λx. ge x ? → ? with
[ O ⇒ λH.⊥
| S term_check' ⇒ λH.
  let st ≝ lookup_present … g checking PR in
  let succs ≝ successors st in
  match succs return λsc. (∀l.l∈sc → ?) → ? with
  [ nil ⇒ λ_. stop_now
  | cons h t ⇒
    match t with
    [ nil ⇒ λSC. (* single successor *)
      let PR' ≝ ? in
      let st' ≝ lookup_present … g h PR' in
      if is_cost_label st' then stop_now else
      match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with
      [ Some to_check' ⇒ λH'.
          check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
      | None ⇒ λ_.
          if h == checking ∨ h ∈ checking_tail then None ? else
            stop_now (* already checked successor *)
      ] (try_remove_some_card … to_check h)
    | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *)
    ]
  ] (successors_present g st (CL … checking … (lookup_lookup_present …)))
].
[ /2 by absurd/
| lapply (H' (\fst to_check') (\snd to_check') ?) [ cases to_check' // ]
  #E -PR' >E in H; #H' /2/
| @SC >memb_hd // 
] qed.

(* An inductive specification of the above function that's easier to work with. *)

inductive check_label_bounded_spec (g:graph statement) : label → list label → identifier_set LabelTag → identifier_set LabelTag → Prop ≝
| clbs_ret : ∀l,PR,tl,toch.
    successors (lookup_present … g l PR) = [ ] →
    check_label_bounded_spec g l tl toch toch
| clbs_checked : ∀l,PR,l',tl,toch. (* this case overlaps with clbs_cost *)
    successors (lookup_present … g l PR) = [l'] →
    ¬ l' ∈ toch →
    l' ≠ l →
    ¬ l' ∈ tl →
    check_label_bounded_spec g l tl toch toch
| clbs_cost : ∀l,PR,l',PR',tl,toch.
    successors (lookup_present … g l PR) = [l'] →
    is_cost_label (lookup_present … g l' PR') →
    check_label_bounded_spec g l tl toch toch
| clbs_step : ∀l,PR,l',PR',tl,toch,toch',toch''.
    successors (lookup_present … g l PR) = [l'] →
(*    l' ∈ toch → implied *)
    ¬ l' ∈ tl →
    ¬ is_cost_label (lookup_present … g l' PR') →
    try_remove … toch l' = Some ? 〈it,toch'〉 →
    check_label_bounded_spec g l' (l::tl) toch' toch'' →
    check_label_bounded_spec g l tl toch toch''
| clbs_branch : ∀l,PR,x,y,zs,tl,toch.  (* the other check will show that these are cost labels *)
    successors (lookup_present … g l PR) = x::y::zs →
    check_label_bounded_spec g l tl toch toch.


lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
  (∀l. l∈to_check → ¬ memb ? l (checking::checking_tail)) →
  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
  check_label_bounded_spec g checking checking_tail to_check to_check'.
#n elim n
[ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *)
| #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check' #REMOVING
  whd in ⊢ (??%? → ?);
  generalize in ⊢ (??(?%)? → ?);
  lapply (refl ? (successors (lookup_present … PR)))
  cases (successors (lookup_present … PR)) in ⊢ (???% → %);
  [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 //
  | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' @if_elim
           [ #CS #E destruct @(clbs_cost … SUCC) //
           | #NCS generalize in ⊢ (??(?%)? → ?);
             lapply (refl ? (try_remove … to_check h))
             cases (try_remove ????) in ⊢ (???% → %);
             [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim
               [ #H' #E destruct
               | #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC)
                 [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
                 | % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) *
                 | assumption
                 ]
               ]
             | * * #to_check'' #RM #H whd in ⊢ (??%? → ?);
               whd in ⊢ (??%? → ?); #H
               cases (try_remove_some ?????? RM) * #L1 #L2 #L3
               @(clbs_step … SUCC ? NCS RM)
               [ @notb_Prop @(not_to_not … (Prop_notb … (REMOVING h ?))) /2/
                 whd in ⊢ (?%); >L1 //
               | @(IH … H)
                 #l #IN'' @notb_Prop % whd in ⊢ (?% → ?); @if_elim
                 [ #E #_ whd in IN'':(?%); >(proj1 ?? (eqb_true …) E) in IN'';
                   >L2 *
                 | #NE lapply (REMOVING l ?)
                   [ whd in ⊢ (?%); cases (L3 l) [ #E destruct cases (Prop_notb … NE) #X @⊥ @X @eq_true_to_b @(proj2 ?? (eqb_true …)) %
                     | #L >L @IN''
                     ]
                   | cases (l∈checking::checking_tail) * *
                   ]
                 ]
               ]
             ]
           ]
         | #h2 #t #SUCCS whd in ⊢ (? → ??%? → ?); #PR' #E destruct
           @(clbs_branch … SUCCS)
         ]
  ]
] qed.

lemma check_label_bounded_c : ∀g,CL,checking,checking_tail,to_check,to_check'.
  check_label_bounded_spec g checking checking_tail to_check to_check' →
  ∀term_check,TERM,PR.
  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check'.
#g #CL #X1 #X2 #X3 #X4 #X elim X
[ #l #PR #tl #toch #SUCC
  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
  whd in ⊢ (??%?); %
| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl
  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
  whd in ⊢ (??%?); @if_elim [ // ] #NCS generalize in ⊢ (??(?%)?);
  cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ // | * * ] ]
  #L >(proj2 … (try_remove_empty …) L) #H2
  whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl)
  %
| #l #PR #l' #PR' #tl #toch #SUCC #CS
  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
  whd in ⊢ (??%?);  >CS whd in ⊢ (??%?); %
| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH
  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS))
  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2
  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN))
  whd in ⊢ (??%?); >(IH term_check' ??) %
| #l #PR #x #y #zs #tl #toch #SUCC
  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
  whd in ⊢ (??%?); %
] qed.

lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'.
  check_label_bounded_spec g checking checking_tail to_check to_check' →
  set_subset … to_check' to_check.
#g #lX #lX' #tX #tX' #S elim S //
#l #PR #l' #PR' #tl #toch #toch' #toch'' #SC #NI #CS #RM #H #IH
cases (try_remove_some … toch' RM) * #L1 #L2 #L3
#id #IN cases (L3 id)
[ #E destruct whd in ⊢ (?%); >L1 //
| #L4 whd in ⊢ (?%); >L4 @IH @IN
] qed.

lemma bound_on_instrs_to_cost_prime : ∀g,l,n.
  bound_on_instrs_to_cost g l n →
  bound_on_instrs_to_cost' g l n.
#g #l #n #H inversion H
#l' #n' #PR #H' #E1 #E2 #_ destruct
lapply (refl ? (is_cost_label (lookup_present … g l' PR)))
cases (is_cost_label ?) in ⊢ (???% → ?); #CS
[ @boitc_here [ @PR | @eq_true_to_b @CS ]
| @boitc_later [ @PR | @eq_false_to_notb @CS | @H ]
] qed.

lemma successors_inv : ∀st,x,y,zs.
  successors st = x::y::zs →
  ∃r,l1,l2. st = St_cond r l1 l2.
* normalize
#a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l destruct
/4/
qed.

include alias "utilities/deqsets.ma".

lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g.
  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
  ∀l,PR,x,y,zs. successors (lookup_present … g l PR) = x::y::zs →
  ∀l'. ∀IN : l' ∈ successors (lookup_present … g l PR).
  is_cost_label (lookup_present … g l' ?).
[2: @(successors_present … IN) @(CL l) @lookup_lookup_present ]
#g #CL #WCL #l #PR #x #y #zs #SUCCS
cases (successors_inv … SUCCS)
#r * #l1 * #l2 #E
#l' #IN generalize in ⊢ (?(?(?????%))); #OR' >E in IN;
lapply (WCL l PR) generalize in ⊢ (?(???%) → ?); >E in ⊢ (% → % → ?); #LP #WCst
cases (andb_Prop_true ?? WCst)
#H1 #H2
whd in ⊢ (?% → ?); @eqb_elim
[ 2: #_ #IN lapply (memb_single … IN) ]
#E destruct //
qed.

(* Show that when we remove labels from to_check we do actually find a bound
   (if it exists).  We need two extra facts: everything is "well" labelled,
   so that we know that branches are followed by labels and we don't need to
   follow them; and anything in the graph that isn't mentioned has already been
   successfully checked. *)

lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'.
  ∀CL:graph_closed g.
  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
  check_label_bounded_spec g checking checking_tail to_check to_check' →
  (∀l. l∈g → ¬l ∈ to_check → l≠checking → ¬l∈checking_tail → ∃n. bound_on_instrs_to_cost g l n) →
  ∀l. l = checking ∨ bool_to_Prop (l∈to_check) →
  bool_to_Prop (l∈to_check') ∨ ∃n. bound_on_instrs_to_cost g l n.
#g #X1 #X2 #X3 #X4 #CL #WCL #X elim X
[ #l #PR #tl #toch #SUCC #INV #l' *
  [ #E destruct %2 %{1} % [ @PR | >SUCC #l' * ]
  | #IN %1 @IN
  ]
| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl #INV #l'' *
  [ #E destruct %2
    cases (INV l' ????)
    [ #n #B
      %{(S n)} % [ @PR | >SUCC #l'' * [2: *] #E destruct /2/ ]
    | @present_member @(successors_present … (CL l ? (lookup_lookup_present … PR)))
      >SUCC @eq_true_to_b @memb_hd
    | assumption
    | assumption
    | assumption
    ]
  | #IN %1 assumption
  ]
| #l #PR #l' #PR' #tl #toch #SUCC #CS #INV #l'' *
  [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ]
  | /2/
  ]
| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN_tl #NCS #RM #H #IH #INV #l'' *
  [ #E destruct %2 cases (IH ? l' ?)
    [ #IN @⊥ lapply (check_label_bounded_subset … H l' IN) #IN'
      cases (try_remove_some ?????? RM) * #_ #L #_ whd in IN':(?%);
      cases (lookup ????) in IN' L; [ * | * #_ #E destruct ]
    | * #n #B %{(S n)} % [ // | #l'' >SUCC * [2: *] #E destruct /2/ ]
    | #l'' #INg #INch' #NEQ #NIN_ltl @(INV l'' INg ???)
      [ @notb_Prop % #INch @(absurd ?? (Prop_notb … INch'))
        cases (try_remove_some ?????? RM) * #_ #_ #L
        cases (L l'') [ #E destruct cases NEQ #X cases (X (refl ??)) ]
        #L' whd in ⊢ (?%); <L' @INch
      | % #E destruct cases (Prop_notb … NIN_ltl) #X @X @eq_true_to_b @memb_hd
      | @notb_Prop @(not_to_not … (Prop_notb … NIN_ltl)) #IN @eq_true_to_b @memb_cons @IN
      ]
    | %1 %
    ]
  | #IN @(IH ? l'' ?)
    [ #l''' #INg #NINch' #NEQ #NINtl @INV
      [ assumption
      | @notb_Prop @(not_to_not … (Prop_notb … NINch'))
        cases (try_remove_some ?????? RM) * #L1 #L2 #L3
        cases (L3 l''')
        [ #E destruct @⊥ cases NEQ /2/
        | #L whd in ⊢ (?% → ?%); >L //
        ]
      | % #E destruct cases (Prop_notb … NINtl) #X @X @eq_true_to_b @memb_hd
      | @notb_Prop @(not_to_not … (Prop_notb … NINtl)) #IN @eq_true_to_b @memb_cons @IN
      ]
    | cases (try_remove_some ?????? RM) * #L1 #L2 #L3
      cases (L3 l'') [ #E destruct %1 % | #L %2 whd in ⊢ (?%); <L @IN ]
    ]
  ]
| #l #PR #x #y #zs #tl #toch #SUCCS #INV #l' *
  [ #E destruct %2 %{1} % [ // ]
    #l' #EX @boitc_here
    [ @(successors_present … (CL l ? (lookup_lookup_present … PR)))
      @Exists_memb @EX
    | @(after_branch_are_cost_labels … WCL … SUCCS)
    ]
  | /2/
  ]
] qed.


(* When we reject a label it is because we found a loop without a cost label
   when we followed its successors.  We need the invariant that only the
   initial label can be a cost label, and have two cases in the result: either
   we found the entire loop and return that, or we haven't come back out of the
   recursive calls to find the head again, so return part of the loop. *)

lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM.
  (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) →
  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? →
  ∃head,PR'. bool_to_Prop (¬ is_cost_label (lookup_present … g head PR')) ∧
  ((∃l. Exists ? (λl'.l'=l) (successors (lookup_present … g head PR')) ∧
       bad_label_list g head l) ∨
   (bool_to_Prop (head ∈ checking_tail) ∧ bad_label_list g head checking)).
#g #CL #term_check elim term_check
[ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct
| #term_check' #IH
  #checking #PR #checking_tail #to_check #TERM #PRECS
  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); lapply (refl ? (successors (lookup_present … PR)))
  cases (successors ?) in ⊢ (???% → %);
  [ #H #H' whd in ⊢ (??%? → ?); #E destruct ]
  #h * [2: #y #zs #H #H' whd in ⊢ (??%? → ?); #E destruct ]
  #SUCC #PR' whd in ⊢ (??%? → ?); @if_elim
  [ #CS #E destruct ] #NCS generalize in ⊢ (??(?%)? → ?);
  cases (try_remove ????)
  [ #H whd in ⊢ (??%? → ?); @if_elim
    (* base case - we've found the head of the list *)
    [ #IN #_ cases (orb_Prop_true … IN)
      [ (* self-loop *) #E >(proj1 ?? (eqb_true …) E) in SUCC PR' NCS; #SUCC #PR' #NCS %{checking} %{PR}
        %{NCS} %1 %{checking} % [ >SUCC % % | // ]
      | #IN' %{h} % [ @PR' @eq_true_to_b @memb_hd ] %{NCS} %2 %{IN'}
        @(gl_step … (gl_end …))
        [ @PR
        | >SUCC @eq_true_to_b @memb_hd
        | cases (orb_Prop_true … IN)
          [ #E <(proj1 ?? (eqb_true …) E) in PR ⊢ %; //
          | cases checking_tail in PRECS ⊢ %;
            [ #_ * | #h' #t #H #_ @H % #E destruct ]
          ]
        ]
      ]
    | #_ #E destruct
    ]
  | * * #to_check' #H1 whd in ⊢ (??%? → ?);
    #CHECK' cases (IH … CHECK')
    [ #head * #PRhead * #NCShead *
      [ #BLL %{head} %{PRhead} % /2/
      | * whd in ⊢ (?% → ?); @if_elim
        [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead NCShead ⊢ %; #PRh #NCSh #BLL %{checking} %{PRh} %{NCSh}
          %1 %{h} >SUCC % [ % % | @BLL ]
        | #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % //
          @(gl_step … BLL)
          [ @PR
          | >SUCC @eq_true_to_b @memb_hd
          | cases checking_tail in PRECS INtl;
            [ #_ *
            | #h #t #H #_ @H % #E destruct
            ]
          ]
        ]
      ]
    | #_ //
    ]
  ]
] qed.
      

(* Now keep checking as long as there's some instruction we haven't checked. *)

let rec check_graph_bounded
  (g : graph statement)
  (CL : graph_closed g)
  (to_check : identifier_set LabelTag)
  (SUB : set_subset … to_check g)
  (start : label)
  (PR : present ?? g start)
  (REMOVED : notb (member ?? to_check start))
  (SMALLER : gt (id_map_size … g) (id_map_size … to_check))
  (term_check : nat)
on term_check : gt term_check (id_map_size … to_check) → bool ≝ 
match term_check return λx. ge x ? → bool with
[ O ⇒ λH.⊥
| S term_check' ⇒ λH.
  let TERM' ≝ ? in
  match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with
  [ None ⇒ λ_. false
  | Some to_check' ⇒ λH'.
    match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with
    [ None ⇒ λ_.λ_.λ_. true
    | Some l_to_check'' ⇒ λL,SUB',C.
        check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ??? term_check' ?
    ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check')
  ] (refl ??)
].
[ 2,3,4,5,6: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB'
  lapply (check_label_bounded_subset … (check_label_bounded_s … H'))
  [ 1,3,5,7,9: #l' #IN @notb_Prop % #IS >(memb_single … IS) in IN; #IN'
    @(absurd … IN' (Prop_notb … REMOVED)) ]
   #SUB''
]
[ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN
| @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L //
| cases (L … (refl ??)) * #L1 #L2 #L3 whd in ⊢ (?(?%)); >L2 //
| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
| /2/
| @SMALLER
] qed.

lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
  check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = true →
  (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) →
  ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n.
#g #CL #term_check elim term_check
[ #to_check #SUB #start #PR #REMOVED #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
| #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM #WCL
  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
  [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ]
  generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
  lapply (choose_empty … to_check')
  cases (choose LabelTag unit to_check')
  [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN
    cases (true_or_false_Prop (l∈to_check ∨ l == start))
    [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
      [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; *
      | //
      | //
      | @WCL
      | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
        >(memb_single … IN') in IN; //
      | #l' #IN_g #NIN_to_check #NEQ #_ @H //
      | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
      ]
    | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
    ]
 | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
   #CHECK #H @(IH … CHECK)
   [ @WCL
   | #l #INg #NIN'' #NEQ
     cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN''))
                          cases (H4 … (refl ??)) * #L1 #L2 #L3
                          cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ]
     #NIN'
      cases (true_or_false_Prop (l∈to_check ∨ l == start))
      [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
        [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN'))
        | //
        | //
        | @WCL
        | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
          >(memb_single … IN') in IN; //
        | #l' #IN_g #NIN_to_check #NEQ #_ @H //
        | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
        ]
      | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
      ]
   ]
 ]
] qed.

(* The check_label_bounded_bad result gives us the loop, so we can use the
   loop_soundness_contradiction result to show that there's no bound for the
   head of the loop. *)

lemma check_graph_bounded_bad : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
  check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = false →
  ∃l. present ?? g l ∧ ∀n. ¬ bound_on_instrs_to_cost g l n.
#g #CL #term_check elim term_check
[ #a #b #c #d #e #f #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
| #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM
  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
  [ #CHECK_LABEL whd in ⊢ (??%? → ?); #_
    cases (check_label_bounded_bad … CHECK_LABEL)
    [ #head * #PR_head * #NCS_head *
      [ * #next * #NEXT #BLL
        %{head} %{PR_head} #n % #BOUND
        cases (bound_step1 … BOUND … NEXT) #m #BOUND'
        @(absurd ? BOUND' (loop_soundness_contradiction … NEXT NCS_head BLL m))
      | * *
      ]
    | * #H cases (H (refl ??))
    ]
  | #to_check' #CHECK_LABEL whd in ⊢ (??%? → ?);
    generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
    cases (choose LabelTag unit to_check')
    [ #H1 #H2 #H3 whd in ⊢ (??%? → ?); #E destruct
    | * * #next * #to_check'' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
      @IH
    ]
  ]
] qed.

 
definition check_sound_cost_fn : internal_function → bool ≝
λfn.
  match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with
  [ None ⇒ λEMP. ⊥
  | Some to_check ⇒ λ_.λCARD,L.
              check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ??? (|f_graph fn|) ?
  ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn)))
    (try_remove_some_card ????)
    (try_remove_some ????).
[ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H
  @PR' @H %
| cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN
  cases (L3 id)
  [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/
  | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) *
    whd in match (present ????); whd in match (present ? unit ??);
    lapply (member_present … IN) whd in match (present ? unit ??); <E
    cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/
  ]
| cases (f_entry fn) //
| cases to_check in L ⊢ %; * #to_check0 #L cases (L … (refl ??)) * #L1 #L2 #L3
  whd in ⊢ (?(?%)); >L2 //
| 5,6: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) //
] qed.

lemma check_sound_cost_fn_ok : ∀fn.
  well_cost_labelled_fn fn →
  bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
#fn #WCL %
[ whd in ⊢ (?% → %);
  generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?);
  cases (try_remove ????)
  [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
    lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
    >(E (refl ??)) * /3/
  | * * #to_check #H1 #H2 #H3
    whd in ⊢ (?% → ?); #CHECK
    #l #PR @(check_graph_bounded_ok … CHECK)
    [ #l' #PR' cases WCL //
    | #l' #IN #NIN #NEQ @⊥
      cases (H1 … (refl ??)) * #L1 #L2 #L3
      @(absurd ?? (Prop_notb … NIN))
      cases (L3 l')
      [ #E >E in NEQ; * #H cases (H (refl ??))
      | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …))
        @member_present @IN
      ]
    | /2/
    ]
  ]
| whd in ⊢ (% → %); #SOUND
  lapply (refl ? (check_sound_cost_fn fn))
  cases (check_sound_cost_fn fn) in ⊢ (???% → %);
  [ //
  | whd in ⊢ (??%? → %);
    generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
    cases (try_remove ????)
    [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
      lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
      >(E (refl ??)) * /3/
    | * * #to_check #H1 #H2 #H3
      whd in ⊢ (??%? → ?); #CHECK
      lapply (check_graph_bounded_bad … CHECK) -CHECK -H1 -H2 -H3
      * #l * #PR #NOT cases (SOUND l PR) #n #B
      @(absurd ? B) @NOT
    ]
  ]
] qed.


definition check_cost_program : RTLabs_program → bool ≝
λp. all ? (λfn. match \snd fn with
                 [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn
                 | External _ ⇒ true
                 ]) (prog_funct … p).

theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p.
#p whd in ⊢ (?(?%)%); %
[ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp
  * #id * #fd
  [ #H cases (andb_Prop_true … H) #W #S
    lapply (proj1 … (check_well_cost_fn_ok …) W) #W'
    %
    [ //
    | @(proj1 … (check_sound_cost_fn_ok …)) //
    ]
  | //
  ]
| #H @(proj2 … (all_All …)) @(All_mp … H)
  * #id * #fd
  [ * #W #S
    lapply ((proj2 … (check_well_cost_fn_ok …)) W)
    lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/
  | //
  ]
] qed.