1 | |
---|
2 | include "RTLabs/CostSpec.ma". |
---|
3 | |
---|
4 | (* TODO: move ----→ *) |
---|
5 | |
---|
6 | lemma Exists_to_All : ∀T,P,l. |
---|
7 | (∀x. Exists ? (λy. y = x) l → P x) → |
---|
8 | All T P l. |
---|
9 | #T #P #l elim l [ // | #h #t #IH #H % [ @H %1 % | @IH #t #E @H %2 @E ] ] |
---|
10 | qed. |
---|
11 | |
---|
12 | let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝ |
---|
13 | match l with |
---|
14 | [ nil ⇒ true |
---|
15 | | cons h t ⇒ P h ∧ all A P t |
---|
16 | ]. |
---|
17 | |
---|
18 | lemma all_All : ∀A,P,l. bool_to_Prop (all A P l) ↔ All A (λa.bool_to_Prop (P a)) l. |
---|
19 | #A #P #l elim l |
---|
20 | [ % // |
---|
21 | | #h #t * #IH #IH' % |
---|
22 | [ whd in ⊢ (?% → %); cases (P h) [ #p % /2/ | * ] |
---|
23 | | * #p #H whd in ⊢ (?%); >p /2/ |
---|
24 | ] |
---|
25 | ] qed. |
---|
26 | |
---|
27 | (* ←---- move *) |
---|
28 | |
---|
29 | definition check_well_cost_fn : internal_function → bool ≝ |
---|
30 | λf. |
---|
31 | idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement f s (f_closed f l s PR)) ∧ |
---|
32 | is_cost_label (lookup_present … (f_graph f) (f_entry f) ?). |
---|
33 | cases (f_entry f) // |
---|
34 | qed. |
---|
35 | |
---|
36 | lemma check_well_cost_fn_ok : ∀fn. bool_to_Prop (check_well_cost_fn fn) ↔ well_cost_labelled_fn fn. |
---|
37 | #fn % |
---|
38 | [ #H cases (andb_Prop_true … H) #ST #EN |
---|
39 | % [ lapply (proj1 … (idmap_all_ok …) ST) // | @EN ] |
---|
40 | | * #ST #EN @andb_Prop |
---|
41 | [ @(proj2 … (idmap_all_ok …)) #l #st #L |
---|
42 | cut (present ?? (f_graph fn) l) [ whd >L % #E destruct ] #PR |
---|
43 | lapply (ST l PR) generalize in ⊢ (?(???%) → ?); |
---|
44 | >(lookup_present_eq ????? L PR) // |
---|
45 | | @eq_true_to_b @EN |
---|
46 | ] |
---|
47 | ] qed. |
---|
48 | |
---|
49 | include "basics/lists/listb.ma". |
---|
50 | include alias "utilities/deqsets.ma". |
---|
51 | |
---|
52 | lemma successors_present : ∀g,st. |
---|
53 | labels_present g st → |
---|
54 | ∀l. l ∈ successors st → |
---|
55 | present ?? g l. |
---|
56 | #g * |
---|
57 | [ #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
58 | | #cs #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
59 | | #ty #r #c #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
60 | | #ty1 #ty2 #op #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
61 | | #ty1 #ty2 #ty3 #op #r1 #r2 #r3 #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
62 | | #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
63 | | #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
64 | | #id #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
65 | | #r #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
66 | | #r #l1 #l2 * #PR1 #PR2 #l3 whd in ⊢ (?% → ?); @eqb_elim [ // | #_ #IN >(memb_single … IN) // ] |
---|
67 | | #_ #l * |
---|
68 | ] qed. |
---|
69 | |
---|
70 | include alias "common/Identifiers.ma". |
---|
71 | |
---|
72 | (* Check that from [checking] we reach a cost label without going through |
---|
73 | [checking_tail], which would form a loop in the CFG. We also have a set of |
---|
74 | labels that we have still [to_check], and return an updated set of labels |
---|
75 | to check if the check for the current label is successful. *) |
---|
76 | let rec check_label_bounded |
---|
77 | (g : graph statement) |
---|
78 | (CL : graph_closed g) |
---|
79 | (checking : label) |
---|
80 | (PR : present ?? g checking) |
---|
81 | (checking_tail : list label) |
---|
82 | (to_check : identifier_set LabelTag) |
---|
83 | (term_check : nat) |
---|
84 | on term_check : gt term_check (id_map_size … to_check) → option (identifier_set LabelTag) ≝ |
---|
85 | let stop_now ≝ Some ? to_check in |
---|
86 | match term_check return λx. ge x ? → ? with |
---|
87 | [ O ⇒ λH.⊥ |
---|
88 | | S term_check' ⇒ λH. |
---|
89 | let st ≝ lookup_present … g checking PR in |
---|
90 | let succs ≝ successors st in |
---|
91 | match succs return λsc. (∀l.l∈sc → ?) → ? with |
---|
92 | [ nil ⇒ λ_. stop_now |
---|
93 | | cons h t ⇒ |
---|
94 | match t with |
---|
95 | [ nil ⇒ λSC. (* single successor *) |
---|
96 | match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with |
---|
97 | [ Some to_check' ⇒ λH'. |
---|
98 | if h ∈ checking_tail then None ? else |
---|
99 | let PR' ≝ ? in |
---|
100 | let st' ≝ lookup_present … g h PR' in |
---|
101 | if is_cost_label st' then stop_now else |
---|
102 | check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ? |
---|
103 | | None ⇒ λ_. stop_now (* already checked successor *) |
---|
104 | ] (try_remove_some_card … to_check h) |
---|
105 | | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *) |
---|
106 | ] |
---|
107 | ] (successors_present g st (CL … checking … (lookup_lookup_present …))) |
---|
108 | ]. |
---|
109 | [ /2 by absurd/ |
---|
110 | | lapply (H' (\fst to_check') (\snd to_check') ?) [ cases to_check' // ] |
---|
111 | #E -PR' >E in H; #H' /2/ |
---|
112 | | @SC >memb_hd // |
---|
113 | ] qed. |
---|
114 | |
---|
115 | (* An inductive specification of the above function that's easier to work with. *) |
---|
116 | |
---|
117 | inductive check_label_bounded_spec (g:graph statement) : label → list label → identifier_set LabelTag → identifier_set LabelTag → Prop ≝ |
---|
118 | | clbs_ret : ∀l,PR,tl,toch. |
---|
119 | successors (lookup_present … g l PR) = [ ] → |
---|
120 | check_label_bounded_spec g l tl toch toch |
---|
121 | | clbs_checked : ∀l,PR,l',tl,toch. |
---|
122 | successors (lookup_present … g l PR) = [l'] → |
---|
123 | ¬ l' ∈ toch → |
---|
124 | check_label_bounded_spec g l tl toch toch |
---|
125 | | clbs_cost : ∀l,PR,l',PR',tl,toch. |
---|
126 | successors (lookup_present … g l PR) = [l'] → |
---|
127 | l' ∈ toch → |
---|
128 | is_cost_label (lookup_present … g l' PR') → |
---|
129 | check_label_bounded_spec g l tl toch toch |
---|
130 | | clbs_step : ∀l,PR,l',PR',tl,toch,toch',toch''. |
---|
131 | successors (lookup_present … g l PR) = [l'] → |
---|
132 | (* l' ∈ toch → implied *) |
---|
133 | ¬ l' ∈ tl → |
---|
134 | ¬ is_cost_label (lookup_present … g l' PR') → |
---|
135 | try_remove … toch l' = Some ? 〈it,toch'〉 → |
---|
136 | check_label_bounded_spec g l' (l::tl) toch' toch'' → |
---|
137 | check_label_bounded_spec g l tl toch toch'' |
---|
138 | | clbs_branch : ∀l,PR,x,y,zs,tl,toch. (* the other check will show that these are cost labels *) |
---|
139 | successors (lookup_present … g l PR) = x::y::zs → |
---|
140 | check_label_bounded_spec g l tl toch toch. |
---|
141 | |
---|
142 | (* TODO: move (or is it somewhere already?) *) |
---|
143 | lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0]. |
---|
144 | (b → P e1) → |
---|
145 | (¬b → P e2) → |
---|
146 | P (if b then e1 else e2). |
---|
147 | #T * /2/ |
---|
148 | qed. |
---|
149 | |
---|
150 | lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'. |
---|
151 | check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' → |
---|
152 | check_label_bounded_spec g checking checking_tail to_check to_check'. |
---|
153 | #n elim n |
---|
154 | [ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *) |
---|
155 | | #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check' |
---|
156 | whd in ⊢ (??%? → ?); |
---|
157 | generalize in ⊢ (??(?%)? → ?); |
---|
158 | lapply (refl ? (successors (lookup_present … PR))) |
---|
159 | cases (successors (lookup_present … PR)) in ⊢ (???% → %); |
---|
160 | [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 // |
---|
161 | | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' generalize in ⊢ (??(?%)? → ?); |
---|
162 | lapply (refl ? (try_remove … to_check h)) |
---|
163 | cases (try_remove ????) in ⊢ (???% → %); |
---|
164 | [ #RM whd in ⊢ (? → ??%? → ?); #H #E destruct @(clbs_checked … SUCC) |
---|
165 | whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) // |
---|
166 | | * * #to_check'' #RM #H whd in ⊢ (??%? → ?); |
---|
167 | @if_elim |
---|
168 | [ #IN whd in ⊢ (??%? → ?); #E destruct |
---|
169 | | #OUT whd in ⊢ (??%? → ?); |
---|
170 | @if_elim |
---|
171 | [ #CS #E destruct @(clbs_cost … SUCC … CS) |
---|
172 | cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L // |
---|
173 | | #CS #H @(clbs_step … SUCC OUT CS RM) @(IH … H) |
---|
174 | ] |
---|
175 | ] |
---|
176 | ] |
---|
177 | | #h2 #t #SUCCS whd in ⊢ (? → ??%? → ?); #PR' #E destruct |
---|
178 | @(clbs_branch … SUCCS) |
---|
179 | ] |
---|
180 | ] |
---|
181 | ] qed. |
---|
182 | |
---|
183 | |
---|
184 | |
---|
185 | lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'. |
---|
186 | check_label_bounded_spec g checking checking_tail to_check to_check' → |
---|
187 | set_subset … to_check' to_check. |
---|
188 | #g #lX #lX' #tX #tX' #S elim S // |
---|
189 | #l #PR #l' #PR' #tl #toch #toch' #toch'' #SC #NI #CS #RM #H #IH |
---|
190 | cases (try_remove_some … toch' RM) * #L1 #L2 #L3 |
---|
191 | #id #IN cases (L3 id) |
---|
192 | [ #E destruct whd in ⊢ (?%); >L1 // |
---|
193 | | #L4 whd in ⊢ (?%); >L4 @IH @IN |
---|
194 | ] qed. |
---|
195 | |
---|
196 | let rec check_graph_bounded |
---|
197 | (g : graph statement) |
---|
198 | (CL : graph_closed g) |
---|
199 | (to_check : identifier_set LabelTag) |
---|
200 | (SUB : set_subset … to_check g) |
---|
201 | (start : label) |
---|
202 | (PR : present ?? g start) |
---|
203 | (SMALLER : gt (id_map_size … g) (id_map_size … to_check)) |
---|
204 | (term_check : nat) |
---|
205 | on term_check : gt term_check (id_map_size … to_check) → bool ≝ |
---|
206 | match term_check return λx. ge x ? → bool with |
---|
207 | [ O ⇒ λH.⊥ |
---|
208 | | S term_check' ⇒ λH. |
---|
209 | let TERM' ≝ ? in |
---|
210 | match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with |
---|
211 | [ None ⇒ λ_. false |
---|
212 | | Some to_check' ⇒ λH'. |
---|
213 | match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with |
---|
214 | [ None ⇒ λ_.λ_.λ_. true |
---|
215 | | Some l_to_check'' ⇒ λL,SUB',C. |
---|
216 | check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ?? term_check' ? |
---|
217 | ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check') |
---|
218 | ] (refl ??) |
---|
219 | ]. |
---|
220 | [ 2,3,4,5: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB' |
---|
221 | lapply (check_label_bounded_subset … (check_label_bounded_s … H')) #SUB'' |
---|
222 | ] |
---|
223 | [ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN |
---|
224 | | @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L // |
---|
225 | | whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/ |
---|
226 | | whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/ |
---|
227 | | /2/ |
---|
228 | | @SMALLER |
---|
229 | ] qed. |
---|
230 | |
---|
231 | (* TODO: move *) |
---|
232 | definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝ |
---|
233 | λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])). |
---|
234 | |
---|
235 | lemma id_set_of_map_subset : ∀tag,A,m. |
---|
236 | id_set_of_map tag A m ⊆ m. |
---|
237 | #tag #A * #m * #id normalize |
---|
238 | >lookup_opt_map normalize cases (lookup_opt ???) // |
---|
239 | qed. |
---|
240 | |
---|
241 | lemma id_set_of_map_present : ∀tag,A,m,id. |
---|
242 | present tag A m id ↔ present tag unit (id_set_of_map … m) id. |
---|
243 | #tag #A * #m * #id % |
---|
244 | normalize @not_to_not |
---|
245 | >lookup_opt_map cases (lookup_opt ???) normalize // |
---|
246 | #a #E destruct |
---|
247 | qed. |
---|
248 | |
---|
249 | lemma id_set_of_map_card : ∀tag,A,m. |
---|
250 | |m| = |id_set_of_map tag A m|. |
---|
251 | #tag #A * #m whd in ⊢ (??%%); >map_size // |
---|
252 | qed. |
---|
253 | |
---|
254 | definition check_sound_cost_fn : internal_function → bool ≝ |
---|
255 | λfn. |
---|
256 | match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with |
---|
257 | [ None ⇒ λEMP. ⊥ |
---|
258 | | Some to_check ⇒ λ_.λCARD,L. |
---|
259 | check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ?? (|f_graph fn|) ? |
---|
260 | ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn))) |
---|
261 | (try_remove_some_card ????) |
---|
262 | (try_remove_some ????). |
---|
263 | [ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H |
---|
264 | @PR' @H % |
---|
265 | | cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN |
---|
266 | cases (L3 id) |
---|
267 | [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/ |
---|
268 | | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) * |
---|
269 | whd in match (present ????); whd in match (present ? unit ??); |
---|
270 | lapply (member_present … IN) whd in match (present ? unit ??); <E |
---|
271 | cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/ |
---|
272 | ] |
---|
273 | | cases (f_entry fn) // |
---|
274 | | 4,5: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) // |
---|
275 | ] qed. |
---|
276 | |
---|
277 | axiom check_sound_cost_fn_ok : ∀fn. bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn. |
---|
278 | |
---|
279 | definition check_cost_program : RTLabs_program → bool ≝ |
---|
280 | λp. all ? (λfn. match \snd fn with |
---|
281 | [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn |
---|
282 | | External _ ⇒ true |
---|
283 | ]) (prog_funct … p). |
---|
284 | |
---|
285 | theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p. |
---|
286 | #p whd in ⊢ (?(?%)%); % |
---|
287 | [ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp |
---|
288 | * #id * #fd |
---|
289 | [ #H cases (andb_Prop_true … H) #W #S % |
---|
290 | [ @(proj1 … (check_well_cost_fn_ok … )) // |
---|
291 | | @(proj1 … (check_sound_cost_fn_ok …)) // |
---|
292 | ] |
---|
293 | | // |
---|
294 | ] |
---|
295 | | #H @(proj2 … (all_All …)) @(All_mp … H) |
---|
296 | * #id * #fd |
---|
297 | [ * #W #S |
---|
298 | lapply ((proj2 … (check_well_cost_fn_ok …)) W) |
---|
299 | lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/ |
---|
300 | | // |
---|
301 | ] |
---|
302 | ] qed. |
---|
303 | |
---|