source: src/RTLabs/CostCheck.ma @ 2305

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

RTLabs cost spec checking function implemented (lacks proof, or much
testing due to a bug elsewhere). Includes some new operations on
PostiveMaps? and identifier_maps/sets.

File size: 11.8 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 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      match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with
97      [ Some to_check' ⇒ λH'.
98        if h ∈ checking_tail then None ? else
99        let PR' ≝ ? in
100        let st' ≝ lookup_present … g h PR' in
101        if is_cost_label st' then stop_now else
102          check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
103      | None ⇒ λ_. stop_now (* already checked successor *)
104      ] (try_remove_some_card … to_check h)
105    | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *)
106    ]
107  ] (successors_present g st (CL … checking … (lookup_lookup_present …)))
108].
109[ /2 by absurd/
110| lapply (H' (\fst to_check') (\snd to_check') ?) [ cases to_check' // ]
111  #E -PR' >E in H; #H' /2/
112| @SC >memb_hd //
113] qed.
114
115(* An inductive specification of the above function that's easier to work with. *)
116
117inductive check_label_bounded_spec (g:graph statement) : label → list label → identifier_set LabelTag → identifier_set LabelTag → Prop ≝
118| clbs_ret : ∀l,PR,tl,toch.
119    successors (lookup_present … g l PR) = [ ] →
120    check_label_bounded_spec g l tl toch toch
121| clbs_checked : ∀l,PR,l',tl,toch.
122    successors (lookup_present … g l PR) = [l'] →
123    ¬ l' ∈ toch →
124    check_label_bounded_spec g l tl toch toch
125| clbs_cost : ∀l,PR,l',PR',tl,toch.
126    successors (lookup_present … g l PR) = [l'] →
127    l' ∈ toch →
128    is_cost_label (lookup_present … g l' PR') →
129    check_label_bounded_spec g l tl toch toch
130| clbs_step : ∀l,PR,l',PR',tl,toch,toch',toch''.
131    successors (lookup_present … g l PR) = [l'] →
132(*    l' ∈ toch → implied *)
133    ¬ l' ∈ tl →
134    ¬ is_cost_label (lookup_present … g l' PR') →
135    try_remove … toch l' = Some ? 〈it,toch'〉 →
136    check_label_bounded_spec g l' (l::tl) toch' toch'' →
137    check_label_bounded_spec g l tl toch toch''
138| clbs_branch : ∀l,PR,x,y,zs,tl,toch.  (* the other check will show that these are cost labels *)
139    successors (lookup_present … g l PR) = x::y::zs →
140    check_label_bounded_spec g l tl toch toch.
141
142(* TODO: move (or is it somewhere already?) *)
143lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0].
144  (b → P e1) →
145  (¬b → P e2) →
146  P (if b then e1 else e2).
147#T * /2/
148qed.
149
150lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
151  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
152  check_label_bounded_spec g checking checking_tail to_check to_check'.
153#n elim n
154[ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *)
155| #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check'
156  whd in ⊢ (??%? → ?);
157  generalize in ⊢ (??(?%)? → ?);
158  lapply (refl ? (successors (lookup_present … PR)))
159  cases (successors (lookup_present … PR)) in ⊢ (???% → %);
160  [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 //
161  | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' generalize in ⊢ (??(?%)? → ?);
162           lapply (refl ? (try_remove … to_check h))
163           cases (try_remove ????) in ⊢ (???% → %);
164           [ #RM whd in ⊢ (? → ??%? → ?); #H #E destruct @(clbs_checked … SUCC)
165             whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
166           | * * #to_check'' #RM #H whd in ⊢ (??%? → ?);
167             @if_elim
168             [ #IN whd in ⊢ (??%? → ?); #E destruct
169             | #OUT whd in ⊢ (??%? → ?);
170               @if_elim
171               [ #CS #E destruct @(clbs_cost … SUCC … CS)
172                 cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L //
173               | #CS #H @(clbs_step … SUCC OUT CS RM) @(IH … H)
174               ]
175             ]
176           ]
177         | #h2 #t #SUCCS whd in ⊢ (? → ??%? → ?); #PR' #E destruct
178           @(clbs_branch … SUCCS)
179         ]
180  ]
181] qed.
182
183
184
185lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'.
186  check_label_bounded_spec g checking checking_tail to_check to_check' →
187  set_subset … to_check' to_check.
188#g #lX #lX' #tX #tX' #S elim S //
189#l #PR #l' #PR' #tl #toch #toch' #toch'' #SC #NI #CS #RM #H #IH
190cases (try_remove_some … toch' RM) * #L1 #L2 #L3
191#id #IN cases (L3 id)
192[ #E destruct whd in ⊢ (?%); >L1 //
193| #L4 whd in ⊢ (?%); >L4 @IH @IN
194] qed.
195
196let rec check_graph_bounded
197  (g : graph statement)
198  (CL : graph_closed g)
199  (to_check : identifier_set LabelTag)
200  (SUB : set_subset … to_check g)
201  (start : label)
202  (PR : present ?? g start)
203  (SMALLER : gt (id_map_size … g) (id_map_size … to_check))
204  (term_check : nat)
205on term_check : gt term_check (id_map_size … to_check) → bool ≝
206match term_check return λx. ge x ? → bool with
207[ O ⇒ λH.⊥
208| S term_check' ⇒ λH.
209  let TERM' ≝ ? in
210  match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with
211  [ None ⇒ λ_. false
212  | Some to_check' ⇒ λH'.
213    match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with
214    [ None ⇒ λ_.λ_.λ_. true
215    | Some l_to_check'' ⇒ λL,SUB',C.
216        check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ?? term_check' ?
217    ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check')
218  ] (refl ??)
219].
220[ 2,3,4,5: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB'
221  lapply (check_label_bounded_subset … (check_label_bounded_s … H')) #SUB''
222]
223[ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN
224| @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L //
225| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
226| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
227| /2/
228| @SMALLER
229] qed.
230
231(* TODO: move *)
232definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
233λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
234
235lemma id_set_of_map_subset : ∀tag,A,m.
236  id_set_of_map tag A m ⊆ m.
237#tag #A * #m * #id normalize
238>lookup_opt_map normalize cases (lookup_opt ???) //
239qed.
240
241lemma id_set_of_map_present : ∀tag,A,m,id.
242  present tag A m id ↔ present tag unit (id_set_of_map … m) id.
243#tag #A * #m * #id %
244normalize @not_to_not
245>lookup_opt_map cases (lookup_opt ???) normalize //
246#a #E destruct
247qed.
248
249lemma id_set_of_map_card : ∀tag,A,m.
250  |m| = |id_set_of_map tag A m|.
251#tag #A * #m whd in ⊢ (??%%); >map_size //
252qed.
253
254definition check_sound_cost_fn : internal_function → bool ≝
255λfn.
256  match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with
257  [ None ⇒ λEMP. ⊥
258  | Some to_check ⇒ λ_.λCARD,L.
259              check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ?? (|f_graph fn|) ?
260  ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn)))
261    (try_remove_some_card ????)
262    (try_remove_some ????).
263[ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H
264  @PR' @H %
265| cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN
266  cases (L3 id)
267  [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/
268  | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) *
269    whd in match (present ????); whd in match (present ? unit ??);
270    lapply (member_present … IN) whd in match (present ? unit ??); <E
271    cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/
272  ]
273| cases (f_entry fn) //
274| 4,5: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) //
275] qed.
276
277axiom check_sound_cost_fn_ok : ∀fn. bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
278
279definition check_cost_program : RTLabs_program → bool ≝
280λp. all ? (λfn. match \snd fn with
281                 [ Internal fn ⇒ check_well_cost_fn fn ∧ check_sound_cost_fn fn
282                 | External _ ⇒ true
283                 ]) (prog_funct … p).
284
285theorem check_cost_program_ok : ∀p. bool_to_Prop (check_cost_program p) ↔ well_cost_labelled_program p.
286#p whd in ⊢ (?(?%)%); %
287[ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp
288  * #id * #fd
289  [ #H cases (andb_Prop_true … H) #W #S %
290    [ @(proj1 … (check_well_cost_fn_ok … )) //
291    | @(proj1 … (check_sound_cost_fn_ok …)) //
292    ]
293  | //
294  ]
295| #H @(proj2 … (all_All …)) @(All_mp … H)
296  * #id * #fd
297  [ * #W #S
298    lapply ((proj2 … (check_well_cost_fn_ok …)) W)
299    lapply ((proj2 … (check_sound_cost_fn_ok …)) S) /2/
300  | //
301  ]
302] qed.
303
Note: See TracBrowser for help on using the repository browser.