1 | |
---|
2 | include "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 | |
---|
8 | definition is_cost_label : statement → bool ≝ |
---|
9 | λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ]. |
---|
10 | |
---|
11 | definition 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 | |
---|
19 | definition 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 | |
---|
33 | definition 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 | |
---|
41 | let rec successors (s : statement) : list label ≝ |
---|
42 | match 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 | |
---|
64 | inductive 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) |
---|
70 | with 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 | |
---|
79 | definition 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 | |
---|
82 | definition 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 | |
---|