source: src/RTLabs/CostCheck.ma @ 2486

Last change on this file since 2486 was 2315, checked in by campbell, 8 years ago

Add some more commentary.
File size: 27.1 KB
Line 
1
2include "RTLabs/CostSpec.ma".
3include "utilities/bool.ma".
4include "utilities/listb.ma".
5include "RTLabs/CostMisc.ma".
6
7definition 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) ?).
11cases (f_entry f) //
12qed.
13
14lemma 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
27include alias "utilities/deqsets.ma".
28
29lemma 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
47include 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. *)
53let 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)
61on term_check : gt term_check (id_map_size … to_check) → option (identifier_set LabelTag) ≝
62let stop_now ≝ Some ? to_check in
63match 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
95inductive 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
122lemma 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
173lemma 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
207lemma 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
212cases (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
218lemma 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
223lapply (refl ? (is_cost_label (lookup_present … g l' PR)))
224cases (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
229lemma 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/
235qed.
236
237include alias "utilities/deqsets.ma".
238
239lemma 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
246cases (successors_inv … SUCCS)
247#r * #l1 * #l2 #E
248#l' #IN generalize in ⊢ (?(?(?????%))); #OR' >E in IN;
249lapply (WCL l PR) generalize in ⊢ (?(???%) → ?); >E in ⊢ (% → % → ?); #LP #WCst
250cases (andb_Prop_true ?? WCst)
251#H1 #H2
252whd in ⊢ (?% → ?); @eqb_elim
253[ 2: #_ #IN lapply (memb_single … IN) ]
254#E destruct //
255qed.
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
263lemma 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
342lemma 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
404let 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)
414on term_check : gt term_check (id_map_size … to_check) → bool ≝
415match 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
444lemma 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
501lemma 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 
531definition 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
556lemma 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
601definition 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
607theorem 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
Note: See TracBrowser for help on using the repository browser.