Linera 协议正确性规范linera-spec完全指南微链共识的 Safety、Liveness 与 Accountability 证明体系【免费下载链接】linera-protocolMain repository for the Linera protocol项目地址: https://gitcode.com/GitHub_Trending/li/linera-protocollinera-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的已确认块被执行后为高度h1创建新实例。由此推出一个关键结论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 中锚定共识核心的三个结果每个都针对单条微链的区块序列。安全性SafetyCommitAgreement定理提交一致性对任意链和高度所有有效的已确认块证书认证同一个块等价地说两个冲突块永远不可能都被提交。该结论的完整证明见 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之间的轮次。问责性AccountabilityAccountableSafety定理可问责安全性如果一致性确实失败那么仅凭两个冲突证书本身就能定罪权重至少为validity_threshold的验证者——这超过MaxByzantineWeight所允许的拜占庭权重上限。且没有任何正确验证者可以被定罪。完整论证见 linera-chain/src/justification/proof.rs。这个论证刻意独立为两个性质健全性SoundnessProofSoundness被EquivocationProof::check接受的证明所点名的验证者确实是 faulty 的正确验证者永不可被定罪。完备性CompletenessConflictCompleteness两个冲突的已确认证书仅凭证书本身即可产出足够的被接受证明。最关键的一点二者都不依赖MaxByzantineWeight。这正是问责性悬挂在安全性之下的原因——它消费的假设比CommitAgreement更少因为它的职责恰恰是在安全性失效的那个 regime 中仍然成立。健全性是逐验证者的只依赖UnforgeableSignatures完备性只需要Intersection而Intersection只需要ThresholdArithmetic。EquivocationProof有四种形态每种都展示验证者v自己的两个签名——或InvalidJustification形态单个签名加其承诺的 opening。其中只有InvalidJustification会查阅committee参数用于判断 opening 是否是委员会 quorumLockViolation、DoubleVote、FirstRoundViolation都与委员会无关无论提供哪个委员会、甚至无论被点名的验证者是否属于某个委员会它们的判定都成立。没有任何形态检查委员会成员资格或权重——被接受的证明说的是这个密钥 equivocate 了而不是这个委员会成员 equivocate 了把一组证明换算成权重是消费者的职责。活性LivenessUnboundedProgress定理无界进展在存在活跃的正确客户端ActiveCorrectDriver且 GST 之后每个正确的、可达的验证者的ChainTipState::next_block_height无界增长。论证见 linera-core/src/proof/liveness.rs。其下层的RoundProgress定理揭示了时间参数与活性的关系由RoundAdvancementGST 之后正确验证者的公共轮次无界增长由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::manager::proof::model故障与网络假设linera_chain::manager::proof::model然后linera_core::proof::assumptions协议对象与定义linera_chain::data_types::proof::objectsQuorum 性质linera_chain::data_types::proof::quorum投票规则linera_chain::manager::proof::voting锁定与证书不变量linera_chain::manager::proof::rounds然后linera_chain::manager::proof::locking提交规则linera_chain::manager::proof::commit安全性证明linera_chain::manager::proof::safety问责性linera_chain::justification::proof领导者、超时与轮次推进linera_chain::manager::proof::timeouts进展引理linera_core::proof::progress活性证明linera_core::proof::liveness可用性、崩溃恢复与追赶linera_core::proof::availability客户端通知linera_core::proof::notifications检查点保留什么linera_chain::proof::checkpoints在仓库中这些模块分别位于 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 行 看到——它消费的全部引理、不变量与定义尽收眼底。这个形状不用任何定制工具就买到了五重检查唯一标识符Rust 名字解析保证声明名全局唯一被引用声明与被引用 Rust 项的存在性rustdoc::broken_intra_doc_links在 CI 中被 deny任何失效引用直接导致构建失败依赖图无环rustc的E0391错误天然检出循环 supertrait每条声明页面上渲染出可点击的依赖列表刻意没有编号名字在插入新声明时保持稳定过期的引用是构建失败而非静默错误的交叉引用。六种标签每条声明以六种标签之一开头每个标签本身都有含义标签是否携带证明含义Definition否固定一个术语并将其钉在它所表示的 Rust 项上Assumption否实现不建立、部署方必须提供的东西Invariant是在每个可达状态中成立通过对迁移的归纳证明Lemma是一条被证明的陈述Theorem是规范存在的目的之一要确立的结果Remark / Caveat否一个观察或局限不断言任何新东西其中没有任何一个是关系性的没有声明被标记为它从什么推出来。因为这些页面可从任何位置通过链接到达不存在可以让标签回指的前一个结果——而 supertrait 列表已经精确地、可检查地点名了每条声明从何而来。配套的算术引理示例linera-chain/src/data_types/proof/quorum.rs 是全规范唯一对权重做算术推理的模块其上层所有结果都经由CorrectValidatorInIntersection、CorrectSignerCastItsVote、CertificateCarriesCorrectVote、CorrectValidatorsFormQuorum四个引理消费它们。两个代表性引理ThresholdArithmeticf⁺ ⌈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实现会从验证者权重重算两者并在与序列化值不符时拒绝该委员会。IntersectionQuorum 交集同一委员会的任何两个 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 之前什么都不承诺。CorrectValidatorAvailabilityGST 后每个正确验证者接受请求并在 Δ 内应答其WorkerState在有限本地时间内完成每个请求。这比CorrectValidator更强后者允许正确验证者永久崩溃。它还要求单链队列不无界增长——被请求淹没的链可以在无任何验证者 faulty 的情况下饿死自己的共识。BlobRetention正确处理过已认证块的验证者保留该块所需 blobs。内容寻址让 blob 无法被伪造但不能让 blob存在。目前该假设通过省略而满足linera-storage与linera-views中没有回收collection逻辑保留无界假设平凡成立——但BlobState记录了origin, last_used_by, epoch其形状表明作者并未把它当作最终策略。已知缺口证明想要而实现未交付的三处lib.rs 明确列出三处实现没有交付证明所想要的东西的缺口。每一处都需要改代码或弱化结果才能闭合没有一处能靠重读来闭合FullReachability锁定恢复步骤想要提案者到达每个正确验证者而synchronize_chain_state只保证 quorum 加一个宽限期。只影响活性。MissingDependenciesAreRecoverable消费消息或读取事件的块依赖第三条链上起源的数据。blobs、祖先、链状态都可以自供给滞后验证者直接拿到它们但这两类不行。如果提案者也不跟随发送/发布链验证者就得等自己对该链的追赶——没有任何假设约束这个等待因此ValidationQuorumForms的2Δ步骤不适用于此类块。只影响活性。AccountabilityScope错误的块执行不可归因且其影响不限于单链错误的messages或events字段会被其他链消费其产出的块本身却可能被正确认证。防护措施是CertifiedBlockWasExecuted与IncomingBundlesAreSelfDerived但与问责性结果不同它们都需要MaxByzantineWeight相关跟踪见 issue #6675。依赖当前代码形态的论证不是缺口但会失效以下是不是缺口的三项每条目前都是可靠的但它们之所以成立是因为代码当前的排布方式而非结构保证。这类改变不会让任何声明显式变错但会使论证失效因此被列出以便变更发生时能被识别声明什么会使它失效VoteConstructionSites出现第六个签名点该论证是对现存五个签名点的穷举搜索ProposalGate出现ChainManager方法的新调用者——守卫位于chain_worker::state的调用点因此若直接调用create_final_vote会在同一轮次签两次SafetyStateRecovery出现第二个恢复点ManagerSafetySnapshot与其恢复目标实例之间的对应关系依赖唯一调用点处的高度检查而非类型强制的任何东西后两项描述的是公共方法的前置条件靠约定而非类型满足——这既是潜在隐患也是维护义务与跟踪apply_confirmed_block的 issue #6686 同构。Coverage已确立与尚未约束今天已确立的四个方面一致性Agreement单条微链的区块序列及其问责性逆命题与进展对应物——即上述三大头条结果。可用性Availability已认证块对认证时缺席的节点保证什么、崩溃要付出什么代价。代表声明包括InboxHoldsOnlySentBundlesinbox 只持有来源真正发送过的 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_viewscargo 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 traitsupertrait 列表就是证明依赖表名字就是身份的稳定标识六种标签编码了声明类型而 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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考 Linera 协议正确性规范（linera-spec）完全指南：微链共识的 Safety、Liveness 与 Accountability 证明体系
Linera 协议正确性规范linera-spec完全指南微链共识的 Safety、Liveness 与 Accountability 证明体系【免费下载链接】linera-protocolMain repository for the Linera protocol项目地址: https://gitcode.com/GitHub_Trending/li/linera-protocollinera-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的已确认块被执行后为高度h1创建新实例。由此推出一个关键结论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 中锚定共识核心的三个结果每个都针对单条微链的区块序列。安全性SafetyCommitAgreement定理提交一致性对任意链和高度所有有效的已确认块证书认证同一个块等价地说两个冲突块永远不可能都被提交。该结论的完整证明见 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之间的轮次。问责性AccountabilityAccountableSafety定理可问责安全性如果一致性确实失败那么仅凭两个冲突证书本身就能定罪权重至少为validity_threshold的验证者——这超过MaxByzantineWeight所允许的拜占庭权重上限。且没有任何正确验证者可以被定罪。完整论证见 linera-chain/src/justification/proof.rs。这个论证刻意独立为两个性质健全性SoundnessProofSoundness被EquivocationProof::check接受的证明所点名的验证者确实是 faulty 的正确验证者永不可被定罪。完备性CompletenessConflictCompleteness两个冲突的已确认证书仅凭证书本身即可产出足够的被接受证明。最关键的一点二者都不依赖MaxByzantineWeight。这正是问责性悬挂在安全性之下的原因——它消费的假设比CommitAgreement更少因为它的职责恰恰是在安全性失效的那个 regime 中仍然成立。健全性是逐验证者的只依赖UnforgeableSignatures完备性只需要Intersection而Intersection只需要ThresholdArithmetic。EquivocationProof有四种形态每种都展示验证者v自己的两个签名——或InvalidJustification形态单个签名加其承诺的 opening。其中只有InvalidJustification会查阅committee参数用于判断 opening 是否是委员会 quorumLockViolation、DoubleVote、FirstRoundViolation都与委员会无关无论提供哪个委员会、甚至无论被点名的验证者是否属于某个委员会它们的判定都成立。没有任何形态检查委员会成员资格或权重——被接受的证明说的是这个密钥 equivocate 了而不是这个委员会成员 equivocate 了把一组证明换算成权重是消费者的职责。活性LivenessUnboundedProgress定理无界进展在存在活跃的正确客户端ActiveCorrectDriver且 GST 之后每个正确的、可达的验证者的ChainTipState::next_block_height无界增长。论证见 linera-core/src/proof/liveness.rs。其下层的RoundProgress定理揭示了时间参数与活性的关系由RoundAdvancementGST 之后正确验证者的公共轮次无界增长由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::manager::proof::model故障与网络假设linera_chain::manager::proof::model然后linera_core::proof::assumptions协议对象与定义linera_chain::data_types::proof::objectsQuorum 性质linera_chain::data_types::proof::quorum投票规则linera_chain::manager::proof::voting锁定与证书不变量linera_chain::manager::proof::rounds然后linera_chain::manager::proof::locking提交规则linera_chain::manager::proof::commit安全性证明linera_chain::manager::proof::safety问责性linera_chain::justification::proof领导者、超时与轮次推进linera_chain::manager::proof::timeouts进展引理linera_core::proof::progress活性证明linera_core::proof::liveness可用性、崩溃恢复与追赶linera_core::proof::availability客户端通知linera_core::proof::notifications检查点保留什么linera_chain::proof::checkpoints在仓库中这些模块分别位于 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 行 看到——它消费的全部引理、不变量与定义尽收眼底。这个形状不用任何定制工具就买到了五重检查唯一标识符Rust 名字解析保证声明名全局唯一被引用声明与被引用 Rust 项的存在性rustdoc::broken_intra_doc_links在 CI 中被 deny任何失效引用直接导致构建失败依赖图无环rustc的E0391错误天然检出循环 supertrait每条声明页面上渲染出可点击的依赖列表刻意没有编号名字在插入新声明时保持稳定过期的引用是构建失败而非静默错误的交叉引用。六种标签每条声明以六种标签之一开头每个标签本身都有含义标签是否携带证明含义Definition否固定一个术语并将其钉在它所表示的 Rust 项上Assumption否实现不建立、部署方必须提供的东西Invariant是在每个可达状态中成立通过对迁移的归纳证明Lemma是一条被证明的陈述Theorem是规范存在的目的之一要确立的结果Remark / Caveat否一个观察或局限不断言任何新东西其中没有任何一个是关系性的没有声明被标记为它从什么推出来。因为这些页面可从任何位置通过链接到达不存在可以让标签回指的前一个结果——而 supertrait 列表已经精确地、可检查地点名了每条声明从何而来。配套的算术引理示例linera-chain/src/data_types/proof/quorum.rs 是全规范唯一对权重做算术推理的模块其上层所有结果都经由CorrectValidatorInIntersection、CorrectSignerCastItsVote、CertificateCarriesCorrectVote、CorrectValidatorsFormQuorum四个引理消费它们。两个代表性引理ThresholdArithmeticf⁺ ⌈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实现会从验证者权重重算两者并在与序列化值不符时拒绝该委员会。IntersectionQuorum 交集同一委员会的任何两个 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 之前什么都不承诺。CorrectValidatorAvailabilityGST 后每个正确验证者接受请求并在 Δ 内应答其WorkerState在有限本地时间内完成每个请求。这比CorrectValidator更强后者允许正确验证者永久崩溃。它还要求单链队列不无界增长——被请求淹没的链可以在无任何验证者 faulty 的情况下饿死自己的共识。BlobRetention正确处理过已认证块的验证者保留该块所需 blobs。内容寻址让 blob 无法被伪造但不能让 blob存在。目前该假设通过省略而满足linera-storage与linera-views中没有回收collection逻辑保留无界假设平凡成立——但BlobState记录了origin, last_used_by, epoch其形状表明作者并未把它当作最终策略。已知缺口证明想要而实现未交付的三处lib.rs 明确列出三处实现没有交付证明所想要的东西的缺口。每一处都需要改代码或弱化结果才能闭合没有一处能靠重读来闭合FullReachability锁定恢复步骤想要提案者到达每个正确验证者而synchronize_chain_state只保证 quorum 加一个宽限期。只影响活性。MissingDependenciesAreRecoverable消费消息或读取事件的块依赖第三条链上起源的数据。blobs、祖先、链状态都可以自供给滞后验证者直接拿到它们但这两类不行。如果提案者也不跟随发送/发布链验证者就得等自己对该链的追赶——没有任何假设约束这个等待因此ValidationQuorumForms的2Δ步骤不适用于此类块。只影响活性。AccountabilityScope错误的块执行不可归因且其影响不限于单链错误的messages或events字段会被其他链消费其产出的块本身却可能被正确认证。防护措施是CertifiedBlockWasExecuted与IncomingBundlesAreSelfDerived但与问责性结果不同它们都需要MaxByzantineWeight相关跟踪见 issue #6675。依赖当前代码形态的论证不是缺口但会失效以下是不是缺口的三项每条目前都是可靠的但它们之所以成立是因为代码当前的排布方式而非结构保证。这类改变不会让任何声明显式变错但会使论证失效因此被列出以便变更发生时能被识别声明什么会使它失效VoteConstructionSites出现第六个签名点该论证是对现存五个签名点的穷举搜索ProposalGate出现ChainManager方法的新调用者——守卫位于chain_worker::state的调用点因此若直接调用create_final_vote会在同一轮次签两次SafetyStateRecovery出现第二个恢复点ManagerSafetySnapshot与其恢复目标实例之间的对应关系依赖唯一调用点处的高度检查而非类型强制的任何东西后两项描述的是公共方法的前置条件靠约定而非类型满足——这既是潜在隐患也是维护义务与跟踪apply_confirmed_block的 issue #6686 同构。Coverage已确立与尚未约束今天已确立的四个方面一致性Agreement单条微链的区块序列及其问责性逆命题与进展对应物——即上述三大头条结果。可用性Availability已认证块对认证时缺席的节点保证什么、崩溃要付出什么代价。代表声明包括InboxHoldsOnlySentBundlesinbox 只持有来源真正发送过的 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_viewscargo 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 traitsupertrait 列表就是证明依赖表名字就是身份的稳定标识六种标签编码了声明类型而 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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考