执行模型

2020-04-10 本文已影响0人真是个点子王

执行模型指定在给定一系列字节码指令和一小组环境数据的情况下如何更改系统状态。这是通过一个称为以太坊虚拟机（EVM）的虚拟状态机的正式模型来指定的。它是一个准图灵完备机；准限定来自这样一个事实：计算本质上是通过一个参数gas有界的，gas限制了计算的总量。

一、基础

EVM是一个简单的基于堆栈体系结构。机器的字(word)大小为256位（bit）（因此堆栈元素的大小也是如此）。这是为了方便Keccak256哈希和椭圆曲线计算而选择的。
内存(memory)模型是一个简单的按字寻址的字节数组
堆栈（stack）的最大尺寸为1024
虚拟机同样还有一个独立的存储模型（storage）,这在概念上类似于内存，但它不是字节（byte）数组，而是一个可寻址的字（word）数组。与内存（memory）不同的是，存储是非易失性的，并作为系统状态的一部分被维护。
存储和内存中的所有位置都被初始化为0。
EVM不符合冯诺依曼的标准结构。它不是将程序代码存储在通常可访问的内存或存储器中，而是单独存储在虚拟ROM中，该虚拟ROM只能通过专门的指令进行交互。
由于多种原因，机器可能会有异常执行，包括堆栈下溢和无效指令。机器会立即停止并将问题报告给执行代理做出相应的处理。

费用（以gas计）在三种不同情况下收取，这三种情况都是执行一项行动的先决条件。第一个也是最常见的情况是计算操作的固有费用。其次，对于下属消息的调用或合同的创建也会对gas形成扣除。这构成了CREATE,CALL和CALLCODE支付的一部分。最后，对于内存使用的增加也会支付一部分gas。
在帐户执行过程中，应付内存(memory)的总费用与所需的32字节的最小倍数成正比，以便所有内存索引（无论是读还是写）都包含在该范围内。这是在及时的基础上支付的。因此，引用一个至少比任何以前索引的内存大32字节的内存区域肯定会导致额外的内存使用费。由于这个费用，地址不太可能超过32位的界限。也就是说，实现必须能够管理这种可能性。
存储(storage)费用有一个稍微微妙的行为，以激励存储使用的最小化（它直接对应于所有节点上的一个更大的状态数据库），对于清除存储中某个条目的操作的执行费用不仅被免除，还被给予一个合格的退款；事实上，这个退款是有效地提前支付的，因为存储位置的初始使用成本远远高于正常使用成本。事实上，这种退款是预先支付的，因为存储位置的初始化成本远远高于正常使用成本。

除了系统状态和计算所需的剩余gas外，执行代理必须提供在执行环境中使用的几个重要信息。其包含在一个元组中：
- $I$ _a,拥有正在执行的代码的账户的地址；
- $I$ _o,发起此执行的j交易的发件人地址；
- $I$ _p,发起这次执行的交易中的gas价格；
- $I$ _d,作为此执行的输入数据的字节数组；如果执行代理是交易，则这将是交易数据；
- $I$ _s,导致代码执行的帐户的地址；如果执行代理是交易，则这将是交易发送者；
- $I$ _v,作为执行程序的一部分传递给此账户的值(Wei)。如果执行代理是交易，则这将是交易的Value；
- $I$ _b,要执行的机器码的字节数组；
- $I$ _H,当前区块的块头；
- $I$ _e,当前消息调用或合同创建的深度（例如，当前正在执行的CALLs或者CREATEs）;
- $I$ _w,对状态进行修改的权限。
执行模型定义了函数，它可以计算结果状态^'，剩余gas^'，累积子状态,以及结果输出。在目前情况下，将其定义为：
- （ $\sigma$ ^'， $g$ ^'， $A$ ， $o$ ） $\equiv$ $\Xi$ （ $\sigma$ ， $g$ ， $I$ ）
这里我们记住累积子状态,被定义为一个元组。这个元组包括自毁集_s,日志序列₁，接触账户_t与退款余额_r
- $A$ $\equiv$ （ $A$ _s， $A$ ₁， $A$ _t， $A$ _r）

我们现在必须定义 $\Xi$ 函数。在绝大多数实际的实践中，这将被建模成完整的系统状态 $\sigma$ 和虚拟机状态 $\mu$ 的迭代过程。形式上，我们用函数 $X$ 递归的定义它。这将使用迭代器函数 $O$ （它定义了状态机的一个单循环的结果）以及函数 $Z$ (确定当前状态是否为机器的异常停止状态)和 $H$ ,当且仅当当前状态是机器的正常停止状态时，指定指令的输出数据。
表示为（）的空序列不等于表示为 $\emptyset$ 的空集合。这在解释 $H$ 的输出的时候非常重要，当执行在继续时，它评估为空集，但当执行暂停时，它评估为一个序列（可能为空）。
注意当我们计算 $\Xi$ 时，我们要去除第四个元素 $I$ ^'以及要从结果机器状态 $\mu$ ^'中抽取剩余的gas $\mu$ _g^'
因此， $X$ 被循环（这里是递归地，但实现通常需要使用一个简单的迭代循环）直到 $Z$ 变为真，表明当前状态异常、机器必须中止以及一些改变需要被丢弃；或者 $H$ 变成了一个序列（不只是一个空集）表明机器已经到达了受控中止。

机器状态 $\mu$ 被定义为一个元组( $g$ , $pc$ , $m$ , $i$ , $s$ )，它们分别是可用的gas，程序计数器 $pc$ $\in$ $N$ ₂₅₆，内存(memory)内容，内存中活动的字数目（从0位置开始连续计数）和堆栈内容。内存(memory)的内容 $\mu$ _m是(这里没太看懂，原文a series of zeros of size 2²⁵⁶)
为了方面阅读，助记符应该被解释为它们的数字等价物；
为了定义 $Z$ , $H$ 和 $O$ ，我们将 $w$ 定义为当前要执行的操作；
我们还假设了 $\delta$ 和 $\alpha$ 的固定量，指定栈顶项的删除和添加，以及可下标访问指令和指令损失函数 $C$ ,以评估给定的指令执行的完整代价。（没太读懂TAT）

异常中止函数 $Z$ 被定义为
这表明执行会在以下情况处于中止状态：没有充足的gas，指令无效（以及因为它的下标 $\delta$ 未定义），堆栈空间不足，指令 $JUMP/JUMPI$ 目的无效，新堆栈大小大于1024或者静态调用期间尝试修改系统状态。聪明的阅读者将意识到这意味着任何指令都不能通过其执行而导致异常中止。（这里也有点问题）

我们先前使用函数 $D$ 作为来确定给定代码执行时的有效跳转目标集。我们通过 $JUMPDEST$ 指令将其定义为代码中的任何位置。
所有这些位置必须位于有效的指令边界上，而不是位于 $PUSH$ 操作的数据部分，而且必须出现在代码显式定义的部分（，而不是隐式的定义为其后的 $STOP$ 操作）
形式上，