LeanExe assigns one subject to each maintained document. The repository README introduces the system, Developing LeanExe owns setup and tests, and the root Development Plan owns unfinished work. The development journal records rationale and test evidence without serving as current guidance.
Document
Authority
LeanExe User Manual Source patterns, examples, diagnostics, and authoring guidance.
Language Specification Accepted Lean subset, numeric semantics, ABI, memory representation, ownership rules, and rejection boundaries.
LeanExe Type Theory Relationship among Lean's source theory, the executable fragment, runtime values, and artifact propositions.
Type Theory of the LeanExe Fragment Mathematical typing, representation, specialization, and ownership judgments, with implementation-defined recognition premises.
Formal Specification of Compilation and Execution Compilation and execution relations, numeric and collection operations, heap representation, ABI, WASI, and open proof obligations.
Compiler Architecture Extraction, specialization, IR, ownership analysis, WASM emission, annotations, and compiler theorem boundaries.
Self-Hosted WebAssembly Emitter Canonical final-module image, host ABI, precise self-hosting claim, compatibility rules, and bootstrap receipt.
Architecture Diagram High-level source, compilation, annotation, LTG, execution, and proof flow.
JSON Tree WASI Example Source, compilation, command execution, and verification for a typed tree-processing program.
Pseudorandom Number Generator Lean SplitMix64 example, seed/count/modulus CLI, and execution tests.
Artifact verification and proving
Document
Authority
Artifact Verification Format Restricted binary profile, exact-byte packages, decoding, validation, theorem boundary, and release evidence.
Verifying a Program Procedure for creating, registering, proving, and independently checking an artifact package.
Artifact Proving Relationship among Talos, ProofKit, compiler annotations, LTG retrieval, generated proof work, and independent checking.
leanexegen ReferenceCLI stages, task isolation, fixed public interface, proof packages, verification, and reproving.
WebAssembly Annotations Implemented sidecar schema, recognized regions, generated checked declarations, and recipe selection.
Knowledge Forest and Structured LTG Package and catalog schemas, forest selection, filtering, checked declarations, learning phases, exclusions, and task snapshots.
LTG Metrics Reproducible measurements of catalog structure, declarations, tactics, coverage, and content size.
Artifact-Proof Strategies General proof-construction and diagnosis guidance that applies across artifact families.
Talos Imported-Memory Defect Reproduction, semantic cause, conformance warning, artifact-profile effect, and upstream repair boundary.
Document
Authority
GPT Inference and Verification Model families, goals, checkpoint-to-output data flow, source and proof directories, and current verification scope.
Development Status Current checked capabilities, known limitations, and release state.
LTG and CLOB Retrospective Measured LTG results, structured-retrieval limits, CLOB findings, and the relationship between them.
Development Plan Ordered active work and completion conditions.
Detailed Plans Technical plans for unfinished work referenced by the root roadmap.
Proof-Grade f64 Artifact Semantics Active plan for exact binary64 artifact execution, finite-result safety, numerical refinement, and checked certificates.
Talos Proof Inventory Registered source-driven and exact-artifact theorem inventory.
Demonstrations Twelve end-to-end programs and their retained proof packages.
Benchmark Evidence Proof-generation runs, journals, telemetry, and acceptance results.
Research Papers Publication sources, PDFs, and marXiv records.
Proof journals, benchmark runs, devnotes.md, and published papers preserve evidence or research records. They may contain observations tied to an older artifact, proof interface, or tool version. Current behavior comes from the references above and the checked implementation.
