Changeset 2307 for src/RTLabs/CostCheck.ma
- Timestamp:
- Aug 30, 2012, 4:47:58 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/CostCheck.ma
r2305 r2307 29 29 definition check_well_cost_fn : internal_function → bool ≝ 30 30 λf. 31 idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement fs (f_closed f l s PR)) ∧31 idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement (f_graph f) s (f_closed f l s PR)) ∧ 32 32 is_cost_label (lookup_present … (f_graph f) (f_entry f) ?). 33 33 cases (f_entry f) // … … 96 96 match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with 97 97 [ Some to_check' ⇒ λH'. 98 if h ∈ checking_tail then None ? else99 98 let PR' ≝ ? in 100 99 let st' ≝ lookup_present … g h PR' in 101 100 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 *) 101 if h ∈ checking_tail then None ? else 102 check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ? 103 | None ⇒ λ_. 104 if h == checking ∨ h ∈ checking_tail then None ? else 105 stop_now (* already checked successor *) 104 106 ] (try_remove_some_card … to_check h) 105 107 | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *) … … 122 124 successors (lookup_present … g l PR) = [l'] → 123 125 ¬ l' ∈ toch → 126 l' ≠ l → 127 ¬ l' ∈ tl → 124 128 check_label_bounded_spec g l tl toch toch 125 129 | clbs_cost : ∀l,PR,l',PR',tl,toch. … … 148 152 qed. 149 153 154 lemma not_orb : ∀b,c:bool. 155 ¬ (b∨c) → 156 (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)). 157 * * normalize /2/ 158 qed. 159 150 160 lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'. 151 161 check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' → … … 162 172 lapply (refl ? (try_remove … to_check h)) 163 173 cases (try_remove ????) in ⊢ (???% → %); 164 [ #RM whd in ⊢ (? → ??%? → ?); #H #E destruct @(clbs_checked … SUCC) 165 whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) // 174 [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim 175 [ #H' #E destruct 176 | #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC) 177 [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) // 178 | % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) * 179 | assumption 180 ] 181 ] 166 182 | * * #to_check'' #RM #H whd in ⊢ (??%? → ?); 167 183 @if_elim 168 [ #IN whd in ⊢ (??%? → ?); #E destruct 169 | #OUT whd in ⊢ (??%? → ?); 184 [ #CS #E destruct @(clbs_cost … SUCC … CS) 185 cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L // 186 | #CS 170 187 @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)188 [ #IN whd in ⊢ (??%? → ?); #E destruct 189 | #OUT whd in ⊢ (??%? → ?); #H 190 @(clbs_step … SUCC OUT CS RM) @(IH … H) 174 191 ] 175 192 ] … … 181 198 ] qed. 182 199 183 200 lemma check_label_bounded_c : ∀g,CL,checking,checking_tail,to_check,to_check'. 201 check_label_bounded_spec g checking checking_tail to_check to_check' → 202 ∀term_check,TERM,PR. 203 check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check'. 204 #g #CL #X1 #X2 #X3 #X4 #X elim X 205 [ #l #PR #tl #toch #SUCC 206 * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR 207 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 208 whd in ⊢ (??%?); % 209 | #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl 210 * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR 211 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 212 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); 213 cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ // | * * ] ] 214 #L >(proj2 … (try_remove_empty …) L) #H2 215 whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl) 216 % 217 | #l #PR #l' #PR' #tl #toch #SUCC #IN #CS 218 * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR 219 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 220 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); 221 cut (lookup … toch l' = Some ? it) [ whd in IN:(?%); cases (lookup ????) in IN ⊢ %; [ * | * // ] ] 222 #L cases (try_remove_this ????? L) #to_check' #RM >RM #H2 223 whd in ⊢ (??%?); >CS whd in ⊢ (??%?); % 224 | #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH 225 * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR 226 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 227 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2 228 whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS)) 229 whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN)) 230 whd in ⊢ (??%?); >(IH term_check' ??) % 231 | #l #PR #x #y #zs #tl #toch #SUCC 232 * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR 233 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 234 whd in ⊢ (??%?); % 235 ] qed. 184 236 185 237 lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'. … … 192 244 [ #E destruct whd in ⊢ (?%); >L1 // 193 245 | #L4 whd in ⊢ (?%); >L4 @IH @IN 246 ] qed. 247 248 lemma bound_on_instrs_to_cost_prime : ∀g,l,n. 249 bound_on_instrs_to_cost g l n → 250 bound_on_instrs_to_cost' g l n. 251 #g #l #n #H inversion H 252 #l' #n' #PR #H' #E1 #E2 #_ destruct 253 lapply (refl ? (is_cost_label (lookup_present … g l' PR))) 254 cases (is_cost_label ?) in ⊢ (???% → ?); #CS 255 [ @boitc_here [ @PR | @eq_true_to_b @CS ] 256 | @boitc_later [ @PR | @eq_false_to_notb @CS | @H ] 257 ] qed. 258 259 lemma present_member : ∀tag,A,m,id. 260 present tag A m id → member tag A m id. 261 #tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??)) 262 qed. 263 264 (* TODO: move and eliminate dup in Traces.ma *) 265 lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S. 266 Exists S (λy. y = x) l → 267 x ∈ l. 268 #S #x #l elim l 269 [ // 270 | #h #t #IH 271 normalize lapply (eqb_true … x h) 272 cases (x==h) * 273 [ #E #_ >(E (refl ??)) // 274 | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct 275 | #H @IH @H 276 ] 277 ] 278 ] qed. 279 280 lemma successors_inv : ∀st,x,y,zs. 281 successors st = x::y::zs → 282 ∃r,l1,l2. st = St_cond r l1 l2. 283 * normalize 284 #a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l destruct 285 /4/ 286 qed. 287 288 include alias "utilities/deqsets.ma". 289 290 lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g. 291 (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → 292 ∀l,PR,x,y,zs. successors (lookup_present … g l PR) = x::y::zs → 293 ∀l'. ∀IN : l' ∈ successors (lookup_present … g l PR). 294 is_cost_label (lookup_present … g l' ?). 295 [2: @(successors_present … IN) @(CL l) @lookup_lookup_present ] 296 #g #CL #WCL #l #PR #x #y #zs #SUCCS 297 cases (successors_inv … SUCCS) 298 #r * #l1 * #l2 #E 299 #l' #IN generalize in ⊢ (?(?(?????%))); #OR' >E in IN; 300 lapply (WCL l PR) generalize in ⊢ (?(???%) → ?); >E in ⊢ (% → % → ?); #LP #WCst 301 cases (andb_Prop_true ?? WCst) 302 #H1 #H2 303 whd in ⊢ (?% → ?); @eqb_elim 304 [ 2: #_ #IN lapply (memb_single … IN) ] 305 #E destruct // 306 qed. 307 308 309 lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'. 310 ∀CL:graph_closed g. 311 (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → 312 check_label_bounded_spec g checking checking_tail to_check to_check' → 313 (∀l. l∈g → ¬l ∈ to_check → l≠checking → ¬l∈checking_tail → ∃n. bound_on_instrs_to_cost g l n) → 314 ∀l. l = checking ∨ bool_to_Prop (l∈to_check) → 315 bool_to_Prop (l∈to_check') ∨ ∃n. bound_on_instrs_to_cost g l n. 316 #g #X1 #X2 #X3 #X4 #CL #WCL #X elim X 317 [ #l #PR #tl #toch #SUCC #INV #l' * 318 [ #E destruct %2 %{1} % [ @PR | >SUCC #l' * ] 319 | #IN %1 @IN 320 ] 321 | #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl #INV #l'' * 322 [ #E destruct %2 323 cases (INV l' ????) 324 [ #n #B 325 %{(S n)} % [ @PR | >SUCC #l'' * [2: *] #E destruct /2/ ] 326 | @present_member @(successors_present … (CL l ? (lookup_lookup_present … PR))) 327 >SUCC @eq_true_to_b @memb_hd 328 | assumption 329 | assumption 330 | assumption 331 ] 332 | #IN %1 assumption 333 ] 334 | #l #PR #l' #PR' #tl #toch #SUCC #IN #CS #INV #l'' * 335 [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ] 336 | /2/ 337 ] 338 | #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN_tl #NCS #RM #H #IH #INV #l'' * 339 [ #E destruct %2 cases (IH ? l' ?) 340 [ #IN @⊥ lapply (check_label_bounded_subset … H l' IN) #IN' 341 cases (try_remove_some ?????? RM) * #_ #L #_ whd in IN':(?%); 342 cases (lookup ????) in IN' L; [ * | * #_ #E destruct ] 343 | * #n #B %{(S n)} % [ // | #l'' >SUCC * [2: *] #E destruct /2/ ] 344 | #l'' #INg #INch' #NEQ #NIN_ltl @(INV l'' INg ???) 345 [ @notb_Prop % #INch @(absurd ?? (Prop_notb … INch')) 346 cases (try_remove_some ?????? RM) * #_ #_ #L 347 cases (L l'') [ #E destruct cases NEQ #X cases (X (refl ??)) ] 348 #L' whd in ⊢ (?%); <L' @INch 349 | % #E destruct cases (Prop_notb … NIN_ltl) #X @X @eq_true_to_b @memb_hd 350 | @notb_Prop @(not_to_not … (Prop_notb … NIN_ltl)) #IN @eq_true_to_b @memb_cons @IN 351 ] 352 | %1 % 353 ] 354 | #IN @(IH ? l'' ?) 355 [ #l''' #INg #NINch' #NEQ #NINtl @INV 356 [ assumption 357 | @notb_Prop @(not_to_not … (Prop_notb … NINch')) 358 cases (try_remove_some ?????? RM) * #L1 #L2 #L3 359 cases (L3 l''') 360 [ #E destruct @⊥ cases NEQ /2/ 361 | #L whd in ⊢ (?% → ?%); >L // 362 ] 363 | % #E destruct cases (Prop_notb … NINtl) #X @X @eq_true_to_b @memb_hd 364 | @notb_Prop @(not_to_not … (Prop_notb … NINtl)) #IN @eq_true_to_b @memb_cons @IN 365 ] 366 | cases (try_remove_some ?????? RM) * #L1 #L2 #L3 367 cases (L3 l'') [ #E destruct %1 % | #L %2 whd in ⊢ (?%); <L @IN ] 368 ] 369 ] 370 | #l #PR #x #y #zs #tl #toch #SUCCS #INV #l' * 371 [ #E destruct %2 %{1} % [ // ] 372 #l' #EX @boitc_here 373 [ @(successors_present … (CL l ? (lookup_lookup_present … PR))) 374 @Exists_memb @EX 375 | @(after_branch_are_cost_labels … WCL … SUCCS) 376 ] 377 | /2/ 378 ] 194 379 ] qed. 195 380 … … 229 414 ] qed. 230 415 416 lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,SMALLER,TERM. 417 (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → 418 check_graph_bounded g CL to_check SUB start PR SMALLER term_check TERM = true → 419 (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) → 420 ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n. 421 #g #CL #term_check elim term_check 422 [ #to_check #SUB #start #PR #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct 423 | #term_check' #IH #to_check #SUB #start #PR #SMALLER #TERM #WCL 424 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 425 cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?); 426 [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ] 427 generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?); 428 lapply (choose_empty … to_check') 429 cases (choose LabelTag unit to_check') 430 [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN 431 cases (true_or_false_Prop (l∈to_check ∨ l == start)) 432 [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?) 433 [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; * 434 | // 435 | // 436 | @WCL 437 | #l' #IN_g #NIN_to_check #NEQ #_ @H // 438 | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E 439 ] 440 | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ] 441 ] 442 | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); 443 #CHECK #H @(IH … CHECK) 444 [ @WCL 445 | #l #INg #NIN'' #NEQ 446 cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN'')) 447 cases (H4 … (refl ??)) * #L1 #L2 #L3 448 cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ] 449 #NIN' 450 cases (true_or_false_Prop (l∈to_check ∨ l == start)) 451 [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?) 452 [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN')) 453 | // 454 | // 455 | @WCL 456 | #l' #IN_g #NIN_to_check #NEQ #_ @H // 457 | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E 458 ] 459 | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ] 460 ] 461 ] 462 ] 463 ] qed. 464 231 465 (* TODO: move *) 232 466 definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝ … … 275 509 ] qed. 276 510 277 axiom check_sound_cost_fn_ok : ∀fn. bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn. 511 axiom check_sound_cost_fn_ok : ∀fn. 512 well_cost_labelled_fn fn → 513 bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn. 514 (* 515 #fn #WCL % 516 [ whd in ⊢ (?% → %); 517 generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?); 518 cases (try_remove ????) 519 [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E 520 lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?); 521 >(E (refl ??)) * /3/ 522 | * * #to_check #H1 #H2 #H3 523 whd in ⊢ (?% → ?); #CHECK 524 #l #PR @(check_graph_bounded_ok … CHECK) 525 [ #l' #PR' cases WCL // 526 | #l' #IN #NIN #NEQ @⊥ 527 cases (H1 … (refl ??)) * #L1 #L2 #L3 528 @(absurd ?? (Prop_notb … NIN)) 529 cases (L3 l') 530 [ #E >E in NEQ; * #H cases (H (refl ??)) 531 | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …)) 532 @member_present @IN 533 ] 534 | /2/ 535 ] 536 ] 537 | TODO 538 *) 278 539 279 540 definition check_cost_program : RTLabs_program → bool ≝ … … 287 548 [ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp 288 549 * #id * #fd 289 [ #H cases (andb_Prop_true … H) #W #S % 290 [ @(proj1 … (check_well_cost_fn_ok … )) // 550 [ #H cases (andb_Prop_true … H) #W #S 551 lapply (proj1 … (check_well_cost_fn_ok …) W) #W' 552 % 553 [ // 291 554 | @(proj1 … (check_sound_cost_fn_ok …)) // 292 555 ]
Note: See TracChangeset
for help on using the changeset viewer.