First reviewed on 2026-09-27: the four binary specification modules, their use by
encode_correct and encode_complete, and their correspondence with the pinned
Talos syntax. The reviewed grammar selects permitted encodings for its scalar
WASM domain. The integer, opcode, control, section, and field checks below
support that conclusion. The reference snapshot contains the discrepancies
recorded under Reference discrepancies.
The 2026-10-17 review covers 83 instruction forms and active data segments. It compares the added binary64 comparisons, absolute value, unsigned conversion, and saturating truncation with the rendered instruction grammar, and data segments with the data section grammar. The source digests below identify this revision.
The 2026-10-19 review adds f32.convert_i64_u at b5 and
i64.trunc_sat_f32_u at fc 05, bringing the inventory to 85 forms. Both
match the rendered numeric instruction grammar.
The comparison uses WebAssembly 3.0, dated 2026-09-21, and its specification
source at revision 608711107b7f1edb13efd57b7d79b49477462d36. The dated
Core 2 specification, Unicode 17.0, and the official reference
interpreter resolve the stated discrepancies. Talos is pinned to
87e3aa5e8f6e6f3b3eb5e7e4c5aba43071002d47. Lean is pinned to
6a10ac8c22beadecabdbb0919c2b50214762f91d.
The correspondence arguments in this document are a manual specification
review. The checked Lean theorems establish correctness relative to
Spec.ModuleBytes. The typing review examines the
additional premises of the validity theorem.
The value rules match the recursive LEB rules in
binary values. For unsigned integers, a terminal byte contributes
its value. A continuation contributes byte - 128 + 128 * tail. The
constructor's conclusion has width w + 7, with w > 0, which enforces the
official continuation condition that the remaining input width exceeds seven.
Induction gives a value below 2^width and a length at most
ceil(width / 7).
For signed integers, a terminal byte below 64 contributes its value. A
terminal byte from 64 through 127 contributes byte - 128. The explicit
signed bounds enforce the unused bits of the last byte. The continuation
equation and width reduction match the signed rule. value.toBitVec.toInt
selects the signed representative of the original 32-bit or 64-bit word,
preserving its bits in an integer constant.
| Rule | Checked condition |
|---|---|
Items |
Concatenates each element's bytes in list order. |
Vector |
Encodes the element count as u32, followed by those elements. |
Sized |
Encodes the payload byte count as u32. The count excludes its own prefix. |
Name |
Counts UTF-8 bytes and retains their order, including embedded zero bytes. |
Vector agrees with the binary list rule. The same size rule
serves code bodies and sections. Their length premises prevent narrowing
an oversized count into a smaller integer.
For names, Lean's String contains a byte array and an IsValidUTF8 proof.
At the pinned Lean revision, String.toUTF8 returns that array, and
String.utf8Encode_toList equates it with the UTF-8 encoding of the character
list. Inspection of Char.valid and String.utf8EncodeChar confirms the
Unicode scalar ranges and the one-, two-, three-, and four-byte layouts.
These agree with Unicode's UTF-8 tables.
The type rules were compared with binary types.
| Rule | Correspondence |
|---|---|
ValType |
7f, 7e, 7d, and 7c encode i32, i64, f32, and f64. |
BlockType |
40 denotes no parameters or results. A numeric type byte denotes no parameters and one result. |
FuncType |
60, parameter vector, result vector. Result order and multiple function results are preserved. |
Limits |
Flags 00 and 01 select 32-bit memory with a minimum and an optional maximum. |
Memory |
The memory-section record fixes is64 = false and empty data. The data section encodes the segments separately. |
Mutability |
00 is immutable and 01 is mutable. |
Global |
Declared type, mutability, matching integer constant, and terminating 0b. |
Core 3 uses u64 for memory limits and offsets. The grammar's u32
encodings are a permitted subset: any derivation of Unsigned w bytes n
also satisfies the unsigned rule at width w + 32, by induction on that
derivation. The encoded numeric value stays equal to n.
In Core 3, a bare 60 function type abbreviates a final subtype with no
supertypes in a singleton recursion group. Shape.gcTypes requires exactly
that Talos metadata. Duplicate and unused type entries remain in position.
Global records preserve all five fields: the value, declared type, mutability, constant source initializer, and empty deferred initializer. Constant evaluation therefore yields the recorded initial value.
All 85 instruction forms in the instruction rules
were compared with the official instruction grammar and its
rendered rules: 64 Plain rules, eight indexed rules,
six memory rules, four constants, and three
structured controls. Hexadecimal byte mappings are listed below. Names are
WASM instruction names, with a common type prefix shown once per group.
| Instruction group | Opcode mapping |
|---|---|
| Control and stack | unreachable=00, nop=01, return=0f, drop=1a |
i32 comparisons |
eqz=45, eq=46, lt_u=49, gt_u=4b, le_u=4d, ge_u=4f |
i64 comparisons |
eqz=50, eq=51, ne=52, lt_u=54, le_u=58, ge_u=5a |
i32 arithmetic |
add=6a, and=71 |
i64 arithmetic |
add=7c, sub=7d, mul=7e, div_u=80, rem_u=82, and=83, or=84, xor=85, shl=86, shr_u=88 |
f32 operations |
eq=5b, lt=5d, le=5f, abs=8b, nearest=90, sqrt=91, add=92, sub=93, mul=94, div=95 |
f64 operations |
eq=61, lt=63, le=65, abs=99, sqrt=9f, add=a0, sub=a1, mul=a2, div=a3 |
| Integer conversion | i32.wrap_i64=a7, i64.extend_i32_u=ad, i32.extend8_s=c0 |
| Numeric conversion | f32.convert_i32_s=b2, f32.convert_i64_u=b5, f32.demote_f64=b6, f64.convert_i64_u=ba, f64.promote_f32=bb, i32.trunc_sat_f32_s=fc 00, i64.trunc_sat_f32_u=fc 05, i64.trunc_sat_f64_u=fc 07 |
| Reinterpretation | i32.reinterpret_f32=bc, i64.reinterpret_f64=bd, f32.reinterpret_i32=be, f64.reinterpret_i64=bf |
| Indexed instructions | br=0c, br_if=0d, call=10, local.get=20, local.set=21, local.tee=22, global.get=23, global.set=24 |
| Loads | i32.load=28, i64.load=29, i32.load8_u=2d |
| Stores | i32.store=36, i64.store=37, i32.store8=3a |
| Memory operations | memory.size=3f 00, memory.grow=40 00 |
| Constants | i32.const=41 with signed 32-bit immediate. i64.const=42 with signed 64-bit immediate. f32.const=43 with four bytes and f64.const=44 with eight bytes, least significant first. |
| Structured control | block=02, loop=03, if=04, else=05, end=0b |
The 2026-09-27 review covered 71 forms. The 2026-10-03 review added the floating-point constants and binary32 comparisons and absolute value. The 2026-10-17 review covers the remaining binary64 operations, and the 2026-10-19 review adds the two binary32 conversions. Floating-point constants use N/8 bytes in the binary value rules.
Indexed immediates use u32. In fc 00, fc 05, and fc 07, the second byte encodes
unsigned subopcode zero, five, or seven. The trailing zero in memory.size and memory.grow encodes
memory index zero.
For loads and stores, alignment exponents are bounded by 2, 3, or 0 for
four-byte, eight-byte, or one-byte accesses. These bounds satisfy
2^alignment <= accessBytes and keep the explicit-memory flag clear.
Offsets preserve the UInt32 value. The encoder chooses alignment zero.
Talos records the offset and operates on memory zero. WASM alignment is a
validation constraint and hint for these ordinary loads and stores.
Each structured rule fixes parameter count zero, an empty parameter-type
list, and result count equal to the encoded result-type list length. The
BlockType premise restricts that length to zero or one. Every nested body
receives its own end. Each if has an explicit else, including an empty
else branch. Instrs preserves instruction order by concatenation.
The module rules agree with the selected productions of the official module grammar.
| Component | Checked correspondence |
|---|---|
| Header | Magic 00 61 73 6d, version 01 00 00 00. |
| Sections | IDs 1, 2, 3, 5, 6, 7, 10, once each, in the prescribed order, then ID 11 when the memory has data segments. The WASI profile adds ID 4 between 3 and 5. Empty vectors are permitted. |
| Table section | 04 04 01 70 00 00 declares one 32-bit nullable funcref table with minimum zero and no maximum. The table-free profile omits this section. |
| Data section | Each segment uses mode 0, an active segment of memory 0, with the offset as i32.const and end, then the bytes as a vector. The memory section carries the declaration without its segments, and the decoder joins the segments back to the memory. |
| Type and import sections | Preserve the type table and import order. Each imported function's selected type index resolves to its recorded signature. |
| Function and code sections | Both range over m.funcs in the same order. Their counts agree. Each type index resolves to that function's parameter and result lists. |
| Locals | Each local forms a group with count one. Vector count therefore also bounds the expanded local count. |
| Function body | Local vector, instruction sequence, end, enclosed by the exact body byte length. |
| Exports | Names, kinds, and indices are retained. The chosen order is function, global, memory, then table exports, preserving order within each list. The table export uses kind 01. |
| Section lengths | Each length counts exactly its payload. |
The fields represented by sections are types, imports, funcs,
memory, globals, exports, globalExports, memoryExports, tables,
and tableExports. Shape fixes canonical gcTypes, empty additional
memories, elements, imported non-function entities, tag exports, and tags,
an absent start function, and dataWithoutMemory = false. Its table profile
admits either no table and no table exports, or the one empty function table
and exactly __indirect_function_table at index zero. Other table types,
limits, widths, counts, names, and export indices fail the profile check.
The memory-section declaration omits the data
segments that the data section carries.
Every field of the pinned Talos module record is accounted for.
Declared function type indices remain unchanged. An imported function has names and a signature in Talos, so the binary rule permits any matching type index. The encoder chooses the first. Each such choice has the same numeric parameter and result types. Function indices include imports before defined functions throughout the module.
The pinned Core 3 value source contains three inconsistencies:
| Location | Snapshot text | Resolution used in this review |
|---|---|---|
| UTF-8 continuation helper | 0x80 < b < 0xC0 |
Unicode includes continuation byte 80. For example, U+0080 encodes as c2 80. |
| Four-byte UTF-8 range | Upper bound U+11000 |
Unicode's upper bound is U+110000. For example, U+1F600 encodes as f0 9f 98 80. |
Bi32 and Bi64 source aliases |
Aliases of BuN |
The same source defines general BiN through signed LEB. The official decoder reads constants with s32 and s64. |
The UTF-8 discrepancies also occur in the rendered Core 3 value formulas. The
dated Core 2 value rules give the intended signed-constant
interpretation and Unicode range. The official reference decoder
confirms signed constant immediates. For example, 41 7f denotes the 32-bit
word ffffffff, which the Lean rule preserves. The Lean definitions agree with
these resolved meanings. A claim of literal agreement with every formula in the
Core 3 snapshot would exceed this review.
The SHA-256 digests of the files reviewed on 2026-10-19 are:
6f69b201e8e22e1febee88b6e97a093b32af26d44266ca2781222d08b7c62d76 Spec/Values.lean
0116708ee6aff512eacc69065ccb81bdad88b27e557579c843458b54b638e2bd Spec/Types.lean
b3441af27be77f91c8a932a033dba750194f611b9b7d64d0965b3b8f603b1b23 Spec/Instructions.lean
e7ac862d6eb41655d094b8f5cd762a312b24cf23983c38e33307688c497a76b1 Spec/Modules.lean