Changeset 2300 for src/RTLabs
 Timestamp:
 Aug 21, 2012, 7:00:43 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2299 r2300 2280 2280 2281 2281 2282 (* We still need to link tal_unrepeating to our definition of cost soundness. 2283 2284 First, let's link unrepeating to our PCs and successors. *) 2285 2286 definition RTLabs_pc_lookup : ∀ge. RTLabs_pc → option statement ≝ 2287 λge,pc. 2288 match pc with 2289 [ rapc_state b l ⇒ 2290 match find_funct_ptr … ge b with [ None ⇒ None ?  Some fd ⇒ 2291 match fd with [ Internal f ⇒ lookup ?? (f_graph f) l  _ ⇒ None ? ] ] 2292  _ ⇒ None ? 2293 ]. 2294 2295 definition genv_lookup : ∀ge. block → label → option statement ≝ 2296 λge,b,l. 2297 match find_funct_ptr … ge b with [ None ⇒ None ?  Some fd ⇒ 2298 match fd with [ Internal f ⇒ lookup ?? (f_graph f) l  _ ⇒ None ? ] ] 2299 . 2300 2301 inductive good_pc_list (ge:genv) : option block → list (as_pc (RTLabs_status ge)) → Prop ≝ 2302  g_pc_end : ∀pc,b. 2303 good_pc_list ge b [pc] 2304  g_pc_step : ∀b,l1,st,l2,tl. 2305 genv_lookup ge b l1 = Some ? st → 2306 l2 ∈ successors st → 2307 good_pc_list ge (Some ? b) (rapc_state b l2::tl) → 2308 good_pc_list ge (Some ? b) (rapc_state b l1::rapc_state b l2::tl) 2309  g_pc_call : ∀b,l1,st,l2,b',tl. 2310 genv_lookup ge b l1 = Some ? st → 2311 l2 ∈ successors st → 2312 good_pc_list ge (Some ? b) (rapc_call (Some ? l2) b'::tl) → 2313 good_pc_list ge (Some ? b) (rapc_state b l1::rapc_call (Some ? l2) b'::tl) 2314  g_pc_cret : ∀b,l,b',tl. 2315 good_pc_list ge (Some ? b) (rapc_state b l::tl) → 2316 good_pc_list ge (Some ? b) (rapc_call (Some ? l) b'::rapc_state b l::tl) 2317  g_pc_return : ∀b,l1,st,caller. 2318 genv_lookup ge b l1 = Some ? st → 2319 successors st = [ ] → 2320 good_pc_list ge (Some ? b) [rapc_state b l1; rapc_ret caller] 2321 . 2322 2282 2283 2284 2285 (* We still need to link tal_unrepeating to our definition of cost soundness. *) 2286 2287 2288 (* Extract the "current" function from a state. *) 2323 2289 definition state_fn : ∀ge. RTLabs_status ge → option block ≝ 2324 2290 λge,s. match Ras_fn_stack … s with [ nil ⇒ None ?  cons h t ⇒ … … 2327 2293  _ ⇒ Some ? h ] ]. 2328 2294 2329 (* After returning from a function we're either in the final state, or we're 2330 back in the caller at the correct instruction. *) 2331 2332 lemma pc_after_return : ∀ge,pre,post,CL,ret,callee. 2333 as_after_return (RTLabs_status ge) «pre,CL» post → 2334 as_pc_of (RTLabs_status ge) pre = rapc_call ret callee → 2335 match ret with 2336 [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ? 2337  Some retl ⇒ 2338 ∃fn. state_fn … pre = Some ? fn ∧ 2339 state_fn … post = Some ? fn ∧ 2340 as_pc_of (RTLabs_status ge) post = rapc_state fn retl 2341 ]. 2342 #ge #pre #post #CL #ret #callee #AF 2343 cases pre in CL AF ⊢ %; 2344 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); 2345 cases (lookup_present ???? (next_ok f)) in CL; 2346 normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct 2347  #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL 2348  #ret #dst #fs #m #S #M #CL normalize in CL; destruct 2349  #r #S #M #CL normalize in CL; destruct 2350 ] 2351 cases post 2352 * [ #postf #postfs #postm * [*] #fn' #S' #M' 2353  5: #postf #postfs #postm * [*] #fn' #S' #M' * 2354  2,6: #A #B #C #D #E #F #G * 2355  3,7: #A #B #C #D #E #F * 2356  #r #S' #M' #AF whd in AF; destruct 2357  #r #S' #M' 2358 ] 2359 #AF #PC normalize in PC; destruct whd 2360 [ %{fn'} cases AF * #A #B #C destruct % [ % %  whd in ⊢ (??%?); >A % ] 2361  % #E normalize in E; destruct 2362 ] qed. 2295 (* Some results to invert the classification of states *) 2363 2296 2364 2297 lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_state ge. … … 2393 2326 [ #fn %{fn} %  #fn #l %{fn} %{l} %  #caller #callee %{caller} %{callee} %  #fn #l %{fn} %{l} % ] 2394 2327 qed. 2395 2396 lemma tal_not_final : ∀ge,fl,s1,s2.2397 ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.2398 RTLabs_is_final (Ras_state … s1) = None ?.2399 #ge #flx #s1x #s2x *2400 [ #s1 #s2 * #tr * #EX #NX #CL #CS2401  #s1 #s2 * #tr * #EX #NX #CL2402  #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS2403  #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal2404  #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS2405 ] @(step_not_final … EX)2406 qed.2407 2408 lemma State_not_callreturn : ∀f,fs,m,cl.2409 RTLabs_classify (State f fs m) = cl →2410 match cl with2411 [ cl_return ⇒ False2412  cl_call ⇒ False2413  _ ⇒ True2414 ].2415 #f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);2416 cases (lookup_present … (next_ok f)) //2417 qed.2418 2419 (* TODO: move *)2420 lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.2421 Exists S (λy. y = x) l →2422 x ∈ l.2423 #S #x #l elim l2424 [ //2425  #h #t #IH2426 normalize lapply (eqb_true … x h)2427 cases (x==h) *2428 [ #E #_ >(E (refl ??)) //2429  #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct2430  #H @IH @H2431 ]2432 ]2433 ] qed.2434 2435 (* invert traces ending in a return *)2436 2437 lemma tal_return : ∀ge,fl,s1,s2.2438 as_classifier (RTLabs_status ge) s1 cl_return →2439 ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.2440 ∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL.2441 #ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal)2442 [ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct2443 whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct2444  #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct2445 %{EX} %{CL} % %2446  #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥2447 whd in CL CL'; >CL in CL'; #E destruct2448  #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct2449 whd in CL CL'; >CL in CL'; #E destruct2450  #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct2451 whd in CL CL'; >CL in CL'; #E destruct2452 ] qed.2453 2454 let rec tal_pc_list_succs ge fl s1 s22455 (tal: trace_any_label (RTLabs_status ge) fl s1 s2)2456 on tal : good_pc_list ge (state_fn … s1) (tal_pc_list (RTLabs_status ge) fl s1 s2 tal) ≝2457 ?.2458 cases tal2459 [ #s1' #s2' #EX #CL #CS whd in ⊢ (???%); @g_pc_end2460  #s1' #s2' #EX #CL @g_pc_end2461  #pre #start #final #EX #CL #AF #tlr #CS @g_pc_end2462  #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal'2463 whd in ⊢ (???%); lapply (declassify_pc' … EX CL) * * [2: #ret ] * #fn2 #PC >PC2464 [ cases (pc_after_return … AF PC) #fn' * * #SF #SF' #PC'2465 lapply (tal_pc_list_succs … tal')2466 cases (tal_pc_list_start … tal')2467 #tl' #E >E >PC' >SF' #IH >SF @g_pc_cret @IH2468  cases (pc_after_return … AF PC) >(tal_not_final … tal') #SF'2469 cases (SF' ?) %2470 ]2471  #fl' #pre #init #end #EX #tal' #CL #CS2472 whd in ⊢ (???%);2473 lapply (tal_pc_list_succs … tal')2474 cases (tal_pc_list_start … tal')2475 #tl' #E >E #IH2476 inversion (eval_preserves_ext … EX)2477 [ #ge' #f #f' #fs #m #m' * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #_ destruct2478 cases EX #tr * #EV #NX2479 cases (eval_successor … EV)2480 [ * #CL' cases (State_not_callreturn … CL')2481  * #l * #AS #SC2482 @(g_pc_step … (lookup_present … (next_ok f)))2483 [ whd in ⊢ (??%?); cases M #FFP #M >FFP2484 whd in ⊢ (??%?); //2485  whd in AS:(??%?); destruct @Exists_memb @SC2486  assumption2487 ]2488 ]2489  #ge' #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #_ destruct2490 cases EX #tr * #EV #NX2491 cases (eval_successor … EV)2492 [ * #CL' normalize in CL'; destruct2493  * #l * #AS #SC2494 @(g_pc_call … (lookup_present … (next_ok f)))2495 [ whd in ⊢ (??%?); cases M #FFP #M >FFP2496 whd in ⊢ (??%?); //2497  whd in AS:(??%?); destruct @Exists_memb @SC2498  assumption2499 ]2500 ]2501  #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #_ destruct2502 normalize in CL; destruct2503  #ge' #f #fs #m #rtv #dst #m' #fn * [2: #fn' #S ] #M #M' #E1 #E2 #E3 #_ destruct2504 cases EX #tr * #EV #NX2505 cases (eval_successor … EV)2506 [ 1,3: * #CL' #SC2507 cases (tal_return … tal') [2,4: % ]2508 #EX' * #CL'' * #FL #TAL' destruct whd in E:(??%%); destruct2509 @(g_pc_return … (lookup_present … (next_ok f)))2510 [ 1,3: whd in ⊢ (??%?); cases M #FFP #M >FFP2511 whd in ⊢ (??%?); //2512  2,4: whd in AS:(??%?); destruct @SC2513 ]2514  *: * #l * whd in ⊢ (??%% → ?); #E destruct2515 ]2516  #ge' #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #_ destruct2517 normalize in CL; destruct2518  #ge' #r #dst #m #M #M' #E1 #E2 #E3 #_ destruct2519 normalize in CL; destruct2520 ]2521 ] qed.2522 2523 let rec labels_of_pcs (l:list RTLabs_pc) : list label ≝2524 match l with2525 [ nil ⇒ [ ]2526  cons h t ⇒2527 match h with2528 [ rapc_state _ l ⇒ [l]2529  rapc_call l _ ⇒ match l with [ Some l ⇒ [l]  None ⇒ [ ]]2530  _ ⇒ [ ]2531 ] @ labels_of_pcs t2532 ].2533 2534 inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝2535  gl_end : bad_label_list g head head2536  gl_step : ∀l1,l2,H.2537 l2 ∈ successors (lookup_present … g l1 H) →2538 ¬ is_cost_label (lookup_present … g l1 H) →2539 bad_label_list g head l2 →2540 bad_label_list g head l1.2541 2542 inductive pc_label : RTLabs_pc → label → Prop ≝2543  pl_state : ∀fn,l. pc_label (rapc_state fn l) l2544  pl_call : ∀l,fn. pc_label (rapc_call (Some ? l) fn) l.2545 2546 discriminator option.2547 2548 lemma pc_label_eq : ∀pc,l1,l2.2549 pc_label pc l1 →2550 pc_label pc l2 →2551 l1 = l2.2552 #pcx #l1x #l2 * #A #B #H inversion H #C #D #E1 #E2 #E3 destruct %2553 qed.2554 2555 lemma pc_label_call_eq : ∀l,fn,l'.2556 pc_label (rapc_call (Some ? l) fn) l' →2557 l = l'.2558 #l #fn #l' #PC inversion PC2559 #a #b #E1 #E2 #E3 destruct2560 %2561 qed.2562 2563 2564 inductive graph_fn (ge:genv) : option block → graph statement → Prop ≝2565  gf : ∀b,fn.2566 find_funct_ptr … ge b = Some ? (Internal ? fn) →2567 graph_fn ge (Some ? b) (f_graph … fn).2568 2569 lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.2570 graph_fn ge (state_fn ge (mk_RTLabs_state ge (State f fs m) S M)) g →2571 g = f_graph (func f).2572 #ge #f #fs #m * [*] #fn #S * #FFP #M #g #G2573 inversion G2574 #b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct2575 %2576 qed.2577 2578 lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.2579 let s ≝ mk_RTLabs_state ge (State f fs m) S M in2580 ∀EV:eval_statement ge s = Value … 〈tr,s'〉.2581 actual_successor s' = Some ? l →2582 state_fn ge s = state_fn ge (next_state ge s s' tr EV).2583 #ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS2584 change with (Ras_state ? (next_state ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);2585 inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_state ge (State f fs m) ? M) … EV))2586 [ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %2587  #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %2588  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct2589  #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct2590 >H33 in AS; normalize #AS destruct2591  #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct2592  #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct2593 ] qed.2594 2595 lemma pc_after_return' : ∀ge,pre,post,CL,ret,callee.2596 as_after_return (RTLabs_status ge) «pre,CL» post →2597 as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →2598 match ret with2599 [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?2600  Some retl ⇒2601 state_fn … pre = state_fn … post ∧2602 pc_label (as_pc_of (RTLabs_status ge) post) retl2603 ].2604 #ge #pre #post #CL #ret #callee #AF2605 cases pre in CL AF ⊢ %;2606 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?);2607 cases (lookup_present ???? (next_ok f)) in CL;2608 normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct2609  #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL2610  #ret #dst #fs #m #S #M #CL normalize in CL; destruct2611  #r #S #M #CL normalize in CL; destruct2612 ]2613 cases post2614 * [ #postf #postfs #postm * [*] #fn' #S' #M'2615  5: #postf #postfs #postm * [*] #fn' #S' #M' *2616  2,6: #A #B #C #D #E #F #G *2617  3,7: #A #B #C #D #E #F *2618  #r #S' #M' #AF whd in AF; destruct2619  #r #S' #M'2620 ]2621 #AF #PC normalize in PC; destruct whd2622 [ cases AF * #A #B #C destruct % [ %  normalize >A // ]2623  % #E normalize in E; destruct2624 ] qed.2625 2328 2626 2329 lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_state ge. … … 2644 2347 ] qed. 2645 2348 2349 lemma State_not_callreturn : ∀f,fs,m,cl. 2350 RTLabs_classify (State f fs m) = cl → 2351 match cl with 2352 [ cl_return ⇒ False 2353  cl_call ⇒ False 2354  _ ⇒ True 2355 ]. 2356 #f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?); 2357 cases (lookup_present … (next_ok f)) // 2358 qed. 2359 2360 (* And some about traces *) 2361 2362 lemma tal_not_final : ∀ge,fl,s1,s2. 2363 ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2. 2364 RTLabs_is_final (Ras_state … s1) = None ?. 2365 #ge #flx #s1x #s2x * 2366 [ #s1 #s2 * #tr * #EX #NX #CL #CS 2367  #s1 #s2 * #tr * #EX #NX #CL 2368  #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS 2369  #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal 2370  #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS 2371 ] @(step_not_final … EX) 2372 qed. 2373 2374 (* invert traces ending in a return *) 2375 2376 lemma tal_return : ∀ge,fl,s1,s2. 2377 as_classifier (RTLabs_status ge) s1 cl_return → 2378 ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2. 2379 ∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL. 2380 #ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal) 2381 [ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct 2382 whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct 2383  #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct 2384 %{EX} %{CL} % % 2385  #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥ 2386 whd in CL CL'; >CL in CL'; #E destruct 2387  #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct 2388 whd in CL CL'; >CL in CL'; #E destruct 2389  #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct 2390 whd in CL CL'; >CL in CL'; #E destruct 2391 ] qed. 2392 2393 (* TODO: move *) 2394 lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S. 2395 Exists S (λy. y = x) l → 2396 x ∈ l. 2397 #S #x #l elim l 2398 [ // 2399  #h #t #IH 2400 normalize lapply (eqb_true … x h) 2401 cases (x==h) * 2402 [ #E #_ >(E (refl ??)) // 2403  #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct 2404  #H @IH @H 2405 ] 2406 ] 2407 ] qed. 2408 2409 (* We aim to extract a loop without a cost label to contradict the reappearance 2410 of a pc within a trace_any_label. This data structure represents the tail 2411 of a loop purely in terms of the RTLabs function body graph. *) 2412 2413 inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝ 2414  gl_end : bad_label_list g head head 2415  gl_step : ∀l1,l2,H. 2416 l2 ∈ successors (lookup_present … g l1 H) → 2417 ¬ is_cost_label (lookup_present … g l1 H) → 2418 bad_label_list g head l2 → 2419 bad_label_list g head l1. 2420 2421 (* We need to link the pcs, states of the semantics with the labels and graphs 2422 of the syntax. *) 2423 2424 inductive pc_label : RTLabs_pc → label → Prop ≝ 2425  pl_state : ∀fn,l. pc_label (rapc_state fn l) l 2426  pl_call : ∀l,fn. pc_label (rapc_call (Some ? l) fn) l. 2427 2428 discriminator option. 2429 2430 lemma pc_label_eq : ∀pc,l1,l2. 2431 pc_label pc l1 → 2432 pc_label pc l2 → 2433 l1 = l2. 2434 #pcx #l1x #l2 * #A #B #H inversion H #C #D #E1 #E2 #E3 destruct % 2435 qed. 2436 2437 lemma pc_label_call_eq : ∀l,fn,l'. 2438 pc_label (rapc_call (Some ? l) fn) l' → 2439 l = l'. 2440 #l #fn #l' #PC inversion PC 2441 #a #b #E1 #E2 #E3 destruct 2442 % 2443 qed. 2444 2445 inductive graph_fn (ge:genv) : option block → graph statement → Prop ≝ 2446  gf : ∀b,fn. 2447 find_funct_ptr … ge b = Some ? (Internal ? fn) → 2448 graph_fn ge (Some ? b) (f_graph … fn). 2449 2450 lemma graph_fn_state : ∀ge,f,fs,m,S,M,g. 2451 graph_fn ge (state_fn ge (mk_RTLabs_state ge (State f fs m) S M)) g → 2452 g = f_graph (func f). 2453 #ge #f #fs #m * [*] #fn #S * #FFP #M #g #G 2454 inversion G 2455 #b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct 2456 % 2457 qed. 2458 2459 lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l. 2460 let s ≝ mk_RTLabs_state ge (State f fs m) S M in 2461 ∀EV:eval_statement ge s = Value … 〈tr,s'〉. 2462 actual_successor s' = Some ? l → 2463 state_fn ge s = state_fn ge (next_state ge s s' tr EV). 2464 #ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS 2465 change with (Ras_state ? (next_state ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?); 2466 inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_state ge (State f fs m) ? M) … EV)) 2467 [ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct % 2468  #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct % 2469  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct 2470  #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct 2471 >H33 in AS; normalize #AS destruct 2472  #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct 2473  #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct 2474 ] qed. 2475 2476 lemma pc_after_return' : ∀ge,pre,post,CL,ret,callee. 2477 as_after_return (RTLabs_status ge) «pre,CL» post → 2478 as_pc_of (RTLabs_status ge) pre = rapc_call ret callee → 2479 match ret with 2480 [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ? 2481  Some retl ⇒ 2482 state_fn … pre = state_fn … post ∧ 2483 pc_label (as_pc_of (RTLabs_status ge) post) retl 2484 ]. 2485 #ge #pre #post #CL #ret #callee #AF 2486 cases pre in CL AF ⊢ %; 2487 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); 2488 cases (lookup_present ???? (next_ok f)) in CL; 2489 normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct 2490  #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL 2491  #ret #dst #fs #m #S #M #CL normalize in CL; destruct 2492  #r #S #M #CL normalize in CL; destruct 2493 ] 2494 cases post 2495 * [ #postf #postfs #postm * [*] #fn' #S' #M' 2496  5: #postf #postfs #postm * [*] #fn' #S' #M' * 2497  2,6: #A #B #C #D #E #F #G * 2498  3,7: #A #B #C #D #E #F * 2499  #r #S' #M' #AF whd in AF; destruct 2500  #r #S' #M' 2501 ] 2502 #AF #PC normalize in PC; destruct whd 2503 [ cases AF * #A #B #C destruct % [ %  normalize >A // ] 2504  % #E normalize in E; destruct 2505 ] qed. 2506 2646 2507 lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_state ge. ∀l. 2647 2508 actual_successor s = Some ? l → … … 2656 2517 2657 2518 include alias "utilities/deqsets.ma". 2519 2520 (* Build the tail of the "bad" loop using the reappearance of the original pc, 2521 ignoring the rest of the trace_any_label once we see that pc. *) 2658 2522 2659 2523 let rec tal_pc_loop_tail ge flX s1X s2X … … 2719 2583 ] qed. 2720 2584 2721 (* For the first step just get a bound after the step; we don't care what it is, 2585 (* Some inversion lemmas on the bounds. 2586 2587 For the first step just get a bound after the step; we don't care what it is, 2722 2588 just that it exists. *) 2723 2589 … … 2766 2632 #g #l1 #l2 * /2/ 2767 2633 qed. 2634 2635 (* Show that a bad_label_list is incompatible with a bound on the number of 2636 instructions to a cost label, by induction on the bound and the invariant 2637 that none of the instructions involved are a cost label. *) 2768 2638 2769 2639 lemma loop_soundness_contradiction : ∀g,l1,l2,H1. … … 2798 2668 ] qed. 2799 2669 2800 2670 (* Combine the above results to show that the pc of a normal instruction 2671 execution state can't be repeated within a trace_any_label. *) 2801 2672 2802 2673 lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_state ge. ∀fl,tal. … … 2845 2716 ] qed. 2846 2717 2847 lemma soundly_step : ∀ge,s1,s2. 2848 soundly_labelled_ge ge → 2849 as_execute (RTLabs_status ge) s1 s2 → 2850 soundly_labelled_state (Ras_state … s1) → 2851 soundly_labelled_state (Ras_state … s2). 2852 #ge #s1 #s2 #GE * #tr * #EX #NX 2853 @(soundly_labelled_state_step … GE … EX) 2854 qed. 2718 (* We need a similar result for call states. We'll do this by showing that 2719 the state following the call state is a normal instruction state and using 2720 the previous result. *) 2855 2721 2856 2722 lemma pc_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4. … … 2909 2775 qed. 2910 2776 2911 2912 2913 (* Show call case by reduction to the next step. *)2914 (*2915 lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal.2916 as_execute (RTLabs_status ge) s1 s1' →2917 as_after_return (RTLabs_status ge) «s1,CL» s2 →2918 as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s4 (tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX2 tal CL2 CS3) →2919 ∃s3,EX,CL',CS,tal'.2920 tal = tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX tal' CL' CS ∧2921 bool_to_Prop (as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal').2922 *)2923 2924 2777 lemma cost_labels_are_other : ∀ge,s. 2925 2778 as_costed (RTLabs_status ge) s → … … 2997 2850  #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 destruct 2998 2851 ] qed. 2852 2853 (* The main part of the proof is to walk down the trace_any_label and find the 2854 repeated call state, then show that its successor appears as well. *) 2999 2855 3000 2856 let rec pc_after_call_repeats_aux ge s1 s1' s2 s3 s4 CL1 fl tal … … 3048 2904 ] 3049 2905 ] qed. 2906 2907 (* Then we can start the proof by finding the original successor state... *) 3050 2908 3051 2909 lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal. … … 3101 2959 qed. 3102 2960 2961 (* And then we get our counterpart to no_loops_in_tal for calls: *) 2962 3103 2963 lemma no_repeats_of_calls : ∀ge,pre,start,after,final,fl,CL. 3104 2964 ∀tal:trace_any_label (RTLabs_status ge) fl after final. … … 3116 2976 qed. 3117 2977 3118 2978 (* Show that if a state is soundly labelled, then so are the states following 2979 it in a trace. *) 2980 2981 lemma soundly_step : ∀ge,s1,s2. 2982 soundly_labelled_ge ge → 2983 as_execute (RTLabs_status ge) s1 s2 → 2984 soundly_labelled_state (Ras_state … s1) → 2985 soundly_labelled_state (Ras_state … s2). 2986 #ge #s1 #s2 #GE * #tr * #EX #NX 2987 @(soundly_labelled_state_step … GE … EX) 2988 qed. 3119 2989 3120 2990 let rec tlr_sound ge s1 s2 … … 3146 3016 ]. 3147 3017 3018 (* And join everything up to show that soundly labelled states give unrepeating 3019 traces. *) 3148 3020 3149 3021 let rec tlr_sound_unrepeating ge
Note: See TracChangeset
for help on using the changeset viewer.