No results found

wasm

Formalising the WASM spec in Lean
#formal-verification #wasm

WasmLean

A formalisation of the semantics of WebAssembly in Lean.

This is currently intended to be used in the target of a C0 (C subset) compiler also written in Lean. Hence, efforts here will mostly reflect parts of WASM that are useful there (i.e. Vector and Float related instructions may lag behind the rest of the project).

Usage

Currently only WASM (binary files) can be converted into WAT (wasm text format). Although, no checks will be performed beyond parsing (i.e. no typechecking, etc.).

First, use lake build to compile the project.

Then you can run the following:

bin/wasm file.wasm
bin/wasm --output file.wat file.wasm

The first line will print the corresponding WAT program to the terminal. The second writes it to the file file.wat. If any error occurs an error message will be printed (for both commands).

You can also specify what you are emitting:

bin/wasm --output file.wat --emit wat file.wasm

Project Organisation/Structure

Files are generally organised into a similar layout as defined by the WASM spec:

The most notably deviation to this is that the WASM definition of integers is defined in the Numbers library.

Progress/Todo

Vectors are not implemented or represented. Instructions for floats are represented, but the implementation of floats isn't yet.

  • Syntax/Structure
    • Values
    • Types
    • Instructions
    • Modules
  • Statics/Validation
    • Types
    • Instructions
    • Modules
    • Type-checker
  • Dynamics/Execution
    • Runtime Structure
    • Numerics
      • Integer Operations
      • Floating-point Operations
      • Conversions
    • Instructions
      • Numeric
        • Floating-point
        • All other numerics
      • Reference
      • Vector
      • Parametric
      • Variable
      • Table
      • Memory
      • Blocks
      • Function Calls
      • Expressions
    • Modules
      • External Typing
      • Value Typing
      • Allocation
      • Instantiation
      • Invocation
    • Intepreter
  • Formats
    • Binary
    • Text
      • Parsing
      • Printing
      • Validation/Transformation