include "RTLabs/syntax.ma".

(* We define a boolean cost label function on statements as well as a cost
   label extraction function because we can use it in hypotheses without naming
   the label. *)
   
definition is_cost_label : statement → bool ≝
λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].

definition cost_label_of : statement → option costlabel ≝
λs. match s with [ St_cost s _ ⇒ Some ? s | _ ⇒ None ? ].

(* We require that labels appear after branch instructions and at the start of
   functions.  The first is required for preciseness, the latter for soundness.
   We will make a separate requirement for there to be a finite number of steps
   between labels to catch loops for soundness (is this sufficient?). *)

definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
λf,s. match s return λs. labels_present ? s → Prop with
[ St_cond _ l1 l2 ⇒ λH.
    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
| St_jumptable _ ls ⇒ λH.
    (* I did have a dependent version of All here, but it's a pain. *)
    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
| _ ⇒ λ_. True
]. whd in H;
[ @(proj1 … H)
| @(proj2 … H)
] qed.

definition well_cost_labelled_fn : internal_function → Prop ≝
λf. (∀l. ∀H:present … (f_graph f) l.
         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
[ @lookup_lookup_present | cases (f_entry f) // ] qed.

(* Define a notion of sound labellings of RTLabs programs. *)

let rec successors (s : statement) : list label ≝
match s with
[ St_skip l ⇒ [l]
| St_cost _ l ⇒ [l]
| St_const _ _ _ l ⇒ [l]
| St_op1 _ _ _ _ _ l ⇒ [l]
| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
| St_load _ _ _ l ⇒ [l]
| St_store _ _ _ l ⇒ [l]
| St_call_id _ _ _ l ⇒ [l]
| St_call_ptr _ _ _ l ⇒ [l]
(*
| St_tailcall_id _ _ ⇒ [ ]
| St_tailcall_ptr _ _ ⇒ [ ]
*)
| St_cond _ l1 l2 ⇒ [l1; l2]
| St_jumptable _ ls ⇒ ls
| St_return ⇒ [ ]
].

definition steps_for_statement : statement → nat ≝
λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).

inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
| bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
| bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
with bound_on_steps_to_cost1 : label → nat → Prop ≝
| bostc_step : ∀l,n,H.
    let stmt ≝ lookup_present … g l H in
    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
          bound_on_steps_to_cost g l' n) →
    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).

definition soundly_labelled_fn : internal_function → Prop ≝
λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.

definition well_cost_labelled_program : RTLabs_program → Prop ≝
  λp. All ? (λx. match \snd x with [ Internal fn ⇒
    well_cost_labelled_fn fn ∧ soundly_labelled_fn fn
  | _ ⇒ True]) (prog_funct … p).