Changeset 2299 for src/RTLabs
 Timestamp:
 Aug 21, 2012, 7:00:42 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2297 r2299 2300 2300 2301 2301 inductive good_pc_list (ge:genv) : option block → list (as_pc (RTLabs_status ge)) → Prop ≝ 2302  g_pc_end : ∀pc,b. good_pc_list ge b [pc] 2302  g_pc_end : ∀pc,b. 2303 good_pc_list ge b [pc] 2303 2304  g_pc_step : ∀b,l1,st,l2,tl. 2304 2305 genv_lookup ge b l1 = Some ? st → … … 2393 2394 qed. 2394 2395 2395 lemma tal_pc_list_start : ∀ge,fl,s1,s2. ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.2396 ∃tl. tal_pc_list (RTLabs_status ge) … tal = (as_pc_of (RTLabs_status ge) s1)::tl.2397 #ge #fl0 #s10 #s20 *2398 [ #s1 #s2 #EX #CL #CS2399  #s1 #s2 #EX #CL2400  #s1 #s2 #s3 #EX #CL #AF #tlr #CS2401  #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal2402  #fl #s1 #s2 #s3 #EX #tal #CL #CS2403 ] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: %  *: skip ]2404 qed.2405 2406 2396 lemma tal_not_final : ∀ge,fl,s1,s2. 2407 2397 ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2. … … 2530 2520 ] 2531 2521 ] qed. 2522 2523 let rec labels_of_pcs (l:list RTLabs_pc) : list label ≝ 2524 match l with 2525 [ nil ⇒ [ ] 2526  cons h t ⇒ 2527 match h with 2528 [ rapc_state _ l ⇒ [l] 2529  rapc_call l _ ⇒ match l with [ Some l ⇒ [l]  None ⇒ [ ]] 2530  _ ⇒ [ ] 2531 ] @ labels_of_pcs t 2532 ]. 2533 2534 inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝ 2535  gl_end : bad_label_list g head head 2536  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) l 2544  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 PC 2559 #a #b #E1 #E2 #E3 destruct 2560 % 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 #G 2573 inversion G 2574 #b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct 2575 % 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 in 2580 ∀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 #AS 2584 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 destruct 2589  #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct 2590 >H33 in AS; normalize #AS destruct 2591  #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct 2592  #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct 2593 ] 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 with 2599 [ 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) retl 2603 ]. 2604 #ge #pre #post #CL #ret #callee #AF 2605 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 destruct 2609  #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL 2610  #ret #dst #fs #m #S #M #CL normalize in CL; destruct 2611  #r #S #M #CL normalize in CL; destruct 2612 ] 2613 cases post 2614 * [ #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; destruct 2619  #r #S' #M' 2620 ] 2621 #AF #PC normalize in PC; destruct whd 2622 [ cases AF * #A #B #C destruct % [ %  normalize >A // ] 2623  % #E normalize in E; destruct 2624 ] qed. 2625 2626 lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_state ge. 2627 as_execute (RTLabs_status ge) s s' → 2628 RTLabs_classify s = cl → 2629 match cl with 2630 [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_state ge (Callstate fd args dst fs m) S M 2631  cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_state ge (Returnstate ret dst fs m) S M 2632  _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_state ge (State f fs m) S M 2633 ] . 2634 #ge #cl * * [ #f #fs #m  #fd #args #dst #fs #m  #ret #dst #fs #m  #r ] 2635 #S #M * #s' #S' #M' #EX #CL 2636 whd in CL:(??%?); 2637 [ cut (cl = cl_other ∨ cl = cl_jump) 2638 [ cases (lookup_present … (next_ok … f)) in CL; 2639 normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ] 2640 * #E >E %{f} %{fs} %{m} %{S} %{M} % 2641  <CL %{fd} %{args} %{dst} %{fs} %{m} %{S} %{M} % 2642  <CL %{ret} %{dst} %{fs} %{m} %{S} %{M} % 2643  @⊥ cases EX #tr * #EV #_ normalize in EV; destruct 2644 ] qed. 2645 2646 lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_state ge. ∀l. 2647 actual_successor s = Some ? l → 2648 pc_label (as_pc_of (RTLabs_status ge) s) l. 2649 #ge * * 2650 [ #f #fs #m * [*] #fn #S #M #l #AS 2651  #fd #args #dst * [2: #f #fs] #m * [1,3:*] #fn #S #M #l #AS 2652  #ret #dst #fs #m #S #M #l #AS 2653  #r #S #M #l #AS 2654 ] whd in AS:(??%?); destruct // 2655 qed. 2656 2657 include alias "utilities/deqsets.ma". 2658 2659 let rec tal_pc_loop_tail ge flX s1X s2X 2660 (pc:as_pc (RTLabs_status ge)) g l 2661 (PC0:pc_label pc l) 2662 (tal: trace_any_label (RTLabs_status ge) flX s1X s2X) 2663 on tal : 2664 ∀l1. 2665 pc_label (as_pc_of (RTLabs_status ge) s1X) l1 → 2666 graph_fn ge (state_fn … s1X) g → 2667 Not (as_costed (RTLabs_status ge) s1X) → 2668 pc ∈ tal_pc_list (RTLabs_status ge) flX s1X s2X tal → 2669 bad_label_list g l l1 ≝ ?. 2670 cases tal 2671 [ #s1 #s2 #EX #CL #CS 2672 #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct 2673 >(pc_label_eq … PC0 PC1) %1 2674  #s1 #s2 #EX #CL 2675 #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct 2676 >(pc_label_eq … PC0 PC1) %1 2677  #pre #start #final #EX #CL #AF #tlr #CS 2678 #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct 2679 >(pc_label_eq … PC0 PC1) %1 2680  #fl #pre #start #after #final #EX #CL #AF #tlr #CS #tal' 2681 #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim 2682 [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1 2683  #NE #IN 2684 lapply (declassify_pc' … EX CL) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC1 2685 [ cases (pc_after_return' … AF PC) #SF #PC' >SF in G; #G 2686 lapply (pc_label_call_eq … PC1) #E destruct 2687 @(tal_pc_loop_tail … PC0 tal' l1 PC' G CS IN) 2688  @⊥ inversion PC1 #a #b #E1 #E2 #E3 destruct 2689 ] 2690 ] 2691  #fl #pre #init #end #EX #tal' #CL #CS 2692 #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim 2693 [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1 2694  #NE #IN 2695 cases (declassify_state … EX CL) 2696 #f * #fs * #m * #S * #M #E destruct 2697 cut (l1 = next f) 2698 [ whd in PC1:(?%?); cases S in M PC1; [*] #fn #S #M whd in ⊢ (?%? → ?); #PC1 2699 inversion PC1 normalize #a #b #E1 #E2 #E3 destruct % ] #E destruct 2700 cases EX #tr * #EV #NX 2701 cases (eval_successor … EV) 2702 [ * #CL' @⊥ cases (tal_return … CL' tal') #EX' * #CL'' * #E1 #E2 destruct 2703 lapply (memb_single … IN) @(declassify_pc … EX' CL'') whd 2704 #fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct 2705  * #l' * #AS #SC 2706 lapply (graph_fn_state … G) #E destruct 2707 @(gl_step … l') 2708 [ @(next_ok f) 2709  @Exists_memb @SC 2710  @notb_Prop @(not_to_not … NCS) #ISL @(proj1 ?? (RTLabs_costed ??)) 2711 @ISL 2712  @(tal_pc_loop_tail … PC0 tal' … (actual_successor_pc_label … AS)) 2713 [ <NX in AS ⊢ %; #AS <(state_fn_next … EV AS) @G 2714  *: // 2715 ] 2716 ] 2717 ] 2718 ] 2719 ] qed. 2720 2721 (* For the first step just get a bound after the step; we don't care what it is, 2722 just that it exists. *) 2723 2724 lemma bound_step1 : ∀g,l1,n. 2725 bound_on_instrs_to_cost g l1 n → 2726 ∀l2,H. Exists ? (λl.l = l2) (successors (lookup_present … g l1 H)) → 2727 ∃m. bound_on_instrs_to_cost' g l2 m. 2728 #g #l1X #nX * #l #n #H #EX #l2 #H' #EX' %{n} @EX @EX' 2729 qed. 2730 2731 lemma bound_zero1 : ∀g,l. 2732 ¬ bound_on_instrs_to_cost g l 0. 2733 #g #l % #B lapply (refl ? O) cases B in ⊢ (???% → ?); 2734 #l' #n #H #_ whd in ⊢ (???% → ?); #E destruct 2735 qed. 2736 2737 lemma bound_zero : ∀g,l. 2738 bound_on_instrs_to_cost' g l 0 → 2739 ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)). 2740 #g #l #B 2741 @(match B return λl,n,B. n = O → ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)) with 2742 [ boitc_here l n H CS ⇒ ? 2743  boitc_later _ _ _ _ B' ⇒ ? 2744 ] (refl ? O)) 2745 [ #E >E %{H} @CS 2746  #E >E in B'; #B' @⊥ @(absurd … B' (bound_zero1 …)) 2747 ] qed. 2748 2749 lemma bound_step : ∀g,l,n. 2750 bound_on_instrs_to_cost' g l (S n) → 2751 ∃H. (bool_to_Prop (is_cost_label (lookup_present … g l H)) ∨ 2752 (let stmt ≝ lookup_present … g l H in 2753 ∀l'. Exists label (λl0. l0 = l') (successors stmt) → 2754 bound_on_instrs_to_cost' g l' n)). 2755 #g #lX #n #B lapply (refl ? (S n)) cases B in ⊢ (???% → %); 2756 [ #l #n #H #CS #E %{H} %1 @CS 2757  #l #m #H #CS * 2758 #l' #n' #H' #EX #E destruct %{H'} %2 2759 #l'' #EX' @EX @EX' 2760 ] qed. 2761 2762 lemma bad_label_list_no_cost : ∀g,l1,l2. 2763 bad_label_list g l1 l2 → 2764 ∀H1. ¬ is_cost_label (lookup_present … g l1 H1) → 2765 ∃H2. bool_to_Prop (¬ is_cost_label (lookup_present … g l2 H2)). 2766 #g #l1 #l2 * /2/ 2767 qed. 2768 2769 lemma loop_soundness_contradiction : ∀g,l1,l2,H1. 2770 Exists ? (λl.l = l2) (successors (lookup_present … g l1 H1)) → 2771 ¬ is_cost_label (lookup_present … g l1 H1) → 2772 bad_label_list g l1 l2 → 2773 ∀n,l'. 2774 bad_label_list g l1 l' → 2775 ¬ bound_on_instrs_to_cost' g l' n. 2776 #g #l1 #l2 #H1 #SC1 #NCS1 #BLL2 2777 #n elim n 2778 [ #l #BLL % #BOUND 2779 cases (bound_zero … BOUND) #H' #ICS 2780 cases (bad_label_list_no_cost … BLL H1 NCS1) #H'' 2781 >ICS * 2782  #m #IH #l #BLL % #BOUND 2783 cases (bound_step … BOUND) #H' * 2784 [ #ICS cases (bad_label_list_no_cost … BLL H1 NCS1) #H'' >ICS * 2785  #EX_BOUND inversion BLL 2786 [ #E1 #E2 destruct 2787 lapply (IH l2 BLL2) 2788 lapply (EX_BOUND … SC1) 2789 @absurd 2790  #l3 #l4 #H3 #SC2 #NCS3 #BLL4 #_ #E1 #E2 destruct 2791 lapply (IH l4 BLL4) 2792 cut (Exists ? (λl.l=l4) (successors (lookup_present … H3))) 2793 [ cases (memb_exists … SC2) #left * #right #E >E @Exists_mid % ] 2794 #SC2' lapply (EX_BOUND … SC2') 2795 @absurd 2796 ] 2797 ] 2798 ] qed. 2799 2800 2801 2802 lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_state ge. ∀fl,tal. 2803 soundly_labelled_state s1 → 2804 RTLabs_classify s1 = cl_other → 2805 as_execute (RTLabs_status ge) s1 s2 → 2806 ¬ as_costed (RTLabs_status ge) s2 → 2807 ¬ as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s3 tal. 2808 #ge #s1 #s2 #s3 #fl #tal #S1 #CL #EX #CS2 cases (declassify_state … EX CL) 2809 #f * #fs * #m * * [* *] #fn #S * * #FFP #M #E destruct 2810 cases EX #tr * #EV #NX 2811 cases (eval_successor … EV) 2812 [ * #CL2 #SC 2813 cases (tal_return … CL2 tal) #EX2 * #CL2' * #E1 #E2 destruct 2814 @notb_Prop % whd in match (tal_pc_list ?????); #IN 2815 lapply (memb_single … IN) cases (declassify_state … EX2 CL2) 2816 #ret * #dst * #fs2 * #m2 * * [2: #fn2 #S2] * #M2 #E destruct 2817 normalize #E destruct 2818  * #l2 * #AS2 #SC1 @notb_Prop % #IN 2819 (* Two cases: either s1 is a cost label, and it's pc's appearence later on 2820 is impossible because nothing later in tal can be a cost label; or it 2821 isn't and we get a loop of successor instruction labels that breaks the 2822 soundness of the cost labelling. *) 2823 cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_state ge (State f fs m) (fn::S) (conj ?? FFP M))) 2824 [ * #H @H 2825 cases (memb_exists … IN) #left * #right #E 2826 @(All_split … (tal_tail_not_costed … tal CS2) … E) 2827  (* Now show that the loop invalidates soundness. *) 2828 cut (pc_label (as_pc_of (RTLabs_status ge) (mk_RTLabs_state ge (State f fs m) (fn::S) (conj ?? FFP M))) (next f)) 2829 [ %1 ] #PC1 2830 cut (pc_label (as_pc_of (RTLabs_status ge) s2) l2) 2831 [ /2/ ] #PC2 2832 lapply (tal_pc_loop_tail … (f_graph (func f)) … PC1 … PC2 … CS2 IN) 2833 [ <NX <(state_fn_next … EV AS2) % // ] 2834 cases S1 #SLF #_ cases (SLF (next f) (next_ok f)) 2835 #bound1 #BOUND1 #BLL #CS1 2836 cases (bound_step1 … BOUND1 … SC1) 2837 #bound2 #BOUND2 @(absurd … BOUND2) 2838 @(loop_soundness_contradiction … BLL … BLL) 2839 [ @(next_ok f) 2840  @SC1 2841  @notb_Prop @(not_to_not … CS1) #CS 2842 @(proj1 … (RTLabs_costed …)) @CS 2843 ] 2844 ] 2845 ] qed. 2846 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. 2855 2856 lemma pc_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4. 2857 as_after_return (RTLabs_status ge) «s1,CL1» s3 → 2858 as_after_return (RTLabs_status ge) «s2,CL2» s4 → 2859 as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 → 2860 state_fn … s1 = state_fn … s2 → 2861 as_pc_of (RTLabs_status ge) s3 = as_pc_of (RTLabs_status ge) s4. 2862 #ge * #s1 #S1 #M1 #CL1 2863 cases (rtlabs_call_inv … CL1) #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct 2864 * #s2 #S2 #M2 #CL2 2865 cases (rtlabs_call_inv … CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct 2866 * * [ #f3 #fs3 #m3 #S3 #M3  #a #b #c #d #e #f #g #h *  #a #b #c #d #e #f #g *  #r3 #S3 #M3 ] 2867 * * [ 1,5: #f4 #fs4 #m4 #S4 #M4  2,6: #a #b #c #d #e #f #g #h *  3,7: #a #b #c #d #e #f #g *  4,8: #r4 #S4 #M4 ] 2868 whd in ⊢ (% → ?); 2869 [ 1,3: cases fs1 in M1 ⊢ %; [1,3: #M *] #f1' #fs1 cases S1 [1,3:*] #fn1 * [1,3:* #X *] #fn1' #S1' #M1 whd in ⊢ (% → ?); 2870 * * #N1 #F1 #STK1 2871 whd in STK1 ⊢ (% → ?); 2872 [ cases fs2 in M2 ⊢ %; [ #M2 * ] #f2' #fs2 cases S2 [*] #fn2 * [* #X *] #fn2 #S2' #M2 * * #N2 #F2 #STK2 2873 normalize in ⊢ (% → % → ?); #E1 #E2 2874 cases S3 in M3 STK1 ⊢ %; [ * ] #fn3 #S3' #M3 #STK1 2875 cases S4 in M4 STK2 ⊢ %; [ * ] #fn4 #S4' #M4 #STK2 2876 whd in ⊢ (??%%); <N2 <N1 destruct >e1 % 2877  #E destruct whd in ⊢ (??%% → ??%% → ?); cases S2 in M2 ⊢ %; [ * ] #fn2 #S2' #M2 normalize in ⊢ (% → ?); 2878 #X destruct 2879 ] 2880  #F destruct whd in ⊢ (% → ?); cases fs2 in M2 ⊢ %; [ #M *] #f2 #fs2' cases S2 [*] #fn2 #S2' #M2 * * #N2 #F2 #STK2 2881 cases S1 in M1 ⊢ %; [*] #fn1 #S1' #M1 2882 normalize in ⊢ (% → ?); #E destruct 2883  #F destruct whd in ⊢ (% → ?); #F destruct #_ #_ % 2884 ] qed. 2885 2886 lemma eq_pc_eq_classify : ∀ge,s1,s2. 2887 as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 → 2888 RTLabs_classify (Ras_state … s1) = RTLabs_classify (Ras_state … s2). 2889 #ge 2890 * * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1  #fd1 #args1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1  #ret1 #dst1 #fs1 #m1 #S1 #M1  #r1 * [2: #fn1 #S1 #E normalize in E; destruct] #M1 ] 2891 * * [ 1,5,9,13: * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2  2,6,10,14: #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2  3,7,11,15: #ret2 #dst2 #fs2 #m2 #S2 #M2  4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ] 2892 whd in ⊢ (??%% → ?); #E destruct try % 2893 [ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%); 2894 cases (lookup_present … next2 nok1) 2895 normalize // 2896  2,3,7: cases S1 in M1 E; [2,4,6:#fn1' #S1'] #M1 whd in ⊢ (??%% → ?); #E destruct 2897  4,5,6: cases S2 in M2 E; [2,4,6:#fn2' #S2'] #M2 whd in ⊢ (??%% → ?); #E destruct 2898 ] qed. 2899 2900 lemma classify_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4. 2901 as_after_return (RTLabs_status ge) «s1,CL1» s3 → 2902 as_after_return (RTLabs_status ge) «s2,CL2» s4 → 2903 as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 → 2904 state_fn … s1 = state_fn … s2 → 2905 RTLabs_classify (Ras_state … s3) = RTLabs_classify (Ras_state … s4). 2906 #ge #s1 #CL1 #s2 #CL2 #s3 #s4 #AF1 #AF2 #PC #FN 2907 @eq_pc_eq_classify 2908 @(pc_after_return_eq … AF1 AF2 PC FN) 2909 qed. 2910 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 lemma cost_labels_are_other : ∀ge,s. 2925 as_costed (RTLabs_status ge) s → 2926 RTLabs_classify (Ras_state … s) = cl_other. 2927 #ge * * [ #f #fs #m #S #M  #fd #args #dst #fs #m #S #M  #ret #dst #fs #m #S #M  #r #S #M ] 2928 #CS lapply (proj2 … (RTLabs_costed …) … CS) 2929 whd in ⊢ (??%? → %); 2930 [ whd in ⊢ (? → ??%?); cases (lookup_present … (next_ok f)) normalize 2931 #A try #B try #C try #D try #E try #F try #G try #H try #I destruct % 2932  *: #E destruct 2933 ] qed. 2934 2935 lemma eq_pc_cost : ∀ge,s1,s2. 2936 as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 → 2937 as_costed (RTLabs_status ge) s1 → 2938 as_costed (RTLabs_status ge) s2. 2939 #ge 2940 * * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1  #fd1 #args1 #dst1 #fs1 #m1 #S1 #M1  #ret1 #dst1 #fs1 #m1 #S1 #M1  #r1 #S1 #M1 ] 2941 [ 2,3,4: #s2 #PC #CS1 lapply (proj2 … (RTLabs_costed …) … CS1) whd in ⊢ (??%% → ?); #E destruct ] 2942 * * [ * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [*] #fn2 #S2 #M2  2,6,10,14: #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2  3,7,11,15: #ret2 #dst2 #fs2 #m2 * [2: #fn2 #S2] #M2  4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ] 2943 whd in ⊢ (??%% → ?); #E destruct 2944 #CS1 @(proj1 … (RTLabs_costed …)) lapply (proj2 … (RTLabs_costed …) … CS1) 2945 cases M1 #FFP1 #M1' cases M2 >FFP1 #E #M2' destruct #H @H 2946 qed. 2947 2948 lemma first_state_in_tal_pc_list : ∀ge,fl,s1,s2,tal. 2949 RTLabs_classify (Ras_state … s1) = cl_other → 2950 as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s1 s2 tal. 2951 #ge #flX #s1X #s2X * 2952 [ #s1 #s2 #EX * 2953 [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥ >CL in CL'; #CL' destruct 2954  #CL #CS #CL' @eq_true_to_b @memb_hd 2955 ] 2956  #s1 #s2 #EX #CL whd in CL; #CL' @⊥ >CL in CL'; #CL' destruct 2957  #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ whd in CL; >CL in CL'; #CL' destruct 2958  #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ whd in CL; >CL in CL'; #CL' destruct 2959  #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd 2960 ] qed. 2961 2962 lemma state_fn_after_return : ∀ge,pre,post,CL. 2963 as_after_return (RTLabs_status ge) «pre,CL» post → 2964 state_fn … pre = state_fn … post. 2965 #ge * #pre #preS #preM * #post #postS #postM #CL #AF 2966 cases (rtlabs_call_inv … CL) #fd * #args * #dst * #fs * #m #E destruct 2967 cases post in postM AF ⊢ %; 2968 [ #postf #postfs #postm cases postS [*] #postfn #S' #M' #AF 2969 cases preS in preM AF ⊢ %; [*] 2970 #fn * 2971 [ cases fs [ #M * ] 2972 #f #fs' * #FFP * 2973  #fn' #S cases fs [ #M * ] 2974 #f #fs' #M * * #N #F #PC destruct % 2975 ] 2976  #A #B #C #D #E #F * 2977  #A #B #C #D #E * 2978  #r #M' #AF whd in AF; destruct 2979 cases preS in preM ⊢ %; 2980 [ //  #fn * [ //  #fn' #S * #FFP * ] ] 2981 ] qed. 2982 2983 lemma state_fn_other : ∀ge,s1,s2. 2984 RTLabs_classify (Ras_state … s1) = cl_other → 2985 as_execute (RTLabs_status ge) s1 s2 → 2986 RTLabs_classify (Ras_state … s2) = cl_return ∨ 2987 state_fn … s1 = state_fn … s2. 2988 #ge #s1 #s2 #CL #EX 2989 cases (declassify_state … EX CL) 2990 #f * #fs * #m * * [**] #fn #S * #M #E destruct 2991 inversion (eval_preserves_ext … EX) 2992 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct %2 % 2993  #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct %2 % 2994  #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct 2995  #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 destruct %1 % 2996  #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct 2997  #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 destruct 2998 ] qed. 2999 3000 let rec pc_after_call_repeats_aux ge s1 s1' s2 s3 s4 CL1 fl tal 3001 (AF1:as_after_return (RTLabs_status ge) «s1,CL1» s2) 3002 (CL2:RTLabs_classify (Ras_state … s2) = cl_other) 3003 (CS2:Not (as_costed (RTLabs_status ge) s2)) 3004 (EX1:as_execute (RTLabs_status ge) s1 s1') on tal : 3005 state_fn … s1 = state_fn … s3 → 3006 as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal → 3007 as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal ≝ ?. 3008 cases tal 3009 [ #s3 #s4 #EX3 #CL3 #CS4 #FN #IN @⊥ 3010 whd in match (tal_pc_list ?????) in IN; 3011 lapply (memb_single … IN) @(declassify_pc … EX1 CL1) #caller #callee 3012 cases CL3 #CL3' @(declassify_pc … EX3 CL3') #fn #l 3013 #IN' destruct 3014  #s2 #s4 #EX2 #CL2 #FN #IN @⊥ 3015 lapply (memb_single … IN) @(declassify_pc … EX1 CL1) #caller #callee 3016 @(declassify_pc … EX2 CL2) whd #fn 3017 #IN' destruct 3018  #s3 #s3' #s4 #EX3 #CL3 #AF3 #tlr3 #CS4 #FN #IN 3019 lapply (memb_single … IN) #E 3020 lapply (pc_after_return_eq … AF1 AF3 E FN) #PC 3021 @⊥ @(absurd ?? CS2) @(eq_pc_cost … CS4) // 3022  #fl' #s3 #s3' #s3'' #s4 #EX3 #CL3 #AF3 #tlr3' #CS3'' #tal3'' #FN 3023 whd in ⊢ (?% → ?); @eqb_elim 3024 [ #PC #_ 3025 >(pc_after_return_eq … AF1 AF3 PC FN) @eq_true_to_b @memb_cons @first_state_in_tal_pc_list 3026 <(classify_after_return_eq … AF1 AF3 PC FN) assumption 3027  #NPC #IN whd in IN:(?%); @eq_true_to_b @memb_cons 3028 @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1 … IN) 3029 >FN @(state_fn_after_return … AF3) 3030 ] 3031  #fl' #s3 #s3' #s4 #EX3 #tal3' #CL3 #CS3' #FN #IN 3032 @eq_true_to_b @memb_cons 3033 @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1) 3034 [ >FN cases (state_fn_other … CL3 EX3) 3035 [ #CL3' @⊥ 3036 cases (tal_return … CL3' tal3') 3037 #EX3' * #CL3'' * #E1 #E2 destruct 3038 whd in IN:(?%); lapply IN @eqb_elim 3039 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1 >CL3 #E destruct 3040  #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1 >CL3' #E destruct 3041 ] 3042  // 3043 ] 3044  lapply IN whd in ⊢ (?% → ?); @eqb_elim 3045 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1 >CL3 #E destruct 3046  #NE #IN @IN 3047 ] 3048 ] 3049 ] qed. 3050 3051 lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal. 3052 as_execute (RTLabs_status ge) s1 s1' → 3053 as_after_return (RTLabs_status ge) «s1,CL» s2 → 3054 ¬as_costed (RTLabs_status ge) s2 → 3055 as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s4 tal → 3056 ∃s3,EX,CL',CS,tal'. 3057 tal = tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX tal' CL' CS ∧ 3058 bool_to_Prop (as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal'). 3059 #ge #s1 #s1' #CL #flX #s2X #s4X * 3060 [ #s2 #s4 #EX2 #CL2 #CS #EX1 #AF #CS2 #IN @⊥ 3061 whd in match (tal_pc_list ?????) in IN; 3062 lapply (memb_single … IN) @(declassify_pc … EX1 CL) #caller #callee 3063 cases CL2 #CL2' @(declassify_pc … EX2 CL2') #fn #l 3064 #IN' destruct 3065  #s2 #s4 #EX2 #CL2 #EX1 #AF #CS2 #IN @⊥ 3066 lapply (memb_single … IN) @(declassify_pc … EX1 CL) #caller #callee 3067 @(declassify_pc … EX2 CL2) whd #fn 3068 #IN' destruct 3069  #s2 #s3 #s4 #EX2 #CL2 #AF2 #tlr3 #CS4 #EX1 #AF1 #CS2 @⊥ 3070 cases (declassify_state … EX1 CL) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct 3071 cases (declassify_state … EX2 CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct 3072 cases AF1 3073  #fl #s2 #s3 #s3' #s4 #EX2 #CL2 #AF2 #tlr3 #CS3' #tal3' #EX1 #AF1 #CS2 @⊥ 3074 cases (declassify_state … EX1 CL) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct 3075 cases (declassify_state … EX2 CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct 3076 cases AF1 3077  #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN 3078 %{s3} %{EX2} %{CL2} %{CS3} %{tal3} % [ % ] 3079 (* Now that we've inverted the first part of the trace, look for the repeat. *) 3080 @(pc_after_call_repeats_aux … CL … AF1 CL2 CS2 EX1) 3081 [ >(state_fn_after_return … AF1) 3082 cases (state_fn_other … CL2 EX2) 3083 [ #CL3 @⊥ 3084 cases (tal_return … CL3 tal3) 3085 #EX3 * #CL3' * #E1 #E2 destruct 3086 whd in IN:(?%); lapply IN @eqb_elim 3087 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL >CL2 #E destruct 3088  #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL >CL3' #E destruct 3089 ] 3090  // 3091 ] 3092  lapply IN whd in ⊢ (?% → ?); @eqb_elim 3093 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL >CL2 #E destruct 3094  #NE #IN @IN 3095 ] 3096 ] 3097 ] qed. 3098 3099 lemma Prop_notb : ∀b:bool. notb b → Not (bool_to_Prop b). 3100 * /2/ 3101 qed. 3102 3103 lemma no_repeats_of_calls : ∀ge,pre,start,after,final,fl,CL. 3104 ∀tal:trace_any_label (RTLabs_status ge) fl after final. 3105 as_execute (RTLabs_status ge) pre start → 3106 as_after_return (RTLabs_status ge) «pre,CL» after → 3107 ¬as_costed (RTLabs_status ge) after → 3108 soundly_labelled_state (Ras_state ge after) → 3109 ¬as_pc_of (RTLabs_status ge) pre ∈ tal_pc_list (RTLabs_status ge) fl after final tal. 3110 #ge #pre #start #after #final #fl #CL #tal #EX #AF #CS #SOUND @notb_Prop % #IN 3111 cases (pc_after_call_repeats … EX AF CS IN) 3112 #s * #EX * #CL' * #CSx * #tal' * #E #IN' 3113 @(absurd ? IN') 3114 @Prop_notb 3115 @no_loops_in_tal assumption 3116 qed. 3117 3118 3119 3120 let rec tlr_sound ge s1 s2 3121 (tlr:trace_label_return (RTLabs_status ge) s1 s2) 3122 (GE:soundly_labelled_ge ge) 3123 on tlr : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝ 3124 match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) with 3125 [ tlr_base _ _ tll ⇒ λS1. tll_sound … tll GE S1 3126  tlr_step _ _ _ tll tlr' ⇒ λS1. let S2 ≝ tll_sound ge … tll GE S1 in 3127 tlr_sound … tlr' GE S2 3128 ] 3129 and tll_sound ge fl s1 s2 3130 (tll:trace_label_label (RTLabs_status ge) fl s1 s2) 3131 (GE:soundly_labelled_ge ge) 3132 on tll : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝ 3133 match tll with 3134 [ tll_base _ _ _ tal _ ⇒ tal_sound … tal GE 3135 ] 3136 and tal_sound ge fl s1 s2 3137 (tal:trace_any_label (RTLabs_status ge) fl s1 s2) 3138 (GE:soundly_labelled_ge ge) 3139 on tal : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝ 3140 match tal with 3141 [ tal_base_not_return _ _ EX _ _ ⇒ λS1. soundly_step … GE EX S1 3142  tal_base_return _ _ EX _ ⇒ λS1. soundly_step … GE EX S1 3143  tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. tlr_sound … tlr GE (soundly_step … GE EX S1) 3144  tal_step_call _ _ _ _ _ EX _ _ tlr _ tal ⇒ λS1. tal_sound … tal GE (tlr_sound … tlr GE (soundly_step … GE EX S1)) 3145  tal_step_default _ _ _ _ EX tal _ _ ⇒ λS1. tal_sound … tal GE (soundly_step … GE EX S1) 3146 ]. 3147 3148 3149 let rec tlr_sound_unrepeating ge 3150 (s1,s2:RTLabs_status ge) 3151 (GE:soundly_labelled_ge ge) 3152 (tlr:trace_label_return (RTLabs_status ge) s1 s2) 3153 on tlr : soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) … tlr ≝ 3154 match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) s1 s2 tlr with 3155 [ tlr_base _ _ tll ⇒ λS1. tll_sound_unrepeating … GE tll S1 3156  tlr_step _ _ _ tll tlr' ⇒ λS1. conj ?? (tll_sound_unrepeating ge … GE tll S1) (tlr_sound_unrepeating … GE tlr' (tll_sound … tll GE S1)) 3157 ] 3158 and tll_sound_unrepeating ge fl 3159 (s1,s2:RTLabs_status ge) 3160 (GE:soundly_labelled_ge ge) 3161 (tll:trace_label_label (RTLabs_status ge) fl s1 s2) 3162 on tll : soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) … tll ≝ 3163 match tll return λfl,s1,s2,tll. soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) fl s1 s2 tll with 3164 [ tll_base _ _ _ tal _ ⇒ tal_sound_unrepeating … GE tal 3165 ] 3166 and tal_sound_unrepeating ge fl 3167 (s1,s2:RTLabs_status ge) 3168 (GE:soundly_labelled_ge ge) 3169 (tal:trace_any_label (RTLabs_status ge) fl s1 s2) 3170 on tal : soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) … tal ≝ 3171 match tal return λfl,s1,s2,tal. soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) fl s1 s2 tal with 3172 [ tal_base_not_return _ _ EX _ _ ⇒ λS1. I 3173  tal_base_return _ _ EX _ ⇒ λS1. I 3174  tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. 3175 tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1) 3176  tal_step_call _ pre start after final EX CL AF tlr _ tal ⇒ λS1. 3177 conj ?? (conj ??? 3178 (tal_sound_unrepeating … GE tal (tlr_sound … tlr GE (soundly_step … GE EX S1)))) 3179 (tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1)) 3180  tal_step_default _ pre init end EX tal CL _ ⇒ λS1. 3181 conj ??? (tal_sound_unrepeating … GE tal (soundly_step … GE EX S1)) 3182 ]. 3183 [ @(no_repeats_of_calls … EX AF) [ assumption  3184 @(tlr_sound … tlr) [ assumption  @(soundly_step … GE EX S1) ] ] 3185  @no_loops_in_tal // 3186 ] qed. 3187
Note: See TracChangeset
for help on using the changeset viewer.