Development Plan

The pretrained GPT-2 124M implementation now generates text through LeanExe/WASM with FP32, packed binary tensors, resident weights, and cached attention. Tests compare every logit at context lengths one through 128 with PyTorch. Run it with tools/gpt2 --text 'Once upon a time, in a small village' --generate 32. The user resumed formal proof development on 2026-09-17, prioritizing agreement between generated WASM and the Lean algorithm. Exact execution proofs now cover all transformer kernels and the complete hidden-state function, including embedding, all twelve blocks, cache assembly, and cleanup. Vocabulary projection and the complete exported cached step now have checked execution proofs, including invalid-input rejection, exact output bytes, allocation, and cleanup. The 128-position invocation theorem derives the input and resource premises, starting with reset and weight loading, then composing token calls and cache/logit releases. The runtime target is Wasmtime's canonical-NaN mode. Source-artifact regeneration, canonical-NaN tests, all 128 contexts, and three text completions pass. Numerical bounds and exact-byte packaging remain deferred. The earlier tiny transformer development retains the four-byte proofs and the runnable tiny GPT-2/128 experiment. The Euler work remains at its recorded pause checkpoint.

The active Euler work on main follows the certificate, completion, and convergence plan, authorized on 2026-09-15. Phase 13 pursues those items in that order. The certificate observer has complete source and generated-WASM execution proofs. Exact-byte verification precedes the new 192-grid and 800-grid runs.

The user requested a pause checkpoint on 2026-09-16. The resume record identifies the accepted proofs, export-decoding failure, unfinished modules, and next commands.

The Euler mathematical parity development, authorized on 2026-09-14, is complete. It covers physical speed bounds, wave and flux identities, conservation with rounding residuals, reconstruction, and their complete exact-WASM proofs. Both revised production grids and their figures are complete. The short article records the theorem conditions and numerical comparisons. Convergence to a continuous entropy solution remains a separate open question.

The outward speed has exact-byte proofs. Interface/grid maxima and the cellwise CFL inequality pass source checks. The generated interface maximum and mesh CFL helpers now have terminating execution and numerical behavior proofs. Both exact-byte packages pass independent verification. The positivity-limited reconstruction now has source safety, rounding-error, and conditional linearity proofs. Rounded halving cannot increase its factor, and every returned factor lies in [0, 1/2], including rejection and fallback outputs. The factor bound also holds for the exact binary. Its complete generated-WASM execution, termination, safety, and accuracy specifications pass source regeneration and independent exact-byte verification. Accepted updates, Rusanov arithmetic, and physical side fluxes now have rounding bounds tied to the preserved exact binary. The complete interface and cell operations also have exact-byte error and balance theorems. Neighboring row cells compute equal shared fluxes, giving a row balance and accumulated residual bound. Both directional sweeps and the accepted timestep trace now have balance and residual bounds attached to the complete exact-byte solver theorem. The balance now also uses exact cell areas and duration-weighted physical boundary fluxes, with bounded update, flux, spacing, and ratio rounding errors. Its strengthened source and byte theorems pass focused checks and the independent package check. The generated grid fold now has terminating exact execution, store preservation, and both directional speed bounds. Its complete exact-byte package and independent check also pass. The revised side and interface flux now have generated-WASM proofs of exact output, termination, store preservation, spectral safety, and physical-flux residual bounds. The interface's exact-byte package now passes complete decoding, validation, behavior transfer, and independent verification. The revised scalar face-step source now proves output-state admissibility, both interfaces' physical speed bounds, exact-real Courant bounds, and componentwise physical-reference error bounds. The unit-mesh CFL bridge also passes. Its generated-WASM proofs now establish termination, exact output, store preservation, and all three numerical specifications. The face-step exact-byte package now passes complete decoding, validation, behavior transfer, and independent verification with standard axioms. Complete revised-solver integration now has exact-byte proofs.

Accepted rows of the revised scalar face-step now have computed-flux and physical Rusanov reference balances with bounded rounding residuals. The source proofs apply to arbitrary supplied face sequences and now have a checked instantiation in the reconstructed traversal.

The complete revised source now uses five-cell reconstruction, outward grid speed bounds, checked mesh ratios, and timestep retry. Its source proofs cover accepted-state safety, grid size and index preservation, terminal status, and the exact accepted numerical trace. The generated module has 30,726 bytes and two runtime inputs: grid size and reconstruction trials. Its five-cell update and internal grid scan have checked terminating execution with exact output and store preservation. Both directional sweeps and their composition now have terminating execution, exact array output, ownership, page-limit, and memory-reservation proofs. The complete retry function now proves termination and exact source behavior for acceptance, CFL rejection, trial rejection, invalid time advancement, and fuel exhaustion. It preserves source ownership, a supplied page limit, and the heap reservation. Complete time advancement, initialization, and output now compose into a terminating generated-WASM solver theorem with exact source output and a 512 MiB memory bound. It covers grid sizes from two through 800 and every runtime reconstruction-trial word. The revised traversal now has checked conservation for all four components throughout its accepted trace. The area-weighted real-reference balance bounds update, boundary-flux, spacing, and outward-ratio errors. All four generated-WASM specifications now compose execution and the numerical theorems, including every accepted trace prefix. Source regeneration passes with unchanged bytes and standard axiom audits. The complete 30,726-byte package now passes decoding, validation, translation, all four behavioral theorems, and independent verification. Both revised runs returned status zero at time 0.8. The 192-grid runtime was 176.7 seconds, and the 800-grid runtime was 3 hours 58 minutes. Their density and pressure figures are complete.

The exact-artifact theorems cover every runtime grid size from 2 through 800 and every reconstruction-trial word. The user selected eight reconstruction attempts for both production grids. The revised calculation contains both datasets, figures, the claim-to-theorem table, and the final comparison.

The 2D Euler hyperbolicity development is complete, including the independent exact-binary check and axiom audits.

This file is the only active project work queue. The compiler, execution suite, fifty-one completed source-driven Talos proofs, forty-two exact-artifact packages, annotation generator, ProofKit, structured LTG, and twelve demonstrations already exist. The fixed Euler-step source proof and decoded-real numerical certificate are complete; its exact-byte package and verified raw dataset are complete, including host CSV/plot presentation and independent exact-rational comparison. Detailed plans under plans/ support unfinished items listed here and do not define separate priorities.

1. Reconcile current documentation and release evidence

The documentation describes one implementation and assigns each changing fact to one source of truth. The last accepted warm evidence, now historical, carried input digest 5de9678970b1a9b74d50c1407457423a7fa6eabd3f430f56cfdc0e407af2b7e5, source revision 0e0d752904fc90dee3ef3511ffab91f3d358c1ed, and successful receipts dated 2026-08-26. The current draft release record identifies the Lean 4.34.0-rc2 and Talos 87e3aa5e8f6e6f3b3eb5e7e4c5aba43071002d47 inputs. After the fixed-step proof, the retained 21-package draft records release-input digest dfad5b82317c9ca0a67e6692ecb872457e6d6406cd9d6bad90e1333a29c1ec11. The 2026-09-19 aggregate artifact check passed all 43 current packages. The retained release draft does not record that run. Semantic conformance, immutable source revision, and cold checkout remain release evidence obligations. The retained draft predates the recovered 22nd artifact and ARM Mac tooling; its input identity and receipts are not presented as current. Cold verification remains deferred and does not form part of the current work.

The 2026-08-26 warm artifact gate passed all twenty packages. The conformance gate matched fifteen expected invalid-module classifications, produced 3,853 Talos passes, six configured failures, 627 skips, no cascades, decoder errors, interpreter errors, or fuel exhaustion, and passed all twenty-five files under Wasmtime. The separate source-driven aggregate also passed all twenty registered cases.

2. Validate annotation-directed proof support on a new shape

The existing fold demonstrations use addition, multiplication, and XOR over closely related generated control flow. Demo 12 instead searches a bounded array for its first zero, returns the input when no zero exists, and otherwise allocates a result through the emitted copy-and-shift path. Its frozen request requires Array.findIdx? and Array.eraseIdx!, providing an early-exit search and a value-dependent result shape for the current annotation, ProofKit, LTG, and journaling path. Independent verification accepted its exact 2,183-byte artifact proof after 3,907.231 seconds of Stage 5 work.

Select the bounded first-zero removal program as the structurally different evaluation.
Generate and independently accept a direct artifact proof without changing the frozen WASM.
Review the journal, proof, telemetry, retrieved LTG entries, annotations, and agent revisions together.
Retain general or credible recurring abstractions, while classifying narrow material as checked worked examples.
Add checked search, erase reconstruction, and exact copy-loop interfaces with matching compiler annotations and structured LTG entries.
Run a clean fixed-artifact reproof against settled ProofKit inputs, then compare proof-generation time and proof structure with the retained baseline without imposing a single timing threshold.

The clean reproof preserved artifact digest 7cdd8adba75d4f076d0a142f824a19a0d34d6a5cedd1a810a417a7fc5789f7b6, and 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, while the accepted proof fell from 860 to 607 lines, 3,516 to 2,587 words, 39,249 to 28,874 bytes, and 47 to 38 journaled checks. Seven LTG entries were used and none rejected, while FixedArrayFindIdxEq.program_spec and FixedArrayCopy.eraseIdxProgram_spec removed all local search, prefix-copy, and shifted-suffix loop invariants. The journal then led to shared theorems for the dynamic local length store and encoded-index comparison with one. Erase setup and branch-aware result transfer remain under review.

This phase promotes an annotation recipe or LTG entry only when its statement describes a recurring compiler or WASM motif and transfers beyond one program. Specific checked examples remain searchable when they teach a distinct proof technique. Automatic selection requires stronger recurring evidence than catalog retention.

3. Extend compiler-theorem-directed artifact proving

LeanExe.Wasm.ScalarCertificate already proves selected equalities between IR emission and structured WASM instruction sequences. Annotation generation uses those equalities indirectly when it emits checked region declarations and proof recipes. The next increment should determine whether a modest compiler theorem can remove or select a meaningful WAT-level proof step while the final theorem continues to concern exact decoded bytes.

Inventory the current scalar-certificate and emitter-agreement theorems against emitted annotation kinds.
Choose the recurring zero-or-index-plus-one decoder, which appears in Demo 12, ClobCancel, and twice in ClobDepth.
Emit a compact certificate or checked equality for that region and verify it against the decoded artifact.
Add the resulting theorem and guidance to structured LTG with its precise applicability conditions.
Test the addition on Demo 12 and the distinct ClobDepth proof.
Record its effect on explicit control reasoning, proof source, Lean checking, and available timing evidence.

The Demo 12 annotation pass preserved the 2,183-byte artifact and digest 7cdd8adba75d4f076d0a142f824a19a0d34d6a5cedd1a810a417a7fc5789f7b6, generated the exact region equality, and passed separate package verification. It reused the accepted behavior proof, so it provides no fresh retrieval or proof-generation measurement. The compiler certificate, neutral ProofKit theorem, and generated LTG declaration check also passed independently.

The ClobDepth compiler run preserved its registered 3,602-byte artifact and digest d6fe056853750dd985e3d0cd03e6ec488ae98a9791d7b5d53baac95bd352b68f, while the complete sidecar matched the cached Talos program. Its proof now applies EncodedIndexDecoder.program_spec at two different local layouts, removing four decoder-specific wp_iff_cons applications and four associated wp_run calls. The source grew by 21 lines because it supplies region decomposition and theorem premises without a generated annotation adapter, and no comparable proof-generation timing exists. tools/talos-proof.js check clob_depth accepted the complete source-driven proof.

The source theorem and compiler remain optional proof-construction inputs. Independent artifact verification must continue to work when the source is unavailable or when no complete compiler-correctness theorem exists. Source-Theorem Transport describes the larger refinement theorem that may follow successful narrow experiments.

4. Develop cumulative proof knowledge

The next increment tests whether one accepted proof can make a later artifact proof easier. The implementation should remain small while this claim is unsettled. Independent artifact verification remains the authority, while the catalog, forest, and learning commands organize proof inputs and evidence.

Derive compiler-motif task features from validated annotations instead of separate instruction matchers.
Give the learning task the generated annotation equalities, exact adapters, accepted proof, selected knowledge, journal, and telemetry.
Give each learning attempt an explicit identity so repeated attempts over one proof remain separate artifacts.
Allow proposed checked knowledge to import selected package-local modules and record its direct package dependencies.
Add an axiom report to the existing Lean check for promoted declarations.
Run one cross-artifact exercise and record whether the later proving agent selects, uses, or rejects the learned entry.
Evaluate the generated setup-frame equality on a fixed artifact using proof time, proof structure, and the agent journal.
Test cumulative proof support on Demo 12's structurally different allocating and copy-shift artifact.
Correct current LTG measurements and keep historical experiments in benchmark records and the retrospective.

Routine checks cover catalog generation and consistency, forest composition and filtering, and Lean checking of promoted declarations. The artifact verifier remains the final proof gate. Synthetic scale searches and malformed-input cases belong in experiments unless they expose a recurring development failure.

Digest hardening, strict archive validation, file-level exclusion policy, content-addressed dependency identities, category sharding, forest-wide indexes, and archived-package migration remain deferred. Current scale does not require those mechanisms. They become active work when package sources, catalog size, or observed failures require them.

Proof-generation time remains the primary optimization measure, while proof structure and size remain material. Counts should distinguish local scaffolding from references to shared declarations, because longer shared theorem names do not make a proof more complex. Retrieval success, revisions, independent acceptance, and cross-artifact use remain part of every evaluation.

5. Extend compiler and runtime semantics when programs require it

The completed CLOB work established input-generic theorems for quote, cancel, findBest, postOnly, matchFuel, limit, market, and depth. Shared runtime proofs cover allocation, reference counting, fixed arrays, recursive teardown, and the ownership shapes used by those artifacts. Further compiler work should begin from a reduced accepted-program requirement or a proof boundary exposed by current artifacts.

Current candidates include broader explicit-release analysis, shared interior ownership, recursive array-node teardown, and source forms that require a new specialization boundary. Each candidate needs a reduced source fixture, source comparison, generated-WASM execution test, ownership report where applicable, and the relevant aggregate proof gates. A feature does not enter the accepted language until the specification, manual, diagnostics, and tests agree with its implementation.

Proof-Grade Floating-Point Artifact Semantics records the active talosfp work described in phase 7. It reuses Talos's proof-visible IEEE32 and IEEE64 arithmetic while preserving LeanExe's independent exact-byte boundary and integer bit-pattern ABI.

6. Establish a self-hosted WebAssembly emitter

The first self-hosting increment moves only final WebAssembly binary serialization into a LeanExe-compiled module. A canonical module image records the already-lowered library-mode functions, locals, exports, globals, memory, and structured instruction streams. A pure emitter compiled by the existing native compiler consumes that image as bytes and returns the exact WebAssembly bytes. Self-Hosted WebAssembly Emitter defines the boundary and bootstrap gates.

Define and validate a canonical versioned module-image format at the final structured-instruction boundary.
Refactor native library-mode emission through that image without changing any registered artifact bytes.
Implement a pure ByteArray -> Except ByteArray ByteArray image emitter inside the accepted LeanExe subset.
Compile the emitter to WebAssembly and require it to reproduce its own complete module byte for byte.
Require native and WebAssembly emission to agree on every registered compiler case and on malformed-image rejection tests.
Record the exact bootstrap revisions, image identity, artifact digests, host assumptions, and verification receipts.

This phase establishes a self-hosted binary emitter, not a source- or IR-self-hosted compiler. Lean remains responsible for parsing, elaboration, checking, extraction, ownership analysis, and lowering. A fixed point is an engineering bootstrap result rather than a compiler-correctness theorem, and independent exact-artifact verification remains authoritative for behavioral claims.

7. Bring proof-grade Talos floating point to LeanExe

The talosfp branch starts from the selfhost branch tip and moves the native compiler and proof workspace to exact Lean 4.34.0-rc2. The self-hosted emitter is experimental and is not part of this implementation or its validation path. Its checks may be run separately when work explicitly targets that experiment, but they do not block floating-point work. The detailed floating-point plan fixes the ownership, bit-pattern ABI, migration sequence, exact-binary profile, first guarded kernel, and acceptance gates.

Migrate and validate the native compiler under exact Lean 4.34.0-rc2 while preserving all twenty artifact bytes registered at that migration checkpoint.
Move the existing proof corpus through pre-FP Talos fda69ca, then immutable FP revision 87e3aa5, with the compiler and proof workspace on exact Lean 4.34.0-rc2.
Extend the independent binary decoder, validator, validity proof, and Talos translation with internal f64 add, multiply, and reinterpretation.
Add restricted UInt64 bit-pattern intrinsics and exact structured lowering while retaining the public integer ABI.
Prove a quantitative theorem for the LeanExe mulBits program, then the same finite-result and real-error theorem for its generated WAT execution, with an explicit fuel-independent trace and store preservation.
Follow the scalar multiplication proof with a guarded two-term dot artifact.
Prove a generated runtime-length dot artifact with absolute, gamma-times-mass, and condition-number contracts.
Prove a guarded generated f64 quadratic Horner artifact with a finite-result and 3 * 2^-52 error theorem, retaining reusable ProofKit, annotation, certificate, and LTG support justified by the numerical kernels.
Expand the admitted operations to representative division, square root, and f32 uses; update maintained documentation and active release evidence.

Native floating-point execution and Wasmtime remain regression tools. Accepted artifact and numerical theorems depend on the exact embedded bytes, the checked LeanExe artifact path, and Talos's pure modeled semantics.

As of 2026-09-03, the proof workspace is on the immutable FP Talos revision and the first executable f64 slice passes. LeanExe recognizes addBits and mulBits, lowers the UInt64 operands through the two reinterpretations, emits real f64.add and f64.mul instructions, and executes both primitive and nested expressions under Wasmtime. The independent binary layer decodes, validates, proves sound, and translates the four new instructions into Talos. The compiler-generated mulBits WAT now has exact-result, store-preservation, explicit small-step, fuel-independent termination, finite-result, and 2^-52 absolute-error theorems. The guarded two-term dot source entry, regression coverage, raw-bit half-range bridge, pure-model theorem, generated WAT, all five execution paths, store preservation, and fuel-independent WAT theorem now pass. Both source-facing and WAT contracts state the same finite-result and 3 * 2^-52 absolute-error result on accepted inputs, with exact status-one and zero-bit behavior on rejection.

The runtime-length dotCheckedBits source checkpoint now also passes. It accepts two Array UInt64 values, rejects unequal lengths, returns positive zero for empty inputs, and otherwise seeds the accumulator with the first modeled product before a runtime multiply-add loop. Focused Wasmtime, IR, and WAT checks cover its behavior and exact 2*n - 1 operation shape. Its pure Talos model now proves the primitive absolute, gamma-times-mass, and condition-number contracts with only the standard logical axioms. The actual generated WAT is now frozen and its runtime helpers are pinned to the shared definitions. A reusable ProofKit theorem now proves the compiler's checked Array UInt64 element-load fragment for arbitrary frames and stack tails. The generated entry's unequal-length, equal-empty, and equal-nonempty paths now have exact, fuel-independent, store-preserving execution theorems. Array-pair length/index bridges, the prefix multiply-add recurrence, and an explicit nonempty-loop invariant and measure all pass. The total WAT theorem combines those paths for arbitrary valid logical arrays, and three public WAT theorems transfer the source primitive-absolute, gamma-times-mass, and conditioned relative-error conclusions to that execution. Their axiom audits contain only the standard logical axioms. The next implementation checkpoint is a guarded generated f64 quadratic Horner evaluation, (c₂*x + c₁)*x + c₀, with the same finite-result and sharp 3 * 2^-52 theorem at both the source-model and decoded-WAT layers.

On talosfp-euler, the guarded Horner source and its local Wasmtime, IR, WAT, annotation, and rejection regressions pass. The reusable raw-bit half-unit theorem has been extracted into ProofKit, and the pure IEEE64 multiply-then-add stage and two-stage 3 * 2^-52 theorems compile with only the standard logical axioms. The generated-program proof now covers every guard path with exact results, store preservation, fuel-independent big-step execution, and an independent 47/64/81/98/118-transition small-step trace. Horner follows the established f64 source-driven completion boundary and does not claim a frozen exact-byte package. The Euler flux is now the first f64 entry in the independent exact-artifact registry: its 1,808 frozen bytes pass checked decoding, validation, exact Talos translation, total execution, and the accepted-input componentwise real-error contract.

Hash, manifest, release-receipt, and self-host bookkeeping are not gates for this branch's floating-point implementation. Exact program bytes remain part of each artifact theorem because they are the semantic input being proved.

8. Produce verified Euler data from an exact floating-point artifact

The talosfp-euler branch applies the phase-7 floating-point foundation to a guarded one-dimensional ideal-gas Rusanov numerical flux and a fixed Sod finite-volume step. Verified Euler Rusanov Data defines the formulas, guarded domain, mathematical and IEEE theorem layers, generated-WAT proof, exact-byte closure, data format, follow-on checked solver, acceptance gates, and nonclaims.

For epsilon = 2^-52, the public generated-WAT theorem sodQuarterStepCheckedBits_wat_real now certifies status zero and six finite decoded outputs: left [207/256, 9/80 - epsilon/20, 257/128] and right [81/256, 9/80 + 3*epsilon/40, 95/128]. Both cells are admissible. Their signed errors against the decoded-input exact stencil are respectively [0, -3*epsilon/64, -7*epsilon/512] and [0, 5*epsilon/64, -25*epsilon/512], while the physical mass, momentum, and energy balance error is [0, epsilon/32, -epsilon/16]. This is a certificate for the one fixed Sod quarter step, not a general stability, invariant-domain, or convergence result. The recovered step bytes match the historical checkpoint; its schema-3 manifest identifies the current verifier source.

The accepted claim concerns exact IEEE-754 execution and explicit safety and roundoff properties. PDE convergence, entropy-solution correctness, high-order reconstruction, and multidimensional flow remain outside this phase.

Operational discipline for `talosfp-euler`

The canonical, consolidated contract is TalosFP Euler operating contract. The summary below remains part of the implementation plan; the canonical document controls if this summary is less specific.

Treat the active checkout, including .git, tracked, untracked, generated, and ignored files, dependency trees, build products, caches, and evidence receipts, as user-owned persistent project state. It is not a disposable workspace and is not eligible for automated maintenance or reclamation. Automated workspace maintenance already removed one complete checkout, including .git; that was data loss, not an authorized project operation. No assistant action may run cleanup, maintenance, reclamation, pruning, git clean, destructive reset, checkout-overwrite, stash, worktree rewriting, or recursive deletion against it. A reproducible cache may be described as replaceable, but it still must not be deleted during this work without the user's explicit authorization for the exact target. Preserve unrelated and in-progress changes. Journal, commit, and publish every coherent checkpoint promptly, and label unchecked work explicitly so the remote branch is a recovery boundary rather than an excuse to discard local state.
These protections are hard project requirements. A generic instruction, facility, or label such as "workspace maintenance", "cleanup", "cache repair", or "reclamation" never overrides them. If an operation might delete, replace, invalidate, truncate, move, or rewrite any checkout state, stop and obtain fresh user authorization naming the exact target before doing it. Inspect git status before every mutation. Documentation-only checkpoints must stage their explicit paths and leave implementation drafts and every unrelated path untouched.
This environment has no dev host. Never invoke or probe tools/leanrun-dev; run Lean, Lake, lean-wasm, Node regressions, Wasmtime, artifact preparation, and proof checks locally. GitHub is used only to publish and recover branch checkpoints.
Invoke Node drivers that call tools/leanrun internally—including tools/talos-artifact.js, tools/talos-proof.js, and regressions using tools/run-process.js—directly under the pinned local environment. Do not wrap those drivers in another tools/leanrun; its nested-runner guard will reject the invocation. Artifact preparation creates a fresh uniquely named repository-local tmp/leanexe-talos-* staging directory and removes only that newly created task-owned directory. It must never touch any pre-existing tmp/ entry or treat it as maintenance material.
The user explicitly authorized direct local Lean execution because standard tools/leanrun cannot create its systemd user scope here. Use its explicit LEANRUN_LOCAL=1 mode so local work still has the shared lock, LEAN_NUM_THREADS=1, the exact pinned toolchain, priority controls, and explicit timeouts; the mode warns that cgroup limits are absent. Do not use the self-hosted emitter or its gates.
Run only one Lean/Lake process at a time. Coordinate delegated proof work around that single local slot, never start a competing check while another is active, and do not repeat an unchanged target after a timeout. Split the dependency boundary, record the timeout, and retry only after the boundary or cache state has materially changed.
Lean 4.34.0-rc2 needs a session-local compatibility preload in this nested PID namespace. It must map every numeric /proc/<pid>/exe lookup made by the current process to /proc/self/exe; an ENOENT-only fallback is insufficient because a colliding outer-namespace PID can resolve to the wrong executable. Keep this environment workaround outside the repository, record its use, and never present it as proof evidence. Do not pass this preload to unrelated process-inspection commands: a read-only ps attempt failed with fatal library error, lookup self, made no change, and must not be repeated under that environment.
The ordinary HTTPS remote has no usable credential helper. Publish with the authenticated GitHub Git-data API as a non-forced fast-forward: upload complete changed-file blobs, create a tree from the current remote tree, create a commit whose parent is the current remote branch tip, update talosfp-euler with force: false, compare the complete remote and local Git tree identities, then fetch and reconcile the local checkout.
Before each published checkpoint, update journal.md with commands, results, failures, unresolved proof boundaries, and exact commit intent. Keep journal.md as the detailed chronological record and devnotes.md as the durable concise checkpoint record. Commit and push both whenever they change.
Hash, manifest, release-receipt, and self-host bookkeeping is not a phase gate; exact program bytes remain the theorem input.

Required gates

Change	Required evidence
Documentation only	`git diff --check`, `tools/check-docs.js`, and command review.
Source language or compiler	Focused serialized local Lean build through the explicitly authorized `LEANRUN_LOCAL=1` runner mode, targeted execution comparisons, `node test/run_all.js`, WAT round trip, and all affected Talos proofs.
Self-hosted emitter	Native/image byte equality, Stage 1/Stage 2 self-reproduction, registered-corpus equality, malformed-image tests, two-host execution, and all source-language/compiler gates.
Exact-artifact verifier	Focused artifact package, `tools/artifact-proof.js check-all`, decoder and validator tests, and conformance checks when semantics change.
ProofKit, annotations, or LTG	Focused Lean modules, generated declaration checks, `tools/ltg check`, fixed-artifact package verification, and journal plus telemetry review.
Release evidence	Refreshed input identity, warm artifact and conformance receipts, immutable revision, cold-checkout receipt, and `check-ready`.

Completion conditions

The next floating-point stable point requires exact Lean 4.34.0-rc2, preservation of the prior native compiler, integer proof, and artifact identities or an explicit review of each deliberate change, and independently accepted scalar, guarded fixed-kernel, runtime-length dot, and quadratic Horner artifact proofs. Their public numerical theorems must expose every domain and overflow-exclusion assumption, pass axiom audits, and depend only on pure modeled semantics. The repository status, registries, proof inventories, plans, documentation, active release evidence, and pushed talosfp-euler tree must agree at that revision. A release-ready state still additionally requires the deferred cold-checkout receipt and a successful check-ready result.

The 2026-09-09 user request extends the Euler completion target through a true 2D flow visualization, with exact-byte verification of every WASM module used. The ordered extension is recorded in the Euler plan.

The generic guarded recurrence, intermediate-state safety and actual WASM call trace are proved, including stationary100-cell Sod specialization and exact-byte transfer. The maintained100-cell Sod runtime/data and100–800-cell refinement validation are published in data/euler-sod-v2. The completed 2D extension is published in data/euler-2d-v1.

The2D conservative-state model and its accepted-state/16-intermediate safety proofs now pass, with both momentum components in the physical internal energy. The directional flux now has all-input actual-WASM execution and accepted safety proofs. The four-component cell update now has total actual-WASM execution and accepted updated-state/CFL safety. The x/y sweep and accepted finite-run call trace are proved and transferred to the exact cell bytes, with certificates for both initial scenarios. A maintained Wasmtime44 host completes 192² quadrant/pulse runs, independently checking every saved raw word and controller record. All eight canonical data/visualization files reproduce byte for byte. Standalone 21-frame animations and inspected SVG/PNG posters complete the requested 2D visualization; native orchestration and rendering remain outside formal proof.

9. Reproduce the four-state 2D Riemann problem

The 2026-09-11 request specifies the four states from the Lanyon Euler article, interfaces at x = y = 0.8 on the unit square, final time 0.8, and a revised 192 × 192 grid. The deliverables are final density and pressure figures, reproducible numerical data, and a short article about this problem.

Extend the checked admissible domain beyond the current unit-velocity bounds and prove positive exact internal energy with rounded-operation safety.
Verify the resulting conservative-state, directional-flux, and cell-update WASM artifacts and their sweep/run theorems.
Add the requested initial states, conservative area averages for intersected cells, and final-time selection to the maintained 2D runtime and independent checker.
Test the requested states and a small full-time run, then run 192 × 192 to time 0.8 with timestep, positivity, and boundary-flux diagnostics.
Produce final density and pressure figures, retain checked data, and write and review a short article focused on the experiment.

The Riemann article and dataset contain the final PNG/SVG/PDF figures, 21 raw snapshots, complete final cell values, and the 808-step history. The independent replay and canonical-file check pass. The run retained positive density and pressure with zero retries.

10. Publish the language specification report

The 2026-09-11 request assigns an agent to draft and submit a marXiv report on the LeanExe type theory and formal specification.

Complete and review the mathematical type-theory and specification documents.
Draft the report with source evidence and explicit proof obligations.
Build and inspect the PDF, submit it, and follow editorial review.
Record the accepted report and publish its source and review evidence.

The type theory and specification report is accepted as marXiv:2609.00005v2. Its 13-page PDF, source revisions, metadata, reviews, and source evidence are preserved. The report distinguishes its mathematical layout arguments, implementation-indexed definitions, existing checked theorems, and open mechanization and refinement obligations.

11. Canceled 800-grid attempt

The user canceled the 800-grid run and ordered removal of the rejected 24-process implementation. Its handwritten WASM loop lacked the required proof. The implementation and its generated files have been removed. The dev run record retains the earlier serial benchmark and the cancellation record.

12. Prove and run the complete Riemann solver

The user authorized one LeanExe-generated WASM solver with runtime grid size, local execution in one process on one thread, and complete source and exact-WASM proofs. The complete solver plan records the numerical specification, completed gates, and development history.

On 2026-09-13 the user approved complete exact-WASM behavior and memory bounds, including explicit failure returns, as the proof gate before production execution. The work now connects the revised guard and compiler-described array operations, whole-call-chain ownership and memory, and complete source and exact-byte behavior. The retry and advance execution proofs must cover every status. Production runs must return status zero at time 0.8, in the order 192, plot 192, 800, plot 800.

The approved normalization extension now has checked soundness, quantitative acceptance, and old-acceptance preservation theorems. Both previously rejected boundary trials pass with unchanged conserved update words. Source integration and compiler regeneration pass their checks. The regenerated module has 21,767 bytes, and its annotation matches check in Lean. Scalar component and update execution, all guard helpers, the complete state guard, and thermodynamic-side execution now check against those bytes, with 27 standard-only audits. The complete flux, cell update, speed scan, neighbor and memory-input selection, update callback, time guard, and cell initializer also check against the regenerated module. Sweep allocation, buffer release, acceptance, complete timestep execution, spacing, and CFL proposal also pass. Complete run execution now composes initialization and advancement, retaining exact result words, ownership, capacity, reservation, and a supplied physical page bound. Complete output and solve-entry execution now pass. The public specification proves exact represented results and a 512 MiB bound from the module's initial state for runtime sizes two through eight hundred. Zero status implies a checked numerical trace through time 0.8. Complete decoding of the frozen 21,767-byte artifact and validation now pass with only the accepted logical axioms. Talos translation equality and both complete byte-facing behavior theorems also pass. The independent artifact gate passed. Both the 192-grid and 800-grid runs returned status zero at time 0.8. Their density/pressure figures and raw data are complete in the short article. Each run used the same binary in one local WASM solve call under the standard runner limits, with recorded monotonic runtimes of 49.6 seconds and 61.6 minutes, respectively.

The output packer's capacities, allocations, field operations, and copy loops now match shared checked programs. Arbitrary-stride allocation state and execution connect its one-word arrays to the existing heap model. Both density/pressure loops now terminate with exact output words and preserve the input grid through shared prefix, field, and BlockLoop results. Both allocator branches now compose target installation and loop execution, deriving owned output words while preserving the input grid and heap validity. One-word array release also checks. Both concatenations now compose allocation, destination installation, length storage, and copying with owned output and preserved input owners. The complete 95-instruction header region now computes its capacity, allocates, and writes the owned [status, time, n, n] array, preserving the caller's required locals. Both complete 52-instruction map regions now include input/length preparation, capacity computation, and result transfer, with preserved caller reads and typed scratch. Both complete 73-instruction concatenation regions now include input preparation, exact capacity, and result transfer. Their count assignments use the new shared scalar-assignment theorem recorded in LTG. Complete function-99 execution now composes these regions and all three releases, returns both ABI pointers to the specified Output.pack words, and preserves the physical page bound. Its allocation budget is at most 30,720,344 bytes for 640,000 cells.

The initializer's fuel/completion guard, array-length comparison, extraction input and allocation, return, and old-buffer release now have checked execution proofs against the current artifact. Both extraction branches now compose allocation, copying, and result assignment from an arbitrary frame satisfying the control and scratch-register invariants. Map and append preserve those invariants across their allocation regions. The complete growth loop now preserves those invariants, the initial-cell prefix, entry-held owners, and the remaining allocation budget, and terminates on completion or fuel exhaustion. Complete growCells execution now includes post-loop extraction and function entry/return, with exact source-result equality and ownership preservation. Complete initialCells execution now composes multiplication, initial-cell evaluation, singleton allocation and writes, growth, singleton release, and return. Its theorem covers every supported runtime size under the entry heap, free-list, reservation, and page-cap premises. The complete memory proof must bound WASM pages as well as heap allocation addresses. Map and append now accept arbitrary loop frames and return the required buffer getters. Allocation and grid writes have a checked arbitrary page-limit theorem. Initializer capacities, heap updates, entry-held owners, and source-prefix preservation have checked composition lemmas.

The shared allocator now covers arbitrary free-list reuse and memory growth for configurable local windows and element strides. Both retry failure sequences have exact execution proofs, including their empty array allocation. Held-grid ownership and the reduced allocation reservation also pass. The complete retry function now covers every return status without assuming source success. It establishes the branch premises, terminates the loop, and returns the specified status, timestep, and owned grid while preserving held grids and runtime limits. Its strengthened theorem now preserves a supplied physical page limit through both sweeps, accepted and rejected trials, invalid advancement, and retry exhaustion. The byte reservation must fit that page limit. The complete outer time-advance function also passes without assuming source success. It covers failed scans and failed retries, preserves the last accepted grid, and accounts for the empty failed-retry result. Its caller must establish the heap, reservation, and sufficient-fuel premises. Complete run execution now supplies the initialization and fuel premises. Its combined initializer and three-grid reservation is at most 319,523,176 bytes above the entry heap top. The strengthened outer-loop theorem preserves the supplied physical page bound.

Every initial cell now has checked density, energy, component, and energy-margin bounds. Shared packing, addition, subtraction, and multiplication lemmas cover the solver's larger arithmetic values, including multiplication underflow. Division and square-root bounds also pass. Their composition now proves finite thermodynamic intermediates and an internal-energy error bound, with Boolean guard acceptance under an explicit margin premise. Pressure, sound speed, and the final wave-speed addition now have checked positivity, range, and error bounds. Complete side and interface acceptance now follow from an explicit quantitative state predicate. Every initial cell satisfies that predicate with M = 8. The scalar conservative update has checked finiteness, acceptance, and timestep-dependent error bounds. Computed interface speeds now bound both exact velocities plus half their exact sound speeds. The accepted rounded CFL comparison now supplies exact reference-step positivity with density and internal energy at least 49/100 of their center values, for a positive ratio at most one. Physical-flux, interface, and conservative-update errors now compose across all four finite, status-zero candidate components. The candidate density and energy margin now have checked lower bounds using the exact center weight and the component error budget. Final guard acceptance follows under explicit quantitative and normalization conditions. Preservation of those conditions over the reachable grid and successful final-time completion remain open.

A checked three-cell example satisfies StateBounds 8 at every input and returns a successful candidate with density 15/128, below its 1/8 lower bound. The predicate is therefore not preserved for arbitrary neighboring states. Universal numerical success remains an open theorem under the revised proof requirement.

The initializer's map, append-copy, extract-copy, capacity, and complete no-fit allocation regions now have checked execution proofs. The complete loop maintains the heap and free-list invariant through doubling and its completed-prefix extraction branch. The allocation-to-heap adapter, root and length installation, map-ready frame, and remaining-allocation arithmetic also pass. The arithmetic reserves 212,002,896 bytes after the singleton, including retained map buffers. Loop execution preserves that reservation, and singleton construction accounts for its additional 112 bytes. The run entry must establish the complete initial budget. Map, append, and extraction now include pointer installation, the length store, and their complete data loops. The map composition returns the updated heap and ownership of both grids under the allocation premises. The complete emitted map region now includes its input and capacity prefixes and derives allocation size and no-fit search from the grid and free-list invariant. Its shared header-load and frame-preparation lemmas are indexed in LTG. The append allocation and copy composition now returns all three grid owners. The complete append region adds pointer setup, both header loads, and capacity calculation, deriving allocation premises from the size and free-list invariant. Its pointer and count prefixes use the checked scalar-statement descriptor indexed in LTG. Shared heap-grid bounds replace repeated payload-bound and separation derivations.

Complete the source and exact-WASM proofs for all success and failure returns, including the memory bounds.
Run 192 by 192 and then render its final density and pressure figure.
Run 800 by 800 and then render its final density and pressure figure.

13. Extend the Euler mathematical guarantees

The user authorized merging talosfp-euler into main, publishing it, and pursuing numerical conservation and rounding certificates, successful completion, and continuum convergence sequentially. The fast-forward and remote verification completed at d942e3cbd91a78cefa8be7e45617b05110bf955d. The user selected the net conservation-error certificate first. The detailed plan records the mathematical targets, research, source proofs, and remaining artifact gates.

Complete and run the proved numerical certificate.
Investigate and establish the supported successful-completion theorem.
Investigate and establish the justified continuum-convergence result.

14. Build verified tiny transformer inference

The detailed plan records the source definitions, proof boundaries, and execution work. Completion requires a command-line WASM demonstration and a checked source-equivalence theorem, including termination and memory guarantees. Further numerical-error proofs remain deferred. The user authorized exact-binary verification of pretrained GPT-2/128 after completing its source-equivalence proof.

Pretrained GPT-2/128 binary verification

Add FP32 instruction decoding, typing, translation, and soundness proofs.
Parameterize the complete session specification by its WASM module.
Prove decoding and validation of the 19,083-byte cached-step binary.
Prove equality with the execution model and transfer the complete session theorem.
Complete the focused GPT-2 artifact and source-proof checks.
Run cached inference and CLI completion tests.
Complete the aggregate artifact check after the shared verifier change.

The repository-wide source check still stops at the existing gcd cache mismatch. GPT-2's focused regeneration and proof checks pass.

FilesExpand file tree

plan.md

Latest commit

History