1 | |
---|
2 | include "RTLabs/CostSpec.ma". |
---|
3 | include "utilities/extra_bool.ma". |
---|
4 | include "utilities/listb_extra.ma". |
---|
5 | include "RTLabs/CostMisc.ma". |
---|
6 | |
---|
7 | definition check_well_cost_fn : internal_function → bool ≝ |
---|
8 | λf. |
---|
9 | idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement (f_graph f) s (f_closed f l s PR)) ∧ |
---|
10 | is_cost_label (lookup_present … (f_graph f) (f_entry f) ?). |
---|
11 | cases (f_entry f) // |
---|
12 | qed. |
---|
13 | |
---|
14 | lemma check_well_cost_fn_ok : ∀fn. bool_to_Prop (check_well_cost_fn fn) ↔ well_cost_labelled_fn fn. |
---|
15 | #fn % |
---|
16 | [ #H cases (andb_Prop_true … H) #ST #EN |
---|
17 | % [ lapply (proj1 … (idmap_all_ok …) ST) // | @EN ] |
---|
18 | | * #ST #EN @andb_Prop |
---|
19 | [ @(proj2 … (idmap_all_ok …)) #l #st #L |
---|
20 | cut (present ?? (f_graph fn) l) [ whd >L % #E destruct ] #PR |
---|
21 | lapply (ST l PR) generalize in ⊢ (?(???%) → ?); |
---|
22 | >(lookup_present_eq ????? L PR) // |
---|
23 | | @eq_true_to_b @EN |
---|
24 | ] |
---|
25 | ] qed. |
---|
26 | |
---|
27 | include alias "utilities/deqsets_extra.ma". |
---|
28 | |
---|
29 | lemma successors_present : ∀g,st. |
---|
30 | labels_present g st → |
---|
31 | ∀l. l ∈ successors st → |
---|
32 | present ?? g l. |
---|
33 | #g * |
---|
34 | [ #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
35 | | #cs #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
36 | | #ty #r #c #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
37 | | #ty1 #ty2 #op #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
38 | | #ty1 #ty2 #ty3 #op #r1 #r2 #r3 #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
39 | | #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
40 | | #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
41 | | #id #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
42 | | #r #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR |
---|
43 | | #r #l1 #l2 * #PR1 #PR2 #l3 whd in ⊢ (?% → ?); @eqb_elim [ // | #_ #IN >(memb_single … IN) // ] |
---|
44 | | #_ #l * |
---|
45 | ] qed. |
---|
46 | |
---|
47 | include alias "common/Identifiers.ma". |
---|
48 | |
---|
49 | (* Check that from [checking] we reach a cost label without going through |
---|
50 | [checking_tail], which would form a loop in the CFG. We also have a set of |
---|
51 | labels that we have still [to_check], and return an updated set of labels |
---|
52 | to check if the check for the current label is successful. *) |
---|
53 | let rec check_label_bounded |
---|
54 | (g : graph statement) |
---|
55 | (CL : graph_closed g) |
---|
56 | (checking : label) |
---|
57 | (PR : present ?? g checking) |
---|
58 | (checking_tail : list label) |
---|
59 | (to_check : identifier_set LabelTag) |
---|
60 | (term_check : nat) |
---|
61 | on term_check : gt term_check (id_map_size … to_check) → option (identifier_set LabelTag) ≝ |
---|
62 | let stop_now ≝ Some ? to_check in |
---|
63 | match term_check return λx. ge x ? → ? with |
---|
64 | [ O ⇒ λH.⊥ |
---|
65 | | S term_check' ⇒ λH. |
---|
66 | let st ≝ lookup_present … g checking PR in |
---|
67 | let succs ≝ successors st in |
---|
68 | match succs return λsc. (∀l.l∈sc → ?) → ? with |
---|
69 | [ nil ⇒ λ_. stop_now |
---|
70 | | cons h t ⇒ |
---|
71 | match t with |
---|
72 | [ nil ⇒ λSC. (* single successor *) |
---|
73 | let PR' ≝ ? in |
---|
74 | let st' ≝ lookup_present … g h PR' in |
---|
75 | if is_cost_label st' then stop_now else |
---|
76 | match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with |
---|
77 | [ Some to_check' ⇒ λH'. |
---|
78 | check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ? |
---|
79 | | None ⇒ λ_. |
---|
80 | if h == checking ∨ h ∈ checking_tail then None ? else |
---|
81 | stop_now (* already checked successor *) |
---|
82 | ] (try_remove_some_card … to_check h) |
---|
83 | | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *) |
---|
84 | ] |
---|
85 | ] (successors_present g st (CL … checking … (lookup_lookup_present …))) |
---|
86 | ]. |
---|
87 | [ /2 by absurd/ |
---|
88 | | lapply (H' (\fst to_check') (\snd to_check') ?) [ cases to_check' // ] |
---|
89 | #E -PR' >E in H; #H' /2/ |
---|
90 | | @SC >memb_hd // |
---|
91 | ] qed. |
---|
92 | |
---|
93 | (* An inductive specification of the above function that's easier to work with. *) |
---|
94 | |
---|
95 | inductive check_label_bounded_spec (g:graph statement) : label → list label → identifier_set LabelTag → identifier_set LabelTag → Prop ≝ |
---|
96 | | clbs_ret : ∀l,PR,tl,toch. |
---|
97 | successors (lookup_present … g l PR) = [ ] → |
---|
98 | check_label_bounded_spec g l tl toch toch |
---|
99 | | clbs_checked : ∀l,PR,l',tl,toch. (* this case overlaps with clbs_cost *) |
---|
100 | successors (lookup_present … g l PR) = [l'] → |
---|
101 | ¬ l' ∈ toch → |
---|
102 | l' ≠ l → |
---|
103 | ¬ l' ∈ tl → |
---|
104 | check_label_bounded_spec g l tl toch toch |
---|
105 | | clbs_cost : ∀l,PR,l',PR',tl,toch. |
---|
106 | successors (lookup_present … g l PR) = [l'] → |
---|
107 | is_cost_label (lookup_present … g l' PR') → |
---|
108 | check_label_bounded_spec g l tl toch toch |
---|
109 | | clbs_step : ∀l,PR,l',PR',tl,toch,toch',toch''. |
---|
110 | successors (lookup_present … g l PR) = [l'] → |
---|
111 | (* l' ∈ toch → implied *) |
---|
112 | ¬ l' ∈ tl → |
---|
113 | ¬ is_cost_label (lookup_present … g l' PR') → |
---|
114 | try_remove … toch l' = Some ? 〈it,toch'〉 → |
---|
115 | check_label_bounded_spec g l' (l::tl) toch' toch'' → |
---|
116 | check_label_bounded_spec g l tl toch toch'' |
---|
117 | | clbs_branch : ∀l,PR,x,y,zs,tl,toch. (* the other check will show that these are cost labels *) |
---|
118 | successors (lookup_present … g l PR) = x::y::zs → |
---|
119 | check_label_bounded_spec g l tl toch toch. |
---|
120 | |
---|
121 | |
---|
122 | lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'. |
---|
123 | (∀l. l∈to_check → ¬ memb ? l (checking::checking_tail)) → |
---|
124 | check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' → |
---|
125 | check_label_bounded_spec g checking checking_tail to_check to_check'. |
---|
126 | #n elim n |
---|
127 | [ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *) |
---|
128 | | #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check' #REMOVING |
---|
129 | whd in ⊢ (??%? → ?); |
---|
130 | generalize in ⊢ (??(?%)? → ?); |
---|
131 | lapply (refl ? (successors (lookup_present … PR))) |
---|
132 | cases (successors (lookup_present … PR)) in ⊢ (???% → %); |
---|
133 | [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 // |
---|
134 | | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' @if_elim |
---|
135 | [ #CS #E destruct @(clbs_cost … SUCC) // |
---|
136 | | #NCS generalize in ⊢ (??(?%)? → ?); |
---|
137 | lapply (refl ? (try_remove … to_check h)) |
---|
138 | cases (try_remove ????) in ⊢ (???% → %); |
---|
139 | [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim |
---|
140 | [ #H' #E destruct |
---|
141 | | #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC) |
---|
142 | [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) // |
---|
143 | | % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) * |
---|
144 | | assumption |
---|
145 | ] |
---|
146 | ] |
---|
147 | | * * #to_check'' #RM #H whd in ⊢ (??%? → ?); |
---|
148 | whd in ⊢ (??%? → ?); #H |
---|
149 | cases (try_remove_some ?????? RM) * #L1 #L2 #L3 |
---|
150 | @(clbs_step … SUCC ? NCS RM) |
---|
151 | [ @notb_Prop @(not_to_not … (Prop_notb … (REMOVING h ?))) /2/ |
---|
152 | whd in ⊢ (?%); >L1 // |
---|
153 | | @(IH … H) |
---|
154 | #l #IN'' @notb_Prop % whd in ⊢ (?% → ?); @if_elim |
---|
155 | [ #E #_ whd in IN'':(?%); >(proj1 ?? (eqb_true …) E) in IN''; |
---|
156 | >L2 * |
---|
157 | | #NE lapply (REMOVING l ?) |
---|
158 | [ whd in ⊢ (?%); cases (L3 l) [ #E destruct cases (Prop_notb … NE) #X @⊥ @X @eq_true_to_b @(proj2 ?? (eqb_true …)) % |
---|
159 | | #L >L @IN'' |
---|
160 | ] |
---|
161 | | cases (l∈checking::checking_tail) * * |
---|
162 | ] |
---|
163 | ] |
---|
164 | ] |
---|
165 | ] |
---|
166 | ] |
---|
167 | | #h2 #t #SUCCS whd in ⊢ (? → ??%? → ?); #PR' #E destruct |
---|
168 | @(clbs_branch … SUCCS) |
---|
169 | ] |
---|
170 | ] |
---|
171 | ] qed. |
---|
172 | |
---|
173 | lemma check_label_bounded_c : ∀g,CL,checking,checking_tail,to_check,to_check'. |
---|
174 | check_label_bounded_spec g checking checking_tail to_check to_check' → |
---|
175 | ∀term_check,TERM,PR. |
---|
176 | check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check'. |
---|
177 | #g #CL #X1 #X2 #X3 #X4 #X elim X |
---|
178 | [ #l #PR #tl #toch #SUCC |
---|
179 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
180 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
181 | whd in ⊢ (??%?); % |
---|
182 | | #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl |
---|
183 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
184 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
185 | whd in ⊢ (??%?); @if_elim [ // ] #NCS generalize in ⊢ (??(?%)?); |
---|
186 | cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ // | * * ] ] |
---|
187 | #L >(proj2 … (try_remove_empty …) L) #H2 |
---|
188 | whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl) |
---|
189 | % |
---|
190 | | #l #PR #l' #PR' #tl #toch #SUCC #CS |
---|
191 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
192 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
193 | whd in ⊢ (??%?); >CS whd in ⊢ (??%?); % |
---|
194 | | #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH |
---|
195 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
196 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
197 | whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS)) |
---|
198 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2 |
---|
199 | whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN)) |
---|
200 | whd in ⊢ (??%?); >(IH term_check' ??) % |
---|
201 | | #l #PR #x #y #zs #tl #toch #SUCC |
---|
202 | * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR |
---|
203 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 |
---|
204 | whd in ⊢ (??%?); % |
---|
205 | ] qed. |
---|
206 | |
---|
207 | lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'. |
---|
208 | check_label_bounded_spec g checking checking_tail to_check to_check' → |
---|
209 | set_subset … to_check' to_check. |
---|
210 | #g #lX #lX' #tX #tX' #S elim S // |
---|
211 | #l #PR #l' #PR' #tl #toch #toch' #toch'' #SC #NI #CS #RM #H #IH |
---|
212 | cases (try_remove_some … toch' RM) * #L1 #L2 #L3 |
---|
213 | #id #IN cases (L3 id) |
---|
214 | [ #E destruct whd in ⊢ (?%); >L1 // |
---|
215 | | #L4 whd in ⊢ (?%); >L4 @IH @IN |
---|
216 | ] qed. |
---|
217 | |
---|
218 | lemma bound_on_instrs_to_cost_prime : ∀g,l,n. |
---|
219 | bound_on_instrs_to_cost g l n → |
---|
220 | bound_on_instrs_to_cost' g l n. |
---|
221 | #g #l #n #H inversion H |
---|
222 | #l' #n' #PR #H' #E1 #E2 #_ destruct |
---|
223 | lapply (refl ? (is_cost_label (lookup_present … g l' PR))) |
---|
224 | cases (is_cost_label ?) in ⊢ (???% → ?); #CS |
---|
225 | [ @boitc_here [ @PR | @eq_true_to_b @CS ] |
---|
226 | | @boitc_later [ @PR | @eq_false_to_notb @CS | @H ] |
---|
227 | ] qed. |
---|
228 | |
---|
229 | lemma successors_inv : ∀st,x,y,zs. |
---|
230 | successors st = x::y::zs → |
---|
231 | ∃r,l1,l2. st = St_cond r l1 l2. |
---|
232 | * normalize |
---|
233 | #a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l destruct |
---|
234 | /4/ |
---|
235 | qed. |
---|
236 | |
---|
237 | include alias "utilities/deqsets_extra.ma". |
---|
238 | |
---|
239 | lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g. |
---|
240 | (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → |
---|
241 | ∀l,PR,x,y,zs. successors (lookup_present … g l PR) = x::y::zs → |
---|
242 | ∀l'. ∀IN : l' ∈ successors (lookup_present … g l PR). |
---|
243 | is_cost_label (lookup_present … g l' ?). |
---|
244 | [2: @(successors_present … IN) @(CL l) @lookup_lookup_present ] |
---|
245 | #g #CL #WCL #l #PR #x #y #zs #SUCCS |
---|
246 | cases (successors_inv … SUCCS) |
---|
247 | #r * #l1 * #l2 #E |
---|
248 | #l' #IN generalize in ⊢ (?(?(?????%))); #OR' >E in IN; |
---|
249 | lapply (WCL l PR) generalize in ⊢ (?(???%) → ?); >E in ⊢ (% → % → ?); #LP #WCst |
---|
250 | cases (andb_Prop_true ?? WCst) |
---|
251 | #H1 #H2 |
---|
252 | whd in ⊢ (?% → ?); @eqb_elim |
---|
253 | [ 2: #_ #IN lapply (memb_single … IN) ] |
---|
254 | #E destruct // |
---|
255 | qed. |
---|
256 | |
---|
257 | (* Show that when we remove labels from to_check we do actually find a bound |
---|
258 | (if it exists). We need two extra facts: everything is "well" labelled, |
---|
259 | so that we know that branches are followed by labels and we don't need to |
---|
260 | follow them; and anything in the graph that isn't mentioned has already been |
---|
261 | successfully checked. *) |
---|
262 | |
---|
263 | lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'. |
---|
264 | ∀CL:graph_closed g. |
---|
265 | (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → |
---|
266 | check_label_bounded_spec g checking checking_tail to_check to_check' → |
---|
267 | (∀l. l∈g → ¬l ∈ to_check → l≠checking → ¬l∈checking_tail → ∃n. bound_on_instrs_to_cost g l n) → |
---|
268 | ∀l. l = checking ∨ bool_to_Prop (l∈to_check) → |
---|
269 | bool_to_Prop (l∈to_check') ∨ ∃n. bound_on_instrs_to_cost g l n. |
---|
270 | #g #X1 #X2 #X3 #X4 #CL #WCL #X elim X |
---|
271 | [ #l #PR #tl #toch #SUCC #INV #l' * |
---|
272 | [ #E destruct %2 %{1} % [ @PR | >SUCC #l' * ] |
---|
273 | | #IN %1 @IN |
---|
274 | ] |
---|
275 | | #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl #INV #l'' * |
---|
276 | [ #E destruct %2 |
---|
277 | cases (INV l' ????) |
---|
278 | [ #n #B |
---|
279 | %{(S n)} % [ @PR | >SUCC #l'' * [2: *] #E destruct /2/ ] |
---|
280 | | @present_member @(successors_present … (CL l ? (lookup_lookup_present … PR))) |
---|
281 | >SUCC @eq_true_to_b @memb_hd |
---|
282 | | assumption |
---|
283 | | assumption |
---|
284 | | assumption |
---|
285 | ] |
---|
286 | | #IN %1 assumption |
---|
287 | ] |
---|
288 | | #l #PR #l' #PR' #tl #toch #SUCC #CS #INV #l'' * |
---|
289 | [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ] |
---|
290 | | /2/ |
---|
291 | ] |
---|
292 | | #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN_tl #NCS #RM #H #IH #INV #l'' * |
---|
293 | [ #E destruct %2 cases (IH ? l' ?) |
---|
294 | [ #IN @⊥ lapply (check_label_bounded_subset … H l' IN) #IN' |
---|
295 | cases (try_remove_some ?????? RM) * #_ #L #_ whd in IN':(?%); |
---|
296 | cases (lookup ????) in IN' L; [ * | * #_ #E destruct ] |
---|
297 | | * #n #B %{(S n)} % [ // | #l'' >SUCC * [2: *] #E destruct /2/ ] |
---|
298 | | #l'' #INg #INch' #NEQ #NIN_ltl @(INV l'' INg ???) |
---|
299 | [ @notb_Prop % #INch @(absurd ?? (Prop_notb … INch')) |
---|
300 | cases (try_remove_some ?????? RM) * #_ #_ #L |
---|
301 | cases (L l'') [ #E destruct cases NEQ #X cases (X (refl ??)) ] |
---|
302 | #L' whd in ⊢ (?%); <L' @INch |
---|
303 | | % #E destruct cases (Prop_notb … NIN_ltl) #X @X @eq_true_to_b @memb_hd |
---|
304 | | @notb_Prop @(not_to_not … (Prop_notb … NIN_ltl)) #IN @eq_true_to_b @memb_cons @IN |
---|
305 | ] |
---|
306 | | %1 % |
---|
307 | ] |
---|
308 | | #IN @(IH ? l'' ?) |
---|
309 | [ #l''' #INg #NINch' #NEQ #NINtl @INV |
---|
310 | [ assumption |
---|
311 | | @notb_Prop @(not_to_not … (Prop_notb … NINch')) |
---|
312 | cases (try_remove_some ?????? RM) * #L1 #L2 #L3 |
---|
313 | cases (L3 l''') |
---|
314 | [ #E destruct @⊥ cases NEQ /2/ |
---|
315 | | #L whd in ⊢ (?% → ?%); >L // |
---|
316 | ] |
---|
317 | | % #E destruct cases (Prop_notb … NINtl) #X @X @eq_true_to_b @memb_hd |
---|
318 | | @notb_Prop @(not_to_not … (Prop_notb … NINtl)) #IN @eq_true_to_b @memb_cons @IN |
---|
319 | ] |
---|
320 | | cases (try_remove_some ?????? RM) * #L1 #L2 #L3 |
---|
321 | cases (L3 l'') [ #E destruct %1 % | #L %2 whd in ⊢ (?%); <L @IN ] |
---|
322 | ] |
---|
323 | ] |
---|
324 | | #l #PR #x #y #zs #tl #toch #SUCCS #INV #l' * |
---|
325 | [ #E destruct %2 %{1} % [ // ] |
---|
326 | #l' #EX @boitc_here |
---|
327 | [ @(successors_present … (CL l ? (lookup_lookup_present … PR))) |
---|
328 | @Exists_memb @EX |
---|
329 | | @(after_branch_are_cost_labels … WCL … SUCCS) |
---|
330 | ] |
---|
331 | | /2/ |
---|
332 | ] |
---|
333 | ] qed. |
---|
334 | |
---|
335 | |
---|
336 | (* When we reject a label it is because we found a loop without a cost label |
---|
337 | when we followed its successors. We need the invariant that only the |
---|
338 | initial label can be a cost label, and have two cases in the result: either |
---|
339 | we found the entire loop and return that, or we haven't come back out of the |
---|
340 | recursive calls to find the head again, so return part of the loop. *) |
---|
341 | |
---|
342 | lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM. |
---|
343 | (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) → |
---|
344 | check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? → |
---|
345 | ∃head,PR'. bool_to_Prop (¬ is_cost_label (lookup_present … g head PR')) ∧ |
---|
346 | ((∃l. Exists ? (λl'.l'=l) (successors (lookup_present … g head PR')) ∧ |
---|
347 | bad_label_list g head l) ∨ |
---|
348 | (bool_to_Prop (head ∈ checking_tail) ∧ bad_label_list g head checking)). |
---|
349 | #g #CL #term_check elim term_check |
---|
350 | [ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct |
---|
351 | | #term_check' #IH |
---|
352 | #checking #PR #checking_tail #to_check #TERM #PRECS |
---|
353 | whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); lapply (refl ? (successors (lookup_present … PR))) |
---|
354 | cases (successors ?) in ⊢ (???% → %); |
---|
355 | [ #H #H' whd in ⊢ (??%? → ?); #E destruct ] |
---|
356 | #h * [2: #y #zs #H #H' whd in ⊢ (??%? → ?); #E destruct ] |
---|
357 | #SUCC #PR' whd in ⊢ (??%? → ?); @if_elim |
---|
358 | [ #CS #E destruct ] #NCS generalize in ⊢ (??(?%)? → ?); |
---|
359 | cases (try_remove ????) |
---|
360 | [ #H whd in ⊢ (??%? → ?); @if_elim |
---|
361 | (* base case - we've found the head of the list *) |
---|
362 | [ #IN #_ cases (orb_Prop_true … IN) |
---|
363 | [ (* self-loop *) #E >(proj1 ?? (eqb_true …) E) in SUCC PR' NCS; #SUCC #PR' #NCS %{checking} %{PR} |
---|
364 | %{NCS} %1 %{checking} % [ >SUCC % % | // ] |
---|
365 | | #IN' %{h} % [ @PR' @eq_true_to_b @memb_hd ] %{NCS} %2 %{IN'} |
---|
366 | @(gl_step … (gl_end …)) |
---|
367 | [ @PR |
---|
368 | | >SUCC @eq_true_to_b @memb_hd |
---|
369 | | cases (orb_Prop_true … IN) |
---|
370 | [ #E <(proj1 ?? (eqb_true …) E) in PR ⊢ %; // |
---|
371 | | cases checking_tail in PRECS ⊢ %; |
---|
372 | [ #_ * | #h' #t #H #_ @H % #E destruct ] |
---|
373 | ] |
---|
374 | ] |
---|
375 | ] |
---|
376 | | #_ #E destruct |
---|
377 | ] |
---|
378 | | * * #to_check' #H1 whd in ⊢ (??%? → ?); |
---|
379 | #CHECK' cases (IH … CHECK') |
---|
380 | [ #head * #PRhead * #NCShead * |
---|
381 | [ #BLL %{head} %{PRhead} % /2/ |
---|
382 | | * whd in ⊢ (?% → ?); @if_elim |
---|
383 | [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead NCShead ⊢ %; #PRh #NCSh #BLL %{checking} %{PRh} %{NCSh} |
---|
384 | %1 %{h} >SUCC % [ % % | @BLL ] |
---|
385 | | #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % // |
---|
386 | @(gl_step … BLL) |
---|
387 | [ @PR |
---|
388 | | >SUCC @eq_true_to_b @memb_hd |
---|
389 | | cases checking_tail in PRECS INtl; |
---|
390 | [ #_ * |
---|
391 | | #h #t #H #_ @H % #E destruct |
---|
392 | ] |
---|
393 | ] |
---|
394 | ] |
---|
395 | ] |
---|
396 | | #_ // |
---|
397 | ] |
---|
398 | ] |
---|
399 | ] qed. |
---|
400 | |
---|
401 | |
---|
402 | (* Now keep checking as long as there's some instruction we haven't checked. *) |
---|
403 | |
---|
404 | let rec check_graph_bounded |
---|
405 | (g : graph statement) |
---|
406 | (CL : graph_closed g) |
---|
407 | (to_check : identifier_set LabelTag) |
---|
408 | (SUB : set_subset … to_check g) |
---|
409 | (start : label) |
---|
410 | (PR : present ?? g start) |
---|
411 | (REMOVED : notb (member ?? to_check start)) |
---|
412 | (SMALLER : gt (id_map_size … g) (id_map_size … to_check)) |
---|
413 | (term_check : nat) |
---|
414 | on term_check : gt term_check (id_map_size … to_check) → bool ≝ |
---|
415 | match term_check return λx. ge x ? → bool with |
---|
416 | [ O ⇒ λH.⊥ |
---|
417 | | S term_check' ⇒ λH. |
---|
418 | let TERM' ≝ ? in |
---|
419 | match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with |
---|
420 | [ None ⇒ λ_. false |
---|
421 | | Some to_check' ⇒ λH'. |
---|
422 | match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with |
---|
423 | [ None ⇒ λ_.λ_.λ_. true |
---|
424 | | Some l_to_check'' ⇒ λL,SUB',C. |
---|
425 | check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ??? term_check' ? |
---|
426 | ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check') |
---|
427 | ] (refl ??) |
---|
428 | ]. |
---|
429 | [ 2,3,4,5,6: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB' |
---|
430 | lapply (check_label_bounded_subset … (check_label_bounded_s … H')) |
---|
431 | [ 1,3,5,7,9: #l' #IN @notb_Prop % #IS >(memb_single … IS) in IN; #IN' |
---|
432 | @(absurd … IN' (Prop_notb … REMOVED)) ] |
---|
433 | #SUB'' |
---|
434 | ] |
---|
435 | [ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN |
---|
436 | | @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L // |
---|
437 | | cases (L … (refl ??)) * #L1 #L2 #L3 whd in ⊢ (?(?%)); >L2 // |
---|
438 | | whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/ |
---|
439 | | whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/ |
---|
440 | | /2/ |
---|
441 | | @SMALLER |
---|
442 | ] qed. |
---|
443 | |
---|
444 | lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM. |
---|
445 | (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → |
---|
446 | check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = true → |
---|
447 | (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) → |
---|
448 | ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n. |
---|
449 | #g #CL #term_check elim term_check |
---|
450 | [ #to_check #SUB #start #PR #REMOVED #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct |
---|
451 | | #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM #WCL |
---|
452 | whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); |
---|
453 | cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?); |
---|
454 | [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ] |
---|
455 | generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?); |
---|
456 | lapply (choose_empty … to_check') |
---|
457 | cases (choose LabelTag unit to_check') |
---|
458 | [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN |
---|
459 | cases (true_or_false_Prop (l∈to_check ∨ l == start)) |
---|
460 | [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?) |
---|
461 | [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; * |
---|
462 | | // |
---|
463 | | // |
---|
464 | | @WCL |
---|
465 | | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN' |
---|
466 | >(memb_single … IN') in IN; // |
---|
467 | | #l' #IN_g #NIN_to_check #NEQ #_ @H // |
---|
468 | | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E |
---|
469 | ] |
---|
470 | | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ] |
---|
471 | ] |
---|
472 | | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); |
---|
473 | #CHECK #H @(IH … CHECK) |
---|
474 | [ @WCL |
---|
475 | | #l #INg #NIN'' #NEQ |
---|
476 | cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN'')) |
---|
477 | cases (H4 … (refl ??)) * #L1 #L2 #L3 |
---|
478 | cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ] |
---|
479 | #NIN' |
---|
480 | cases (true_or_false_Prop (l∈to_check ∨ l == start)) |
---|
481 | [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?) |
---|
482 | [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN')) |
---|
483 | | // |
---|
484 | | // |
---|
485 | | @WCL |
---|
486 | | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN' |
---|
487 | >(memb_single … IN') in IN; // |
---|
488 | | #l' #IN_g #NIN_to_check #NEQ #_ @H // |
---|
489 | | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E |
---|
490 | ] |
---|
491 | | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ] |
---|
492 | ] |
---|
493 | ] |
---|
494 | ] |
---|
495 | ] qed. |
---|
496 | |
---|
497 | (* The check_label_bounded_bad result gives us the loop, so we can use the |
---|
498 | loop_soundness_contradiction result to show that there's no bound for the |
---|
499 | head of the loop. *) |
---|
500 | |
---|
501 | lemma check_graph_bounded_bad : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM. |
---|
502 | check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = false → |
---|
503 | ∃l. present ?? g l ∧ ∀n. ¬ bound_on_instrs_to_cost g l n. |
---|
504 | #g #CL #term_check elim term_check |
---|
505 | [ #a #b #c #d #e #f #TERM @⊥ inversion TERM #A try #B try #C try #D destruct |
---|
506 | | #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM |
---|
507 | whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); |
---|
508 | cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?); |
---|
509 | [ #CHECK_LABEL whd in ⊢ (??%? → ?); #_ |
---|
510 | cases (check_label_bounded_bad … CHECK_LABEL) |
---|
511 | [ #head * #PR_head * #NCS_head * |
---|
512 | [ * #next * #NEXT #BLL |
---|
513 | %{head} %{PR_head} #n % #BOUND |
---|
514 | cases (bound_step1 … BOUND … NEXT) #m #BOUND' |
---|
515 | @(absurd ? BOUND' (loop_soundness_contradiction … NEXT NCS_head BLL m)) |
---|
516 | | * * |
---|
517 | ] |
---|
518 | | * #H cases (H (refl ??)) |
---|
519 | ] |
---|
520 | | #to_check' #CHECK_LABEL whd in ⊢ (??%? → ?); |
---|
521 | generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?); |
---|
522 | cases (choose LabelTag unit to_check') |
---|
523 | [ #H1 #H2 #H3 whd in ⊢ (??%? → ?); #E destruct |
---|
524 | | * * #next * #to_check'' #H2 #H3 #H4 whd in ⊢ (??%? → ?); |
---|
525 | @IH |
---|
526 | ] |
---|
527 | ] |
---|
528 | ] qed. |
---|
529 | |
---|
530 | |
---|
531 | definition check_sound_cost_fn : internal_function → bool ≝ |
---|
532 | λfn. |
---|
533 | match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with |
---|
534 | [ None ⇒ λEMP. ⊥ |
---|
535 | | Some to_check ⇒ λ_.λCARD,L. |
---|
536 | check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ??? (|f_graph fn|) ? |
---|
537 | ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn))) |
---|
538 | (try_remove_some_card ????) |
---|
539 | (try_remove_some ????). |
---|
540 | [ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H |
---|
541 | @PR' @H % |
---|
542 | | cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN |
---|
543 | cases (L3 id) |
---|
544 | [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/ |
---|
545 | | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) * |
---|
546 | whd in match (present ????); whd in match (present ? unit ??); |
---|
547 | lapply (member_present … IN) whd in match (present ? unit ??); <E |
---|
548 | cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/ |
---|
549 | ] |
---|
550 | | cases (f_entry fn) // |
---|
551 | | cases to_check in L ⊢ %; * #to_check0 #L cases (L … (refl ??)) * #L1 #L2 #L3 |
---|
552 | whd in ⊢ (?(?%)); >L2 // |
---|
553 | | 5,6: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) // |
---|
554 | ] qed. |
---|
555 | |
---|
556 | lemma check_sound_cost_fn_ok : ∀fn. |
---|
557 | well_cost_labelled_fn fn → |
---|
558 | bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn. |
---|
559 | #fn #WCL % |
---|
560 | [ whd in ⊢ (?% → %); |
---|
561 | generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?); |
---|
562 | cases (try_remove ????) |
---|
563 | [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E |
---|
564 | lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?); |
---|
565 | >(E (refl ??)) * /3/ |
---|
566 | | * * #to_check #H1 #H2 #H3 |
---|
567 | whd in ⊢ (?% → ?); #CHECK |
---|
568 | #l #PR @(check_graph_bounded_ok … CHECK) |
---|
569 | [ #l' #PR' cases WCL // |
---|
570 | | #l' #IN #NIN #NEQ @⊥ |
---|
571 | cases (H1 … (refl ??)) * #L1 #L2 #L3 |
---|
572 | @(absurd ?? (Prop_notb … NIN)) |
---|
573 | cases (L3 l') |
---|
574 | [ #E >E in NEQ; * #H cases (H (refl ??)) |
---|
575 | | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …)) |
---|
576 | @member_present @IN |
---|
577 | ] |
---|
578 | | /2/ |
---|
579 | ] |
---|
580 | ] |
---|
581 | | whd in ⊢ (% → %); #SOUND |
---|
582 | lapply (refl ? (check_sound_cost_fn fn)) |
---|
583 | cases (check_sound_cost_fn fn) in ⊢ (???% → %); |
---|
584 | [ // |
---|
585 | | whd in ⊢ (??%? → %); |
---|
586 | generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?); |
---|
587 | cases (try_remove ????) |
---|
588 | [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E |
---|
589 | lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?); |
---|
590 | >(E (refl ??)) * /3/ |
---|
591 | | * * #to_check #H1 #H2 #H3 |
---|
592 | whd in ⊢ (??%? → ?); #CHECK |
---|
593 | lapply (check_graph_bounded_bad … CHECK) -CHECK -H1 -H2 -H3 |
---|
594 | * #l * #PR #NOT cases (SOUND l PR) #n #B |
---|
595 | @(absurd ? B) @NOT |
---|
596 | ] |
---|
597 | ] |
---|
598 | ] qed. |
---|
599 | |
---|
600 | |
---|
601 | definition check_cost_program : RTLabs_program → bool ≝ |
---|
602 | λp. all ? (λfn. match \snd fn with |
---|
603 | [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn |
---|
604 | | External _ ⇒ true |
---|
605 | ]) (prog_funct … p). |
---|
606 | |
---|
607 | theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p. |
---|
608 | #p whd in ⊢ (?(?%)%); % |
---|
609 | [ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp |
---|
610 | * #id * #fd |
---|
611 | [ #H cases (andb_Prop_true … H) #W #S |
---|
612 | lapply (proj1 … (check_well_cost_fn_ok …) W) #W' |
---|
613 | % |
---|
614 | [ // |
---|
615 | | @(proj1 … (check_sound_cost_fn_ok …)) // |
---|
616 | ] |
---|
617 | | // |
---|
618 | ] |
---|
619 | | #H @(proj2 … (all_All …)) @(All_mp … H) |
---|
620 | * #id * #fd |
---|
621 | [ * #W #S |
---|
622 | lapply ((proj2 … (check_well_cost_fn_ok …)) W) |
---|
623 | lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/ |
---|
624 | | // |
---|
625 | ] |
---|
626 | ] qed. |
---|
627 | |
---|
628 | |
---|
629 | definition check_cost_program_prf : ∀p:RTLabs_program. res (well_cost_labelled_program p) ≝ |
---|
630 | λp. (match check_cost_program p return λb. bool_to_Prop b ↔ well_cost_labelled_program p → res ? with |
---|
631 | [ true ⇒ λH. OK ?? |
---|
632 | | false ⇒ λ_. Error ? (msg BadCostLabelling) |
---|
633 | ]) |
---|
634 | (check_cost_program_ok p). |
---|
635 | @(proj1 … H) |
---|
636 | % qed. |
---|
637 | |
---|