Towards Formal Verification of State Continuity for Enclave Programs