​
提纲

​
假设

↑ 返回提纲 作为模块化 ABCI 应用的一部分，CCV 会同时与共识引擎（通过 ABCI）以及其他应用模块（例如质押模块）交互。 作为一个 IBC 应用，CCV 会与外部中继器交互（定义见 ICS 18）。 本节说明我们对这些其他组件所作的假设。 关于 CCV 所运行环境的更完整讨论，见 在 ABCI 应用中放置 CCV 一节。
直观理解: CCV 的安全性依赖于安全区块链假设， 即安全性并不要求 活跃区块链 和 正确中继器 成立。 但需要注意，CCV 的活性同时依赖 活跃区块链 和 正确中继器 假设； 此外，正确中继器 假设又依赖于 安全区块链 和 活跃区块链 假设。 验证者更新提供、解绑安全、罚没担保 和 分配担保 假设定义了提供者链的 ABCI 应用需要满足的条件。 证据提供 假设定义了消费者链的 ABCI 应用需要满足的条件。
  • 安全区块链：提供者链和消费者链都必须是安全的。这意味着，对于每条链，其底层共识引擎满足安全性（例如链不会分叉），并且状态机的执行遵循所描述的协议。
  • 活跃区块链：提供者链和消费者链都必须是活跃的。这意味着，对于每条链，其底层共识引擎满足活性（即最终会有新区块加入链中）。
    注意：安全区块链 和 活跃区块链 两个假设都要求共识引擎自身的假设成立，例如少于三分之一的投票权是拜占庭的。可参考 Tendermint 论文。
  • 正确中继器：在提供者链与消费者链之间，至少存在一个正确且活跃的中继器。该假设具有以下含义。
    • CCV 通道上的建立握手消息会在通道初始化子协议超时之前被中继（见 initTimeout）。
    • 在 CCV 通道上发送的每个数据包都会在数据包超时到期前被中继到接收端（见 vscTimeout 和 ccvTimeoutTimestamp）。
    • 正确的中继器最终会在代币转移通道上中继数据包。
    显然，CCV 协议有责任设置这些超时参数（参见 CCV 状态 中的 ccvTimeoutTimestamp、vscTimeout、initTimeout），以使正确中继器假设可行。
    讨论：IBC 依赖超时来表示已发送的数据包不会在另一端被接收。 一旦有序 IBC 通道发生超时，该通道就会被关闭（见 ICS 4）。 正确中继器假设是必要的，以确保 CCV 通道永远不会超时，因此也就不会转入关闭状态。 在实践中，正确中继器假设是现实可行的，因为任何验证者都可以承担中继器角色，而且成功中继数据包符合正确验证者的最佳利益。 以下策略给出了一个如何确保正确中继器假设成立的实际示例。 设 S 表示发送链，D 表示目标链； 令 drift(S,D) 表示 S 与 D 之间的时间漂移， 即 drift(S,D) = S.currentTimestamp() - D.currentTimestamp()（drift(S,D) > 0 表示 S 相对于 D “更超前”）。 对于每个数据包，S 只设置 timeoutTimestamp = S.currentTimestamp() + to，其中 to 是应用层参数。 timeoutTimestamp 表示目标链上的某个时间戳，在该时间之后数据包将不再被处理（参见 ICS 4）。 因此，数据包必须在 to - drift(S,D) 的时间段内完成中继， 即 to - drift(S,D) > RTmax，其中 RTmax 是所有数据包中的最大中继时间。 从理论上讲，选择 to 的值需要知道 drift(S,D) 的值（即 to > drift(S,D)）； 然而，在链级别上并不知道 drift(S,D)。 在实践中，选择一个满足 to >> drift(S,D) 且 to >> RTmax 的 to，例如 to = 4 weeks，就可以使正确中继器假设成为可行假设。
  • 验证者更新提供：设 {U1, U2, ..., Ui} 是在区块高度 h 处由提供者质押模块应用到提供者链验证者集合上的一批验证者更新。 那么，提供者 CCV 模块在高度 h 从提供者质押模块获取到的这批验证者更新，必须与 {U1, U2, ..., Ui} 完全一致。
  • 解绑安全：设 uo 是任意一个解绑操作，它从执行一笔解绑交易开始， 并在返还对应质押时完成； 设 U(uo) 是由发起 uo 导致的验证者更新； 设 vsc(uo) 是包含 U(uo) 的 VSC。 则：
    • （解绑发起）提供者 CCV 模块在接收到 U(uo) 之前，必须已收到 uo 发起的通知；
    • （解绑完成）在提供者链从所有消费者链都登记了 vsc(uo) 成熟的通知之前，uo 不得在提供者链上完成。
    注意：根据具体实现，对于验证者解绑操作，解绑安全中的（解绑发起）部分可能并非必要。
  • 罚没担保：如果提供者 ABCI 应用（例如罚没模块）收到一个请求，要对区块高度 h 发生不当行为的验证者 val 进行罚没，那么它应罚没 val 在高度 h 时所绑定的代币数量，但已经完全解绑的部分除外。
  • 证据提供：如果消费者 ABCI 应用在区块高度 h 收到一份有效的不当行为证据，那么它必须在同一高度 h 将该证据恰好一次提交给消费者 CCV 模块。 此外，消费者 ABCI 应用不得向消费者 CCV 模块提交无效证据。
    注意：何谓有效的不当行为证据取决于不当行为的类型，这超出了本规范的范围。
  • 分配担保：提供者 ABCI 应用（例如分配模块）会将分配模块账户中的代币分发给属于验证者集合的验证者。

​
期望属性

以下属性关注的是一条提供者链为多条消费者链提供安全性的场景。 在提供者链与每条消费者链之间，都会建立一条独立的（唯一的）CCV 通道。
注意：除活性属性之外，即 通道活性、应用 VSC 活性、登记成熟活性 和 分配活性，CCV 的其他属性都不要求正确中继器假设成立。 尽管如此，要保证系统属性（验证者集合复制除外）即 基于绑定的消费者投票权、可罚没的消费者不当行为 和 消费者奖励分配，仍然需要正确中继器假设。

​
系统属性

↑ 返回大纲 我们使用以下记号：
  • ts(h) 是高度为 h 的区块的时间戳，即 ts(h) = B.currentTimestamp()，其中 B 是高度为 h 的区块；
  • pBonded(h,val) 是验证者 val 在提供者链上、区块高度为 h 时质押的代币数量；
  • pUnbonding(h,val) 是验证者 val 在提供者链上、区块高度为 h 时开始解除质押的代币数量；
  • VP(T) 是与 T 个代币对应的投票权；
  • Power(c,h,val) 是在链 c 的区块高度 h 时授予验证者 val 的投票权；
  • Token(power) 是验证者为了获得 power 投票权而必须在提供者链上质押的代币数量， 即 Token(VP(T)) = T；
  • slash(val, h, hi, sf) 是在提供者链上（即 pc）于高度 h 对验证者 val 扣罚的代币数量，该扣罚对应于其在（提供者链）高度 hi 提交的一次违规行为（罚没比例为 sf）， 即 slash(val, h, hi, sf) = sf * Token(Power(pc,hi,val))； 注意，违规行为也可能发生在消费者链上，此时 hi 是其在提供者链上的对应高度。
此外，我们使用 ha << hb 表示高度之间的一种顺序关系，即高度为 ha 的区块先于高度为 hb 的区块发生。 对于同一条链上的高度，<< 等价于 <，即 ha << hb 蕴含 hb 大于 ha。 对于两条不同链上的高度，<< 由两条链之间通过有序通道发送的数据包建立， 即如果链 A 在高度 ha 向链 B 发送一个数据包，而 B 在高度 hb 接收到它，则有 ha << hb。
注意：<< 是可传递的，即 ha << hb 且 hb << hc 蕴含 ha << hc。 注意：在提议链上处理用于创建新消费者链 cc 的治理提案的那个区块，先于 cc 的所有区块发生。
CCV 提供以下系统属性。
  • 验证者集合复制：任何消费者链上的每一个验证者集合，都必须是或曾经是提供者链上的某个验证者集合。
  • 基于质押的消费者链投票权：设 val 是一个验证者，cc 是一条消费者链，hc 和 hc' 都是 cc 上的高度，hp 和 hp' 都是提供者链上的高度，且满足：
    • val 在 cc 的高度 hc 上拥有 Power(cc,hc,val) 投票权；
    • hc' 是 cc 上满足 ts(hc') >= ts(hc) + UnbondingPeriod 的最小高度，即 val 在 hc' 之前不能在 cc 上完全解除质押；
    • hp 是提供者链上满足 hp << hc 的最大高度，即 Power(pc,hp,val) = Power(cc,hc,val)，其中 pc 是提供者链；
    • hp' 是提供者链上满足 hc' << hp' 的最小高度，即 val 在 hp' 之前不能在提供者链上完全解除质押；
    • sumUnbonding(hp, h, val) 是 val 在提供者链上于所有高度 hu 开始解除质押且在高度 h 时仍处于解除质押中的代币总和，其中 hp < hu <= h
    • sumSlash(hp, h, val) 是 val 在所有高度 hs 上、针对发生于 hp 的违规行为所产生的罚没总和，其中 hp < hs <= h。
    那么对于提供者链上的所有高度 h， 
    hp <= h < hp': 
Power(cc,hc,val) <= VP( pBonded(h,val) + sumUnbonding(hp, h, val) + sumSlash(hp, h, val) )
    注意：上述不等式中之所以有 + sumUnbonding(hp, h, val)，是因为 val 在 hp 之后开始解除质押的代币，已经参与形成了其在 cc 的高度 hc 上获得的投票权（即 Power(cc,hc,val)）。 因此，这些代币在 hp' 之前都应可被罚没。 注意：上述不等式中之所以有 + sumSlash(hp, h, val)，是因为对 val 的罚没会减少其锁定的代币（即 pBonded(h,val) 和 sumUnbonding(hp, h, val)），但不会减少它在 cc 的高度 hc 上已经获得的投票权（即 Power(cc,hc,val)）。 直观理解：基于质押的消费者链投票权属性确保，在消费者链上执行验证的验证者，在提供者链上有足够数量的代币被质押，并且质押时间足够长，从而使安全模型成立。 这意味着，如果验证者在消费者链上作恶，那么在解绑期内，其在提供者链上质押的代币可以被罚没。 例如，如果 1 个单位的投票权需要 1.000.000 个已质押代币（即 VP(1.000.000)=1）， 那么一个在消费者链上获得 1 个单位投票权的验证者，必须至少在提供者链上保持 1.000.000 个代币处于质押状态，直到消费者链上的解绑期结束。 注意：当一条现有链成为消费者链时（参见通道初始化：现有链），现有的验证者集合会被提供者验证者集合替换。 出于安全考虑，现有验证者集合已质押的权益必须保持质押状态，直到解绑期结束。 因此，现有的 Staking 模块必须至少保留到解绑期结束。
  • 可罚没的消费者链作恶行为：如果验证者 val 在消费者链 cc 的区块高度 hi 发生一次违规行为，罚没比例为 sf， 那么任何在 cc 的高度 he 被接收到的作恶证据，只要满足 ts(he) < ts(hi) + UnbondingPeriod， 就必须在提供者链上恰好罚没 sf*Token(Power(cc,hi,val)) 数量的代币。 此外，对于同一次作恶行为，val 必须不能被重复罚没。
    **注意：**不同于单链验证，在 CCV 中，即使作恶证据是在满足 ts(he) >= ts(hi) + UnbondingPeriod 的高度 he 才被接收，sf*Token(Power(cc,hi,val)) 这些代币也可以被罚没， 因为解除质押操作需要在提供者链和所有消费者链上都达到成熟状态。 注意： 可罚没的消费者链作恶行为属性还确保，如果某个委托人在高度 hi 之前就开始从 val 解除质押数量为 x 的代币，那么这 x 不会被罚没，因为 x 不属于 Token(Power(c,hi,val)) 的一部分。
  • 消费者链奖励分配：如果一条消费者链向提供者链发送了数量为 T 的代币，作为提供安全性的奖励，那么
    • 与 T 等值的代币必须最终在提供者链上铸造出来，并分配给属于验证者集合的验证者；
    • 代币总供应量必须保持不变，即这 T 个（原始）代币会在消费者链上被托管。

​
CCV 通道

↑ 返回大纲
  • 通道唯一性：提供者链与某条消费者链之间的通道必须是唯一的。
  • 通道有效性：如果某个数据包 P 被 CCV 通道的一端接收，那么 P 必须是由通道另一端发送的。
  • 通道顺序性：如果数据包 P1 先于数据包 P2 通过某条 CCV 通道发送，那么通道另一端在接收到 P1 之前，绝不能先接收到 P2。
  • 通道活性：通过 CCV 通道发送的每一个数据包，最终都必须被通道另一端接收。

​
验证者集合、验证者更新与 VSC

↑ 返回大纲 在本节中，我们将简要讨论在多链上下文中，验证者集合、验证者更新以及 VSC 之间的关系。 每条链都由一系列区块组成。 每个区块结束时，验证者更新（即验证者投票权的变化）会导致下一个区块的验证者集合发生变化。 因此，区块序列会产生一个验证者更新序列和一个验证者集合序列。 此外，提供者链上的验证者更新序列会为所有消费者链产生一个 VSC 序列。 理想情况下，每条消费者链都会应用这个 VSC 序列，从而得到与提供者链相同的验证者集合序列。 然而，一般情况下并不一定如此。原因有两个：
  • 首先，对于任意两条链 A 和 B，我们不能假设 A 产生新区块的速度与 B 相同 （即，我们认为任意两条链的区块序列是完全异步的）；
  • 其次，由于中继延迟，我们不能假设发送 VSC 的速率与接收 VSC 的速率一致。
因此，消费者链有可能在同一个区块内接收到多个 VSC，并在该区块结束时将它们一并应用， 即通过仅保留每个验证者的最新更新来对这些 VSC 中的验证者更新进行聚合。 其结果是，提供者链上的某些验证者集合并不会出现在所有消费者链上。 换句话说，每条消费者链上的验证者集合构成了提供者链验证者集合的一个子序列。 尽管如此，作为 CCV 的一项要求，提供者链上的所有验证者更新都必须包含在所有消费者链的验证者集合序列中。 之所以可行，是因为每个验证者更新都包含该验证者的绝对投票权。 对于某个验证者 val，针对 val 的验证者更新序列（即 val 的投票权更新序列）是 val 投票权相对变化序列的前缀和。 因此，给定一个在区块高度 h 发生、针对 val 的验证者更新 U， U 会汇总截至高度 h 发生的 val 投票权的所有相对变化， 即 U = c_1+c_2+...+c_i，其中 c_i 是在 h 之前发生的最后一次相对变化。 注意，相对变化是整数值。 因此，CCV 可以依赖以下属性：
  • 验证者更新包含性：设 U1 和 U2 是两个针对同一验证者 val 的验证者更新。 如果 U1 先于 U2 发生，那么 U2 会汇总 U1 已经汇总的 val 投票权的所有变化，即：
    • U1 = c_1+c_2+...+c_i，且
    • U2 = c_1+c_2+...+c_i+c_(i+1)+...+c_j。
验证者更新包含性属性使 CCV 能够聚合多个 VSC。 消费者链只需对每个验证者应用最后一次更新即可。 由于某个验证者的最后一次更新包含了该验证者此前的所有更新，因此一旦它被应用，之前的所有更新也就都被应用了。

​
Staking 模块接口

↑ 返回大纲 以下属性定义了 CCV 如何基于提供者链上的验证者更新，向消费者链提供 VSC 的保证。
  • 验证者更新到 VSC 的有效性：提供给消费者链的每一个 VSC，都只能包含那些已经应用到提供者链验证者集合中的验证者更新（即，由提供者链上已质押代币数量变化所产生的更新）。
  • 验证者更新到 VSC 的顺序性：设 U1 和 U2 是提供者链上的两个验证者更新。如果 U1 先于 U2 发生，那么在某个被提供的 VSC 中包含 U2 之前，必须已经包含 U1。注意，单个 VSC 内部的顺序并不重要。
  • 验证者更新到 VSC 的活性：提供者链验证者集合中每个验证者的每一次更新，最终都必须被包含到提供给所有消费者链的某个 VSC 中。
注意，作为 验证者更新到 VSC 的活性 属性的结果，CCV 还保证以下属性：
  • 提供 VSC 的一致性：如果提供者链向某条消费者链提供了一个 VSC，那么它最终也必须向所有消费者链提供该 VSC。

​
验证者集合更新

↑ 返回大纲 向消费者链提供 VSC 的提供者链有两个期望结果：消费者链应用这些 VSC；以及提供者链从每条消费者链登记 VSC 成熟通知。 因此，为了表述清晰，我们将 VSC 的属性分为两类：消费者链上应用由提供者链提供的 VSC 的属性；以及提供者链上登记 VSC 成熟通知的属性。 为简单起见，我们聚焦于单条消费者链。 以下属性定义了 CCV 对消费者链上应用由提供者链提供的 VSC 的保证。
  • 应用 VSC 有效性：消费者链应用的每个 VSC 都 MUST 是由提供者链提供的。
  • 应用 VSC 顺序：如果提供者链先提供一个 VSC vsc1，后提供另一个 VSC vsc2，则消费者链 MUST NOT 先于 vsc1 中包含的验证者更新去应用 vsc2 中包含的验证者更新。
  • 应用 VSC 活性：如果提供者链提供了一个 VSC vsc，则消费者链 MUST 最终应用 vsc 中包含的所有验证者更新。
以下属性定义了 CCV 对提供者链上登记由提供者链提供给消费者链的 VSC 的成熟通知（来自消费者链）的保证。
  • 登记成熟有效性：如果提供者链登记了一条来自消费者链的 VSC 成熟通知，则提供者链 MUST 已经向该消费者链提供过该 VSC。
  • 登记成熟时效性：自消费者链应用某个 VSC vsc 起，在消费者链上的 UnbondingPeriod 尚未经过之前，提供者链 MUST NOT 登记该 vsc 的成熟通知。
  • 登记成熟顺序：如果某个 VSC vsc1 由提供者链先于另一个 VSC vsc2 提供，则提供者链 MUST NOT 先登记 vsc2 的成熟通知，再登记 vsc1 的成熟通知。
  • 登记成熟活性：如果提供者链向消费者链提供了一个 VSC vsc，则提供者链 MUST 最终登记来自消费者链的 vsc 成熟通知。

​
消费者发起的惩罚

↑ 返回大纲
  • 消费者惩罚保证：设 cc 是一条消费者链，其 CCV 模块在高度 he 收到证据，证明验证者 val 在 cc 上于高度 hi 发生了不当行为。 设 hv 为 cc 的 CCV 模块从提供者 CCV 模块接收到第一个 VSC 的高度，即 CCV 通道建立时的高度。 则 cc 的 CCV 模块 MUST 向提供者 CCV 模块发送恰好一个 SlashPacket P，满足
    • P 在高度 h = max(he, hv) 发送；
    • P.val = val 且 P.id = HtoVSC[hi]， 即在高度 hi 时于 cc 上最近一次更新验证者集合的 VSC 的 ID；如果不存在这样的 VSC（即 hi < hv），则为 0。
    注意：消费者惩罚保证属性的一个结果是，消费者链上的初始验证者集合在 CCV 通道初始化期间无法被惩罚。 因此，消费者链 SHOULD NOT allow user transactions before the CCV channel is established。 注意，一旦 CCV 通道建立（即从提供者 CCV 模块接收到一个 VSC），CCV 就能够对通道初始化期间发生违规的初始验证者集合执行惩罚。
  • 提供者惩罚保证：如果提供者 CCV 模块从消费者链 cc 收到一个 SlashPacket，其中包含验证者 val 和一个 VSC ID vscId， 则它 MUST 向提供者 Slashing 模块发起恰好一次请求，以在高度 h 对 val 的不当行为执行惩罚，其中
    • 如果 vscId = 0，则 h 是提供者链向 cc 建立 CCV 通道时所在区块的高度；
    • 否则，h 是提供者链向 cc 提供 ID 为 vscId 的 VSC 所在区块之后紧接着的那个区块的高度。
    此外，提供者 CCV 模块 MUST 在登记来自 cc 且在该 SlashPacket 之后收到的任何成熟通知之前，先发起这次惩罚请求。
  • VSC 成熟与惩罚顺序：如果消费者链先向提供者链发送一个 SlashPacket，后发送某个 VSC 的成熟通知，则提供者链 MUST NOT 在收到该 SlashPacket 之前收到该成熟通知。
    注意：VSC 成熟与惩罚顺序要求 VSC 成熟通知通过它们各自独立的 IBC 数据包发送（即 VSCMaturedPacket），而不是例如通过 VSCPacket 的确认消息发送。

​
奖励分配

↑ 返回大纲
  • 分配活性：如果消费者链上的 CCV 模块向提供者链上的分配模块账户发送数量为 T 的代币，作为提供安全性的奖励，则最终会在提供者链上的分配模块账户中铸造出 T 个（等值）代币。

​
正确性推理

↑ 返回大纲 在本节中，我们论证 技术规范 中描述的 CCV 协议的正确性， 即，我们对上一节中描述的性质给出非形式化证明。
  • 通道唯一性：当消费者链上的 CCV 模块接收到第一个成功执行的 ChanOpenAck 消息时，CCV 通道在消费者链一侧建立；之后所有的 ChanOpenAck 消息都会失败（参见 Safe Blockchain）。 设 ccvChannel 表示该通道。那么，ccvChannel 是唯一一个可连接到由消费者 CCV 模块拥有的端口的 OPEN 通道。 当提供者链上的 CCV 模块接收到第一个成功执行的 ChanOpenConfirm 消息时，CCV 通道在提供者链一侧建立；之后所有的 ChanOpenConfirm 消息都会失败（参见 Safe Blockchain）。 ccvChannel 是唯一一个可以成功执行 ChanOpenConfirm 的通道（参见 Safe Blockchain，即 IBC 通道打开握手保证）。 因此，ccvChannel 是唯一的。 此外，其存在性由 Correct Relayer 假设保证。
  • 通道有效性：直接由 Safe Blockchain 假设推出。
  • 通道有序性：提供者链在接收 ChanOpenTry 消息时只接受有序通道（参见 Safe Blockchain）。 类似地，消费者链在接收 ChanOpenInit 消息时也只接受有序通道（参见 Safe Blockchain）。 因此，该性质直接由 CCV 通道是有序通道这一事实推出。
  • 通道活性：该性质由 Correct Relayer 假设推出。
  • 从验证者更新到 VSC 的有效性：提供者 CCV 模块只会提供包含从 Staking 模块获得的验证者更新的 VSC， 即，通过调用 GetValidatorUpdates() 方法获得（参见 Safe Blockchain）。 此外，这些验证者更新已被应用到提供者链的验证者集合中（参见 Validator Update Provision）。
  • 从验证者更新到 VSC 的顺序性：我们通过反证法证明该性质。 给定两个验证者更新 U1 和 U2，其中 U1 在提供者链上先于 U2 发生，我们假设 U2 在某个已提供的 VSC 中先于 U1 被包含。 然而，提供者 CCV 模块不可能先于 U1 获得 U2（参见 Validator Update Provision）。 因此，提供者 CCV 模块不可能先提供包含 U2 的 VSC，再提供包含 U1 的 VSC（参见 Safe Blockchain），这与初始假设矛盾。
  • 从验证者更新到 VSC 的活性：提供者 CCV 模块最终会向所有消费者链提供包含从提供者 Staking 模块获得的全部验证者更新的 VSC（参见 Safe Blockchain、Life Blockchain）。 因此，只需证明：提供者链验证者集合中任一验证者的每次更新最终都必然能从提供者 Staking 模块中获得。 我们通过反证法证明这一点。给定一个验证者更新 U，它在高度为 h 的区块 B 结束时被应用到提供者链的验证者集合中，我们假设提供者 CCV 模块永远不会获得 U。 然而，在高度 h，提供者 CCV 模块会尝试从提供者 Staking 模块获取新一批验证者更新（参见 Safe Blockchain）。 因此，这批验证者更新必然包含所有在区块 B 结束时应用到提供者链验证者集合中的验证者更新，包括 U（参见 Validator Update Provision），这与初始假设矛盾。
  • 应用 VSC 的有效性：该性质由以下两个断言推出。
    • 消费者链只会通过 CCV 通道，对在 VSCPacket 中接收到的 VSC 进行应用（参见 Safe Blockchain）。
    • 提供者链只会发送包含已提供 VSC 的 VSCPacket（参见 Safe Blockchain）。
  • 应用 VSC 的顺序性：我们通过反证法证明该性质。 给定两个 VSC vsc1 和 vsc2，且提供者链先提供 vsc1 再提供 vsc2，我们假设消费者链先应用 vsc2 中包含的验证者更新，再应用 vsc1 中包含的验证者更新。 以下断言序列将导出矛盾。
    • 提供者链不可能先发送包含 vsc2 的 VSCPacket P2，再发送包含 vsc1 的 VSCPacket P1（参见 Safe Blockchain）。
    • 消费者链不可能先接收到 P2，再接收到 P1（参见 Channel Order）。
    • 在 Safe Blockchain 假设下，我们区分两种情况。
      • 第一种情况，消费者链在区块 B1 中接收 P1，并在区块 B2 中接收 P2（其中 B1 < B2）。 那么，它会在 B1 结束时应用 vsc1 中包含的验证者更新，并在 B2 结束时应用 vsc2 中包含的验证者更新（参见 Validator Update Inclusion），这与初始假设矛盾。
      • 第二种情况，消费者链在同一个区块中同时接收 P1 和 P2。 那么，它会在该区块结束时应用 vsc1 和 vsc2 中包含的全部验证者更新。 因此，它不可能先应用 vsc2 中包含的验证者更新。
  • 应用 VSC 的活性：提供者链最终会通过 CCV 通道发送一个包含 vsc 的 VSCPacket（参见 Safe Blockchain、Life Blockchain）。 因此，消费者链最终会接收到该数据包（参见 Channel Liveness）。 随后，消费者链会在区块结束时聚合所有接收到的 VSC，并应用所有聚合后的更新（参见 Safe Blockchain、Life Blockchain）。 因此，消费者链会应用 vsc 中的全部验证者更新（参见 Validator Update Inclusion）。
  • 注册成熟度的有效性：该性质由以下断言序列推出。
    • 提供者链只有在通过 CCV 通道接收到通知这些 VSC 已成熟的 VSCMaturedPacket 时，才会注册 VSC 成熟通知（参见 Safe Blockchain）。
    • 提供者链在 CCV 通道上只会接收到由消费者链发送的数据包（参见 Channel Validity）。
    • 消费者链只会发送与其在 CCV 通道上收到的 VSCPacket 相匹配的 VSCMaturedPacket（参见 Safe Blockchain）。
    • 消费者链在 CCV 通道上只会接收到由提供者链发送的数据包（参见 Channel Validity）。
    • 提供者链只会发送包含已提供 VSC 的 VSCPacket（参见 Safe Blockchain）。
  • 注册成熟度的及时性：我们通过反证法证明该性质。 给定一个由提供者链提供给消费者链的 VSC vsc，我们假设自消费者链应用 vsc 起，在消费者链上的 UnbondingPeriod 尚未过去之前，提供者链就注册了 vsc 的成熟通知。 以下断言序列将导出矛盾。
    • 提供者链不可能在通过 CCV 通道接收到满足 P.id = vsc.id 的 VSCMaturedPacket P 之前，就注册 vsc 的成熟通知（参见 Safe Blockchain）。
    • 提供者链不可能在消费者链发送 P 之前，就通过 CCV 通道接收到 P（参见 Channel Validity）。
    • 消费者链不可能在自通过 CCV 通道接收到满足 P'.id = P.id 的 VSCPacket P' 起至少经过 UnbondingPeriod 之前发送 P（参见 Safe Blockchain）。 注意，由于时间以区块时间度量，因此接收 P' 的时间与应用 vsc 的时间相同。
    • 消费者链不可能在提供者链发送 P' 之前，就通过 CCV 通道接收到 P'（参见 Channel Validity）。
    • 提供者链不可能在提供 vsc 之前发送 P'。
    • 由于通过 CCV 通道发送数据包所需的时长不可能为负，因此，自消费者链应用 vsc 起，在消费者链上的 UnbondingPeriod 尚未过去之前，提供者链不可能就注册 vsc 的成熟通知。
  • 注册成熟度的顺序性：我们通过反证法证明该性质。给定两个 VSC vsc1 和 vsc2，且提供者链先提供 vsc1 再提供 vsc2，我们假设提供者链先注册 vsc2 的成熟通知，再注册 vsc1 的成熟通知。 以下断言序列将导出矛盾。
    • 提供者链不可能先发送 VSCPacket P2（其中 P2.updates = C2），再发送 VSCPacket P1（其中 P1.updates = C1）（参见 Safe Blockchain）。
    • 消费者链不可能先接收 P2，再接收 P1（参见 Channel Order）。
    • 消费者链不可能先发送 VSCMaturedPacket P2'（其中 P2'.id = P2.id），再发送 VSCMaturedPacket P1'（其中 P1'.id = P1.id）（参见 Safe Blockchain）。
    • 提供者链不可能先接收 P2'，再接收 P1'（参见 Channel Order）。
    • 提供者链不可能先注册 vsc2 的成熟通知，再注册 vsc1 的成熟通知（参见 Safe Blockchain）。
  • 注册成熟度的活性：该性质由以下断言序列推出。
    • 提供者链最终会在 CCV 通道上发送 VSCPacket P，其中 P.updates = C（参见 Safe Blockchain、Life Blockchain）。
    • 消费者链最终会在 CCV 通道上接收到 P（参见 Channel Liveness）。
    • 消费者链最终会在 CCV 通道上发送 VSCMaturedPacket P'，其中 P'.id = P.id（参见 Safe Blockchain、Life Blockchain）。
    • 提供者链最终会在 CCV 通道上接收到 P'（参见 Channel Liveness）。
    • 提供者链最终会注册 vsc 的成熟通知（参见 Safe Blockchain、Life Blockchain）。
  • 消费者惩罚保障：直接由 Safe Blockchain 推出。
  • 提供者惩罚保障：直接由 Safe Blockchain 推出。
  • VSC 成熟度与惩罚顺序：直接由 Channel Order 推出。
  • 分发活性：消费者链上的 CCV 模块会通过 IBC 代币转账数据包向提供者链发送数量为 T 的代币（定义见 ICS 20）。 因此，如果该数据包在超时时间内被中继，那么提供者链上就会铸造 T 个（等值）代币。 否则，这 T 个代币会退还给消费者 CCV 模块账户。 在这种情况下，这 T 个代币将成为下一个代币转账数据包的一部分。 最终，正确的中继者会中继一个包含这 T 个代币的代币转账数据包（参见 Correct Relayer、Life Blockchain）。 因此，提供者链上最终会铸造 T 个（等值）代币。
  • 验证者集合复制：该性质由 Safe Blockchain 假设以及 Apply VSC Validity 和 Validator Update To VSC Validity 两个性质共同推出。
  • 基于质押的消费者投票权：hp 的存在性由构造方式给出，即，提议者链上处理治理提案以生成新消费者链 cc 的区块，先于 cc 的所有区块发生。 hc' 和 hp' 的存在性由 Life Blockchain 和 Channel Liveness 给出。 为了证明 Bond-Based Consumer Voting Power 性质，我们使用如下一个直接来源于协议设计的性质（参见 Safe Blockchain、Life Blockchain）。
    • Property1：设 val 是一个验证者；设 Ua 和 Ub 是 val 的两个更新，它们由消费者链 cc 分别在区块高度 ha 和 hb 处依次应用（即，中间没有应用 val 的其他更新）。 那么，对所有满足 ha <= h < hb 的区块高度 h，都有 Power(cc,ha,val) = Power(cc,h,val)（即，在 ts(ha) 与 ts(hb) 之间这段期间内，cc 赋予 val 的投票权保持不变）。
我们通过反证法证明 基于质押的消费者投票权 性质。 我们假设在提供者链上、hp 与 hp' 之间存在某个高度 h，使得 Power(cc,hc,val) > VP( pBonded(h,val) + sumUnbonding(hp, h, val) + sumSlash(hp, h, val) )。 下面这组断言将导出矛盾。
  • 设 U1 为 val 的最新一次更新，该更新在区块高度 hc 之前或不晚于该高度被 cc 应用 （即，U1 是为 val 设置 Power(cc,hc,val) 的更新）。 设 hp1 为 U1 在提供者链上发生的高度；设 hc1 为 U1 在 cc 上被应用的高度。 则，hp1 << hc1 <= hc、hp1 <= hp，且 Power(cc,hc,val) = Power(cc,hc1,val) = VP(pBonded(hp1,val))。 这意味着，val 在高度 hp1 质押的部分代币，已在高度 hp' 之前或不晚于该高度被完全解除质押（参见 Power(cc,hc,val) > VP( pBonded(h,val) + sumUnbonding(hp, h, val) + sumSlash(hp, h, val) )）。
  • 设 uo 为第一个此类解除质押操作，它在提供者链的高度 hp2 发起，且满足 hp1 < hp2 <= hp'。 注意，在高度 hp2，由 uo 解除质押的代币属于 pUnbonding(hp2,val)。 设 U2 为因发起 uo 而导致的验证者更新。 设 hc2 为 U2 在 cc 上被应用的高度；显然，Power(cc,hc2,val) < Power(cc,hc,val)。 注意，hc2 的存在性由 验证者更新到 VSC 活性 和 应用 VSC 活性 保证。 则，hc2 > hc1（参见 hp2 > hp1、验证者更新到 VSC 顺序、应用 VSC 顺序）。
  • 对所有满足 hc1 <= h < hc2 的高度 h，都有 Power(cc,hc,val) = Power(cc,hc1,val) = Power(cc,h,val)（参见 性质1）。 因此，hc2 > hc（参见 Power(cc,hc2,val) < Power(cc,hc,val)）。
  • uo 不可能在 ts(hc2) + UnbondingPeriod 之前完成，这意味着它不可能在 hc' 之前完成，因此也不可能在 hp' 之前完成（参见 hc' << hp'）。
  • 可罚没的消费者不当行为：可罚没的消费者不当行为 性质的第二部分（即，val 不会因同一不当行为被罚没超过一次）可直接由 证据提供、通道有效性、消费者罚没保证、提供者罚没保证 推出。 为了证明 可罚没的消费者不当行为 性质的第一部分（即，在提供者链上恰好罚没数量为 sf*Token(Power(cc,hi,val)) 的代币），我们考虑如下陈述序列。
    • cc 的 CCV 模块在高度 he 收到 val 在 cc 的高度 hi 发生不当行为的证据（参见 证据提供、安全区块链、活区块链）。
    • 设 hv 为 cc 的 CCV 模块收到来自提供者 CCV 模块的第一个 VSC 的高度。 则，cc 的 CCV 模块会在高度 h = max(he, hv) 向提供者链发送一个 SlashPacket P，满足 P.val = val 且 P.id = HtoVSC[hi]（参见 消费者罚没保证）。
    • 提供者 CCV 模块最终会收到 P（参见 通道活性）。
    • 提供者 CCV 模块会在处理来自 cc 的 CCV 模块的任何后续成熟度通知之前，请求提供者 Slashing 模块对 val 在高度 hp = VSCtoH[P.id] 的不当行为执行罚没（参见 提供者罚没保证）。
    • 提供者 Slashing 模块会罚没 val 在高度 hp 已质押的代币数量，但不包括已经完全解除质押的部分（参见 罚没保证）。
    因此，剩下需要证明的是 Token(Power(cc,hi,val)) = pBonded(hp,val)，其中 hp = VSCtoH[HtoVSC[hi]]。我们区分两种情况：
    • HtoVSC[hi] != 0，这意味着根据定义，HtoVSC[hi] 是最后一个更新 Power(cc,hi,val) 的 VSC 的 ID。 同样根据定义，这个 VSC 包含了提供者链在高度 VSCtoH[HtoVSC[hi]] 上对投票权的最后一次更新。 因此，Token(Power(cc,hi,val)) = pBonded(hp,val)。
    • HtoVSC[hi] == 0，这意味着根据定义，Power(cc,hi,val) 是在通道初始化期间于创世时设置的。 同样根据定义，这与向该消费者链提供第一个 VSC 时对应的提供者链区块的投票权相同，即 VSCtoH[HtoVSC[hi]]。 因此，Token(Power(cc,hi,val)) = pBonded(hp,val)。
  • 消费者奖励分配：消费者奖励分配 性质的第一部分（即，代币最终会在提供者链上铸造，然后在验证者之间分配）可直接由 分配活性 和 分配保证 推出。 消费者奖励分配 性质的第二部分（即，代币总供应量保持不变）可直接由同质化代币转移协议的 供应量 性质推出（参见 ICS 20）。

​
Outline

​
Assumptions

↑ Back to Outline As part of a modular ABCI application, CCV interacts with both the consensus engine (via ABCI) and other application modules (e.g, the Staking module). As an IBC application, CCV interacts with external relayers (defined in ICS 18). In this section we specify what we assume about these other components. A more thorough discussion of the environment in which CCV operates is given in the section Placing CCV within an ABCI Application.
Intuition: CCV safety relies on the Safe Blockchain assumption, i.e., neither Live Blockchain and Correct Relayer are required for safety. Note though that CCV liveness relies on both Live Blockchain and Correct Relayer assumptions; furthermore, the Correct Relayer assumption relies on both Safe Blockchain and Live Blockchain assumptions. The Validator Update Provision, Unbonding Safety, Slashing Warranty, and Distribution Warranty assumptions define what is needed from the ABCI application of the provider chain. The Evidence Provision assumptions defines what is needed from the ABCI application of the consumer chains.
  • Safe Blockchain: Both the provider and the consumer chains are safe. This means that, for every chain, the underlying consensus engine satisfies safety (e.g., the chain does not fork) and the execution of the state machine follows the described protocol.
  • Live Blockchain: Both the provider and the consumer chains are live. This means that, for every chain, the underlying consensus engine satisfies liveness (i.e., new blocks are eventually added to the chain).
    Note: Both Safe Blockchain and Live Blockchain assumptions require the consensus engine’s assumptions to hold, e.g., less than a third of the voting power is Byzantine. For an example, take a look at the Tendermint Paper.
  • Correct Relayer: There is at least one correct, live relayer between the provider and consumer chains. This assumption has the following implications.
    • The opening handshake messages on the CCV channel are relayed before the Channel Initialization subprotocol times out (see initTimeout).
    • Every packet sent on the CCV channel is relayed to the receiving end before the packet timeout elapses (see both vscTimeout and ccvTimeoutTimestamp).
    • A correct relayer will eventually relay packets on the token transfer channel.
    Clearly, the CCV protocol is responsible of setting the timeouts (see ccvTimeoutTimestamp, vscTimeout, initTimeout in the CCV State), such that the Correct Relayer assumption is feasible.
    Discussion: IBC relies on timeouts to signal that a sent packet is not going to be received on the other end. Once an ordered IBC channel timeouts, the channel is closed (see ICS 4). The Correct Relayer assumption is necessary to ensure that the CCV channel cannot ever timeout and, as a result, cannot transit to the closed state. In practice, the Correct Relayer assumption is realistic since any validator could play the role of the relayer and it is in the best interest of correct validators to successfully relay packets. The following strategy is a practical example of how to ensure the Correct Relayer assumption holds. Let S denote the sending chain and D the destination chain; and let drift(S,D) be the time drift between S and D, i.e., drift(S,D) = S.currentTimestamp() - D.currentTimestamp() (drift(S,D) > 0 means that S is “ahead” of D). For every packet, S only sets timeoutTimestamp = S.currentTimestamp() + to, with to an application-level parameter. The timeoutTimestamp indicates a timestamp on the destination chain after which the packet will no longer be processed (cf. ICS 4). Therefore, the packet MUST be relayed within a time period of to - drift(S,D), i.e., to - drift(S,D) > RTmax, where RTmax is the maximum relaying time across all packet. Theoretically, choosing the value of to requires knowing the value of drift(S,D) (i.e., to > drift(S,D)); yet, drift(S,D) is not known at a chain level. In practice, choosing to such that to >> drift(S,D) and to >> RTmax, e.g., to = 4 weeks, makes the Correct Relayer assumption feasible.
  • Validator Update Provision: Let {U1, U2, ..., Ui} be a batch of validator updates applied (by the provider Staking module) to the validator set of the provider chain at block height h. Then, the batch of validator updates obtained (by the provider CCV module) from the provider Staking module at height h MUST be exactly the batch {U1, U2, ..., Ui}.
  • Unbonding Safety: Let uo be any unbonding operation that starts with an unbonding transaction being executed and completes with the event that returns the corresponding stake; let U(uo) be the validator update caused by initiating uo; let vsc(uo) be the VSC that contains U(uo). Then,
    • (unbonding initiation) the provider CCV module MUST be notified of uo’s initiation before receiving U(uo);
    • (unbonding completion) uo MUST NOT complete on the provider chain before the provider chain registers notifications of vsc(uo)’s maturity from all consumer chains.
    Note: Depending on the implementation, the (unbonding initiation) part of the Unbonding Safety MAY NOT be necessary for validator unbonding operations.
  • Slashing Warranty: If the provider ABCI application (e.g., the Slashing module) receives a request to slash a validator val that misbehaved at block height h, then it slashes the amount of tokens val had bonded at height h except the amount that has already completely unbonded.
  • Evidence Provision: If the consumer ABCI application receives a valid evidence of misbehavior at block height h, then it MUST submit it to the consumer CCV module exactly once and at the same height h. Furthermore, the consumer ABCI application MUST NOT submit invalid evidence to the consumer CCV module.
    Note: What constitutes a valid evidence of misbehavior depends on the type of misbehavior and it is outside the scope of this specification.
  • Distribution Warranty: The provider ABCI application (e.g., the Distribution module) distributes the tokens from the distribution module account among the validators that are part of the validator set.

​
Desired Properties

The following properties are concerned with one provider chain providing security to multiple consumer chains. Between the provider chain and each consumer chain, a separate (unique) CCV channel is established.
Note: Except for liveness properties — Channel Liveness, Apply VSC Liveness, Register Maturity Liveness, and Distribution Liveness — none of the properties of CCV require the Correct Relayer assumption to hold. Nonetheless, the Correct Relayer assumption is necessary to guarantee the systems properties (except for Validator Set Replication) — Bond-Based Consumer Voting Power, Slashable Consumer Misbehavior, and Consumer Rewards Distribution.

​
System Properties

↑ Back to Outline We use the following notations:
  • ts(h) is the timestamp of a block with height h, i.e., ts(h) = B.currentTimestamp(), where B is the block at height h;
  • pBonded(h,val) is the number of tokens bonded by validator val on the provider chain at block height h;
  • pUnbonding(h,val) is the number of tokens a validator val starts unbonding on the provider at block height h;
  • VP(T) is the voting power associated to a number T of tokens;
  • Power(c,h,val) is the voting power granted to a validator val on a chain c at block height h;
  • Token(power) is the amount of tokens necessary to be bonded (on the provider chain) by a validator to be granted power voting power, i.e., Token(VP(T)) = T;
  • slash(val, h, hi, sf) is the amount of token slashed from a validator val on the provider chain (i.e., pc) at height h for an infraction (with a slashing fraction of sf) committed at (provider) height hi, i.e., slash(val, h, hi, sf) = sf * Token(Power(pc,hi,val)); note that the infraction can be committed also on a consumer chain, in which case hi is the corresponding height on the provider chain.
Also, we use ha << hb to denote an order relation between heights, i.e., the block at height ha happens before the block at height hb. For heights on the same chain, << is equivalent to <, i.e., ha << hb entails hb is larger than ha. For heights on two different chains, << is establish by the packets sent over an order channel between two chains, i.e., if a chain A sends at height ha a packet to a chain B and B receives it at height hb, then ha << hb.
Note: << is transitive, i.e., ha << hb and hb << hc entail ha << hc. Note: The block on the proposer chain that handles a governance proposal to spawn a new consumer chain cc happens before all the blocks of cc.
CCV provides the following system properties.
  • Validator Set Replication: Every validator set on any consumer chain MUST either be or have been a validator set on the provider chain.
  • Bond-Based Consumer Voting Power: Let val be a validator, cc be a consumer chain, both hc and hc' be heights on cc, and both hp and hp' be heights on the provider chain, such that
    • val has Power(cc,hc,val) voting power on cc at height hc;
    • hc' is the smallest height on cc that satisfies ts(hc') >= ts(hc) + UnbondingPeriod, i.e., val cannot completely unbond on cc before hc';
    • hp is the largest height on the provider chain that satisfies hp << hc, i.e., Power(pc,hp,val) = Power(cc,hc,val), where pc is the provider chain;
    • hp' is the smallest height on the provider chain that satisfies hc' << hp', i.e., val cannot completely unbond on the provider chain before hp';
    • sumUnbonding(hp, h, val) is the sum of all tokens of val that start unbonding on the provider at all heights hu and are still unbonding at height h, such that hp < hu <= h
    • sumSlash(hp, h, val) is the sum of the slashes of val at all heights hs for infractions committed at hp, such that hp < hs <= h.
    Then for all heights h on the provider chain, 
    hp <= h < hp': 
Power(cc,hc,val) <= VP( pBonded(h,val) + sumUnbonding(hp, h, val) + sumSlash(hp, h, val) )
    Note: The reason for + sumUnbonding(hp, h, val) in the above inequality is that tokens that val start unbonding after hp have contributed to the power granted to val at height hc on cc (i.e., Power(cc,hc,val)). As a result, these tokens should be available for slashing until hp'. Note: The reason for + sumSlash(hp, h, val) in the above inequality is that slashing val reduces its locked tokens (i.e., pBonded(h,val) and sumUnbonding(hp, h, val)), however it does not reduce the power already granted to it at height hc on cc (i.e., Power(cc,hc,val)). Intuition: The Bond-Based Consumer Voting Power property ensures that validators that validate on the consumer chains have enough tokens bonded on the provider chain for a sufficient amount of time such that the security model holds. This means that if the validators misbehave on the consumer chains, their tokens bonded on the provider chain can be slashed during the unbonding period. For example, if one unit of voting power requires 1.000.000 bonded tokens (i.e., VP(1.000.000)=1), then a validator that gets one unit of voting power on a consumer chain must have at least 1.000.000 tokens bonded on the provider chain until the unbonding period elapses on the consumer chain. Note: When an existing chain becomes a consumer chain (see Channel Initialization: Existing Chains), the existing validator set is replaced by the provider validator set. For safety, the stake bonded by the existing validator set must remain bonded until the unbonding period elapses. Thus, the existing Staking module must be kept for at least the unbonding period.
  • Slashable Consumer Misbehavior: If a validator val commits an infraction, with a slashing fraction of sf, on a consumer chain cc at a block height hi, then any evidence of misbehavior that is received by cc at height he, such that ts(he) < ts(hi) + UnbondingPeriod, MUST results in exactly the amount of tokens sf*Token(Power(cc,hi,val)) to be slashed on the provider chain. Furthermore, val MUST NOT be slashed more than once for the same misbehavior.
    Note: Unlike in single-chain validation, in CCV the tokens sf*Token(Power(cc,hi,val)) MAY be slashed even if the evidence of misbehavior is received at height he such that ts(he) >= ts(hi) + UnbondingPeriod, since unbonding operations need to reach maturity on both the provider and all the consumer chains. Note: The Slashable Consumer Misbehavior property also ensures that if a delegator starts unbonding an amount x of tokens from val before height hi, then x will not be slashed, since x is not part of Token(Power(c,hi,val)).
  • Consumer Rewards Distribution: If a consumer chain sends to the provider chain an amount T of tokens as reward for providing security, then
    • T (equivalent) tokens MUST be eventually minted on the provider chain and then distributed among the validators that are part of the validator set;
    • the total supply of tokens MUST be preserved, i.e., the T (original) tokens are escrowed on the consumer chain.

​
CCV Channel

↑ Back to Outline
  • Channel Uniqueness: The channel between the provider chain and a consumer chain MUST be unique.
  • Channel Validity: If a packet P is received by one end of a CCV channel, then P MUST have been sent by the other end of the channel.
  • Channel Order: If a packet P1 is sent over a CCV channel before a packet P2, then P2 MUST NOT be received by the other end of the channel before P1.
  • Channel Liveness: Every packet sent over a CCV channel MUST eventually be received by the other end of the channel.

​
Validator Sets, Validator Updates and VSCs

↑ Back to Outline In this section, we provide a short discussion on how the validator set, the validator updates, and the VSCs relates in the context of multiple chains. Every chain consists of a sequence of blocks. At the end of each block, validator updates (i.e., changes in the validators voting power) results in changes in the validator set of the next block. Thus, the sequence of blocks produces a sequence of validator updates and a sequence of validator sets. Furthermore, the sequence of validator updates on the provider chain results in a sequence of VSCs to all consumer chains. Ideally, this sequence of VSCs is applied by every consumer chain, resulting in a sequence of validator sets identical to the one on the provider chain. However, in general this need not be the case. The reason is twofold:
  • first, given any two chains A and B, we cannot assume that A’s rate of adding new block is the same as B’s rate (i.e., we consider the sequences of blocks of any two chains to be completely asynchronous);
  • and second, due to relaying delays, we cannot assume that the rate of sending VSCs matches the rate of receiving VSCs.
As a result, it is possible for multiple VSCs to be received by a consumer chain within the same block and be applied together at the end of the block, i.e., the validator updates within the VSCs are being aggregated by keeping only the latest update per validator. As a consequence, some validator sets on the provider chain are not existing on all consumer chains. In other words, the validator sets on each consumer chain form a subsequence of the validator sets on the provider chain. Nonetheless, as a requirement of CCV, all the validator updates on the provider chain MUST be included in the sequence of validator sets on all consumer chains. This is possible since every validator update contains the absolute voting power of that validator. Given a validator val, the sequence of validator updates targeting val (i.e., updates of the voting power of val) is the prefix sum of the sequence of relative changes of the voting power of val. Thus, given a validator update U targeting val that occurs at a block height h, U sums up all the relative changes of the voting power of val that occur until height h, i.e., U = c_1+c_2+...+c_i, such that c_i is the last relative change that occurs by h. Note that relative changes are integer values. As a consequence, CCV can rely on the following property:
  • Validator Update Inclusion: Let U1 and U2 be two validator updates targeting the same validator val. If U1 occurs before U2, then U2 sums up all the changes of the voting power of val that are summed up by U1, i.e.,
    • U1 = c_1+c_2+...+c_i and
    • U2 = c_1+c_2+...+c_i+c_(i+1)+...+c_j.
The Validator Update Inclusion property enables CCV to aggregate multiple VSCs. It is sufficient for the consumer chains to apply only the last update per validator. Since the last update of a validator includes all the previous updates of that validator, once it is applied, all the previous updates are also applied.

​
Staking Module Interface

↑ Back to Outline The following properties define the guarantees of CCV on providing VSCs to the consumer chains as a consequence of validator updates on the provider chain.
  • Validator Update To VSC Validity: Every VSC provided to a consumer chain MUST contain only validator updates that were applied to the validator set of the provider chain (i.e., resulted from a change in the amount of bonded tokens on the provider chain).
  • Validator Update To VSC Order: Let U1 and U2 be two validator updates on the provider chain. If U1 occurs before U2, then U2 MUST NOT be included in a provided VSC before U1. Note that the order within a single VSC is not relevant.
  • Validator Update To VSC Liveness: Every update of a validator in the validator set of the provider chain MUST eventually be included in a VSC provided to all consumer chains.
Note that as a consequence of the Validator Update To VSC Liveness property, CCV guarantees the following property:
  • Provide VSC uniformity: If the provider chain provides a VSC to a consumer chain, then it MUST eventually provide that VSC to all consumer chains.

​
Validator Set Update

↑ Back to Outline The provider chain providing VSCs to the consumer chains has two desired outcomes: the consumer chains apply the VSCs; and the provider chain registers VSC maturity notifications from every consumer chain. Thus, for clarity, we split the properties of VSCs in two: properties of applying provided VSCs on the consumer chains; and properties of registering VSC maturity notifications on the provider chain. For simplicity, we focus on a single consumer chain. The following properties define the guarantees of CCV on applying on the consumer chain VSCs provided by the provider chain.
  • Apply VSC Validity: Every VSC applied by the consumer chain MUST be provided by the provider chain.
  • Apply VSC Order: If a VSC vsc1 is provided by the provider chain before a VSC vsc2, then the consumer chain MUST NOT apply the validator updates included in vsc2 before the validator updates included in vsc1.
  • Apply VSC Liveness: If the provider chain provides a VSC vsc, then the consumer chain MUST eventually apply all validator updates included in vsc.
The following properties define the guarantees of CCV on registering on the provider chain maturity notifications (from the consumer chain) of VSCs provided by the provider chain to the consumer chain.
  • Register Maturity Validity: If the provider chain registers a maturity notification of a VSC from the consumer chain, then the provider chain MUST have provided that VSC to the consumer chain.
  • Register Maturity Timeliness: The provider chain MUST NOT register a maturity notification of a VSC vsc before UnbondingPeriod has elapsed on the consumer chain since the consumer chain applied vsc.
  • Register Maturity Order: If a VSC vsc1 was provided by the provider chain before another VSC vsc2, then the provider chain MUST NOT register the maturity notification of vsc2 before the maturity notification of vsc1.
  • Register Maturity Liveness: If the provider chain provides a VSC vsc to the consumer chain, then the provider chain MUST eventually register a maturity notification of vsc from the consumer chain.

​
Consumer Initiated Slashing

↑ Back to Outline
  • Consumer Slashing Warranty: Let cc be a consumer chain, such that its CCV module receives at height he evidence that a validator val misbehaved on cc at height hi. Let hv be the height when the CCV module of cc receives the first VSC from the provider CCV module, i.e., the height when the CCV channel is established. Then, the CCV module of cc MUST send (to the provider CCV module) exactly one SlashPacket P, such that
    • P is sent at height h = max(he, hv);
    • P.val = val and P.id = HtoVSC[hi], i.e., the ID of the latest VSC that updated the validator set on cc at height hi or 0 if such a VSC does not exist (if hi < hv).
    Note: A consequence of the Consumer Slashing Warranty property is that the initial validator set on a consumer chain cannot be slashed during the initialization of the CCV channel. Therefore, consumer chains SHOULD NOT allow user transactions before the CCV channel is established. Note that once the CCV channel is established (i.e., a VSC is received from the provider CCV module), CCV enables the slashing of the initial validator set for infractions committed during channel initialization.
  • Provider Slashing Warranty: If the provider CCV module receives from a consumer chain cc a SlashPacket containing a validator val and a VSC ID vscId, then it MUST make exactly one request to the provider Slashing module to slash val for misbehaving at height h, such that
    • if vscId = 0, h is the height of the block when the provider chain established a CCV channel to cc;
    • otherwise, h is the height of the block immediately subsequent to the block when the provider chain provided to cc the VSC with ID vscId.
    Furthermore, the provider CCV module MUST make this slash request before registering any maturity notifications received from cc after the SlashPacket.
  • VSC Maturity and Slashing Order: If a consumer chain sends to the provider chain a SlashPacket before a maturity notification of a VSC, then the provider chain MUST NOT receive the maturity notification before the SlashPacket.
    Note: VSC Maturity and Slashing Order requires the VSC maturity notifications to be sent through their own IBC packets (i.e., VSCMaturedPackets) instead of e.g., through acknowledgements of VSCPackets.

​
Reward Distribution

↑ Back to Outline
  • Distribution Liveness: If the CCV module on a consumer chain sends to the distribution module account on the provider chain an amount T of tokens as reward for providing security, then T (equivalent) tokens are eventually minted in the distribution module account on the provider chain.

​
Correctness Reasoning

↑ Back to Outline In this section we argue the correctness of the CCV protocol described in the Technical Specification, i.e., we informally prove the properties described in the previous section.
  • Channel Uniqueness: The consumer chain side of the CCV channel is established when the consumer CCV module receives the first ChanOpenAck message that is successfully executed; all subsequent ChanOpenAck messages will fail (cf. Safe Blockchain). Let ccvChannel denote this channel. Then, ccvChannel is the only OPEN channel that can be connected to a port owned by the consumer CCV module. The provider chain side of the CCV channel is established when the provider CCV module receives the first ChanOpenConfirm message that is successfully executed; all subsequent ChanOpenConfirm messages will fail (cf. Safe Blockchain). The ccvChannel is the only channel for which ChanOpenConfirm can be successfully executed (cf. Safe Blockchain, i.e., IBC channel opening handshake guarantee). As a result, ccvChannel is unique. Moreover, ts existence is guaranteed by the Correct Relayer assumption.
  • Channel Validity: Follows directly from the Safe Blockchain assumption.
  • Channel Order: The provider chain accepts only ordered channels when receiving a ChanOpenTry message (cf. Safe Blockchain). Similarly, the consumer chain accepts only ordered channels when receiving ChanOpenInit messages (cf. Safe Blockchain). Thus, the property follows directly from the fact that the CCV channel is ordered.
  • Channel Liveness: The property follows from the Correct Relayer assumption.
  • Validator Update To VSC Validity: The provider CCV module provides only VSCs that contain validator updates obtained from the Staking module, i.e., by calling the GetValidatorUpdates() method (cf. Safe Blockchain). Furthermore, these validator updates were applied to the validator set of the provider chain (cf. Validator Update Provision).
  • Validator Update To VSC Order: We prove the property through contradiction. Given two validator updates U1 and U2, with U1 occurring on the provider chain before U2, we assume U2 is included in a provided VSC before U1. However, U2 could not have been obtained by the provider CCV module before U1 (cf. Validator Update Provision). Thus, the provider CCV module could not have provided a VSC that contains U2 before a VSC that contains U1 (cf. Safe Blockchain), which contradicts the initial assumption.
  • Validator Update To VSC Liveness: The provider CCV module eventually provides to all consumer chains VSCs containing all validator updates obtained from the provider Staking module (cf. Safe Blockchain, Life Blockchain). Thus, it is sufficient to prove that every update of a validator in the validator set of the provider chain MUST eventually be obtained from the provider Staking module. We prove this through contradiction. Given a validator update U that is applied to the validator set of the provider chain at the end of a block B with height h, we assume U is never obtained by the provider CCV module. However, at height h, the provider CCV module tries to obtain a new batch of validator updates from the provider Staking module (cf. Safe Blockchain). Thus, this batch of validator updates MUST contain all validator updates applied to the validator set of the provider chain at the end of block B, including U (cf. Validator Update Provision), which contradicts the initial assumption.
  • Apply VSC Validity: The property follows from the following two assertions.
    • The consumer chain only applies VSCs received in VSCPackets through the CCV channel (cf. Safe Blockchain).
    • The provider chain only sends VSCPackets containing provided VSCs (cf. Safe Blockchain).
  • Apply VSC Order: We prove the property through contradiction. Given two VSCs vsc1 and vsc2 such that the provider chain provides vsc1 before vsc2, we assume the consumer chain applies the validator updates included in vsc2 before the validator updates included in vsc1. The following sequence of assertions leads to a contradiction.
    • The provider chain could not have sent a VSCPacket P2 containing vsc2 before a VSCPacket P1 containing vsc1 (cf. Safe Blockchain).
    • The consumer chain could not have received P2 before P1 (cf. Channel Order).
    • Given the Safe Blockchain assumption, we distinguish two cases.
      • First, the consumer chain receives P1 during block B1 and P2 during block B2 (with B1 < B2). Then, it applies the validator updates included in vsc1 at the end of B1 and the validator updates included in vsc2 at the end of B2 (cf. Validator Update Inclusion), which contradicts the initial assumption.
      • Second, the consumer chain receives both P1 and P2 during the same block. Then, it applies the validator updates included in both vsc1 and vsc2 at the end of the block. Thus, it could not have apply the validator updates included in vsc2 before.
  • Apply VSC Liveness: The provider chain eventually sends over the CCV channel a VSCPacket containing vsc (cf. Safe Blockchain, Life Blockchain). As a result, the consumer chain eventually receives this packet (cf. Channel Liveness). Then, the consumer chain aggregates all received VSCs at the end of the block and applies all the aggregated updates (cf. Safe Blockchain, Life Blockchain). As a result, the consumer chain applies all validator updates in vsc (cf. Validator Update Inclusion).
  • Register Maturity Validity: The property follows from the following sequence of assertions.
    • The provider chain only registers VSC maturity notifications when receiving on the CCV channel a VSCMaturedPackets notifying the maturity of those VSCs (cf. Safe Blockchain).
    • The provider chain receives on the CCV channel only packets sent by the consumer chain (cf. Channel Validity).
    • The consumer chain only sends VSCMaturedPackets matching the VSCPackets it receives on the CCV channel (cf. Safe Blockchain).
    • The consumer chain receives on the CCV channel only packets sent by the provider chain (cf. Channel Validity).
    • The provider chain only sends VSCPackets containing provided VSCs (cf. Safe Blockchain).
  • Register Maturity Timeliness: We prove the property through contradiction. Given a VSC vsc provided by the provider chain to the consumer chain, we assume that the provider chain registers a maturity notification of vsc before UnbondingPeriod has elapsed on the consumer chain since the consumer chain applied vsc. The following sequence of assertions leads to a contradiction.
    • The provider chain could not have register a maturity notification of vsc before receiving on the CCV channel a VSCMaturedPacket P with P.id = vsc.id (cf. Safe Blockchain).
    • The provider chain could not have received P on the CCV channel before the consumer chain sent it (cf. Channel Validity).
    • The consumer chain could not have sent P before at least UnbondingPeriod has elapsed since receiving a VSCPacket P' with P'.id = P.id on the CCV channel (cf. Safe Blockchain). Note that since time is measured in terms of the block time, the time of receiving P' is the same as the time of applying vsc.
    • The consumer chain could not have received P' on the CCV channel before the provider chain sent it (cf. Channel Validity).
    • The provider chain could not have sent P' before providing vsc.
    • Since the duration of sending packets through the CCV channel cannot be negative, the provider chain could not have registered a maturity notification of vsc before UnbondingPeriod has elapsed on the consumer chain since the consumer chain applied vsc.
  • Register Maturity Order: We prove the property through contradiction. Given two VSCs vsc1 and vsc2 such that the provider chain provides vsc1 before vsc2, we assume the provider chain registers the maturity notification of vsc2 before the maturity notification of vsc1. The following sequence of assertions leads to a contradiction.
    • The provider chain could not have sent a VSCPacket P2, with P2.updates = C2, before a VSCPacket P1, with P1.updates = C1 (cf. Safe Blockchain).
    • The consumer chain could not have received P2 before P1 (cf. Channel Order).
    • The consumer chain could not have sent a VSCMaturedPacket P2', with P2'.id = P2.id, before a VSCMaturedPacket P1', with P1'.id = P1.id (cf. Safe Blockchain).
    • The provider chain could not have received P2' before P1' (cf. Channel Order).
    • The provider chain could not have registered the maturity notification of vsc2 before the maturity notification of vsc1 (cf. Safe Blockchain).
  • Register Maturity Liveness: The property follows from the following sequence of assertions.
    • The provider chain eventually sends on the CCV channel a VSCPacket P, with P.updates = C (cf. Safe Blockchain, Life Blockchain).
    • The consumer chain eventually receives P on the CCV channel (cf. Channel Liveness).
    • The consumer chain eventually sends on the CCV channel a VSCMaturedPacket P', with P'.id = P.id (cf. Safe Blockchain, Life Blockchain).
    • The provider chain eventually receives P' on the CCV channel (cf. Channel Liveness).
    • The provider chain eventually registers the maturity notification of vsc (cf. Safe Blockchain, Life Blockchain).
  • Consumer Slashing Warranty: Follows directly from Safe Blockchain.
  • Provider Slashing Warranty: Follows directly from Safe Blockchain.
  • VSC Maturity and Slashing Order: Follows directly from Channel Order.
  • Distribution Liveness: The CCV module on the consumer chain sends to the provider chain an amount T of tokens through an IBC token transfer packet (as defined in ICS 20). Thus, if the packet is relayed within the timeout period, then T (equivalent) tokens are minted on the provider chain. Otherwise, the T tokens are refunded to the consumer CCV module account. In this case, the T tokens will be part of the next token transfer packet. Eventually, a correct relayer will relay a token transfer packet containing the T tokens (cf. Correct Relayer, Life Blockchain). As a result, T (equivalent) tokens are eventually minted on the provider chain.
  • Validator Set Replication: The property follows from the Safe Blockchain assumption and both the Apply VSC Validity and Validator Update To VSC Validity properties.
  • Bond-Based Consumer Voting Power: The existence of hp is given by construction, i.e., the block on the proposer chain that handles a governance proposal to spawn a new consumer chain cc happens before all the blocks of cc. The existence of hc' and hp' is given by Life Blockchain and Channel Liveness. To prove the Bond-Based Consumer Voting Power property, we use the following property that follows directly from the design of the protocol (cf. Safe Blockchain, Life Blockchain).
    • Property1: Let val be a validator; let Ua and Ub be two updates of val that are applied subsequently by a consumer chain cc, at block heights ha and hb, respectively (i.e., no other updates of val are applied in between). Then, Power(cc,ha,val) = Power(cc,h,val), for all block heights h, such that ha <= h < hb (i.e., the voting power granted to val on cc in the period between ts(ha) and ts(hb) is constant).
    We prove the Bond-Based Consumer Voting Power property through contradiction. We assume there exist a height h on the provider chain between hp and hp' such that Power(cc,hc,val) > VP( pBonded(h,val) + sumUnbonding(hp, h, val) + sumSlash(hp, h, val) ). The following sequence of assertions leads to a contradiction.
    • Let U1 be the latest update of val that is applied by cc before or not later than block height hc (i.e., U1 is the update that sets Power(cc,hc,val) for val). Let hp1 be the height at which U1 occurs on the provider chain; let hc1 be the height at which U1 is applied on cc. Then, hp1 << hc1 <= hc, hp1 <= hp, and Power(cc,hc,val) = Power(cc,hc1,val) = VP(pBonded(hp1,val)). This means that some of the tokens bonded by val at height hp1 were completely unbonded before or not later than height hp' (cf. Power(cc,hc,val) > VP( pBonded(h,val) + sumUnbonding(hp, h, val) + sumSlash(hp, h, val) )).
    • Let uo be the first such unbonding operation that is initiated on the provider chain at height hp2, such that hp1 < hp2 <= hp'. Note that at height hp2, the tokens unbonded by uo are part of pUnbonding(hp2,val). Let U2 be the validator update caused by initiating uo. Let hc2 be the height at which U2 is applied on cc; clearly, Power(cc,hc2,val) < Power(cc,hc,val). Note that the existence of hc2 is ensured by Validator Update To VSC Liveness and Apply VSC Liveness. Then, hc2 > hc1 (cf. hp2 > hp1, Validator Update To VSC Order, Apply VSC Order).
    • Power(cc,hc,val) = Power(cc,hc1,val) = Power(cc,h,val), for all heights h, such that hc1 <= h < hc2 (cf. Property1). Thus, hc2 > hc (cf. Power(cc,hc2,val) < Power(cc,hc,val)).
    • uo cannot complete before ts(hc2) + UnbondingPeriod, which means it cannot complete before hc' and thus it cannot complete before hp' (cf. hc' << hp').
  • Slashable Consumer Misbehavior: The second part of the Slashable Consumer Misbehavior property (i.e., val is not slashed more than once for the same misbehavior) follows directly from Evidence Provision, Channel Validity, Consumer Slashing Warranty, Provider Slashing Warranty. To prove the first part of the Slashable Consumer Misbehavior property (i.e., exactly the amount of tokens sf*Token(Power(cc,hi,val)) are slashed on the provider chain), we consider the following sequence of statements.
    • The CCV module of cc receives at height he the evidence that val misbehaved on cc at height hi (cf. Evidence Provision, Safe Blockchain, Life Blockchain).
    • Let hv be the height when the CCV module of cc receives the first VSC from the provider CCV module. Then, the CCV module of cc sends at height h = max(he, hv) to the provider chain a SlashPacket P, such that P.val = val and P.id = HtoVSC[hi] (cf. Consumer Slashing Warranty).
    • The provider CCV module eventually receives P (cf. Channel Liveness).
    • The provider CCV module requests the provider Slashing module to slash val for misbehaving at height hp = VSCtoH[P.id] before handling any further maturity notifications received from the CCV module of cc (cf. Provider Slashing Warranty).
    • The provider Slashing module slashes the amount of tokens val had bonded at height hp except the amount that has already completely unbonded (cf. Slashing Warranty).
    Thus, it remains to be proven that Token(Power(cc,hi,val)) = pBonded(hp,val), with hp = VSCtoH[HtoVSC[hi]]. We distinguish two cases:
    • HtoVSC[hi] != 0, which means that by definition HtoVSC[hi] is the ID of the last VSC that update Power(cc,hi,val). Also by definition, this VSC contains the last updates to the voting power at height VSCtoH[HtoVSC[hi]] on the provider. Thus, Token(Power(cc,hi,val)) = pBonded(hp,val).
    • HtoVSC[hi] == 0, which means that by definition Power(cc,hi,val) was setup at genesis during Channel Initialization. Also by definition, this is the same voting power of the provider chain block when the first VSC was provided to that consumer chain, i.e., VSCtoH[HtoVSC[hi]]. Thus, Token(Power(cc,hi,val)) = pBonded(hp,val).
  • Consumer Rewards Distribution: The first part of the Consumer Rewards Distribution property (i.e., the tokens are eventually minted on the provider chain and then distributed among the validators) follows directly from Distribution Liveness and Distribution Warranty. The second part of the Consumer Rewards Distribution property (i.e., the total supply of tokens is preserved) follows directly from the Supply property of the Fungible Token Transfer protocol (see ICS 20).