Ignore:
Timestamp:
Jun 12, 2012, 10:52:37 AM (7 years ago)
Author:
campbell
Message:

PCs for RTLabs structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r2025 r2044  
    256256.
    257257
    258 lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Prop.
     258lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Type[0].
    259259  (∀a. e = OK A a → f a = OK ? v → P v) →
    260260  (match e with [ OK v ⇒ f v | Error m ⇒ Error ? m ] = OK ? v → P v).
     
    305305] qed.
    306306
     307(* Show that, in principle at least, we can calculate which function we called
     308   on a transition. The proof is a functional inversion similar to eval_preserves,
     309   above. *)
     310
     311definition func_block_of_exec : ∀ge,s,t,fd,args,dst,fs,m.
     312  eval_statement ge s = Value ??? 〈t,Callstate fd args dst fs m〉 →
     313  Σb:block. find_funct_ptr … ge b = Some ? fd.
     314#ge *
     315[ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m'
     316  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
     317  cases (lookup_present … nok)
     318  (* Function call cases. *)
     319  [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs #E normalize in E; destruct
     320    [ %{v} @Efd
     321    | cases v in Efd;
     322      [ 5: * #pty #b #pc #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
     323           [ #E @E | #E normalize in E; destruct ]
     324      | *: normalize #A try #B try #C destruct
     325      ]
     326    ]
     327  (* and everything else cannot occur, but we need to work through the
     328     definition to find the resulting state to demonstrate that. *)
     329  | #l #LP whd in ⊢ (??%? → ?); #E destruct
     330  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct
     331  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct
     332  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
     333  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
     334  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
     335  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
     336  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct
     337  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_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 ]
     338  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct
     339  ]
     340| * #fn #args #retdst #stk #m #tr #fd' #args' #dst' #fs' #m'
     341  whd in ⊢ (??%? → ?);
     342  [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     343    #E destruct
     344  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
     345  ]
     346| #v #r * [2: #f #fs ] #m #tr #fd' #args' #dst' #fs' #m'
     347  whd in ⊢ (??%? → ?);
     348  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct
     349  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct | *: normalize #a try #b destruct ] ]
     350  ]
     351| #r #tr #fd' #args' #dst' #fs' #m'
     352  normalize #E destruct
     353] qed.
     354
    307355
    308356lemma initial_state_is_not_final : ∀p,s.
Note: See TracChangeset for help on using the changeset viewer.