design.md

Design

The repository is one Lake package. LeanExe and Verified contain the two compilers. Library groups reusable algorithms and their proofs, Demos contains applications, Examples contains compiler fixtures, and TestSupport contains shared cases and reference calculators under tests/. The default targets are LeanExe, Examples, and Demos. The Verified aggregate imports the verified application compilations through Demos.Verified. The complete numerical proof build includes Library. The README gives the layout and commands, the compiler manuals describe each dialect and proof procedure, and the development journal records the work.

Goal

Two compilers translate Lean functions to WebAssembly, with execution proofs in Talos. The LeanExe compiler translates a Lean function to an IR, compile translates the IR to a Wasm.Module, and a per-program proof shows that the module computes the Lean function. The verified compiler translates a typed source program with compileWith, and a universal theorem proves that the module computes the program's meaning. A binary decoder, tested against the official WebAssembly testsuite, defines what the bytes mean. decode_encode carries the module's execution theorem to its encoded bytes.

Components of the two compilers

The LeanExe compiler is not verified as a whole. Each of its rules gets its own theorem and an entry in the LTG knowledge base, so per-program proofs shrink while the trusted base stays the same. Per-program proofs, using the LTG entries, cover what the rules do not. The Verified library is a second compiler, written as a Lean function over a typed source language, whose one theorem covers every program it accepts.

Component	Design
IR	Embedded in Lean: expressions over locals, assignment, if, while, loads, stores, and calls. Values are 64-bit words, Booleans, and binary64 and binary32 bit patterns. Arrays, records, and ownership appear as memory operations in the compiler's templates and in the proofs.
Translation	compile : IR → Wasm.Module, with one wp rule per construct proved once against Talos. The IR means what its compiled code does.
Compiler	Lean to IR, reading each definition's unfolding equation. Verifying a rule means proving that its template implements its source construct, stated in terms of Lean's own functions, so no Lean.Expr semantics is trusted.
Hints	Untrusted annotations: the rule behind each fragment, its source term, its instruction path in the decoded module, and the name of each local. A wrong hint costs proof time and cannot produce a false theorem.
Runtime	alloc and release, specified and proved once. Every object has one owner. The LeanExe compiler places release, and per-program proofs check the placement. The verified compiler's theorem covers the releases in its code.
Statement	Implements, over a Represent class that says how a value appears as WASM values and heap data. A call either returns the correct result or traps at unreachable, with no premise about free memory. It includes a frame clause: every region of the heap before the call, below top and outside every free block, that lies apart from the consumed blocks keeps its bytes, stays such a region, and lies apart from the result, and the memory's maximum size is unchanged. The caller's arrays and owned trees therefore keep their contents. ImplementsA with an allocator budget states total execution, a call that returns without a trap.
Bytes	The encoder, decode_encode, and one decoder.
Floating point	The WebAssembly deterministic profile, described below.

The LeanExe compiler manual describes what each component covers. The trusted base is Lean's kernel, Talos's semantics, the decoder, the step from a module constant to a file, and any I/O adapter. The LeanExe compiler's dialect has fixed-width integers and IEEE floats, compiles panic to default, allows recursive values, and does I/O through a pure step function driven by a fixed adapter. Rule lemmas state what their templates leave unchanged, meaning the locals they do not write and the memory outside the blocks they allocate or write, because lemmas for nested templates do not compose otherwise.

The verified compiler shares the runtime, Implements, the encoding, and the trusted base. Its one theorem replaces the LeanExe compiler's per-program proofs and hints. The verified compiler manual describes its dialect and theorems, and its internals describe the code and the proof.

Component	Design
Source language	Expr S Γ t, typed by the callees' signatures S and the context Γ, with a meaning denote in Lean. Values include words, Bools, binary32 and binary64 floats, scalar tuples and sums, flat arrays, packed byte buffers, records with array fields, sums whose fields hold packed bytes, arrays, and recursive values, List UInt64, and fixed-layout recursive types. LeanExe.loop and LeanExe.repeatWhile use one loop construct with a condition.
Compiler	compileWith, a Lean function from a program, tables, wrappers, and a byte-literal pool to a module using the shared runtime.
Theorem	Prog.correctStaticWith, under heap, table, ownership, and literal-coverage premises. Its proof combines one lemma per construct through the facts of After. Prog.correctWith specializes to programs without nonempty byte literals, and Prog.correct also omits tables and wrappers.
Reflector	verified_compile, meta code that writes Lean definitions as source functions and proves each equation from one lemma per Lean form. The kernel checks every equation, so the reflector is not trusted.
Modes	Expr.paramChoice chooses each array or recursive-value parameter's mode, borrowed or owned. The theorem holds for every choice.
Bounds	Expr.allocs follows the code with the same modes and live sets, and an owned array has a potential, a number of bytes that covers its later moves to larger blocks.
Recursion	Recognized tail recursion uses a loop with a proved decreasing rank. Other recursion and its callers take the call depth, trap at depth 1,000, and have at most 32 positions per frame. An entry starts each depth-taking function at depth 0.
Tables	Data segments from the heap base, read as borrowed parameters, with wrappers that pass their addresses and compileWith_initialStore for the initial store.
Composition	Typed program reuse and call relocation transport source meanings across modules. Generated scalar store-preservation proofs support calls from other compiled programs. The composition API describes the rules and examples.

verified_compile_wasi adds effectful compilation for LeanExe.Wasi.Action, with stdin reads, stdout and stderr writes, bounded loops, and exit. It reflects actions into typed effectful code and compiles them to core WebAssembly using fd_read, fd_write, and proc_exit from WASI Preview 1. Exported-entry proofs relate target execution to native actions, including returned values, terminal outcomes, committed effects, and a joint ordered trace. The WASI manual states the API, host assumptions, and conditional total-execution premises. The WASI design records the architecture and reviewed decisions.

Files

File	Role
Compiler fixtures	Programs, specifications, compilations, worked proofs, and cases for individual compiler features.
Algorithm library	Native algorithms and their mathematical and compilation proofs, grouped by family.
Application demos	Application definitions, proofs, and host programs.
Test support	Shared cases, formatting, and numerical reference calculators.
LeanExe/Dialect/	The modules a program may import: LeanExe.loop, the dialect's index loop, LeanExe.build, an array computed by index, LeanExe.repeatWhile, LeanExe.insertAt and LeanExe.eraseAt, which insert and remove an element at a position, and LeanExe.Float32.nearest.
LeanExe/Dialect/Float32.lean, LeanExe/ProofKit/Float64.lean, Signed32.lean	Raw-bit wrappers that the binary32 and binary64 equality proofs state their results about.
LeanExe/IR/Expr.lean	IR expressions, the IR state, Expr.eval, the expression rule Expr.program_spec, and State.Frame with Expr.eval_frame. State.Frame says a state changed only given locals and scratch locals.
LeanExe/IR/Stmt.lean	IR statements, their compiled code, Triple, one rule per statement, Triple.mono, and Triple.of_forall.
LeanExe/IR/Function.lean	Func (parameters, variable types, body, results) and compile, which puts the runtime's alloc and release at functions 0 and 1 and a list of compiled functions after them, each exported by name, with a memory and the runtime globals.
LeanExe/IR/Correct.lean	Func.implements_moves: a body that aborts or ends with some heap satisfying the allocator invariant, the region frame Heap.Keeps over the consumed blocks, and the result evaluating to f x gives Implements. Func.implements_heap is the case of a body that consumes nothing, and Func.implements that of a body that keeps the store.
LeanExe/IR/TailLoop.lean	Func.tail_implements, the rule lemma for tail recursion, and TailStep, its obligation about one loop iteration.
LeanExe/IR/Fold.lean	Stmt.fold, the compiler's template for Array.foldl, and Stmt.arraySize, its template for an array's size, with their rule lemmas, and Func.foldl_implements for a function whose body is the fold template.
LeanExe/IR/Loop.lean	Stmt.loop, the template for LeanExe.loop, with its rule lemma Stmt.loop_spec and State.Holds.
LeanExe/IR/Read.lean	Expr.readValue_at and Expr.read_spec, which evaluate a bounds-checked array read to xs[k.toNat]!, and getElem!_map_toBits for reads of an Array Float.
LeanExe/IR/Build.lean	Stmt.fill, the loop that stores an array's elements from a starting index, with Stmt.fill_spec; Stmt.build, the copying template for new arrays, with Stmt.buildWith, which runs a statement per element, and its rule Stmt.buildWith_spec, of which Stmt.build_spec is a case; the lemmas that equate set!, insertIdx!, and eraseIdxIfInBounds with the template; and Stmt.copy, the copy of an array variable, with Stmt.copy_spec.
LeanExe/IR/Run.lean	Stmt.run, which computes the effect of straight-line statements, its rule Stmt.run_spec, and State.update with the lemmas simp uses.
LeanExe/IR/Recursion.lean	The rules for recursion other than tail recursion: Keeps, the internal function's specification; Func.recursion, by strong induction on a measure; Stmt.selfCall_spec; and Func.entry_implements. Rebuilds, Func.rebuildRecursion, Stmt.selfCall_rebuilds, Func.implements_rebuilt, and Func.entry_rebuilds are the counterparts for a function that consumes a tree.
LeanExe/IR/Release.lean	Stmt.release, with Stmt.release_spec for an owned array and Stmt.releaseNode_spec for an owned value of a recursive type.
LeanExe/IR/Call.lean	Stmt.callImplements_spec, the rule for a call between compiled functions, proved from the callee's Implements theorem, and Stmt.callPure_spec, the rule for a call that keeps the store.
LeanExe/IR/ArrayLiteral.lean	The template for an array literal, with its rule lemma.
LeanExe/IR/Append.lean	Stmt.append, the template for xs ++ ys that consumes xs: in place when its block has room, and otherwise into a new block of twice the capacity, or of the size needed, at most 2 ^ 32 bytes; its rule Stmt.append_spec, and Live.append for a body's temporaries.
LeanExe/IR/Update.lean	The in-place templates for an owned array at its last use: Stmt.setInPlace, Stmt.eraseInPlace, Stmt.insertInPlace, and Stmt.pushInPlace, with Stmt.reserve, the growth step of the last two, and their rules, which end in Stmt.AppendPost.
LeanExe/IR/Live.lean, Tuple.lean, ArrayLoop.lean	Live, the invariant of a body that calls functions and releases temporaries, with the rules for a call, a call that consumes a temporary, a call that returns a nest of word arrays and consumes temporaries, a release at any position, an array loop, a loop over a nest of word arrays, and the start and end of a body. Arrays states what an owned nest of word arrays is.
LeanExe/IR/Record.lean, ListFold.lean	Stmt.record, the template that allocates a record and writes its header and slots, with its rule Stmt.record_spec; and Stmt.listFold, the fold over a list of words, with its rule Stmt.listFold_spec.
LeanExe/IR/Hint.lean	Hint types.
LeanExe/IR/Words.lean, Combinators.lean	Lemmas and tactics shared by the proofs: the words of Bool tests, divU_eq, eval_body, and eval_state; and loop_induction, loop_congr, build_size, and build_get for the combinators.
LeanExe/Compiler/Scalar.lean, Command.lean	The LeanExe compiler and leanexe_compile. leanexe_compile p := f adds p.ir, p.hints, and p.module, a module with one compiled function. leanexe_compile p := [f, g, …] adds p.f.ir and p.f.hints for each listed definition, p.funcs, and p.module := compile p.funcs.
LeanExe/Pipeline/Implements.lean	Represent, Scalar, Flat for types represented as words, Encode and Node for types represented as records on the heap, Moved for a consumed argument, Separate and Apart for the consumed blocks, Implements, ImplementsPure for functions that keep the store, Satisfies, and Implements.transfer.
LeanExe/Pipeline/Records.lean	Facts about records: a region outside the free blocks through an allocation, the frame of an owned record and of an owned value, Heap.NewRecord for a record just allocated and filled, Heap.Built for a value built by a sequence of allocations, and ListAt, a list of words in memory, which a borrowed list gives.
LeanExe/Pipeline/Runtime.lean	The heap state and the invariants Heap.At, Heap.Borrowed, and Heap.Owned.
LeanExe/Pipeline/Aborts.lean	Runs aborts: every run returns values with a postcondition or, when aborts, traps at unreachable. ReturnsOrAborts is Runs true. Its entry and call rules.
LeanExe/Pipeline/Budget.lean	The allocator budget: units, Heap.Budget, and Heap.Bounded, with the allocation, release, room, and page lemmas that complete-execution proofs use.
LeanExe/Pipeline/Allocation.lean	What one allocation guarantees: the block, the allocator invariant, Heap.Fits (a bump allocation ends within 65,535 pages), and the preservation of borrowed and owned arrays.
LeanExe/Pipeline/RuntimeSpec.lean	alloc_spec_or_abort, release_run with findPlace_spec, joinProgram_spec, and freeObject_spec for any locals of release (ReleaseVars), Heap.Object, and the heap after a release.
LeanExe/Pipeline/ReleaseTree.lean	release_tree_run: release frees a tree of records. release_tree_run_top also proves that the allocator's top is unchanged. dropChildren_spec for a record, the loop invariant Releasing with Releasing.start, next, and done, and wp_loop_ghost, a loop rule with a ghost measure.
LeanExe/Runtime/	Defs.lean, the code of alloc and release; FreeList.lean, the free-list layout that Heap.At uses, with the split of a reused block; Merge.lean, the free list and memory after release inserts a block in address order and merges it with its neighbors, and the proof that the list stays laid out; and Tree.lean, a model of the structure that release frees.
LeanExe/Encoding/	The encoder, the decoder, and decode_encode. tests/decoder/DecodeTest.lean runs the decoder over the testsuite.
LeanExe/ProofKit/	General lemmas: memory, arrays, allocation, frames, the binary32 and binary64 equality chain, and the error bounds, real analysis, and rounding lemmas used by the Euler solvers and the numerical function proofs.
LeanExe/WGSL/, Demos/Gpt32/, tests/wgsl/, tests/gpt32/, tests/web/	The WGSL path: the WGSL subset, its printer, parser, and semantics, the translation of IR kernels, GPT-2's binary32 kernels and host program with their theorems, and their tests on two Vulkan drivers and in a browser.
Verified/, tests/verified/	The verified compiler: its source language (Source.lean), the compiler (Compile.lean), the representation of values (State.lean), the heap specifications (Heap.lean), the bound and the potential (Bound.lean, Potential.lean, BoundFacts.lean), the theorem Prog.correct (After.lean, Correct.lean), the initial store (Instantiate.lean), the reflector (Reflect/), the examples with their bytes theorems (Examples/), and the comparison of their modules with native Lean.
tools/Emit.lean	Script: evaluates a module constant, encodes it, checks that decode returns it, and writes the file.
ltg/, ltg/Check.lean	The LTG knowledge base, each entry an entry.json and a README.md, and the script that imports every module the entries list and reports declarations that do not exist.
Examples/Scale/, Library/Numerics/Arithmetic/Gcd/, Demos/Clob/, Demos/Gpt/, and the other directories named after an example	Compiler fixtures in Examples, reusable families in Library, and applications in Demos, with their leanexe_compile commands and theorems. The LeanExe compiler manual's list of examples names them all.
Demos/Gpt/Composites.lean, tools/gpt_composites.py	The Implements theorems of the GPT functions that call other functions and release their temporaries, generated by the script from a description of each function's calls.
Demos/Gpt/Causal.lean, Exact.lean	Theorems about the Lean definitions: forward_prefix, row i of forward depends only on tokens 0 to i; and steps_exact, the cached steps give forward's rows bit for bit.
tools/gpt2.py	A command-line program that generates text with gpt.wasm: uv run tools/gpt2.py --output-tokens 32 --prompt "…". It tokenizes the prompt with the pinned Hugging Face tokenizer, runs step on each prompt token in one host session, and then chooses each output token by the highest score from scores, stopping at <|endoftext|>. It reads the weight files that gpt2_compare.py writes.
Library/Random/SplitMix64/, tests/prng/compare.py	SplitMix64: splitMix, one step of Vigna's generator, and unitFloat, a word as a float in [0, 1). Their compiled forms are proved for any module that contains them (splitMix_pure, unitFloat_pure), prng.wasm exports both, and the test compares it with the reference algorithm.
tests/gpt/	GPT tests: Cases.lean computes the cases with native Lean, run.sh compares every export on them, sessions.sh checks that every allocation is freed, hf_compare.py compares forward with Hugging Face's model on random weights, gpt2_compare.py on the GPT-2 124M weights, and sample_frequencies.py compares top-k sampling counts with their probabilities. Python tools declare their dependencies in PEP 723 metadata and run with uv run.
Demos/Euler/	The two Euler solvers, Program.lean and ReconstructedProgram.lean, their Implements and total-execution proofs, run properties, admissibility, hyperbolicity, CFL bounds, and conservation balance, with the real-number theory of the Euler equations in Equations/ and the rounding analysis of the fluxes and updates in Reference/. The records in first-order/ and reconstructed/ describe the runs.
Demos/Drone/, tests/drone/	The drone planner, its optimality and flight-safety theorems, total execution within 70 pages, and the comparison with a reference implementation. The drone README describes it.
Library/Numerics/Arithmetic/PrimeFactors/, Examples/Lookup/, Examples/Below100/, Examples/Increment/, Examples/RemoveZero/	Small examples, each with a request, a README, a specification, a program, and a theorem that the bytes compute the specification.
.claude/skills/verified-executable/, tools/demo-check, tests/TestSupport/Host.lean	From an English request to a verified executable: the skill an agent follows, the checker that writes the required theorem and accepts or rejects a run, and the host kinds of the samples. Examples/TreeLookup/ is its first run.
docs/leanexe-manual.md, docs/verified-manual.md	The manuals of the two compilers: the dialect, compiling and running, proving, and testing.

Proved

scale_implements states that scale.module implements scale a b c = a * b / c + 1 on every triple of UInt64 arguments. Its proof applies Func.implements and one simp call. The only remaining step is Lean's a * b / 0 = 0.

gcd_implements states that gcd.module implements Euclid's algorithm on every pair of UInt64 arguments. The compiler produces a while loop over a done flag whose body branches on b = 0. The proof applies Func.tail_implements and proves only gcd_step, one iteration.

sumArray_implements states that sumArray.module implements sumArray xs = xs.foldl (· + ·) 0 on every borrowed Array UInt64. The compiler produces an assignment of 0 to an accumulator followed by Stmt.fold, a loop that loads the length word and then each element. Func.foldl_implements applies Func.implements, the assignment rule, and Stmt.fold_spec to any function whose body is this template with a word operation other than division and remainder, and sumArray_implements, productArray_implements, and xorArray_implements apply it. Stmt.fold_spec needs the array's layout in memory, which Heap.Borrowed provides, and an obligation that the fold body evaluates to g a e.

pairSum_implements states that pairSum.module implements pairSum a b = #[a, b].foldl (· + ·) 0 on every pair of UInt64 arguments. The compiled code calls alloc, stores the length and the two elements, folds, and calls release. The proof applies Func.implements_heap, Stmt.arrayLiteral_spec, the assignment rule, Stmt.fold_spec, and Stmt.release_spec with Heap.At.release.

sumCount_implements states that sumCount.module implements sumCount xs = #[xs.foldl (· + ·) 0, xs.size.toUInt64] on every borrowed Array UInt64: the result is an array that the caller owns, and the argument stays borrowed. The proof applies Func.implements_heap, Stmt.fold_spec, Stmt.arraySize_spec, and Stmt.arrayLiteral_spec, whose preservation clause keeps the argument borrowed.

axpy_implements states that axpy.module computes axpy a x y = a * x + y bit for bit on every triple of Float arguments, NaN included. The proof applies Func.implements and one simp call with F64Bits.toBits_add and toBits_mul. scaledHypot_implements does the same for scaledHypot x y s = (x * x + y * y).sqrt / s, adding toBits_div and toBits_sqrt. piecewise_implements covers a function with ==, <, ≤, negation, Float.abs, min, max, three literals, and nested if.

sumSquares_implements states that sumSquares.module computes sumSquares xs = xs.foldl (fun acc x => acc + x * x) 0.0 bit for bit on every borrowed Array Float. An Array Float is stored as the Array UInt64 of its elements' bit patterns, and the fold's accumulator and element locals have type f64. The proof applies Stmt.fold_spec with a step on bit patterns, and a lemma converts the result with core's Array.foldl_map and Array.foldl_hom.

mean_implements proves mean xs = xs.foldl (· + ·) 0.0 / xs.size.toUInt64.toFloat bit for bit, with the fold, the array-size rule, and F64Convert.toBits_toFloat. bucket_implements proves bucket x lo width = ((x - lo) / width).toUInt64, a histogram index, with one simp call and F64Convert.toUInt64_eq. Both conversion theorems cover NaN, the infinities, and out-of-range values.

marketBuy_implements proves the first CLOB operation: marketBuy askPrices askSizes qty iterates over the ask levels with LeanExe.loop, taking min remaining askSizes[i]! at each level, and returns #[filled, cost], an array the caller owns. The source equals a loop over a named step function by rfl. The loop rule Stmt.loop_spec needs one obligation about the body, which body_run proves by computing the body's effect with Stmt.run and simp, including two bounds-checked reads. The assignments before the loop are proved the same way, and the result array by Stmt.arrayLiteral_spec.

fillLevel_implements proves fillLevel sizes k amount = sizes.set! k.toNat (sizes[k.toNat]! - amount). The array is consumed and updated in place by Stmt.setInPlace at its last use, and set!_eq_build equates set! with the copying template that a non-last use compiles to. insertLevel_implements proves insertLevel prices sizes k price size = (prices.insertIdx! k.toNat price, sizes.insertIdx! k.toNat size), which returns two arrays as two WebAssembly results. Func holds a list of results, and Implements states the owned results in declaration order: Talos lists results with the top of the stack first, as it does arguments. Chaining two templates uses the runtime lemmas that an owned object stays owned after another allocation and after writes to the new block (Heap.Owned.allocate, Heap.Owned.writesWithin).

setLevel_implements proves setLevel prices sizes k size = (prices, sizes.set! k.toNat size). addBid and cancelBid call findLevel and then, depending on whether the level at that position has the price, setLevel, insertLevel, or removeLevel. bid_spec proves the part the two share, the search call, the number of levels, and the condition, once for any number of locals. pairCall_spec proves a call whose two arrays become the caller's result, and pairCopy_spec copies of two arrays as the result, both for any result locals and caller arguments. applyCommand_implements proves applyCommand prices sizes kind price size, which calls addBid for kind 0 and cancelBid for kind 1 and returns both arrays for any other kind.

The compiler allocates a conditional's result locals before its branches, and a call or array build in a branch writes into them directly, so no branch copies results between locals. Implements states that the memory's maximum size is unchanged: a call after another call needs room in the store the first leaves, and Heap.Room.after derives it from that fact.

depth_implements proves depth prices sizes limit, the total size of the levels priced at or above limit, a loop whose state is one word, by Func.implements and Stmt.loop_spec. findLevel_implements proves findLevel prices price, the search loop of addBid. removeLevel_implements proves removeLevel prices sizes k = (prices.eraseIdxIfInBounds k.toNat, sizes.eraseIdxIfInBounds k.toNat), and eraseIdxIfInBounds_eq_build equates the operation with the copying template, using core's getElem_eraseIdx.

dot_implements proves the first CPU GPT kernel, dot xs ys, a loop that sums xs[i]! * ys[i]! over the length of xs, bit for bit. An Array Float read compiles to Expr.ofBits around the word read, and Expr.ofBits compiles to f64.reinterpret_i64 and leaves the bit pattern unchanged. getElem!_map_toBits relates the read of the bit patterns to Lean's read, which yields UInt64.toFloat 0, bit pattern 0, past the end.

matVec_implements proves matVec m v rows cols, the product of a rows × cols matrix stored by rows and a vector, returned as a new Array Float, bit for bit. Each element is a loop over a row: Stmt.buildWith runs a statement before it stores each element, and Stmt.build is the case with .skip, which emits no instructions. The compiler translates the element in a block whose statements become the per-element statement, and it rejects allocation there and accepts only calls of functions of scalars whose theorems state that they keep the store, so that the statement keeps the store. A float element is stored through Expr.toBits, which compiles to i64.reinterpret_f64.

layerNorm_implements proves layerNorm xs g b eps: the mean and the variance by two loops, 1.0 / (var + eps).sqrt, and a new array whose element i is (xs[i]! - mean) * inv * g[i]! + b[i]!, bit for bit. It applies Stmt.loop_spec twice, straight-line runs for the float assignments, and Stmt.build_spec.

exp_implements proves that the compiled exp computes the Lean definition exp bit for bit. exp reduces x to k·ln 2 + r with a two-part ln 2, evaluates the Taylor polynomial of degree 13 for e^r, and multiplies by 2^k as a product of two powers of two built from their bits with Float.ofBits. It returns x for NaN, infinity above 709.8, and 0 below -745.2. Float.ofBits compiles to f64.reinterpret_i64, which keeps a NaN payload while Lean's model does not, so the proof shows that v <<< 52 is never a NaN pattern (F64Bits.shiftLeft_52_not_nan). No theorem bounds the error against the true exponential, and the tests measure it.

softmax_implements proves softmax xs, which takes the maximum by a loop, sums exp (xs[i] - max) by a second loop, and builds the array of each exponential divided by the sum, bit for bit. It calls exp in its sum loop and in each element. ImplementsPure states that a function of scalars returns f x and keeps the store, for every store: Func.implementsPure proves it for a compiled function whose body keeps the store, ImplementsPure.implements derives Implements, and Stmt.callPure_spec proves a call that keeps the store. Call arguments are typed expressions, so a call can pass a float, and the compiler allows calls in loop bodies and array elements when every argument and result is a scalar.

matVec2_implements proves matVec2 w1 w2 x hidden d = matVec w2 (matVec w1 x hidden d) d hidden, in which the intermediate vector is a temporary array: a let at the top of the body binds it, the second call borrows it, and the compiler releases it at the end of the function. Releasing it requires that every array still live lies apart from it, so Implements has a freshness clause: every object the result owns lies apart from each array borrowed or owned before the call, stated through the Represent method outside. The keep clause for owned arrays also keeps their capacity, since an owned array's block is measured with it.

matMul_implements proves matMul a b n k m, the product of an n × k and a k × m matrix stored by rows, bit for bit. Each element is a loop over the shared dimension, with read positions that use unsigned division and remainder by m. The proof splits on m = 0, where the IR's operations test for a zero divisor and Lean's define that case directly.

The MLP of a transformer block is proved in pieces. add (element-wise sum) and geluArray are kernels built with the copying template. tanh z = 1 - 2 / (e^(2z) + 1) and GPT-2's gelu are functions that keep the store, proved with Func.implementsPure, so geluArray's elements may call gelu, which calls tanh, which calls exp. mlp x w1 w2 t d f = matMul (geluArray (matMul x w1 t d f)) w2 t f d is a composite with two temporaries, proved with Live.

Row-wise layer norm normalizes each of the t rows of a t × d matrix stored by rows. Two kernels compute each row's mean and inverse deviation once, rowMeans and rowInvStd, each a build whose element runs a loop over the row. normalizeRows builds each element from five reads at positions e, e / d, and e % d, and splits on d = 0 as matMul does. layerNormRows x g b t d eps calls the three kernels in turn and holds the means and the inverse deviations as temporaries.

Masked attention uses nh heads of width dh on rows of width d = nh · dh, as GPT-2 splits them. maskedScores q k t nh dh scale builds t rows of nh blocks of t scores: element (i, h, j) is scale · (q[i] · k[j]) over the columns of head h where j ≤ i, and a masked element reads no key. Storing the scores by position first keeps rows 0 to i a prefix of every array. Row-wise softmax consists of rowMax and rowSumExp, which read elements 0 to r / nh of row r, and softmaxApply, combined in the composite softmaxRows. causalMatMul p v t nh dh multiplies each head's weights by that head's columns of the values, with row i summing over rows 0 to i of v only. attention x wq bq wk bk wv bv wo bo l t nh dh computes q, k, and v with linear, the masked scores with scale = 1 / √dh, the softmax of each of the t · nh rows of scores, the product with v by causalMatMul, and the product of that with wo.

Demos/Gpt/Causal.lean proves attention_rows and block_rows: when two inputs agree on rows 0 to i, so do the outputs, for t, nh, and dh below 2 ^ 16 and f below 2 ^ 32, which exclude overflow in the UInt64 index arithmetic. The two inputs may have different numbers of rows t and t', both above i. The theorems concern the Lean definitions, and with Implements they hold for the bytes.

block x g1 b1 wq bq wk bk wv bv wo bo g2 b2 wfc bfc wproj bproj l t nh dh f eps is one transformer block in the form of GPT-2's: r = x + attention (layerNormRows x g1 b1), then r + mlp (layerNormRows r g2 b2). Its four linear layers use linear x w b n k m, the product x · w plus the bias b in each column, summed before the bias is added, as in GPT-2's conv1d. The weight arrays stack the layers one after another, and linear, normalizeRows, and the functions that call them read layer l at an offset: w[l · k · m + …] for a k × m matrix and b[l · m + …] for its bias.

forward is the forward pass of GPT-2 with layers blocks: embed adds row tokens[i] of the token embeddings to row i of the position embeddings, a loop over the layers applies the blocks, then a final layer norm, and matMulT scores each position against every token embedding. The loop is LeanExe.loop layers x0 fun l x => block x … l …, which the compiler translates to Stmt.arrayLoop: a copy of x0 into the loop's state, then one call of block per layer, each followed by the release of the previous state. Live.arrayLoop proves the statement, and Live proves forward. forward_prefix proves that row i of the scores depends only on tokens 0 to i, whatever the number of tokens, under the same bounds with vocab added, by induction over the layers. layers_rows states the same for the input of every layer, and forward_causal is the case of equal numbers of tokens.

steps_exact states that step run on tokens 0 to p from an empty cache, followed by scores, equals row p of forward on any T > p tokens, as Array Float: the same floating-point values bit for bit. The hypotheses bound the dimensions so that no UInt64 index wraps: T, nh, dh, and layers below 2 ^ 16, f and vocab below 2 ^ 32, nh and dh positive, and the whole cache, T · (2 · layers + 1) · nh · dh values, below 2 ^ 32. The proof uses an invariant on the cache: block j holds row j of the last layer's input and rows j of each layer's keys and values, as forward on all T tokens computes them. Each kernel that layerStep runs on one row computes the corresponding row of block's kernel, and the attention kernels stepScores, stepSoftmax, and stepMix compute row p of maskedScores, softmaxRows, and causalMatMul from the cached keys and values. With step_implements and scores_implements, the compiled cached generation computes forward's rows exactly. step consumes the cache, and appendBlock, cache ++ s, compiles to Stmt.append.

Demos/Gpt/SampleVerify.lean proves the sampler. negInfs is a build, insertTop a build whose position comes from a loop counting the buffer entries not below the new score, and sampleFrom a function that keeps the store: one loop sums the weights of the kept scores, and the other chooses the token, with calls of exp, splitMix, and unitFloat, whose theorems splitMix_pure and unitFloat_pure hold in any module that contains them. topKBuffer is an array-state loop of insertTop calls that starts from negInfs k, and sampleTopK calls topKBuffer, passes the buffer to sampleFrom, and releases it, using the Live rules Live.callScalar_seq and Live.releaseFirst.

scale_bytes, gcd_bytes, sumArray_bytes, folds_bytes, pairSum_bytes, sumCount_bytes, axpy_bytes, scaledHypot_bytes, piecewise_bytes, sumSquares_bytes, mean_bytes, bucket_bytes, clob_bytes, gpt_bytes, prng_bytes, and the bytes theorems of the other examples combine these with round_trip: encode succeeds on the module, and the decoder reads the bytes back as a module that implements its functions. The kernel checks that encoding succeeds by evaluating the encoder (decide +kernel). All of these theorems, the rule lemmas, the runtime specifications, and decode_encode depend only on propext, Classical.choice, and Quot.sound. The proofs use ProofKit's kernel-checked Memory.read64_write64 and remove CodeLib's Mem.read64_write64_same, which is proved with bv_decide, from the simp set in RuntimeSpec.lean.

alloc and release follow Knuth's first fit and liberation with a sorted list (TAOCP vol. 1, §2.5, Algorithms A and B). alloc takes the first free block that fits. When at least 56 bytes would remain, it lowers the block's size word and places the object at the block's upper end, so the free block keeps its place and link. release searches the free list, which is in address order, for the first block above the freed one, then merges the freed block with that block and with the block before it when their regions touch. FixedArrayReuse.program_spec proves the split, findPlace_spec the search, joinProgram_spec one merge, and freeObject_spec the whole return of a block. Safety does not depend on the order of the list, and a merged block's region is the union of two free regions. FreeListAt.release proves that the list stays laid out, insertFree_cover that every new block starts and ends where an old block or the freed block does, and insertFree_apart that a region apart from the freed block and every free block stays apart from every new block. Heap.Borrowed.release and Heap.Owned.release take Heap.At, because release writes the header of the free block below the freed one. The proofs bound top within one call, and a test covers memory across a session.

euler_solve, euler_reconstructed_solve, and euler_solve_total state that the bytes of euler.module compute both Euler solvers. The last states that, from the allocator state of a fresh instance with a memory cap of at least 1,407 pages, both solve exports return their words without a trap and end within 1,407 pages. run_reference_balance and reconstructedRun_reference_balance state conservation against the exact Rusanov flux through the boundary. drone_compute and drone_safe state that the bytes of drone.module compute the planner, whose flight is optimal among admitted flights and safe in the point-mass model, and drone_compute_total states total execution within 70 pages. primeFactors_bytes, lookup_bytes, below100_bytes, increment_bytes, removeZero_bytes, gcd_bytes, and treeLookup_bytes state that the bytes of the small examples compute their specifications, written apart from the programs, and increment_total states total execution without memory growth.

Prog.correctWith states that the verified compiler's module of every program of its source language, with its tables and wrappers, computes the program's meaning, in the sense of ImplementsP, with the flags, bounds, and frames conditions that the compiler computes. Prog.correct is its case for a program without tables. compileWith_initialStore states that the store in which a module with tables starts meets the allocator invariant, caps the memory at 65,535 pages, and holds each table at its address, when the tables end below 65,535 pages. For each example other than Tuples.lean, which builds its program without the reflector, verified_compile states that the bytes decode to the module and that the module computes each definition, with a theorem that excludes a trap under the definition's bound. drone_trapFree bounds the drone planner's allocation by 2,251,064 bytes, chain_trapFree and fill_trapFree cover recursions below depth 1,000, lcg_advance, parkMiller_advance, and xorshift_advance state the generators' bytes together with their period theorems, and the order book's theorems show that a command stream run in two chunks gives the book of one run. The verified compiler manual lists the examples.

The verified compiler's GPT module compiles the 48 unchanged binary64 GPT functions, including cached inference and sampling. verified_compile derives their execution theorems from Prog.correctWith, their allocation bounds, their trap-free theorems under those bounds, and the module's bytes theorem.

The verified compiler's Euler module compiles the 55 unchanged functions of both solvers with the same generated theorems. Its trap-free results use the generated allocation bounds. euler_solve_total and its 1,407-page bound apply to the LeanExe compiler's module.

Tested

tests/modules/run.sh compares every case of each module's Cases.lean between Wasmtime and native Lean. For scale, the cases include a zero divisor and products that wrap. For gcd, they include zero arguments, consecutive Fibonacci numbers, and (2^64-1, 2^64-59). For sumArray, pairSum, and sumCount, the host allocates the input through alloc, and the allocation and free counters show every block freed after the host releases the result and the input. A pairSum session shows the second call reusing the block the first freed, and releasing an array whose child mask marks its one element as a pointer frees both the array and the child.

The float modules return the same bits as native Lean on chosen and pseudo-random inputs. axpy covers infinities, the canonical NaN, signed zeros, a subnormal result, overflow, and two-rounding cases. scaledHypot covers division by both signed zeros, overflow and underflow in the squares, and NaN. piecewise covers equal values, both signed zeros, NaN in each position, and inverted bounds. sumSquares covers the empty array, infinities, NaN, subnormals, overflow, and small terms added before and after a large one. mean covers empty arrays, and bucket covers NaN in each position, infinities, division by zero, and results at and beyond 2^64 - 1. The host passes and prints f64 values as bit patterns (f64:BITS) and float arrays as array-u64: with the elements' bit patterns.

clob.wasm holds the ten CLOB operations, runCommands, which folds applyCommand over an array of commands, and stepCommand and runOut, which also append the best bid after each command to an output array. The cases cover every path of applyCommand, including empty books, prices equal to an existing level, above every level, and below every level, positions at and past the end, quantities and costs that wrap past 2^64, and arrays of different lengths. Native Lean prints its panic message for out-of-bounds reads and for insertIdx! past the end, and it returns the default value, as the compiled code does. In a session, eight addBid calls build a book from two empty arrays, removeLevel and two cancelBid calls change it, the host releases each superseded array, and the final book and the counters, with as many frees as allocations, match native Lean. tests/modules/chunks.py applies CLOB commands in chunks and one by one.

gpt.wasm holds the GPT kernels and composites, the cached step's functions, and the sampler. tests/gpt/run.sh compares every export with native Lean on chosen inputs, with empty and zero-sized arrays, arrays shorter or longer than their dimensions, infinities, NaN, signed zeros, overflow, subnormals, one to three heads, zero to three stacked layers, and caches built step by step. tests/gpt/sessions.sh checks that every session frees every allocation, temporaries included. exp matches native Lean bit for bit on special values, 400 points from -745 to 710, and arbitrary bit patterns. Against the C library's exp in native Lean, its error is at most 1 unit in the last place on 400,000 points from -745 to 710, 90 percent of them exact, and the special values match exactly. A session that appends a block of 1,000 words to a cache 256 times with appendBlock, which appends in place, ends with 4,128,768 bytes of memory and 11 frees: nine when the cache outgrows its block and two at the end.

forward computes the same function as Hugging Face's GPT2LMHeadModel (transformers 5.18.0, PyTorch 2.14.1, float64, attn_implementation="eager"), with every parameter drawn from a normal distribution with standard deviation 0.5 and 1 added to the layer-norm gains. Over ten configurations, with zero to twelve layers, one to four heads, widths up to 16, hidden widths up to 64, vocabularies up to 50, and up to eight tokens, and three seeds each, the largest difference between the two sets of scores is 2.7e-15 of the largest score. The differences come from the order of summation and from exp and tanh. The configuration with width 1 matches exactly.

On the GPT-2 124M weights, forward matches Hugging Face's model in float64. gpt2_compare.py writes the twenty weight arrays, about 1.0 GB, to files that the host loads with its file-u64:PATH argument kind. For prompts of 5, 30, and 224 tokens, every score differs from Hugging Face's by at most 6.4e-15 of the largest score, and the steps from an empty cache give forward's last row bit for bit. With the cache, the script runs one host session that loads the weights once with the session command file-u64 ID PATH, keeps each new cache with keep ID VALUE, and writes the scores to a file with save-u64 VALUE PATH. Greedy generation from a 5-token prompt to 256 tokens chooses Hugging Face's token at every step, with differences of at most 1.16e-13 of the largest score, and the session ends with about 1.08 GB of memory, the weights and about 100 MB.

lists.wasm holds listSum, listRange, and sumRange, and words.wasm holds Words.first, Words.sumAcc, and Words.range over a user list type whose Encode instance gives the layout of List UInt64. They match native Lean on lists whose sums wrap, long lists, and counts up to 1,000, and a sumRange call shows as many frees as allocations. The host's chain-u64: argument kind allocates the records and writes their headers, and its result kind of the same name reads the records in order and checks each header.

The decoder test runs the official testsuite: every valid module in the decoder's subset decodes to the reference and round-trips, and every malformed module in the subset is rejected. tests/verified/run.sh compares each module of the verified compiler with native Lean, checks the blocks that each call leaves allocated, and checks the accuracy of the numerical examples. The drone README describes tests/drone/run.sh, the verified compiler manual describes the verified compiler's tests, and the LeanExe compiler manual describes the WGSL tests.

Decisions

Both compilers

Decision	Reason
The system stays as small as possible. For the LeanExe compiler, per-program IR proofs prove what the proved rules do not cover.	LTG knowledge bases help with those proofs, and the verified compiler needs none for the programs in its dialect.
Development proceeds in increments. Each takes one program from Lean source to bytes, a proved Implements, a Wasmtime comparison with native Lean, an axiom audit, and a commit, adding only what that program needs.	Building whole layers before connecting them defers every integration error.
Implements is one statement over a Represent class. Every compiled module has a memory and the runtime globals.	A module without memory would make Heap.At false and the theorem vacuous.
Every object has one owner, values move at their last use, and an owned array at its last use is updated in place.	Lean values can be shared, so ownership must be established in the source: moves make every reference count 1, and release needs no count.
Runtime integers are fixed-width only, and panic compiles to default. The LeanExe compiler supports recursive values.	Bounded Nat traps where Lean returns the exact value, and Lean's logic gives default for an out-of-bounds a[i]!.
I/O uses a pure step function, State → Input → State × Output, driven by a fixed adapter, trusted until proved.	Each step call is pure, so Implements covers it.
release and the runtime counters are absent from the source dialect. Modules keep the counters as globals.	Their values are 0 in Lean and real in WASM.
Floating-point theorems describe the WebAssembly deterministic profile.	Talos implements it, and it matches Lean's float model.
Every module contains alloc and release at functions 0 and 1, with the allocation and free counters. release is not recursive: it frees an object and, through a loop over its masked slots, the objects it owns.	A recursive release uses one WASM stack frame per node.
Python tools are added to the repository only as uv-runnable scripts with PEP 723 metadata, always run with uv run.	Each script declares its dependencies, and no environment outside the repository is needed.
Implements states that a call returns the correct result or traps at unreachable, with no premise about free memory. Triple assumes that its assertion accepts that trap. alloc traps when memory cannot grow, the build template traps for 2 ^ 29 or more words, and every compiled module declares at most 65,535 pages, which Implements assumes of the memory's cap.	A premise about free memory does not compose across calls, because each call's bound adds to top and nothing bounds fragmentation. A trap is a visible failure, so the theorems describe every completed call. With at most 65,535 pages every block ends below 2 ^ 32, the bound the free-list proofs use. Total execution is stated separately, with ImplementsA and an allocator budget.
release checks the child mask before it reads any slots.	Freeing an array without child pointers would otherwise take one loop iteration per element to test a zero mask, and the check removes two nested loops from the proof of the common case.
Heap.Owned records that the object ends inside the 32-bit address space.	The freed block's free-list entry needs it, and every allocated block satisfies it.
Proofs may not use bv_decide or native_decide.	Both add an axiom that trusts compiled code.
The dialect's float array is Array Float, and FloatArray is not supported.	Lean core has no lemmas about FloatArray, and the loop of FloatArray.foldlM is private, so a proof about its fold depends on a private declaration. Array has public lemmas and literal syntax. In WebAssembly both types have the same unboxed layout. In native Lean, Array Float stores each element as a separate heap object, which costs speed and memory in native runs only.
A function returns several values as WebAssembly multi-value results, one per component: a pair is its first component's values followed by its second's, as in Represent for pairs.	This follows the pair representation the proofs use and needs no heap object per tuple. Arrays of flat records store each record as its words, as the grids example shows.
Implements has a frame clause that covers every region of the heap apart from the consumed blocks, which includes the caller's arrays and trees.	Composing a call with the callee's theorem requires it: a caller holding a new array must know the call leaves it intact.
Implements states that the memory's maximum size (memoryCaps) is unchanged.	A call after another call needs room in the store the first leaves, and room depends on the maximum size. The allocation rules prove the fact (Heap.NewArray.caps).
Heap.At requires at most 65,536 pages, and Heap.Borrowed requires only that the input lies below top and outside every free block.	A 32-bit memory has at most 65,536 pages.
alloc follows Knuth's first fit and release his liberation with a sorted list (TAOCP vol. 1, §2.5, Algorithms A and B). alloc places the object at the upper end of the first free block that fits and shrinks the block when at least 56 bytes remain. release inserts the block in address order, merges it with free neighbors, and leaves top unchanged.	First fit without splitting or merging leaks memory whenever allocation sizes change between calls: the growing cache would need 5.05 GB for 256 positions. A simulation of the run peaks at 100 MB with splitting and merging.

The LeanExe compiler

Decision	Reason
The LeanExe compiler is verified rule by rule, and each proved rule gets an LTG entry.	Each rule's theorem shortens every proof that uses the rule, without enlarging the trusted base.
The LeanExe compiler reads unfolding equations (getUnfoldEqnFor?), so a recursive call appears as a call of the definition.	It avoids recognizing the term shapes Lean generates for structural and well-founded recursion.
The LeanExe compiler emits the IR as a definition and the module as compile ir.	The module is tied to the IR by definition, and a wrong compiler match makes the proof fail.
The LeanExe compiler emits hints keyed to positions in the decoded module. They can move into a WASM custom section, with names in the name section, when proving from the bytes alone becomes a goal.	Hints need not be exact. The decoder skips custom sections, so no theorem changes.
Statements get wp rules only, packaged as Triple over the store and IR state. while is the only loop, with a done local for several exits.	It keeps one semantics, Talos's, and adds no simulation theorem. Every IR rule is a lemma about WASM code, which serves proving from bytes.
Expr.eval with Expr.program_spec serves as the expression rule.	It is proved, and per-program proofs can rewrite with the evaluator.
Programs use Lean's Float and Float32. Float.ofBits compiles to f64.reinterpret_i64, and a proof must show that its argument is not a NaN pattern.	Lean's model replaces a NaN payload with the canonical NaN, and f64.reinterpret_i64 keeps it.
LTG is a directory of entries, searched directly and checked by a Lean script.	The script checks that every declaration an entry names exists.
Expressions read memory: Expr.eval takes the memory, and Expr.read compiles xs[i.toNat]! to a bounds-checked load. Statements are the only writers, through store address value, with 64-bit words and 32-bit address wrapping.	WebAssembly loads are expressions, and a read inside an expression keeps each program's proof close to evaluating the source.
A value that needs statements (a load or a loop) compiles to statements before its expression, placed inside the branch that needs them, never hoisted out of an if. Array.foldl with a lambda and default bounds becomes a counted loop, Nat.toUInt64 xs.size a load of the length word, and an array literal of k elements an allocation of 48 + 8(k + 1) bytes followed by stores.	Hoisting a load out of a guarding branch can trap where Lean returns a value.
The LeanExe compiler places a fold's statements before the value that contains them, so it rejects a fold in a value-level branch, in a fold or loop body, or in a recursive definition.	Placement inside value-level branches and loop bodies is added when a program needs it.
GPT-2 is the target: the same function as OpenAI's published code and Hugging Face's PyTorch model. Attention has nh heads of width dh, with d = nh · dh, and the four linear layers have biases. Tests compare with Hugging Face's model in float64.	Passing nh and dh leaves no invalid head configuration. Both sides in binary64 differ only in summation order and in exp and tanh.
The number of layers is a loop parameter: LeanExe.loop has an array state, its body may call allocating functions, each iteration releases the previous state, and the kernels read each layer's weights at an offset in stacked arrays.	A loop keeps the composition inside the proofs. GPT-2 fixes the layer count only through its weights.
The loop copies its initial array into its state, so the state is always owned and each iteration releases the previous one. The loop body is one call that returns the next state.	With one call in the body, the loop rule needs one callee specification and one Live step per iteration.
The GPT-2 124M test uses the pinned openai-community/gpt2 checkpoint (revision 607a30d783dfa663caf39e06633721c8d4cfcd7e), widened from binary32 to binary64, with prompts of at most 256 tokens. The test script writes one file of little-endian words per array, and the host loads each with file-u64:PATH.	Binary64 keeps the proved pipeline unchanged. The memory the calls use stays below 4 GiB.
Generation uses a key and value cache. A theorem proves that the cached steps give the same bits as the corresponding row of forward, so forward's softmax reads entries j ≤ i only, and forward and a step perform the same operations. Attention reads earlier positions from the cache and the new position from the new key and value, the layer loop's state holds the row and the new keys and values, and step appends the new block in place. The cache is one block per position, holding that position's key and value for every layer and its final hidden row, and a separate scores reads the last block.	Without a cache, generating to 256 tokens takes an estimated 3.8 hours. The design needs no capacity parameter and keeps the cached path inside the proved functions. Dropping the masked entries from the softmax leaves attention's output unchanged: Lean's max is if x ≤ y then y else x, so max acc (−∞) is acc, exp returns +0.0 below −745.2, and the running sum starts at +0.0, so adding +0 leaves it unchanged.
The generated composite proofs take the arguments apart with Represent.borrowed_float_pair, prove argument evaluation with one Expr.evalResults lemma per argument, and release temporaries with Live.releaseSecond_seq.	rintro on the undestructured argument tuple grows with the fourth power of the number of arrays, and simp over long argument lists costs seconds per call.
Attention is causal for all inputs: a masked score reads no key, and the product with v reads rows 0 to i only. Loops in value-level branches are unsupported.	An additive mask over all keys lets a later row turn an earlier row into NaN. The loop counts implement the mask without a compiler change.
Stmt.fold is a definition built from existing statements, and its rule lemma is stated about that definition. The fold body is an expression, so a nested fold is rejected.	The IR gains no constructor, and the lemma needs no new wp rule.
Rule lemmas state what they leave unchanged with State.Frame scratch writes before after: the same numbers of parameters and locals, and the same value at every local below scratch outside writes. A rule lemma takes a precondition that fixes the store and the state, and Triple.of_forall reaches that form from any precondition.	State.Frame is transitive, expressions preserve it (Expr.eval_frame), and the lengths let later assignments and scratch writes succeed.
Func.implements_heap takes arguments of any Represent type, and its body Triple may use Heap.At, the cap premise, and the arguments' representation in the initial store. It aborts or ends with some heap for which the invariant and the arguments' representation hold. Func.implements is its case for a body that keeps the store.	One entry rule serves every argument type.
The LeanExe compiler computes hint positions from code lengths, which do not depend on the scratch index.	The number of compiler variables, and so the scratch index, is known only after translation.
Triple takes the module as a parameter.	A call rule needs the callee's ReturnsOrAborts in that module, which wp_call_returnsOrAborts consumes.
call func args result is one IR statement for any function, with a rule parameterized by the callee's specification.	The same statement serves the runtime functions and calls between compiled functions.
An array literal that a fold consumes becomes a temporary: the compiler allocates it before the fold and releases it right after.	The fold is the temporary's only use.
IR f64 values are bit patterns, and Expr.eval applies Talos's IEEE64 functions. Per-program proofs connect Lean's Float through F64Bits.toBits_add and its siblings.	The IR means what its compiled code does, and the equality theorems appear once, as simp lemmas.
Func is typed: params and vars list the types of the parameters and the compiler's variables, and result pairs a type with an expression of that type. Scratch locals are 64-bit words.	Float arguments, results, and variables use WebAssembly's f64 type, and a load of an f64 adds f64.reinterpret_i64. A dependent pair keeps equations such as func.result = ⟨.u64, .get n⟩ free of casts.
Folds run over an Array UInt64 or an Array Float with a UInt64 or Float accumulator.	An Array Float is stored as the Array UInt64 of its elements' bit patterns, so the fold rule and the heap specifications apply to it unchanged.
Loops use LeanExe.loop (n : UInt64) (init : α) (f : UInt64 → α → α) : α, with UInt64 indices and xs[i.toNat]!, which yields 0 out of bounds. A loop state of several variables compiles to several locals.	Compiled UInt64 arithmetic equals Lean's, so no proof concerns overflow, and the loop rule resembles the fold rule. Nat.fold would need overflow facts for index arithmetic, a tail-recursive helper needs a proof of each iteration, and for loops would require recognizing the elaborated forIn. LeanExe.loop does not stop early, and LeanExe.repeatWhile and tail recursion cover early exit.
Programs build arrays with Lean's operations (set!, insertIdx!, eraseIdxIfInBounds, push). An owned array at its last use is updated in place, and any other use copies through one copying template, whose rule is proved once. One lemma per operation equates the operation to the template by Array.ext and core's size_* and getElem_* lemmas. LeanExe.build builds arrays computed by index.	The source is the specification. Core's lemmas about these operations serve later proofs about programs.
A module holds several functions: leanexe_compile name := [f, g, …] compiles the listed definitions, exports each, and compiles a call to a listed function as call. Each function has its own Implements theorem, and a call rule takes the callee's theorem as its premise.	Each callee is proved once. Inlining would repeat callee proofs at every call site, and separate linked modules need theorems across instances. The explicit list keeps the module's contents in the source.
The copying template runs a statement per element (Stmt.buildWith), so an element of LeanExe.build may run a loop. The statement may not allocate, and it may call only functions of scalars whose theorems state that they keep the store.	The matrix-vector product needs a loop per element. One rule covers the template with and without the statement.
Demos.Gpt.exp is a Lean definition, and the execution proof preserves its operations. Tests measure its accuracy.	Lean's Float.exp is opaque, so its numerical behavior needs a separate specification. The algorithm index lists the accuracy theorems for the verified compiler's separate implementations.
A function of scalars may be called in a loop body or an array element when its theorem, ImplementsPure, states that it keeps the store.	Softmax calls exp there. The general call rule cannot apply, because Implements does not say that a call keeps the store.
A let at the top of a function body may bind an array. The compiler releases it at the end of the function. Implements states that a call's result is fresh and that owned arrays keep their capacity.	Kernels combine by calls with intermediate arrays. Without freshness, Implements would allow a function to return its argument as its owned result, and a caller that released it would free its own argument.
-x compiles to -0.0 - x, Float.abs to f64.abs, and min and max to f64.le and a conditional. min and max evaluate their operands twice.	Subtracting from negative zero is exact and canonicalizes NaN as Lean's negation does.
The LeanExe compiler computes a float literal's bits, and proofs check them with decide.	The kernel evaluates Lean's Float.ofScientific for ordinary literals. Exponents beyond Lean's default threshold need options raised.
Top-k sampling runs in gpt.wasm as proved Lean code: sampleTopK scores k temperature state returns a token and the next generator state. It keeps every token whose score is at least the k-th largest score counted with repeats, as Hugging Face's TopKLogitsWarper does, and draws from weights exp ((s − max) / temperature). The generator is SplitMix64, in its own module prng.wasm with proofs and tests and also compiled into gpt.wasm. The CLI stays greedy unless --top-k is given. Without --seed it takes a seed from the operating system and prints it to stderr.	Sampling in Lean keeps the whole generation step proved, and the CLI only passes the generator state along. Hugging Face's rule is the reference users know. A printed seed makes every run repeatable.

The verified compiler

Decision	Reason
The verified compiler is a separate library, Verified, written as a Lean function from a typed source language with a denote to a module. It shares the trusted base and Implements with LeanExe and has its own definitions of the IR parts it needs.	The LeanExe compiler is meta code over Lean.Expr, so no theorem can cover it as a whole. A compiler over a source syntax can have one theorem for every program it accepts.
The verified compiler's reflector writes ordinary Lean definitions as source functions, and the kernel checks an equation for each. The reflector builds the equations and theorems as terms.	Programs stay ordinary Lean, and other libraries' programs compile unchanged. Terms let the kernel check each equation without unfolding a definition, which for a loop over literal data would run the loop pass by pass.
Expr.fold means the full Array.foldl and compiles to a UInt64-counted loop. The proof derives the size bound from the represented array, and the reflector accepts the default whole-array bounds.	The logical fold retains Lean's meaning on every array, and executable lengths and indices remain words. The rule reuses the loop's ownership, allocation, frames, and release proofs.
Array.insertIdx! uses a typed full-length comparison, the existing insertion, and an empty build. The comparison's compiled word-sized length is justified by the heap representation.	Lean returns #[] for an index beyond the length. The source preserves this result on every logical array, and the compiler reuses its conditional, comparison, insertion, and build rules.
A function's theorem is ImplementsA aborts, with aborts false when the code cannot allocate and takes no call depth.	Such a function gets a theorem that excludes a trap with no further proof.
Expr.paramChoice chooses each array parameter's mode, and an owned array at its last use is updated, extended, or shifted in its own block.	The theorem holds for every choice of modes, so the choice needs no trust and affects only the code's cost.
Recognized tail recursion uses typed return and continue nodes, fixed parameter modes, and a Wasm loop. The reflector derives a rank from Lean's generated induction theorem. set_option verified.tailLoops false retains guarded recursion.	The fixed-point equation establishes meaning, and the decreasing rank establishes termination. Continuing steps move or copy the next state under the same ownership rules as calls. Native step charges give the public allocation bound.
Guarded recursive functions and their callers take the call depth, trap at depth 1,000, and have at most 32 positions per frame. A tail loop takes depth when it calls guarded code and preserves that depth between iterations.	Talos bounds no call depth, and Wasmtime's stack is finite. At 8 bytes for each value live across a call and 16 bytes per frame, 1,000 frames of 32 positions take at most 272,000 bytes of Wasmtime's 512 KiB default stack.
The verified compiler computes an allocation bound from the code, and p.f.trapFree excludes a trap when top can rise by the bound within the memory cap. p.f.bound_eq states the bound in the function's parameters.	ImplementsA true holds of a module that always traps. A bound computed from the code needs no budget proof per program, and the equation lets a user prove a concrete bound by rewriting.
An owned array has the potential 4 · 8 (n + 1) ∸ 2c, and every owned array parameter of a function whose body extends an array is paid: the caller charges its credit.	The potential covers the bytes of a growing array's moves to larger blocks, so a loop of n pushes has a bound linear in n. A rule that pays a parameter only when its own value is extended differs by at most one credit per array per call, and neither rule gives the smaller bound for every program.
Constant tables are data segments, read as borrowed parameters, and wrappers pass their addresses.	A table needs no allocation and no copy, so Trig.sinWith and Trig.cosWith keep ImplementsA false, and the wrappers Trig.sin and Trig.cos keep ImplementsTables false.

Floating point

Lean 4.34 defines Float and Float32 through Float.Model and Float32.Model, IEEE binary64 and binary32 with round-to-nearest, ties to even. Every NaN in both models is the positive quiet NaN with only the top fraction bit set, 0x7FF8000000000000 or 0x7FC00000, and ofBits converts every NaN input to it. Talos's IEEE64 and IEEE32 return the same constants for every NaN result.

ProofKit proves LeanExe.Float32.xBits = Wasm.IEEE32.x for add, sub, mul, div, and sqrt, for all inputs including NaN. The binary64 counterparts for all five operations are the F64*.lean files and F64Bits. Lemmas that do not depend on the format are in FloatRounding, FloatShift, FloatRationalRounding, FloatSqrtRounding, and FloatCommon, which both chains import. IEEE64.roundDyadicMagnitude and roundRationalMagnitude pass rounded * 2^shift to roundScaledMagnitude where the binary32 rounders encode the fields directly, and roundScaled_mul_pow relates the two forms. F64Bits restates the results as (a + b).toBits = IEEE64.add a.toBits b.toBits for Lean floats. The wrappers are thin: LeanExe.Float32.addBits applies Lean's Float32 addition to decoded bits, so the theorems also justify compiling Lean's float types directly.

Lean and WASM differ in three places:

1. Lean's neg and abs return the positive canonical NaN for a NaN input. WASM fneg and fabs change only the sign bit.
2. Lean's ofBits canonicalizes NaN. WASM reinterpret keeps the payload.
3. Lean's min and max choose an operand by ≤. WASM fmin and fmax return NaN for a NaN operand and order -0 below +0.

The WebAssembly specification (numerics) makes the sign of a generated NaN nondeterministic and its payload canonical only when every NaN input is canonical. Its deterministic profile (profiles) requires that "All NaN values generated by floating-point instructions are canonical and positive," and Talos implements that behavior. tools/wasmtime-host.c enables Cranelift's NaN canonicalization. Browsers do not implement the profile, and on x86 0/0 produces a negative NaN. On aarch64, native Lean's toBits returns 0x7FF8000000000000 for a NaN with a payload, for 0/0, and for -(0/0). Modeling the full profile in Talos, with an oracle choosing NaN results and the compiler canonicalizing NaN where bits become observable, is the route if theorems must cover results computed in a browser.

IEEE64 has the same functions as IEEE32 and calls IEEE32.roundShift, roundQuotient, and roundSqrtIntegral directly, so lemmas about those helpers are imported, not copied. Binary64 comparisons follow from F64Compare.compare_canonical: decoding a non-NaN bit pattern gives a canonical unpacked float whose value is Talos's scaledValue, and Lean's comparison of canonical floats orders them by value. Negation compiles to -0.0 - x (F64Sign.sub_negZero), absolute value to f64.abs, and min and max to a comparison and a conditional, which removes the first and third differences. For Float.ofBits, the LeanExe compiler emits f64.reinterpret_i64, and a proof must show that the argument is not a NaN pattern. The verified compiler adds −0 after the reinterpretation, which gives the canonical NaN for a NaN pattern. F64Convert proves the conversions between UInt64 and Float, and F32Compare and F32Sign give the binary32 comparison and sign theorems. Conversions between Float and Float32 have no theorems.

GPU

The shared WGSL library defines the language subset, its printer and inverse parser, its semantics, and the proved translation of IR builds to kernels. Dispatch theorems prove kernel results and race freedom under buffer and invocation bounds. The model uses strict binary32 arithmetic. Applying the results to hardware assumes that the driver and device implement that model. The binary32 GPT application adds generate_host, which proves the scores of a generation step and race freedom under its shape, weight, and token bounds. The LeanExe compiler manual describes the translation and its tests.

The verified compiler's source lowering constructs an IR kernel with a proof of its source meaning, then uses the shared WGSL translation and dispatch theorems. Its binary32 GPT compilation uses the existing thirteen source functions. The host instance supplies their native dispatch theorems to the shared item, layer, and generation proofs.

Scope of the theorem

1. The claim is about Talos's semantics. Wasmtime appears only in tests, and the Talos interpreter and the decoder are trusted.
2. The premises Heap.At and Heap.Borrowed, and a memory cap of at most 65,535 pages, are assumed. Every compiled module declares that maximum. For the verified compiler's modules, p.initial proves that the store in which the module starts meets the allocator invariant and the cap and holds each table as a borrowed array. Instantiation of the LeanExe compiler's modules and the host executables remain outside the proofs. A call may trap at unreachable when memory cannot grow or an array would exceed 32-bit memory, and the theorems state the result of every call that does not trap. A module that always traps would satisfy them, which the verified compiler's p.f.trapFree excludes under its bound. Talos's memory.grow succeeds whenever the new page count is within the maximum, while the WebAssembly specification lets an engine refuse growth for its own reasons. alloc checks the result of memory.grow and executes unreachable on failure (MemoryGrowth.growProgram), so on such an engine the call traps and returns no result, a path the theorems do not describe.
3. Implements states a frame: every heap region below top, outside the free blocks, and apart from the consumed blocks keeps its bytes and lies apart from the result, and the memory's maximum size is unchanged. It states nothing about memory outside the heap that the allocator manages.
4. Emit.lean evaluates encode with compiled Lean code. For gpt.wasm, gpt_file in Demos/Gpt/File.lean, checked after the file is written, proves that the file holds encode gpt.module, exp_file in Library/Numerics/Float64/Exp/ExpFile.lean does the same for exp.wasm, and each transcendental module whose byte theorem is proved has a file module of the same form, which the Verified test driver checks in its loop over name:TheoremModule:FileModule entries. The elaborator binary_file% that reads the file is trusted. No theorem covers the other modules' files.
5. WASI entry proofs assume a host satisfying the three import specifications, valid byte and static-data representations, and separation from scratch memory. They preserve source effects through normal return, accepted exit, host trap, and permitted guest resource failure. Total execution additionally requires a typed resource-prefix bound and no reached host trap. The WASI proof premises state these conditions and the external assumptions about stream adapters, OS I/O, and real engines.

Open work

• LeanExe compiler: defaults from instances, records with array fields, and arrays whose elements own memory.
• LeanExe compiler: the host's invocation of kernels and a run in a browser.
• LeanExe compiler: a proof of the I/O adapter.
• LeanExe compiler: Array Float literals.
• LeanExe compiler: LTG entries for Stmt.append_spec, Stmt.repeatWhile_pure_spec, and Live.tupleLoop.
• Verified compiler: owned record and pair parameters.

The interpreter testsuite run recorded on 2026-10-10 passed 64,751 commands, with 346 skips and 27 decode errors on unsupported text forms. The exponential guide and the journal record its scope. The interpreter remains trusted. Talos bounds no call depth. Guarded recursive calls in both compilers trap at depth 1,000. Tail continuations use loop branches.

Commands

export PATH="$HOME/.elan/bin:$HOME/.cargo/bin:$PATH"
tools/leanrun --timeout 60m lake build
mkdir -p build/gcd build/sumArray
tools/leanrun --timeout 10m lake env lean --run tools/Emit.lean \
  Library.Numerics.Arithmetic.Gcd.Module Library.Numerics.Arithmetic.Gcd.gcd.module build/gcd/gcd.wasm
tools/leanrun --timeout 10m lake env lean --run tools/Emit.lean \
  Examples.SumArray.Module Examples.SumArray.sumArray.module build/sumArray/sumArray.wasm
wasm-tools validate build/gcd/gcd.wasm
build/tools/leanexe-wasmtime-host call build/gcd/gcd.wasm gcd i64 i64:48 i64:18
build/tools/leanexe-wasmtime-host call-stats build/sumArray/sumArray.wasm sumArray i64 \
  array-u64:1,2,3
tools/leanrun --timeout 10m lake env lean --run ltg/Check.lean ltg/entries
tools/leanrun --timeout 60m lake env lean --run tests/decoder/DecodeTest.lean \
  "$(command -v wasm-tools)" build/decode-test
uv run tools/gpt_composites.py            # regenerates Demos/Gpt/Composites.lean
mkdir -p build/gpt
tools/leanrun --timeout 10m lake env lean --run tools/Emit.lean \
  Demos.Gpt.Module Demos.Gpt.gpt.module build/gpt/gpt.wasm
tools/leanrun --timeout 20m lake env lean Demos/Gpt/File.lean   # the file holds the proved bytes
tests/gpt/run.sh                          # every export against native Lean
tests/modules/run.sh                      # the other modules against native Lean
uv run tests/modules/chunks.py            # CLOB commands in chunks and one by one
tests/gpt/sessions.sh                     # every allocation freed
uv run tests/gpt/hf_compare.py            # forward against Hugging Face in float64
uv run tests/gpt/gpt2_compare.py          # forward and cached generation on GPT-2 124M
uv run tools/gpt2.py --output-tokens 32 --prompt "It was a dark and stormy night"
uv run tools/gpt2.py --output-tokens 32 --top-k 40 --seed 7 --prompt "It was a dark and stormy night"
uv run tests/gpt/sample_frequencies.py     # top-k sampling probabilities
mkdir -p build/prng
tools/leanrun --timeout 10m lake env lean --run tools/Emit.lean \
  Library.Random.SplitMix64.Module Library.Random.SplitMix64.prng.module build/prng/prng.wasm
uv run tests/prng/compare.py              # SplitMix64 against the reference
tools/leanrun --memory-high 10G --timeout 12h lake build Verified Library
tests/verified/run.sh                     # the verified compiler's examples against native Lean

The decoder test expects build/decode-test to hold wasm-tools json-from-wast output for the testsuite scripts in the CodeLib checkout. For an example of the LeanExe compiler, the axiom audit is a Lean file that imports the example's Verify module and runs #print axioms on its theorems. For the verified compiler, the audit imports the files of Verified/Examples/ and runs #print axioms on each compiled.bytes and named theorem.