5.3 语言模型
本文档描述了 Reach 的基本假设与概念。首先，我们探讨在评估模型中运行一个 Reach 项目。然后，我们将围绕 Reach 程序中与 Reach 程序员相关的部分讨论编译模型中的细节。最后，我们讨论语法模型是如何对 Reach 程序进行语法构造的。
5.3.1 评估模型
Reach 程序描述一个去中心化应用（ DApp ），其本质是一个分布式计算，涉及多个参与者利用共识网络上同一个合约对计算获得的中间值达成一致。
“多个”是一个专业术语，意思是“零个或更多个”。
当计算终止时，由于所有参与者对中间值达成一致，故对输出结果也达成一致。
在 Reach 计算开始时，不需要事先知道有哪些参与者，这一信息可以在应用程序的整个执行过程中演化更新。
共识网络是一种网络协议，该协议带有一种网络代币、一组非网络代币、一组账户、一组合约与时间。网络代币是种不透明的记账单位；非网络代币同样是一种不透明的记账单位；典型的共识网络允许一组非网络代币随时间增长并通过账户分发。共识网络的时间是全序集合中的一类单调递增离散值。时间增量代表着两个时间点之间的差值，以离散的时间单位表示。共识网络支持在不同账户间转移网络代币和非网络代币。帐户具备非负数的网络代币余额，是唯一的身份（称为地址）。帐户能以无法抵赖或伪造的方式对值进行签名，这称为发布。“共识网络连接器”一章讨论了 Reach 支持哪些共识网络。
这是对共识网络的一种抽象描述，可能无法由实际网络直接实现。
例如，在基于 UTXO 的网络中，通常没有明确表示的账户余额的账本。然而，这类网络确实抽象地具备带有余额的账户，因为特定的私钥表示账户对某组网络代币具有独占访问权，这就是其余额。
同样，如果你知道许多共识网络是基于区块链的，并且使用链长度（也被称为高度或区块数）作为时间的概念，那 Reach 的时间概念可能显得过于抽象（“单调递增。。。全续集合“）。在这里，时间将是一个自然数，这是典型的全续集合。然而，Reach 可灵活支持基于非区块链的共识网络，因此它也并不强制使用这种基于自然数的时间概念。
最后，Reach 对共识网络的定义并不依托于任何特定的技术或特征。特别是，它不仅指所谓的“Layer 1”协议，也不排斥由受信任方控制网络的中心化系统。
合约是具有三种额外职能的账户：它们持续存储值（称为共识状态），它们可以接收发布，并且当它们接收发布时会进行系统地处理，可以修改其共识状态，制作发布，并且可响应反馈转移网络代币。除了值之外，共识状态还可以包含地址和值之间的固定数量的映射。这些映射被称为“线性状态”，因为它们的大小与合约中参与者的数量成线性关系。合约的创建称为部署。
参与者是参与 DApp 的逻辑角色。它与共识网络上的一个帐户相关联。
参与者具有持续存储的值，称为其本地状态。它有一个与之交互的前端。前端是一个抽象的角色，它支持一组消耗和产生值的函数；当参与者调用其中一个函数时，它被称为交互。
参与者类是那种在单个应用程序中可能出现多次的参与者。参与者类的成员在其作为类成员的状态很重要时称为参与者实例，而在其他情况下仅称为“参与者”。参与者实例与其他实例一样是独立的参与者；例如，具有自己的本地状态、前端等。主要区别在于，当参与者类的成员加入应用程序时，它不像其他参与者那样是固化的，因为参与者实例并不完全代表参与者类。
计算开始时，默认此帐户为空。
在某些共识网络上，向合约账户的转移可能超越了 Reach 的权限。如果发生这种情况，那么这些网络代币将汇给最后一次共识转移的发起者。
任何转移到该帐户的网络代币必须在 DApp 完成时移除。这称为代币线性性质。
DApp 计算可以看作是一个具有唯一第一步的步骤图。步骤是指本地步骤的集合，这一集合由参与者遵循单个共识步骤构成，而单个共识步骤则是由单个共识转移引发的。
本地步骤由单个参与者执行，是一系列本地计算。本地计算可以绑定一块本地状态，断言本地状态的性质，或者与前端交互。共识转移由单个参与者（称为发起人）执行，该参与者基于其本地状态制作发布一组公开值，并将零个或多个网络代币转移到合约帐户。共识转移规定了一个可选步骤，称为超时，如果发起人在给定的时间增量流逝之前未能进行转移，则执行该步骤。所有本地状态最初都是私有的，直到通过解密显式公开，这也是一种本地计算。
参与者在首次制作发布时被识别为加入应用。对于非参与者实例而言，由于其共识状态包含了参与者与特定账户（即地址）的固化关联关系，因此也使得参与者固化。所有来源于已固化参与者的后续发布，均必须来自相应的固化账户。
公式步骤步骤是具有唯一首次计算的共识计算图。共识计算要么绑定共识状态，要么断言共识状态的性质，要么执行转移，要么在不同的下一个共识计算间进行选择，要么与另一个合约（称为远程对象）通信，要么提交到下个步骤。
断言可以是：知识断言，即一个诚实的参与者不能知道另一个诚实的参与者确实知道的东西；状态断言，这是一个永远正确的公式；假设，这是一个基于前端行为诚实的正确公式；要求，这是一个基于参与者行为诚实的正确公式；以及，可能性断言，该公式中存在一些诚实的参与者和前端可以提交的值，通过这些值来确保公式的正确性。诚实的参与者是指执行 DApp 指定步骤的参与者，而诚实的前端是指它们所返回的值，均确保所有假设都是布尔型 true。
值可以是：null 值、布尔值、无符号整数、字节字符串、摘要、地址、固定元组值、定长单一类型数组的值、或固定的值记录。值可以其二进制编码摘要为加密哈希值。
值总是处于三种可能的状态之一。它们可以是共识状态，在这种情况下，其对所有参与者可见。它们可以是单个参与者的本地状态，这意味着只对该参与者可见。本地状态又进一步分为私有本地状态和公有本地状态，发布只能包含后者而不能包含前者。这些状态如图 16 所示。
图16:值的三种状态
5.3.2 编译模型
Reach 程序不能独立于一个共识网络和一组前端之外执行。因此 Reach 的语义抽象地对待这些组件，而不指定它们的语义。所以，Reach 的语义不能直接在虚拟机或解释器中有效地执行。相反，Reach 程序被编译成一个特定的共识网络连接器和一组执行特定共识网络计算的参与者后端。若连接器和后端可靠地为 Reach 定义的抽象语义建模，则它们是可靠的。
在编译过程中无论参与者和前端是否诚实，Reach 编译器都会自动检验代币线性性质、所有静态断言和可能性断言是否为真。类似地，所有的知识断言都采用参与者知识的保守近似值进行检验。保守近似值假定计算的所有输入都由计算结果显示，摘要和交互例外。近似值意味着 Reach 无法推理人工表达的加密公式细节，并会假定这些公式是不安全的。最后，关于知识检查器的一个微妙点是相关的：在 Reach 程序中具有不同身份的技术参与者实际上可能是由同一个参与者实例化的，即如果 Alice 选择与自己下一盘棋，她自己又是黑方又是白方；这种可能性总是存在的，知识检查器并不认为这违反了“白方知道黑方不知道的信息”这一断言。
若无法静态验证这些断言，则编译过程将中止。在验证之后，这类的静态断言和可能性断言将从程序中删除，并且不会在运行时发生。相反，运行时后端强制执行假设，连接器强制执行要求。如果在运行时违反了假设，那么后端将中止。如果在运行时违反了要求，那么连接器会确保 DApp 的所有方面（合约和参与者）都忽略由此产生的共识转移，这通常会导致超时。
5.3.3 语法模型
Reach 程序由源文件中符合语法规则的一组 JavaScript 语法指定。接下来的程序章节将详细描述 Reach 程序的语法。
若有收获，就点个赞吧
0 人点赞
