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).