以太坊黄皮书连载(五)

天露   |     |   1077 次阅读

翻译作者:Jorden Gao 邮箱:gaotl33@126.com / tianlu.jorden.gao@gmail.com
微信账号:wa713714
本文作者:Dr. Gavin Wood,以太坊&Ethcore的创始者 邮箱:GAVIN@ETHCORE.IO

公式解释说明:由于网页不默认word公式的格式,以下为公式的解释说明:
1.B_20中为下角标;
2. f
^* ((x_0,x_1,…))≡( f_ (x_0),f_ ^ (x_1),…) 中^为上角标;
3. R_u∈P ∩〖 R〗b∈B_256 中〖 〗忽略不计;
4. D(H)≡ {(D_0^ if H_i^( )=0
{ max⁡〖(D_0^ ,P(H)
(H_d^ )^ +x*ε1+ϵ) if H_i^( )<〗 N_H^( )
{max⁡(D_0^ ,P(H)_(H_d^ )^ +x*ε2+ϵ) otherwise)

中3 { 是一个大个{
若有公式疑问,建议下载原文对应公式看;再次抱歉!(等全文翻译完成,可去百度文库下载全文word形式,此word形式无公式问题)

9.执行模型(“Execution Model”)
执行模型具体说明怎么使用一系列字节代码指令和一个环境数据的小数组去改变这个系统状态。这些是通过一个虚拟状态机的正式形式被具体说明,正如大家所知的以太坊虚拟机(“Ethereum Virtual Machine - EVM”)。它是一个类似完全图灵机器(“quasi-Turing-complete machine”);这个quasi条件是一个这样的事实:算力在内部被限制通过一个参数,燃料,它是限制已经完成的算力总数。

9.1.基础(“Basics”)。EVM是一个简单基于堆栈结构。机制的字大小(堆栈项目的大小)是256位。这些被选择去完成Keccak-256位方案和椭圆形曲线算计。记忆模型(“memory”)是一个简单赋有字地址的字节数组。堆栈最大尺寸为1024。这个机制也有一个不独立存储模型;这类似一个记忆的概念而不是一个字节数组。这个机制是可赋有字地址的字数组。不像可变的记忆模型,存储是不可变的而且是作为系统状态的一部分被保持。在记忆和存储模型中所有的初始化数据被定义为0。
这个机制不跟随标准的诺依曼结构(“Neumann architecture”)。它被特别地存储在只和一个特别指令互动的一个虚拟ROM中,而不是把存储程序代码放在一般可进入的记忆或存储器中。
在某些情况下这个机制有例外的执行,包括堆栈溢出和无效指令。在缺乏燃料(“out-of-gas - OOG”)特例中,他们不会脱离状态去改变完整性。话句话说,这个机制会立即分别暂定和记述这个问题到执行代理人(无论是交易的处理者,还是重复地大量产生执行环境)。

9.2.费用综述(“Fees Overview”)。费用(命名为燃料)被用在三个不同的情况下,在这三种情况下,费用都是执行任何操作的必备条件。第一种情况也是最普通的情况就是计算操作的本身费用(见附件G)。第二中情况,燃料可能被减少因为一个下级的信息调用或者合约创建;这个形成创建,调用和调用代码(“CREATE,CALL, and CALLCODE”)费用中的一部分。第三种情况,燃料可能因为一个记忆模型使用量的上升而被支付。
对于一个账号的执行,可支付的记忆模型用量的总费用是按在一定范围中被包含的所有记忆索引(无论是读还是写)下要求的32位字节的最小倍数成比例的。这个为了实时(“just in time”)的基础而被支付的;同样地,参考任意大于之前索引的至少32字节记忆区间在某种意义下都将导致一个额外的记忆模型用量费用。由于这个非常不像地址的费用曾经超出过32字节的限制。就如上述所说,工作流程必须能够管理这个不可测的事件。
存储的费用有一个极其微小的行为 —— 为了形成存储模型用量的最小化(直接与一个在所有结点上的大型状态数据通信),在存储器中清除一个元素的执行费用不仅仅被免除,而且会返回一些费用;事实上,这个返回的费用是被支付的预先费用,而且消耗的初始化存储模型用量实质上会远远超过正常的用量。
严格的EVM燃料消耗定义见附件H。

9.3.执行环境(“Execution Environment”)。除了系统状态σ,和计算剩余的燃料g,这里还有一些在执行代理人必须提供的执行环境下重要使用过的信息块;他们被包含数组I中:
I_( a)^ ,拥有正在执行的代码的账号地址。
I_( o)^ ,发起执行交易中的发送者地址。
I_( p)^ ,发起执行交易中的燃料价格。
I_( d)^ ,执行中输入数据的字节数组;如果这个执行代理人是一个交易,这个将为交易数据。
I_( s)^ ,触发这个代码执行的账号地址;如果这个执行代理人是一个交易,这个将为交易发送者。
I_( v)^ ,价值,单位为wei,通过这个账号在执行中作为一样工序的部分;如果这个执行代理人是一个交易,这个将为交易的价值
I_( b)^ ,机制中被执行代码的字节数组
I_H^ ,当前区块的区块头
I_e^ ,当前信息调用或者合约创建的深度(比如调用的数值或者当前创建被执行)
执行模型定义为函数Ξ,能计算出最后的状态〖σ_ ^ 〗_ ^',剩余燃料g_ ^',自杀列表s,日记序列l,返回值r和最好的输出o,他们的定义为:
(115) (〖σ_ ^ 〗_ ^',g_ ^',s,l,r,o)≡Ξ(σ,g,I)

9.4.执行综述(“Execution Overview”)。我们现在必须去定义这个函数Ξ。在很多实际的情况下,这将被模型化以整个系统状态σ和机制状态μ的对比作为一个重复的过程。正式的来说,我们定义它用函数X去重复。这个函数使用一个迭代函数O(定义状态机制中单循环的结果)和函数Z ,如果当前状态是一个特例的机制暂停状态,和函数H —— 具体说明这个指令的输出数据如果仅仅当前状态是一个正常的机制暂停状态。
空的序列表示为 ( ),它不等于空的集合∅;这是非常重要的当去理解H的输出数据,赋值到∅会连续执行但是赋值到系列(潜在的空序列)会暂停执行。
(116) Ξ(σ,g,I)≡X_( 0,1,2,4)^ ((σ,μ,A_ ^0,I) )
(117) μ( g)^ ≡g
(118) μ
( pc)^ ≡0
(119) μ( m)^ ≡(0,0,…)
(120) μ
( i)^ ≡0
(121) μ( s)^ ≡( )
(122) X((σ,μ,A
^ ,I))≡{(( ∅,μ,A_ ^0,I,( ) ) if Z(σ,μ,I)
O(σ,μ,A_ ^ ,I)•o if o≠∅
X(O(σ,μ,A_ ^ ,I) ) otherwise)┤
其中
(123) o≡H(μ,I)
(124) (a,b,c) •d≡(a,b,c,d)
注意我们必须舍弃从函数X正确返回和赋值到函数Ξ数组的第四个值,因为这里下角标为X_( 0,1,2,4)^ 。
X是被循环(重复地操作,但是这些工具通常被期待去使用一个迭代的循环)直到Z变成true,表示当前状态是特例和机制必须被暂停而且舍弃全部变化,或者H变成一个系列(是空序列而不是一个空的集合),代表这个机制已经得到了一个可控制的暂停。

9.4.1.机制状态(“Machine State”)。这个机制状态μ是作为一个数组(g,pc,m,i,s)被定义,它们分别可用的燃料,程序计数器pc∈P_( 256)^ ,记忆的内容,在记忆中积极的字数(从0不停的计算),和堆栈内容。这个记忆内容μ( m)^ 是长度为2 ^256值为0的一个空系列。
为了阅读的简单性,记忆的指令以小的大写字母创建(例如 ADD),应该被解释为他们数值的等价;整个指令集在给出的附件H具体说明。
为了定义Z,H和O,我们定义w作为当前被执行的操作:
(125) w ≡{(I_( b)^ [μ( pc)^ ] if μ( pc)^ <||I_( b)^ ||
STOP otherwise)┤
我们也认为被修复的δ和α总和,具体说明了堆栈项目减少和增加,而且都能用指令去描述,并且一个指令消耗函数C将用燃料赋值到给定执行指令的全消耗中。

9.4.2.特例的暂停(“Exceptional Halting”)。特例的暂停函数Z被定义为:
(126) Z(σ,μ,I)≡μ( g)^ <C((σ,μ,I) ) ∪
δw^ =∅ ∪
|(|μ_s^ | )|<δ_w^ ∪
( w ∈ {JUMP,JUMP} ∩
μ
s^ [0]∉D(I
( b)^ )) ∪
|(|μ_s^ | )|-δ_w^ +α_w^ >1024
这些执行都属于特例的暂停的状态:如果这里有不充足的燃料,无效的指令(就是为什么δ的下角标没有定义),不充分的堆栈项目,一个JUMP/JUMPI的目的地是无效或者新的堆栈大小将大于1024。 机灵的读者将很容易的发现在整个执行过程中没有一个指令能直接进入特例的暂停。

9.4.3.跳转目的地的有效性(“Jump Destination Validity”)。我们之前使用D作为一个函数去决定给定
正在允许代码中的有效跳转目的地的集合。我们定义JUMPDEST指令能在正在运行代码中的任意位置。
像这样所有的位置必须是在有效指令边界,而不是使用PUSH操作进入数据的一部分,而且必须出现在被详细说明定义的部分代码中(而不是使用被详细说明定义的STOP指令去跟踪它)。
公式表达为:
(127) D(c)≡D_J^ (c,0)
其中:
(128) D_J^ (c,0)≡{({ } if i≥|c|
{i}∪D_J^ (c,N(i,c[i] ) ) if c[i]=JUMPDEST
D_J^ (c,N(i,c[i] ) ) otherwise)┤
其中N是代码中下一个有效的指令位置,跳过PUSH指令的数据,如果下列任意式子成立:
(129) N(i,w)≡{(i+w-PUSH1+2 if W∈[PUSH1,PUSH32]
i+1 otherwise)┤

9.4.4.正常暂停(“Normal Halting”)。正常暂停函数H被定义为:
(130) H(μ,I)≡{(H_RETURN^ (μ) if w=RETURN
( ) if w∈{STOP,SUICIDE}
∅ otherwise)┤
操作中返回的数据,RETUREN,有一个特别的函数H_RETURN^ ,详细定义见附件H。

9.5.执行循环(“The Execution Cycle”)。堆栈项目是从最左边被增加或减少,低索引的序列部分;剩下的所有项目都被保留不变:
(131) O(σ,μ,A_ ^ ,I) ≡ (〖σ_ ^ 〗',〖μ_ ^ 〗_ ^',A_ ^',I)
(132) Δ ≡αw^ -δw^
(133) |(|μ_s^( ') | )| ≡ |(|μ_s^ | )|+Δ
(134) ∀x∈[α_w^ ,|(|μ_s^( ^' ) | )| ]:μ_s^( ^' ) [x] 〖≡ μ〗_s^ [x+Δ]
燃料通过指令的燃料消耗和大量的指令被减少,程序计数器在每一个循环上增加,对于这三个特例,我们假设了一个函数J,下角标是二个指令中的一个,根据以下的式子赋值:
(135) μ
g^' ≡ μ_g^ -C(〖σ
^ 〗_ ^ ,〖μ_ ^ 〗_ ^ ,I)
(136) μ( pc)^( ') ≡ {(J_JUMP^ (μ) if w=JUMP
J_JUMPI^ (μ) if w=JUMPI
N(μ
( pc)^( ^ ),w) otherwise)┤
在一般情况下,我们认为这个记忆(“memory”),自杀(“suicide”)列表和系统状态不改变:
(137) μ( m)^( ') ≡ μ( m)^
(138) 〖μi^(' ) ≡ μ〗( i)^
(139) A_ ^(' ) ≡ A
(140) σ_ ^' ≡ 〖σ_ ^ 〗_ ^
然而,指令通常会改变一个到几个元素的值。改变的元素会被通过附件H中强调的指令一一列举出来,α和δ边上的值和一个燃料需求的公式描述。

10.区块树到区块链(“Blocktree To Blockchain”)
标准的区块链是一个区块树上所有元素从根到叶子的路径(“path”)。为了形成什么是路径的共识,我们概念性地定义这个路径是已经计算过最长的路径,或者是最重的路径。叶子当前的数值是最清晰的因素去辨别最重的路径,它也是路径中当前区块的数值,不算上没有挖的创世块。随着路径越来越长,总挖矿的影响越来越大而且为了到达叶子上它必须被完成。这是一个已有方案的改进,比如它已经应用在比特币协议(“Bitcoin-derived protocols”)中。
因为一个区块头包含难度(difficult),区块头能充分证明已完成的计算有效性。任意一个区块贡献到总的计算或者区块链的整个难度中。
因此我们重复地定义区块B的难度为:
(141) B_t^ ≡ B_t^'+B_d^
(142) B_ ^' ≡ P(B_H^ )
在给定一个区块B,B_t^ 是它本身总难度,B_ ^'是它本身当前区块和B_d^ 是它本身的难度。

 
0 人喜欢