include "RTLabs/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 : ∀g:graph statement. ∀s. labels_present g s → bool ≝
λg,s. match s return λs. labels_present g s → bool with
[ St_cond _ l1 l2 ⇒ λH.
    is_cost_label (lookup_present … g l1 ?) ∧
    is_cost_label (lookup_present … g l2 ?)
(*| 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 … g l H) = true) ls*)
| _ ⇒ λ_. true
]. whd in H;
[ @(proj1 … H)
| @(proj2 … H)
] qed.

definition well_cost_labelled_fn : internal_function → Prop ≝
λf. (∀l,PR. well_cost_labelled_statement (f_graph f) (lookup_present … (f_graph f) l PR) (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 ⇒ [ ]
].

(* To show that the labelling is sound we need a bound on the number of
   instructions in the current function until the next cost label. *)

inductive bound_on_instrs_to_cost (g:graph statement) : label → nat → Prop ≝
| boitc_step : ∀l,n,H.
    let stmt ≝ lookup_present … g l H in
    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
          bound_on_instrs_to_cost' g l' n) →
    bound_on_instrs_to_cost g l (S n)
with bound_on_instrs_to_cost' : label → nat → Prop ≝
| boitc_here : ∀l,n,H.
    is_cost_label (lookup_present … g l H) →
    bound_on_instrs_to_cost' g l n
| boitc_later : ∀l,n,H.
    ¬ is_cost_label (lookup_present … g l H) →
    bound_on_instrs_to_cost g l n →
    bound_on_instrs_to_cost' g l n.

definition soundly_labelled_fn : internal_function → Prop ≝
λf. ∀l. present … (f_graph f) l → ∃n. bound_on_instrs_to_cost (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).