diff --git a/.claude/skills/hive/SKILL.md b/.claude/skills/hive/SKILL.md index 5ac9a07..fc78bcd 100644 --- a/.claude/skills/hive/SKILL.md +++ b/.claude/skills/hive/SKILL.md @@ -16,7 +16,7 @@ description: | Negative triggers: Do NOT activate for spinning up a local devnet to RUN it rather than test it (use the leanQuickstart skill). Do NOT activate for consensus container shapes / fork choice / state transition (use the leanSpec skill). Do NOT activate for aggregation - / zkVM / proof internals (use the leanMultisig skill). Do NOT activate for the metric + / zkVM / proof internals (use the leanVM skill). Do NOT activate for the metric contract — names/types/buckets/labels — (use the leanMetrics skill). Do NOT activate for pure docs-site (mdBook) work. Do NOT activate when working outside the Verity project. --- @@ -150,7 +150,7 @@ Paths are relative to the hive repo root, read at `master`. ## 7. Relationship to the other skills & Verity - **leanQuickstart** (separate skill) = spin up and **run** a local lean devnet. -- **leanSpec** / **leanMultisig** / **leanMetrics** (separate skills) = protocol & +- **leanSpec** / **leanVM** / **leanMetrics** (separate skills) = protocol & container shapes / aggregation & zkVM / the metric contract. - **hive** (this skill) = the **test harness** that exercises clients (build + `--sim` + `--client`), especially the `lean` simulator. diff --git a/.claude/skills/leanMetrics/SKILL.md b/.claude/skills/leanMetrics/SKILL.md index 55b141f..688d91a 100644 --- a/.claude/skills/leanMetrics/SKILL.md +++ b/.claude/skills/leanMetrics/SKILL.md @@ -14,7 +14,7 @@ description: | any work exposing or monitoring consensus-client metrics in Verity. Negative triggers: Do NOT activate for consensus container shapes / fork choice / state transition behavior (use the leanSpec skill). Do NOT activate for aggregation / - zkVM / proof internals (use the leanMultisig skill). Do NOT activate for pure docs-site + zkVM / proof internals (use the leanVM skill). Do NOT activate for pure docs-site (mdBook) work. Do NOT activate when working outside the Verity project. --- @@ -126,10 +126,10 @@ authoritative for the contract. 3. For coverage/status questions, read the per-client status column (✅/📝/□). 4. In your output, cite the **`metrics.md` section + the `main` commit SHA** you checked. -## 5. Relationship to leanSpec & leanMultisig & Verity +## 5. Relationship to leanSpec & leanVM & Verity - **leanSpec** (separate skill) = consensus protocol & container shapes (Python). -- **leanMultisig** (separate skill) = aggregation + zkVM (Rust). +- **leanVM** (separate skill) = aggregation + zkVM (Rust). - **leanMetrics** (this skill) = the observability **metric contract** (Prometheus names/types/buckets/labels) + Grafana dashboards. - Verity's `verity-metrics` crate implements leanMetrics; **ethlambda** and **Ream** are diff --git a/.claude/skills/leanQuickstart/SKILL.md b/.claude/skills/leanQuickstart/SKILL.md index e4cede6..abe320a 100644 --- a/.claude/skills/leanQuickstart/SKILL.md +++ b/.claude/skills/leanQuickstart/SKILL.md @@ -14,7 +14,7 @@ description: | and any work spinning up or running a local lean multi-client devnet for Verity. Negative triggers: Do NOT activate for consensus container shapes / fork choice / state transition (use the leanSpec skill). Do NOT activate for aggregation / zkVM / - proof internals (use the leanMultisig skill). Do NOT activate for the metric + proof internals (use the leanVM skill). Do NOT activate for the metric contract — names/types/buckets/labels — (use the leanMetrics skill); this skill only covers RUNNING the bundled Prometheus/Grafana stack. Do NOT activate for pure docs-site (mdBook) work. Do NOT activate when working outside the Verity project. @@ -114,10 +114,10 @@ Paths are relative to the lean-quickstart repo root, read at `main`. `metrics/docker-compose-metrics.yaml` if you want the Prometheus/Grafana stack. 4. In your output, cite the **file/script + the `main` commit SHA** you checked. -## 5. Relationship to leanSpec, leanMultisig, leanMetrics & Verity +## 5. Relationship to leanSpec, leanVM, leanMetrics & Verity - **leanSpec** (separate skill) = consensus protocol & container shapes (the chain rules). -- **leanMultisig** (separate skill) = aggregation + zkVM proof internals. +- **leanVM** (separate skill) = aggregation + zkVM proof internals. - **leanMetrics** (separate skill) = the observability **metric contract** (names/types/ buckets/labels). This skill only covers **running** the bundled Prometheus/Grafana stack, not what the metrics are. diff --git a/.claude/skills/leanSpec/SKILL.md b/.claude/skills/leanSpec/SKILL.md index 132ae12..6a42de5 100644 --- a/.claude/skills/leanSpec/SKILL.md +++ b/.claude/skills/leanSpec/SKILL.md @@ -8,7 +8,7 @@ description: | test vectors. Maps a topic to the authoritative leanSpec path for any protocol element. Triggers: "leanSpec", "leanSpecを確認", "仕様を確認", "Verityの仕様", "prime", "verity context", "where is the spec for", "container shape", "コンテナの形", "3SF", "fork choice", - "state transition", "XMSS", "leanMultisig", "devnet spec", and starting any Verity + "state transition", "XMSS", "leanVM", "devnet spec", and starting any Verity implementation or review work. Negative triggers: Do NOT activate for pure docs-site work (mdBook page authoring or build/serve). Do NOT activate when working outside the Verity project. @@ -84,7 +84,7 @@ Paths are relative to the leanSpec repo root, read at `origin/main`. | Genesis / validator / chain config | `src/lean_spec/subspecs/{genesis,validator,chain}/`, `forks/lstar/containers/config.py` | | API | `src/lean_spec/subspecs/api/` | | Conformance test vectors | `tests/consensus/devnet/{state_transition,fc,ssz,networking,sync,verify_signatures}/` | -| leanMultisig (aggregation / zkVM) | **not** in leanSpec — use the dedicated `leanMultisig` skill (`github.com/leanEthereum/leanMultisig`) | +| leanVM (aggregation / zkVM) | **not** in leanSpec — use the dedicated `leanVM` skill (`github.com/leanEthereum/leanVM`) | | ethlambda (Rust *design* reference, not spec) | external `github.com/lambdaclass/ethlambda` | ## 4. How to use (implementing / reviewing / answering) diff --git a/.claude/skills/leanMultisig/SKILL.md b/.claude/skills/leanVM/SKILL.md similarity index 63% rename from .claude/skills/leanMultisig/SKILL.md rename to .claude/skills/leanVM/SKILL.md index 8a45e27..63c811e 100644 --- a/.claude/skills/leanMultisig/SKILL.md +++ b/.claude/skills/leanVM/SKILL.md @@ -1,13 +1,14 @@ --- -name: leanMultisig +name: leanVM description: | Ground every question about post-quantum signature aggregation and the zkVM in - leanMultisig — the authoritative spec and Rust reference implementation - (github.com/leanEthereum/leanMultisig), always read from the latest remote main. + leanVM — the authoritative spec and Rust reference implementation + (github.com/leanEthereum/leanVM), always read from the latest remote main. Verity's verity-crypto crate depends on it directly. Use before implementing, reviewing, or answering anything about XMSS aggregation, Type-1/Type-2 proofs, the prover/verifier, the zkVM, the zkDSL, or WHIR. - Triggers: "leanMultisig", "lean_multisig", "leanMultisigを確認", "署名集約", "aggregation", + Triggers: "leanVM", "lean_vm", "leanVMを確認", "leanMultisig", "lean_multisig" (the + repo's former name — old references still mean this skill), "署名集約", "aggregation", "Type-1 proof", "Type-2 proof", "zkVM", "zkDSL", "WHIR", "prover", "verifier", "verity-crypto", and any work touching signature aggregation or proof generation in Verity. Negative triggers: Do NOT activate for consensus container shapes / fork choice / state @@ -15,9 +16,13 @@ description: | activate when working outside the Verity project. --- -# leanMultisig — source of truth for aggregation & the zkVM +# leanVM — source of truth for aggregation & the zkVM -leanMultisig (`github.com/leanEthereum/leanMultisig`) is a minimal zkVM targeting +> Renamed upstream from **leanMultisig** to **leanVM** (2026-08-14; the old GitHub URL +> redirects). Older Verity docs, memories, and upstream discussions may still use the old +> name — they refer to this same repository. + +leanVM (`github.com/leanEthereum/leanVM`) is a minimal zkVM targeting aggregation of hash-based (Generalized-XMSS) signatures. It is the **authoritative spec and Rust reference implementation** for everything aggregation/zkVM-related in Verity. Verity's `verity-crypto` crate depends on it directly (as a pinned git dependency). @@ -25,38 +30,38 @@ Verity's `verity-crypto` crate depends on it directly (as a pinned git dependenc ## 0. Core principle - The behavior of signature aggregation, Type-1/Type-2 proofs, the prover/verifier, the - zkVM and its zkDSL is defined by **leanMultisig** (its Rust crates + design docs). When + zkVM and its zkDSL is defined by **leanVM** (its Rust crates + design docs). When in doubt, read the source. - Division of authority with the leanSpec skill: **leanSpec** defines the *consensus containers* that carry proofs (`TypeOneMultiSignature`, `SignedBlock.proof` = - `ByteList512KiB`, the verify entry points). **leanMultisig** defines how those proofs + `ByteList512KiB`, the verify entry points). **leanVM** defines how those proofs are *produced and verified*. For container shapes → leanSpec; for proof internals → here. -## 1. Always read leanMultisig from the remote `main` (no local path assumptions) +## 1. Always read leanVM from the remote `main` (no local path assumptions) -leanMultisig moves fast. Read the latest `main` of the canonical upstream directly from +leanVM moves fast. Read the latest `main` of the canonical upstream directly from the remote — this works for every developer and in CI, with no dependency on anyone's local clone path. -Repo: `github.com/leanEthereum/leanMultisig` (canonical; do **not** use a personal fork). +Repo: `github.com/leanEthereum/leanVM` (canonical; do **not** use a personal fork). ```bash # Latest main commit — cite this SHA in your output: -gh api repos/leanEthereum/leanMultisig/commits/main --jq '.sha' +gh api repos/leanEthereum/leanVM/commits/main --jq '.sha' # Read a file at main: -gh api "repos/leanEthereum/leanMultisig/contents/crates/xmss/xmss.md?ref=main" --jq '.content' | base64 -d +gh api "repos/leanEthereum/leanVM/contents/crates/xmss/xmss.md?ref=main" --jq '.content' | base64 -d # raw fallback (no gh): -curl -s https://raw.githubusercontent.com/leanEthereum/leanMultisig/main/crates/xmss/xmss.md +curl -s https://raw.githubusercontent.com/leanEthereum/leanVM/main/crates/xmss/xmss.md # List a directory at main: -gh api "repos/leanEthereum/leanMultisig/contents/crates?ref=main" --jq '.[].name' +gh api "repos/leanEthereum/leanVM/contents/crates?ref=main" --jq '.[].name' # Full tree: -gh api "repos/leanEthereum/leanMultisig/git/trees/main?recursive=1" --jq '.tree[].path' +gh api "repos/leanEthereum/leanVM/git/trees/main?recursive=1" --jq '.tree[].path' ``` -No `gh`/`curl`? Use WebFetch on `https://github.com/leanEthereum/leanMultisig/blob/main/`. +No `gh`/`curl`? Use WebFetch on `https://github.com/leanEthereum/leanVM/blob/main/`. If you happen to have a local clone, you *may* use it for fast navigation/grep — but `git fetch origin` first and read `origin/main` (clones drift onto feature branches and @@ -64,7 +69,7 @@ forks). Never assume a specific clone path. ## 2. How Verity consumes it -- `verity-crypto` depends on leanMultisig as a **pinned git dependency** in `Cargo.toml`. +- `verity-crypto` depends on leanVM as a **pinned git dependency** in `Cargo.toml`. The pinned commit is what Verity builds against; the latest `main` is the source of truth for understanding/spec questions. When bumping the pin, re-read `main`. - The proving stack is expensive; the prover context is set up once at startup. Verity @@ -72,9 +77,9 @@ forks). Never assume a specific clone path. ## 3. Topic → authoritative location map -Paths are relative to the leanMultisig repo root, read at `main`. +Paths are relative to the leanVM repo root, read at `main`. -| Topic | leanMultisig (authoritative) | +| Topic | leanVM (authoritative) | |---|---| | XMSS signature scheme | `crates/xmss/` (+ `crates/xmss/xmss.md`) | | Aggregation: Type-1 / Type-2 proofs | `crates/rec_aggregation/` (+ `crates/rec_aggregation/TYPE1_TYPE2_LAYOUT.md`) | @@ -90,14 +95,14 @@ Paths are relative to the leanMultisig repo root, read at `main`. ## 4. How to use (implementing / reviewing / answering) -1. Read the **authoritative leanMultisig path at `main`** for the topic first. +1. Read the **authoritative leanVM path at `main`** for the topic first. 2. For the consensus containers carrying proofs, defer to the **leanSpec** skill. -3. In your output, cite the **leanMultisig path + the `main` commit SHA** you checked. +3. In your output, cite the **leanVM path + the `main` commit SHA** you checked. ## 5. Relationship to leanSpec & Verity - **leanSpec** (separate skill) = consensus protocol spec & container shapes (Python). -- **leanMultisig** (this skill) = aggregation + zkVM (Rust); produces/verifies the proofs +- **leanVM** (this skill) = aggregation + zkVM (Rust); produces/verifies the proofs that fill leanSpec's containers. - Verity (Rust) wires both together: `verity-types` (leanSpec shapes) + - `verity-crypto` (leanMultisig + Generalized-XMSS). The client is pre-implementation today. + `verity-crypto` (leanVM + Generalized-XMSS). The client is pre-implementation today. diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index 30e0d9e..4875a41 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -70,7 +70,7 @@ flowchart TB subgraph B["Runtime Shell — Rust, panic-free"] direction LR CODEC["SSZ codec + hash_tree_root
wire bytes ↔ typed values"] - CRYPTO["Signature verification
verity-crypto: XMSS · leanMultisig"] + CRYPTO["Signature verification
verity-crypto: XMSS · leanVM"] STORE["State + fork-choice store
single writer · threads immutable values"] DB["Database
blocks · states · anchor"] FFI["FFI bindings layer"] @@ -167,8 +167,9 @@ upstream Lean library name per Rust's `-sys` convention. - `verity-p2p` — gossip and req/resp over libp2p. - `verity-crypto` — adapter over the two upstream signature libraries: [`leansig`](https://github.com/leanEthereum/leanSig) - for per-validator XMSS sign / verify, and [`leanMultisig`](https://github.com/leanEthereum/leanMultisig) - for aggregation and aggregate-proof verification. One capability contract, two suppliers behind it. + for per-validator XMSS sign / verify, and [`leanVM`](https://github.com/leanEthereum/leanVM) + (formerly leanMultisig) for aggregation and aggregate-proof verification. One capability + contract, two suppliers behind it. - `verity-db` — persistence (Repository): blocks, states, aggregate proofs, and the finalized anchor. Keeps the storage concern out of the single-writer aggregate coordinator. See [Storage engine and retention](#storage-engine-and-retention). diff --git a/CLAUDE.md b/CLAUDE.md index 1067b6c..9f4ccea 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -18,7 +18,7 @@ Owner-ratified ground rules for the first Rust code. Do not re-open these withou - **Goal**: a full node from the start (networking included), not a fixtures-passing library. leanSpec fixture conformance is still the CI backbone. - **Crates**: start with a single `verity-consensus` crate (no chain/validator split). Proposer selection lives chain-side as a pure function next to STF/fork choice. Shared types stay a module until a second crate exists. - **Dependencies**: - - XMSS: [`leansig`](https://github.com/leanEthereum/leanSig) as a git dependency, **rev-pinned** (not branch-tracked), for per-validator sign / verify. Aggregation and aggregate-proof verification come from [`leanMultisig`](https://github.com/leanEthereum/leanMultisig) — both sit behind `verity-crypto`'s one capability contract, so a doc naming only one of them is incomplete, not contradictory. + - XMSS: [`leansig`](https://github.com/leanEthereum/leanSig) as a git dependency, **rev-pinned** (not branch-tracked), for per-validator sign / verify. Aggregation and aggregate-proof verification come from [`leanVM`](https://github.com/leanEthereum/leanVM) (renamed upstream from `leanMultisig` on 2026-08-14; the old URL redirects) — both sit behind `verity-crypto`'s one capability contract, so a doc naming only one of them is incomplete, not contradictory. - SSZ: `libssz` 0.2.2 (lambdaclass). [NyxFoundation/leanSSZ](https://github.com/NyxFoundation/leanSSZ) (proven Lean SSZ, C ABI PoC complete) is deliberately NOT adopted initially — it is the future Lean-adoption candidate for SSZ. - Networking: upstream `rust-libp2p` (QUIC, gossipsub, reqresp). Fork only if a concrete need materializes, as lambdaclass did for ethlambda. - Storage: **RocksDB** behind a backend trait with an in-memory sibling implementation (ethlambda's `StorageBackend` split). Decided 2026-08-10 — see **Storage** below. diff --git a/DOMAIN_MODEL.md b/DOMAIN_MODEL.md index c477a09..213302d 100644 --- a/DOMAIN_MODEL.md +++ b/DOMAIN_MODEL.md @@ -34,7 +34,7 @@ below; this section is the *strategic* frame above it. |---|---|---|---|---| | **State Transition** | Consensus-critical | `State` aggregate + `SignedBlock` processing; justification / finalization invariants | Verified Core (pure fns) | Verity Consensus (separate Lean repo) | | **Fork Choice** | Consensus-critical | `Store` aggregate, LMD GHOST, head / safe_target, payload `new → known` | Verified Core pure decision fns **+** Runtime Shell single-writer store | Verity Consensus + `verity-chain` | -| **Signature & Aggregation** | Supporting | signatures, Type-1 / Type-2 proofs, verify / aggregate | Runtime Shell | `verity-crypto` (ACL → leanSig, leanMultisig) | +| **Signature & Aggregation** | Supporting | signatures, Type-1 / Type-2 proofs, verify / aggregate | Runtime Shell | `verity-crypto` (ACL → leanSig, leanVM) | | **Serialization** | Supporting | SSZ encode / decode, `hash_tree_root`, merkleization | Runtime Shell | `verity-types` (+ external SSZ lib) | | **Validator Duties** | Supporting | proposer / attester duties, production, signing, aggregation scheduling | I/O Edge | `verity-validator` | | **Networking** | Generic | gossip topics, req / resp, peers | I/O Edge | `verity-p2p` | @@ -62,7 +62,7 @@ pattern names *how* each relationship is governed. |---|---|---| | **leanSpec** | State Transition / Fork Choice | **Conformist** on container shapes; **Partnership** on correctness (proofs find spec bugs; fixes flow back upstream) | | **leanSig** | Signature & Aggregation | **ACL / Anti-Corruption Layer** (adapter) — per-validator XMSS sign / verify | -| **leanMultisig** | Signature & Aggregation | **ACL / Anti-Corruption Layer** (adapter) — aggregation and aggregate-proof verification | +| **leanVM** | Signature & Aggregation | **ACL / Anti-Corruption Layer** (adapter) — aggregation and aggregate-proof verification | | **leanMetrics** | Telemetry | **Conformist** (exact metric contract) | | **external SSZ library** | Serialization | **ACL / adapter** | @@ -86,7 +86,7 @@ flowchart LR subgraph ext["External upstream contexts"] SPEC["leanSpec"] SIGLIB["leanSig"] - MULTI["leanMultisig"] + MULTI["leanVM"] METR["leanMetrics"] SSZ["SSZ library"] end diff --git a/README.md b/README.md index a3ba32f..eeb8ba7 100644 --- a/README.md +++ b/README.md @@ -22,7 +22,7 @@ Verity makes a different bet — that the implementation should be *proven* to m ## References - https://github.com/leanEthereum/leanSpec -- https://github.com/leanEthereum/leanMultisig +- https://github.com/leanEthereum/leanVM - https://github.com/leanEthereum/leanMetrics - https://hive.leanroadmap.org/ - https://observatory.leanroadmap.org/ diff --git a/_typos.toml b/_typos.toml index 8240dfe..6acf992 100644 --- a/_typos.toml +++ b/_typos.toml @@ -13,7 +13,7 @@ extend-exclude = [ [default.extend-words] # "ser" — serialization abbreviation (mermaid node IDs, serde ser/de), not a typo of "set". ser = "ser" -# "symetric" — the real directory name in leanMultisig (`crates/backend/symetric`), misspelled +# "symetric" — the real directory name in leanVM (`crates/backend/symetric`), misspelled # upstream. Correcting it in our docs would point readers at a path that does not exist. symetric = "symetric" diff --git a/docs/src/concepts/formal-verification.md b/docs/src/concepts/formal-verification.md index 68a0538..0c8b0d7 100644 --- a/docs/src/concepts/formal-verification.md +++ b/docs/src/concepts/formal-verification.md @@ -1,6 +1,6 @@ --- title: Formal Verification -last_updated: 2026-07-22 +last_updated: 2026-08-17 tags: - formal-verification - lean4 @@ -119,7 +119,7 @@ What must be trusted for the claim to hold — listed so no link stays implicit: library computes the proven functions. - **Cryptography.** `hash_tree_root` collision resistance is an axiom (SSZ-7); the algebra of Poseidon / KoalaBear and XMSS is ArkLib's domain and enters the model only at call - sites; leanMultisig's implementation is trusted in the Runtime Shell. + sites; leanVM's implementation is trusted in the Runtime Shell. - **The Rust toolchain and shell.** rustc, and the Runtime Shell / I/O Edge code — held to the panic-free bar and model checking rather than proof. - **Hardware and OS**, under everything. diff --git a/docs/src/reference/architecture.md b/docs/src/reference/architecture.md index 4c64e97..104d735 100644 --- a/docs/src/reference/architecture.md +++ b/docs/src/reference/architecture.md @@ -1,6 +1,6 @@ --- title: Verity Architecture -last_updated: 2026-08-14 +last_updated: 2026-08-17 tags: - architecture - verification-boundary @@ -85,7 +85,7 @@ flowchart TB subgraph B["Runtime Shell — Rust, panic-free"] direction LR CODEC["SSZ codec + hash_tree_root
wire bytes ↔ typed values"] - CRYPTO["Signature verification
verity-crypto: XMSS · leanMultisig"] + CRYPTO["Signature verification
verity-crypto: XMSS · leanVM"] STORE["State + fork-choice store
single writer · threads immutable values"] DB["Database
blocks · states · anchor"] FFI["FFI bindings layer"] @@ -182,8 +182,9 @@ upstream Lean library name per Rust's `-sys` convention. - `verity-p2p` — gossip and req/resp over libp2p. - `verity-crypto` — adapter over the two upstream signature libraries: [`leansig`](https://github.com/leanEthereum/leanSig) - for per-validator XMSS sign / verify, and [`leanMultisig`](https://github.com/leanEthereum/leanMultisig) - for aggregation and aggregate-proof verification. One capability contract, two suppliers behind it. + for per-validator XMSS sign / verify, and [`leanVM`](https://github.com/leanEthereum/leanVM) + (formerly leanMultisig) for aggregation and aggregate-proof verification. One capability + contract, two suppliers behind it. - `verity-db` — persistence (Repository): blocks, states, aggregate proofs, and the finalized anchor. Keeps the storage concern out of the single-writer aggregate coordinator. See [Storage engine and retention](#storage-engine-and-retention).