A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code