企业官网建设流程全解析

Linera 协议正确性规范（linera-spec）完全指南：微链共识的 Safety、Liveness 与 Accountability 证明体系

【免费下载链接】linera-protocolMain repository for the Linera protocol项目地址: https://gitcode.com/GitHub_Trending/li/linera-protocol

linera-spec是 Linera 协议正确性规范的统一入口：它本身不包含任何代码，只作为一个"索引 crate"，把散落在linera-chain与linera-core中的全部规范声明（statement）用 rustdoc 内链串联成一份可编译、可交叉引用的形式化论证体系。本文以 linera-spec/README.md 与 linera-spec/src/lib.rs 为核心骨架，结合各proof模块源码，系统讲解该规范的系统模型、三大头条结论（CommitAgreement/AccountableSafety/UnboundedProgress）、阅读顺序、声明编码方式（marker trait + supertrait 依赖）、安全性与活性假设的刻意分离、已知缺口与覆盖范围，并给出本地构建规范文档的完整命令。

读完本文，你将能够：理解 Linera 微链共识被证明了什么、没被证明什么；读懂规范中每一条声明的六种标签与证明依赖链；知道哪些假设是安全论证的根基、哪些只影响活性；以及如何在一分钟内用cargo doc在本机构建出可点击的完整规范文档。

背景：什么是 Linera 的正确性规范

Linera 是一个多链协议：状态被划分为若干microchain（微链），每条微链在每个区块高度独立运行自己的共识实例。任何链都无法直接读取另一条链的状态，它们之间只能通过显式消息传递（message passing）和共享的不可变存储（目前已发布的内容寻址 blobs 与事件流）通信。

在这种架构下，"共识正确"需要被精确地定义和论证。linera-speccrate 就是这份论证的入口。它声明自己要达成的目标：建立对单条微链区块序列的一致（agreement），以及被认证区块对缺席节点（在区块被认证时不在场的节点）的保证。规范按子系统（subsystem by subsystem）撰写，其索引的Coverage一节明确列出了目前尚未被任何声明约束的内容。

一个"无代码" crate 的存在意义

从 linera-spec/Cargo.toml 可以看到，这个 crate 只声明了三个依赖：linera-chain、linera-core、linera-execution，且package.metadata.cargo-machete中特意注明了这三个依赖"仅为了让规范索引能解析进持有声明的 crate 的 intra-doc 链接"，因为 rustdoc 需要它们被声明，但 Rust 源码中并没有任何引用。这就是"无代码 crate"的典型形态。

它的存在理由在 linera-spec/src/lib.rs 中有清晰说明：声明（statements）本就位于它们所描述的代码旁边——分布在linera_chain::manager::proof、linera_chain::data_types::proof、linera_chain::justification::proof、linera_chain::proof与linera_core::proof中。需要一个独立的 crate 来统一索引它们，是因为linera-core依赖linera-chain，链条 crate 自己无法引用活性（progress/liveness）结论；而如果索引放在linera-core里，就不得不用散文描述半个规范。linera-spec站在两者之上，可以用路径逐条引用每个声明，所有交叉引用都由文档构建（rustdoc）自动校验。

核心系统模型：共识实例、轮次与正确性定义

规范的第一站是 linera-chain/src/manager/proof/model.rs，这里定义了系统模型和安全性论证所依赖的全部假设，是整个依赖图的叶子节点。

Consensus instance：一次只决定一个块

定义（共识实例）：协议按链、按高度一次决定一个块。一个consensus instance是二元组(chain, height)，其状态是一个ChainManager，可通过ChainStateView::manager访问，其高度对应ChainTipState::next_block_height。

实例的创建与销毁由ChainManager::reset完成：它清空所有视图、从新的所有权重新推导领导者分布，并把current_round设为ChainOwnership::first_round。该函数只在linera_chain::chain的两个位置被调用：initialize_if_needed（链在高度 0 变为活跃时）和reset_chain_manager（高度h的已确认块被执行后，为高度h+1创建新实例）。

由此推出一个关键结论：locking 模块中的所有不变量都限定在单个实例内——它们从实例创建起成立到实例被 reset 为止，不跨 reset 承诺任何东西。这是可靠的，因为 reset 只会在该高度区块已提交后发生，后续实例决定的是不同高度。跨 reset 恢复状态是唯一的例外，由SafetyStateRecovery处理。

Round 的全序与后继

定义（轮次顺序）：轮次是Round值，由枚举上派生的Ord全序决定，先按变体、再按内嵌的u32排序：

Round::Fast < Round::MultiLeader(0) < Round::MultiLeader(1) < … < Round::SingleLeader(0) < Round::SingleLeader(1) < … < Round::Validator(0) < Round::Validator(1) < …

特别地，Round::Fast是全局最小值，多个论证直接使用这一点（例如形如x.round() < Round::Fast的守卫永不可满足）。

后继函数是ChainOwnership::next_round，它不是上述全序的后继——它会跳过链未配置的多领导者轮次，并饱和进Round::Validator。它只是单调的，而这正是轮次推进结果所需要的全部性质。

Correct validator：关于"签名"而非"可用性"

定义（正确验证者）：一个验证者在某次执行中correct，当且仅当它产生的每个签名都由该代码的未修改构建、经由linera_core::worker::WorkerState的公共入口驱动、且私钥无其他方持有而产生。不正确的验证者即faulty，可以随时签署任何内容，包括自相矛盾的声明。

这个定义是关于签名、而非关于可用性的。一个正确验证者可以缓慢或不可达而不变 faulty，尤其是：它可以在任意时刻崩溃并重启，丢失尚未持久化的一切。这是 crash-recovery 模型而非 fail-stop 模型：GST 之前崩溃可以任意频繁、重启可以任意缓慢；GST 之后恢复受linera_core::proof::assumptions::BoundedRecovery约束。

这正是DurablePersistence是承重墙（load-bearing）而非卫生习惯的原因：一个签了投票却在保存前崩溃的验证者，重启后没有任何"投过票"的记录——它可以在同一轮次再次投票，从而破坏OneValidationVotePerRound。这是一个安全性失败，而非丢消息。所以持久化义务被表述为正确性的条件，而不是实现细节。

冲突块与链式结构

定义（冲突块）：两个Block在具有相同chain_id与height但哈希不同时conflict。证书认证的是ConfirmedBlock/ValidatedBlock，二者都包装一个Block并哈希到该块的哈希。

注意一个关键细节：Block是ProposedBlock连同其BlockExecutionOutcome。因此两个提案相同但执行结果不同的块也冲突——它们导向不同的链状态，协议必须排除它们，这一排除由DeterministicExecution承担。

祖先链无需单独定义：ChainTipState::verify_block_chaining要求提案的高度等于 tip 的下一个高度、其previous_block_hash等于 tip 的块哈希，因此链的已提交块构成一条哈希链接的链表，每个高度一个块。

三大头条结果：Safety、Accountability 与 Liveness

规范在 lib.rs 的 Headline results 中锚定共识核心的三个结果，每个都针对单条微链的区块序列。

安全性（Safety）：CommitAgreement

定理（提交一致性）：对任意链和高度，所有有效的已确认块证书认证同一个块；等价地说，两个冲突块永远不可能都被提交。该结论的完整证明见 linera-chain/src/manager/proof/safety.rs，它不使用任何同步性、可用性或公平性假设，只依赖MaxByzantineWeight（每轮次的拜占庭权重上限）以及密码学与持久化假设。

证明思路是：假设存在对A（轮次r）和B（轮次s）的有效已确认证书，不失一般性设r ≤ s。

• 若r = s：由EpochAgreement二者以同一委员会裁决，由CertificateEmbedsQuorum它们的签名者集是该委员会的两个 quorum，由CorrectValidatorInIntersection存在同时签了二者的正确验证者v，再由OneConfirmationVotePerRound推出A = B。
• 若r < s：则s不是Round::Fast，由CommitRestsOnValidation存在对B的有效验证证书；再对A在轮次r的提交与s > r应用LockPreservation归纳，推出该证书认证的就是A，故B = A。

其中唯一的非平凡步骤是LockPreservation——一个对轮次的归纳，证明一旦某个块被提交，任何更晚的轮次都无法再验证别的块。归纳的良基性来自轮次的全序，且每次对归纳假设的援引都发生在严格介于r与s之间的轮次。

问责性（Accountability）：AccountableSafety

定理（可问责安全性）：如果一致性确实失败，那么仅凭两个冲突证书本身，就能定罪权重至少为validity_threshold的验证者——这超过MaxByzantineWeight所允许的拜占庭权重上限。且没有任何正确验证者可以被定罪。完整论证见 linera-chain/src/justification/proof.rs。

这个论证刻意独立为两个性质：

• 健全性（Soundness，ProofSoundness）：被EquivocationProof::check接受的证明所点名的验证者确实是 faulty 的；正确验证者永不可被定罪。
• 完备性（Completeness，ConflictCompleteness）：两个冲突的已确认证书，仅凭证书本身即可产出足够的被接受证明。

最关键的一点：二者都不依赖MaxByzantineWeight。这正是问责性悬挂在安全性之下的原因——它消费的假设比CommitAgreement更少，因为它的职责恰恰是在安全性失效的那个 regime 中仍然成立。健全性是逐验证者的，只依赖UnforgeableSignatures；完备性只需要Intersection，而Intersection只需要ThresholdArithmetic。

EquivocationProof有四种形态，每种都展示验证者v自己的两个签名——或（InvalidJustification形态）单个签名加其承诺的 opening。其中只有InvalidJustification会查阅committee参数（用于判断 opening 是否是委员会 quorum）；LockViolation、DoubleVote、FirstRoundViolation都与委员会无关，无论提供哪个委员会、甚至无论被点名的验证者是否属于某个委员会，它们的判定都成立。没有任何形态检查委员会成员资格或权重——被接受的证明说的是"这个密钥 equivocate 了"，而不是"这个委员会成员 equivocate 了"；把一组证明换算成权重是消费者的职责。

活性（Liveness）：UnboundedProgress

定理（无界进展）：在存在活跃的正确客户端（ActiveCorrectDriver）且 GST 之后，每个正确的、可达的验证者的ChainTipState::next_block_height无界增长。论证见 linera-core/src/proof/liveness.rs。

其下层的RoundProgress定理揭示了时间参数与活性的关系：由RoundAdvancement，GST 之后正确验证者的公共轮次无界增长；由RoundTimeoutGrowth，轮次n的超时是base_timeout + timeout_increment · n，随n无界。设T为 GST 之后正确领导者完成一轮所需的墙上时间（由ProposalAccepted、ValidationQuorumForms、FinalizationQuorumForms可知它是O(Δ)加有界本地处理，故有限），选择满足base_timeout + timeout_increment · n > T的n。由EventuallyCorrectLeader存在轮次号至少为n、领导者正是正确驱动者所属所有者的SingleLeader轮次，于是在该轮内：提案被全部正确验证者接受 → 验证证书形成 → 确认证书形成，三步都在超时内完成，没有正确验证者在此期间签署超时投票，该轮不被截断，块得以提交。

第三步的"无正确验证者离开该轮"前提正是超时比较买来的：没有RoundTimeoutGrowth，轮次会在飞行途中过期，每次尝试以同样方式失败，轮次将永远推进而不提交任何块。

阅读顺序：证明就位，阅读有序

声明（statements）位于它们所描述的代码旁，但被写成按特定顺序阅读，且每条声明只引用位于其之上的声明。README 与 lib.rs 给出了完整的阅读顺序表：

在仓库中，这些模块分别位于 linera-chain/src/manager/proof/、linera-chain/src/data_types/proof/、linera-chain/src/justification/proof.rs、linera-chain/src/proof/ 与 linera-core/src/proof/。

如何读一条声明：marker trait 编码与六种标签

这是本规范在形式化工程上最有辨识度的设计。每条声明都是一个没有成员、没有实现者、没有运行时足迹的公共 marker trait。它的名字就是它的身份；其 doc 注释承载声明正文，除非它是定义或假设，否则还承载证明。

Supertraits 即证明依赖

一条声明将其 supertraits 精确地列为"其证明所消费的、更早的声明"：

pub trait RoundProgress: EventuallyCorrectLeader + LockRecovery + ProposalAccepted + … // ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ // 这条证明消费的声明

例如 linera-core/src/proof/liveness.rs 中的RoundProgress就列出了EventuallyCorrectLeader + LockRecovery + ProposalAccepted + ValidationQuorumForms + FinalizationQuorumForms + TimeoutCertificateForms + CommittedBlock七个 supertraits；而 linera-chain/src/manager/proof/safety.rs 的LockPreservation则列出了UnlockingJustification + CommitRestsOnValidation + UniqueValidatedBlockPerRound + NoValidatedBlockInFastRound + OneConfirmationVotePerRound + … + EpochAgreement共 18 个依赖。CommitAgreement本身的 supertrait 列表同样可在同一文件 第 207 行 看到——它消费的全部引理、不变量与定义尽收眼底。

这个形状不用任何定制工具就买到了五重检查：

1. 唯一标识符：Rust 名字解析保证声明名全局唯一；
2. 被引用声明与被引用 Rust 项的存在性：rustdoc::broken_intra_doc_links在 CI 中被 deny，任何失效引用直接导致构建失败；
3. 依赖图无环：rustc的E0391错误天然检出循环 supertrait；
4. 每条声明页面上渲染出可点击的依赖列表；
5. 刻意没有编号：名字在插入新声明时保持稳定，过期的引用是构建失败而非静默错误的交叉引用。

六种标签

每条声明以六种标签之一开头，每个标签本身都有含义：

其中没有任何一个是关系性的：没有声明被标记为"它从什么推出来"。因为这些页面可从任何位置通过链接到达，不存在可以让标签回指的"前一个结果"——而 supertrait 列表已经精确地、可检查地点名了每条声明从何而来。

配套的算术引理示例

linera-chain/src/data_types/proof/quorum.rs 是全规范唯一对权重做算术推理的模块，其上层所有结果都经由CorrectValidatorInIntersection、CorrectSignerCastItsVote、CertificateCarriesCorrectVote、CorrectValidatorsFormQuorum四个引理消费它们。两个代表性引理：

ThresholdArithmetic：f⁺ = ⌈N/3⌉且2·q ≥ N + f⁺。证明依据Committee::new的计算：validity_threshold = total_votes.div_ceil(3)、quorum_threshold = (total_votes + validity_threshold).div_ceil(2)。两个字段都是存储而非使用时重算的，因此证明需要它们对"网络上传来的委员会"也可靠——确实如此：Committee的Deserialize实现会从验证者权重重算两者，并在与序列化值不符时拒绝该委员会。

Intersection（Quorum 交集）：同一委员会的任何两个 quorumS₁、S₂满足w(S₁ ∩ S₂) ≥ f⁺。由容斥原理：w(S₁ ∩ S₂) = w(S₁) + w(S₂) − w(S₁ ∪ S₂) ≥ q + q − N ≥ (N + f⁺) − N = f⁺。由此立即得到：同一委员会的任何两个 quorum 至少共享一个正确验证者（交集权重至少f⁺，而拜占庭权重严格小于f⁺）。

安全性与活性的刻意分离

规范中两条论证线的假设故意不相交，模块布局也反映了这一点：

MaxByzantineWeight, UnforgeableSignatures, EventualSynchrony, ClockAccuracy, DurablePersistence, SequentialChainState, CorrectValidatorAvailability, EpochAgreement, DeterministicExecution ActiveCorrectDriver, LeaderFairness, | RoundTimeoutGrowth, FullReachability v | quorum properties | | | v v voting rules --> rounds --> locking --> commit --> progress | | v v SAFETY LIVENESS CommitAgreement UnboundedProgress | v ACCOUNTABILITY AccountableSafety

右列的一切都可以失效——网络可以永远分区、所有客户端可以消失、时钟可以漂移——而不会危及CommitAgreement。左列没有任何一项可以失效而不危及它。问责性悬挂在安全性之下而非之上：它消费的假设比CommitAgreement更少，因为它的工作恰恰是在安全性不成立的那个 regime 中仍然成立。

活性所需的假设集中在 linera-core/src/proof/assumptions.rs，例如：

• EventualSynchrony：存在协议未知的 GST 与 Δ，GST 后正确参与者间的每条消息在 Δ 内送达。注意"参与者"包括客户端——Linera 共识轮次由客户端驱动（ActiveCorrectDriver），因此相关往返是客户端到验证者，而非验证者到验证者。GST 之前什么都不承诺。
• CorrectValidatorAvailability：GST 后每个正确验证者接受请求并在 Δ 内应答，其WorkerState在有限本地时间内完成每个请求。这比CorrectValidator更强（后者允许正确验证者永久崩溃）。它还要求单链队列不无界增长——被请求淹没的链可以在无任何验证者 faulty 的情况下饿死自己的共识。
• BlobRetention：正确处理过已认证块的验证者保留该块所需 blobs。内容寻址让 blob 无法被伪造，但不能让 blob存在。目前该假设通过省略而满足：linera-storage与linera-views中没有回收（collection）逻辑，保留无界，假设平凡成立——但BlobState记录了origin, last_used_by, epoch，其形状表明作者并未把它当作最终策略。

已知缺口：证明想要而实现未交付的三处

lib.rs 明确列出三处"实现没有交付证明所想要的东西"的缺口。每一处都需要改代码或弱化结果才能闭合，没有一处能靠重读来闭合：

1. FullReachability：锁定恢复步骤想要提案者到达每个正确验证者，而synchronize_chain_state只保证 quorum 加一个宽限期。只影响活性。
2. MissingDependenciesAreRecoverable：消费消息或读取事件的块依赖第三条链上起源的数据。blobs、祖先、链状态都可以自供给（滞后验证者直接拿到它们），但这两类不行。如果提案者也不跟随发送/发布链，验证者就得等自己对该链的追赶——没有任何假设约束这个等待，因此ValidationQuorumForms的2Δ步骤不适用于此类块。只影响活性。
3. AccountabilityScope：错误的块执行不可归因，且其影响不限于单链：错误的messages或events字段会被其他链消费，其产出的块本身却可能被正确认证。防护措施是CertifiedBlockWasExecuted与IncomingBundlesAreSelfDerived，但与问责性结果不同，它们都需要MaxByzantineWeight（相关跟踪见 issue #6675）。

依赖当前代码形态的论证：不是缺口，但会失效

以下是不是缺口的三项：每条目前都是可靠的，但它们之所以成立是因为代码当前的排布方式，而非结构保证。这类改变不会让任何声明显式变错，但会使论证失效，因此被列出以便变更发生时能被识别：

后两项描述的是"公共方法的前置条件靠约定而非类型满足"——这既是潜在隐患，也是维护义务，与跟踪apply_confirmed_block的 issue #6686 同构。

Coverage：已确立与尚未约束

今天已确立的四个方面

• 一致性（Agreement）：单条微链的区块序列，及其问责性逆命题与进展对应物——即上述三大头条结果。
• 可用性（Availability）：已认证块对认证时缺席的节点保证什么、崩溃要付出什么代价。代表声明包括InboxHoldsOnlySentBundles（inbox 只持有来源真正发送过的 bundles）、BundleConsumedAtMostOnce（没有两个块消费同一 bundle）、BlockOutputsArePersisted（已发布 blobs、事件与证书在块被计入已处理之前到达存储）。
• 检查点守恒（Conservation across a checkpoint）：事件、消息、blobs 与执行状态在跨检查点后行为与没有检查点时一致（linera-chain/src/proof/checkpoints.rs）。
• 委员会知识的奠基（Grounding of committee knowledge）：没有委员会认证自己的引入，这正是对 epoch 做归纳的合法性来源（CommitteeKnowledgeIsWellFounded，见 linera-chain/src/proof/epochs.rs）。

客户端通知也被规范了（linera-core/src/proof/notifications.rs），但模型把它当作有损信道而非任何保证的依托。

尚未被任何声明约束的内容

• 状态迁移正确性：执行达成一致的块是否产生正确状态。DeterministicExecution是被假设而非被证明的，执行终止性根本没有被声明。已被保证的是：已认证块被某个正确验证者执行过（CertifiedBlockWasExecuted）、投票者把每个消费的 bundle 与自己的 inbox 匹配过（IncomingBundlesAreSelfDerived）、缺失输入的块所需的输入可供给滞后验证者（MissingDependenciesAreRecoverable）。安全论证触及执行的唯一一点是FastRetryPreservesBlock——它用DeterministicExecution而非重试时的运行时检查，闭合"同一提案 → 同一块"的步骤。其余地方两者刻意分离。
• 跨链消息传递子系统——尤其是投递：没有任何声明保证 outbox 会被排空，因此没有 bundle 被保证送达。
• 委员会重配置：部分覆盖。CommitteeKnowledgeIsWellFounded固定了节点对委员会知识的来源，MaxByzantineWeight对每个未撤销委员会都被假设，因此故障界随 epoch 创建而累积；仍被假设的是 epoch 的委员会本身达成一致（EpochAgreement），且撤销目前不可用——没有委员会会被退役，累积永不停止。
• 链所有权与生命周期：谁可以在某高度提案、如何变化；ConsensusInstance记录了对此的假设。
• 资源控制与费用：计量、声明的块限制与费用守恒。
• 事件流子系统：追加性以及跨链OracleResponse::Event读背后的发布者侧保证；目前只涉及检查点边界——EventFloorTracksCheckpoints说明哪些索引跨检查点仍可读。

在本地构建规范文档

README 给出的构建命令（推荐完整版，六个 crate 缺一不可，因为声明页面大量引用linera_base的轮次、所有权、块高度与密码学类型，用linera_execution的委员会阈值，且点击进入ChainManager本身会到达linera_views）：

cargo doc --no-deps -p linera-spec -p linera-chain -p linera-core \ -p linera-base -p linera-execution -p linera-views open target/doc/linera_spec/index.html # xdg-open on Linux

在暖工作区上只需几秒。若想缩短命令，有两点须知：

• 不要用--open：当传入多个 package 时它只会挑一个打开，而挑中的往往不是linera-spec；请直接打开target/doc/linera_spec/index.html。
• 不要去掉--no-deps：去掉会为整个依赖闭包——数百个 crate——生成文档，而不是这六个。

六个 crate 全部需要，链接才能解析。省略任何 one 都会导致 intra-doc 链接断裂，而这正是这套体系将"文档腐坏"转化为"构建失败"的用武之地。

结语：一套把文档正确性交给编译器守门的形式化体系

linera-spec的独特之处在于它把"规范"从散文降维成了可编译的 Rust 结构：每一条声明是一个无运行时足迹的 marker trait，supertrait 列表就是证明依赖表，名字就是身份的稳定标识，六种标签编码了声明类型，而 rustdoc 内链、E0391与 CI 中的broken_intra_doc_linksdeny 共同把"引用腐烂"从文档问题变成了构建错误。在此基础上，它诚实地区分了三类内容：已被证明的（三大头条结果与四块覆盖区）、已知缺口（FullReachability、MissingDependenciesAreRecoverable、AccountabilityScope）、以及依赖当前代码排布、变更即失效的论证（VoteConstructionSites、ProposalGate、SafetyStateRecovery）。想要深入逐条阅读，在仓库根目录运行上文构建命令，然后从target/doc/linera_spec/index.html的Coverage与阅读顺序表开始，按子系统逐步深入各proof模块即可。

【免费下载链接】linera-protocolMain repository for the Linera protocol项目地址: https://gitcode.com/GitHub_Trending/li/linera-protocol