1 | include "RTLabs/CostSpec.ma". |
---|
2 | |
---|
3 | (* This isn't quite right - it should be injective over all PCs, not just |
---|
4 | per-function. *) |
---|
5 | |
---|
6 | (* Check that the RTLabs pc → cost label map is injective for a given RTLabs |
---|
7 | program. |
---|
8 | |
---|
9 | First we check functions individually, then lift to the whole program. *) |
---|
10 | |
---|
11 | definition graph_cost_injectivity : graph statement → Prop ≝ |
---|
12 | λg. ∀l1,l2,PR1,PR2,cl. |
---|
13 | cost_label_of (lookup_present ?? g l1 PR1) = Some ? cl → |
---|
14 | cost_label_of (lookup_present ?? g l2 PR2) = Some ? cl → |
---|
15 | l1 = l2. |
---|
16 | |
---|
17 | definition function_cost_injectivity ≝ |
---|
18 | λf. graph_cost_injectivity (f_graph f). |
---|
19 | |
---|
20 | definition program_cost_injectivity : RTLabs_program → Prop ≝ |
---|
21 | λp. All ? (λx. match \snd x with [ Internal f ⇒ function_cost_injectivity f | _ ⇒ True]) (prog_funct … p). |
---|
22 | |
---|
23 | definition reverse_label_map : graph statement → (option (identifier_map CostTag (identifier LabelTag))) ≝ |
---|
24 | λg. |
---|
25 | foldi |
---|
26 | statement |
---|
27 | (option (identifier_map CostTag (identifier LabelTag))) |
---|
28 | LabelTag |
---|
29 | (λl,s,m. |
---|
30 | match m with |
---|
31 | [ None ⇒ None ? |
---|
32 | | Some m ⇒ |
---|
33 | match cost_label_of s with |
---|
34 | [ Some cl ⇒ |
---|
35 | match lookup ?? m cl with |
---|
36 | [ None ⇒ Some ? (add … m cl l) |
---|
37 | | Some _ ⇒ None ? |
---|
38 | ] |
---|
39 | | None ⇒ Some ? m |
---|
40 | ] |
---|
41 | ]) |
---|
42 | g |
---|
43 | (Some ? (empty_map …)). |
---|
44 | |
---|
45 | |
---|
46 | definition check_fun_inj : internal_function → bool ≝ |
---|
47 | λf. |
---|
48 | match reverse_label_map (f_graph f) with |
---|
49 | [ None ⇒ false |
---|
50 | | Some _ ⇒ true |
---|
51 | ]. |
---|
52 | |
---|
53 | |
---|
54 | lemma reverse_label_map_ok : ∀g,r. |
---|
55 | reverse_label_map g = r → |
---|
56 | match r with |
---|
57 | [ None ⇒ ¬graph_cost_injectivity g |
---|
58 | | Some m ⇒ graph_cost_injectivity g |
---|
59 | ]. |
---|
60 | #g #r #F change with (foldi ??????) in F:(??%?); |
---|
61 | lapply (foldi_ind' ??????? (λm,ls. |
---|
62 | match m with |
---|
63 | [ None ⇒ ¬(graph_cost_injectivity g) |
---|
64 | | Some m ⇒ ∀l,cl. (present ?? ls l ∧ ∃PR. cost_label_of (lookup_present ?? g l PR) = Some ? cl) ↔ lookup ?? m cl = Some ? l |
---|
65 | ]) ?? F) |
---|
66 | [ #l #ls #s * |
---|
67 | [ #FR #L #H whd in H ⊢ %; @H |
---|
68 | | #m #FR #L #H whd in H ⊢ (match % with [_⇒?|_⇒?]); |
---|
69 | lapply (refl ? (cost_label_of s)) cases (cost_label_of s) in ⊢ (???% → %); |
---|
70 | [ #NCS whd #l' #cl cases (H l' cl) #H1 #H2 % |
---|
71 | [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3) |
---|
72 | [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct |
---|
73 | | * #_ #PR'' @H1 % /2/ |
---|
74 | ] |
---|
75 | | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/ |
---|
76 | ] |
---|
77 | | #cl #CL whd in ⊢ (match % with [_⇒?|_⇒?]); |
---|
78 | lapply (refl ? (lookup ?? m cl)) cases (lookup ?? m cl) in ⊢ (???% → %); |
---|
79 | [ #Lcl whd #l' #cl' cases (H l' cl') #H1 #H2 % |
---|
80 | [ * #H3 * #PRg' #H4 cases (present_add_cases ?????? H3) |
---|
81 | [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct |
---|
82 | @lookup_add_hit |
---|
83 | | * #NE #PR'' lapply (H1 ?) [% /2/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ] |
---|
84 | ] |
---|
85 | | #Lcl' cases (lookup_add_cases ??????? Lcl') |
---|
86 | [ * #E1 #E2 destruct % [ @present_add_hit | %{(lookup_is_present … L)} >(lookup_present_eq ????? L ?) assumption ] |
---|
87 | | #Lcl'' cases (H2 Lcl'') /3/ |
---|
88 | ] |
---|
89 | ] |
---|
90 | | #l' #L' whd % #GCI whd in GCI; |
---|
91 | cases (H l' cl) #H1 #H2 cases (H2 L') #PR' * #PRg' #CS' |
---|
92 | lapply (GCI l l' (lookup_is_present … L) PRg' cl ??) |
---|
93 | [ assumption |
---|
94 | | >(lookup_present_eq ????? L ?) assumption |
---|
95 | | #E destruct @(absurd … PR' FR) |
---|
96 | ] |
---|
97 | ] |
---|
98 | ] |
---|
99 | ] |
---|
100 | | whd #l #cl % |
---|
101 | [ * * #H cases (H (refl ??)) |
---|
102 | | #E normalize in E; destruct |
---|
103 | ] |
---|
104 | | cases r |
---|
105 | [ whd in ⊢ (% → %); // |
---|
106 | | #m whd in ⊢ (% → %); #H |
---|
107 | #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2 |
---|
108 | cases (H l1 cl) #H1 #_ lapply (H1 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR1} @CL1 ] ] |
---|
109 | cases (H l2 cl) #H2 #_ lapply (H2 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR2} @CL2 ] ] |
---|
110 | #E >E #E' destruct % |
---|
111 | ] |
---|
112 | ] qed. |
---|
113 | |
---|
114 | lemma check_fun_inj_ok : ∀f. bool_to_Prop (check_fun_inj f) ↔ function_cost_injectivity f. |
---|
115 | #f % |
---|
116 | [ whd in ⊢ (?% → ?); |
---|
117 | lapply (reverse_label_map_ok (f_graph f)) |
---|
118 | cases (reverse_label_map ?) |
---|
119 | [ #_ * |
---|
120 | | #m #H #_ @(H (Some ? m)) % |
---|
121 | ] |
---|
122 | | lapply (reverse_label_map_ok (f_graph f)) |
---|
123 | whd in ⊢ (? → ? → ?%); |
---|
124 | cases (reverse_label_map ?) |
---|
125 | [ #H #INJ @(absurd … INJ (H (None ?) (refl ??))) |
---|
126 | | // |
---|
127 | ] |
---|
128 | ] qed. |
---|
129 | |
---|
130 | definition check_program_cost_injectivity : RTLabs_program → bool ≝ |
---|
131 | λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f | _ ⇒ true ]) (prog_funct … p). |
---|
132 | |
---|
133 | theorem check_program_cost_injectivity_ok : ∀p. |
---|
134 | bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p. |
---|
135 | #p % |
---|
136 | [ #H whd in H:(?%) ⊢ %; |
---|
137 | @(All_mp ????? (proj1 … (all_All …) H)) |
---|
138 | * #_ * // #f @(proj1 … (check_fun_inj_ok f)) |
---|
139 | | whd in ⊢ (% → ?%); |
---|
140 | #H |
---|
141 | @(proj2 … (all_All …)) |
---|
142 | @(All_mp … H) |
---|
143 | * #_ * // #f |
---|
144 | @(proj2 … (check_fun_inj_ok f)) |
---|
145 | ] qed. |
---|
146 | |
---|
147 | |
---|
148 | definition check_program_cost_injectivity_prf : ∀p:RTLabs_program. res (program_cost_injectivity p) ≝ |
---|
149 | λp. (match check_program_cost_injectivity p return λb. bool_to_Prop b ↔ program_cost_injectivity p → res ? with |
---|
150 | [ true ⇒ λH. OK ?? |
---|
151 | | false ⇒ λ_. Error ? (msg BadCostLabelling) |
---|
152 | ]) |
---|
153 | (check_program_cost_injectivity_ok p). |
---|
154 | @(proj1 … H) |
---|
155 | % qed. |
---|
156 | |
---|