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.
Compiler Architecture Extraction, specialization, IR, ownership analysis, WASM emission, annotations, and compiler theorem boundaries.
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.
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
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 Deferred 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.
