# 理解 Clarity 的可判定性 ### 一种语言是非图灵完备或可判定，这意味着什么？ 非图灵完备和可判定这两个术语，你会经常在谈论 Clarity 的安全优势时听到，但它们是什么意思？ 虽然二者相关，但并不能完全互换，因为它们之间存在一些差异。 #### 非图灵完备 如果一个系统或语言无法模拟图灵机（即一种抽象计算模型），那么它就是非图灵完备的。与图灵完备系统相比，非图灵完备系统的计算能力更有限。图灵完备的系统或语言可以模拟任何图灵机。非图灵完备系统的例子包括有限状态机和某些特定领域语言（如 Clarity）。 非图灵完备语言通常无法表达所有可能的算法。具体来说，一些其解法需要无界循环或递归的问题，无法用非图灵完备语言表达。最后这一特性在 Clarity 的语境中特别重要，因为它使得无界循环和重入等特性在语言层面被禁止。 #### 可判定 如果存在一种算法，能够总是在有限时间内判断给定输入是否具有某种特定性质，那么这个问题就是可判定的。换句话说，可判定问题可以由一台保证对所有输入实例都会停机的图灵机来解决。可判定性是问题的属性，而图灵完备性是语言或计算系统的属性。 Clarity 具有可判定性这一事实意味着，开发者（以及工具）可以更容易地对 Clarity 合约的行为进行推理，并且无论输入如何，都能确定性地预测其行为。 ### 智能合约开发者的思维方式 在深入具体内容之前，我们先建立背景和视角，也就是作为希望编写安全代码的智能合约开发者应当持有的思维方式。 随着你进一步探索 Solidity 和 Clarity 的安全属性，你会看到总是有一些缓解措施 *可以* 由开发者采取，以帮助解决其中一些安全问题。 这种思路的主要问题在于，它增加了智能合约安全中人为出错的概率。如果我们能够在保留功能性的同时尽可能降低人为错误的可能性，那我们就应该这样做。 ### 智能合约应该是图灵完备的吗？ 我们将会发现智能合约的新应用。这些应用将超越当前的智能合约、传统合同，甚至可能开启新的经济机会。鉴于这些可能性，我们应当如何构建智能合约？我们的智能合约语言应当具备哪些特征？ 将数据与程序分离是一种良好实践。智能合约应该是数据，还是程序，还是介于两者之间的东西？如果智能合约是数据，那么执行它们的程序应该是图灵完备的，还是可能应当能力更弱一些？如果智能合约是程序，那么它们应当用什么语言编写？这种编程语言应当具备哪些特征？ 丘奇－图灵论题是假设所有形式化的计算概念都可以由图灵机或现代计算机来刻画。如果一种编程语言能够涵盖所有形式化的计算概念，那么它就是图灵完备的。许多编程语言都是图灵完备的。例如，Python、C++、Rust、Java、Lisp 和 Solidity 都是图灵完备的。 考虑一个程序及其输入。在最坏情况下，确定这个程序的输出是不可能的。对某个特定输入下的程序进行验证，是通过生成正确性证明来完成的。 正确性证明是可以通过机械方式验证的逻辑证明。为程序及其输入找到正确性证明是不可判定的。Kurt Gödel 证明了存在不可判定的逻辑命题。 这表明，图灵完备语言中的所有程序在最坏情况下都无法被验证。因此，图灵完备的智能合约语言必须允许那些无法被验证的合约存在。 Alonzo Church 和 Alan Turing 证明了存在不可计算的问题。不可计算问题不能被任何图灵机解决。因此，假设丘奇－图灵论题成立，这些不可计算问题也不能被任何计算机解决。 我们将在本节后面进一步探讨这一观点。 图灵完备语言具有非常强的表达能力。事实上，假设丘奇－图灵论题成立，从某种意义上说，图灵完备语言的表达能力已经达到了最大。 这里是否存在权衡？不可计算问题以及有效性可能不可判定的程序，会带来哪些类型的问题？ 随着智能合约开始涵盖合同法的一部分，想一想税法中庞大的法律和法规体系。 例如，美国税法及其法规的篇幅达数百万词。国际税法及其法规则使这一数字高得多。 这些法律和法规是程序，还是数据？如果税法用一种图灵完备语言来编写，那么法律就可能会编码不可计算的问题。对于会计师来说，其建议变得不可判定将是一场噩梦。 Clarity 是非图灵完备的，但表达能力依然很强。这使得 Clarity 具有可判定性，并且无法编码不可计算的问题。围绕 Solidity 等智能合约语言，已有一些讨论和论文提出 Solidity 的非图灵完备子集。这些子集是可判定的，也不能编码不可计算的问题。然而，目前对于应采用哪些子集尚无共识，而且它们也没有被广泛使用。 ### 可判定性在智能合约中的优势 为什么在智能合约的语境中，可判定性如此重要？ 首先，Clarity 调用不可能在调用过程中途耗尽 gas。由于其可判定性，我们可以对调用图进行完整的静态分析，从而在执行前准确了解成本。 Solidity 允许无界循环、递归和动态函数调用，这使得事先准确预测执行成本或 gas 使用量变得困难。因此，如果 gas 限额设置不当，或者合约遇到计算需求意外升高的场景，Solidity 合约在执行过程中可能会耗尽 gas。 一个实际例子是 Solidity 中某类 DoS 攻击问题，在这种攻击中，合约因无界执行约束而无法运作。一个例子是 GovernMental 攻击：为进行支付而需要删除的一个映射变得过于庞大，以至于对其进行操作超出了区块 gas 限制。 Clarity 的语言设计中有几种不同的特性可以防止此类 DoS 攻击。 分析系统之所以能够准确估算执行成本，是因为 Clarity 有意限制了某些功能。 例如，Clarity 中没有递归，因此我们不能无限反复地调用某个函数。 Clarity 中的数据类型也受到限制。任何不需要硬性长度上限的数据类型都不可迭代。 例如，映射和元组在定义时不要求输入最大长度，但你也不能对它们进行迭代。 另一方面，可迭代的列表则要求开发者在定义时设定上限。这是能够对 Clarity 合约进行准确静态分析的重要原因之一。 那么，在 Clarity 中我们会如何实现一个大小未定义的映射呢？我们不会，因为这是一种智能合约设计中的反模式。 相反，Clarity 会迫使我们去思考更好的解决方案。例如，让用户自己处理映射/列表元素操作，而不是在合约层面执行批量操作。 如果你 [分析 GovernMental 攻击](https://hackernoon.com/smart-contract-attacks-part-2-ponzi-games-gone-wrong-d5a8b1a98dd8#h-attack-2-call-stack-attack)，你会看到它利用了多个安全问题，而这些问题在 Clarity 中都得到了缓解。你还会看到，为了让这种攻击再次实施在经济上变得不可行，后来也加入了修复措施。 这也引出了在建立有关智能合约和区块链系统的恰当思维模型时另一个关键点：复杂性意味着更多潜在漏洞，而这又意味着需要增加更多复杂性来解决这些漏洞。 当这种情况一再发生时，我们就是在把自己困在一个日益复杂的系统之中。在语言层面解决这些问题，可以防止这种不断增长的复杂性。 若想深入了解 Clarity 是如何设计的，请查看 [SIP-002](https://github.com/stacksgov/sips/blob/main/sips/sip-002/sip-002-smart-contract-language.md). {% hint style="info" %} 你还可以在以下内容中查看更多常见的智能合约漏洞以及它们是如何被缓解的： [这篇文章](https://stacks.org/bringing-clarity-to-8-dangerous-smart-contract-vulnerabilities/). {% endhint %} 当我们考察安全测试和审计时，这也会产生二阶影响。智能合约测试的一种常见工具是形式化验证，在这种方法中，我们用数学方式证明智能合约的某些性质在所有情况下是否会保持为真。 这可能导致路径爆炸问题，即可用路径太多，从而使形式化验证变得极其困难。Clarity 缓解了这个问题，因为程序不可能遇到无界循环。 这引导我们形成一个更一般性的思维模型，以思考随着智能合约持续成为我们经济中越来越重要的一部分，可判定性意味着什么。请记住，区块链系统的目标是创建一个开放、透明、公平的金融系统。 这意味着智能合约将负责为越来越多的人管理大量财富。随着智能合约涵盖更多金融结构，其复杂性和使用范围都会增长。 复杂性是安全的敌人。系统越复杂，在执行步骤没有硬性限制时，产生不可计算问题的危险就越大。 这对于不仅开放透明而且不可变更的金融基础设施来说是致命的。让我们再多探讨一下这种不可计算性的概念。 ### 对不可计算性的直觉理解 直观来说，不可计算性是不可判定性的算法视角。不可计算性与不可判定性具有相同的基础。不可判定的问题通常被表述为逻辑命题或关于整数的命题。当然，程序本身就是逻辑命题，甚至也可以被看作整数，尽管我们通常以不同方式看待程序。我们往往会从内存模型、实现细节和执行语义等更多方面来看待程序。 这个 [停机问题](https://en.wikipedia.org/wiki/Halting_problem)：举个例子，给定任意程序 `P` 以及任意有限输入 `I` 对于 `P`，那么停机问题就是要判断 `P` 在输入上是否停机 `I`. Alonzo Church 和 Alan Turing 证明了停机问题是不可解的。 Christopher Strachey 给出了一个基于反证法的直观证明，说明停机问题是不可计算的。这个证明首先假设存在一个程序 `H` 它可以为任何程序解决停机问题 `P`. `H(P)` 如果 `P` 会停机则返回 true，否则返回 false。然后构造一个程序 `P` 当 `H(P)` 为 true 时它不会停机，从而产生矛盾。类似地，这个程序 `P` 当 `H(P)` 为 false 时会停机，这同样导致矛盾。 不可计算问题是指无论提供多少时间或资源，都无法由算法或计算机解决的问题。这类问题有多种形式，其中一个例子是 Emil Post 提出的 Post 对应问题。 Post 对应问题可以用字符串对和一个整数来描述。设想你有 n 对字符串，称为 P。这些字符串由某个字符集中的字符组成，例如 UTF-8 或任何至少有两个符号的字母表。这些字符串对如下所示： ``` P = { (x1, y1), (x2, y2), … , (xn, yn) } ``` 现在，你还有一个大于 0 的整数 m。Post 对应问题要问的是，是否存在一种方法，能够利用给定的字符串对构造一个索引列表 (i1, i2, …, im)。如果需要，这些索引可以重复，但有一个条件：当你使用这些索引把各对中的 x 字符串组合起来时，得到的结果字符串必须等于使用相同索引从相同字符串对中组合出的 y 字符串。换句话说： ``` x(i1) x(i2) … x(im) = y(i1) y(i2) … y(im) ``` 当开发者尝试解决 Post 对应问题时，他们通常会尝试使用不定循环（即没有固定迭代次数的循环），而不是递归。这是因为这个问题似乎需要在不同的索引组合中搜索，直到找到解，或者证明不存在解为止。 简单来说，Post 对应问题涉及寻找一个索引序列，使其应用于给定的字符串对后，能从 x 和 y 两部分分别生成相同的拼接字符串。这个问题被认为是不可计算的，因为不存在一种通用算法，能够对所有可能的输入字符串对和整数求解它。 事实证明，关于程序行为的许多问题都是不可计算的。对于用图灵完备语言构建的智能合约来说，这会带来许多后果，其中许多我们现在还未意识到，但随着未来遇到这些问题，我们必然会逐渐意识到。 ### Raymond Smullyan 对不可判定性的直觉理解 这是 Raymond Smullyan 用来理解命题逻辑中不可判定性的方法的一部分。它利用元信息来表明某件事必然为真，尽管它无法在命题逻辑中被证明。这一方法建立在一个悖论之上。 在命题逻辑中，如果我们无法证明一个逻辑命题为真或为假，那么这个命题就是不可判定的。给定一个命题逻辑陈述 S，证明是一串形式化的逻辑推导，从基本事实出发，最终指出 S 为真还是为假。 Smullyan 从一个骑士与骗子之岛开始。骑士永远说真话。骗子永远说谎。除此之外，我们无法区分岛民。 有一位伟大的逻辑学家叫 Ray。凡是 Ray 证明的都是真的。这就像一个优秀的定理证明器。 岛民 Jack 向逻辑学家 Ray 宣称：“你无法证明我是骑士。” 接下来的推理基于对这一情形的元知识。这种元知识表明，在命题逻辑中有些问题是不可判定的。 如果 Ray 能证明 Jack 是骑士，那么 Jack 就一定是骗子，因为 Jack 一定说了谎。这是因为 Ray 证明了 Jack 是骑士。既然 Jack 是骗子，Ray 的证明就与“Ray 只证明真命题”这一假设相矛盾。因此，这种情况不成立。 如果 Ray 无法证明 Jack 是骑士，那么 Jack 就一定是骑士，因为 Jack 说了真话。但 Ray 却无法证明 Jack 是骑士这一事实。 在智能合约和编程语言的语境中，像 Solidity 这样的图灵完备语言伴随着出现不可判定问题的可能性。 这些不可判定问题类似于骑士与骗子故事中呈现的悖论：基于给定信息，无法判断 Jack 究竟是骑士还是骗子。 在骑士与骗子的故事中，Ray 类似于一个定理证明器，或者图灵完备语言中的一个智能合约。Ray 面对的是一个在该系统约束（骑士与骗子）内不可判定的陈述，这会导致悖论。 类似地，图灵完备的智能合约语言可能会遇到无法解决的不可判定问题，从而导致意外行为、漏洞或资源消耗问题（例如以太坊中的 gas 耗尽）。 另一方面，像 Clarity 这样的非图灵完备语言通过限制其表达能力来避免不可判定问题。 在骑士与骗子故事的语境中，非图灵完备语言根本不会允许 Jack 说出可能导致悖论的话。通过禁止无界循环和递归等某些特性，非图灵完备语言能够对智能合约的行为和资源使用提供更强的保证。 这种可预测性在很多情况下都很理想，尤其是在处理高价值交易或关键系统时。 ### 参考资料 《各种有趣主题的数学：娱乐数学研究（插图版）》，Jennifer Beineke（编者），Jason Rosenhouse（编者），Raymond M. Smullyan（前言），普林斯顿大学出版社，2016 年。