Appendix

• Embedding
  • Types
  • Errors
  • Pre- and Post-Conditions
  • Store
  • Modules
  • Module Instances
  • Functions
  • Tables
  • Memories
  • Globals
• Implementation Limitations
  • Syntactic Limits
  • Validation
  • Execution
• Validation Algorithm
  • Data Structures
  • Validation of Opcode Sequences
• Custom Sections
  • Name Section
• Soundness
  • Results
  • Store Validity
  • Configuration Validity
  • Administrative Instructions
  • Store Extension
  • Theorems