source: src/RTLabs/CostCheck.ma @ 2313

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

RTLabs cost checker correct.

File size: 28.2 KB
Line 
1
2include "RTLabs/CostSpec.ma".
3
4(* TODO: move ----→ *)
5
6lemma 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 ] ]
10qed.
11
12let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝
13match l with
14[ nil ⇒ true
15| cons h t ⇒ P h ∧ all A P t
16].
17
18lemma 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
29definition 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) ?).
33cases (f_entry f) //
34qed.
35
36lemma 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
49include "basics/lists/listb.ma".
50include alias "utilities/deqsets.ma".
51
52lemma 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
70include 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. *)
76let 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)
84on term_check : gt term_check (id_map_size … to_check) → option (identifier_set LabelTag) ≝
85let stop_now ≝ Some ? to_check in
86match 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      let PR' ≝ ? in
97      let st' ≝ lookup_present … g h PR' in
98      if is_cost_label st' then stop_now else
99      match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with
100      [ Some to_check' ⇒ λH'.
101          check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
102      | None ⇒ λ_.
103          if h == checking ∨ h ∈ checking_tail then None ? else
104            stop_now (* already checked successor *)
105      ] (try_remove_some_card … to_check h)
106    | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *)
107    ]
108  ] (successors_present g st (CL … checking … (lookup_lookup_present …)))
109].
110[ /2 by absurd/
111| lapply (H' (\fst to_check') (\snd to_check') ?) [ cases to_check' // ]
112  #E -PR' >E in H; #H' /2/
113| @SC >memb_hd //
114] qed.
115
116(* An inductive specification of the above function that's easier to work with. *)
117
118inductive check_label_bounded_spec (g:graph statement) : label → list label → identifier_set LabelTag → identifier_set LabelTag → Prop ≝
119| clbs_ret : ∀l,PR,tl,toch.
120    successors (lookup_present … g l PR) = [ ] →
121    check_label_bounded_spec g l tl toch toch
122| clbs_checked : ∀l,PR,l',tl,toch. (* this case overlaps with clbs_cost *)
123    successors (lookup_present … g l PR) = [l'] →
124    ¬ l' ∈ toch →
125    l' ≠ l →
126    ¬ l' ∈ tl →
127    check_label_bounded_spec g l tl toch toch
128| clbs_cost : ∀l,PR,l',PR',tl,toch.
129    successors (lookup_present … g l PR) = [l'] →
130    is_cost_label (lookup_present … g l' PR') →
131    check_label_bounded_spec g l tl toch toch
132| clbs_step : ∀l,PR,l',PR',tl,toch,toch',toch''.
133    successors (lookup_present … g l PR) = [l'] →
134(*    l' ∈ toch → implied *)
135    ¬ l' ∈ tl →
136    ¬ is_cost_label (lookup_present … g l' PR') →
137    try_remove … toch l' = Some ? 〈it,toch'〉 →
138    check_label_bounded_spec g l' (l::tl) toch' toch'' →
139    check_label_bounded_spec g l tl toch toch''
140| clbs_branch : ∀l,PR,x,y,zs,tl,toch.  (* the other check will show that these are cost labels *)
141    successors (lookup_present … g l PR) = x::y::zs →
142    check_label_bounded_spec g l tl toch toch.
143
144(* TODO: move (or is it somewhere already?) *)
145lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0].
146  (b → P e1) →
147  (¬b → P e2) →
148  P (if b then e1 else e2).
149#T * /2/
150qed.
151
152lemma not_orb : ∀b,c:bool.
153  ¬ (b∨c) →
154  (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)).
155* * normalize /2/
156qed.
157
158lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
159  (∀l. l∈to_check → ¬ l∈checking::checking_tail) →
160  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
161  check_label_bounded_spec g checking checking_tail to_check to_check'.
162#n elim n
163[ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *)
164| #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check' #REMOVING
165  whd in ⊢ (??%? → ?);
166  generalize in ⊢ (??(?%)? → ?);
167  lapply (refl ? (successors (lookup_present … PR)))
168  cases (successors (lookup_present … PR)) in ⊢ (???% → %);
169  [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 //
170  | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' @if_elim
171           [ #CS #E destruct @(clbs_cost … SUCC) //
172           | #NCS generalize in ⊢ (??(?%)? → ?);
173             lapply (refl ? (try_remove … to_check h))
174             cases (try_remove ????) in ⊢ (???% → %);
175             [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim
176               [ #H' #E destruct
177               | #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC)
178                 [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
179                 | % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) *
180                 | assumption
181                 ]
182               ]
183             | * * #to_check'' #RM #H whd in ⊢ (??%? → ?);
184               whd in ⊢ (??%? → ?); #H
185               cases (try_remove_some ?????? RM) * #L1 #L2 #L3
186               @(clbs_step … SUCC ? NCS RM)
187               [ @notb_Prop @(not_to_not … (Prop_notb … (REMOVING h ?))) /2/
188                 whd in ⊢ (?%); >L1 //
189               | @(IH … H)
190                 #l #IN'' @notb_Prop % whd in ⊢ (?% → ?); @if_elim
191                 [ #E #_ whd in IN'':(?%); >(proj1 ?? (eqb_true …) E) in IN'';
192                   >L2 *
193                 | #NE lapply (REMOVING l ?)
194                   [ whd in ⊢ (?%); cases (L3 l) [ #E destruct cases (Prop_notb … NE) #X @⊥ @X @eq_true_to_b @(proj2 ?? (eqb_true …)) %
195                     | #L >L @IN''
196                     ]
197                   | cases (l∈checking::checking_tail) * *
198                   ]
199                 ]
200               ]
201             ]
202           ]
203         | #h2 #t #SUCCS whd in ⊢ (? → ??%? → ?); #PR' #E destruct
204           @(clbs_branch … SUCCS)
205         ]
206  ]
207] qed.
208
209lemma check_label_bounded_c : ∀g,CL,checking,checking_tail,to_check,to_check'.
210  check_label_bounded_spec g checking checking_tail to_check to_check' →
211  ∀term_check,TERM,PR.
212  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check'.
213#g #CL #X1 #X2 #X3 #X4 #X elim X
214[ #l #PR #tl #toch #SUCC
215  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
216  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
217  whd in ⊢ (??%?); %
218| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl
219  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
220  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
221  whd in ⊢ (??%?); @if_elim [ // ] #NCS generalize in ⊢ (??(?%)?);
222  cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ // | * * ] ]
223  #L >(proj2 … (try_remove_empty …) L) #H2
224  whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl)
225  %
226| #l #PR #l' #PR' #tl #toch #SUCC #CS
227  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
228  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
229  whd in ⊢ (??%?);  >CS whd in ⊢ (??%?); %
230| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH
231  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
232  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
233  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS))
234  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2
235  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN))
236  whd in ⊢ (??%?); >(IH term_check' ??) %
237| #l #PR #x #y #zs #tl #toch #SUCC
238  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
239  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
240  whd in ⊢ (??%?); %
241] qed.
242
243lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'.
244  check_label_bounded_spec g checking checking_tail to_check to_check' →
245  set_subset … to_check' to_check.
246#g #lX #lX' #tX #tX' #S elim S //
247#l #PR #l' #PR' #tl #toch #toch' #toch'' #SC #NI #CS #RM #H #IH
248cases (try_remove_some … toch' RM) * #L1 #L2 #L3
249#id #IN cases (L3 id)
250[ #E destruct whd in ⊢ (?%); >L1 //
251| #L4 whd in ⊢ (?%); >L4 @IH @IN
252] qed.
253
254lemma bound_on_instrs_to_cost_prime : ∀g,l,n.
255  bound_on_instrs_to_cost g l n →
256  bound_on_instrs_to_cost' g l n.
257#g #l #n #H inversion H
258#l' #n' #PR #H' #E1 #E2 #_ destruct
259lapply (refl ? (is_cost_label (lookup_present … g l' PR)))
260cases (is_cost_label ?) in ⊢ (???% → ?); #CS
261[ @boitc_here [ @PR | @eq_true_to_b @CS ]
262| @boitc_later [ @PR | @eq_false_to_notb @CS | @H ]
263] qed.
264
265lemma present_member : ∀tag,A,m,id.
266  present tag A m id → member tag A m id.
267#tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??))
268qed.
269
270(* TODO: move and eliminate dup in Traces.ma *)
271lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
272  Exists S (λy. y = x) l →
273  x ∈ l.
274#S #x #l elim l
275[ //
276| #h #t #IH
277  normalize lapply (eqb_true … x h)
278  cases (x==h) *
279  [ #E #_ >(E (refl ??)) //
280  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
281            | #H @IH @H
282            ]
283  ]
284] qed.
285
286lemma successors_inv : ∀st,x,y,zs.
287  successors st = x::y::zs →
288  ∃r,l1,l2. st = St_cond r l1 l2.
289* normalize
290#a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l destruct
291/4/
292qed.
293
294include alias "utilities/deqsets.ma".
295
296lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g.
297  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
298  ∀l,PR,x,y,zs. successors (lookup_present … g l PR) = x::y::zs →
299  ∀l'. ∀IN : l' ∈ successors (lookup_present … g l PR).
300  is_cost_label (lookup_present … g l' ?).
301[2: @(successors_present … IN) @(CL l) @lookup_lookup_present ]
302#g #CL #WCL #l #PR #x #y #zs #SUCCS
303cases (successors_inv … SUCCS)
304#r * #l1 * #l2 #E
305#l' #IN generalize in ⊢ (?(?(?????%))); #OR' >E in IN;
306lapply (WCL l PR) generalize in ⊢ (?(???%) → ?); >E in ⊢ (% → % → ?); #LP #WCst
307cases (andb_Prop_true ?? WCst)
308#H1 #H2
309whd in ⊢ (?% → ?); @eqb_elim
310[ 2: #_ #IN lapply (memb_single … IN) ]
311#E destruct //
312qed.
313
314
315lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'.
316  ∀CL:graph_closed g.
317  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
318  check_label_bounded_spec g checking checking_tail to_check to_check' →
319  (∀l. l∈g → ¬l ∈ to_check → l≠checking → ¬l∈checking_tail → ∃n. bound_on_instrs_to_cost g l n) →
320  ∀l. l = checking ∨ bool_to_Prop (l∈to_check) →
321  bool_to_Prop (l∈to_check') ∨ ∃n. bound_on_instrs_to_cost g l n.
322#g #X1 #X2 #X3 #X4 #CL #WCL #X elim X
323[ #l #PR #tl #toch #SUCC #INV #l' *
324  [ #E destruct %2 %{1} % [ @PR | >SUCC #l' * ]
325  | #IN %1 @IN
326  ]
327| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl #INV #l'' *
328  [ #E destruct %2
329    cases (INV l' ????)
330    [ #n #B
331      %{(S n)} % [ @PR | >SUCC #l'' * [2: *] #E destruct /2/ ]
332    | @present_member @(successors_present … (CL l ? (lookup_lookup_present … PR)))
333      >SUCC @eq_true_to_b @memb_hd
334    | assumption
335    | assumption
336    | assumption
337    ]
338  | #IN %1 assumption
339  ]
340| #l #PR #l' #PR' #tl #toch #SUCC #CS #INV #l'' *
341  [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ]
342  | /2/
343  ]
344| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN_tl #NCS #RM #H #IH #INV #l'' *
345  [ #E destruct %2 cases (IH ? l' ?)
346    [ #IN @⊥ lapply (check_label_bounded_subset … H l' IN) #IN'
347      cases (try_remove_some ?????? RM) * #_ #L #_ whd in IN':(?%);
348      cases (lookup ????) in IN' L; [ * | * #_ #E destruct ]
349    | * #n #B %{(S n)} % [ // | #l'' >SUCC * [2: *] #E destruct /2/ ]
350    | #l'' #INg #INch' #NEQ #NIN_ltl @(INV l'' INg ???)
351      [ @notb_Prop % #INch @(absurd ?? (Prop_notb … INch'))
352        cases (try_remove_some ?????? RM) * #_ #_ #L
353        cases (L l'') [ #E destruct cases NEQ #X cases (X (refl ??)) ]
354        #L' whd in ⊢ (?%); <L' @INch
355      | % #E destruct cases (Prop_notb … NIN_ltl) #X @X @eq_true_to_b @memb_hd
356      | @notb_Prop @(not_to_not … (Prop_notb … NIN_ltl)) #IN @eq_true_to_b @memb_cons @IN
357      ]
358    | %1 %
359    ]
360  | #IN @(IH ? l'' ?)
361    [ #l''' #INg #NINch' #NEQ #NINtl @INV
362      [ assumption
363      | @notb_Prop @(not_to_not … (Prop_notb … NINch'))
364        cases (try_remove_some ?????? RM) * #L1 #L2 #L3
365        cases (L3 l''')
366        [ #E destruct @⊥ cases NEQ /2/
367        | #L whd in ⊢ (?% → ?%); >L //
368        ]
369      | % #E destruct cases (Prop_notb … NINtl) #X @X @eq_true_to_b @memb_hd
370      | @notb_Prop @(not_to_not … (Prop_notb … NINtl)) #IN @eq_true_to_b @memb_cons @IN
371      ]
372    | cases (try_remove_some ?????? RM) * #L1 #L2 #L3
373      cases (L3 l'') [ #E destruct %1 % | #L %2 whd in ⊢ (?%); <L @IN ]
374    ]
375  ]
376| #l #PR #x #y #zs #tl #toch #SUCCS #INV #l' *
377  [ #E destruct %2 %{1} % [ // ]
378    #l' #EX @boitc_here
379    [ @(successors_present … (CL l ? (lookup_lookup_present … PR)))
380      @Exists_memb @EX
381    | @(after_branch_are_cost_labels … WCL … SUCCS)
382    ]
383  | /2/
384  ]
385] qed.
386
387include "RTLabs/CostMisc.ma".
388
389lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM.
390  (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) →
391  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? →
392  ∃head,PR'. bool_to_Prop (¬ is_cost_label (lookup_present … g head PR')) ∧
393  ((∃l. Exists ? (λl'.l'=l) (successors (lookup_present … g head PR')) ∧
394       bad_label_list g head l) ∨
395   (bool_to_Prop (head ∈ checking_tail) ∧ bad_label_list g head checking)).
396#g #CL #term_check elim term_check
397[ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct
398| #term_check' #IH
399  #checking #PR #checking_tail #to_check #TERM #PRECS
400  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); lapply (refl ? (successors (lookup_present … PR)))
401  cases (successors ?) in ⊢ (???% → %);
402  [ #H #H' whd in ⊢ (??%? → ?); #E destruct ]
403  #h * [2: #y #zs #H #H' whd in ⊢ (??%? → ?); #E destruct ]
404  #SUCC #PR' whd in ⊢ (??%? → ?); @if_elim
405  [ #CS #E destruct ] #NCS generalize in ⊢ (??(?%)? → ?);
406  cases (try_remove ????)
407  [ #H whd in ⊢ (??%? → ?); @if_elim
408    (* base case - we've found the head of the list *)
409    [ #IN #_ cases (orb_Prop_true … IN)
410      [ (* self-loop *) #E >(proj1 ?? (eqb_true …) E) in SUCC PR' NCS; #SUCC #PR' #NCS %{checking} %{PR}
411        %{NCS} %1 %{checking} % [ >SUCC % % | // ]
412      | #IN' %{h} % [ @PR' @eq_true_to_b @memb_hd ] %{NCS} %2 %{IN'}
413        @(gl_step … (gl_end …))
414        [ @PR
415        | >SUCC @eq_true_to_b @memb_hd
416        | cases (orb_Prop_true … IN)
417          [ #E <(proj1 ?? (eqb_true …) E) in PR ⊢ %; //
418          | cases checking_tail in PRECS ⊢ %;
419            [ #_ * | #h' #t #H #_ @H % #E destruct ]
420          ]
421        ]
422      ]
423    | #_ #E destruct
424    ]
425  | * * #to_check' #H1 whd in ⊢ (??%? → ?);
426    #CHECK' cases (IH … CHECK')
427    [ #head * #PRhead * #NCShead *
428      [ #BLL %{head} %{PRhead} % /2/
429      | * whd in ⊢ (?% → ?); @if_elim
430        [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead NCShead ⊢ %; #PRh #NCSh #BLL %{checking} %{PRh} %{NCSh}
431          %1 %{h} >SUCC % [ % % | @BLL ]
432        | #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % //
433          @(gl_step … BLL)
434          [ @PR
435          | >SUCC @eq_true_to_b @memb_hd
436          | cases checking_tail in PRECS INtl;
437            [ #_ *
438            | #h #t #H #_ @H % #E destruct
439            ]
440          ]
441        ]
442      ]
443    | #_ //
444    ]
445  ]
446] qed.
447     
448
449
450
451let rec check_graph_bounded
452  (g : graph statement)
453  (CL : graph_closed g)
454  (to_check : identifier_set LabelTag)
455  (SUB : set_subset … to_check g)
456  (start : label)
457  (PR : present ?? g start)
458  (REMOVED : notb (member ?? to_check start))
459  (SMALLER : gt (id_map_size … g) (id_map_size … to_check))
460  (term_check : nat)
461on term_check : gt term_check (id_map_size … to_check) → bool ≝
462match term_check return λx. ge x ? → bool with
463[ O ⇒ λH.⊥
464| S term_check' ⇒ λH.
465  let TERM' ≝ ? in
466  match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with
467  [ None ⇒ λ_. false
468  | Some to_check' ⇒ λH'.
469    match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with
470    [ None ⇒ λ_.λ_.λ_. true
471    | Some l_to_check'' ⇒ λL,SUB',C.
472        check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ??? term_check' ?
473    ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check')
474  ] (refl ??)
475].
476[ 2,3,4,5,6: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB'
477  lapply (check_label_bounded_subset … (check_label_bounded_s … H'))
478  [ 1,3,5,7,9: #l' #IN @notb_Prop % #IS >(memb_single … IS) in IN; #IN'
479    @(absurd … IN' (Prop_notb … REMOVED)) ]
480   #SUB''
481]
482[ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN
483| @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L //
484| cases (L … (refl ??)) * #L1 #L2 #L3 whd in ⊢ (?(?%)); >L2 //
485| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
486| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
487| /2/
488| @SMALLER
489] qed.
490
491lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
492  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
493  check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = true →
494  (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) →
495  ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n.
496#g #CL #term_check elim term_check
497[ #to_check #SUB #start #PR #REMOVED #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
498| #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM #WCL
499  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
500  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
501  [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ]
502  generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
503  lapply (choose_empty … to_check')
504  cases (choose LabelTag unit to_check')
505  [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN
506    cases (true_or_false_Prop (l∈to_check ∨ l == start))
507    [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
508      [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; *
509      | //
510      | //
511      | @WCL
512      | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
513        >(memb_single … IN') in IN; //
514      | #l' #IN_g #NIN_to_check #NEQ #_ @H //
515      | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
516      ]
517    | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
518    ]
519 | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
520   #CHECK #H @(IH … CHECK)
521   [ @WCL
522   | #l #INg #NIN'' #NEQ
523     cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN''))
524                          cases (H4 … (refl ??)) * #L1 #L2 #L3
525                          cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ]
526     #NIN'
527      cases (true_or_false_Prop (l∈to_check ∨ l == start))
528      [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
529        [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN'))
530        | //
531        | //
532        | @WCL
533        | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
534          >(memb_single … IN') in IN; //
535        | #l' #IN_g #NIN_to_check #NEQ #_ @H //
536        | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
537        ]
538      | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
539      ]
540   ]
541 ]
542] qed.
543
544lemma check_graph_bounded_bad : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
545  check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = false →
546  ∃l. present ?? g l ∧ ∀n. ¬ bound_on_instrs_to_cost g l n.
547#g #CL #term_check elim term_check
548[ #a #b #c #d #e #f #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
549| #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM
550  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
551  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
552  [ #CHECK_LABEL whd in ⊢ (??%? → ?); #_
553    cases (check_label_bounded_bad … CHECK_LABEL)
554    [ #head * #PR_head * #NCS_head *
555      [ * #next * #NEXT #BLL
556        %{head} %{PR_head} #n % #BOUND
557        cases (bound_step1 … BOUND … NEXT) #m #BOUND'
558        @(absurd ? BOUND' (loop_soundness_contradiction … NEXT NCS_head BLL m))
559      | * *
560      ]
561    | * #H cases (H (refl ??))
562    ]
563  | #to_check' #CHECK_LABEL whd in ⊢ (??%? → ?);
564    generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
565    cases (choose LabelTag unit to_check')
566    [ #H1 #H2 #H3 whd in ⊢ (??%? → ?); #E destruct
567    | * * #next * #to_check'' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
568      @IH
569    ]
570  ]
571] qed.
572
573 
574(* TODO: move *)
575definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
576λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
577
578lemma id_set_of_map_subset : ∀tag,A,m.
579  id_set_of_map tag A m ⊆ m.
580#tag #A * #m * #id normalize
581>lookup_opt_map normalize cases (lookup_opt ???) //
582qed.
583
584lemma id_set_of_map_present : ∀tag,A,m,id.
585  present tag A m id ↔ present tag unit (id_set_of_map … m) id.
586#tag #A * #m * #id %
587normalize @not_to_not
588>lookup_opt_map cases (lookup_opt ???) normalize //
589#a #E destruct
590qed.
591
592lemma id_set_of_map_card : ∀tag,A,m.
593  |m| = |id_set_of_map tag A m|.
594#tag #A * #m whd in ⊢ (??%%); >map_size //
595qed.
596
597definition check_sound_cost_fn : internal_function → bool ≝
598λfn.
599  match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with
600  [ None ⇒ λEMP. ⊥
601  | Some to_check ⇒ λ_.λCARD,L.
602              check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ??? (|f_graph fn|) ?
603  ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn)))
604    (try_remove_some_card ????)
605    (try_remove_some ????).
606[ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H
607  @PR' @H %
608| cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN
609  cases (L3 id)
610  [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/
611  | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) *
612    whd in match (present ????); whd in match (present ? unit ??);
613    lapply (member_present … IN) whd in match (present ? unit ??); <E
614    cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/
615  ]
616| cases (f_entry fn) //
617| cases to_check in L ⊢ %; * #to_check0 #L cases (L … (refl ??)) * #L1 #L2 #L3
618  whd in ⊢ (?(?%)); >L2 //
619| 5,6: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) //
620] qed.
621
622lemma check_sound_cost_fn_ok : ∀fn.
623  well_cost_labelled_fn fn →
624  bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
625#fn #WCL %
626[ whd in ⊢ (?% → %);
627  generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?);
628  cases (try_remove ????)
629  [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
630    lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
631    >(E (refl ??)) * /3/
632  | * * #to_check #H1 #H2 #H3
633    whd in ⊢ (?% → ?); #CHECK
634    #l #PR @(check_graph_bounded_ok … CHECK)
635    [ #l' #PR' cases WCL //
636    | #l' #IN #NIN #NEQ @⊥
637      cases (H1 … (refl ??)) * #L1 #L2 #L3
638      @(absurd ?? (Prop_notb … NIN))
639      cases (L3 l')
640      [ #E >E in NEQ; * #H cases (H (refl ??))
641      | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …))
642        @member_present @IN
643      ]
644    | /2/
645    ]
646  ]
647| whd in ⊢ (% → %); #SOUND
648  lapply (refl ? (check_sound_cost_fn fn))
649  cases (check_sound_cost_fn fn) in ⊢ (???% → %);
650  [ //
651  | whd in ⊢ (??%? → %);
652    generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
653    cases (try_remove ????)
654    [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
655      lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
656      >(E (refl ??)) * /3/
657    | * * #to_check #H1 #H2 #H3
658      whd in ⊢ (??%? → ?); #CHECK
659      lapply (check_graph_bounded_bad … CHECK) -CHECK -H1 -H2 -H3
660      * #l * #PR #NOT cases (SOUND l PR) #n #B
661      @(absurd ? B) @NOT
662    ]
663  ]
664] qed.
665
666
667definition check_cost_program : RTLabs_program → bool ≝
668λp. all ? (λfn. match \snd fn with
669                 [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn
670                 | External _ ⇒ true
671                 ]) (prog_funct … p).
672
673theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p.
674#p whd in ⊢ (?(?%)%); %
675[ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp
676  * #id * #fd
677  [ #H cases (andb_Prop_true … H) #W #S
678    lapply (proj1 … (check_well_cost_fn_ok …) W) #W'
679    %
680    [ //
681    | @(proj1 … (check_sound_cost_fn_ok …)) //
682    ]
683  | //
684  ]
685| #H @(proj2 … (all_All …)) @(All_mp … H)
686  * #id * #fd
687  [ * #W #S
688    lapply ((proj2 … (check_well_cost_fn_ok …)) W)
689    lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/
690  | //
691  ]
692] qed.
693
Note: See TracBrowser for help on using the repository browser.