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_partial_traces.ma

    r2894 r2895  
    14881488lemma init_state_is : ∀p,s.
    14891489  make_initial_state p = OK ? s →
    1490   𝚺b. match s with [ Callstate _ fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
     1490  𝚺b. match s with [ Callstate fid fd _ _ fs _ ⇒
     1491       fs = [ ] ∧
     1492       fid = prog_main … p ∧
     1493       find_symbol ? (make_global p) (prog_main … p) = Some ? b ∧
     1494       find_funct_ptr ? (make_global p) b = Some ? fd
    14911495   | _ ⇒ False ].
    14921496#p #s
     
    14961500#E whd in E:(??%%); destruct
    14971501%{b} whd
    1498 % // @Ef
     1502% [% [%] ] // [ @Eb | @Ef ]
    14991503qed.
    15001504
     
    15041508cases s
    15051509[ #f #fs #m *
    1506 | #vf #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
     1510| #fid #fd #args #dst #fs #m * * * #E1 #E2 #E3 #E4 destruct whd % /2/
    15071511| #rv #rr #fs #m *
    15081512| #r *
Note: See TracChangeset for help on using the changeset viewer.