Ignore:
Timestamp:
Dec 2, 2011, 1:02:08 PM (8 years ago)
Author:
campbell
Message:

More on RTLabs structured traces.
Fixed mistake in structure trace definition that made it unhabitable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1559 r1583  
    229229  mk_fullexec … RTLabs_exec make_global make_initial_state.
    230230
     231
     232(* Some lemmas about the semantics. *)
     233
     234(* Note parts of frames and states that are preserved. *)
     235
     236inductive frame_rel : frame → frame → Prop ≝
     237| mk_frame_rel :
     238  ∀func,locals,next,next_ok,sp,retdst,locals',next',next_ok'. frame_rel
     239   (mk_frame func locals next next_ok sp retdst)
     240   (mk_frame func locals' next' next_ok' sp retdst)
     241.
     242
     243inductive state_rel : genv → state → state → Prop ≝
     244| normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m')
     245| to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m)
     246| tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m')
     247| from_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m')
     248| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
     249| from_ret : ∀ge,f,fs,rtv,dst,f',m. frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m)
     250.
     251
     252lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     253  (∀a. e = Value ??? a → f a = Value ??? v → P v) →
     254  (bindIO O I A B e f = Value ??? v → P v).
     255#O #I #A #B *
     256[ #o #k #f #v #P #H #E whd in E:(??%?); destruct
     257| #a #f #v #P #H #E @H [ @a | @refl | @E ]
     258| #m #f #v #P #H #E whd in E:(??%?); destruct
     259] qed.
     260
     261lemma eval_perserves : ∀ge,s,tr,s'.
     262  eval_statement ge s = Value ??? 〈tr,s'〉 →
     263  state_rel ge s s'.
     264#ge *
     265[ * #func #locals #next #next_ok #sp #retdst #fs #m
     266  #tr #s'
     267  whd in ⊢ (??%? → ?);
     268  generalize in ⊢ (??(?%)? → ?);
     269  cases (lookup_present LabelTag statement (f_graph func) next next_ok)
     270  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
     271  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
     272  | #r #c #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #locals' #Eloc #E whd in E:(??%?); destruct % %
     273  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev'  @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % %
     274  | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v1 #Ev1 @bindIO_value #v2 #Ev2 @bindIO_value #v' #Ev'  @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % %
     275  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev'  @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % %
     276  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev'  @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % %
     277  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bindIO_value #b #Eb @bindIO_value #fd #Efd  @bindIO_value #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
     278  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #fd #Efd  @bindIO_value #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     279  | #id #rs #LP whd in ⊢ (??%? → ?); @bindIO_value #b #Eb @bindIO_value #fd #Efd  @bindIO_value #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     280  | #r #rs #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #fd #Efd  @bindIO_value #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 ]
     281  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #b #Eb #E whd in E:(??%?); destruct % %
     282  | #r #ls #LP whd in ⊢ (??%? → ?); @bindIO_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 ]
     283  | #LP whd in ⊢ (??%? → ?); @bindIO_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bindIO_value #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5
     284  ]
     285| * #fn #args #retdst #stk #m #tr #s'
     286  whd in ⊢ (??%? → ?);
     287  [ @bindIO_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     288    #E destruct %4
     289  | @bindIO_value #evargs #Eargs @bindIO_value #evres #Eres whd in Eres:(??%?);
     290    destruct
     291  ]
     292| #v #r * [2: #f #fs ] #m #tr #s'
     293  whd in ⊢ (??%? → ?);
     294  [ @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct
     295    %6 cases f #func #locals #next #next_ok #sp #retdst %
     296  | #E destruct
     297  ]
     298] qed.
     299
Note: See TracChangeset for help on using the changeset viewer.