Simplicity:漏洞和副作用
Blockstream Research Simplicity Language

Simplicity:漏洞和副作用

Andrew Poelstra

与大多数编程语言不同,Simplicity 表达式是由一系列组合器构建的,这些组合器由更小的表达式构建而成。这些表达式代表了接受某些输入并将其映射到某些输出的函数。 下面是最简单的 Simplicity 程序:

main := iden

这个程序的输入是空的,输出也是空的。让我们做一些更有趣的事情,取一点并反转它:

   bit0 := injl unit : 1 * 1 -> 2
   bit1 := injr unit : 1 * 1 -> 2

   padR := pair iden unit     : 2 -> 2 * 1 
   bitflip := case bit1 bit0  : 2 * 1 -> 2
   main := comp padR bitflip  : 2 -> 2

这里最终的简化表达式是我们的main函数。通过从下到上的阅读,我们可以看到它是由几个较小的函数组成的,最终由 unit 组合器接地。单元组合器产生空输出。单元组合器与接收任意输入并返回不变值iden 和输出外部提供值witness一起,构成了每个 Simplicity 表达式的基础。在本代码片段中,我们提供了类型注解,以帮助指明从表达式的每个部分流向下一部分的数据。这里的 "1 "代表单元类型,也就是我们所说的 "空输出"。2 "表示位,其值可以是 0 或 1。如果你没有详细了解这个片段,也不用担心。这里只是为了直观地展示 Simplicity 代码的外观。稍后,我们将更仔细地分析一个更有趣的程序。

一种规范语言

根结底,所有的编程语言都表达了将计算组合起来以构建更大计算的思想。比特币脚本(如 Forth 或 PostScript)通过堆栈机来实现这一点,在堆栈机中,每次计算都会依次操作一个数据对象列表。以太坊的 EVM 使用函数调用架构,代码可以调用其他代码块(可能在其他合约中),这些代码块将数据作为输入,并将数据作为输出返回。这也是当今几乎所有主流编程语言所使用的模型。

编程语言使用副作用 (side effects) 来与外部世界交互,例如正在花费的事务。在 EVM 中,合约还能访问键值数据存储,从而无需明确传递状态就能跨事务保持状态。

在比特币脚本和 EVM 中,位反转都可以用一个操作码来完成(尽管比特币版本可以接受许多不同的输入,其中大部分都不像位,而 EVM 版本则是按位操作,但总是同时对 256 位进行操作)。我们不禁要问,为什么简单性模型会导致如此简单的事情变得如此繁琐?

我们在 Simplicity 中的目标是正式规定程序的语义,包括程序所代表的功能,以及评估程序所涉及的计算资源。原则上,我们可以正式规定一种像 Bitcoin Script 或 EVM 一样运行的语言,但这项任务会非常困难,而且其结果也几乎难以被任何人验证。相反,我们用简单性定义了一小套基本组合器,每一个组合器都反映了组合函数的数学基本方式。由此产生的语言语义非常小,甚至可以放在一件 T 恤上

实际上,对于位反转这样的事情,这些代码只需编写一次,然后重复使用。事实上,我们已经为您完成了编写工作,并将其内置到语言中。在编写自己的代码时,只需使用快捷键 jet_not 代替上述代码即可。我们将在下一节详细介绍喷射器。

最终,在实践中,几乎没有人会编写简单性代码。简单性为区块链程序提供了一个定义明确的基础,但它仅仅是一个基础。真正的工作将在更高级别的语言中完成,这些语言编译成简单性代码,并证明其操作的正确性。

程序与表达式

具有琐碎输入和输出值的表达式有一个特殊的名称。我们称这些表达式为程序。从数学上讲,只有一个函数可以将琐碎的输入映射到琐碎的输出,因此这种简单性表达式的作用并不明显。但它们不仅有用,而且是区块链上唯一允许使用的表达式!

那么,策略是什么呢?其实有两个:一个是在地址中提交的简化程序有漏洞,只有在实际花费硬币时才会填上;另一个是简化程序有副作用,可以访问区块链数据或提前终止,从而跳出纯数学函数的界限。

在 Simplicity 程序中有两种方法可以指定漏洞:disconnect 组合器和 witness 器。而见证则非常简单:见证组合器会返回一个给定类型的值,称为 witness(如数字签名、散列预映像或签名密钥的特定选择)。

Simplicity 还有两种支持副作用的方法:一种是内省事务数据(我们将在后面的文章中详细讨论),另一种是断言。断言会停止程序的执行。在比特币脚本中,VERIFY操作码用于断言,当程序遇到无效签名或其他数据时,它允许程序失败。EVM 使用 STOP 操作码来达到同样的目的。

我们现在可以看到,一个程序的输入和输出类型在名义上是微不足道的,但实际上却能进行有用的计算:见证作为程序输入的目的,而断言则提供 "通过/失败 "的程序输出。

我们再来看一个例子。下面是一个程序,它获取两个证人并检查它们是否相等:

-- Witnesses
wit1 := witness : 1 -> 2^32 
wit2 := witness : 1 -> 2^32 

-- Program code
pr1 := pair wit1 wit2 : 1 -> 2^64
jt2 := jet_eq_32      : 2^64 -> 2
cp3 := comp pr1 jt2   : 1 -> 2
jt4 := jet_verify     : 2 -> 1

main := comp cp3 jt4  : 1 -> 1

我们可以从下往上阅读这个程序:程序本身是一个名为 main 的表达式,类型为 1->1。 这里,表达式的 "类型 "表示它的输入和输出值。1 类型只有一个值,因此不描述任何信息。2 类型有两个可能的值,因此它可以表示单个位,2^32 表示 32 位字符串,以此类推。

从底部的等式中,我们可以看到 main 是名称为 cp3 和 jt4 的表达式的组合。那么 cp3 本身就是 pr1 和 jt2 的组合,以此类推。这个程序中使用了五个组合器:

  • comp, 或 composition, 会使用两个表达式,并以第一个表达式的输出作为输入对第二个表达式进行运算。
  • pair 接收两个表达式,并生成一个新表达式,其输出是一对值:左侧部分是第一个表达式的输出,右侧部分是第二个表达式的输出。
  • witness 不需要输入,但它的输出是多态类型:程序所需的任何类型都是它的类型。它产生的值是在评估时提供的值。
  • jet_eq_32 是一种 jet, 这意味着它是一个单独的组合器,可以替换一个更大的简化表达式。被替换的表达式称为其规范,简繁体解释器可以通过评估规范或使用具有相同效果的优化机器码来评估喷流。这个特殊的喷射器接收两个 32 位值,并输出一位,表示这两个值相等(1)或不相等(0)。
  • jet_verify 也算是一种 jet. 该程序将一个位作为输入,如果该位为 0,则中止程序。它没有输出。

结论

在这篇密集的博文中,我们看到了 Simplicity 代码的样子,并发现即使是看似简单的功能,在明确写出来时也会显得相当复杂。但这种复杂性反映了内部实际发生的事情。作为一种规范语言,Simplicity 允许我们将一切明确化,这样我们就可以对其进行数学建模,证明我们的应用程序所需的基本属性,然后对其进行封装,从而确信我们的代码有了坚实的基础。

简单性还有更多的组合器和许多喷射器,我们将在以后的文章中介绍。随着语言的逐步完善,我们将探索更多的实际例子,并研究 "证明 "程序属性的意义。

下一篇文章将介绍 "共享 "的概念,它允许将两个相同的表达式合并为一个表达式,并介绍与 "相同 "的含义有关的一些微妙之处。

加入 GitHub 上的 Simplicity 讨论,提出问题、与社区交流并分享您的见解。在 Twitter 上关注我们 @blksresearch,随时了解 Simplicity 博文发布的最新动态。

If you have specific preferences, please, mark the topic(s) you would like to read: