source: src/RTLabs/CostSpec.ma @ 2475

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

Half the proofs for sound cost labelling check.

File size: 3.2 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 : ∀g:graph statement. ∀s. labels_present g s → bool ≝
20λg,s. match s return λs. labels_present g s → bool with
21[ St_cond _ l1 l2 ⇒ λH.
22    is_cost_label (lookup_present … g l1 ?) ∧
23    is_cost_label (lookup_present … g 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 … g 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,PR. well_cost_labelled_statement (f_graph f) (lookup_present … (f_graph f) l PR) (f_closed f l …)) ∧
35    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
36[ @lookup_lookup_present | cases (f_entry f) // ] qed.
37
38(* Define a notion of sound labellings of RTLabs programs. *)
39
40let rec successors (s : statement) : list label ≝
41match s with
42[ St_skip l ⇒ [l]
43| St_cost _ l ⇒ [l]
44| St_const _ _ _ l ⇒ [l]
45| St_op1 _ _ _ _ _ l ⇒ [l]
46| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
47| St_load _ _ _ l ⇒ [l]
48| St_store _ _ _ l ⇒ [l]
49| St_call_id _ _ _ l ⇒ [l]
50| St_call_ptr _ _ _ l ⇒ [l]
51(*
52| St_tailcall_id _ _ ⇒ [ ]
53| St_tailcall_ptr _ _ ⇒ [ ]
54*)
55| St_cond _ l1 l2 ⇒ [l1; l2]
56(*| St_jumptable _ ls ⇒ ls*)
57| St_return ⇒ [ ]
58].
59
60(* To show that the labelling is sound we need a bound on the number of
61   instructions in the current function until the next cost label. *)
62
63inductive bound_on_instrs_to_cost (g:graph statement) : label → nat → Prop ≝
64| boitc_step : ∀l,n,H.
65    let stmt ≝ lookup_present … g l H in
66    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
67          bound_on_instrs_to_cost' g l' n) →
68    bound_on_instrs_to_cost g l (S n)
69with bound_on_instrs_to_cost' : label → nat → Prop ≝
70| boitc_here : ∀l,n,H.
71    is_cost_label (lookup_present … g l H) →
72    bound_on_instrs_to_cost' g l n
73| boitc_later : ∀l,n,H.
74    ¬ is_cost_label (lookup_present … g l H) →
75    bound_on_instrs_to_cost g l n →
76    bound_on_instrs_to_cost' g l n.
77
78definition soundly_labelled_fn : internal_function → Prop ≝
79λf. ∀l. present … (f_graph f) l → ∃n. bound_on_instrs_to_cost (f_graph f) l n.
80
81definition well_cost_labelled_program : RTLabs_program → Prop ≝
82  λp. All ? (λx. match \snd x with [ Internal fn ⇒
83    well_cost_labelled_fn fn ∧ soundly_labelled_fn fn
84  | _ ⇒ True]) (prog_funct … p).
85
86
Note: See TracBrowser for help on using the repository browser.