This project aims to provide an Idris-model of the WebAssembly specification. It is at a very early stage; there isn't much to spot yet.
Possible use cases:
- Prove meta-theorems about the WebAssembly specification, for example, decidability of type-checking.
- Prove properties of specific WebAssembly programs, for example, termination.
- Generate WebAssembly bytecode for (verified) compilers.
- Statically analyze WebAssembly programs to uncover bugs.
- Serve as an oracle for test-suites of WebAssembly implementations.
- Structure
- Values
- Types
- Instructions
- Modules
- Validation
- Types
- Instructions
- Modules
- Execution
- Runtime Structure
- Numerics
- Instructions
- Modules
- Binary Format
- Values
- Types
- Instructions
- Modules
- Text Format
- Values
- Types
- Insructions
- Modules
Typecheck package: idris --checkpkg .\WebAssembly.ipkg
Generate documentation: idris --mkdoc .\WebAssembly.ipkg