Changeset 2894
 Timestamp:
 Mar 16, 2013, 9:08:18 PM (6 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r2893 r2894 190 190 ] qed. 191 191 192 lemma extend_RTLabs_eval_statement : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'. 193 eval_statement ge s = return 〈tr,s'〉 → 194 ∃S,M. eval_ext_statement ge s = return 〈tr,mk_RTLabs_ext_state … s' S M〉. 195 #ge #s #tr #s' #EV 196 whd in match (eval_ext_statement ??); 197 letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *) 198 cut (∀s',t,EV. Ras_state … (f s' t EV) = s') 199 [ // ] 200 generalize in match f; f 201 >EV #next #NEXT whd in ⊢ (??(λ_.??(λ_.??%?))); 202 lapply (NEXT … (refl ??)) 203 cases (next s' tr ?) #s'' #S'' #M'' #E destruct %{S''} %{M''} % 204 qed. 205 192 206 lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'. 193 207 exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 → … … 255 269 ] qed. 256 270 271 lemma int_trace_split : ∀C,t1,t2,callstack,cs2,obs. 272 intensional_trace_of_trace C callstack (t1@t2) = 〈cs2,obs〉 → 273 ∃cs1,t1',t2'. 274 intensional_trace_of_trace C callstack t1 = 〈cs1,t1'〉 ∧ 275 intensional_trace_of_trace C cs1 t2 = 〈cs2,t2'〉 ∧ 276 obs = t1'@t2'. 277 #C #t1 #t2 #cs0 #cs2 #obs >int_trace_append' 278 cases (intensional_trace_of_trace C cs0 t1) #cs1 #t1' 279 normalize nodelta #E %{cs1} %{t1'} 280 cases (intensional_trace_of_trace C cs1 t2) in E ⊢ %; #cs2 #t2' 281 normalize nodelta #E destruct 282 %{t2'} 283 /3/ 284 qed. 285 286 definition cs_change : trace_ends_with_ret → ident → list ident → list ident → Prop ≝ λends,fn,cs,cs'. 287 match ends with 288 [ ends_with_ret ⇒ cs = cs' 289  doesnt_end_with_ret ⇒ fn::cs = cs' 290 ]. 291 292 lemma as_exec_eq_step : ∀ge,s1,s2,tr,s2'. 293 as_execute (RTLabs_status ge) s1 s2 → 294 step io_out io_in RTLabs_ext_fullexec ge s1 = Value ??? 〈tr,s2'〉 → 295 s2 = s2'. 296 #ge #s1 #s2 #tr #s2' * #tr * #EX 297 whd in ⊢ (? → ??%? → ?); 298 letin f ≝ (next_state ge s1) change with (f (Ras_state … s2) tr EX) in ⊢ (??%? → ?); 299 generalize in ⊢ (??(%???)? → ??(?%)? → ?); >EX in ⊢ (% → % → ??(match % with [_⇒?_⇒?_⇒?]?)? → ?); 300 #next #NEXT whd in ⊢ (??%? → ?); #E destruct >NEXT % 301 qed. 302 303 include alias "basics/logic.ma". (* For ∧ *) 304 305 let rec eq_end_tlr ge s trace' s' tlr s'' on tlr : 306 exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 → 307 s' = s'' ≝ ? 308 and eq_end_tll ge s trace' s' ends tll s'' on tll : 309 exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 → 310 s' = s'' ≝ ? 311 and eq_end_tal ge s trace' s' ends tal s'' on tal : 312 exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 → 313 s' = s'' ≝ ?. 314 [ cases tlr 315 [ #s1 #s2 #tll @eq_end_tll 316  #s1 #s2 #s3 #tll #tlr' #EX 317 cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1 318 <(eq_end_tll … EX1) #EX2 #E 319 @(eq_end_tlr … EX2) 320 ] 321  cases tll 322 #ends' #s1 #s2 #tal #CS 323 @eq_end_tal 324  cases tal 325 [ #s1 #s2 #EX #CL #CS whd in ⊢ (??(?%?????)? → ?); #EX' 326 cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' 327 whd in EX':(??%%); destruct 328 @(as_exec_eq_step … EX ST) 329  #s1 #s2 #EX #CL #EX' 330 cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' 331 whd in EX':(??%%); destruct 332 @(as_exec_eq_step … EX ST) 333  #s1 #s2 #s3 #EX #CL #AF #tlr #CS #EX' 334 cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' 335 lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX' 336 @(eq_end_tlr … tlr … EX') 337  #s1 #s2 #s3 #EX #CL #tlr #EX' 338 cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' 339 lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX' 340 @(eq_end_tlr … tlr … EX') 341  #ends #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal' #EX' 342 cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' 343 lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX' 344 cases (exec_steps_split … EX') #trace1 * #trace2 * #s5 * * #EX2 #EX3 #E3 345 lapply (eq_end_tlr … tlr … EX2) #E4 <E4 in EX3; #EX3 346 @(eq_end_tal … EX3) 347  #ends #s1 #s2 #s3 #EX #tal' #CL #CS #EX' 348 cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' 349 lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX' 350 @(eq_end_tal … EX') 351 ] 352 ] qed. 353 354 definition maybe_label ≝ 355 λge,s,obs. 356 match as_label (RTLabs_status ge) s with 357 [ None ⇒ obs 358  Some cl ⇒ (IEVcost cl)::obs 359 ]. 360 361 lemma definitely_maybe_label : ∀ge,s,CS,tl. 362 (IEVcost (as_label_safe (RTLabs_status ge) «s,CS»))::tl = maybe_label ge s tl. 363 #ge #s #CS #tl 364 whd in ⊢ (???%); whd in match (as_label_safe ??); 365 >(opt_to_opt_safe … CS) in ⊢ (???%); 366 % 367 qed. 368 369 lemma only_plain_step_events_is_one_cost : ∀ge,s,tr,s'. 370 eval_statement ge s = Value ??? 〈tr,s'〉 → 371 (∃cl. tr = [EVcost cl] ∧ RTLabs_cost_label s = Some ? cl) ∨ 372 (tr = [ ] ∧ RTLabs_cost_label s = None ?). 373 #ge * 374 [ #f #fs #m #tr #s' whd in ⊢ (??%? → ?); 375 whd in match (RTLabs_cost_label ?); generalize in ⊢ (??(?%)? → ?); 376 cases (next_instruction f) 377 [ #l #LP normalize nodelta #E whd in E:(??%%); destruct %2 % % 378  #cl #l #LP #E whd in E:(??%%); destruct % %{cl} % % 379  #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct %2 % % 380  #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % % 381  #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % % 382  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % % 383  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % % 384  #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 % % 385  #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok * #fd #fid #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ? Efd) #b * #Ev' #Efn %2 % % 386  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct %2 % % 387  #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result ?) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %2 % % 388 ] 389  #vf * #fn #args #retdst #stk #m #tr #s' 390 whd in ⊢ (??%? → ?); 391 [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?); 392 #E destruct %2 % % 393  @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct %2 % % 394 ] 395  #v #r * [2: #f #fs ] #m #tr #s' 396 whd in ⊢ (??%? → ?); 397 [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %2 % % 398  cases v [ normalize #E destruct  * [ 2: * #r normalize #E destruct %2 % %  *: normalize #a try #b destruct ] ] 399 ] 400  #r #tr #s' normalize #E destruct 401 ] qed. 402 403 lemma drop_exec_ext : ∀ge,s,tr,s'. 404 eval_ext_statement ge s = return 〈tr,s'〉 → 405 eval_statement ge s = return 〈tr,Ras_state … s'〉. 406 #ge #s #tr #s' 407 whd in ⊢ (??%? → ?); 408 letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *) 409 cut (∀s',t,EV. Ras_state … (f s' t EV) = s') 410 [ // ] 411 generalize in match f; f 412 cases (eval_statement ge s) 413 [ #o #k #n #N #E whd in E:(??%%); destruct 414  * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT // 415  #m #n #N #E whd in E:(??%%); destruct 416 ] qed. 417 418 lemma RTLabs_as_label : ∀ge,s. 419 RTLabs_cost_label (Ras_state … s) = as_label (RTLabs_status ge) s. 420 cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE 421 #ge * * 422 [ * #func #locals #next #nok #sp #r #fs #m #stk #mtc 423 whd in ⊢ (???%); 424 whd in match (as_pc_of ??); 425 cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2 426 whd in ⊢ (???%); >M1 whd in ⊢ (???%); 427 whd in ⊢ (??%?); change with (lookup_present ?????) in match (next_instruction ?); 428 >(lookup_lookup_present … nok) whd in ⊢ (??%%); 429 % 430  #vf #fd #args #dst #fs #m * [*] #func #stk #mtc whd in ⊢ (??%%); % 431  #v #dst #fs #m * [2: #fn #stk] #mtc % 432  // #r #stk #mtc % 433 ] qed. 434 257 435 436 437 lemma step_cost_event : ∀ge,s,tr,s',obs. 438 step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 → 439 maybe_label ge s obs = intensional_events_of_events tr@obs. 440 #ge #s #tr #s' #obs #ST 441 cases (only_plain_step_events_is_one_cost … (drop_exec_ext … ST)) 442 [ * #cl * #E1 #CS whd in ⊢ (??%?); 443 <RTLabs_as_label >CS destruct % 444  * #E #CS whd in ⊢ (??%?); 445 <RTLabs_as_label >CS destruct % 446 ] qed. 447 448 lemma call_ret_event : ∀ge,s,tr,s',obs. 449 step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 → 450 (as_classify (RTLabs_status ge) s = cl_call ∨ as_classify (RTLabs_status ge) s = cl_return) → 451 maybe_label ge s obs = obs ∧ tr = [ ]. 452 #ge * * 453 [ #f #fs #m #S #M #tr #s' #obs #ST * whd in match (as_classify ??); 454 cases (next_instruction f) normalize 455 #A try #B try #C try #D try #E try #F try #G try #H try #I destruct 456  #fid * #fn #args #retdst #stk #m #S #M #tr #s' #obs #ST #_ 457 letin s ≝ (Callstate ??????) 458 cut (RTLabs_cost_label s = None ?) 459 [ 1,3: // ] #CS % 460 [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ] 461 lapply (drop_exec_ext … ST) 462 whd in ⊢ (??%? → ?); 463 [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?); 464 #E destruct % 465  @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct 466 ] 467  #v #r * [2: #f #fs ] #m #S #M #tr #s' #obs 468 letin s ≝ (Returnstate ????) #ST #_ 469 cut (RTLabs_cost_label s = None ?) 470 [ 1,3: // ] #CS % 471 [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ] 472 lapply (drop_exec_ext … ST) 473 whd in ⊢ (??%? → ?); 474 [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct % 475  cases v [ normalize #E destruct  * [ 2: * #r normalize #E destruct %  *: normalize #a try #b destruct ] ] 476 ] 477  #r #S #M #tr #s' #obs normalize #E destruct 478 ] qed. 479 480 lemma itot_call : ∀C,cs,s,rem,cs',trace. 481 ∀CL:match cs_classify C s with [ cl_call ⇒ True  _ ⇒ False ]. 482 intensional_trace_of_trace C cs (〈s,E0〉::rem) = 〈cs',trace〉 → 483 ∃trace'. 484 trace = (IEVcall (cs_callee C s CL))::trace' ∧ 485 intensional_trace_of_trace C (cs_callee C s CL :: cs) rem = 〈cs',trace'〉. 486 #C #cs #s #rem #cs' #trace #CL 487 whd in ⊢ (??%? → ?); 488 @generalize_callee cases (cs_classify C s) in CL ⊢ %; * 489 #name whd in ⊢ (??%? → ?); cases (intensional_trace_of_trace C (name I::cs) rem) 490 #cs' #trace' #E whd in E:(??%?); destruct %{trace'} % % 491 qed. 492 493 (* WIP 494 lemma as_call_cs_callee : ∀ge,s,CL,CL'. 495 as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'. 496 #ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E 497 destruct cases S in M CL' ⊢ %; [ * ] #fn' #S' * #M1 #M' #CL' 498 whd in ⊢ (??%%); cases (symbol_for_block ??) 499 500 501 (* observables_trace_label_label emits the cost label for the first step of the 502 enclosed tal, so we have to add that label if it exists to the front of the 503 events from the structured trace *) 504 let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr : 505 exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s'〉 → 506 intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 → 507 pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ? 508 and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll : 509 exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace1,s'〉 → 510 intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 → 511 pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ? 512 and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal : 513 exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace1,s'〉 → 514 intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 → 515 maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?. 516 [ cases tlr 517 [ #s1 #s2 #tll @eq_obs_tll 518  #s1 #s2 #s3 #tll #tlr #EX #ITOT 519 cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1 #EX2 #E 520 >E in ITOT; #ITOT cases (int_trace_split … ITOT) #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs 521 lapply (eq_end_tll … EX1) #E2 <E2 in EX1; #EX1 522 cases (eq_obs_tll … EX1 ITOT1) #ITOT1' #CS_CH whd in CS_CH; <CS_CH in ITOT2 EX2; <E2 #ITOT2 #EX2 523 cases (eq_obs_tlr … EX2 ITOT2) #E3 #E4 destruct % % 524 ] 525  cases tll #ends' #s1 #s2 #tal #CS #EX #ITOT whd in ⊢ (?(??%?)?); 526 whd in ⊢ (?(??(??%?)?)?) ; >(definitely_maybe_label … CS) 527 @(eq_obs_tal … EX ITOT) 528  cases tal 529 [ #s1 #s2 #ST * #CL #CS #EX 530 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX 531 whd in EX:(??%?); destruct 532 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?); 533 whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?); 534 whd in ⊢ (? → ? → ?(??(???%)?)?); 535 >CL #call whd in ⊢ (??%? → ?); #E destruct 536 % [ 1,3: @(step_cost_event … ST')  2,4: % ] 537  #s1 #s2 #ST #CL #EX 538 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX 539 whd in EX:(??%?); destruct 540 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?); 541 whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?); 542 whd in ⊢ (? → ? → ?(??(???%)?)?); >CL #call whd in ⊢ (??%? → ?); #E destruct 543 cases (call_ret_event … ST') 544 [ #E1 #E2 >E1 >E2 % % 545  skip 546  %2 @CL 547 ] 548  #s1 #s2 #s3 #ST #CL #AF #tlr #CS #EX 549 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX 550 whd in EX:(??%?); destruct cases (call_ret_event … ST') 551 [ #E1 #E2 >E1 >E2  skip  %1 @CL ] #ITOT 552 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ? = ?) in CL; >CL % ] 553 #obs' * #E3 #ITOT' 554 <(as_exec_eq_step … ST ST') in EX; #EX 555 cases (eq_obs_tlr … EX ITOT') 556 #OBS' #E4 <E4 % 557 [ >E3 <OBS' whd in ⊢ (??%?); 558 559 560 561 562 ] qed. 563 *) 564 565 258 566 259 567 (* I'm not entirely certain that existentially quantifying fn is the right thing … … 295 603 ] 296 604  @WCLge 297  * #s2' #rem #_ #tlr # STACK #_605  * #s2' #rem #_ #tlr #LEN #STACK #_ 298 606 %{s1'} %{s2'} % [2: %{tlr} 299 607 % [ % [ % 
src/RTLabs/RTLabs_partial_traces.ma
r2840 r2894 106 106 #ST' whd in ⊢ (??%?); % 107 107 qed. 108 109 let rec length_flat_trace O I ge s (t:flat_trace O I ge s) on t : nat ≝ 110 match t with 111 [ ft_stop _ ⇒ 0 112  ft_step _ _ _ _ t' ⇒ S (length_flat_trace … t') 113 ]. 108 114 109 115 … … 633 639 ] qed. 634 640 641 (* Measure the number of steps in the structured trace so that we know it's the 642 same execution that we started with. TODO: move *) 643 let rec length_tlr (S:abstract_status) s1 s2 (tlr:trace_label_return S s1 s2) on tlr : nat ≝ 644 match tlr with 645 [ tlr_base _ _ tll ⇒ length_tll … tll 646  tlr_step _ _ _ tll tlr' ⇒ length_tll … tll + length_tlr … tlr' 647 ] 648 and length_tll (S:abstract_status) e s1 s2 (tll:trace_label_label S e s1 s2) on tll : nat ≝ 649 match tll with 650 [ tll_base _ _ _ tal _ ⇒ length_tal … tal 651 ] 652 and length_tal (AS:abstract_status) e s1 s2 (tal:trace_any_label AS e s1 s2) on tal : nat ≝ 653 match tal with 654 [ tal_base_not_return _ _ _ _ _ ⇒ 1 655  tal_base_return _ _ _ _ ⇒ 1 656  tal_base_call _ _ _ _ _ _ tlr _ ⇒ S (length_tlr … tlr) 657  tal_base_tailcall _ _ _ _ _ tlr ⇒ S (length_tlr … tlr) 658  tal_step_call _ _ _ _ _ _ _ _ tlr _ tal' ⇒ S (length_tlr … tlr + length_tal … tal') 659  tal_step_default _ _ _ _ _ tal' _ _ ⇒ S (length_tal … tal') 660 ]. 661 662 663 635 664 (* Don't need to know that labels break loops because we have termination. *) 636 665 … … 641 670 (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start) 642 671 (original_terminates: will_return ge depth start full) 643 (T:RTLabs_ext_state ge → Type[0]) (l imit:nat) : Type[0] ≝672 (T:RTLabs_ext_state ge → Type[0]) (length:∀s. T s → nat) (limit:nat) : Type[0] ≝ 644 673 { 645 674 new_state : RTLabs_ext_state ge; … … 647 676 cost_labelled : well_cost_labelled_state new_state; 648 677 new_trace : T new_state; 678 tr_length : plus (length … new_trace) (length_flat_trace … remainder) = length_flat_trace … full; 649 679 stack_ok : stack_preserved ge ends start new_state; 650 680 terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth ]) with … … 661 691 (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start) 662 692 (original_terminates: will_return ge depth start full) 663 (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝ 693 (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0]) 694 (length:∀e,s. T e s → nat) 695 (limit:nat) : Type[0] ≝ 664 696 { 665 697 ends : trace_ends_with_ret; 666 trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit698 trace_res :> trace_result ge depth ends start full original_terminates (T ends) (length ends) limit 667 699 }. 668 700 … … 671 703 the size of the termination proof might need to be relaxed, too. *) 672 704 673 definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l 1,l2. l2 ≥ l1 →674 ∀r:trace_result ge d e s1 t1 TM1 T1 l 1.705 definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2. l2 ≥ l1 → 706 ∀r:trace_result ge d e s1 t1 TM1 T1 ln1 l1. 675 707 will_return_end … TM1 = will_return_end … TM2 → 676 T2 (new_state … r) → 708 ∀trace:T2 (new_state … r). 709 ln2 (new_state … r) trace + length_flat_trace … (remainder … r) = length_flat_trace … t2 → 677 710 stack_preserved ge e s2 (new_state … r) → 678 trace_result ge d e s2 t2 TM2 T2 l 2 ≝679 λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l 1,l2,lGE,r,TME,trace,SP.680 mk_trace_result ge d e s2 t2 TM2 T2 l 2711 trace_result ge d e s2 t2 TM2 T2 ln2 l2 ≝ 712 λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2,lGE,r,TME,trace,LN,SP. 713 mk_trace_result ge d e s2 t2 TM2 T2 ln2 l2 681 714 (new_state … r) 682 715 (remainder … r) 683 716 (cost_labelled … r) 684 717 trace 718 LN 685 719 SP 686 720 ? … … 691 725 cases e in r ⊢ %; 692 726 [ <TME TME * cases d in TM1 TM2 ⊢ %; 693 [ #TM1 #TM2 #ns #rem #WCLS #T1NS # SP whd in ⊢ (% → %); #TMS @TMS694  #d' #TM1 #TM2 #ns #rem #WCLS #T1NS # SP whd in ⊢ (% → %); * #TMa * #L1 #TME727 [ #TM1 #TM2 #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %); #TMS @TMS 728  #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %); * #TMa * #L1 #TME 695 729 %{TMa} % // @(transitive_le … lGE) @L1 696 730 ] 697  <TME TME * #ns #rem #WCLS #T1NS # SP whd in ⊢ (% → %);731  <TME TME * #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %); 698 732 * #TMa * #L1 #TME 699 733 %{TMa} % // @(transitive_le … lGE) @L1 700 734 ] qed. 701 735 702 definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l 1,l2. l2 ≥ l1 →703 ∀r:sub_trace_result ge d s1 t1 TM1 T1 l 1.736 definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2. l2 ≥ l1 → 737 ∀r:sub_trace_result ge d s1 t1 TM1 T1 ln1 l1. 704 738 will_return_end … TM1 = will_return_end … TM2 → 705 T2 (ends … r) (new_state … r) → 739 ∀trace:T2 (ends … r) (new_state … r). 740 ? (*XXX matita infers this, but won't check it ?! *) + length_flat_trace … (remainder … r) = length_flat_trace ???? t2 → 706 741 stack_preserved ge (ends … r) s2 (new_state … r) → 707 sub_trace_result ge d s2 t2 TM2 T2 l 2 ≝708 λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l 1,l2,lGE,r,TME,trace,SP.709 mk_sub_trace_result ge d s2 t2 TM2 T2 l 2742 sub_trace_result ge d s2 t2 TM2 T2 ln2 l2 ≝ 743 λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2,lGE,r,TME,trace,LN,SP. 744 mk_sub_trace_result ge d s2 t2 TM2 T2 ln2 l2 710 745 (ends … r) 711 (replace_trace … lGE … r TME trace SP).746 (replace_trace … lGE … r TME trace LN SP). 712 747 713 748 (* Small syntax hack to avoid ambiguous input problems. *) 714 749 definition myge : nat → nat → Prop ≝ ge. 750 751 lemma crappyhack : ∀tlr,rem1,tr,tal,rem2:nat. 752 tlr+rem1 = tr → tal + rem2 = rem1 → S (tlr + tal) + rem2 = S tr. 753 #tlr #rem1 #tr #tal #rem2 #E1 #E2 destruct <associative_plus % 754 qed. 715 755 716 756 let rec make_label_return ge depth (s:RTLabs_ext_state ge) … … 724 764 on TIME : trace_result ge depth ends_with_ret s trace TERMINATES 725 765 (trace_label_return (RTLabs_status ge) s) 726 (will_return_length … TERMINATES) ≝ 766 (length_tlr (RTLabs_status ge) s) 767 (will_return_length … TERMINATES) ≝ 727 768 728 769 match TIME return λTIME. TIME ≥ ? → ? with … … 737 778 TERMINATES 738 779 TIME ? in 739 match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →740 trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with780 match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) (length_tll (RTLabs_status ge) x s) ? → 781 trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) ? (will_return_length … TERMINATES) with 741 782 [ ends_with_ret ⇒ λr. 742 replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)783 replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) ? (stack_ok … r) 743 784  doesnt_end_with_ret ⇒ λr. 744 785 let r' ≝ make_label_return ge depth (new_state … r) … … 749 790 replace_trace … r' ? 750 791 (tlr_step (RTLabs_status ge) s (new_state … r) 751 (new_state … r') (new_trace … r) (new_trace … r')) ? 792 (new_state … r') (new_trace … r) (new_trace … r')) ?? 752 793 ] (trace_res … r) 753 794 … … 765 806 on TIME : sub_trace_result ge depth s trace TERMINATES 766 807 (λends. trace_label_label (RTLabs_status ge) ends s) 808 (λends. length_tll (RTLabs_status ge) ends s) 767 809 (will_return_length … TERMINATES) ≝ 768 810 … … 773 815 let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in 774 816 replace_sub_trace … r ? 775 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r)817 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) ? (stack_ok … r) 776 818 777 819 ] TERMINATES_IN_TIME … … 787 829 on TIME : sub_trace_result ge depth s0 trace TERMINATES 788 830 (λends. trace_any_label (RTLabs_status ge) ends s0) 831 (λends. length_tal (RTLabs_status ge) ends s0) 789 832 (will_return_length … TERMINATES) ≝ 790 833 791 834 match TIME return λTIME. TIME ≥ ? → ? with 792 835 [ O ⇒ λTERMINATES_IN_TIME. ⊥ 793  S TIME ⇒ λTERMINATES_IN_TIME. 836  S TIME ⇒ λTERMINATES_IN_TIME. 794 837 match s0 return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s. 795 838 well_cost_labelled_state s → 796 839 ∀TM:will_return ??? trace. 797 840 myge ? (times 3 (will_return_length ??? trace TM)) → 798 sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) ( will_return_length … TM)841 sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (λends. length_tal (RTLabs_status ge) ends s) (will_return_length … TM) 799 842 with [ mk_RTLabs_ext_state s stk mtc0 ⇒ λtrace. 800 843 match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk. … … 802 845 ∀TM:will_return ??? trace. 803 846 myge ? (times 3 (will_return_length ??? trace TM)) → 804 sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) ( will_return_length … TM) with847 sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (λends. length_tal (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with 805 848 [ ft_stop st ⇒ 806 849 λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥ … … 809 852 let start' ≝ mk_RTLabs_ext_state ge start stk mtc in 810 853 let next' ≝ next_state ? start' ?? EV in 811 match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) ( will_return_length … TERMINATES) with854 match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (λends. length_tal (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 812 855 [ cl_other ⇒ λCL. 813 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) ( will_return_length … TERMINATES) with856 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (λends. length_tal (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 814 857 (* We're about to run into a label. *) 815 858 [ true ⇒ λCS. 816 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?859 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ? 817 860 doesnt_end_with_ret 818 861 (mk_trace_result ge … next' trace' ? 819 (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ?? )862 (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ???) 820 863 (* An ordinary step, keep going. *) 821 864  false ⇒ λCS. 822 865 let r ≝ make_any_label ge depth next' trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in 823 replace_sub_trace ????????????? r ?866 replace_sub_trace ??????????????? r ? 824 867 (tal_step_default (RTLabs_status ge) (ends … r) 825 start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ? 868 start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ?? 826 869 ] (refl ??) 827 870 828 871  cl_jump ⇒ λCL. 829 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?872 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ? 830 873 doesnt_end_with_ret 831 874 (mk_trace_result ge … next' trace' ? 832 (tal_base_not_return (RTLabs_status ge) start' next' ???) ?? )875 (tal_base_not_return (RTLabs_status ge) start' next' ???) ???) 833 876 834 877  cl_call ⇒ λCL. 835 878 let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in 836 match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start' ?? (λends. trace_any_label (RTLabs_status ge) ends ?) ( will_return_length … TERMINATES) with879 match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start' ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (λends. length_tal (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 837 880 (* We're about to run into a label, use base case for call *) 838 881 [ true ⇒ λCS. 839 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?882 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ? 840 883 doesnt_end_with_ret 841 884 (mk_trace_result ge … 842 885 (tal_base_call (RTLabs_status ge) start' next' (new_state … r) 843 ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ?? )886 ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ???) 844 887 (* otherwise use step case *) 845 888  false ⇒ λCS. … … 850 893 (tal_step_call (RTLabs_status ge) (ends … r') 851 894 start' next' (new_state … r) (new_state … r') ? CL ? 852 (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ? 895 (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?? 853 896 ] (refl ??) 854 897 855 898  cl_return ⇒ λCL. 856 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?899 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ? 857 900 ends_with_ret 858 (mk_trace_result ge ??????? 901 (mk_trace_result ge ???????? 859 902 next' 860 903 trace' 861 904 ? 862 905 (tal_base_return (RTLabs_status ge) start' next' ? CL) 906 ? 863 907 ? 864 908 ?) … … 872 916  // 873 917  // 874  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT) 875  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ // 918  @(tr_length … r) 919  cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #GT #_ @(le_S_to_le … GT) 920  cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #_ #EEQ // 921  <(tr_length … r) <(tr_length … r') @associative_plus 876 922  @(stack_preserved_join … (stack_ok … r)) // 877 923  @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r)) 878  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_924  cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #LT #_ 879 925 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 880 926 @(transitive_le … (3*(will_return_length … TERMINATES))) … … 888 934  // 889 935  @(proj1 … (RTLabs_costed …)) // 936  @(tr_length … r) 890 937  @le_S_S_to_le @TERMINATES_IN_TIME 891 938  @(wrl_nonzero … TERMINATES_IN_TIME) … … 900 947  @(will_return_return … CL TERMINATES) 901 948  @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) 949  % 902 950  %{tr} %{EV} @refl 903 951  @(well_cost_labelled_state_step … EV) // 904 952  whd @(will_return_notfn … TERMINATES) %2 @CL 905 953  @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) 954  % 906 955  %{tr} %{EV} % 907 956  %1 whd @CL 908 957  @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) // 909 958  @(well_cost_labelled_state_step … EV) // 910  whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %959  whd cases (terminates ????????? r) #TMr * #LTr #EQr %{TMr} % 911 960 [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES) 912 961 #TMx * #LT' #_ @LT' … … 915 964 ] 916 965  @(stack_preserved_step ge start' ?? CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r) 966  whd in ⊢ (???%); <(tr_length … r) % 917 967  %{tr} %{EV} % 918 968  @(RTLabs_after_call … next') [ @eval_to_as_exec  // ] 919 969  @(cost_labelled … r) 920 970  skip 921  cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le971  cases r #ns #rm #WS #TLR #SP #LN * #TM * #LT #_ @le_S_to_le 922 972 @(transitive_lt … LT) 923 973 cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT' 924  cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ974  cases r #ns #rm #WS #TLR #SP #LN * #TM * #_ #EQ <EQ 925 975 cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ' 926 976  @(RTLabs_after_call … next') [ @eval_to_as_exec  // ] 927 977  %{tr} %{EV} % 978  @(crappyhack ????? (tr_length … r) (tr_length … r')) 928 979  @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r) 929 980  @(cost_labelled … r) 930  cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78981  cases r #H72 #H73 #H74 #H75 #HX #LN * #HY * #GT #H78 931 982 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 932 983 cases (will_return_call … TERMINATES) in GT; … … 947 998  whd @(will_return_notfn … TERMINATES) %1 @CL 948 999  @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) 1000  % 949 1001  %{tr} %{EV} % 950 1002  %2 whd @CL … … 954 1006  @CL 955 1007  %{tr} %{EV} % 1008  whd in ⊢ (??%%); @eq_f @(tr_length … r) 956 1009  @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) 957 1010  @(well_cost_labelled_state_step … EV) // … … 971 1024 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 972 1025 (TERMINATES: will_return ge depth s trace) 973 : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) ( will_return_length … TERMINATES) ≝1026 : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (length_tlr (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝ 974 1027 make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES 975 1028 (2 + 3 * will_return_length … TERMINATES) ?.
Note: See TracChangeset
for help on using the changeset viewer.