1 | include "RTLabs/Traces.ma". |
---|
2 | |
---|
3 | (* Check that the RTLabs pc → cost label map is injective for a given RTLabs |
---|
4 | program. |
---|
5 | |
---|
6 | First we check functions individually, then lift to the whole program. *) |
---|
7 | |
---|
8 | definition graph_cost_injectivity : graph statement → Prop ≝ |
---|
9 | λg. ∀l1,l2,PR1,PR2,cl. |
---|
10 | cost_label_of (lookup_present ?? g l1 PR1) = Some ? cl → |
---|
11 | cost_label_of (lookup_present ?? g l2 PR2) = Some ? cl → |
---|
12 | l1 = l2. |
---|
13 | |
---|
14 | definition function_cost_injectivity ≝ |
---|
15 | λf. graph_cost_injectivity (f_graph f). |
---|
16 | |
---|
17 | definition program_cost_injectivity : RTLabs_program → Prop ≝ |
---|
18 | λp. All ? (λx. match \snd x with [ Internal f ⇒ function_cost_injectivity f | _ ⇒ True]) (prog_funct … p). |
---|
19 | |
---|
20 | definition reverse_label_map : graph statement → (option (identifier_map CostTag (identifier LabelTag))) ≝ |
---|
21 | λg. |
---|
22 | foldi |
---|
23 | statement |
---|
24 | (option (identifier_map CostTag (identifier LabelTag))) |
---|
25 | LabelTag |
---|
26 | (λl,s,m. |
---|
27 | match m with |
---|
28 | [ None ⇒ None ? |
---|
29 | | Some m ⇒ |
---|
30 | match cost_label_of s with |
---|
31 | [ Some cl ⇒ |
---|
32 | match lookup ?? m cl with |
---|
33 | [ None ⇒ Some ? (add … m cl l) |
---|
34 | | Some _ ⇒ None ? |
---|
35 | ] |
---|
36 | | None ⇒ Some ? m |
---|
37 | ] |
---|
38 | ]) |
---|
39 | g |
---|
40 | (Some ? (empty_map …)). |
---|
41 | |
---|
42 | |
---|
43 | definition check_fun_inj : internal_function → bool ≝ |
---|
44 | λf. |
---|
45 | match reverse_label_map (f_graph f) with |
---|
46 | [ None ⇒ false |
---|
47 | | Some _ ⇒ true |
---|
48 | ]. |
---|
49 | |
---|
50 | definition domain_of_pm : ∀A. positive_map A → positive_map unit ≝ |
---|
51 | λA,t. fold A (positive_map unit) (λp,a,b. insert unit p it b) t (pm_leaf unit). |
---|
52 | |
---|
53 | lemma pm_fold_ignore_adding_junk : ∀A. ∀m. ∀f,g:Pos → Pos. ∀s. |
---|
54 | (∀p,q. f p ≠ g q) → |
---|
55 | ∀p. lookup_opt unit (f p) (fold A ? (λx,a,b. insert unit (g x) it b) m s) = lookup_opt unit (f p) s. |
---|
56 | #A #m elim m |
---|
57 | [ normalize // |
---|
58 | | #oa #l #r #IHl #IHr |
---|
59 | #f #g #s #not_g #p |
---|
60 | normalize |
---|
61 | >IHr |
---|
62 | [ >IHl |
---|
63 | [ cases oa |
---|
64 | [ normalize % |
---|
65 | | #a normalize >(lookup_opt_insert_miss ?? (f p)) [ % | @not_g ] |
---|
66 | ] |
---|
67 | | #x #y % #E cases (not_g x (p0 y)) #H @H @E |
---|
68 | ] |
---|
69 | | #x #y % #E cases (not_g x (p1 y)) #H @H @E |
---|
70 | ] |
---|
71 | ] qed. |
---|
72 | |
---|
73 | lemma pm_fold_ind_gen : ∀A,B,m,f,b. |
---|
74 | ∀pre:Pos→Pos. (∀x,y.pre x = pre y → x = y) → ∀ps. (∀p. lookup_opt ? (pre p) ps = None ?) → |
---|
75 | ∀P:B → positive_map unit → Prop. |
---|
76 | P b ps → |
---|
77 | (∀p,ps,a,b. lookup_opt unit (pre p) ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f (pre p) a b) (insert unit (pre p) it ps)) → |
---|
78 | P (fold A B (λx. f (pre x)) m b) (fold ?? (λp,a,b. insert unit (pre p) it b) m ps). |
---|
79 | #A #B #m elim m |
---|
80 | [ // |
---|
81 | | #oa #l #r #IHl #IHr |
---|
82 | #f #b #pre #PRE #ps #PS #P #emp #step whd in ⊢ (?%%); |
---|
83 | @IHr |
---|
84 | [ #x #y #E lapply (PRE … E) #E' destruct // |
---|
85 | | #p change with ((λx. pre (p1 x)) p) in match (pre (p1 p)); >pm_fold_ignore_adding_junk |
---|
86 | [ cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p1 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ] |
---|
87 | | #p #q % #E lapply (PRE … E) #E' destruct |
---|
88 | ] |
---|
89 | | @IHl |
---|
90 | [ #x #y #E lapply (PRE … E) #E' destruct // |
---|
91 | | #p cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p0 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ] |
---|
92 | | cases oa in step ⊢ %; [ #_ @emp | #a #step normalize @step [ @PS | % | @emp ] ] |
---|
93 | | #p #ps' #a #b' @step |
---|
94 | ] |
---|
95 | | #p #ps' #a #b' @step |
---|
96 | ] |
---|
97 | ] qed. |
---|
98 | |
---|
99 | lemma pm_fold_ext : ∀A,B,m,f,b. |
---|
100 | fold A B f m b = fold A B (λx:Pos. f x) m b. |
---|
101 | #A #B #m elim m /4/ |
---|
102 | qed. |
---|
103 | |
---|
104 | lemma pm_fold_ind : ∀A,B,f,m,b. ∀P:B → positive_map unit → Prop. |
---|
105 | P b (pm_leaf unit) → |
---|
106 | (∀p,ps,a,b. lookup_opt unit p ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f p a b) (insert unit p it ps)) → |
---|
107 | P (fold A B f m b) (domain_of_pm A m). |
---|
108 | #A #B #f #m #b #P #emp #step |
---|
109 | >pm_fold_ext |
---|
110 | whd in ⊢ (??%); |
---|
111 | @(pm_fold_ind_gen A B m f b (λx.x) ? (pm_leaf unit) ???) |
---|
112 | [ // |
---|
113 | | // |
---|
114 | | @emp |
---|
115 | | @step |
---|
116 | ] qed. |
---|
117 | |
---|
118 | lemma pm_fold_eq : ∀A,B,b,f. |
---|
119 | (∀p,k:Pos. ∀a,s1,s2. lookup_opt B p s1 = lookup_opt B p s2 → lookup_opt B p (f k a s1) = lookup_opt B p (f k a s2)) → |
---|
120 | ∀p,s1,s2. |
---|
121 | lookup_opt B p s1 = lookup_opt B p s2 → |
---|
122 | lookup_opt B p (fold A (positive_map B) f b s1) = lookup_opt B p (fold A (positive_map B) f b s2). |
---|
123 | #A #B #b elim b |
---|
124 | [ #f #H #p #s1 #s2 #H @H |
---|
125 | | #oa #l #r #IHl #IHr #f #H #p #s1 #s2 #H' |
---|
126 | whd in match (fold ???? s1); |
---|
127 | whd in match (fold ???? s2); |
---|
128 | @IHr [ #q #k #a #s1' #s2' #H'' @H @H'' ] |
---|
129 | @IHl [ #q #k #a #s1' #s2' #H'' @H @H'' ] |
---|
130 | cases oa [ @H' | #a @H @H' ] |
---|
131 | ] qed. |
---|
132 | |
---|
133 | |
---|
134 | |
---|
135 | lemma pm_fold_ignore_prefix : ∀A. ∀m. ∀pre:Pos → Pos. (∀x,y. pre x = pre y → x = y) → |
---|
136 | ∀p. ∀pre'. |
---|
137 | lookup_opt unit (pre p) (fold A ? (λx,a,b. insert unit (pre (pre' x)) it b) m (pm_leaf ?)) = |
---|
138 | lookup_opt unit p (fold A ? (λx,a,b. insert unit (pre' x) it b) m (pm_leaf ?)). |
---|
139 | #A #m #pre #PRE |
---|
140 | cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ] |
---|
141 | generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?); |
---|
142 | generalize in match (pm_leaf unit); |
---|
143 | elim m |
---|
144 | [ #s1 #s2 #S #p #pre' @S |
---|
145 | | #oa #l #r #IHl #IHr |
---|
146 | #s1 #s2 #S #p #pre' |
---|
147 | whd in ⊢ (??(???%)(???%)); |
---|
148 | @(IHr ???? (λx. pre' (p1 x))) |
---|
149 | #p' @IHl |
---|
150 | #p'' cases oa |
---|
151 | [ @S |
---|
152 | | #a cases (decidable_eq_pos p'' (pre' one)) |
---|
153 | [ #E destruct |
---|
154 | >(lookup_opt_insert_hit ?? (pre (pre' one))) |
---|
155 | >(lookup_opt_insert_hit ?? (pre' one)) |
---|
156 | % |
---|
157 | | #NE >(lookup_opt_insert_miss ??? (pre (pre' one))) |
---|
158 | [ >(lookup_opt_insert_miss ??? (pre' one)) // |
---|
159 | | % #E @(absurd … (PRE … E) NE) |
---|
160 | ] |
---|
161 | ] |
---|
162 | ] |
---|
163 | ] qed. |
---|
164 | |
---|
165 | lemma domain_of_pm_present : ∀A,m,p. |
---|
166 | lookup_opt A p m ≠ None ? ↔ lookup_opt unit p (domain_of_pm A m) ≠ None ?. |
---|
167 | |
---|
168 | #A #m whd in match (domain_of_pm ??); |
---|
169 | elim m |
---|
170 | [ #p normalize /3/ |
---|
171 | | #oa #l #r #IHl #IHr |
---|
172 | whd in match (fold ???? (pm_leaf unit)); |
---|
173 | * |
---|
174 | [ change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?))); |
---|
175 | >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ] |
---|
176 | change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?))); |
---|
177 | >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ] |
---|
178 | cases oa |
---|
179 | [ normalize /3/ |
---|
180 | | #a change with (insert unit one ??) in ⊢ (??(?(??(???%)?))); |
---|
181 | >(lookup_opt_insert_hit ?? one) normalize |
---|
182 | % #_ % #E destruct |
---|
183 | ] |
---|
184 | | #p >(pm_fold_eq ??????? (pm_leaf unit)) |
---|
185 | [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ] |
---|
186 | @IHr |
---|
187 | | >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ] |
---|
188 | cases oa |
---|
189 | [ % |
---|
190 | | #a >(lookup_opt_insert_miss ?? (p1 p)) [2: % #E destruct ] |
---|
191 | % |
---|
192 | ] |
---|
193 | | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p1 y)) |
---|
194 | [ #E destruct |
---|
195 | >(lookup_opt_insert_hit ?? (p1 y)) |
---|
196 | >(lookup_opt_insert_hit ?? (p1 y)) |
---|
197 | % |
---|
198 | | #NE >(lookup_opt_insert_miss ?? x … NE) |
---|
199 | >(lookup_opt_insert_miss ?? x … NE) |
---|
200 | @S |
---|
201 | ] |
---|
202 | ] |
---|
203 | | #p |
---|
204 | >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ] |
---|
205 | >(pm_fold_eq ??????? (pm_leaf unit)) |
---|
206 | [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ] |
---|
207 | @IHl |
---|
208 | | cases oa |
---|
209 | [ % |
---|
210 | | #a >(lookup_opt_insert_miss ?? (p0 p)) [2: % #E destruct ] |
---|
211 | % |
---|
212 | ] |
---|
213 | | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p0 y)) |
---|
214 | [ #E destruct |
---|
215 | >(lookup_opt_insert_hit ?? (p0 y)) |
---|
216 | >(lookup_opt_insert_hit ?? (p0 y)) |
---|
217 | % |
---|
218 | | #NE >(lookup_opt_insert_miss ?? x … NE) |
---|
219 | >(lookup_opt_insert_miss ?? x … NE) |
---|
220 | @S |
---|
221 | ] |
---|
222 | ] |
---|
223 | ] |
---|
224 | ] qed. |
---|
225 | |
---|
226 | |
---|
227 | (* Returns the domain of a map as the canonical set (one made only from the |
---|
228 | empty set and addition. *) |
---|
229 | definition domain_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝ |
---|
230 | λtag,A,m. an_id_map tag unit (domain_of_pm A (match m with [ an_id_map m ⇒ m ])). |
---|
231 | lemma domain_of_map_present : ∀tag,A,m,id. |
---|
232 | present tag A m id ↔ present tag unit (domain_of_map … m) id. |
---|
233 | #tag #A * #m * #p @domain_of_pm_present |
---|
234 | qed. |
---|
235 | |
---|
236 | lemma foldi_ind : ∀A,B,tag,f,m,b. ∀P:B → identifier_set tag → Prop. |
---|
237 | P b (empty_set …) → |
---|
238 | (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) → |
---|
239 | P (foldi A B tag f m b) (domain_of_map … m). |
---|
240 | #A #B #tag #f * #m #b #P #P0 #STEP |
---|
241 | whd in match (foldi ??????); change with (an_id_map ?? (domain_of_pm A m)) in match (domain_of_map ???); |
---|
242 | @pm_fold_ind |
---|
243 | [ @P0 |
---|
244 | | #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps)) |
---|
245 | [ normalize >FR /3/ |
---|
246 | | @L |
---|
247 | | @pre |
---|
248 | ] |
---|
249 | ] qed. |
---|
250 | |
---|
251 | lemma foldi_ind' : ∀A,B,tag,f,m,b,b'. ∀P:B → identifier_set tag → Prop. |
---|
252 | P b (empty_set …) → |
---|
253 | (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) → |
---|
254 | foldi A B tag f m b = b' → |
---|
255 | P b' (domain_of_map … m). |
---|
256 | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct @foldi_ind /2/ |
---|
257 | qed. |
---|
258 | |
---|
259 | lemma reverse_label_map_ok : ∀g,r. |
---|
260 | reverse_label_map g = r → |
---|
261 | match r with |
---|
262 | [ None ⇒ ¬graph_cost_injectivity g |
---|
263 | | Some m ⇒ graph_cost_injectivity g |
---|
264 | ]. |
---|
265 | #g #r #F change with (foldi ??????) in F:(??%?); |
---|
266 | lapply (foldi_ind' ??????? (λm,ls. |
---|
267 | match m with |
---|
268 | [ None ⇒ ¬(graph_cost_injectivity g) |
---|
269 | | Some m ⇒ ∀l,cl. (present ?? ls l ∧ ∃PR. cost_label_of (lookup_present ?? g l PR) = Some ? cl) ↔ lookup ?? m cl = Some ? l |
---|
270 | ]) ?? F) |
---|
271 | [ #l #ls #s * |
---|
272 | [ #FR #L #H whd in H ⊢ %; @H |
---|
273 | | #m #FR #L #H whd in H ⊢ (match % with [_⇒?|_⇒?]); |
---|
274 | lapply (refl ? (cost_label_of s)) cases (cost_label_of s) in ⊢ (???% → %); |
---|
275 | [ #NCS whd #l' #cl cases (H l' cl) #H1 #H2 % |
---|
276 | [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3) |
---|
277 | [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct |
---|
278 | | * #_ #PR'' @H1 /3/ |
---|
279 | ] |
---|
280 | | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/ |
---|
281 | ] |
---|
282 | | #cl #CL whd in ⊢ (match % with [_⇒?|_⇒?]); |
---|
283 | lapply (refl ? (lookup ?? m cl)) cases (lookup ?? m cl) in ⊢ (???% → %); |
---|
284 | [ #Lcl whd #l' #cl' cases (H l' cl') #H1 #H2 % |
---|
285 | [ * #H3 * #PRg' #H4 cases (present_add_cases ?????? H3) |
---|
286 | [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct |
---|
287 | @lookup_add_hit |
---|
288 | | * #NE #PR'' lapply (H1 ?) [/3/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ] |
---|
289 | ] |
---|
290 | | #Lcl' cases (lookup_add_cases ??????? Lcl') |
---|
291 | [ * #E1 #E2 destruct % [ @present_add_hit | %{(lookup_is_present … L)} >(lookup_present_eq ????? L ?) assumption ] |
---|
292 | | #Lcl'' cases (H2 Lcl'') /3/ |
---|
293 | ] |
---|
294 | ] |
---|
295 | | #l' #L' whd % #GCI whd in GCI; |
---|
296 | cases (H l' cl) #H1 #H2 cases (H2 L') #PR' * #PRg' #CS' |
---|
297 | lapply (GCI l l' (lookup_is_present … L) PRg' cl ??) |
---|
298 | [ assumption |
---|
299 | | >(lookup_present_eq ????? L ?) assumption |
---|
300 | | #E destruct /2/ |
---|
301 | ] |
---|
302 | ] |
---|
303 | ] |
---|
304 | ] |
---|
305 | | whd #l #cl % |
---|
306 | [ * * #H cases (H (refl ??)) |
---|
307 | | #E normalize in E; destruct |
---|
308 | ] |
---|
309 | | cases r |
---|
310 | [ // |
---|
311 | | #m whd in ⊢ (% → %); #H |
---|
312 | #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2 |
---|
313 | cases (H l1 cl) #H1 #_ lapply (H1 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR1} @CL1 ] ] |
---|
314 | cases (H l2 cl) #H2 #_ lapply (H2 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR2} @CL2 ] ] |
---|
315 | #E >E #E' destruct % |
---|
316 | ] |
---|
317 | ] qed. |
---|
318 | |
---|
319 | lemma check_fun_inj_ok : ∀f. bool_to_Prop (check_fun_inj f) ↔ function_cost_injectivity f. |
---|
320 | #f % |
---|
321 | [ whd in ⊢ (?% → ?); |
---|
322 | lapply (reverse_label_map_ok (f_graph f)) |
---|
323 | cases (reverse_label_map ?) |
---|
324 | [ #_ * |
---|
325 | | #m #H #_ @(H (Some ? m)) % |
---|
326 | ] |
---|
327 | | lapply (reverse_label_map_ok (f_graph f)) |
---|
328 | whd in ⊢ (? → ? → ?%); |
---|
329 | cases (reverse_label_map ?) |
---|
330 | [ #H #INJ @(absurd … INJ (H (None ?) (refl ??))) |
---|
331 | | // |
---|
332 | ] |
---|
333 | ] qed. |
---|
334 | |
---|
335 | definition check_program_cost_injectivity : RTLabs_program → bool ≝ |
---|
336 | λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f | _ ⇒ true ]) (prog_funct … p). |
---|
337 | |
---|
338 | theorem check_project_cost_injectivity_ok : ∀p. |
---|
339 | bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p. |
---|
340 | #p % |
---|
341 | [ #H whd in H:(?%) ⊢ %; |
---|
342 | @(All_mp ????? (proj1 … (all_All …) H)) |
---|
343 | * #_ * // #f @(proj1 … (check_fun_inj_ok f)) |
---|
344 | | whd in ⊢ (% → ?%); |
---|
345 | #H |
---|
346 | @(proj2 … (all_All …)) |
---|
347 | @(All_mp … H) |
---|
348 | * #_ * // #f |
---|
349 | @(proj2 … (check_fun_inj_ok f)) |
---|
350 | ] qed. |
---|
351 | |
---|
352 | |
---|
353 | |
---|