合约设计¶

RChain合约是一个具有明确规定的、表现良好的并且被形式化验证过的程序，它可以与其他合约程序交互。

在本小节中，我们通过Rholang的设计思路来介绍智能合约。首先, 我们给出了 RChain 平台上智能合约的概述。之后, 我们描述了RChain用于实现形式化验证的核心模型, 并在 RChain 系统层上对并发进行建模。然后, 我们将探讨如何将该核心模型进行扩展, 以适应业界的接口语言标准, 如反射、并行、异步、响应式数据流和编译时安全类型检查。

合约概述¶

从宽泛的’合约’的定义来讲，一个智能合约是一个具有以下内容的过程:

持久化状态
相关代码
相关的RChain地址

要记住的一个要点是智能合约具有任意复杂度的特性。它可能是一个原子操作或是一个构成复杂协议的协议超集。

一个合约可以被外部网络代理的信息所触发，外部代理可以是一个合约或一个网络用户。

一条信息：

触发信息通过指定通道发布，该通道可以是公开的或私人的。
触发消息可能是格式范围内的任何值，从一个简单值到一个无序的字节数组、一个变量、一个数据结构、一个过程的代码以及介于该范围之间的大多数事物。

代理在指定通信信道上发送和接收消息，该信道称为“命名通道”。

一个命名通道：

是一个 “定位”, 独立进程将确保同步该位置。
用于节点之间信息发送和接受的过程。
是不可猜测和匿名的，除非在处理过程中被特意引入。

通道被实现为在“只读”和“只写”进程之间共享的变量。因此，通道的功能仅受限于解释一个变量的含义。由于通道代表了“定位”的抽象概念，因此可能会采用不同的形式。对于我们的早期解释，命名通道的功能可以从单个服务器的本地存储器地址（变量）到分布式系统中节点的网络地址。

与该解释一致，一个区块链地址是经过命名的通道，即一个代理可以到达的位置。

两个合约在名为“Address”的通道上发送和接收信息：

这个模型描述了两个合约，它们都可以接收和发送消息。在某个时刻，一个外部actor会提示 Contract1 在通道 address 上发送了一个值 v ，该 address 是 Contract2 的地址。同时，Contract2 监听 address 通道上的值 v。在收到 v 后， Contract2 继续将 v 作为参数并调用后续操作。最后两个步骤是按序发生的。

注意，这个模型假设发送者拥有 Contract2 的地址。还要注意的是，在发送者发送了 v 后，Contract1 已经运行终止。因此，除非提示，它不能再发送任何信息。类似地，在它继续调用后续操作之后，Contract2 也运行到终止状态，因此它不能再监听任何其他消息。

RChain合约用有良好的内部并发性，这意味着这些流程以及任何不相互依赖的流程都可以并行组合执行。所以我们修改了我们的符号：

与其他许多进程并行执行时，外部actor会提示 Contract1 在通道 address 上发送了一个值 v，该通道即 Contract2 的地址。如果 Contract1 没有值要发送，该通道将会阻塞。如果 Contract2 没有收到任何值，它会阻塞信道且不会触发后续调用操作。

交易¶

交易语义如何符合我们对合约的描述？从过程层面上来看，一个交易就是确认一条消息已经被“见证”在一个信道上。

消息本身就是虚拟的对象，但一个合约的前置状态和后置状态指的是代理发送一条消息之前和之后的状态，这些状态被另一个代理见证，打上时间戳并被记录在存储器中，也被称为（在观念上）“区块链”。

消息传递是一个原子操作。无论一条信息是否被见证，只有成功见证的消息才有资格作为一条可验证的交易并被放入一个区块中。迄今为止，我们的例子描述了原子协议本身，但是完整的应用程序可以在运行时产生、发送和接收数以万计的信道。因此，当一些资源的价值被一个过程所改变和见证时，通过代理记录它在什么时间和地点被见证了该改变。这个实现与将数据解释为线性资源是一致的。

在发送消息之前和之后, RChain拥有在信道的任一端放置消息的能力,因此查看消息的序列化形式是RChain的特定属性。此外, 通过将成功的消息声明为交易, 所有消息 (无论是从外部用户到合约，还是在合约之间) 都将被解释。因此, 我们平衡了合约的可扩展自治性和职责。

有关此模型如何适应响应式编程的行业趋势的范例, 请观察以下两个合约, 基于 “实时” 数据源上的交互模型:

与多个其他进程组合并行执行时, Contract1 会被提示在信道 address 上发送一组值 vN，即 Contract2 的地址。在这种情况下，读者将会注意到 Contract2 作为一个线程，它监听一组值作为单个数据流的输入，这与一个流末端的输出的一组值是双向的。当信道 address 见证了一组值 v1…vN 时，将使用 v1…vN 作为参数来调用后续一些操作。虽然 Contract1 和 Contract2 之间的交互是异步的，输入操作 address?(v1...vN) 和 Contract2 的 Continuation(v) 必然是连续的。在每个实例中 address?(v1…vN) 被称为 Continuation(v) 的前缀。

我们对 RChain 平台上的并发合约的交互进行了非常基本的描述, 包括合约、将地址识别为通信信道以及把成功地通过上述信道传递的消息看作交易。接下来, 我们将概述形式化构建了这些结构的核心系统。

形式化模型: Rho演算¶

形式化验证是许多关键任务技术的实际标准。一些最早的形式化验证方法被应用于核电机组的两级停堆系统 [1]。许多ATM软件解决方案通过从线性时序逻辑模型推导解决方案来验证性能表现。许多军事信息和决策系统调用Hoare逻辑来验证碰撞容忍度。一个不加选择的智能合约工具, 它要求托管的关键任务合约, 对其用户负有相同的可验证责任。因此，我们的接口语言和执行模型的设计方法是基于一个可证明其正确性的计算模型 [2]。

同时，能够处理其核心模型中并发进程的编程范式和语言也相对较少。相反, 他们不采用一些基于线程的并发模型, 而是通过一次做多个事情来解决可扩展性问题。相比之下，移动过程计算为“计算是什么”提出了一个完全不同的概念。在这些模型中，计算主要来自过程的交互。为了形式化验证一个执行模型，并允许该执行模型从根本上支持并发，这就是我们替RChain的计算模型选择了一个进程演算模型的原因。

具体来说，RChain执行模型源于rho演算的语法和语义。rho演算是π演算的一个变种，π演算于2004年被推出，它是第一个提出使用反射策略的并发计算模型。 “Rho”代表反射的，高阶的。

虽然对本文的目的来说，理解π演算是不必要的，但还是强烈鼓励那些不熟悉π演算的人去学习和探索π演算相关知识。 π演算是第一个成功构建网络的形式化系统，其中节点可以定期加入网络并从网络中退出。它假设细粒度的并发和进程通信，即两个进程可能由第三个进程引入。 rho-calculus扩展继承了所有这些特性，并添加了反射。

有关更多信息, 请参见 The Polyadic Pi-Calculus 和 Higher Category Models of the Pi-Calculus.

反射¶

目前，反射被广泛认为是实用编程语言的一个关键特性，广义上被称为“元编程”。反射是一种规范的方式，它将程序转换为程序可以操作的数据，然后将修改后的数据转换成新的程序。 Java、C＃和Scala最终都将反射作为其核心特性，甚至OCaml和Haskell最后也开发了反射版本 [3]。原因很简单：在工业规模上，程序员使用程序来编写程序。如果没有这种能力，编写先进的工业规模的程序将花费太长的时间。

语法和语义¶

rho演算构造“名字”和“进程”。类似于π演算，名字可能是沟通的信道或一个值。然而，在加入“反射”的rho演算中，一个名字也可能是一个“引用”的进程，其中一个引用的进程是一个进程的代码。在接下来的章节中，名字的通用性将变得尤为重要。

从名称和过程的概念，该演算建立了一些基本的“进程”。进程可能具有持久状态，但并不假设它一定成立。术语“进程”是“智能合约”中较为通用的术语。因此，每一个合约都是一个过程，但不是每一个进程都是智能合约。

Rho演算构建了以下基本术语来描述进程之间的交互：

P,Q,R ::= 0                  // nil or stopped process

          |   for( ptrn1 <- x1; … ; ptrnN <- xN ).P // input guarded process
          |   x!( @Q )       // output
          |   \*x\           // dereferenced or unquoted name
          |   P|Q            // parallel composition

x,ptrn ::= @P                // name or quoted process

前三个术语用于表示I/O，用于描述消息传递的动作：

0 表示惰性或停止进程的，是模型的基础
输入项 for( ptrn1 <- x1; … ; ptrnN <- xN )P 表示是输入守护进程 P ，在一组信道 xN 上监听一组模式 ptrnN。在接收到这样的模式时, 调用附加部分P [4]。Scala程序员会注意到“for-comprehension”是单子化处理信道访问的语法糖 [5]。结果就是所有的输入通道都服从于模式匹配，这就构成了各种输入守护。
输出项 x!( @Q ) 在通道上 x 发送名字 @Q。尽管在 x 上发送的名字可能是一个值、一个通道或一个被引用的进程（它本身可能包含许多信道和值），我们的符号使用 @Q 来重申名字的表达能力。

下一个项是一个结构性的，描述并发：

P|Q is the form of a process that is the parallel composition of two processes P and Q where both processes are executing and communicating asynchronously.

另外两个项被引入来提供反射：

@P 这个“反射”项引入了“引用进程”的概念，引用过程是一个进程的代码，它被序列化并且通过信道发送。
x 这个“修改”项，允许引用的进程从一个信道上接收并反序列化。

这个语法给出了包含Rholang类型系统原语的基本项。 rho演算假设名称上的内部结构，在进程之间传递时被保留下来。能够探索名字的内部结构的一个结果是，进程可以被序列化到一个通道，然后在被接收时被反序列化，这意味着进程不仅可以相互传递信号，还可以将完整形式的进程发送给其他人。因此是更高阶的扩展。

Rho演算也给出了一个单一可归约（替代）规则来实现计算，被称为“COMM”规则。归约是原子性的; 他们要么发生，要么不发生。这是直接归约rho演算中项的唯一规则：

for( ptrn <- x ).P | x!(@Q) -> P{ @Q/ptrn } //Reduction Rule

COMM规则要求两个进程是位于并发执行的。它还要求两者处于同信道关系。也就是说，一个进程正在从通道 x 中读取，而另一个进程正在写入通道 x。这两个进程被称为“同步”于 x。输入进程并行地在 x 等待符合某模式，记为 ptrn 的数据到来。在模式被匹配到后，执行后续代码 P。归约之后，简化的项表示 P，它将在某个环境下运行，其中 P 绑定到 ptrn。也就是说，在 P 的代码体中，出现的每一个 ptrn 都会被替换为 @Q。

COMM规则意味着通过信道可以成功地传递消息。读者可能还记得，通过一个信道成功传递一条信息可以构成一个可证实的交易。事实上， 一个归约是一个事务 ，正是因为它证实了一个资源已被访问和修改。结果， 归约执行的次数对应于所执行的原子计算数量，它们基本上与提交给一个块的事务数有关。 这种对应确保所有平台计算都是可无区别可量化的。

能够探索名字的内部结构的另一个含义是，信道可能封装更多的信道。虽然它们在原子意义上是非常轻量级的，但是当信道具有内部结构时，它们可以用作数据存储，数据结构，以及任意深度的可证明的无限队列。实际上，在几乎所有的实现中，一个合约的持久存储由存储在一个通道 state 中的状态值组成，接受请求 set 来设置值，用 get 来后去一个新的值 newValue。我们将在名称空间这一节中展示内部结构对信道的广泛影响。更多详细信息，请参阅 A Reflective Higher-Order Calculus 和 Namespace Logic - A Logic for a Reflective Higher-Order Calculus。

行为类型¶

一个行为类型是一个对象的一个属性，它将对象绑定到action模式的一个离散范围内。行为类型不仅限制输入和输出的结构，而且还限制在不同条件下通信和（可能地）并发进程之间允许的输入和输出的顺序。

行为类型特定于移动过程计算，特别是由于非确定性移动计算的引入和适。更具体地说，并发模型可以引入多个场景，在这些场景下可以访问数据，但并不知道这些场景发生的顺序。数据可以在协议的某个阶段被共享，但不能在后续阶段共享。从这个意义上说，资源竞争是有问题的。如果系统不遵守对象的精确共享约束，则可能导致系统改变。因此，我们要求网络资源严格按照规定使用，这些规定描述和详细说明了一系列过程（这些过程表现出了类似的“安全”行为）。

Rholang 行为类型系统将用模态逻辑运算符迭代地修饰相关条件, 它是关于这些条件行为的命题。最终属性数据信息流和资源访问将在类型系统中具体化，该系统支持编译时检查。

行为类型系统Rholang将支持根据其具体代码和行为方式来评估合约集合。因此, Rholang合约将语义提升到类型级别的优势项, 在这里我们能够确定整个协议如何安全地进行衔接。

在他们的开创性论文 Logic as a Distributive Law 中，Mike Stay和Gregory Meredith提出了一种用于从任何一元数据迭代生成空间行为逻辑的算法。

意义¶

这个模型在过去的十年里多次被同行评审过。证明其可靠性的原型已经有近十年的历史了。最小的rho-calculus语法表达了六个原语 - 远远低于以太坊智能合约语言Solidity中的原语，然而这个模型比Solidity能表达的更丰富。特别是，基于Solidity的智能合约不具备内部并发的特性，而基于Rholang的合约则支持内部并发。

总而言之，rho演算的形式化模型是第一个实现下面特性的计算模型：

通过“反射”来实现最大化的代码可移植性，这允许将完整形式的流程作为一级公民来传递给其他网络过程。
借用一个框架，以数学方式来验证反射、通信过程和动态拓扑网络的基本并发系统的行为。
表示一个完全可扩展的设计，自然适应结构化模式匹配、流程延续、响应式API、并行性，异步性和行为类型的行业趋势。

RhoLang — 一种并发语言¶

Rholang是一个功能全面的图灵完整的通用编程语言，它使用rho演算来进行构建。它是一个具备行为类型和反射机制的高阶进程语言（r-eflective, h-igher o-rder process language），也是 RChain官方智能合约所使用的语言。其目的是具体化细粒度的并发编程。

语言必然是面向并发的，重点是通过保护输入信道来传递消息。通道是静态类型的，可以用作单个消息管道、流或数据存储。与类型化的函数式语言类似，Rholang将支持不可变的数据结构。

为了体验Rholang，下面是一个名为`Cell’的合约，它只有一个值并允许客户端获取和设置该参数：

contract Cell( get, set, state ) = {
  select {
    case rtn <- get; v <- state => {
      rtn!( *v ) | state!( *v ) | Cell( get, set, state )
    }

    case newValue <- set; v <- state => {
      state!( *newValue ) | Cell( get, set, state )
    }
  }
}

该合约需要一个 get 请求信道，一个 set`请求信道，以及一个 :code:`state 信道，我们将在状态信道中保存一个数据资源。它等待 get 和 set 信道的客户端请求。客户端请求通过 case 类来进行模式匹配 [6]。

收到一个请求后，合约加入 ; 到一个刚达到的请求 state 信道的客户端。这个连接做了两件事。首先，它从访问中删除内部的 state。同时，又会依次执行 get 和 set 操作，所以它们总是对一个单一的资源副本进行操作 - 同时提供一个数据资源同步机制和一个访问和在 state 更新的操作。

在 get 的情况下，一个请求带有一个 rtn 地址，state 中的值 v 将被发往该地址。由于 v 已经从 state 信道中被取回，它被放回，且 Cell 操作将被递归地调用。

在 set 的情况下，一个请求带有一个 newValue，它被发布到 state 信道（旧值被连接操作所拿走）。同时，Cell 操作将被递归调用。

通过 select 确认，在 Cell 中只有一个线程可以响应客户端请求。这是一场竞赛，失败的线索，无论是getter还是setter操作，都会被杀死。这样，当调用 Cell 的递归调用时，失败的线程不会被挂起，而新的 Cell 进程仍然能够响应客户端的这两种请求。

有关Rholang的更完整的历史叙述，请参阅 Mobile Process Calculi for Programming the Blockchain。

[1]	Lawford, M., Wassyng, A.: Formal Verification of Nuclear Systems: Past, Present, and Future. Information & Security: An International Journal. 28, 223–235 (2012).

[2]	In addition to selecting a formally verifiable model of computation, are investigating a few verification frameworks such as the K-Framework to achieve this.

[3]	查看Scala文档：Reflection

[4]	查看Scala文档：For-Comprehensions

[5]	查看Scala文档：Delimited Continuations

[6]	查看Scala文档：Case Classes