Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying Code