Changeset 2299


Ignore:
Timestamp:
Aug 21, 2012, 7:00:42 PM (7 years ago)
Author:
campbell
Message:

Soundly labelled RTLabs structured traces are "unrepeating".

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2297 r2299  
    23002300
    23012301inductive 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]
    23032304| g_pc_step : ∀b,l1,st,l2,tl.
    23042305    genv_lookup ge b l1 = Some ? st →
     
    23932394qed.
    23942395
    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 #CS
    2399 | #s1 #s2 #EX #CL
    2400 | #s1 #s2 #s3 #EX #CL #AF #tlr #CS
    2401 | #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
    2402 | #fl #s1 #s2 #s3 #EX #tal #CL #CS
    2403 ] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: % | *: skip ]
    2404 qed.
    2405 
    24062396lemma tal_not_final : ∀ge,fl,s1,s2.
    24072397  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
     
    25302520  ]
    25312521] qed.
     2522
     2523let rec labels_of_pcs (l:list RTLabs_pc) : list label ≝
     2524match 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
     2534inductive 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
     2542inductive 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
     2546discriminator option.
     2547
     2548lemma 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 %
     2553qed.
     2554
     2555lemma 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%
     2561qed.
     2562
     2563
     2564inductive 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
     2569lemma 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
     2573inversion G
     2574#b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct
     2575%
     2576qed.
     2577
     2578lemma 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
     2584change with (Ras_state ? (next_state ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
     2585inversion (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
     2595lemma 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
     2605cases 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  ]
     2613cases 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
     2626lemma 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
     2636whd 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
     2646lemma 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 //
     2655qed.
     2656
     2657include alias "utilities/deqsets.ma".
     2658
     2659let 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)
     2663on 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 ≝ ?.
     2670cases 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   
     2724lemma 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'
     2729qed.
     2730
     2731lemma 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
     2735qed.
     2736
     2737lemma 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
     2749lemma 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
     2762lemma 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/
     2767qed.
     2768   
     2769lemma 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
     2802lemma 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
     2810cases EX #tr * #EV #NX
     2811cases (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
     2847lemma 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)
     2854qed.
     2855
     2856lemma 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
     2863cases (rtlabs_call_inv … CL1) #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
     2864* #s2 #S2 #M2 #CL2
     2865cases (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 ]
     2868whd 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
     2886lemma 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 ]
     2892whd 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
     2900lemma 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)
     2909qed.
     2910
     2911
     2912
     2913(* Show call case by reduction to the next step. *)
     2914(*
     2915lemma 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
     2924lemma 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)
     2929whd 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
     2935lemma 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 ]
     2943whd in ⊢ (??%% → ?); #E destruct
     2944#CS1 @(proj1 … (RTLabs_costed …)) lapply (proj2 … (RTLabs_costed …) … CS1)
     2945cases M1 #FFP1 #M1' cases M2 >FFP1 #E #M2' destruct #H @H
     2946qed.
     2947
     2948lemma 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
     2962lemma 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
     2966cases (rtlabs_call_inv … CL) #fd * #args * #dst * #fs * #m #E destruct
     2967cases 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
     2983lemma 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
     2989cases (declassify_state … EX CL)
     2990#f * #fs * #m * * [**] #fn #S * #M #E destruct
     2991inversion (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
     3000let 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 ≝ ?.
     3008cases 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
     3051lemma 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
     3099lemma Prop_notb : ∀b:bool. notb b → Not (bool_to_Prop b).
     3100* /2/
     3101qed.
     3102
     3103lemma 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
     3111cases (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
     3116qed.
     3117
     3118
     3119
     3120let rec tlr_sound ge s1 s2
     3121  (tlr:trace_label_return (RTLabs_status ge) s1 s2)
     3122  (GE:soundly_labelled_ge ge)
     3123on tlr : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
     3124match 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]
     3129and tll_sound ge fl s1 s2
     3130  (tll:trace_label_label (RTLabs_status ge) fl s1 s2)
     3131  (GE:soundly_labelled_ge ge)
     3132on tll : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
     3133match tll with
     3134[ tll_base _ _ _ tal _ ⇒ tal_sound … tal GE
     3135]
     3136and tal_sound ge fl s1 s2
     3137  (tal:trace_any_label (RTLabs_status ge) fl s1 s2)
     3138  (GE:soundly_labelled_ge ge)
     3139on tal : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
     3140match 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
     3149let 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)
     3153on tlr : soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) … tlr ≝
     3154match 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]
     3158and 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)
     3162on tll : soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) … tll ≝
     3163match 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]
     3166and 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)
     3170on tal : soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) … tal ≝
     3171match 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
  • src/common/StructuredTraces.ma

    r2186 r2299  
    3232definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
    3333  λa_s,st.as_label ? st ≠ None ?.
     34
     35lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) ∨ (¬as_costed S s).
     36#S #s whd in match (as_costed S s);
     37cases (as_label S s) [ %2 % * /2/ | #c %1 % #E destruct ]
     38qed.
    3439
    3540definition as_label_safe : ∀a_s : abstract_status.
     
    181186qed.
    182187
     188lemma not_costed_no_label : ∀S,st.
     189  ¬as_costed S st →
     190  as_label_of_pc S (as_pc_of S st) = None ?.
     191#S #st * normalize cases (as_label_of_pc S ?)
     192[ // | #l #H cases (H ?) % #E destruct ]
     193qed.
     194
     195lemma tal_pc_list_start : ∀S,fl,s1,s2. ∀tal: trace_any_label S fl s1 s2.
     196  ∃tl. tal_pc_list … tal = (as_pc_of S s1)::tl.
     197#S #fl0 #s10 #s20 *
     198[ #s1 #s2 #EX #CL #CS
     199| #s1 #s2 #EX #CL
     200| #s1 #s2 #s3 #EX #CL #AF #tlr #CS
     201| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
     202| #fl #s1 #s2 #s3 #EX #tal #CL #CS
     203] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: % | *: skip ]
     204qed.
     205
     206let rec tal_tail_not_costed S fl st1 st2 tal
     207  (H:Not (as_costed S st1)) on tal :
     208  All ? (λl. as_label_of_pc S l = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?.
     209cases tal in H ⊢ %;
     210[ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS')
     211| #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS)
     212| #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
     213| #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS'
     214  cases (tal_pc_list_start … tal')
     215  #hd #E >E
     216  % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ]
     217| #fl' #pre #init #end #EX #tal' #CL #CS #CS'
     218  cases (tal_pc_list_start … tal')
     219  #hd #E >E
     220  % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ]
     221] qed.
     222
     223
    183224inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
    184225  | tac_base:
Note: See TracChangeset for help on using the changeset viewer.