source: src/RTLabs/CostSpec.ma @ 2303

Last change on this file since 2303 was 2303, checked in by campbell, 7 years ago

Some preliminary checking of cost labelling properties in RTLabs.

File size: 3.3 KB
Line 
1
2include "RTLabs/syntax.ma".
3
4(* We define a boolean cost label function on statements as well as a cost
5   label extraction function because we can use it in hypotheses without naming
6   the label. *)
7   
8definition is_cost_label : statement → bool ≝
9λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
10
11definition cost_label_of : statement → option costlabel ≝
12λs. match s with [ St_cost s _ ⇒ Some ? s | _ ⇒ None ? ].
13
14(* We require that labels appear after branch instructions and at the start of
15   functions.  The first is required for preciseness, the latter for soundness.
16   We will make a separate requirement for there to be a finite number of steps
17   between labels to catch loops for soundness (is this sufficient?). *)
18
19definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → bool ≝
20λf,s. match s return λs. labels_present ? s → bool with
21[ St_cond _ l1 l2 ⇒ λH.
22    is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
23    is_cost_label (lookup_present … (f_graph f) l2 ?)
24(*| St_jumptable _ ls ⇒ λH.
25    (* I did have a dependent version of All here, but it's a pain. *)
26    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls*)
27| _ ⇒ λ_. true
28]. whd in H;
29[ @(proj1 … H)
30| @(proj2 … H)
31] qed.
32
33definition well_cost_labelled_fn : internal_function → Prop ≝
34λf. (∀l. ∀H:present … (f_graph f) l.
35         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
36    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
37[ @lookup_lookup_present | cases (f_entry f) // ] qed.
38
39(* Define a notion of sound labellings of RTLabs programs. *)
40
41let rec successors (s : statement) : list label ≝
42match s with
43[ St_skip l ⇒ [l]
44| St_cost _ l ⇒ [l]
45| St_const _ _ _ l ⇒ [l]
46| St_op1 _ _ _ _ _ l ⇒ [l]
47| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
48| St_load _ _ _ l ⇒ [l]
49| St_store _ _ _ l ⇒ [l]
50| St_call_id _ _ _ l ⇒ [l]
51| St_call_ptr _ _ _ l ⇒ [l]
52(*
53| St_tailcall_id _ _ ⇒ [ ]
54| St_tailcall_ptr _ _ ⇒ [ ]
55*)
56| St_cond _ l1 l2 ⇒ [l1; l2]
57(*| St_jumptable _ ls ⇒ ls*)
58| St_return ⇒ [ ]
59].
60
61(* To show that the labelling is sound we need a bound on the number of
62   instructions in the current function until the next cost label. *)
63
64inductive bound_on_instrs_to_cost (g:graph statement) : label → nat → Prop ≝
65| boitc_step : ∀l,n,H.
66    let stmt ≝ lookup_present … g l H in
67    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
68          bound_on_instrs_to_cost' g l' n) →
69    bound_on_instrs_to_cost g l (S n)
70with bound_on_instrs_to_cost' : label → nat → Prop ≝
71| boitc_here : ∀l,n,H.
72    is_cost_label (lookup_present … g l H) →
73    bound_on_instrs_to_cost' g l n
74| boitc_later : ∀l,n,H.
75    ¬ is_cost_label (lookup_present … g l H) →
76    bound_on_instrs_to_cost g l n →
77    bound_on_instrs_to_cost' g l n.
78
79definition soundly_labelled_fn : internal_function → Prop ≝
80λf. ∀l. present … (f_graph f) l → ∃n. bound_on_instrs_to_cost (f_graph f) l n.
81
82definition well_cost_labelled_program : RTLabs_program → Prop ≝
83  λp. All ? (λx. match \snd x with [ Internal fn ⇒
84    well_cost_labelled_fn fn ∧ soundly_labelled_fn fn
85  | _ ⇒ True]) (prog_funct … p).
86
87
Note: See TracBrowser for help on using the repository browser.