LeanExe proves behavioral properties of exact WebAssembly binaries by reasoning over the Talos execution semantics. The final theorem starts from bytes embedded in Lean, passes through checked decoding and validation, and identifies the resulting Talos module with the module used by the behavioral proof. Source programs, compiler internals, annotations, and proof-generation agents may help construct that proof without becoming premises of the retained theorem.
The source-driven path begins with a registered Lean declaration. tools/talos-artifact.js prepare compiles the declaration, renders the generated module as WAT, asks the pinned Talos generator for a Lean module value, and updates the tracked execution cache after successful generation. tools/talos-proof.js check regenerates that model and checks the handwritten behavioral theorem against it.
The exact-artifact path begins with a frozen program.wasm. It embeds the complete byte sequence in Lean, decodes the binary into raw syntax, validates the accepted Core 3.0 profile, translates the validated module to Talos, and proves equality with the execution cache used by the behavioral theorem. tools/artifact-proof.js checks the package identity, theorem declarations, logical dependencies, and behavioral result without reading source or invoking the compiler.
| Property | Source-driven path | Exact-artifact path |
|---|---|---|
| Initial subject | Current compiler output for a registered Lean entry | Registered immutable WASM bytes |
| Model production | WAT plus the external Talos generator | Checked binary decoder, validator, and translator |
| Compiler required during check | Yes | No |
| Source required during check | Yes | No |
| Behavioral theorem | Input-generic theorem over a Talos module | The same theorem after checked module equality |
| Primary use | Compiler development and proof construction | Independent verification of a distributed artifact |
The artifact format defines the binary and package boundary. Verifying a Program defines the commands and repository files for each path. The Talos proof inventory names the current theorems.
A behavioral proof normally states a Wasm.TerminatesWith result over represented inputs, allocator conditions, memory bounds, and a postcondition for return values and observable state. It enters the function through a weakest-precondition theorem, divides the body at semantic boundaries, and composes checked lemmas for calls, loops, branches, allocation, loads, stores, release, and final result construction. Application-specific mathematics supplies invariants, measures, representation relations, and the connection between returned words and the intended computation.
ProofKit contains reusable Talos theorems and tactics for recurring generated patterns. Its modules cover frames, memory reads and writes, arrays, allocation, runtime functions, direct calls, scalar transitions, traversal, bounded dispatch, loop composition, and result wrappers. Artifact-Proof Strategies gives general construction guidance, while the ProofKit reference names the checked API.
Generated proof packages preserve a frequent prose journal. The journal records which supplied help the agent found, which theorem or tactic applied, why an attempted abstraction failed, how the proof approach changed, and which recurring obligation lacks a suitable shared boundary. Journal observations are evaluated with the accepted proof and telemetry before annotations, ProofKit, LTG, or agent instructions change.
Compiler annotations describe selected regions of the structured instruction output. A region names its kind, exact structured location, parameters, and generating compiler functions. The current vocabulary covers direct calls, length dispatches, array searches and comparison nodes, encoded optional-index decoders, map and filter wrappers, array folds, scalar loops, pair results, and related composition boundaries.
The sidecar does not establish a fact about the distributed binary by itself. The annotation consumer validates the document, selects the corresponding region from the decoded artifact, and generates a Lean declaration whose equality or semantic adapter checks against that exact region. Any mismatch in artifact identity, path, interval, opcode, local index, constant, descriptor, or expected continuation prevents the declaration from checking.
Proof recipes name the generated equality, the compatible ProofKit theorem, its imports, and the premises the application proof must supply. Some recipes compose several checked regions, such as a bounded-length branch followed by allocation and a singleton result. WebAssembly Annotations defines the current schema and recipe-generation rules.
Compiler theorems currently help one part of annotation production. LeanExe.Wasm.ScalarCertificate proves that successful reification of supported scalar IR expressions, conditions, statements, loops, and encoded optional-index assignments agrees with the backend's structured instruction emitter. The compiler can therefore reject descriptor drift at the emitter boundary and issue a descriptor that follows from its own lowering definitions.
The encoded-index increment covers one recurring six-top-level-instruction decoder. The compiler recognizes an assignment from the zero-or-index-plus-one representation and proves its descriptor emission equal to backend emission. A separate structural scanner selects matching emitted regions and records their local roles without claiming that the IR recognizer produced them.
The artifact package checks the descriptor again against the exact decoded region. Its JavaScript matcher checks every decoder opcode, branch body, constant, and local role, and generated Lean proves equality between the selected interval and EncodedIndexDecoder.program. Recipe version two records the corresponding resolved-tail theorem in direct.tailEquality; the same field covers every version-two direct semantic recipe. The generator remains outside the trust boundary because Lean accepts each declaration only when reduction over the exact decoded program proves it.
The decoder theorem assumes the source word's zero-or-index-plus-one meaning. A search theorem or application fact must still connect the word to an optional result and establish any index bound needed later. The compiler-derived support therefore removes local decoder execution while keeping search correctness in the artifact proof.
The Demo 12 annotation pass preserved the frozen 2,183-byte artifact with digest 7cdd8adba75d4f076d0a142f824a19a0d34d6a5cedd1a810a417a7fc5789f7b6. It generated checked region and resolved-tail equalities for the decoder at path then@7/else@20, interval [2,8). Full package verification accepted the exact artifact and its existing behavior theorem with these declarations present.
The unguided reproof produced an accepted 542-line, 1,991-word, 25,612-byte proof after 5,604.715205 seconds of Stage 5 work. The agent used eight LTG entries, rejected two, and applied EncodedIndexDecoder.program_spec, but it did not use the generated <region>_tail_eq; it instead recovered the surrounding prefix through repeated Lean checks. Its journal has 74 paragraphs that mention an import check, including 26 checks after semantic completion that addressed elaboration placeholders rather than additional semantic reasoning.
The guided matched reproof used the generated equality in its accepted source and completed Stage 5 in 3,371.682385 seconds, 2,233.032820 seconds or 39.842 percent below the unguided run. Its journal has 36 import-check paragraphs, a reduction of 38 or 51.351 percent, while the accepted proof grew to 735 lines, 3,142 words, and 35,906 bytes. The two runs fix the formal specification, Lean source, WASM digest, annotations, ProofKit and LTG snapshots, and Codex version, but they remain separate generative runs; the comparison establishes uptake and one measured result rather than a general causal estimate. Independent package verification accepted the guided proof.
The general-tail and frame reproof used the first-match, decoder, and erase-copy tail equalities, as well as the broader decoder getter. Stage 5 took 5,903.365887 seconds, and the accepted source contains 1,059 lines, 50,046 bytes, and 45 private declarations. This result confirms that a fresh agent can retrieve and compose all three checked boundaries, but its proof is slower and larger than both the guided proof and the retained full-support proof. Independent package verification accepted the exact artifact theorem.
ClobDepth provides cross-program evidence for the decomposition shape. Its checked source proof applies EncodedIndexDecoder.program_spec twice and uses equivalent local tail equalities to replace whole-program decomposition, two generalize steps, reverse rewrites, and repeated structural premises. The refactor reduces the file from 116 to 112 lines and from 4,509 to 4,484 bytes, while its whitespace-delimited word count rises from 550 to 569; a focused build completed in 2.8 seconds. This proof states local equalities because it does not import a generated annotation package, so it demonstrates structural reuse without measuring generated-proof time.
The complete tools/talos-proof.js check clob_depth gate regenerated the source-driven artifact, required byte equality with the registered WASM, and built all 3,040 Lean targets. Project.ClobDepth.FoundPrepare rebuilt in 2.7 seconds during that gate. The check completed with exit status zero.
The same transformation did not improve ClobCancel. Its proof state begins before the resolved decoder branch, so the tail equality required an additional bridge, retained the existing generalize step, and increased the proof. The trial was reverted, providing a negative case for selecting the adapter from the current proof state rather than from annotation presence alone.
A complete source-to-WASM correctness theorem would support a second result with a larger stated dependency set. That theorem would connect source semantics, IR semantics, lowering, byte identity, and modeled WASM execution, allowing a source theorem to transport to the artifact. The current artifact-only path does not require that theorem, and the Source-Theorem Transport Plan keeps the two claims distinct.
The knowledge forest selects versioned packages whose LTG catalogs index checked proof assets, tactics, guidance, annotation support, and worked examples. A proof task starts with the forest, package category indexes, and artifact-derived features, then retrieves selected entry metadata and content as needed. Category memberships, feature terms, annotation kinds, consumer evidence, exclusions, related entries, declaration names, and tactic records support this selection.
tools/knowledge check validates package identities, dependencies, catalog structure, package-local source paths and imports, evidence bindings, and the selected forest. Promotion asks Lean to build package-local modules and resolve advertised declarations. tools/ltg check and tools/ltg metrics retain the detailed catalog and ProofKit checks for the core package, while Knowledge Forest and Structured LTG defines retrieval and lifecycle operations.
Narrow material remains in the catalog when it forms a checked worked example with a distinct lesson. Promotion to shared automatic selection requires recurring use or a reason that the entry describes a common compiler or WASM motif. Exact-artifact exclusions keep a measured task from retrieving its own proof, while separate forest selections control broader evaluation families.
A completed artifact proof can produce a knowledge package for later proof construction. That package may retain checked Lean support, guidance, or a worked example, and promotion places the reviewed package in a selectable forest snapshot. Later proofs still establish their own exact-artifact theorem, while any imported package-local theorem appears in the checked Lean dependency graph.
tools/leanexegen gives a proof-generation task the frozen formal specification, exact Talos program, selected annotations, ProofKit, a filtered knowledge-forest snapshot, and explicit instructions to iterate with Lean. The source-generation task and proof-generation task are separate, and the proof task does not receive the source. The outer process then runs package validation, import checks, artifact identity checks, and independent Lean verification.
The agent may ignore an annotation, knowledge entry, theorem, tactic, or suggested approach when it does not fit the goal. Acceptance depends on the resulting Lean theorem and package checks rather than on following a prescribed proof script. Reproof mode freezes the specification, source, and WASM so an experiment can change the selected forest without changing the subject.
Proof-generation time has the greatest weight because the work seeks practical artifact proofs, but no single timing result determines retention. Evaluation also considers independent acceptance, LTG retrieval, agent revisions, proof structure, local scaffolding, repeated derivations, shared theorem and tactic use, compiler-derived evidence use, and transfer to another artifact. Identifier length and raw word bytes do not count as proof complexity because descriptive names often record shared abstraction use.
Experiments preserve accepted, rejected, and censored outcomes. A fixed-artifact comparison holds the formal specification, source, binary, model, tool versions, task instructions, resource profile, and cache policy constant. A new demo provides out-of-sample evidence when existing artifacts share the structure targeted by an annotation or theorem.
The current demonstrations show useful transfer for fixed-array wrappers, searches, maps, filters, scalar post-test loops, array folds, frame accessors, allocator composition, and fixed results. Demo 12 adds a bounded early-exit first-match scan and a variable-length copy-and-shift result over a 2,183-byte artifact containing 597 instructions and five loops. Its baseline proof used the checked length dispatch, capacity, allocator, result-store, and copy-loop patterns, while constructing the inner search and erase reasoning locally; Stage 5 took 3,907.231 seconds, and the accepted source contains 860 lines, 3,516 whitespace-delimited words, and 39,249 bytes.
The first journal review produced two shared interfaces. FixedArrayFindIdxEq.program_spec executes the exact one-word literal-key first-match loop, while UInt64Array.At.eraseIdx!_of_reads reconstructs the erased array from target memory facts after allocation and copying. The compiler emits and the artifact consumer checks leanexe.array.find-idx-eq.v1, and an independently verified annotation package equates Demo 12's frozen search interval with FixedArrayFindIdxEq.program 8 0.
An exploratory fixed-artifact reproof retrieved and used both interfaces, rejected the fold support as a mismatch, and completed its artifact theorem in a focused Lean check. Concurrent editing changed a shared ProofKit module during the run, so the ordinary package gate could not rebuild a consistent dependency set. The attempt supplies structural evidence but no accepted proof-time measurement. The accepted baseline remains 3,907.231 seconds, 860 lines, 3,516 words, and 39,249 bytes.
FixedArrayCopy.program_spec now executes the complete raw-cell prefix and shifted-suffix loop pair, accepting either ordering of nonoverlapping source and target regions and preserving the target header and source reads. Its generated leanexe.array.erase-copy.v1 recipe supplies combined and per-loop equalities, while eraseIdxProgram_spec adapts the width-one, source-before-target case to public Array.eraseIdx! representation. A production annotation pass preserved Demo 12's artifact digest, checked the exact nested interval [53,59) against FixedArrayCopy.program 1 8 14 11 12 15, and passed a separate leanexegen verify -s rebuild of the complete package. The exact loop shape also appears in the CLOB matchFuel and limit functions at width five, but the current CLOB proofs need stronger global, ownership, and outside-region continuations and do not use the theorem.
The retained clean fixed-artifact reproof covers the unchanged digest 7cdd8adba75d4f076d0a142f824a19a0d34d6a5cedd1a810a417a7fc5789f7b6. A separate tools/leanexegen verify -s invocation accepted the measured package before the follow-up ProofKit changes. Stage 5 took 3,987.145392 seconds against the 3,907.231311-second baseline, an increase of 2.045 percent. A current-ProofKit re-freeze later preserved the digest and passed independent verification without running fresh proof generation or evaluating current LTG retrieval.
The accepted source decreased from 860 to 607 lines, 3,516 to 2,587 words, and 39,249 to 28,874 bytes, reductions of 29.419, 26.422, and 26.434 percent. It used seven LTG entries without rejection, reduced journaled checks from 47 to 38, and replaced every local search, prefix-copy, and shifted-suffix loop invariant with FixedArrayFindIdxEq.program_spec and FixedArrayCopy.eraseIdxProgram_spec. ProofKit now contains the dynamic local length-store theorem and encoded-index comparison fact identified by the journal. Erase setup and branch-aware result transfer remain under review.