LeanExe.Encoding defines the encoder. Wasm.Encoding.encode accepts a
Wasm.Module and returns Except String ByteArray, and
Wasm.Encoding.writeModule path module writes a successful result and raises an
I/O error if encoding fails. Decode.lean defines the decoder,
Wasm.Encoding.decode, which the trusted base uses to give the bytes their
meaning, and RoundTrip.lean connects the two.
| Theorem | Statement |
|---|---|
encode_correct |
Every successful result satisfies Encodes for the input module. |
encode_complete |
Every input satisfying Ready succeeds and satisfies Encodes. |
encode_valid_complete |
Ready and Spec.Validity.Module imply success, representation, and ValidBinary. |
encode_behavior |
The same premises and any property of the input module imply an encoding representing a module with that property. |
decode_encode |
The decoder reads every successful encoding of a module whose functions have at most Decoder.maxLocals locals back as that module. |
round_trip |
For such a module whose encoding evaluates to success, encode succeeds and the decoder returns the module. LeanExe's generated bytes theorems use it. |
The Verified compiler checks encoder success when generating a module and
applies decode_encode in its bytes theorems.
Ready states the representable shapes and the format's size bounds. It
checks function type indices against the preserved type table, numeric value
types, the instruction forms below, UTF-8 byte counts, vector counts, local
counts, and body and section sizes. Its size functions count the specified
output form independently of module encoder success.
Spec.Validity.Module states scalar WASM typing, memory limits, resolved
function signatures, export bounds, and distinct export names. Its shape
condition also fixes the admitted table and table-export profile. ValidBinary
means that the binary represents a module satisfying this predicate.
Validity and application behavior remain input proof obligations. The encoder
preserves the represented module, so the composition theorem applies to an
existing behavioral theorem about that module.
The grammar in the specification directory imports Talos syntax and Lean's core library. It defines binary relations without calling the encoder. These definitions and their correspondence with the published WASM rules form the trusted specification. Lean checks proofs relative to those definitions.
The binary specification review and typing specification review record the rule comparisons, source revisions, and theorem premises. The binary review also records discrepancies in the cited Core 3 snapshot's UTF-8 formulas and integer aliases, with the authoritative references used to resolve them.
| Part | Official rules | Lean definition |
|---|---|---|
| Integers, vectors, and names | Binary values, lists | Spec.Values |
| Numeric and function types, limits | Binary types | Spec.Types |
| Instructions and control delimiters | Binary instructions | Spec.Instructions |
| Sections and complete modules | Binary modules | Spec.Modules |
| Typing and module validity | Instruction validation, module validation | Spec.Validity |
The scope follows LeanExe's emitted scalar language: i32, i64, f32, and
f64 types, its integer and floating-point operations, direct calls, function
imports, integer globals, exports, and one optional 32-bit memory. Functions
may return multiple values. Structured controls have zero parameters and
zero or one result, with matching explicit Talos annotations.
The optional WASI table profile admits exactly one empty 32-bit nullable
funcref table with minimum zero and no maximum. It requires exactly the
table export __indirect_function_table at index zero. Table-free modules
have no table exports. Both encoder and decoder reject other table shapes
or table-export arrangements. Element segments and indirect calls remain
outside this profile. The pinned WASI application ABI
requires the export for applications that call WASI.
The encoder retains duplicate and unused type entries and declared function
type indices. Function imports select the first matching signature in that
table. Each local uses a one-element declaration group. Memory instructions
use alignment zero, which is a valid alignment hint for every emitted load and
store. Every conditional includes an explicit else. The module contains
the type, import, function, memory, global, export, and code sections, including
empty sections, and a data section when the memory has data segments. Each
data segment is active, in memory 0, at an i32.const offset. These choices
select permitted binary forms.
The table profile adds section 4 between the function and memory sections.
Its bytes are 04 04 01 70 00 00: section id, payload length, table count,
nullable funcref, limits flag, and minimum. The table-free path omits that
section and preserves its existing bytes. The checked-parts encoder retains
six section parts for table-free modules and appends the table section as a
seventh part for the WASI profile. Assembly places that part in section order.
The accepted Talos metadata includes canonical function gcTypes, integer
global initializers with matching declared types and constant sourceInit,
and data segments with Talos's default metadata: memory index 0, no offset
type, and no offset expression. Unsupported syntax or inconsistent metadata produces
an error. The theorem's subject is the returned Lean byte array. Running
those bytes also depends on the external runtime and host environment.
DecodeTest.lean runs the decoder over
the modules that wasm-tools json-from-wast extracts from the official
WebAssembly testsuite. Each module in the decoder's subset must decode to the
module that Talos reads from the text of the same file, and decode (encode m)
must return m when encode m succeeds. Each malformed binary must be
rejected. The test expects build/decode-test to hold the extracted modules of
the testsuite scripts in the CodeLib checkout.
tools/leanrun --timeout 60m lake env lean --run tests/decoder/DecodeTest.lean \
"$(command -v wasm-tools)" build/decode-testtools/Emit.lean also checks, for each module it
writes, that the decoder reads the bytes back as the module, and the module
tests run the written files in Wasmtime.
The table-profile proofs check the table-free empty module's exact bytes, the admitted table's round trip, table-export bounds, and rejection of unsupported table types, limits, counts, export names, and export indices.