Lighter ZK 电路公开报告 - ZKSECURITY

我们的团队与 Lighter 合作，审查了他们用于可验证订单簿撮合的自定义 ZK 电路。代码扎实且组织良好。与 Lighter 的工程师合作非常愉快，他们都非常配合。

你可以在此处阅读完整报告。

本文的其余部分包含该报告的概述部分的复制/粘贴。

Lighter 电路概述

Lighter 是一种作为 Layer 2 (L2) 实现的交易所，因为它的状态转换在 Layer 1 (L1) 上进行验证和最终确定。L1 通过验证零知识证明来确保每个状态转换都有效，从而使 Lighter 成为 ZK rollup。零知识证明不仅证明了一系列状态转换已正确执行，还将子状态转换的压缩摘要公开给 L1。

将子状态转换公开给 L1 非常重要，原因有两个：不仅某些转换需要额外执行逻辑并在 L1 上强制执行策略，而且服务运营中出现的问题不得导致系统完全停止。由于数据发布在 L1 上，因此在紧急情况下，任何 L1 用户都可以通过重放所有公开的差异来重新计算 L2 的最新状态。

有两个主要电路支持 Lighter L2 应用程序，包括我们所说的 zkLighter 电路：

1. 主操作电路，在系统正常运行期间，它应该是主要电路。
2. 退出舱口电路，代码中所谓的“desert”电路，在发生紧急情况时接管并允许用户退出系统。有关更多信息，请参见本概述的末尾。

在本概述的其余部分中，我们将滥用术语 zkLighter 电路 来指代第一个电路。

应用程序的状态

为了提供持久存储的更新，Lighter 的存储结构使其可以通过 Merkle 树进行身份验证。更新可以采用验证应用程序完整状态的 Merkle 树根，并生成更新的 Merkle 树根，该根可以保存为新状态的经过身份验证的快照。

我们可以将 Lighter 的整个状态总结为一个超树（树的树），如下所示：

上图中有 6 个真实的 Merkle 树，它们被分配给不同的颜色。其他“树”只是其输入的哈希，没有内部节点。

请注意，帐户的状态分为两个不同的树：左侧的树包含所有帐户信息，除了锁定在已插入订单簿中的订单中的资产数量。为了优化目的，此额外信息包含在“帐户元数据”树中。

市场的订单簿树非常特殊，因为它是一棵相当大的树（高度为 72），并且在其所有内部节点中包含额外的信息。因此值得单独查看它：

订单簿中的订单存储在基于价格和随机数计算的特殊路径下。由于价格是路径的第一部分，因此叶子按从最低到最高的价格排序，并且自然会用左侧的买单和右侧的卖单（以及中间可见的价差）来绘制树。

树中始终应该存在一个缺口，缺口的左侧有买单，右侧有卖单，从而构成 价差。

请注意，虽然卖单从零开始索引，但买单从最大随机数值开始。这种设计选择导致了先前对更高优先级订单的观察，但也导致了一种特殊情况，即卖单和买单在同一个“价格子树”中交叉：如果一个卖单被插入到与其他买单相同的子树中，那么这些其他买单可以被视为传入订单的已匹配部分的 交叉订单，并且会在卖单的右侧找到（反之亦然，对于插入到具有多个卖单的价格子树中的买单）。当我们讨论匹配引擎时，此观察结果将在以后很有用。

zkLighter 区块

zkLighter 电路处理的主要对象是区块。与典型的区块链一样，区块包含一个交易列表，并通过将这些交易应用于已知的先前状态（如先前区块所证明的那样）来生成状态转换，并证明更新后的状态。

交易以确保匹配算法中没有作弊的方式逐一“执行”。也就是说，只要交易的排序以公平的方式进行，交易就是最佳的。

请注意，某些交易不是真正的用户交易，而是插入的“虚假”交易，有助于完成某些类型的用户交易的执行（特别是，可能需要多个“周期”才能完成的交易）。我们将在后面的章节中对此进行更详细的说明。

一个区块的逻辑如下：

1. 确保第一个交易建立在区块的旧状态根之上。
2. 验证每个交易，确保每个交易都建立在前一个交易的输出状态之上。
3. 将区块号、时间戳、状态转换前后的根状态（因为 L1 需要验证状态转换是否建立在最新记录的状态之上）、Merkle 树的其他有用根（有效性树和交易树）以及最终描述构成状态转换的某些交易的公共数据向量作为公共输入公开。

我们将相同的逻辑总结为伪代码如下：

def verify_block(public, private):
    # init
    pub_data = [0] * BLOCK_TXS * 24
    pos = 0

    # check first transaction
    assert(private.old_state_root == private.txs[0].state_root_before)
    pending_pub_data, tx_pub_data_size, roots = verify_transaction(private.txs[0], private.created_at, roots)
    copy(pub_data[pos:], pending_pub_data) # via multiplexer
    pos += tx_pub_data_size

    # check the rest of transactions
    for i in range(1, BLOCK_TXS):
        assert(private.txs[i-1].state_root_after == private.txs[i].state_root_before)
        pending_pub_data, tx_pub_data_size, roots = verify_transaction(private.txs[i], private.created_at, roots)
        copy(pub_data[pos:], pending_pub_data) # via multiplexer
        pos += tx_pub_data_size

    # compute new state root (unnecessary as compute)
    new_state_root = private.txs[i-1].state_root_after
    [new_account_root, new_validium_root, new_transaction_root] = roots

    # create commitment as public output
    tx_pub_data_hash = sha256(pub_data)
    commitment_data = [ # 176 Bytes in total:\
        private.block_number,         # 8\
        private.created_at,           # 8\
        private.old_state_root,       # 32\
        new_state_root,               # 32\
        new_validium_root,            # 32\
        new_transaction_root,         # 32\
        tx_pub_data_hash,             # 32\
    ]
    commitment = sha256(commitment_data)
    assert(commitment == public.block_commitment)

交易类型

zkLighter 中的大部分逻辑来自周期的执行，其中一个周期包含可以执行交易的逻辑。如前所述，交易可以是用户交易，也可以是帮助在多个周期中驱动用户交易执行的“虚假”交易。

对交易进行分类的一种方法是将其分为不同的类别。某些交易是 L2 交易，因为它们通过 L2 帐户状态中包含的公钥进行身份验证：

• 转账。这是 L2 中帐户之间的直接资产转账。
• 提款。这是从 L2 到 L1 的提款交易。
• 创建订单。这会在某个市场中创建一个订单。
• 取消订单。这会取消某个市场中的订单。
• 更改公钥。这允许用户更新其帐户的公钥。请注意，此交易并非“纯粹” L2 交易，因为它主要在 L1 上进行身份验证：L1 合约的逻辑负责确保帐户关联的 L1 地址是 msg.sender。

其他一些交易被认为是 L1 交易，并提交给 L1 合约。我们假设当一个区块公开来自此类交易的状态转换时，L1 逻辑将确保它们也已提交到 L1。这些交易类型是：

• 创建订单簿。L1 上的管理员应该能够创建一个新的市场来交易一对资产。
• 更新订单簿。L1 上的管理员应该能够更新现有市场的信息。
• 存款。这允许 L1 用户将一些特定的资产存入 L2 上的任何帐户。
• 完全退出。这允许用户清空其帐户中的特定资产。这意味着不仅用户的帐户将被清空，而且该资产的所有订单（在该资产可能是一对的任何市场中）都将被取消。请注意，此交易的存在是为了确保用户即使在系统审查他们时仍然可以退出系统（因此与提款交易不同，这些交易是在 L1 上发布和验证的）。

最后，有两种类型的“虚假”交易用于完成先前某些用户交易的执行：

• 声明订单。此交易用于继续处理 CreateOrder 交易，因为 taker 订单可能会删除和更新市场订单簿中的多个 maker 订单。
• 退出订单。此交易用于继续处理 FullExit 交易，因为 prover 需要与该退出交易关联的订单一样多的周期。

为了帮助跟踪跨周期交易的执行状态，还使用了一个名为“register”的附加变量。由于作为单个用户交易执行的一部分需要插入的虚假交易数量没有理论限制，因此 register 也是跨区块的持久变量（如第一个状态图中所示）。

关于展开的逻辑的说明

zkLighter 的逻辑被编码在零知识电路中，因此循环必须展开，并且不能发生真正的分支。这给代码增加了相当多的复杂性，代码必须确保始终可以计算每个分支并产生虚拟结果。我们在本节中提到了一些技术。

本节中的大多数技术可以简化为使用 多路复用器。例如，通常会计算布尔值并使用它们来确保一次只采用一条路径（并且一次只设置一个交易）：

// compute tx type
isEmptyTx := types.IsEqual(api, tx.TxType, types.TxTypeEmpty)
isChangePubKey := types.IsEqual(api, tx.TxType, types.TxTypeChangePubKey)
// TRUNCATED...

isSupportedTx := api.Add(
    isEmptyTx,
    isChangePubKey,
    // TRUNCATED...
)
api.AssertIsEqual(isSupportedTx, 1)

// verify nonce, expired at and signature
isLayer2Tx := api.Add(
    isChangePubKey,
    isTransferTx,
    // TRUNCATED...
)

未采用的分支通常会采用此类标志以避免断言虚拟值。为此，反过来会增强断言函数以有条件地断言。例如：

func AssertIsVariableEqual(api API, isEnabled, i1, i2 Variable) {
    zero := 0
    i1 = api.Select(isEnabled, i1, zero)
    i2 = api.Select(isEnabled, i2, zero)
    api.AssertIsEqual(i1, i2)
}

此外，必须以涵盖所有可能情况的方式进行搜索和写入数组：

pos := 0
inc := 1

// use incremental arrays to avoid high constraint cmp operation
// pos is used to indicate the current position to write in pubData
// inc is used to indicate whether current position needs to be incremented
// Let's say pubDataSize is 4, the values in iteration will be:
// IsEqual : 0 0 0 0 1 0 0 0 0
// Inc     : 1 1 1 1 0 0 0 0 0
// Pos     : 1 2 3 4 4 4 4 4 4
for i := 0; i < types.PubDataDWordSizePerTx; i++ {
    // for the first tx, no need to iterate for position.
    pubData[i] = pendingPubData[i]
    inc = api.Sub(inc, types.IsEqual(api, i, txPubDataSize))
    pos = api.Add(pos, inc)
}

验证交易

zkLighter 中的交易包含所有可能的交易，原因如上所述。此外，它包含足够的数据来验证签名（如果交易是用户交易），以及 sequencer 提供的 witness 数据，以供 prover 将交易应用于状态。witness 数据主要包括存储在最新状态中的数据，这些数据将由交易修改，以及用于验证数据完整性的 Merkle 证明。

type TxConstraints struct {
    // tx type
    TxType Variable
    // different transactions
    ChangePubKeyTxInfo    ChangePubKeyTxConstraints
    DepositTxInfo         DepositTxConstraints
    TransferTxInfo        TransferTxConstraints
    CreateOrderBookTxInfo CreateOrderBookTxConstraints
    UpdateOrderBookTxInfo UpdateOrderBookTxConstraints
    CreateOrderTxInfo     CreateOrderTxConstraints
    CancelOrderTxInfo     CancelOrderTxConstraints
    ClaimOrderTxInfo      ClaimOrderTxConstraints
    ExitOrderTxInfo       ExitOrderTxConstraints
    WithdrawTxInfo        WithdrawTxConstraints
    FullExitTxInfo        FullExitTxConstraints

    // nonce
    Nonce Variable
    // expired at
    ExpiredAt Variable
    // signature
    Signature SignatureConstraints

    // everything else after this point is storage data that is provided by the sequencer and that can be inserted in the circuit to help execution
}

我们可以将交易电路的逻辑总结如下：

1. 确定我们正在查看的交易。
2. 对交易数据进行哈希处理，并在 L2 交易的情况下验证交易的签名。
3. 从交易中计算公共数据（我们最终会公开公开这些数据）。
4. 验证交易的字段（检查因交易而异）。
5. 此时，我们还会验证，如果 register 非空，则正确的交易与其关联。
6. 计算“增量”——基于交易类型和状态的 witness 叶子所做的更改。
7. 验证当前 witness 叶子是否在当前状态中。这意味着验证许多 Merkle 成员资格证明。直到在公共输入中公开的根。
8. 使用先前计算的“增量”更新现在已验证的叶子。
9. 重新计算 Merkle 根（使用用于验证 Merkle 成员资格的相同证明），直到在公共输入中公开的根。
10. 确保除了我们正在查看的交易之外，每个交易都设置为零。
11. 返回公共数据、其大小（因为向量填充了零）和更新后的根。

witness 的叶子在 Merkle 树中进行身份验证、更新和计算新根的三步概念是上述协议中大部分逻辑的基础。我们在下图给出了这三个步骤的示例。

其中的大部分复杂性（本身就是代码库的复杂部分）来自更新状态，更具体地说，是负责执行用户交易的匹配引擎。我们将在下一节中对此进行更详细的说明。

订单簿交易

如前所述，用户可以提交两种类型的订单交易： 创建订单 和 取消订单。顾名思义，取消订单仅负责删除订单簿中的叶子，因此这是我们最后一次提到它。

有四种不同类型的创建订单交易，它们都结合了不同的技术，以使用户确信 matchmaker 没有任何作弊行为，并且每个已处理的交易都是最佳的（只要交易的排序是公平的）。在回顾它们之前，我们先介绍一些术语（这些术语不是 Lighter 文档的一部分）：

• 目标叶子：这是叶子，它代表我们需要匹配的来自 taker 角度的最差（resp. 最小）的最新 maker 订单——在完全匹配的情况下，或者我们可能需要插入订单簿中的叶子——在部分匹配的情况下。如果我们最终插入，则目标叶子代表与用户订单交易相同类型的订单。
• 待处理叶子：这些是订单可以完全消耗以部分或完全完成交易的所有叶子，如果它们是相同类型的，则其优先级高于目标叶子，或者如果它们是不同类型的（由于买单和卖单在价格子树中的排列方式），则是交叉订单。

请注意，待处理叶子始终被限制为小于订单交易的大小。这是一个重要的属性，因为它用于证明不同订单类型的匹配的最佳性。直观地说，此属性允许我们将自己定位在订单树中的正确位置：正好位于完全匹配和不完全匹配之间。

我们现在回顾不同类型的订单交易。

限价订单。此订单为买单（resp. 卖单）设置最高（resp. 最低）价格。如果它无法与市场中现有的 maker 订单完全匹配，则剩余的匹配金额将插入订单簿中（在与尽可能多的标记订单部分匹配后）。

由于订单簿树的内部节点的特殊组成（其中包含所有子节点的汇总买单和报价），因此可以使用目标叶子并向上爬树以计算所有待处理订单的总和。在完全匹配的情况下，目标叶子和待处理订单应代表要交易的全部金额（并且易于验证）。在部分匹配的情况下，可以验证要插入的叶子和树的其余部分之间的交叉订单小于匹配金额（并且价格将是正确的，因为我们在正确的价格子树中）。

我们在下图中说明了如何爬树以计算所有待处理订单的总和：

有趣的是，可以猜测相邻子树中包含的汇总总和，而无需 witness 相邻节点的前像（避免计算哈希）：它可以从父节点和当前子节点派生，如下图所示：

在这两种情况下，register 都设置为 ExecutePendingTrade，并将剩余金额作为“待处理大小”提供，以便从订单树中声明。sequencer 插入足够的声明交易以将待处理大小减少到 0，其中每个声明交易消耗当前最高优先级订单（我们可以通过内部节点检查是否存在其他更高优先级的交易）。一旦待处理大小减少到 0，就可以重置 register 以接受下一个用户交易。

市价订单。此订单类似于限价订单，但不会最终出现在订单簿中。因此，它是一个 taker 订单（因为它不“制造”市场）。

对于完全匹配，这是市价订单所期望的，期望与限价订单完全匹配具有相同类型的目标叶子。如果一切顺利，协议的其余部分将遵循与成功的限价订单相同的逻辑。

市价订单有两种有效的可能失败的情况。在这种情况下，prover 仍然必须能够处理它们并证明不可能处理订单，因为某些订单是必须履行的优先订单，否则会触发协议的退出舱口（请参阅后文）。

第一个边缘情况是订单簿中没有足够的流动性来匹配交易，这很容易证明，因为总流动性包含在订单树的根节点中。

第二个边缘情况是交易已匹配但在不希望的价格下：每个市价订单都明确地与 slippage 值相关联，该值指示接受交易的最差价格。如果满足这种情况，prover 将提供与限价订单情况类似的目标叶子。由于待处理叶子的总和始终被限制为低于订单的大小，因此电路可以检查市价订单是否正好位于目标叶子和待处理叶子之间。

Fill-or-kill (FoK) 订单。这是一个 taker 订单，如果无法与一组现有的 maker 订单完全匹配，则为 no-op。

FoK 订单遵循与限价订单相同的策略，除非在完全匹配的情况下才启动声明过程。

Immediate-or-Cancel 订单。这是另一个 taker 订单，可以与多个 maker 订单匹配，如果仅部分匹配，则不会最终出现在订单簿中。

它们遵循与之前的 FoK 订单相同的策略，除非即使没有完全匹配，仍然启动声明过程。

我们将在下图中回顾一些细节：

退出舱口模式

Lighter 智能合约应该（因为我们只查看了电路方面）有两种运行模式：一种正常的运行模式和一种回退模式（代码中称为“desert”），如果在发生不好的事情时，它会成为持久的默认模式。“不好的事情”在论文中定义为例如，无法及时处理优先交易。

一旦激活 退出舱口，唯一接受的证明将更改为所谓的“desert”证明，该证明仅允许用户退出应用程序并提取锁定在应用程序中的任何资金。只要用户知道状态（如前所述，可以通过使用智能合约处理的来自所有状态转换的公开数据来重建状态），就可以由用户生成这些证明。

该证明基于简单电路的执行：

• 检查状态树是否正确验证帐户中的资产（通过执行一堆 merkle 证明验证）。
• 作为公共输入，公开：
  • 帐户索引：因此我们可以保存该事件并强制每个帐户单次退出。
  • 帐户 L1 地址：因此我们知道如何路由解锁的资金。
  • 资产 ID 和资产余额：以了解要从 lighter 应用程序解锁的Token类型和数量。
  • 状态根：因此我们可以验证执行是针对保存在智能合约中的正确状态完成的。

为了完整起见，用伪代码表示：

def verify_desert(public, private):
    # 1. verify state root based on account and validium root
    new_state_root = mimc(private.account, private.validium_root)
    assert(private.state_root == new_state_root)

    # construct public data
    pub_data = [\
        to_bytes(private.tx.account_index, 32/8),\
        to_bytes(private.tx.asset_id, 16/8),\
        to_bytes(private.tx.asset_amount, 128/8),\
        to_bytes(private.tx.L1_address, 160/8),\
    ]

    # verify provided exit tx
    assert(private.tx.L1_address == private.account_info.L1_address)
    assert(private.tx.account_idx == private.account_info.account_idx)
    assert(private.tx.asset_id == private.account_info.assets_info.asset_id)
    assert(private.tx.asset_amount == private.account_info.assets_info.asset_amount)

    # sanitize assets info
    assert(private.account_info.assets_info.asset_id < 2^16)

    # verify account asset root
    asset_merkle_helper = to_binary(private.account_info.assets_info.asset_id, 16)
    asset_node_hash = mimc(private.account_info.assets_info.balance)
    Merkle.verify(private.account_info.asset_root, asset_node_hash, private.merkle_proofs_account_asset, asset_merkle_helper)

    # sanitize account info
    assert(private.account_info.account_index < 2^32)

    # verify account root
    account_index_merkle_helper = to_binary(private.account_info.account_index, 32)
    account_node_hash = mimc(private.account_info)
    Merkle.verify(private.account_root, account_node_hash, private.merkle_proofs_account, account_index_merkle_helper)

    # compress public input into public output
    pending_commitment_data = append(private.state_root, pub_data)
    commitment = sha256(pending_commitment_data)
    assert(commitment == public.commitment)

• 原文链接： blog.zksecurity.xyz/post...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～