source: src/RTLabs/CostCheck.ma @ 2314

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

Move generic definitions from recent commit to appropriate places.

File size: 26.2 KB
Line 
1
2include "RTLabs/CostSpec.ma".
3include "utilities/bool.ma".
4include "utilities/listb.ma".
5
6definition check_well_cost_fn : internal_function → bool ≝
7λf.
8  idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement (f_graph f) s (f_closed f l s PR)) ∧
9  is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
10cases (f_entry f) //
11qed.
12
13lemma check_well_cost_fn_ok : ∀fn. bool_to_Prop (check_well_cost_fn fn) ↔ well_cost_labelled_fn fn.
14#fn %
15[ #H cases (andb_Prop_true … H) #ST #EN
16  % [ lapply (proj1 … (idmap_all_ok …) ST) // | @EN ]
17| * #ST #EN @andb_Prop
18  [ @(proj2 … (idmap_all_ok …)) #l #st #L
19    cut (present ?? (f_graph fn) l) [ whd >L % #E destruct ] #PR
20    lapply (ST l PR) generalize in ⊢ (?(???%) → ?);
21    >(lookup_present_eq ????? L PR) //
22  | @eq_true_to_b @EN
23  ]
24] qed.
25
26include alias "utilities/deqsets.ma".
27
28lemma successors_present : ∀g,st.
29  labels_present g st →
30  ∀l. l ∈ successors st →
31  present ?? g l.
32#g *
33[ #l1 #PR #l2 #IN >(memb_single … IN) @PR
34| #cs #l1 #PR #l2 #IN >(memb_single … IN) @PR
35| #ty #r #c #l1 #PR #l2 #IN >(memb_single … IN) @PR
36| #ty1 #ty2 #op #r1 #r2  #l1 #PR #l2 #IN >(memb_single … IN) @PR
37| #ty1 #ty2 #ty3 #op #r1 #r2 #r3 #l1 #PR #l2 #IN >(memb_single … IN) @PR
38| #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR
39| #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR
40| #id #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR
41| #r #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR
42| #r #l1 #l2 * #PR1 #PR2 #l3 whd in ⊢ (?% → ?); @eqb_elim [ // | #_ #IN >(memb_single … IN) // ]
43| #_ #l *
44] qed.
45
46include alias "common/Identifiers.ma".
47
48(* Check that from [checking] we reach a cost label without going through
49   [checking_tail], which would form a loop in the CFG.  We also have a set of
50   labels that we have still [to_check], and return an updated set of labels
51   to check if the check for the current label is successful. *)
52let rec check_label_bounded
53  (g : graph statement)
54  (CL : graph_closed g)
55  (checking : label)
56  (PR : present ?? g checking)
57  (checking_tail : list label)
58  (to_check : identifier_set LabelTag)
59  (term_check : nat)
60on term_check : gt term_check (id_map_size … to_check) → option (identifier_set LabelTag) ≝
61let stop_now ≝ Some ? to_check in
62match term_check return λx. ge x ? → ? with
63[ O ⇒ λH.⊥
64| S term_check' ⇒ λH.
65  let st ≝ lookup_present … g checking PR in
66  let succs ≝ successors st in
67  match succs return λsc. (∀l.l∈sc → ?) → ? with
68  [ nil ⇒ λ_. stop_now
69  | cons h t ⇒
70    match t with
71    [ nil ⇒ λSC. (* single successor *)
72      let PR' ≝ ? in
73      let st' ≝ lookup_present … g h PR' in
74      if is_cost_label st' then stop_now else
75      match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with
76      [ Some to_check' ⇒ λH'.
77          check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
78      | None ⇒ λ_.
79          if h == checking ∨ h ∈ checking_tail then None ? else
80            stop_now (* already checked successor *)
81      ] (try_remove_some_card … to_check h)
82    | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *)
83    ]
84  ] (successors_present g st (CL … checking … (lookup_lookup_present …)))
85].
86[ /2 by absurd/
87| lapply (H' (\fst to_check') (\snd to_check') ?) [ cases to_check' // ]
88  #E -PR' >E in H; #H' /2/
89| @SC >memb_hd //
90] qed.
91
92(* An inductive specification of the above function that's easier to work with. *)
93
94inductive check_label_bounded_spec (g:graph statement) : label → list label → identifier_set LabelTag → identifier_set LabelTag → Prop ≝
95| clbs_ret : ∀l,PR,tl,toch.
96    successors (lookup_present … g l PR) = [ ] →
97    check_label_bounded_spec g l tl toch toch
98| clbs_checked : ∀l,PR,l',tl,toch. (* this case overlaps with clbs_cost *)
99    successors (lookup_present … g l PR) = [l'] →
100    ¬ l' ∈ toch →
101    l' ≠ l →
102    ¬ l' ∈ tl →
103    check_label_bounded_spec g l tl toch toch
104| clbs_cost : ∀l,PR,l',PR',tl,toch.
105    successors (lookup_present … g l PR) = [l'] →
106    is_cost_label (lookup_present … g l' PR') →
107    check_label_bounded_spec g l tl toch toch
108| clbs_step : ∀l,PR,l',PR',tl,toch,toch',toch''.
109    successors (lookup_present … g l PR) = [l'] →
110(*    l' ∈ toch → implied *)
111    ¬ l' ∈ tl →
112    ¬ is_cost_label (lookup_present … g l' PR') →
113    try_remove … toch l' = Some ? 〈it,toch'〉 →
114    check_label_bounded_spec g l' (l::tl) toch' toch'' →
115    check_label_bounded_spec g l tl toch toch''
116| clbs_branch : ∀l,PR,x,y,zs,tl,toch.  (* the other check will show that these are cost labels *)
117    successors (lookup_present … g l PR) = x::y::zs →
118    check_label_bounded_spec g l tl toch toch.
119
120(* TODO: move (or is it somewhere already?) *)
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
258lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'.
259  ∀CL:graph_closed g.
260  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
261  check_label_bounded_spec g checking checking_tail to_check to_check' →
262  (∀l. l∈g → ¬l ∈ to_check → l≠checking → ¬l∈checking_tail → ∃n. bound_on_instrs_to_cost g l n) →
263  ∀l. l = checking ∨ bool_to_Prop (l∈to_check) →
264  bool_to_Prop (l∈to_check') ∨ ∃n. bound_on_instrs_to_cost g l n.
265#g #X1 #X2 #X3 #X4 #CL #WCL #X elim X
266[ #l #PR #tl #toch #SUCC #INV #l' *
267  [ #E destruct %2 %{1} % [ @PR | >SUCC #l' * ]
268  | #IN %1 @IN
269  ]
270| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl #INV #l'' *
271  [ #E destruct %2
272    cases (INV l' ????)
273    [ #n #B
274      %{(S n)} % [ @PR | >SUCC #l'' * [2: *] #E destruct /2/ ]
275    | @present_member @(successors_present … (CL l ? (lookup_lookup_present … PR)))
276      >SUCC @eq_true_to_b @memb_hd
277    | assumption
278    | assumption
279    | assumption
280    ]
281  | #IN %1 assumption
282  ]
283| #l #PR #l' #PR' #tl #toch #SUCC #CS #INV #l'' *
284  [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ]
285  | /2/
286  ]
287| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN_tl #NCS #RM #H #IH #INV #l'' *
288  [ #E destruct %2 cases (IH ? l' ?)
289    [ #IN @⊥ lapply (check_label_bounded_subset … H l' IN) #IN'
290      cases (try_remove_some ?????? RM) * #_ #L #_ whd in IN':(?%);
291      cases (lookup ????) in IN' L; [ * | * #_ #E destruct ]
292    | * #n #B %{(S n)} % [ // | #l'' >SUCC * [2: *] #E destruct /2/ ]
293    | #l'' #INg #INch' #NEQ #NIN_ltl @(INV l'' INg ???)
294      [ @notb_Prop % #INch @(absurd ?? (Prop_notb … INch'))
295        cases (try_remove_some ?????? RM) * #_ #_ #L
296        cases (L l'') [ #E destruct cases NEQ #X cases (X (refl ??)) ]
297        #L' whd in ⊢ (?%); <L' @INch
298      | % #E destruct cases (Prop_notb … NIN_ltl) #X @X @eq_true_to_b @memb_hd
299      | @notb_Prop @(not_to_not … (Prop_notb … NIN_ltl)) #IN @eq_true_to_b @memb_cons @IN
300      ]
301    | %1 %
302    ]
303  | #IN @(IH ? l'' ?)
304    [ #l''' #INg #NINch' #NEQ #NINtl @INV
305      [ assumption
306      | @notb_Prop @(not_to_not … (Prop_notb … NINch'))
307        cases (try_remove_some ?????? RM) * #L1 #L2 #L3
308        cases (L3 l''')
309        [ #E destruct @⊥ cases NEQ /2/
310        | #L whd in ⊢ (?% → ?%); >L //
311        ]
312      | % #E destruct cases (Prop_notb … NINtl) #X @X @eq_true_to_b @memb_hd
313      | @notb_Prop @(not_to_not … (Prop_notb … NINtl)) #IN @eq_true_to_b @memb_cons @IN
314      ]
315    | cases (try_remove_some ?????? RM) * #L1 #L2 #L3
316      cases (L3 l'') [ #E destruct %1 % | #L %2 whd in ⊢ (?%); <L @IN ]
317    ]
318  ]
319| #l #PR #x #y #zs #tl #toch #SUCCS #INV #l' *
320  [ #E destruct %2 %{1} % [ // ]
321    #l' #EX @boitc_here
322    [ @(successors_present … (CL l ? (lookup_lookup_present … PR)))
323      @Exists_memb @EX
324    | @(after_branch_are_cost_labels … WCL … SUCCS)
325    ]
326  | /2/
327  ]
328] qed.
329
330include "RTLabs/CostMisc.ma".
331
332lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM.
333  (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) →
334  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? →
335  ∃head,PR'. bool_to_Prop (¬ is_cost_label (lookup_present … g head PR')) ∧
336  ((∃l. Exists ? (λl'.l'=l) (successors (lookup_present … g head PR')) ∧
337       bad_label_list g head l) ∨
338   (bool_to_Prop (head ∈ checking_tail) ∧ bad_label_list g head checking)).
339#g #CL #term_check elim term_check
340[ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct
341| #term_check' #IH
342  #checking #PR #checking_tail #to_check #TERM #PRECS
343  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); lapply (refl ? (successors (lookup_present … PR)))
344  cases (successors ?) in ⊢ (???% → %);
345  [ #H #H' whd in ⊢ (??%? → ?); #E destruct ]
346  #h * [2: #y #zs #H #H' whd in ⊢ (??%? → ?); #E destruct ]
347  #SUCC #PR' whd in ⊢ (??%? → ?); @if_elim
348  [ #CS #E destruct ] #NCS generalize in ⊢ (??(?%)? → ?);
349  cases (try_remove ????)
350  [ #H whd in ⊢ (??%? → ?); @if_elim
351    (* base case - we've found the head of the list *)
352    [ #IN #_ cases (orb_Prop_true … IN)
353      [ (* self-loop *) #E >(proj1 ?? (eqb_true …) E) in SUCC PR' NCS; #SUCC #PR' #NCS %{checking} %{PR}
354        %{NCS} %1 %{checking} % [ >SUCC % % | // ]
355      | #IN' %{h} % [ @PR' @eq_true_to_b @memb_hd ] %{NCS} %2 %{IN'}
356        @(gl_step … (gl_end …))
357        [ @PR
358        | >SUCC @eq_true_to_b @memb_hd
359        | cases (orb_Prop_true … IN)
360          [ #E <(proj1 ?? (eqb_true …) E) in PR ⊢ %; //
361          | cases checking_tail in PRECS ⊢ %;
362            [ #_ * | #h' #t #H #_ @H % #E destruct ]
363          ]
364        ]
365      ]
366    | #_ #E destruct
367    ]
368  | * * #to_check' #H1 whd in ⊢ (??%? → ?);
369    #CHECK' cases (IH … CHECK')
370    [ #head * #PRhead * #NCShead *
371      [ #BLL %{head} %{PRhead} % /2/
372      | * whd in ⊢ (?% → ?); @if_elim
373        [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead NCShead ⊢ %; #PRh #NCSh #BLL %{checking} %{PRh} %{NCSh}
374          %1 %{h} >SUCC % [ % % | @BLL ]
375        | #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % //
376          @(gl_step … BLL)
377          [ @PR
378          | >SUCC @eq_true_to_b @memb_hd
379          | cases checking_tail in PRECS INtl;
380            [ #_ *
381            | #h #t #H #_ @H % #E destruct
382            ]
383          ]
384        ]
385      ]
386    | #_ //
387    ]
388  ]
389] qed.
390     
391
392
393
394let rec check_graph_bounded
395  (g : graph statement)
396  (CL : graph_closed g)
397  (to_check : identifier_set LabelTag)
398  (SUB : set_subset … to_check g)
399  (start : label)
400  (PR : present ?? g start)
401  (REMOVED : notb (member ?? to_check start))
402  (SMALLER : gt (id_map_size … g) (id_map_size … to_check))
403  (term_check : nat)
404on term_check : gt term_check (id_map_size … to_check) → bool ≝
405match term_check return λx. ge x ? → bool with
406[ O ⇒ λH.⊥
407| S term_check' ⇒ λH.
408  let TERM' ≝ ? in
409  match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with
410  [ None ⇒ λ_. false
411  | Some to_check' ⇒ λH'.
412    match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with
413    [ None ⇒ λ_.λ_.λ_. true
414    | Some l_to_check'' ⇒ λL,SUB',C.
415        check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ??? term_check' ?
416    ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check')
417  ] (refl ??)
418].
419[ 2,3,4,5,6: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB'
420  lapply (check_label_bounded_subset … (check_label_bounded_s … H'))
421  [ 1,3,5,7,9: #l' #IN @notb_Prop % #IS >(memb_single … IS) in IN; #IN'
422    @(absurd … IN' (Prop_notb … REMOVED)) ]
423   #SUB''
424]
425[ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN
426| @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L //
427| cases (L … (refl ??)) * #L1 #L2 #L3 whd in ⊢ (?(?%)); >L2 //
428| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
429| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
430| /2/
431| @SMALLER
432] qed.
433
434lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
435  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
436  check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = true →
437  (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) →
438  ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n.
439#g #CL #term_check elim term_check
440[ #to_check #SUB #start #PR #REMOVED #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
441| #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM #WCL
442  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
443  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
444  [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ]
445  generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
446  lapply (choose_empty … to_check')
447  cases (choose LabelTag unit to_check')
448  [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN
449    cases (true_or_false_Prop (l∈to_check ∨ l == start))
450    [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
451      [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; *
452      | //
453      | //
454      | @WCL
455      | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
456        >(memb_single … IN') in IN; //
457      | #l' #IN_g #NIN_to_check #NEQ #_ @H //
458      | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
459      ]
460    | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
461    ]
462 | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
463   #CHECK #H @(IH … CHECK)
464   [ @WCL
465   | #l #INg #NIN'' #NEQ
466     cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN''))
467                          cases (H4 … (refl ??)) * #L1 #L2 #L3
468                          cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ]
469     #NIN'
470      cases (true_or_false_Prop (l∈to_check ∨ l == start))
471      [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
472        [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN'))
473        | //
474        | //
475        | @WCL
476        | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
477          >(memb_single … IN') in IN; //
478        | #l' #IN_g #NIN_to_check #NEQ #_ @H //
479        | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
480        ]
481      | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
482      ]
483   ]
484 ]
485] qed.
486
487lemma check_graph_bounded_bad : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
488  check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = false →
489  ∃l. present ?? g l ∧ ∀n. ¬ bound_on_instrs_to_cost g l n.
490#g #CL #term_check elim term_check
491[ #a #b #c #d #e #f #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
492| #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM
493  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
494  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
495  [ #CHECK_LABEL whd in ⊢ (??%? → ?); #_
496    cases (check_label_bounded_bad … CHECK_LABEL)
497    [ #head * #PR_head * #NCS_head *
498      [ * #next * #NEXT #BLL
499        %{head} %{PR_head} #n % #BOUND
500        cases (bound_step1 … BOUND … NEXT) #m #BOUND'
501        @(absurd ? BOUND' (loop_soundness_contradiction … NEXT NCS_head BLL m))
502      | * *
503      ]
504    | * #H cases (H (refl ??))
505    ]
506  | #to_check' #CHECK_LABEL whd in ⊢ (??%? → ?);
507    generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
508    cases (choose LabelTag unit to_check')
509    [ #H1 #H2 #H3 whd in ⊢ (??%? → ?); #E destruct
510    | * * #next * #to_check'' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
511      @IH
512    ]
513  ]
514] qed.
515
516 
517definition check_sound_cost_fn : internal_function → bool ≝
518λfn.
519  match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with
520  [ None ⇒ λEMP. ⊥
521  | Some to_check ⇒ λ_.λCARD,L.
522              check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ??? (|f_graph fn|) ?
523  ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn)))
524    (try_remove_some_card ????)
525    (try_remove_some ????).
526[ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H
527  @PR' @H %
528| cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN
529  cases (L3 id)
530  [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/
531  | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) *
532    whd in match (present ????); whd in match (present ? unit ??);
533    lapply (member_present … IN) whd in match (present ? unit ??); <E
534    cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/
535  ]
536| cases (f_entry fn) //
537| cases to_check in L ⊢ %; * #to_check0 #L cases (L … (refl ??)) * #L1 #L2 #L3
538  whd in ⊢ (?(?%)); >L2 //
539| 5,6: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) //
540] qed.
541
542lemma check_sound_cost_fn_ok : ∀fn.
543  well_cost_labelled_fn fn →
544  bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
545#fn #WCL %
546[ whd in ⊢ (?% → %);
547  generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?);
548  cases (try_remove ????)
549  [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
550    lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
551    >(E (refl ??)) * /3/
552  | * * #to_check #H1 #H2 #H3
553    whd in ⊢ (?% → ?); #CHECK
554    #l #PR @(check_graph_bounded_ok … CHECK)
555    [ #l' #PR' cases WCL //
556    | #l' #IN #NIN #NEQ @⊥
557      cases (H1 … (refl ??)) * #L1 #L2 #L3
558      @(absurd ?? (Prop_notb … NIN))
559      cases (L3 l')
560      [ #E >E in NEQ; * #H cases (H (refl ??))
561      | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …))
562        @member_present @IN
563      ]
564    | /2/
565    ]
566  ]
567| whd in ⊢ (% → %); #SOUND
568  lapply (refl ? (check_sound_cost_fn fn))
569  cases (check_sound_cost_fn fn) in ⊢ (???% → %);
570  [ //
571  | whd in ⊢ (??%? → %);
572    generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
573    cases (try_remove ????)
574    [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
575      lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
576      >(E (refl ??)) * /3/
577    | * * #to_check #H1 #H2 #H3
578      whd in ⊢ (??%? → ?); #CHECK
579      lapply (check_graph_bounded_bad … CHECK) -CHECK -H1 -H2 -H3
580      * #l * #PR #NOT cases (SOUND l PR) #n #B
581      @(absurd ? B) @NOT
582    ]
583  ]
584] qed.
585
586
587definition check_cost_program : RTLabs_program → bool ≝
588λp. all ? (λfn. match \snd fn with
589                 [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn
590                 | External _ ⇒ true
591                 ]) (prog_funct … p).
592
593theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p.
594#p whd in ⊢ (?(?%)%); %
595[ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp
596  * #id * #fd
597  [ #H cases (andb_Prop_true … H) #W #S
598    lapply (proj1 … (check_well_cost_fn_ok …) W) #W'
599    %
600    [ //
601    | @(proj1 … (check_sound_cost_fn_ok …)) //
602    ]
603  | //
604  ]
605| #H @(proj2 … (all_All …)) @(All_mp … H)
606  * #id * #fd
607  [ * #W #S
608    lapply ((proj2 … (check_well_cost_fn_ok …)) W)
609    lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/
610  | //
611  ]
612] qed.
613
Note: See TracBrowser for help on using the repository browser.