Page 149 - 《软件学报》2021年第6期

韩宁 等:以太坊中间语言的可执行语义 1723

二元组的列表 es_pts,再用库函数 foldl 遍历该列表,检查每个二元组(e,t)中实参表达式 e 的类型检查结果是否与
类型名称 t 相对应.若本步检查通过,则函数调用表达式为良类型.此时,若函数无输出参数(|rtl|=0,亦即无返回
值),则可确定函数调用的类型为语句类型(ETypable StmtType vte);否则,函数调用的类型为数据类型(ETypable
(DataType rtl) vte).
以上定义中,第 5 行所涉及的技术细节无关对该类型规则的直观理解,故关于其意义不再赘述.
代码块的类型规则借助表达式列表的类型检查函数 type_es 实现如下:
type_b vte xs fte (Blk es)=(case (type_es vte xs fte es) of (b,vte′)⇒b).
其中,type_es vte xs fte es 在代码块类型检查所用的变量类型环境 vte、外层声明变量集合 xs 和函数类型环
境 fte 下,给出类型检查结果 b(True 或 False)以及经过 es 中所有表达式更新的变量类型环境 vte′,而 b 被直接用
作代码块的类型检查结果.类型检查函数 type_es 具有如下定义.
1. type_es vte xs fte es=
2. foldl(λacc e.(if (fst acc) then
3. (case type_e(snd acc) xs fte e of (ETypable StmtType vte′)⇒(True,vte′)|_⇒(False,(snd acc)))
4. else acc))
5. (True,vte) es
本定义利用库函数 foldl 对表达式列表 es 中的各个表达式逐一进行类型检查,要求各个表达式均为语句类
型(StmtType).对 es 中的每个表达式 e,若其前面的表达式均通过检查,则 e 的类型检查所使用的变量类型环境由
e 前面所有表达式的类型检查更新得到.

5 Yul 语言小步语义的定义和形式化

5.1 语义函数

Yul 语言小步语义的形式化通过定义语义函数进行.语义函数 step 和 step_ctx 在 Isabelle 中类型见表 2.函数
step 给出在当前交易环境(tre::trans_env)下,当前栈(gstk::gstack)执行一步后的结果(gstk′::gstack).函数 step_ctx
表示表达式(e::expr)在上下文(ec::ectx)中的单步执行.两个语义函数的定义相互递归.
Table 2 Semantic functions and structures in Yul
表 2 Yul 的语义函数和函数中包含的结构
step :: “trans_env⇒gstack⇒gstack”
step_ctx :: “trans_env⇒expr⇒ectx⇒gstack⇒gstack”
trans_env = (| oaddr::address
gprice::“256 word” (交易环境)
bheader::blk_header|)
gstack = “gstack_frame list” (全局栈)
表 2 中,交易环境类型 trans_env 记录交易过程中初始交易账户地址 oaddr,每单位 gas 的价格 gprice 和区
块头 bheader 的信息.这些信息在同一交易的执行过程中保持不变.
全局栈类型 gstack 用来跟踪合约所作外部调用,其每一个栈帧通常包含一个被调合约执行时的控制状态
(仍需执行的程序代码)、变量状态、函数标识符和函数定义的绑定状态、链上所有账户的状态(包括余额、存
储等)、被调合约和调用者的地址、交易转移的金额、输入数据、gas 余量等信息.其中,被调合约的控制状态、
变量状态、函数标识符和函数定义的绑定状态这 3 项信息对被调合约所作的每一个内部调用以及所进入的每
一个局部代码块分别保存,形成一个局部栈(类型为 lstack).全局栈帧也可反映合约发生异常或终止执行的状态,
从而包含其他信息,详见下文.
全局栈形式化为全局栈帧列表,表头对应栈顶.全局栈帧由符号 gfrm 表示,有 3 种可能的形态:表示正常执行
状态的全局栈帧〈lstk,gs,ck〉 N 、表示异常状态的全局栈帧〈ck〉 E 和表示合约执行终止的全局栈帧〈gs,ret_data,ck〉 H .
表示正常执行状态的全局栈帧包括局部栈(lstk::lstack)、全局状态(gs::gstate)和外部调用类型(ck::call_kind);表