Reasoning About a Machine with Local Capabilities: Provably Safe Stack\n and Return Pointer Management - Technical Appendix Including Proofs and\n Details