source: src/RTLabs/CostSpec.ma @ 2226

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

Whole program proof.

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 : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
20λf,s. match s return λs. labels_present ? s → Prop with
21[ St_cond _ l1 l2 ⇒ λH.
22    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
23    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
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
61definition steps_for_statement : statement → nat ≝
62λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
63
64inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
65| bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
66| bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
67with bound_on_steps_to_cost1 : label → nat → Prop ≝
68| bostc_step : ∀l,n,H.
69    let stmt ≝ lookup_present … g l H in
70    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
71          bound_on_steps_to_cost g l' n) →
72    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
73
74definition soundly_labelled_fn : internal_function → Prop ≝
75λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
76
77definition well_cost_labelled_program : RTLabs_program → Prop ≝
78  λp. All ? (λx. match \snd x with [ Internal fn ⇒
79    well_cost_labelled_fn fn ∧ soundly_labelled_fn fn
80  | _ ⇒ True]) (prog_funct … p).
81
82
Note: See TracBrowser for help on using the repository browser.