leanEthereum · mzf11125 · Aug 14, 2026
diff --git a/Justfile b/Justfile
@@ -130,6 +130,11 @@ apitest server_url *args:
 interop *args:
     uv run --group test pytest tests/interop/ -v --no-cov --timeout=120 -x --tb=short --log-cli-level=INFO "$@"
 
+# Generate reference pages and navigation from spec docstrings
+[group('docs')]
+docs-generate:
+    uv run python tools/generate_docs.py
+
 # Build documentation site with mkdocs
 [group('docs')]
 docs *args:

diff --git a/docs/reference/crypto/index.md b/docs/reference/crypto/index.md
@@ -0,0 +1,3 @@
+# Cryptographic primitives used by the protocol specification.
+
+::: lean_spec.spec.crypto
diff --git a/docs/reference/crypto/koalabear.md b/docs/reference/crypto/koalabear.md
@@ -0,0 +1,3 @@
+# Core definition of the KoalaBear prime field Fp.
+
+::: lean_spec.spec.crypto.koalabear
diff --git a/docs/reference/crypto/merkleization.md b/docs/reference/crypto/merkleization.md
@@ -0,0 +1,3 @@
+# Merkleization primitives and hash-tree-root dispatch for SSZ.
+
+::: lean_spec.spec.crypto.merkleization
diff --git a/docs/reference/crypto/poseidon.md b/docs/reference/crypto/poseidon.md
@@ -0,0 +1,3 @@
+# Specification of the Poseidon permutation over the KoalaBear field.
+
+::: lean_spec.spec.crypto.poseidon
diff --git a/docs/reference/crypto/xmss/constants.md b/docs/reference/crypto/xmss/constants.md
@@ -0,0 +1,3 @@
+# Cryptographic constants and configuration presets for the XMSS spec.
+
+::: lean_spec.spec.crypto.xmss.constants
diff --git a/docs/reference/crypto/xmss/containers.md b/docs/reference/crypto/xmss/containers.md
@@ -0,0 +1,3 @@
+# Generalized XMSS containers.
+
+::: lean_spec.spec.crypto.xmss.containers
diff --git a/docs/reference/crypto/xmss/encoding.md b/docs/reference/crypto/xmss/encoding.md
@@ -0,0 +1,3 @@
+# Message-to-codeword pipeline for the Generalized XMSS scheme.
+
+::: lean_spec.spec.crypto.xmss.encoding
diff --git a/docs/reference/crypto/xmss/field.md b/docs/reference/crypto/xmss/field.md
@@ -0,0 +1,3 @@
+# Field-element decomposition and secure sampling for the Generalized XMSS scheme.
+
+::: lean_spec.spec.crypto.xmss.field
diff --git a/docs/reference/crypto/xmss/index.md b/docs/reference/crypto/xmss/index.md
@@ -0,0 +1,3 @@
+# Generalized XMSS hash-based signature scheme.
+
+::: lean_spec.spec.crypto.xmss
diff --git a/docs/reference/crypto/xmss/interface.md b/docs/reference/crypto/xmss/interface.md
@@ -0,0 +1,3 @@
+# Public interface for the Generalized XMSS signature scheme.
+
+::: lean_spec.spec.crypto.xmss.interface
diff --git a/docs/reference/crypto/xmss/merkle.md b/docs/reference/crypto/xmss/merkle.md
@@ -0,0 +1,3 @@
+# Sparse Merkle subtrees for the top-bottom traversal of an XMSS key.
+
+::: lean_spec.spec.crypto.xmss.merkle
diff --git a/docs/reference/crypto/xmss/poseidon.md b/docs/reference/crypto/xmss/poseidon.md
@@ -0,0 +1,3 @@
+# Poseidon hash engine in compression and sponge modes for the Generalized XMSS scheme.
+
+::: lean_spec.spec.crypto.xmss.poseidon
diff --git a/docs/reference/crypto/xmss/prf.md b/docs/reference/crypto/xmss/prf.md
@@ -0,0 +1,3 @@
+# SHAKE128-based pseudorandom function for deterministic key derivation.
+
+::: lean_spec.spec.crypto.xmss.prf
diff --git a/docs/reference/crypto/xmss/types.md b/docs/reference/crypto/xmss/types.md
@@ -0,0 +1,3 @@
+# Base types for the XMSS signature scheme.
+
+::: lean_spec.spec.crypto.xmss.types
diff --git a/docs/reference/forks/index.md b/docs/reference/forks/index.md
@@ -0,0 +1,3 @@
+# Multi-fork dispatch layer for leanSpec consensus specification.
+
+::: lean_spec.spec.forks
diff --git a/docs/reference/forks/lstar/aggregation.md b/docs/reference/forks/lstar/aggregation.md
@@ -0,0 +1,3 @@
+# Lstar fork — attestation aggregation.
+
+::: lean_spec.spec.forks.lstar.aggregation
diff --git a/docs/reference/forks/lstar/block_production.md b/docs/reference/forks/lstar/block_production.md
@@ -0,0 +1,3 @@
+# Lstar fork — proposer-side block building.
+
+::: lean_spec.spec.forks.lstar.block_production
diff --git a/docs/reference/forks/lstar/config.md b/docs/reference/forks/lstar/config.md
@@ -0,0 +1,3 @@
+# Chain and Consensus Configuration Specification
+
+::: lean_spec.spec.forks.lstar.config
diff --git a/docs/reference/forks/lstar/containers/aggregation.md b/docs/reference/forks/lstar/containers/aggregation.md
@@ -0,0 +1,3 @@
+# Post-quantum signature aggregation proofs wrapping the Rust prover.
+
+::: lean_spec.spec.forks.lstar.containers.aggregation
diff --git a/docs/reference/forks/lstar/containers/attestation.md b/docs/reference/forks/lstar/containers/attestation.md
@@ -0,0 +1,3 @@
+# Attestation vote envelopes: signed, aggregated, and their list form.
+
+::: lean_spec.spec.forks.lstar.containers.attestation
diff --git a/docs/reference/forks/lstar/containers/block.md b/docs/reference/forks/lstar/containers/block.md
@@ -0,0 +1,3 @@
+# Block container family carrying attestations and the merged block proof.
+
+::: lean_spec.spec.forks.lstar.containers.block
diff --git a/docs/reference/forks/lstar/containers/checkpoint.md b/docs/reference/forks/lstar/containers/checkpoint.md
@@ -0,0 +1,3 @@
+# Casper-FFG checkpoints and the attestation vote they anchor.
+
+::: lean_spec.spec.forks.lstar.containers.checkpoint
diff --git a/docs/reference/forks/lstar/containers/genesis.md b/docs/reference/forks/lstar/containers/genesis.md
@@ -0,0 +1,3 @@
+# Chain configuration committed into the consensus state.
+
+::: lean_spec.spec.forks.lstar.containers.genesis
diff --git a/docs/reference/forks/lstar/containers/identifiers.md b/docs/reference/forks/lstar/containers/identifiers.md
@@ -0,0 +1,3 @@
+# Scalar identifiers naming validators, subnets, and the registry index space.
+
+::: lean_spec.spec.forks.lstar.containers.identifiers
diff --git a/docs/reference/forks/lstar/containers/index.md b/docs/reference/forks/lstar/containers/index.md
@@ -0,0 +1,3 @@
+# Container types for the Lean consensus specification.
+
+::: lean_spec.spec.forks.lstar.containers
diff --git a/docs/reference/forks/lstar/containers/interval.md b/docs/reference/forks/lstar/containers/interval.md
@@ -0,0 +1,3 @@
+# Interval time unit for the Lean consensus specification.
+
+::: lean_spec.spec.forks.lstar.containers.interval
diff --git a/docs/reference/forks/lstar/containers/participation.md b/docs/reference/forks/lstar/containers/participation.md
@@ -0,0 +1,3 @@
+# Validator participation bitfields over the registry index space.
+
+::: lean_spec.spec.forks.lstar.containers.participation
diff --git a/docs/reference/forks/lstar/containers/state.md b/docs/reference/forks/lstar/containers/state.md
@@ -0,0 +1,3 @@
+# Consensus state and the justification/finalization accounting it tracks.
+
+::: lean_spec.spec.forks.lstar.containers.state
diff --git a/docs/reference/forks/lstar/containers/store.md b/docs/reference/forks/lstar/containers/store.md
@@ -0,0 +1,3 @@
+# Fork-choice store: the node's local view of the chain.
+
+::: lean_spec.spec.forks.lstar.containers.store
diff --git a/docs/reference/forks/lstar/containers/validator.md b/docs/reference/forks/lstar/containers/validator.md
@@ -0,0 +1,3 @@
+# The validator registry tracked in the consensus state.
+
+::: lean_spec.spec.forks.lstar.containers.validator
diff --git a/docs/reference/forks/lstar/errors.md b/docs/reference/forks/lstar/errors.md
@@ -0,0 +1,3 @@
+# Rejection reasons and the typed error that carries them.
+
+::: lean_spec.spec.forks.lstar.errors
diff --git a/docs/reference/forks/lstar/fork_choice.md b/docs/reference/forks/lstar/fork_choice.md
@@ -0,0 +1,3 @@
+# Lstar fork — fork choice: store, LMD-GHOST, attestation handling.
+
+::: lean_spec.spec.forks.lstar.fork_choice
diff --git a/docs/reference/forks/lstar/index.md b/docs/reference/forks/lstar/index.md
@@ -0,0 +1,3 @@
+# Lstar fork
+
+::: lean_spec.spec.forks.lstar
diff --git a/docs/reference/forks/lstar/signatures.md b/docs/reference/forks/lstar/signatures.md
@@ -0,0 +1,3 @@
+# Lstar fork — block signature verification.
+
+::: lean_spec.spec.forks.lstar.signatures
diff --git a/docs/reference/forks/lstar/slot.md b/docs/reference/forks/lstar/slot.md
@@ -0,0 +1,3 @@
+# Slot primitive shared by the consensus and crypto layers.
+
+::: lean_spec.spec.forks.lstar.slot
diff --git a/docs/reference/forks/lstar/spec.md b/docs/reference/forks/lstar/spec.md
@@ -0,0 +1,3 @@
+# Lstar fork — identity and construction facade.
+
+::: lean_spec.spec.forks.lstar.spec
diff --git a/docs/reference/forks/lstar/state_transition.md b/docs/reference/forks/lstar/state_transition.md
@@ -0,0 +1,3 @@
+# Lstar fork — state transition.
+
+::: lean_spec.spec.forks.lstar.state_transition
diff --git a/docs/reference/forks/lstar/timeline.md b/docs/reference/forks/lstar/timeline.md
@@ -0,0 +1,3 @@
+# Lstar fork — interval ticking and time progression.
+
+::: lean_spec.spec.forks.lstar.timeline
diff --git a/docs/reference/forks/lstar/validator_duties.md b/docs/reference/forks/lstar/validator_duties.md
@@ -0,0 +1,3 @@
+# Lstar fork — validator duties: proposal head and production.
+
+::: lean_spec.spec.forks.lstar.validator_duties
diff --git a/docs/reference/forks/protocol.md b/docs/reference/forks/protocol.md
@@ -0,0 +1,3 @@
+# Fork protocol interface for leanSpec consensus.
+
+::: lean_spec.spec.forks.protocol
diff --git a/docs/reference/forks/registry.md b/docs/reference/forks/registry.md
@@ -0,0 +1,3 @@
+# Registry of registered forks, ordered oldest to newest.
+
+::: lean_spec.spec.forks.registry
diff --git a/docs/reference/index.md b/docs/reference/index.md
@@ -0,0 +1,3 @@
+# Protocol specification: per-fork consensus rules and registry.
+
+::: lean_spec.spec
diff --git a/docs/reference/observability/index.md b/docs/reference/observability/index.md
@@ -0,0 +1,3 @@
+# Vendor-neutral observability for the Lean specification.
+
+::: lean_spec.spec.observability
diff --git a/docs/reference/observability/observer.md b/docs/reference/observability/observer.md
@@ -0,0 +1,3 @@
+# Telemetry observer protocol and its process-wide singleton.
+
+::: lean_spec.spec.observability.observer
diff --git a/docs/reference/ssz/bitfields.md b/docs/reference/ssz/bitfields.md
@@ -0,0 +1,3 @@
+# SSZ bitfield types.
+
+::: lean_spec.spec.ssz.bitfields
diff --git a/docs/reference/ssz/boolean.md b/docs/reference/ssz/boolean.md
@@ -0,0 +1,3 @@
+# SSZ boolean type — true or false serialized as a single byte.
+
+::: lean_spec.spec.ssz.boolean
diff --git a/docs/reference/ssz/byte_arrays.md b/docs/reference/ssz/byte_arrays.md
@@ -0,0 +1,3 @@
+# SSZ byte array types.
+
+::: lean_spec.spec.ssz.byte_arrays
diff --git a/docs/reference/ssz/collections.md b/docs/reference/ssz/collections.md
@@ -0,0 +1,3 @@
+# SSZ vector and list collections.
+
+::: lean_spec.spec.ssz.collections
diff --git a/docs/reference/ssz/container.md b/docs/reference/ssz/container.md
@@ -0,0 +1,3 @@
+# SSZ Container Type.
+
+::: lean_spec.spec.ssz.container
diff --git a/docs/reference/ssz/exceptions.md b/docs/reference/ssz/exceptions.md
@@ -0,0 +1,3 @@
+# Exception hierarchy for the SSZ type system.
+
+::: lean_spec.spec.ssz.exceptions
diff --git a/docs/reference/ssz/index.md b/docs/reference/ssz/index.md
@@ -0,0 +1,3 @@
+# SSZ primitive types and (de)serialization for the Lean Ethereum specification.
+
+::: lean_spec.spec.ssz
diff --git a/docs/reference/ssz/ssz_base.md b/docs/reference/ssz/ssz_base.md
@@ -0,0 +1,3 @@
+# Abstract bases for the SSZ type system.
+
+::: lean_spec.spec.ssz.ssz_base
diff --git a/docs/reference/ssz/uint.md b/docs/reference/ssz/uint.md
@@ -0,0 +1,3 @@
+# Unsigned Integer Type Specification.
+
+::: lean_spec.spec.ssz.uint
diff --git a/mkdocs.yml b/mkdocs.yml
@@ -44,7 +44,7 @@ plugins:
             members_order: source
             separate_signature: true
             filters: ["!^_"]
-            docstring_section_style: google
+            docstring_style: google
 
 markdown_extensions:
   - admonition
@@ -59,7 +59,67 @@ markdown_extensions:
 
 nav:
   - Home: index.md
-
+  - Reference:
+    - Overview: reference/index.md
+    - crypto:
+        - Overview: reference/crypto/index.md
+        - koalabear: reference/crypto/koalabear.md
+        - merkleization: reference/crypto/merkleization.md
+        - poseidon: reference/crypto/poseidon.md
+        - xmss:
+            - Overview: reference/crypto/xmss/index.md
+            - constants: reference/crypto/xmss/constants.md
+            - containers: reference/crypto/xmss/containers.md
+            - encoding: reference/crypto/xmss/encoding.md
+            - field: reference/crypto/xmss/field.md
+            - interface: reference/crypto/xmss/interface.md
+            - merkle: reference/crypto/xmss/merkle.md
+            - poseidon: reference/crypto/xmss/poseidon.md
+            - prf: reference/crypto/xmss/prf.md
+            - types: reference/crypto/xmss/types.md
+    - forks:
+        - Overview: reference/forks/index.md
+        - lstar:
+            - Overview: reference/forks/lstar/index.md
+            - aggregation: reference/forks/lstar/aggregation.md
+            - block_production: reference/forks/lstar/block_production.md
+            - config: reference/forks/lstar/config.md
+            - containers:
+                - Overview: reference/forks/lstar/containers/index.md
+                - aggregation: reference/forks/lstar/containers/aggregation.md
+                - attestation: reference/forks/lstar/containers/attestation.md
+                - block: reference/forks/lstar/containers/block.md
+                - checkpoint: reference/forks/lstar/containers/checkpoint.md
+                - genesis: reference/forks/lstar/containers/genesis.md
+                - identifiers: reference/forks/lstar/containers/identifiers.md
+                - interval: reference/forks/lstar/containers/interval.md
+                - participation: reference/forks/lstar/containers/participation.md
+                - state: reference/forks/lstar/containers/state.md
+                - store: reference/forks/lstar/containers/store.md
+                - validator: reference/forks/lstar/containers/validator.md
+            - errors: reference/forks/lstar/errors.md
+            - fork_choice: reference/forks/lstar/fork_choice.md
+            - signatures: reference/forks/lstar/signatures.md
+            - slot: reference/forks/lstar/slot.md
+            - spec: reference/forks/lstar/spec.md
+            - state_transition: reference/forks/lstar/state_transition.md
+            - timeline: reference/forks/lstar/timeline.md
+            - validator_duties: reference/forks/lstar/validator_duties.md
+        - protocol: reference/forks/protocol.md
+        - registry: reference/forks/registry.md
+    - observability:
+        - Overview: reference/observability/index.md
+        - observer: reference/observability/observer.md
+    - ssz:
+        - Overview: reference/ssz/index.md
+        - bitfields: reference/ssz/bitfields.md
+        - boolean: reference/ssz/boolean.md
+        - byte_arrays: reference/ssz/byte_arrays.md
+        - collections: reference/ssz/collections.md
+        - container: reference/ssz/container.md
+        - exceptions: reference/ssz/exceptions.md
+        - ssz_base: reference/ssz/ssz_base.md
+        - uint: reference/ssz/uint.md
 extra:
   social:
     - icon: fontawesome/brands/github
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Cryptographic primitives used by the protocol specification.

		::: lean_spec.spec.crypto
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Core definition of the KoalaBear prime field Fp.

		::: lean_spec.spec.crypto.koalabear
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Merkleization primitives and hash-tree-root dispatch for SSZ.

		::: lean_spec.spec.crypto.merkleization
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Specification of the Poseidon permutation over the KoalaBear field.

		::: lean_spec.spec.crypto.poseidon
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Cryptographic constants and configuration presets for the XMSS spec.

		::: lean_spec.spec.crypto.xmss.constants
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Generalized XMSS containers.

		::: lean_spec.spec.crypto.xmss.containers
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Message-to-codeword pipeline for the Generalized XMSS scheme.

		::: lean_spec.spec.crypto.xmss.encoding
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Field-element decomposition and secure sampling for the Generalized XMSS scheme.

		::: lean_spec.spec.crypto.xmss.field
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Generalized XMSS hash-based signature scheme.

		::: lean_spec.spec.crypto.xmss
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Public interface for the Generalized XMSS signature scheme.

		::: lean_spec.spec.crypto.xmss.interface