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
- ...
- define resource safety