LeanExe accepts a restricted executable subset of Lean 4 and emits a standalone WebAssembly module for one selected entry declaration. Lean remains the parser, elaborator, type checker, and proof checker. The compiler reads checked declarations from the Lean environment, rejects declarations outside this specification, and emits WASM only for accepted programs.
The language targets deterministic pure programs over machine integers, byte buffers, arrays, structures, and inductive values. It supports enough Lean to write conventional first-order programs with bounded loops and recursive helper data structures. Lean effects such as IO, file access, user-defined host calls, concurrency, randomness, and time remain outside the accepted source language; WASI command mode adds fixed adapters for byte output, bounded byte input, stderr error output, and process exit status.
The compiler input is a module name and a fully qualified Lean declaration name. The module must already build under Lake or otherwise be visible to Lean's module loader. The compiler imports that module, finds the checked declaration, computes runtime-relevant dependencies rooted at the module's root namespace, and lowers the accepted call graph.
An entry declaration must be a named constant with an executable value. It must be safe, non-partial, monomorphic at runtime, first-order, and closed after Lean elaboration. Helper declarations should live under the same root namespace as the imported module; external declarations compile only when LeanExe implements them as primitives.
Proofs may appear in source files and in proof fields of supported structures or inductives. Proof arguments and proof fields are erased when they have no runtime content. A theorem, proposition, quotient, axiom, opaque executable constant, unsafe declaration, or effectful declaration cannot contribute executable behavior to an accepted program.
The command-line entry point for generic compilation is:
tools/leanrun .lake/build/bin/lean-wasm compile \
--module Module.Name \
--entry Module.Name.entry \
--out build/entry.wasmcompile-wat writes the module as WAT text from the same structured instructions the binary encoder serializes, and tools/check-wat.sh verifies that parsing the text reproduces the binary byte for byte. compile-wasi emits a WASI command module for a zero-argument entry whose result type is ByteArray; the generated _start wrapper calls the pure Lean entry and writes the returned bytes to stdout. compile-wasi-stdin --max-input-bytes n emits a WASI command module for an entry of type ByteArray -> ByteArray; the generated _start wrapper reads stdin through fd_read up to the configured limit, calls the pure Lean entry, and writes the returned bytes to stdout. compile-wasi-stdin-except --max-input-bytes n emits a WASI command module for an entry of type ByteArray -> Except ByteArray ByteArray; Except.ok writes stdout and returns success, while Except.error writes stderr and exits with status 1. compile-wasi-argv-except --max-args n --max-argv-bytes n emits a WASI command module for an entry of type Array ByteArray -> Except ByteArray ByteArray; the wrapper reads WASI argv, skips argv[0], and passes user arguments as an internal array of byte strings. compile-wasi-stdin-argv-except --max-input-bytes n --max-args n --max-argv-bytes n emits a WASI command module for an entry of type ByteArray -> Array ByteArray -> Except ByteArray ByteArray; the wrapper passes bounded stdin and user arguments to the pure Lean entry. report --module Module.Name --entry Module.Name.entry imports the same module and prints the entry shape, dependency frontier, and first rejection reasons. dump-ir --module Module.Name --entry Module.Name.entry prints the extracted IR for an accepted entry. ownership-report --module Module.Name --entry Module.Name.entry compiles the entry to IR and prints ownership data for each extracted function, including result owner offsets, helper-result fresh-owner offsets, compiler-emitted releases, returned owner expressions, fold accumulator release offsets, and explicit LeanExe.Runtime.release expressions. A program that Lean accepts but LeanExe rejects lies outside this language.
The default library-mode module exports growable linear memory, alloc(len : i64) : i64, reset(), retain(ptr : i64) : i64, release(ptr : i64), free(ptr : i64), the runtime counter globals allocCount, retainCount, releaseCount, and freeCount (each a mutable i64), and the selected entry function. The memory starts at 16 pages, the heap starts at byte offset 4096, and alloc returns a byte offset in exported memory. free is an alias for release.
The entry export name is the last component of the Lean declaration name. For example, My.Module.answer exports answer. The entry name must not be memory, alloc, reset, retain, release, free, allocCount, retainCount, releaseCount, or freeCount, because those names belong to the runtime ABI.
The stdout-only WASI command-mode module imports wasi_snapshot_preview1.fd_write, exports _start, and exports the same memory. It does not export alloc, reset, or the selected Lean entry as the public program interface. The selected entry must take no parameters and return ByteArray; _start writes the returned pointer-length byte range to stdout and traps if fd_write returns an error or reports a short write.
The stdin-to-stdout WASI command-mode module imports both fd_read and fd_write. The selected entry must have type ByteArray -> ByteArray. _start reserves max-input-bytes + 1 bytes in the arena, reads stdin until EOF, traps when input exceeds the configured limit, passes the read byte range to the pure Lean entry, and writes the returned byte range to stdout. The configured limit must fit in the initial 16-page memory after the arena start at byte offset 4096.
The stdin-to-Except WASI command-mode module imports fd_read, fd_write, and proc_exit. The selected entry must have type ByteArray -> Except ByteArray ByteArray. _start uses the same bounded stdin reader as the stdin-to-stdout mode. It writes Except.ok payload bytes to stdout and returns normally. It writes Except.error payload bytes to stderr and calls proc_exit 1. It traps on invalid Except tags, input that exceeds the configured limit, fd_read errors, fd_write errors, and short writes.
The argv-to-Except WASI command-mode module imports args_sizes_get, args_get, fd_write, and proc_exit. The selected entry must have type Array ByteArray -> Except ByteArray ByteArray. _start allocates an internal Array ByteArray, fills each element with a borrowed-owner marker, the pointer, and the length for one user argument, skips argv[0], passes the array with owner 0, and then applies the same success and error behavior as the stdin-to-Except adapter. --max-args limits the number of user arguments. --max-argv-bytes limits the WASI argument buffer, including argv[0] and NUL terminators. It traps when either runtime limit is exceeded or when a WASI import reports an error.
The stdin-and-argv-to-Except WASI command-mode module imports fd_read, args_sizes_get, args_get, fd_write, and proc_exit. The selected entry must have type ByteArray -> Array ByteArray -> Except ByteArray ByteArray. _start reserves the bounded stdin buffer, aligns the arena for the argv pointer table, builds the internal argument array, passes both stdin and argv with owner 0, and then applies the same success and error behavior as the stdin-to-Except adapter. It traps when stdin exceeds --max-input-bytes, argv exceeds either configured argv bound, any WASI import reports an error, or a write is short.
Every scalar ABI slot is a WASM i64. Bool uses 0 for false and 1 for true. UInt8 and UInt32 use one slot and are reduced modulo 2^8 or 2^32 when they enter or leave the public ABI. UInt64 uses the full unsigned 64-bit representation, and Nat uses the bounded unsigned representation described below.
ByteArray crosses the public ABI as two slots: byte pointer and byte length. Inside compiled code, ByteArray uses three slots: owner pointer, byte pointer, and byte length. Owner 0 marks borrowed storage from the host or a WASI adapter, while a nonzero owner names the reference-counted allocation root that release may reclaim. Structure values flatten their runtime fields in Lean declaration order after proof-field erasure. Nonrecursive inductive values flatten as a constructor tag followed by payload slots for every constructor in declaration order; inactive payload slots are ignored on input and may hold default values on output.
Arrays cross the public ABI as one arena pointer. Inside compiled code, an Array α value uses two slots: owner pointer and visible array pointer. Owner 0 marks a borrowed public or adapter array, while a nonzero owner names the reference-counted allocation root. The pointed-to layout starts with the array length as an i64 header followed by flattened element slots. Public array elements may contain fixed-width heap-reference fields: ByteArray elements use owner, pointer, and length slots, and nested Array elements use owner and pointer slots. The same rule applies inside supported structures, nonrecursive inductives, Option, and Except stored in public arrays. Public structures and nonrecursive tagged entry values may also contain heap-bearing array fields when the flattened layout has no recursive inductive value. Public array elements cannot contain recursive inductive values.
LeanExe allocates heap-backed values in WASM linear memory with a small reference-counted object header before each returned payload pointer. Heap-backed values such as ByteArray, Array, recursive inductives, internal nested arrays, and JSON AST nodes use this allocator when compiled code constructs them. Allocations never move, the allocator grows memory when the free list and current heap range cannot satisfy a request, and the current collector reuses whole released blocks through a free list.
In library mode, alloc(len) creates a raw byte object with reference count 1 and returns the payload pointer. retain(ptr) increments the count for a nonzero pointer and returns the same pointer. release(ptr) decrements the count, puts the object on the free list when the count reaches zero, and traps on invalid or double release; free(ptr) is the same operation under a host-facing name.
The generated compiler backend emits reference-counted allocation headers for byte arrays, arrays, and recursive-inductive heap objects. Recursive-inductive heap objects store a child-pointer mask in their header, so release can recursively release fields that hold recursive-inductive child pointers, ByteArray owner slots, or Array owner slots. Arrays store the same child-pointer mask for fixed-width element layouts, including marked slots inside products, structures, and nonrecursive tagged values. Array-producing operations retain recursive children, ByteArray owners, and Array owners when they copy existing elements, and they transfer freshly constructed owned children into inserted element slots. Array operations that can return the original array preserve the original owner slot, so a no-op over a borrowed public array remains borrowed.
Internal helper results preserve one owner root per heap value. When a structure or tagged value contains an array or byte-array field constructed inline, result materialization evaluates that field once and copies the owner and pointer slots from the same local value. This is part of the ownership model, because the release pass assumes the owner slot names the allocation root for the visible pointer.
The compiler emits release for local heap temporaries only when the released owner is nonrecursive, currently ByteArray or Array, and the allocation is visible in a local expression, local binding, or helper-call result. The rule applies in scalar-result functions and in heap-result functions when the owner is absent from returned heap roots and from borrowed root expressions used by the returned value. Recursive heap temporaries are conservative in ordinary result cleanup: the compiler may leak them, but it must not release them unless an explicit source-level ownership boundary or a supported accumulator-replacement rule applies. The compiler derives helper-result ownership summaries from a first extracted IR pass and re-extracts with the summaries available to the existing release insertion paths. Recursive heap allocation stores both a child-pointer mask and an owned-child mask: allocation retains borrowed child pointers, while child pointers proven fresh by local allocation analysis or helper-result summaries transfer into the parent without an extra retain.
The ownership-report command exposes the ownership facts that drive these release decisions. It uses the same extraction path as compile, so the report reflects the IR that the WASM backend receives. The command is diagnostic only; it does not change accepted source language semantics or emitted WASM.
For Array.foldl, Array.foldr, Array.foldlM, ByteArray.foldl, ByteArray.foldlM, and accepted loops, the compiler also releases replaced accumulator owner slots after the first iteration when the next accumulator slot is proven to hold a fresh owned root and the loop body has not already released the old slot. This rule is type-directed: it applies to ByteArray owners, Array owners, recursive-inductive pointers, and owner slots inside products, structures, sums, and nonrecursive tagged values carried by the accumulator. The generated loop evaluates and stages the next accumulator before releasing the previous iteration's owned accumulator slot, then copies the staged slots into the accumulator locals. Multiple owner slots in one accumulator are released at most once for a shared pointer value. The first accumulator value is not released by this rule, because ordinary Lean aliases can still refer to the initial value after the loop. The compiler remains conservative for heap-pointer results that escape the current function and for temporaries whose last use occurs before a supported local, helper-result, fold, or loop ownership boundary.
Liveness pruning treats a materialized multi-slot fold result as one atomic local assignment. If any result slot from that fold remains live, the compiler keeps the whole fold assignment and assigns every slot once, preserving sharing for tagged or structured results whose later code reads only the tag or one payload field.
Compiled Lean code may read runtime counters through LeanExe.Runtime.allocCount, LeanExe.Runtime.retainCount, LeanExe.Runtime.releaseCount, and LeanExe.Runtime.freeCount, each of type UInt64. A compiled LeanExe.Runtime.release value consumes one owned reference to the value's nonzero root and returns freeCount after the operation. An array whose owner is 0, including a borrowed public or WASI-adapter array, causes no counter or memory change and returns the current freeCount.
For a nonzero root, release validates the allocation header, increments releaseCount, and decrements the root reference count. A remaining reference count ends the operation without freeing memory. A count that reaches zero increments freeCount, recursively releases every marked child owner, and adds the root block to the free list; an invalid root or a root whose count is already zero traps.
The consumed reference must be the final live reference to that root unless another reference was retained. A child may remain live after root release when construction or copying retained the child's independent reference, so root consumption does not require graph-wide uniqueness. A second unretained alias to the root, a repeated release, a return or container escape of that reference, or a later use of the consumed value violates the ownership judgment.
The source validator accepts a direct local root from a visible fresh allocation or a helper result whose ownership summary marks the root fresh. The release must constitute that root reference's final use, and no intervening operation may copy, return, store, or otherwise transfer it. A statically owner-zero array also satisfies the judgment as a no-op, while branch-dependent ownership, conditionally owned operations, structure fields, loop-carried roots, parameters, and unresolved aliases reject before WASM emission. The rejection identifies the declaration, released expression, provenance, and violated rule, while ownership-report prints the justification for every accepted source release.
These intrinsics extend ordinary Lean semantics. The definitions in LeanExe/Runtime.lean return zero and do not mutate state during ordinary Lean evaluation, while generated WASM applies the counter and release transitions above. The reference IR interpreter also treats counter reads and release as zero-valued no-ops, so standard-Lean and IR differential claims exclude observable runtime-intrinsic behavior and use Wasmtime execution plus Talos theorems over freshly regenerated runtime models for that behavior.
The exported reset() function rewinds the heap and clears the free list, invalidating every pointer returned by alloc or by a compiled entry. A host must not retain pointers across reset(), even if their reference count was positive before the reset. reset() remains useful as a coarse call-boundary reclamation operation when the host has finished with every result from prior calls.
WASI command modules are single-run command programs. Their _start adapter and compiled Lean entry allocate in linear memory, write observable output, and then return or call proc_exit. The operating environment discards the module instance after process exit, but a single command can still exhaust host-imposed WASM memory limits before it exits. Source code that builds large intermediate recursive values can call LeanExe.Runtime.release at explicit ownership boundaries to make the freed blocks available later in the same command.
| Lean type | Entry parameter | Entry result | Internal value | Notes |
|---|---|---|---|---|
Unit |
No | No | Yes | Runtime value is erased to a zero-valued scalar where needed. |
Bool |
Yes | Yes | Yes | ABI slot is 0 or 1. |
UInt8 |
Yes | Yes | Yes | Public ABI slot is reduced modulo 2^8. |
UInt32 |
Yes | Yes | Yes | Public ABI slot is reduced modulo 2^32. |
UInt64 |
Yes | Yes | Yes | Main scalar integer type for public entries. |
Nat |
Yes | Yes | Yes | Runtime values must fit in the bounded i64 representation. |
ByteArray |
Yes | Yes | Yes | Public ABI is pointer and length; internal layout is owner, pointer, and length. |
LeanExe.AsciiString |
Yes | Yes | Yes | One-field structure over ByteArray; validation is explicit. |
Array α |
Yes | Yes | Yes | Public ABI is one pointer; internal layout is owner and pointer. α must have a fixed-width array layout. |
Prod α β |
No | No | Yes | Products are internal values with lazy projection behavior. |
PSum α β |
No | No | Yes | Internal sum values are accepted for Lean's generated mutual-recursion helpers. |
| Structure | Yes | Yes | Yes | Nonrecursive structures with concrete supported runtime type arguments and supported runtime fields. Internal-only structures may contain recursive-inductive pointer fields. |
| User inductive | Yes | Yes | Yes | Nonrecursive inductives with concrete supported runtime type arguments and supported runtime fields. Internal-only tagged values may contain recursive-inductive pointer payloads. |
| Recursive inductive | No | No | Yes | Monomorphic self-recursive inductives, mutual recursive inductive families, and monomorphic recursive instances are allowed inside accepted code. |
List α |
No | No | Yes | Internal monomorphic instances are accepted when α has a supported internal layout, including products. Public list ABI is unsupported. Source-defined structural helpers may traverse and return lists. Limited direct-lambda library calls are accepted for monomorphic helpers. |
Option α |
Yes | Yes | Yes | Treated as a supported tagged value when α is supported. |
Except ε α |
Yes | Yes | Yes | Treated as a supported tagged value when both payload types are supported. |
| Propositions | Erased | Erased | Erased | Proofs may justify Lean source but have no WASM value. |
String |
No | No | Compile-time ASCII only | Runtime strings are unsupported; restricted compile-time ASCII expressions may feed String.toUTF8, String.length, String.isEmpty, and equality. |
Entry parameters support Bool, UInt8, UInt32, UInt64, bounded Nat, ByteArray, fixed-width Array, supported structures, supported nonrecursive inductives, Option, and Except. Entry results support the same set. Public structures, public tagged values, public Option, public Except, and public arrays may contain ByteArray and fixed-width Array fields at any nonrecursive position, including arrays of supported structures, arrays of source-defined tags, arrays of Option, and arrays of Except. Public entry layouts must not contain recursive-inductive values anywhere in their flattened layout. Unit, products, PSum, and recursive inductives are internal-only types even though helpers may use them.
An array element type is fixed-width when LeanExe can assign a constant number of i64 slots to each element. Public array elements may be Bool, UInt8, UInt32, UInt64, bounded Nat, ByteArray, nested Array values whose element type is also public-array-supported, supported structures, supported nonrecursive inductives, Option, and Except. Supported public structures and public tagged values may contain those same public array element types in their flattened runtime fields. Public array elements cannot contain products, PSum, recursive inductive values, recursive structures, indexed inductives, or unspecialized polymorphic values. Internal arrays may additionally store products and recursive inductive values, and they may store fixed-width structures or tagged values that contain those fields.
UInt64 arithmetic uses the unsigned 64-bit Lean semantics. Addition, subtraction, and multiplication wrap modulo 2^64. Division by zero returns 0, and remainder by zero returns the dividend, matching Lean's fixed-width integer behavior.
UInt8 and UInt32 are represented internally as constrained i64 values. Public entry arguments are reduced modulo 2^8 or 2^32 before the source function observes them, and public results are reduced to the same widths before returning to the host. Literals and ofNat conversions reduce modulo the type width, arithmetic wraps to the same width, and conversions to wider supported types preserve the constrained value. Shifts mask the shift amount modulo the type width before shifting.
Runtime Nat uses an unsigned 64-bit bound rather than arbitrary precision. A runtime Nat literal must be less than 2^64 unless it is consumed directly by a fixed-width conversion that defines its own modulo behavior. Nat subtraction is saturating, Nat.pred uses that saturation, and Nat.succ uses checked addition.
Nat addition and multiplication trap when the result would exceed the bounded representation. Nat division by zero returns 0, and Nat remainder by zero returns the dividend. Nat.beq, Nat.blt, Nat.ble, Nat.min, and Nat.max use unsigned comparisons over the bounded representation.
Supported comparisons and equality include scalar equality for Unit, Bool, UInt8, UInt32, UInt64, and Nat; bytewise equality for ByteArray; elementwise equality for fixed-width arrays whose element type also supports equality; structural equality for supported products, structures, internal sums, Option, Except, and nonrecursive tagged values whose runtime fields also support equality; unsigned comparisons for supported numeric scalars; and boolean operations &&, ||, !, and Bool.xor. Equality may come from ==, !=, or a decided equality proposition such as if left = right then ..., provided the Lean source has the required BEq or DecidableEq evidence. Structural equality compares fields in source order and tagged values by constructor tag before active payload fields, while ByteArray and Array equality compare lengths before scanning bytes or elements in order. Recursive-inductive equality, array equality over recursive-inductive elements, unsupported numeric types, arbitrary-precision runtime arithmetic, signed integer operations, and floating-point operations are outside the language.
The accepted term language is first-order. It includes variables, local let, direct calls to accepted helpers, numeric literals, constructors, projections, if, dependent if with erased proof binders, pattern matching, pure Id, Option, and Except do notation in the accepted shapes below, for loops over ByteArray, fixed-width Array, and Std.Legacy.Range in accepted monads, while loops that elaborate through Lean.Loop in accepted monads, and a restricted fuel-recursive loop shape. Lean's PUnit sequencing value uses the same runtime representation as Unit, which lets checked do-notation assignment sequencing compile without exposing PUnit in the public ABI. The subset excludes higher-order arguments, closures, polymorphic runtime values, type-class-driven runtime dispatch, opaque executable constants, and arbitrary recursors.
Local let bindings preserve Lean evaluation behavior for lazy internal values. A demanded field, branch, or projection extracts only the value needed by the result. This matters for products, options, structures, byte-producing helpers, and branch-selected values whose unused components may contain trapping expressions.
Named helper calls are allowed when the helper has a supported internal type and lives under the same root namespace as the entry module. Nonrecursive helpers are extracted directly or inlined as needed, and recursive helpers can be called directly when they match the accepted fuel-recursive shape. The extractor emits real WASM calls when demand analysis proves that strict argument materialization preserves Lean behavior, including multi-slot structured arguments whose unused fields may contain trapping expressions. Non-exported helpers use internal parameter and result layouts, while exported entries use the public ABI. Conditional structured results are materialized into locals through statement-level branches so one source call does not become one call per returned slot. Strict helper-call arguments and eager fixed-width array element payloads materialize top-level let and call values in source order before flattening, so a structured helper used in those positions is evaluated once. The identity function, Id.run, and pure Id Pure.pure and Bind.bind applications are erased. Local lambdas that Lean introduces as pure do-notation continuations are substituted and beta-reduced when their uses stay first-order; a function value that escapes this normalization remains unsupported. Pure.pure, Bind.bind, and Functor.map over Option and Except ε lower to the same first-order constructor and match representation as direct Option and Except calls when callbacks are direct lambdas and all payload types are concrete supported types.
Transparent specialization unfolds nonlocal transparent applications only when the application contains a direct lambda argument and the callee is not one of the explicitly lowered primitive, matcher, or recursor families. This admits selected first-order uses of Lean library functions without closure allocation. Functor.map is treated as an explicitly lowered primitive for Option and Except, so Lean's class projection for the selected instance is not unfolded into a runtime function value. Function values still cannot escape, appear in public types, or survive as runtime values.
Local first-order polymorphic helpers can be inline-specialized at concrete call sites when static type, proof, and direct-lambda arguments appear among supported runtime arguments, every runtime parameter has a supported concrete type after substitution, and the concrete result type is supported. Direct-lambda static arguments are substituted into the helper body and do not become runtime closures. Runtime binders keep their source order, and caller-local values captured by a substituted lambda remain available through the inline binding environment. The specialized body uses the same lazy argument bindings as monomorphic inline helpers, so an unused runtime argument is not evaluated. This covers helpers such as Box α -> α, PairBox α β -> α, ParamResult ε α -> Bool, genericApplyWithSeed 10 value (fun item => ...), and typed decoder helpers such as decodeRequiredField fields name (fun raw => decodeArray (fun item => decodeItem item) raw) at concrete supported instantiations.
Type-class evidence is a static specialization input when the evidence parameter's type is a Lean class application or one of the built-in evidence carrier classes that the compiler erases from runtime layouts. Lean performs instance synthesis before LeanExe sees the declaration; LeanExe reads the elaborated evidence term, substitutes it into the specialized helper body, reduces method projections, and then extracts the resulting first-order expression. Accepted examples include built-in BEq and Inhabited helpers, a source-defined class with scalar and structure instances, an instance for Option α that depends on TypeclassScore α, class methods used inside Array.foldl, Array.any, and Array.find? direct-lambda callbacks, and generic helpers whose specialized bodies call List.foldl or List.find? at concrete supported element types. A public entry cannot take a class dictionary as a runtime parameter, and a helper remains rejected when evidence normalization leaves a method projection, a function-valued dictionary field, dynamic dispatch, or an unsupported method result in the runtime expression.
Pure Id.run do blocks compile when their checked form contains local let bindings, let mut assignment chains, nested if expressions, matches over supported first-order values, and if let forms that elaborate to supported matches. Mutable locals may hold scalars, structures, ByteArray, fixed-width arrays, products, nonrecursive tagged values, Option, Except, or recursive-inductive pointers when those values otherwise satisfy the internal layout rules. Structures used as mutable locals may contain heap fields such as ByteArray and internal Array values. Conditional and matcher branches may return an Id α value through Lean's generated continuation shape, and branch results must have one supported common value shape. Generated single-constructor structure matchers may bind flattened fields when Lean uses that shape to recover mutable locals from nested accumulator structures such as MProd. Generated sparse match helpers for Option and supported nonrecursive user inductives compile when the arms stay first-order; a catch-all arm that receives the scrutinee is bound to the corresponding source value on each fallback path.
Checked loops compile when Lean elaborates them to ForIn.forIn over ByteArray, a fixed-width Array, Std.Legacy.Range, or Lean.Loop with monad Id, Option, or Except ε. Lean.Loop is the checked form Lean uses for source while loops. Range loops use bounded Nat start, stop, and step fields and follow Lean's exclusive-stop iteration order, while Lean.Loop repeats until the extracted step returns ForInStep.done.
The source loop accumulator may be a scalar, a ByteArray, an Array pointer value with supported fixed-width elements, a product, a structure, a nonrecursive tagged value, or a recursive-inductive pointer value. Products, structures, and tagged values may contain ByteArray fields when their other fields are supported; the internal owner slot follows the value through the loop. In Option and Except ε loops, the compiler carries the accumulator as Option α or Except ε α, unwraps the successful payload before evaluating the body, and stops after the first none, Except.error, or ForInStep.done.
The accepted loop body may use let mut assignments that elaborate to local lets, nested accepted computations including nested accepted loops, byte-array and array indexing, pure byte-array or array updates, generated first-order continuation lambdas, continue branches that yield the current accumulator, and break branches that return ForInStep.done. Conditional break or continue may appear before later assignments in the same loop body. Maps, polymorphic iterators, runtime callback values, and monads other than Id, Option, and Except ε are unsupported.
Helper calls may return supported structured values, including structures, byte arrays, arrays, Option, Except, and user-defined tagged values. The call result uses the same flattened ABI slots as an entry result, then the extractor reconstructs the source-level value shape for projections and matches. This rule matters for parser-style code, where a bounded recursive helper often returns a tagged parse result that later code matches before producing a public ByteArray.
Pattern matching is supported for Bool, nonrecursive Nat zero/successor matches, products, structures, nonrecursive user inductives, recursive user inductives in internal positions, Option, and Except. Branch results must have a common supported value shape. Sparse generated match helpers are accepted for Option and nonrecursive user inductives when Lean introduces them for if let or a catch-all arm. Sparse generated match helpers over recursive inductives are unsupported. Proposition-valued motives and dependent runtime result shapes are unsupported.
Option and Except short-circuiting combinators are accepted when they remain first-order. The supported forms are direct Option.map, Option.bind, Option.filter, Option.any, Option.all, Except.map, Except.mapError, Except.bind, and overloaded Functor.map, Pure.pure, and Bind.bind for Option and Except ε. Array.foldlM and ByteArray.foldlM are accepted for Option and Except ε when the callback is a direct lambda, the accumulator has a supported concrete type, and the collection has a supported element layout.
The generated monadic fold stops after the first none or Except.error, so callback code for later elements is not evaluated. Lean do notation over Option and Except ε compiles when it elaborates to accepted Pure.pure, Bind.bind, and ForIn.forIn forms. An Except do body may call accepted helpers, use accepted monadic for or while loops, and return supported structured, tagged, array, or byte-array payloads.
An error result skips later binds and loop iterations, and therefore skips later trapping computations. The compiler rejects ExceptT, OptionT, IO, EIO, named callback values that survive as runtime data, and monads other than Id, Option, and Except ε. foldlM through Id is not part of the accepted surface; use foldl for pure folds.
The accepted fuel-recursive function shape uses a first Nat fuel parameter that decreases on each recursive call. The function may carry scalar values, byte arrays, arrays, structures, nonrecursive tagged values, and internal recursive inductive pointers through the loop. This admits state-passing parser loops whose cursor, accumulator, and flags live in a supported structure.
Tail-position fuel-recursive calls compile to a WASM loop when they appear under local let bindings, nested if and dependent-if branches, Bool matches, Option matches, and supported nonrecursive inductive matches. Branches that do not recurse become early exits, while fuel exhaustion evaluates the base case with the current carried values. The base and every early-exit value must have the same supported result type.
Fuel-recursive calls may also appear in expression position when the call uses Lean's generated Nat-recursive handle for the same helper. The extractor emits an ordinary WASM call with fuel decremented by one, which supports recursive-descent parser code that calls itself to parse a nested value and then wraps or inspects the result. If a recursive-inductive match appears in a fuel-recursive step, the extractor compiles that match as an exit expression rather than as loop control, so ordinary recursive-data inspection remains available in bounded search helpers.
Direct structural recursion is accepted for helper functions whose first parameter has a supported self-recursive inductive type or a monomorphic instance of one. Constructor arms may use Lean's generated below value for direct recursive fields, including branching constructors with multiple direct recursive fields. Product fields in constructor arms may be destructured by source patterns, so a list arm such as (k, v) :: rest consumes the head as a supported product value and binds its two projected fields. The extractor resolves generated projection paths such as the left and right recursive results of a binary node to separate WASM self-calls. This covers source-defined list-shaped traversals, association-list lookup over List (UInt64 × UInt64), list-building helpers such as append and reverse, binary-tree traversals, expression evaluators, and ordinary monomorphic List traversals over supported internal element layouts. Expression-position structural recursion is lowered by synthesizing a private helper over the recursive scrutinee, any supported first-order post-arguments, and any supported first-order values captured from the surrounding lambda or let context. The synthetic helper puts the recursive scrutinee first and passes captured values as ordinary helper parameters, so recursive calls through Lean's generated below value reuse the captured values. This covers direct List.length, list append notation through ++, direct List.concat, List.reverse, List.map, List.filter, and List.foldr expressions when callbacks specialize to closed first-order code, and it covers structural predicates such as a binary-tree contains needle tree helper whose needle parameter precedes the recursive tree argument. The extractor can defunctionalize generated function-valued results when function arguments are direct lambdas and runtime carried arguments are explicit first-order helper parameters. It also accepts a top-level closed structural fold over a list-shaped recursive inductive when Lean's generated step tail-calls the single recursive field with one hidden first-order accumulator. This covers direct xs.foldl f init bodies such as leanList123.foldl (fun acc x => acc * 10 + x) 0, and it includes supported heap-bearing accumulator shapes such as ByteArray, structures containing ByteArray, Option ByteArray, and Except ByteArray ByteArray when the direct callback specializes to first-order matches. Closed structural predicates over a list-shaped recursive inductive are accepted when Lean's generated step combines a direct predicate result with the single recursive-field result through Bool.or or Bool.and, and terminal arms return the corresponding identity value. This covers direct xs.any p and xs.all p bodies when p is a direct lambda. A narrow well-founded-recursion shape is accepted when Lean lowers recursive descent through an Array field to WellFounded.fix: the constructor arm must fold over the generated Array.attach value, the recursive call must use the generated well-founded handle, and the result must have a supported first-order shape. Mutual structural recursion is accepted when Lean lowers ordinary mutual helper definitions to WellFounded.Nat.fix over a nested PSum tree, each leaf immediately matches one supported recursive-family member, recursive calls use the generated well-founded handle, and recursive descent goes through direct fields or fixed-width array folds over attached array elements. Arbitrary well-founded recursion, mutual helper groups outside that nested PSum structural shape, course-of-values uses beyond direct recursive result projections, public recursive parameters, and public recursive results remain unsupported.
A supported structure has no indices, one constructor, no recursive structure definition, and runtime fields whose types are supported after concrete type arguments are substituted. Constructors, field projections, structure-update elaborations, single-constructor matches, entry parameters, local values, helper parameters, helper results, arrays of structures, and exported structure results are accepted. Proof fields are removed from the runtime layout. Public structures may contain ByteArray fields and fixed-width Array fields, including arrays whose elements contain supported heap fields. Internal structures may also contain recursive-inductive fields; recursive-inductive fields flatten as one-slot heap pointers. Structures remain internal-only when their flattened layout contains a recursive pointer.
A supported nonrecursive user inductive has no indices, at least one constructor, and runtime constructor fields whose types are supported after concrete type arguments are substituted. Constructors, generated matcher extraction, sparse generated matches from if let and catch-all arms, nullary enum matches, branch-selected values, entry parameters, local values, helper values, arrays of tagged values, and exported results are accepted. The ABI tag is the constructor index in Lean constructor order. Public tagged values may contain ByteArray fields and fixed-width Array fields, including arrays whose elements contain supported heap fields. Internal tagged values may also contain recursive-inductive payloads, including inside arrays and Option results produced by array search operations. Tagged values remain internal-only when their flattened layout contains a recursive pointer.
A supported recursive inductive family is non-indexed after all runtime type parameters have been specialized to supported types. The family may contain one inductive or several mutual inductives. Constructor fields may contain any member of the same specialized family, Array values whose elements have supported fixed-width internal layouts, or other supported nonrecursive field types. Recursive values may be constructed, matched, stored in locals, passed to helpers, returned from helpers, selected by branches, stored in internal arrays, and carried through accepted fuel-recursive loops. The current specialization path covers ordinary monomorphic List construction, matching, helper calls, direct structural recursion over one or more direct recursive fields per constructor, source-defined List helpers for length, append, reverse, and fold-right-style traversals, recursive Array.foldl descent through generated Array.attach values, monomorphic helper calls to List.map, List.filter, List.find?, List.foldl, List.any, and List.all, and direct expression-position List.length, list append notation through ++, List.concat, List.reverse, List.map, List.filter, and List.foldr when callbacks are direct lambdas and the specialized result is a first-order value. The tested List element types include scalar values, products such as UInt64 × UInt64, structures, nonrecursive tagged values, ByteArray, Option UInt64, Option ByteArray, and Except ByteArray UInt64. Expression-position structural recursion may capture supported first-order values from the surrounding lambda or let context, which covers helpers whose non-recursive parameters precede the recursive value. It also covers internal mutual-family values whose constructors refer to another member of the family directly or through a fixed-width Array, fixed-width structures and tagged wrappers over those family members, and ordinary mutual structural traversals over recursive-family members when Lean generates the accepted nested PSum well-founded shape. List.foldl is accepted when its carried accumulator is an explicit helper parameter after the list parameter, and direct top-level List.foldl is accepted when it lowers to the closed structural-fold shape with one hidden first-order accumulator, including tagged heap-bearing accumulators in the tested Option and Except shapes. Direct List.any and List.all expressions are accepted when they lower to the closed structural-predicate shape with one direct-lambda predicate. The compiler does not compile local callback values passed to closed structural folds, function-valued fold accumulators, nested closed structural folds, closed structural predicates whose step does not match the accepted Bool.or or Bool.and shape, generated fold helper applications whose static function arguments do not specialize to first-order code, mutual structural recursion outside the accepted nested PSum shape, mutual recursive helper functions that do not structurally descend through recursive-family values, expression-position structural recursion whose post-arguments or captured values have unsupported runtime types, or structural recursion that closes over the original recursive scrutinee outside Lean's generated below value.
Recursive inductive values do not have a public entry ABI yet. They cannot appear as entry parameters, entry results, public array elements, structure fields exposed through entry values, or nonrecursive inductive payloads exposed through entry values. They may appear inside internal structure fields, internal nonrecursive tagged payloads, and internal arrays of those fixed-width values. Indexed inductives, unspecialized polymorphic inductives, unspecialized polymorphic structures, polymorphic functions that require runtime specialization, mutual families whose members cannot share one runtime-parameter specialization, recursive structures, inherited-field structure flattening, course-of-values recursion through generated below tails, and unsupported runtime fields are rejected.
Array α values use a copy-on-write arena layout. The first i64 cell stores the length, and element cells follow immediately. A one-slot element at index i lives at byte offset 8 * (i + 1), while a width-w element uses slots 8 * (1 + i * w + s) for slot s. Element width comes from the type layout: scalar values use one slot, ByteArray values use owner, pointer, and length slots, nested arrays use owner and pointer slots, fixed-width products, structures, and tagged values use their flattened slot count, and recursive inductive values use one pointer slot in internal arrays.
Accepted scalar element types are Bool, UInt8, UInt32, UInt64, and bounded Nat. ByteArray is accepted as an internal array element and occupies three slots. Supported products, structures, and tagged values flatten by field order; supported tagged values store the tag followed by payload slots for every constructor. Nested arrays store owner-pointer pairs in internal arrays, and recursive inductive values store one heap pointer slot. Internal fixed-width arrays may store structures and tagged values that contain byte arrays, arrays, or recursive heap-pointer fields. Fixed-width array operations preserve old arrays by allocating a new array for updates.
Array literals compile when Lean elaborates them as List.toArray over a literal list whose item type has a fixed-width layout. The supported constructors are Array.empty, Array.mkEmpty, Array.emptyWithCapacity, Array.singleton, and Array.replicate. Capacity arguments are not observable in the accepted language.
The supported read operations are Array.size, Array.isEmpty, proof-indexed a[i], a[i]!, a[i]?, Array.getD, Array.back, Array.back!, and Array.back?. Trapping reads emit WASM unreachable on out-of-bounds access. Safe reads return Option values without reading an element payload when the index is out of bounds.
The supported update and sequence operations are Array.set, Array.set!, Array.setIfInBounds, Array.modify, Array.push, Array.pop, Array.append, append notation through ++, Array.extract, Array.insertIdx, Array.insertIdx!, Array.insertIdxIfInBounds, Array.eraseIdx, Array.eraseIdx!, Array.eraseIdxIfInBounds, Array.swap, Array.swapAt, Array.swapIfInBounds, and Array.reverse. Bang operations trap on invalid indices. In-bounds updates allocate fresh arrays and leave aliases to old arrays unchanged. Operations that copy existing elements retain recursive-inductive child pointers, ByteArray owners, and Array owners stored in the copied slots, and operations that insert freshly constructed recursive values, byte arrays, or arrays transfer those pointers into the new array. Array equality is accepted when the element type has a fixed-width layout and supported equality, including internal arrays whose elements contain byte arrays or nested arrays. Recursive-inductive element equality remains unsupported.
The supported iteration and search operations are Array.map, Array.foldl, Array.foldr, Array.foldlM, Array.find?, Array.findIdx?, Array.any, Array.all, and Array.filter. Mappers, folders, and predicates must be direct lambdas that LeanExe can extract without closure allocation. Array.find? and Array.findIdx? evaluate one predicate scan and bind its result before matching the tag or reading the payload. Array.foldl and Array.foldr support scalar accumulators, ByteArray accumulators, supported array pointers, products, structures, nonrecursive tagged values, and recursive-inductive pointer values. Array.foldl scans from start through stop, clamping stop to the array size. Array.foldr scans right-to-left from min start array.size down to the exclusive stop bound. Array.foldlM supports the same accumulator payloads through Option and Except ε, stopping at the first failure tag. After the first iteration, when a heap-valued accumulator is replaced by a proven-fresh owned value, the generated loop releases the previous iteration's owned accumulator root after staging the new value. Array.foldl and Array.foldlM may consume array.attach elements when the callback immediately matches the attached value and uses only the runtime element; the membership proof is erased. Products, structures, and tagged values may contain ByteArray fields when their other fields are supported.
Public arrays may contain ByteArray, nested arrays, structures with heap fields, source-defined tagged values with heap payloads, Option values, and Except values when the flattened layout has a fixed slot width and contains no recursive inductive value. The supported array operation set applies to those heap-bearing element layouts as well as to scalar element layouts. A host that passes such an array must write the same flattened element layout used internally. Borrowed child values use owner 0, and owned child values use a reference-counted owner pointer that release may reclaim. Public arrays of recursive values, polymorphic array code, array capacity behavior, and effectful callbacks are unsupported. WASI argv command mode uses the same Array ByteArray representation as the public ABI. The implementation favors Lean value semantics over in-place mutation. Programs should assume copy-on-write behavior for every accepted update.
Maps are not a primitive runtime type. Programs may define simple table structures over supported arrays, as in an open-addressed UInt64 map backed by Array Slot, when the operations stay inside the accepted first-order subset.
ByteArray values use pointer-length representation at the public ABI and owner-pointer-length representation inside compiled code. Entry parameters come from host memory with owner 0, and returned public values expose only pointer and length. Returned bytes may point to host-provided input memory, a slice of that memory, or arena memory allocated by compiled code. The host must read returned bytes before calling reset().
Supported read operations include ByteArray.size, ByteArray.isEmpty, ByteArray.get!, proof-indexed indexing, bang indexing, safe indexing, and ByteArray.extract. Out-of-bounds trapping reads emit WASM unreachable. Safe indexing returns Option UInt8, and extract clamps the stop index to the source length.
Supported construction and update operations include ByteArray.empty, ByteArray.mk from Array UInt8, String.toUTF8 on compile-time ASCII string expressions, ByteArray.push, ByteArray.append, append notation through ++, proof-indexed ByteArray.set, trapping ByteArray.set!, and value-level ByteArray.copySlice. ByteArray.push, ByteArray.append, and byte-array append notation evaluate their source operands once before using the pointer and length slots. Operations that allocate a new byte buffer set owner equal to the allocated pointer. ByteArray.extract preserves the source owner while adjusting pointer and length, so slices keep the root alive when stored inside heap-backed values. Update operations allocate new byte buffers and preserve aliases to the old input. ByteArray.copySlice follows Lean's pure value behavior rather than capacity behavior.
Supported binary and loop operations include ByteArray.toUInt64LE!, ByteArray.toUInt64BE!, ByteArray.foldl, ByteArray.foldlM, ByteArray.findIdx?, and ByteArray equality through ==, !=, or decided equality propositions. The fixed-width decoding operations require exactly eight bytes and trap otherwise. ByteArray.foldl supports scalar accumulators, ByteArray accumulators, supported array pointers, products, structures, nonrecursive tagged values, and recursive-inductive pointer values. ByteArray.foldlM supports the same accumulator payloads through Option and Except ε, stopping at the first failure tag. After the first iteration, when a heap-valued accumulator is replaced by a proven-fresh owned value, the generated loop releases the previous iteration's owned accumulator root after staging the new value. Products, structures, and tagged values may contain ByteArray fields when their other fields are supported. Byte-array folders and predicates must be direct lambdas.
Unsupported byte-array features include USize indexing APIs, ByteArray.uset, runtime string conversion, UTF-8 decoding, effectful callbacks, monadic folds outside Option and Except ε, and closure-valued callbacks. Library-mode hosts interact with byte arrays through alloc, memory, and the pointer-length ABI. WASI command mode supports observable byte output for zero-argument ByteArray entries, bounded stdin-to-stdout transforms for ByteArray -> ByteArray entries, bounded error-aware stdin transforms for ByteArray -> Except ByteArray ByteArray entries, bounded argv transforms for Array ByteArray -> Except ByteArray ByteArray entries, and bounded stdin-plus-argv transforms for ByteArray -> Array ByteArray -> Except ByteArray ByteArray entries.
LeanExe.AsciiString is a source-level structure whose runtime representation is one ByteArray field. The type is intended for byte-oriented text that must remain in the ASCII range, which covers JSON punctuation, decimal digits, unescaped field names, simple error messages, and generated protocol text. It avoids runtime Lean String and Char semantics, so indexing remains byte indexing and the compiler does not need UTF-8 decoding.
ASCII text may be written with standard Lean String syntax when the expression is consumed at compile time. The accepted forms are ASCII literals, local String lets, top-level String constants, String.append, and string append notation through ++. The compiler lowers those expressions through String.toUTF8, String.length, String.isEmpty, ==, and !=, rejecting any expression whose UTF-8 bytes are not all below 128.
Runtime String values remain outside the accepted language. String parameters, String results, string values returned from helpers, runtime branch-selected strings, indexing, Char, UTF-8 decoding, and Unicode semantics are unsupported. Programs that need text at the public boundary should accept ByteArray, validate it with AsciiString.ofByteArray?, and use AsciiString for byte-indexed ASCII processing.
The library provides empty, ofTrustedByteArray, toByteArray, size, isEmpty, get!, get?, getD, isAsciiByte, pushTrustedByte, pushByte?, append, extract, equals, startsWith, containsByte, isAscii, ofByteArray?, singletonTrusted, and singleton?. Trusted constructors do not inspect bytes and therefore rely on the caller to preserve the ASCII invariant. Checked constructors and checked pushes return Option AsciiString, using none when input bytes are outside 0..127.
The compiler treats AsciiString as an ordinary supported monomorphic structure over ByteArray. An AsciiString entry parameter or result flattens like that structure, so the public ABI is the same pointer-length pair used by the underlying ByteArray field. The recommended public boundary remains ByteArray -> ByteArray with explicit AsciiString.ofByteArray? validation inside the program, because that makes malformed host input part of the source-level behavior.
The JSON support consists of ASCII-only parser and generator helpers written in the accepted Lean subset. LeanExe.Ascii.Basic provides byte constants, whitespace skipping, and byte expectations. LeanExe.Ascii.Decimal provides checked UInt64 decimal parsing and decimal rendering, while LeanExe.Ascii.Json provides range-based object and array utilities, restricted string parsing, balanced value skipping, and small object generators.
LeanExe.Ascii.Json.findFieldRange scans a top-level object for a named field and returns the byte range of the field value. parseArrayRanges scans a top-level array and returns the byte range of each element. parseUInt64Range, getUInt64Field, getStringField, getBoolField, getNullField, getObjectField, getArrayField, getArrayRangesField, and getRawField build on those range helpers. The scanner accepts unescaped ASCII strings whose bytes are at least 32 and below 128, excluding " and \, and it rejects non-ASCII input before parsing when programs call AsciiString.ofByteArray?.
Composite value skipping tracks nesting depth for {...} and [...] so a getter or array scanner can pass over unknown nested values. parseArrayRanges validates commas, rejects trailing commas, and requires the whole input slice to be one array. The skipper validates balanced nesting and restricted strings, but it does not implement the full JSON grammar inside skipped object or array values. It also does not enforce that a closing } matches an opening { rather than [, so code that needs complete JSON validation still needs a real AST parser.
LeanExe.Ascii.Json.Value adds a recursive JSON AST for programs that need complete parsing of nested arrays and objects. The AST supports null, booleans, unsigned UInt64 numbers, restricted unescaped ASCII strings, arrays, and objects. parse and parseBytes require the whole input to be one JSON value and reject malformed nesting, trailing commas, trailing input, non-ASCII bytes, unsupported string escapes, signed numbers, fractional numbers, and exponent notation.
The AST helper layer includes Field.name, Field.value, asUInt64?, asBool?, asArray?, asObject?, asString?, get?, countField, getUniqueField?, nameInArray, allFieldNamesIn, render?, render, and object1Value. Object lookup is linear and follows the parser's array order. get? returns the first matching field, while getUniqueField? requires exactly one matching field. allFieldNamesIn checks that every object field name belongs to a caller-provided allowed-name array. LeanExe.Ascii.Json.Decode wraps the AST operations in Except ByteArray helpers: parseBytesExcept, requireUInt64, requireBool, requireString, requireArray, requireObject, requireField, requireUniqueField, decodeRequiredField, typed field getters, requireOnlyFields, decodeUInt64Array, decodeArray, and renderExcept. decodeRequiredField accepts object fields, a field name, and a direct decoder lambda. decodeArray accepts a direct decoder lambda and returns an array of decoded source-level values, so programs can decode arrays of source-defined structures without adding JSON-specific compiler behavior. The generic renderer emits compact JSON for AST values that fit the restricted string rules; byte-producing examples may also use the lower-level append helpers when they need more direct control over recursive output.
The generator helpers include appendQuotedBytes?, appendQuotedString?, appendFieldPrefix?, appendUInt64Field?, appendBoolField?, appendNullField?, appendStringField?, appendRawField?, object1UInt64, object1Bool, object1String, and the shared errorJson. Quoted string generation uses the same restricted unescaped ASCII string rules as parsing. appendRawField? accepts an AsciiString only when skipValueAt consumes the whole value after whitespace.
LeanExe.Examples.JsonDouble.transform : ByteArray -> ByteArray validates ASCII input, reads field n through Ascii.Json.getUInt64Field, doubles it when the doubled value fits in UInt64, and returns JSON bytes through Ascii.Json.object1UInt64. Success returns {"result":<number>}, while malformed input, non-ASCII input, missing field, wrong value type, parse overflow, and doubled-value overflow return {"error":1}. Unknown fields may appear before or after n when their values satisfy the limited value skipper; decimal digits must be nonempty, unsigned, and within the UInt64 range.
LeanExe.Examples.JsonAdd.transform : ByteArray -> ByteArray reads fields a and b through Ascii.Json.getUInt64Field, rejects decimal parse overflow, rejects UInt64 addition overflow, and returns {"sum":<number>} on success. Field order is independent, and unknown fields may appear when their values satisfy the limited value skipper. The program returns {"error":1} for malformed input, non-ASCII input, missing required fields, wrong value types, trailing input, and overflow.
LeanExe.Examples.JsonCollatzLength.transform : ByteArray -> ByteArray accepts an object with a field named collatzLengthFor, reads it through Ascii.Json.getUInt64Field, and returns {"length":<number>} through Ascii.Json.object1UInt64. The length counts sequence terms, so input 41 returns 110. The program rejects zero, decimal parse overflow, 3n+1 overflow during sequence evaluation, fuel exhaustion before reaching 1, malformed input, non-ASCII input, and trailing input.
LeanExe.Examples.JsonGcd.transform : ByteArray -> Except ByteArray ByteArray accepts a JSON array from stdin when compiled through compile-wasi-stdin-except, interprets every top-level element as a decimal UInt64, and writes {"gcd":<number>} to stdout. The input array must be nonempty. Empty arrays, malformed arrays, non-ASCII input, nonnumeric elements, decimal parse overflow, and trailing input return Except.error {"error":1}, which the WASI adapter writes to stderr with exit status 1.
LeanExe.Examples.JsonTypedDecode.transform : ByteArray -> Except ByteArray ByteArray parses a JSON object through the AST parser, decodes it into a source-defined Request structure with fields values : Array UInt64, multiplier : UInt64, and includeCount : Bool, rejects duplicate, missing, unknown, and mistyped fields, checks arithmetic overflow, and writes {"sum":...,"scaled":...,"count":...,"included":...}. The example uses the LeanExe.Ascii.Json.Decode helpers rather than range-based field scanning.
LeanExe.Examples.JsonObjectArrayDecode.transform : ByteArray -> Except ByteArray ByteArray parses a JSON object with fields items : Array Item and scale : UInt64, where each Item has id and weight fields. It decodes required fields through decodeRequiredField, decodes the items array through decodeArray (fun item => decodeItem item), rejects duplicate, missing, unknown, and mistyped fields at both object levels, checks arithmetic overflow, and writes {"weighted":...,"count":...}.
LeanExe.Examples.JsonTreeCommand.makeTree : ByteArray -> Except ByteArray ByteArray accepts a JSON array from stdin when compiled through compile-wasi-stdin-except, parses it through the AST parser, inserts each numeric element into a simple binary-search tree, and writes that tree as nested JSON objects with value, left, and right fields. LeanExe.Examples.JsonTreeCommand.searchTree : ByteArray -> Array ByteArray -> Except ByteArray ByteArray accepts the tree JSON on stdin, parses it through the AST parser, decodes it into the source-level Tree type, and reads one decimal search key in argv when compiled through compile-wasi-stdin-argv-except. It searches the typed tree through structural recursion, writes {"found":true} or {"found":false} on success, and returns Except.error {"error":1} for malformed input, invalid tree JSON, or wrong argument count.
LeanExe.Examples.JsonMergeTreeCommand.makeMergedTree : ByteArray -> Except ByteArray ByteArray describes a JSON command that builds two source trees, copies their values into a third tree, releases the two source roots, and reports allocator counters. The current source validator rejects the first final-root release because the root was passed into the heap-valued merged binding, and the fresh-result summary does not yet prove that handoff. searchMergedTree remains source for the companion command, but the complete pipeline stays deferred until the compiler proves the merge handoff.
LeanExe.Examples.JsonGcTreeRewrite.transform : ByteArray -> Except ByteArray ByteArray describes a command that builds a balanced tree, rewrites whole generations, releases each old root, and reports allocator counters. The current source validator rejects the loop release because its root comes from a field of loop-carried RunState. The source remains a reduced requirement for field-sensitive ownership analysis and does not belong to the accepted language until that analysis justifies every release.
LeanExe.Examples.JsonTools.transform : ByteArray -> ByteArray demonstrates generated JSON output through object1UInt64 and reads its input through Ascii.Json.getUInt64Field, including skipped unknown values before the requested field. LeanExe.Examples.JsonTools.lookup : ByteArray -> UInt64 demonstrates the same generic object-field lookup as a scalar entry.
This library does not implement string escape decoding, Unicode, signed numbers, fractional numbers, exponent notation, a universal duplicate-field policy, schema combinators, or rich parse errors. Programs that need small protocol-shaped JSON can accept ByteArray, parse through Ascii.Json.parseBytes or Ascii.Json.parseBytesExcept, inspect the AST with typed getters, decode source-defined structures with Except do-notation, and generate compact output with the AST renderer or append helpers. Programs that only need one top-level field or a top-level numeric array can still use the older range helpers, which avoid constructing an AST but provide weaker validation for skipped nested values.
Option α uses the same tagged-value representation as a two-constructor user inductive. Supported operations include Option.none, Option.some, Option.casesOn, Option.rec, Option.getD, Option.get!, Option.orElse, Option.elim, Option.map, Option.filter, Option.any, Option.all, Option.bind, Option.isSome, and Option.isNone. The payload type must be supported wherever the Option value appears.
Except ε α is represented as a two-constructor tagged value. Supported operations include Except.error, Except.ok, Except.casesOn, Except.rec, Except.map, Except.mapError, Except.bind, Except.toOption, Except.isOk, and restricted fallback through <|>. Both payload types must be supported in the value's position.
Products are supported as internal values. Prod.mk, .1, .2, Prod.casesOn, and Prod.rec preserve lazy field demand in the extractor. Product entry parameters and product entry results are rejected because the public ABI assigns source identity to structures and tagged values instead. PSum is supported as an internal sum value for the generated helper behind accepted mutual structural recursion; it has no public ABI.
Unsupported runtime features include polymorphic executable code beyond inline-specialized first-order helpers, class dictionaries or method projections that survive static specialization, higher-order functions that survive as runtime values, closures, structural recursion beyond the supported direct recursive result projections, closed fold, closed predicate, generated array-descent, and nested PSum mutual-recursion forms described above, arbitrary Lean or Std library calls, function-valued structural-recursion motives that cannot be defunctionalized into direct lambdas and accepted first-order carried parameters, unsafe, partial, opaque executable constants, executable axioms, quotients, IO, EIO, BaseIO, Task, file access, environment access, time, randomness, concurrency, reflection, and FFI. Unsupported data features include runtime String, runtime Char, public arrays of recursive values, exported recursive data structures, recursive structures, indexed inductives, unspecialized polymorphic structures or inductives, and polymorphic values at runtime. Concrete instantiations of supported parametric structures and inductives are accepted, and simple first-order polymorphic or type-class-constrained helper calls may inline-specialize, but LeanExe does not compile one shared generic runtime function body for all type arguments and does not emit runtime dictionary dispatch. Direct-lambda arguments may specialize transparent helpers only when the lambda is substituted into the helper before extraction and every remaining runtime binder has a supported concrete type. Unsupported numeric features include signed integers, floating-point arithmetic, and arbitrary-precision runtime Nat.
Unsupported features should produce a rejection during report or compile. They should not be emulated through hidden Lean runtime calls. A missing rejection is a compiler bug, because accepted WASM must be explainable through this specification.
The report command classifies the entry point and its reachable declarations. It marks known primitives, erased proofs, supported source-defined structures and inductives, rejected executable dependencies, and external frontier items. The first useful diagnostic for a failed compile is:
tools/leanrun .lake/build/bin/lean-wasm report --module Module.Name --entry Module.Name.entryThe compiler command returns status 2 for command-use and bound errors, 3 for source or project input that cannot compile, 4 for I/O failures, and 5 for internal inconsistencies. A handled failure writes lean-wasm: <category>: followed by the command and available module, entry, and output-path context to stderr. Stdout remains reserved for requested reports and values, and the developer guide defines the tested process interface.
The compiler's user-facing correctness claim is semantic agreement for accepted pure programs under the bounded numeric and memory model stated here. Tests compare generated WASM behavior with Lean execution for the supported examples and correctness fixtures. The generic compiler does not claim a complete mechanized proof of source-to-WASM equivalence.
The repository contains Talos proofs for twenty registered modules. The source-driven path proves properties of models regenerated from compiler output, while the exact-artifact path proves sound decoding, restricted-profile validity, exact Talos translation, and behavior for frozen binary bytes. The general compiler-correctness theorem remains future work because neither path proves source-to-WASM refinement for every accepted program.
Traps are part of the modeled behavior for operations that Lean would panic on in ordinary execution, such as bang indexing out of bounds. The compiler must preserve observable evaluation order for accepted pure code, including lazy field projection and short-circuiting boolean operations. Host behavior outside the ABI, including reading stale pointers after reset or passing malformed flattened values, is outside the Lean source semantics.