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