Changeset 2895 for src/RTLabs/RTLabs_traces.ma

Timestamp:

Mar 16, 2013, 9:08:19 PM (7 years ago)

Author:

campbell

Message:

Match up function id from RTLabs Callstate with shadow stack,
use in observables proof.

File:

• src/RTLabs/RTLabs_traces.ma (modified) (3 diffs)

src/RTLabs/RTLabs_traces.ma

@@ -1785 +1785 @@
 lemma init_state_is : ∀p,s.
   make_initial_state p = OK ? s →
-  𝚺b. match s with [ Callstate _ fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
+  𝚺b. match s with [ Callstate fid fd _ _ fs _ ⇒
+       fs = [ ] ∧
+       fid = prog_main … p ∧
+       find_symbol ? (make_global p) (prog_main … p) = Some ? b ∧
+       find_funct_ptr ? (make_global p) b = Some ? fd
    | _ ⇒ False ].
 #p #s
@@ -1793 +1797 @@
 #E whd in E:(??%%); destruct
 %{b} whd
-% // @Ef
+% [% [%] ] // [ @Eb | @Ef ]
 qed.
 
@@ -1801 +1805 @@
 cases s
 [ #f #fs #m *
-| #vf #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
+| #fid #fd #args #dst #fs #m * * * #E1 #E2 #E3 #E4 destruct whd % /2/
 | #rv #rr #fs #m *
 | #r *