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_graph 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 | let PR' ≝ ? in |
---|
99 | let st' ≝ lookup_present … g h PR' in |
---|
100 | if is_cost_label st' then stop_now else |
---|
101 | if h ∈ checking_tail then None ? else |
---|
102 | check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ? |
---|
103 | | None ⇒ λ_. |
---|
104 | if h == checking ∨ h ∈ checking_tail then None ? else |
---|
105 | stop_now (* already checked successor *) |
---|
106 | ] (try_remove_some_card … to_check h) |
---|
107 | | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *) |
---|
108 | ] |
---|
109 | ] (successors_present g st (CL … checking … (lookup_lookup_present …))) |
---|
110 | ]. |
---|
111 | [ /2 by absurd/ |
---|
112 | | lapply (H' (\fst to_check') (\snd to_check') ?) [ cases to_check' // ] |
---|
113 | #E -PR' >E in H; #H' /2/ |
---|
114 | | @SC >memb_hd // |
---|
115 | ] qed. |
---|
116 | |
---|
117 | (* An inductive specification of the above function that's easier to work with. *) |
---|
118 | |
---|
119 | inductive check_label_bounded_spec (g:graph statement) : label → list label → identifier_set LabelTag → identifier_set LabelTag → Prop ≝ |
---|
120 | | clbs_ret : ∀l,PR,tl,toch. |
---|
121 | successors (lookup_present … g l PR) = [ ] → |
---|
122 | check_label_bounded_spec g l tl toch toch |
---|
123 | | clbs_checked : ∀l,PR,l',tl,toch. |
---|
124 | successors (lookup_present … g l PR) = [l'] → |
---|
125 | ¬ l' ∈ toch → |
---|
126 | l' ≠ l → |
---|
127 | ¬ l' ∈ tl → |
---|
128 | check_label_bounded_spec g l tl toch toch |
---|
129 | | clbs_cost : ∀l,PR,l',PR',tl,toch. |
---|
130 | successors (lookup_present … g l PR) = [l'] → |
---|
131 | l' ∈ toch → |
---|
132 | is_cost_label (lookup_present … g l' PR') → |
---|
133 | check_label_bounded_spec g l tl toch toch |
---|
134 | | clbs_step : ∀l,PR,l',PR',tl,toch,toch',toch''. |
---|
135 | successors (lookup_present … g l PR) = [l'] → |
---|
136 | (* l' ∈ toch → implied *) |
---|
137 | ¬ l' ∈ tl → |
---|
138 | ¬ is_cost_label (lookup_present … g l' PR') → |
---|
139 | try_remove … toch l' = Some ? 〈it,toch'〉 → |
---|
140 | check_label_bounded_spec g l' (l::tl) toch' toch'' → |
---|
141 | check_label_bounded_spec g l tl toch toch'' |
---|
142 | | clbs_branch : ∀l,PR,x,y,zs,tl,toch. (* the other check will show that these are cost labels *) |
---|
143 | successors (lookup_present … g l PR) = x::y::zs → |
---|
144 | check_label_bounded_spec g l tl toch toch. |
---|
145 | |
---|
146 | (* TODO: move (or is it somewhere already?) *) |
---|
147 | lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0]. |
---|
148 | (b → P e1) → |
---|
149 | (¬b → P e2) → |
---|
150 | P (if b then e1 else e2). |
---|
151 | #T * /2/ |
---|
152 | qed. |
---|
153 | |
---|
154 | lemma not_orb : ∀b,c:bool. |
---|
155 | ¬ (b∨c) → |
---|
156 | (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)). |
---|
157 | * * normalize /2/ |
---|
158 | qed. |
---|
159 | |
---|
160 | lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'. |
---|
161 | check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' → |
---|
162 | check_label_bounded_spec g checking checking_tail to_check to_check'. |
---|
163 | #n elim n |
---|
164 | [ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *) |
---|
165 | | #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check' |
---|
166 | whd in ⊢ (??%? → ?); |
---|
167 | generalize in ⊢ (??(?%)? → ?); |
---|
168 | lapply (refl ? (successors (lookup_present … PR))) |
---|
169 | cases (successors (lookup_present … PR)) in ⊢ (???% → %); |
---|
170 | [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 // |
---|
171 | | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' generalize in ⊢ (??(?%)? → ?); |
---|
172 | lapply (refl ? (try_remove … to_check h)) |
---|
173 | cases (try_remove ????) in ⊢ (???% → %); |
---|
174 | [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim |
---|
175 | [ #H' #E destruct |
---|
176 | | #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC) |
---|
177 | [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) // |
---|
178 | | % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) * |
---|
179 | | assumption |
---|
180 | ] |
---|
181 | ] |
---|
182 | | * * #to_check'' #RM #H whd in ⊢ (??%? → ?); |
---|
183 | @if_elim |
---|
184 | [ #CS #E destruct @(clbs_cost … SUCC … CS) |
---|
185 | cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L // |
---|
186 | | #CS |
---|
187 | @if_elim |
---|
188 | [ #IN whd in ⊢ (??%? → ?); #E destruct |
---|
189 | | #OUT whd in ⊢ (??%? → ?); #H |
---|
190 | @(clbs_step … SUCC OUT CS RM) @(IH … H) |
---|
191 | ] |
---|
192 | ] |
---|
193 | ] |
---|
194 | | #h2 #t #SUCCS whd in ⊢ (? → ??%? → ?); #PR' #E destruct |
---|
195 | @(clbs_branch … SUCCS) |
---|
196 | ] |
---|
197 | ] |
---|
198 | ] qed. |
---|
199 | |
---|
200 | lemma check_label_bounded_c : ∀g,CL,checking,checking_tail,to_check,to_check'. |
---|
201 | check_label_bounded_spec g checking checking_tail to_check to_check' → |
---|
202 | ∀term_check,TERM,PR. |
---|
203 | check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check'. |
---|
204 | #g #CL #X1 #X2 #X3 #X4 #X elim X |
---|
205 | [ #l #PR #tl #toch #SUCC |
---|
206 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
207 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
208 | whd in ⊢ (??%?); % |
---|
209 | | #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl |
---|
210 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
211 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
212 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); |
---|
213 | cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ // | * * ] ] |
---|
214 | #L >(proj2 … (try_remove_empty …) L) #H2 |
---|
215 | whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl) |
---|
216 | % |
---|
217 | | #l #PR #l' #PR' #tl #toch #SUCC #IN #CS |
---|
218 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
219 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
220 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); |
---|
221 | cut (lookup … toch l' = Some ? it) [ whd in IN:(?%); cases (lookup ????) in IN ⊢ %; [ * | * // ] ] |
---|
222 | #L cases (try_remove_this ????? L) #to_check' #RM >RM #H2 |
---|
223 | whd in ⊢ (??%?); >CS whd in ⊢ (??%?); % |
---|
224 | | #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH |
---|
225 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
226 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
227 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2 |
---|
228 | whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS)) |
---|
229 | whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN)) |
---|
230 | whd in ⊢ (??%?); >(IH term_check' ??) % |
---|
231 | | #l #PR #x #y #zs #tl #toch #SUCC |
---|
232 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
233 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
234 | whd in ⊢ (??%?); % |
---|
235 | ] qed. |
---|
236 | |
---|
237 | lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'. |
---|
238 | check_label_bounded_spec g checking checking_tail to_check to_check' → |
---|
239 | set_subset … to_check' to_check. |
---|
240 | #g #lX #lX' #tX #tX' #S elim S // |
---|
241 | #l #PR #l' #PR' #tl #toch #toch' #toch'' #SC #NI #CS #RM #H #IH |
---|
242 | cases (try_remove_some … toch' RM) * #L1 #L2 #L3 |
---|
243 | #id #IN cases (L3 id) |
---|
244 | [ #E destruct whd in ⊢ (?%); >L1 // |
---|
245 | | #L4 whd in ⊢ (?%); >L4 @IH @IN |
---|
246 | ] qed. |
---|
247 | |
---|
248 | lemma bound_on_instrs_to_cost_prime : ∀g,l,n. |
---|
249 | bound_on_instrs_to_cost g l n → |
---|
250 | bound_on_instrs_to_cost' g l n. |
---|
251 | #g #l #n #H inversion H |
---|
252 | #l' #n' #PR #H' #E1 #E2 #_ destruct |
---|
253 | lapply (refl ? (is_cost_label (lookup_present … g l' PR))) |
---|
254 | cases (is_cost_label ?) in ⊢ (???% → ?); #CS |
---|
255 | [ @boitc_here [ @PR | @eq_true_to_b @CS ] |
---|
256 | | @boitc_later [ @PR | @eq_false_to_notb @CS | @H ] |
---|
257 | ] qed. |
---|
258 | |
---|
259 | lemma present_member : ∀tag,A,m,id. |
---|
260 | present tag A m id → member tag A m id. |
---|
261 | #tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??)) |
---|
262 | qed. |
---|
263 | |
---|
264 | (* TODO: move and eliminate dup in Traces.ma *) |
---|
265 | lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S. |
---|
266 | Exists S (λy. y = x) l → |
---|
267 | x ∈ l. |
---|
268 | #S #x #l elim l |
---|
269 | [ // |
---|
270 | | #h #t #IH |
---|
271 | normalize lapply (eqb_true … x h) |
---|
272 | cases (x==h) * |
---|
273 | [ #E #_ >(E (refl ??)) // |
---|
274 | | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct |
---|
275 | | #H @IH @H |
---|
276 | ] |
---|
277 | ] |
---|
278 | ] qed. |
---|
279 | |
---|
280 | lemma successors_inv : ∀st,x,y,zs. |
---|
281 | successors st = x::y::zs → |
---|
282 | ∃r,l1,l2. st = St_cond r l1 l2. |
---|
283 | * normalize |
---|
284 | #a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l destruct |
---|
285 | /4/ |
---|
286 | qed. |
---|
287 | |
---|
288 | include alias "utilities/deqsets.ma". |
---|
289 | |
---|
290 | lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g. |
---|
291 | (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → |
---|
292 | ∀l,PR,x,y,zs. successors (lookup_present … g l PR) = x::y::zs → |
---|
293 | ∀l'. ∀IN : l' ∈ successors (lookup_present … g l PR). |
---|
294 | is_cost_label (lookup_present … g l' ?). |
---|
295 | [2: @(successors_present … IN) @(CL l) @lookup_lookup_present ] |
---|
296 | #g #CL #WCL #l #PR #x #y #zs #SUCCS |
---|
297 | cases (successors_inv … SUCCS) |
---|
298 | #r * #l1 * #l2 #E |
---|
299 | #l' #IN generalize in ⊢ (?(?(?????%))); #OR' >E in IN; |
---|
300 | lapply (WCL l PR) generalize in ⊢ (?(???%) → ?); >E in ⊢ (% → % → ?); #LP #WCst |
---|
301 | cases (andb_Prop_true ?? WCst) |
---|
302 | #H1 #H2 |
---|
303 | whd in ⊢ (?% → ?); @eqb_elim |
---|
304 | [ 2: #_ #IN lapply (memb_single … IN) ] |
---|
305 | #E destruct // |
---|
306 | qed. |
---|
307 | |
---|
308 | |
---|
309 | lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'. |
---|
310 | ∀CL:graph_closed g. |
---|
311 | (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → |
---|
312 | check_label_bounded_spec g checking checking_tail to_check to_check' → |
---|
313 | (∀l. l∈g → ¬l ∈ to_check → l≠checking → ¬l∈checking_tail → ∃n. bound_on_instrs_to_cost g l n) → |
---|
314 | ∀l. l = checking ∨ bool_to_Prop (l∈to_check) → |
---|
315 | bool_to_Prop (l∈to_check') ∨ ∃n. bound_on_instrs_to_cost g l n. |
---|
316 | #g #X1 #X2 #X3 #X4 #CL #WCL #X elim X |
---|
317 | [ #l #PR #tl #toch #SUCC #INV #l' * |
---|
318 | [ #E destruct %2 %{1} % [ @PR | >SUCC #l' * ] |
---|
319 | | #IN %1 @IN |
---|
320 | ] |
---|
321 | | #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl #INV #l'' * |
---|
322 | [ #E destruct %2 |
---|
323 | cases (INV l' ????) |
---|
324 | [ #n #B |
---|
325 | %{(S n)} % [ @PR | >SUCC #l'' * [2: *] #E destruct /2/ ] |
---|
326 | | @present_member @(successors_present … (CL l ? (lookup_lookup_present … PR))) |
---|
327 | >SUCC @eq_true_to_b @memb_hd |
---|
328 | | assumption |
---|
329 | | assumption |
---|
330 | | assumption |
---|
331 | ] |
---|
332 | | #IN %1 assumption |
---|
333 | ] |
---|
334 | | #l #PR #l' #PR' #tl #toch #SUCC #IN #CS #INV #l'' * |
---|
335 | [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ] |
---|
336 | | /2/ |
---|
337 | ] |
---|
338 | | #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN_tl #NCS #RM #H #IH #INV #l'' * |
---|
339 | [ #E destruct %2 cases (IH ? l' ?) |
---|
340 | [ #IN @⊥ lapply (check_label_bounded_subset … H l' IN) #IN' |
---|
341 | cases (try_remove_some ?????? RM) * #_ #L #_ whd in IN':(?%); |
---|
342 | cases (lookup ????) in IN' L; [ * | * #_ #E destruct ] |
---|
343 | | * #n #B %{(S n)} % [ // | #l'' >SUCC * [2: *] #E destruct /2/ ] |
---|
344 | | #l'' #INg #INch' #NEQ #NIN_ltl @(INV l'' INg ???) |
---|
345 | [ @notb_Prop % #INch @(absurd ?? (Prop_notb … INch')) |
---|
346 | cases (try_remove_some ?????? RM) * #_ #_ #L |
---|
347 | cases (L l'') [ #E destruct cases NEQ #X cases (X (refl ??)) ] |
---|
348 | #L' whd in ⊢ (?%); <L' @INch |
---|
349 | | % #E destruct cases (Prop_notb … NIN_ltl) #X @X @eq_true_to_b @memb_hd |
---|
350 | | @notb_Prop @(not_to_not … (Prop_notb … NIN_ltl)) #IN @eq_true_to_b @memb_cons @IN |
---|
351 | ] |
---|
352 | | %1 % |
---|
353 | ] |
---|
354 | | #IN @(IH ? l'' ?) |
---|
355 | [ #l''' #INg #NINch' #NEQ #NINtl @INV |
---|
356 | [ assumption |
---|
357 | | @notb_Prop @(not_to_not … (Prop_notb … NINch')) |
---|
358 | cases (try_remove_some ?????? RM) * #L1 #L2 #L3 |
---|
359 | cases (L3 l''') |
---|
360 | [ #E destruct @⊥ cases NEQ /2/ |
---|
361 | | #L whd in ⊢ (?% → ?%); >L // |
---|
362 | ] |
---|
363 | | % #E destruct cases (Prop_notb … NINtl) #X @X @eq_true_to_b @memb_hd |
---|
364 | | @notb_Prop @(not_to_not … (Prop_notb … NINtl)) #IN @eq_true_to_b @memb_cons @IN |
---|
365 | ] |
---|
366 | | cases (try_remove_some ?????? RM) * #L1 #L2 #L3 |
---|
367 | cases (L3 l'') [ #E destruct %1 % | #L %2 whd in ⊢ (?%); <L @IN ] |
---|
368 | ] |
---|
369 | ] |
---|
370 | | #l #PR #x #y #zs #tl #toch #SUCCS #INV #l' * |
---|
371 | [ #E destruct %2 %{1} % [ // ] |
---|
372 | #l' #EX @boitc_here |
---|
373 | [ @(successors_present … (CL l ? (lookup_lookup_present … PR))) |
---|
374 | @Exists_memb @EX |
---|
375 | | @(after_branch_are_cost_labels … WCL … SUCCS) |
---|
376 | ] |
---|
377 | | /2/ |
---|
378 | ] |
---|
379 | ] qed. |
---|
380 | |
---|
381 | let rec check_graph_bounded |
---|
382 | (g : graph statement) |
---|
383 | (CL : graph_closed g) |
---|
384 | (to_check : identifier_set LabelTag) |
---|
385 | (SUB : set_subset … to_check g) |
---|
386 | (start : label) |
---|
387 | (PR : present ?? g start) |
---|
388 | (SMALLER : gt (id_map_size … g) (id_map_size … to_check)) |
---|
389 | (term_check : nat) |
---|
390 | on term_check : gt term_check (id_map_size … to_check) → bool ≝ |
---|
391 | match term_check return λx. ge x ? → bool with |
---|
392 | [ O ⇒ λH.⊥ |
---|
393 | | S term_check' ⇒ λH. |
---|
394 | let TERM' ≝ ? in |
---|
395 | match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with |
---|
396 | [ None ⇒ λ_. false |
---|
397 | | Some to_check' ⇒ λH'. |
---|
398 | match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with |
---|
399 | [ None ⇒ λ_.λ_.λ_. true |
---|
400 | | Some l_to_check'' ⇒ λL,SUB',C. |
---|
401 | check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ?? term_check' ? |
---|
402 | ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check') |
---|
403 | ] (refl ??) |
---|
404 | ]. |
---|
405 | [ 2,3,4,5: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB' |
---|
406 | lapply (check_label_bounded_subset … (check_label_bounded_s … H')) #SUB'' |
---|
407 | ] |
---|
408 | [ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN |
---|
409 | | @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L // |
---|
410 | | whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/ |
---|
411 | | whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/ |
---|
412 | | /2/ |
---|
413 | | @SMALLER |
---|
414 | ] qed. |
---|
415 | |
---|
416 | lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,SMALLER,TERM. |
---|
417 | (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → |
---|
418 | check_graph_bounded g CL to_check SUB start PR SMALLER term_check TERM = true → |
---|
419 | (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) → |
---|
420 | ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n. |
---|
421 | #g #CL #term_check elim term_check |
---|
422 | [ #to_check #SUB #start #PR #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct |
---|
423 | | #term_check' #IH #to_check #SUB #start #PR #SMALLER #TERM #WCL |
---|
424 | whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); |
---|
425 | cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?); |
---|
426 | [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ] |
---|
427 | generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?); |
---|
428 | lapply (choose_empty … to_check') |
---|
429 | cases (choose LabelTag unit to_check') |
---|
430 | [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN |
---|
431 | cases (true_or_false_Prop (l∈to_check ∨ l == start)) |
---|
432 | [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?) |
---|
433 | [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; * |
---|
434 | | // |
---|
435 | | // |
---|
436 | | @WCL |
---|
437 | | #l' #IN_g #NIN_to_check #NEQ #_ @H // |
---|
438 | | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E |
---|
439 | ] |
---|
440 | | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ] |
---|
441 | ] |
---|
442 | | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); |
---|
443 | #CHECK #H @(IH … CHECK) |
---|
444 | [ @WCL |
---|
445 | | #l #INg #NIN'' #NEQ |
---|
446 | cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN'')) |
---|
447 | cases (H4 … (refl ??)) * #L1 #L2 #L3 |
---|
448 | cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ] |
---|
449 | #NIN' |
---|
450 | cases (true_or_false_Prop (l∈to_check ∨ l == start)) |
---|
451 | [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?) |
---|
452 | [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN')) |
---|
453 | | // |
---|
454 | | // |
---|
455 | | @WCL |
---|
456 | | #l' #IN_g #NIN_to_check #NEQ #_ @H // |
---|
457 | | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E |
---|
458 | ] |
---|
459 | | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ] |
---|
460 | ] |
---|
461 | ] |
---|
462 | ] |
---|
463 | ] qed. |
---|
464 | |
---|
465 | (* TODO: move *) |
---|
466 | definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝ |
---|
467 | λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])). |
---|
468 | |
---|
469 | lemma id_set_of_map_subset : ∀tag,A,m. |
---|
470 | id_set_of_map tag A m ⊆ m. |
---|
471 | #tag #A * #m * #id normalize |
---|
472 | >lookup_opt_map normalize cases (lookup_opt ???) // |
---|
473 | qed. |
---|
474 | |
---|
475 | lemma id_set_of_map_present : ∀tag,A,m,id. |
---|
476 | present tag A m id ↔ present tag unit (id_set_of_map … m) id. |
---|
477 | #tag #A * #m * #id % |
---|
478 | normalize @not_to_not |
---|
479 | >lookup_opt_map cases (lookup_opt ???) normalize // |
---|
480 | #a #E destruct |
---|
481 | qed. |
---|
482 | |
---|
483 | lemma id_set_of_map_card : ∀tag,A,m. |
---|
484 | |m| = |id_set_of_map tag A m|. |
---|
485 | #tag #A * #m whd in ⊢ (??%%); >map_size // |
---|
486 | qed. |
---|
487 | |
---|
488 | definition check_sound_cost_fn : internal_function → bool ≝ |
---|
489 | λfn. |
---|
490 | match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with |
---|
491 | [ None ⇒ λEMP. ⊥ |
---|
492 | | Some to_check ⇒ λ_.λCARD,L. |
---|
493 | check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ?? (|f_graph fn|) ? |
---|
494 | ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn))) |
---|
495 | (try_remove_some_card ????) |
---|
496 | (try_remove_some ????). |
---|
497 | [ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H |
---|
498 | @PR' @H % |
---|
499 | | cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN |
---|
500 | cases (L3 id) |
---|
501 | [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/ |
---|
502 | | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) * |
---|
503 | whd in match (present ????); whd in match (present ? unit ??); |
---|
504 | lapply (member_present … IN) whd in match (present ? unit ??); <E |
---|
505 | cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/ |
---|
506 | ] |
---|
507 | | cases (f_entry fn) // |
---|
508 | | 4,5: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) // |
---|
509 | ] qed. |
---|
510 | |
---|
511 | axiom check_sound_cost_fn_ok : ∀fn. |
---|
512 | well_cost_labelled_fn fn → |
---|
513 | bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn. |
---|
514 | (* |
---|
515 | #fn #WCL % |
---|
516 | [ whd in ⊢ (?% → %); |
---|
517 | generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?); |
---|
518 | cases (try_remove ????) |
---|
519 | [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E |
---|
520 | lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?); |
---|
521 | >(E (refl ??)) * /3/ |
---|
522 | | * * #to_check #H1 #H2 #H3 |
---|
523 | whd in ⊢ (?% → ?); #CHECK |
---|
524 | #l #PR @(check_graph_bounded_ok … CHECK) |
---|
525 | [ #l' #PR' cases WCL // |
---|
526 | | #l' #IN #NIN #NEQ @⊥ |
---|
527 | cases (H1 … (refl ??)) * #L1 #L2 #L3 |
---|
528 | @(absurd ?? (Prop_notb … NIN)) |
---|
529 | cases (L3 l') |
---|
530 | [ #E >E in NEQ; * #H cases (H (refl ??)) |
---|
531 | | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …)) |
---|
532 | @member_present @IN |
---|
533 | ] |
---|
534 | | /2/ |
---|
535 | ] |
---|
536 | ] |
---|
537 | | TODO |
---|
538 | *) |
---|
539 | |
---|
540 | definition check_cost_program : RTLabs_program → bool ≝ |
---|
541 | λp. all ? (λfn. match \snd fn with |
---|
542 | [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn |
---|
543 | | External _ ⇒ true |
---|
544 | ]) (prog_funct … p). |
---|
545 | |
---|
546 | theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p. |
---|
547 | #p whd in ⊢ (?(?%)%); % |
---|
548 | [ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp |
---|
549 | * #id * #fd |
---|
550 | [ #H cases (andb_Prop_true … H) #W #S |
---|
551 | lapply (proj1 … (check_well_cost_fn_ok …) W) #W' |
---|
552 | % |
---|
553 | [ // |
---|
554 | | @(proj1 … (check_sound_cost_fn_ok …)) // |
---|
555 | ] |
---|
556 | | // |
---|
557 | ] |
---|
558 | | #H @(proj2 … (all_All …)) @(All_mp … H) |
---|
559 | * #id * #fd |
---|
560 | [ * #W #S |
---|
561 | lapply ((proj2 … (check_well_cost_fn_ok …)) W) |
---|
562 | lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/ |
---|
563 | | // |
---|
564 | ] |
---|
565 | ] qed. |
---|
566 | |
---|