chore: follow the upstream leanMultisig → leanVM repository rename - #25
Merged
Conversation
The upstream repo leanEthereum/leanMultisig was renamed to leanEthereum/leanVM on 2026-08-14 (the old URL redirects). Update every reference: CLAUDE.md, README.md, ARCHITECTURE.md and its docs mirror, DOMAIN_MODEL.md, formal-verification.md, the _typos.toml comment, and the skill set (directory renamed to leanVM; the old name kept as a legacy trigger; cross-referencing skills updated). First mentions in prose carry a '(formerly leanMultisig)' note so older discussions stay traceable.
adust09
added a commit
that referenced
this pull request
Aug 20, 2026
* docs: specify the verity-db storage schema (#19) * docs: specify the verity-db storage schema Settles the table layout under the engine and retention decisions already recorded in ARCHITECTURE.md: keys, pruning rules, and how state is stored. The layout is driven by a growth model that the SSZ fixtures alone hide. A state measures 342-774 B there, but process_slots appends to historical_block_hashes every slot and cannot trim it, because that list is indexed by absolute slot. State size is therefore ~300 B + 32 B x slot: ~691 KB one day in, ~8.4 MB at the 2^18 limit. A full state per block would cost ~7.5 GB over the first day and grow quadratically — heavier than the aggregate proofs. Snapshots every 1,024 slots plus parent-linked diffs bring the same data to ~10-15 MB/day, provided a diff omits historical_block_hashes and regenerates it from base_root and the slot gap. Full state history is retained: snapshots and diffs are never pruned, so any past block's state stays reconstructible. The diff chain grows monotonically; that cost is accepted for the leverage it gives while the upstream spec moves. Blocks are stored unsigned with the proof as a separate row, so a block whose proof has been pruned still reads back. Attestation-level signatures and aggregated payloads stay in memory, matching what leanSpec's reference node persists — the one addition is block proofs, which are persisted so BlocksByRange serving survives a restart. Also adds STORAGE.md to the scheduled link check, alongside the other root docs. * docs(storage): tighten Metadata, StateRootIndex, and fork-scoping wording - Metadata: drop genesis_time from the scalar list; note it is a field of config used to derive the network fingerprint, not a separate column. - StateRootIndex: align the Pruned cell with Blocks (never), keeping the tie-to-block note, so the two rows no longer read as contradictory. - Snapshot/diff recovery: scope the config/validators-immutability claim to the current lstar STF and flag validator-mutating forks as the revisit point. * docs(storage): align schema with persistence decisions Capture the agreed recovery, fork-choice, and range-sync invariants in the existing storage-schema pull request so the first implementation has one consistent repository contract. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs: settle the I/O Edge concurrency model (#20) * docs: settle the I/O Edge concurrency model Settle the question ARCHITECTURE.md left open: which concurrency primitive enforces the single-writer discipline, where signature and proof verification execute, and how inbound work reaches the chain task. Decisions, selected for verifiability (Loom tractability, sequential FFI, fold-refinement against leanSpec) rather than throughput: - verity-chain is one dedicated tokio task owning Store and State; reads leave as watch-published Arc<ChainView> snapshots. - Verification runs in a dedicated stage between the network task and the chain task, on spawn_blocking (no rayon, no promotion path), with a private-constructor Verified* type boundary and a bounded pending buffer for unknown-parent items. - Three inbound channels split by full-queue policy (tick = watch and coalescable, local duty products = never dropped, network = shed at the network edge only, pre-verification), read via biased select. Evidence recorded in the document: leanSpec constrains ordering only (read at cce7955), and a four-client survey (ethlambda e16f477, ream 842a709, zeam 6495beb, qlean-mini 55b6eb3) shows no client gates propagation on verification while maturing clients offload it. * docs: close the cold-start gaps in the concurrency model A cold-start review (reader with no design-discussion context) found the document non-self-sufficient. Close every gap at the document level: - Define the ChainView contract (head + checkpoints + registry resolution by root) and state that the watch snapshot is the entire read path — no query channel into the chain task. - Define what Verified* values carry (typed container + computed roots). - Specify the pending-buffer mechanics: select on input + watch::changed, retry only newly-resolvable entries, FIFO eviction, silent eviction recovered by range sync, never blocks, failed verification drops immediately. - Specify the chain-task loop: one event per biased-select iteration; tick handling must step interval-by-interval to the target. - Add a Lifecycle section (startup order, first-ChainView readiness signal, shutdown drain/discard policy per channel). - Add a deliberately-deferred list (capacities, struct layouts, peer scoring) so deferrals are not mistaken for omissions. - State the escaped-panic policy (abort, availability failure). * docs: resolve the second cold-start round on the concurrency model Second no-context review still found divergence points; fix each at the design level and fence the rest: - ChainView: fix the retention bound (unfinalized tree + finalized anchor; historical reads are verity-db's job, so an RPC historical query is a database read, not a snapshot miss), publication cadence (at most once per loop iteration, post-import), and distribution (receiver handed out at construction; doubles as the readiness signal — no separate mechanism). - Tick: current interval IS Store.time and the handler is the spec's own on_tick loop; leanSpec's tick_interval is the authoritative action map (the listed actions are orientation, not restated spec); catch-up replays cheaply (no STF work in interval actions). - Aggregation wiring: the interval-2 action hands the signature-pool snapshot to verity-validator's worker; the chain task never awaits. - Verification failures: definitive failures (malformed SSZ, root mismatch, invalid signature/proof) drop immediately with metrics; the pending buffer holds only the one recoverable case. - Network edge: try_send into the stage's bounded input channel named as the pipeline's single drop point. - Shutdown: drained = sender dropped + recv to None, no side-channel. - Deferred list: add sizing anchors (tens for local, hundreds for network/pending) and internal data structures. * docs: settle the third-round cold-start findings - The pending buffer holds both recoverable cases under one policy: a block awaiting its parent post-state and an attestation awaiting its target post-state, keyed by the awaited root. Eviction recovery differs per kind and is stated: blocks via range sync, attestation votes re-arrive embedded in an aggregate or block body. - Shutdown: channel closure is the only signal (no broadcast); the binary stops edge producers, sender drops cascade, downstream tasks exit on None. - Startup: the verity binary opens/validates the database and hands the chain task its handle; Store initialization (time included) follows leanSpec. * docs: close the fourth-round cold-start findings on the concurrency model - Specify the production side of channel 2: validator-duty tasks are driven by the same slot clock that feeds channel 1 (one clock in the binary, two consumers), read the ChainView snapshot for proposal head / attestation target, and push signed products into channel 2; the chain task never triggers production by callback (sole involvement: the interval-2 aggregation handoff). - Define in-flight disposal at shutdown: running spawn_blocking verifications finish and their results are discarded (blocking work is uncancellable); the pending buffer is dropped. - Make the interval-action map normative by reference to leanSpec main (tracked revision), not a frozen restatement. * docs: settle XMSS validator key-state management (#23) * docs: settle XMSS validator key-state management Settle design area 2 of the client-specific design campaign: how Verity manages stateful XMSS signing keys. The asset protected is the key's cryptographic soundness (reuse = forgeability), not a protocol penalty — the lean protocol has no slashing. Decisions: - Signing watermark with persist-before-sign: last-signed slot per (validator, role) in a dedicated verity-db column family, fsynced before any signature leaves the process; equality refused even for identical messages; clock-rewind fails closed at startup. The validator signing path is the family's sole writer — the one documented exception to the chain writer, one-writer-per-family. - Key material: lean-quickstart-compatible layout, Verity-owned loader in verity-crypto (none exists in the ecosystem), manifest roles authoritative, fail-closed rejects (missing/identical role keys, pubkey mismatch), fully memory-resident (~67 MB/validator). - Preparation: midpoint check per duty tick, advance on spawn_blocking via clone-advance-swap so signing never waits, advanced key persisted by atomic replace (bounds startup catch-up by downtime, not node age), panic-containing sign wrapper, startup catch-up gated before validator readiness. Grounded in leanSpec cce7955 (epoch = slot; two keys per validator; deterministic signatures; no slashing) and leanSig c08a3ba (no reuse guard; panics outside the ~6-day prepared window; no loader exists), plus a four-client survey (ethlambda e16f477, ream 842a709, zeam 6495beb, qlean-mini 55b6eb3): none persists signing state; ream never advances the window; zeam falls back to one key for both roles. * docs: close the first cold-start round on key management - Startup: key preparation is verity-validator's own init task, runs in parallel with chain startup (needs no consensus state); duty readiness is a join of two independent gates (first ChainView AND keys prepared), not a step inserted into the lifecycle sequence. - Absent watermark row = normal first-run state, first sign creates it; the fail-closed clock-rewind condition is watermark >= current slot, matching the sign path's own comparison. - State why the original key stays signable during clone-advance: midpoint advancing makes old and new windows overlap ~3 days around the current slot. - Advanced-key persistence: the spawn_blocking worker writes the file (atomic temp+rename) before returning the clone; write failure is non-fatal (watermark, not the key file, carries no-reuse). * docs: reconcile validator startup between the concurrency and key docs The second cold-start round found the one remaining defect: CONCURRENCY.md said validator-duty tasks 'start' only after the first ChainView, while KEY_MANAGEMENT.md ran key preparation in parallel with chain startup. Resolve it on both sides: the first ChainView gates *serving*, not construction — the binary spawns the validator task at process start, its key preparation runs in parallel with chain startup, and the duty loop serves only on the join of (first ChainView observed) and (keys prepared). * docs: state that the first ChainView is a necessary, not sufficient, serving gate Third cold-start round: CONCURRENCY.md alone read as if ChainView were the only serving gate, while KEY_MANAGEMENT.md adds a second gate for the duty loop (keys prepared). Name the rule in CONCURRENCY.md itself: ChainView is necessary for every component, components may add their own conditions, and validator-duty is the named case. * chore(lint): allow the leanSig commit SHA c08a3ba as an identifier typos tokenizes the abbreviated SHA and flags its trailing 'ba' as a typo of 'by'/'be'; the SHA is cited in KEY_MANAGEMENT.md. * docs: settle the sync pipeline (#24) * docs: settle the sync pipeline Settle design area 3 of the client-specific design campaign: how Verity joins the network and catches up. Pays the two debts recorded by CONCURRENCY.md and KEY_MANAGEMENT.md: the gap-noticing mechanism (the verification stage signals awaited/evicted parent roots to the sync service) and the peer-scoring policy. Decisions: - Lifecycle: the reference node's IDLE -> SYNCING -> SYNCED machine; trigger = our head below the majority-voted network finalized slot (not head-lag - zeam's documented deadlock; not max - one liar); continuously re-evaluated (Status re-exchanged periodically, unlike ethlambda/qlean-mini's once-per-connection); duties require SYNCED as the duty loop's third serving gate; checkpoint sync is an HTTP entry procedure verified at ethlambda depth, fail-closed with no silent fallback. - Fetch pipeline: sync service as its own I/O Edge task; small gaps by BlocksByRoot (capped walk), large gaps by BlocksByRange forward, one batch in flight; all fetched blocks pass through the verification stage into channel 3 - no side door; structural response validation in the sync service feeds the peer score; during SYNCING the block topic stays subscribed while attestation/ aggregation processing pauses. - Peers: the reference reliability score (100, +10/-20, weighted random, never fully excluding, 2 concurrent/peer); transient failures never set capability conclusions (TTL'd flags on genuine protocol rejection only); invalid gossip is metrics-only (relays are not originators under forward-before-verify); no automatic disconnects or bans, with named revisit triggers. Grounded in leanSpec cce7955 (wire contract fixed, behavior free, reference sync implementation as precedent) and the four-client survey (ethlambda e16f477, ream 842a709, zeam 6495beb, qlean-mini 55b6eb3). * docs: close the first cold-start round on the sync pipeline - Entry: exhaustive three-path decision tree (checkpoint URL given / populated DB / empty DB -> genesis); on the checkpoint path DB and genesis are not fallbacks. - Checkpoint failures split: transient fetch errors retry within a bounded budget, definitive failures (decode, verification, 4xx) exit immediately; exhausted budget fails closed. - 'Majority vote' defined precisely: median of peers' claimed finalized slots, lower-middle on even counts. - Range pagination terminates on the state machine's own condition, read from the watch-published ChainView (no query channel). - Failure-consequence table: one fixed (score, capability-flag) outcome per event class; RESOURCE_UNAVAILABLE is the spec's legal answer (no penalty, re-route); the capability flag's only trigger is protocol-negotiation failure. * docs: resolve the second cold-start round on the sync pipeline - Define checkpoint-root consistency exactly: the fetched anchor block's hash_tree_root equals the state's latest_finalized.root, and same-slot justified/finalized checkpoints share one root. - Fix the gap signal's slot field: it is the waiting child's slot (the awaited block is known only by root), which upper-bounds the gap for the by-root/by-range split. * docs: align the duty-loop gate count across all three runtime docs The final cold-start round caught KEY_MANAGEMENT.md and CONCURRENCY.md still asserting exactly two serving gates while SYNC.md adds a third (sync state SYNCED). State the same rule in all three places: the join is of independent conditions - ChainView observed, keys prepared, and node SYNCED. * chore: follow the upstream leanMultisig -> leanVM repository rename (#25) The upstream repo leanEthereum/leanMultisig was renamed to leanEthereum/leanVM on 2026-08-14 (the old URL redirects). Update every reference: CLAUDE.md, README.md, ARCHITECTURE.md and its docs mirror, DOMAIN_MODEL.md, formal-verification.md, the _typos.toml comment, and the skill set (directory renamed to leanVM; the old name kept as a legacy trigger; cross-referencing skills updated). First mentions in prose carry a '(formerly leanMultisig)' note so older discussions stay traceable. * feat(types): define the consensus containers as verity-types (#26) Start the Rust implementation with the crate every other one depends on. verity-types holds container shapes and their SSZ codec, transcribed field for field from leanSpec at 0588c2d. Field order is consensus-critical because it determines hash_tree_root, so the transcription follows leanSpec's order rather than any reading convenience. The crate takes no dependency beyond SSZ. leanSpec defines predicates such as Slot.is_justifiable_after and Checkpoint.advance_to as methods on these containers; they are omitted here on purpose. Those predicates are the leading candidates to move into the Verified Core, and binding them to the foundational crate would make every crate that merely uses a type link the FFI boundary once that move happens. They land behind the capability that owns them. The Uint64 newtypes carry hand-written SSZ impls rather than #[ssz(transparent)] because the derive does not forward is_basic_type. A basic type reporting itself composite merkleizes one element per chunk instead of packing, producing a wrong root with no other symptom. SignedAttestation is not defined: its signature field is an XMSS container from the signature library, and it lands with verity-crypto. proptest is introduced for the SSZ round trip only. This narrows the kickoff decision that no verification harness ships on day one: a codec is one of the few places the property is writable directly, and leanSpec's fixtures only supply the shapes the spec happened to generate. The graduated harness of MODEL_CHECK.md is still introduced later. Retiring the verity-consensus canary stub removes the last member depending on leanSig, so cargo pruned the Plonky3 rev pin from Cargo.lock along with leansig, rocksdb, and libp2p. CLAUDE.md records that the pin must be re-established by whoever adds leanSig back. * chore(ci): run checks on develop without deploying PRD from it develop is DEV and main is PRD, but push triggers only listed main, so DEV never ran the quality gates. Build and lint on both branches; docs.verityclient.com still deploys only from main. --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Upstream renamed
leanEthereum/leanMultisigtoleanEthereum/leanVMon 2026-08-14 (discovered during the leanEthereum org sweep for the sync-pipeline design; the old URL redirects, and the repo's internal layout —crates/xmss/xmss.md,crates/backend/symetric,crates/lean_vm, … — is unchanged, verified against the current tree).This PR updates every reference in the repo:
CLAUDE.md,README.md,ARCHITECTURE.md+ itsdocs/src/reference/architecture.mdmirror,DOMAIN_MODEL.md,docs/src/concepts/formal-verification.md(frontmatterlast_updatedbumped on the two edited docs pages). First prose mentions carry a "(formerly leanMultisig)" note so older discussions and memories stay traceable..claude/skills/leanMultisig/renamed to.claude/skills/leanVM/with the old name kept as an explicit legacy trigger; the four cross-referencing skills (leanSpec, leanMetrics, leanQuickstart, hive) updated._typos.tomlcomment (the upstream-misspelledsymetricdirectory still exists in leanVM — path re-verified).