Changeset 1675 for src/RTLabs/Traces.ma
 Timestamp:
 Feb 6, 2012, 3:33:52 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1671 r1675 19 19  Returnstate _ _ _ _ ⇒ cl_return 20 20 ]. 21 22 definition is_cost_label : statement → bool ≝23 λs. match s with [ St_cost _ _ ⇒ true  _ ⇒ false ].24 21 25 22 definition RTLabs_cost : state → bool ≝ … … 769 766 qed. 770 767 768 769 770 definition soundly_labelled_frame : frame → Prop ≝ 771 λf. soundly_labelled_pc (f_graph (func f)) (next f). 772 773 definition soundly_labelled_state : state → Prop ≝ 774 λs. match s with 775 [ State f _ _ ⇒ soundly_labelled_frame f 776  Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False  cons f _ ⇒ soundly_labelled_frame f ] 777  Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False  cons f _ ⇒ soundly_labelled_frame f ] 778 ]. 779 definition frame_steps_to_label_bound : frame → nat → Prop ≝ 780 λf. steps_to_label_bound (f_graph (func f)) (next f). 781 782 inductive state_steps_to_label_bound : state → nat → Prop ≝ 783  sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) (n*2) 784  sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S (n*2)) 785  sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S (n*2)) 786 . 787 788 (* 789 lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'. 790 state_steps_to_label_bound (State f fs m) (S (S n)) → 791 ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) → 792 eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → 793 state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n  _ ⇒ S n ]). 794 #ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H 795 [ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct 796 cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct  #n' #H1 #E2 normalize in E2; destruct ] 797 #NC whd in ⊢ (??%? → ?); 798 generalize in ⊢ (??(?%)? → ?); 799 lapply (steps_to_label_bound_inv_step … H1 next_ok NC) 800 cases (lookup_present ??? next next_ok) 801 [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl 802  #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl 803  #r #cs #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #E3 @bind_ok #locals' #E4 whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl 804  #t1 #t2 #op #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl 805  #op #r1 #r2 #r3 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl 806  #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl 807  #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl 808  #id #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl 809  #r #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl 810  #id #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl 811  #r #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b  @Efn ]   cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] 812  #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % % 813  #r #ls #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct  #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct  #l' #e #E whd in E:(??%?); destruct % % ]  *: #vl #E whd in E:(??%?); destruct ] 814  #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5 815 ] 816 *) 771 817 (* When constructing an infinite trace, we need to be able to grab the finite 772 818 portion of the trace for the next [trace_label_diverges] constructor. We … … 825 871 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 826 872 (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace))) 827 (LABEL_LIMIT: ∃s'. And (nth_state ge s trace (S n) = Some ? s') (RTLabs_cost s' = true))873 (LABEL_LIMIT: state_steps_to_label_bound s n) 828 874 on n : finite_prefix ge s ≝ 829 875 match n return λn. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S n) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
Note: See TracChangeset
for help on using the changeset viewer.