Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_traces.ma

    r2839 r2895  
    17851785lemma init_state_is : ∀p,s.
    17861786  make_initial_state p = OK ? s →
    1787   𝚺b. match s with [ Callstate _ fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
     1787  𝚺b. match s with [ Callstate fid fd _ _ fs _ ⇒
     1788       fs = [ ] ∧
     1789       fid = prog_main … p ∧
     1790       find_symbol ? (make_global p) (prog_main … p) = Some ? b ∧
     1791       find_funct_ptr ? (make_global p) b = Some ? fd
    17881792   | _ ⇒ False ].
    17891793#p #s
     
    17931797#E whd in E:(??%%); destruct
    17941798%{b} whd
    1795 % // @Ef
     1799% [% [%] ] // [ @Eb | @Ef ]
    17961800qed.
    17971801
     
    18011805cases s
    18021806[ #f #fs #m *
    1803 | #vf #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
     1807| #fid #fd #args #dst #fs #m * * * #E1 #E2 #E3 #E4 destruct whd % /2/
    18041808| #rv #rr #fs #m *
    18051809| #r *
Note: See TracChangeset for help on using the changeset viewer.