source: src/RTLabs/CostCheck.ma @ 2308

Last change on this file since 2308 was 2308, checked in by campbell, 7 years ago

More proof (and corrections) on cost checking.

File size: 26.6 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
387(* TODO: share with Traces.ma. *)
388inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝
389| gl_end : bad_label_list g head head
390| gl_step : ∀l1,l2,H.
391    l2 ∈ successors (lookup_present … g l1 H) →
392    ¬ is_cost_label (lookup_present … g l1 H) →
393    bad_label_list g head l2 →
394    bad_label_list g head l1.
395(*
396inductive checked_label_costs (g:graph statement) : list label → label → Prop ≝
397| clc_start : ∀l. checked_label_costs g [ ] l
398| clc_two : ∀l,H,l'. ¬ is_cost_label (lookup_present … g l H) → checked_label_costs g [l'] l
399| clc_many : ∀h,t,l,H. ¬ is_cost_label (lookup_present … g h H) → checked_label_costs g t l → checked_label_costs g (h::t) l.
400*)
401lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM.
402  (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) →
403  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? →
404  ∃head,PR'. bool_to_Prop (¬ is_cost_label (lookup_present … g head PR')) ∧
405  (bad_label_list g head head ∨
406   (bool_to_Prop (head ∈ checking::checking_tail) ∧ bad_label_list g head checking)).
407#g #CL #term_check elim term_check
408[ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct
409| #term_check' #IH
410  #checking #PR #checking_tail #to_check #TERM #PRECS
411  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); lapply (refl ? (successors (lookup_present … PR)))
412  cases (successors ?) in ⊢ (???% → %);
413  [ #H #H' whd in ⊢ (??%? → ?); #E destruct ]
414  #h * [2: #y #zs #H #H' whd in ⊢ (??%? → ?); #E destruct ]
415  #SUCC #PR' whd in ⊢ (??%? → ?); @if_elim
416  [ #CS #E destruct ] #NCS generalize in ⊢ (??(?%)? → ?);
417  cases (try_remove ????)
418  [ #H whd in ⊢ (??%? → ?); @if_elim
419      (* base case - we've found the head of the list *)
420    [ #IN #_ %{h} % [ @PR' @eq_true_to_b @memb_hd ] % [ @NCS ] %2 %
421      [ cases (orb_Prop_true … IN) /2/
422      | @(gl_step … (gl_end …))
423        [ @PR
424        | >SUCC @eq_true_to_b @memb_hd
425        | cases (orb_Prop_true … IN)
426          [ #E <(proj1 ?? (eqb_true …) E) in PR ⊢ %; //
427          | cases checking_tail in PRECS ⊢ %;
428            [ #_ * | #h' #t #H #_ @H % #E destruct ]
429          ]
430        ]
431      ]
432    | #_ #E destruct
433    ]
434  | * * #to_check' #H1 whd in ⊢ (??%? → ?);
435    #CHECK' cases (IH … CHECK')
436    [ #head * #PRhead * #NCShead *
437      [ #BLL %{head} %{PRhead} % /2/
438      | * whd in ⊢ (?% → ?); @if_elim
439        [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead ⊢ %; #PRh #BLL %{h} %{PRh} %{NCS} %1 @BLL
440        | #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % //
441          @(gl_step … BLL)
442          [ @PR
443          | >SUCC @eq_true_to_b @memb_hd
444          | cases checking_tail in PRECS INtl;
445            [ #_ #INc <(memb_single … INc) in PR ⊢ %; //
446            | #h #t #H #_ @H % #E destruct
447            ]
448          ]
449        ]
450      ]
451    | #_ //
452    ]
453  ]
454] qed.
455     
456
457
458
459let rec check_graph_bounded
460  (g : graph statement)
461  (CL : graph_closed g)
462  (to_check : identifier_set LabelTag)
463  (SUB : set_subset … to_check g)
464  (start : label)
465  (PR : present ?? g start)
466  (REMOVED : notb (member ?? to_check start))
467  (SMALLER : gt (id_map_size … g) (id_map_size … to_check))
468  (term_check : nat)
469on term_check : gt term_check (id_map_size … to_check) → bool ≝
470match term_check return λx. ge x ? → bool with
471[ O ⇒ λH.⊥
472| S term_check' ⇒ λH.
473  let TERM' ≝ ? in
474  match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with
475  [ None ⇒ λ_. false
476  | Some to_check' ⇒ λH'.
477    match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with
478    [ None ⇒ λ_.λ_.λ_. true
479    | Some l_to_check'' ⇒ λL,SUB',C.
480        check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ??? term_check' ?
481    ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check')
482  ] (refl ??)
483].
484[ 2,3,4,5,6: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB'
485  lapply (check_label_bounded_subset … (check_label_bounded_s … H'))
486  [ 1,3,5,7,9: #l' #IN @notb_Prop % #IS >(memb_single … IS) in IN; #IN'
487    @(absurd … IN' (Prop_notb … REMOVED)) ]
488   #SUB''
489]
490[ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN
491| @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L //
492| cases (L … (refl ??)) * #L1 #L2 #L3 whd in ⊢ (?(?%)); >L2 //
493| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
494| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
495| /2/
496| @SMALLER
497] qed.
498
499lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
500  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
501  check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = true →
502  (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) →
503  ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n.
504#g #CL #term_check elim term_check
505[ #to_check #SUB #start #PR #REMOVED #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
506| #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM #WCL
507  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
508  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
509  [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ]
510  generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
511  lapply (choose_empty … to_check')
512  cases (choose LabelTag unit to_check')
513  [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN
514    cases (true_or_false_Prop (l∈to_check ∨ l == start))
515    [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
516      [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; *
517      | //
518      | //
519      | @WCL
520      | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
521        >(memb_single … IN') in IN; //
522      | #l' #IN_g #NIN_to_check #NEQ #_ @H //
523      | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
524      ]
525    | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
526    ]
527 | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
528   #CHECK #H @(IH … CHECK)
529   [ @WCL
530   | #l #INg #NIN'' #NEQ
531     cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN''))
532                          cases (H4 … (refl ??)) * #L1 #L2 #L3
533                          cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ]
534     #NIN'
535      cases (true_or_false_Prop (l∈to_check ∨ l == start))
536      [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
537        [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN'))
538        | //
539        | //
540        | @WCL
541        | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
542          >(memb_single … IN') in IN; //
543        | #l' #IN_g #NIN_to_check #NEQ #_ @H //
544        | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
545        ]
546      | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
547      ]
548   ]
549 ]
550] qed.
551
552(* TODO: move *)
553definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
554λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
555
556lemma id_set_of_map_subset : ∀tag,A,m.
557  id_set_of_map tag A m ⊆ m.
558#tag #A * #m * #id normalize
559>lookup_opt_map normalize cases (lookup_opt ???) //
560qed.
561
562lemma id_set_of_map_present : ∀tag,A,m,id.
563  present tag A m id ↔ present tag unit (id_set_of_map … m) id.
564#tag #A * #m * #id %
565normalize @not_to_not
566>lookup_opt_map cases (lookup_opt ???) normalize //
567#a #E destruct
568qed.
569
570lemma id_set_of_map_card : ∀tag,A,m.
571  |m| = |id_set_of_map tag A m|.
572#tag #A * #m whd in ⊢ (??%%); >map_size //
573qed.
574
575definition check_sound_cost_fn : internal_function → bool ≝
576λfn.
577  match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with
578  [ None ⇒ λEMP. ⊥
579  | Some to_check ⇒ λ_.λCARD,L.
580              check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ??? (|f_graph fn|) ?
581  ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn)))
582    (try_remove_some_card ????)
583    (try_remove_some ????).
584[ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H
585  @PR' @H %
586| cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN
587  cases (L3 id)
588  [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/
589  | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) *
590    whd in match (present ????); whd in match (present ? unit ??);
591    lapply (member_present … IN) whd in match (present ? unit ??); <E
592    cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/
593  ]
594| cases (f_entry fn) //
595| cases to_check in L ⊢ %; * #to_check0 #L cases (L … (refl ??)) * #L1 #L2 #L3
596  whd in ⊢ (?(?%)); >L2 //
597| 5,6: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) //
598] qed.
599
600axiom check_sound_cost_fn_ok : ∀fn.
601  well_cost_labelled_fn fn →
602  bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
603(*
604#fn #WCL %
605[ whd in ⊢ (?% → %);
606  generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?);
607  cases (try_remove ????)
608  [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
609    lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
610    >(E (refl ??)) * /3/
611  | * * #to_check #H1 #H2 #H3
612    whd in ⊢ (?% → ?); #CHECK
613    #l #PR @(check_graph_bounded_ok … CHECK)
614    [ #l' #PR' cases WCL //
615    | #l' #IN #NIN #NEQ @⊥
616      cases (H1 … (refl ??)) * #L1 #L2 #L3
617      @(absurd ?? (Prop_notb … NIN))
618      cases (L3 l')
619      [ #E >E in NEQ; * #H cases (H (refl ??))
620      | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …))
621        @member_present @IN
622      ]
623    | /2/
624    ]
625  ]
626| TODO
627*)
628
629definition check_cost_program : RTLabs_program → bool ≝
630λp. all ? (λfn. match \snd fn with
631                 [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn
632                 | External _ ⇒ true
633                 ]) (prog_funct … p).
634
635theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p.
636#p whd in ⊢ (?(?%)%); %
637[ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp
638  * #id * #fd
639  [ #H cases (andb_Prop_true … H) #W #S
640    lapply (proj1 … (check_well_cost_fn_ok …) W) #W'
641    %
642    [ //
643    | @(proj1 … (check_sound_cost_fn_ok …)) //
644    ]
645  | //
646  ]
647| #H @(proj2 … (all_All …)) @(All_mp … H)
648  * #id * #fd
649  [ * #W #S
650    lapply ((proj2 … (check_well_cost_fn_ok …)) W)
651    lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/
652  | //
653  ]
654] qed.
655
Note: See TracBrowser for help on using the repository browser.