The current goal of the project is to formalize the semantics of the move language in Coq, prove its key safety properties, and extract a provably correct bytecode verifier.

The definitions used in the project are documented in more readable form in document.*.

Coq version: 8.16.

• definitions
  • types
  • values
  • memory model
• static semantics
  • borrow checking rules
  • type checking rules
• Operational semantics
  • local instructions
  • global instructions
• Safety properties
  • type safety
  • reference safety
  • resource safety
    • define resource safety
      • define tag-consistency: resource tags are unique
      • define resource intro/elim
      • define local resource safety
    • prove tag-consistency is preserved by small step evaluation
      • mvloc
      • cploc
      • ...
    • prove resource safety is preserved by small step evaluation
      • mvloc
      • cploc
      • ...