Changeset 2044 for src/RTLabs/semantics.ma

Timestamp:

Jun 12, 2012, 10:52:37 AM (7 years ago)

Author:

campbell

Message:

PCs for RTLabs structured traces.

File:

• src/RTLabs/semantics.ma (modified) (2 diffs)

src/RTLabs/semantics.ma

@@ -256 +256 @@
 .
 
-lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Prop.
+lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Type[0].
   (∀a. e = OK A a → f a = OK ? v → P v) →
   (match e with [ OK v ⇒ f v | Error m ⇒ Error ? m ] = OK ? v → P v).
@@ -305 +305 @@
 ] qed.
 
+(* Show that, in principle at least, we can calculate which function we called
+   on a transition. The proof is a functional inversion similar to eval_preserves,
+   above. *)
+
+definition func_block_of_exec : ∀ge,s,t,fd,args,dst,fs,m.
+  eval_statement ge s = Value ??? 〈t,Callstate fd args dst fs m〉 →
+  Σb:block. find_funct_ptr … ge b = Some ? fd.
+#ge *
+[ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m'
+  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
+  cases (lookup_present … nok)
+  (* Function call cases. *)
+  [ 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
+    [ %{v} @Efd
+    | cases v in Efd;
+      [ 5: * #pty #b #pc #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
+           [ #E @E | #E normalize in E; destruct ]
+      | *: normalize #A try #B try #C destruct
+      ]
+    ]
+  (* and everything else cannot occur, but we need to work through the
+     definition to find the resulting state to demonstrate that. *)
+  | #l #LP whd in ⊢ (??%? → ?); #E destruct
+  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct
+  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct
+  | #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
+  | #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
+  | #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
+  | #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
+  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct
+  | #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 ]
+  | #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
+  ]
+| * #fn #args #retdst #stk #m #tr #fd' #args' #dst' #fs' #m'
+  whd in ⊢ (??%? → ?);
+  [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
+    #E destruct
+  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
+  ]
+| #v #r * [2: #f #fs ] #m #tr #fd' #args' #dst' #fs' #m'
+  whd in ⊢ (??%? → ?);
+  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct
+  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct | *: normalize #a try #b destruct ] ]
+  ]
+| #r #tr #fd' #args' #dst' #fs' #m'
+  normalize #E destruct 
+] qed.
+
 
 lemma initial_state_is_not_final : ∀p,s.