Changeset 2305 for src/RTLabs/CostCheck.ma
 Timestamp:
 Aug 30, 2012, 4:47:54 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostCheck.ma
r2303 r2305 47 47 ] qed. 48 48 49 axiom check_sound_cost_fn : internal_function → bool. 49 include "basics/lists/listb.ma". 50 include alias "utilities/deqsets.ma". 51 52 lemma 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 70 include 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. *) 76 let 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) 84 on term_check : gt term_check (id_map_size … to_check) → option (identifier_set LabelTag) ≝ 85 let stop_now ≝ Some ? to_check in 86 match 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 117 inductive 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?) *) 143 lemma 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/ 148 qed. 149 150 lemma 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 185 lemma 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 190 cases (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 196 let 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) 205 on term_check : gt term_check (id_map_size … to_check) → bool ≝ 206 match 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 *) 232 definition 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 235 lemma 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 ???) // 239 qed. 240 241 lemma 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 % 244 normalize @not_to_not 245 >lookup_opt_map cases (lookup_opt ???) normalize // 246 #a #E destruct 247 qed. 248 249 lemma 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 // 252 qed. 253 254 definition 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 50 277 axiom check_sound_cost_fn_ok : ∀fn. bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn. 51 278
Note: See TracChangeset
for help on using the changeset viewer.