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

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

足时抛出异常;
(6) 函数 transferFrom:从指定账户 from 向指定账户 to 转移数量为 amount 的代币,若账户 from 不允许本
账户提取额度 amount、from 余额不足或账户 to 接受数量为 amount 的代币会引起溢出,则抛出异常.

6.2 代币合约的形式化及类型检查
本节在 Isabelle/HOL 中对 MyToken 代币合约进行形式化建模,并利用已形式化的类型检查函数对其进行
类型检查.代币合约的形式化代码 mytoken_code 如下所示,该代码由 1 段派遣程序(dispatcher)、6 个接口函数、
13 个辅助函数的形式化构成:
definition mytoken_code::block where
“mytoken_code=Blk(dispatch_logic_my_token@[total_supply_func,...,(*函数定义*),...,log_func])”
派遣程序是由 if 表达式和 switch 表达式组成的表达式列表,如下所示,其主要功能是根据用户调用合约时
所提供的输入数据将调用转到合约中具体的接口函数.
1. definition dispatch_logic_my_token::“expr list” where
2. “dispatch_logic_my_token=[
3. EIf (EFunCall b_gt_id[EFunCall b_callvalue_id[ ],lit_zero]) (Blk[revert_zz_call]),
4. ESwitch (EFunCall f_selector_id[ ])
5. [
6. (((NL 0x095ea7b3):L U256),
7. Blk[(EFunCall f_approve_id
8. [EFunCall f_decode_as_address_id[lit_zero],EFunCall f_decode_as_uint_id[lit_one]])]),
9. …
10. (((NL 0xa9059cbb):L U256),
11. Blk[(EFunCall f_transfer_id
12. [EFunCall f_decode_as_address_id[lit_zero],EFunCall f_decode_as_uint_id[lit_one]])]),
13. ]
14. (Some (Blk[revert_zz_call]))
15. ]”
该部分(形式化)代码首先判断调用合约时是否存在以太坊原生数字货币的转账.由于代币合约管理代币而
非以太坊原生数字货币,故不接受原生数字货币转账,当该转账数额大于 0 时,使合约异常终止,回滚状态(第 3
行).若无原生数字货币转移发生,则正式进入派遣逻辑,利用 selector 函数得到全局状态中交易输入数据 input
的前 4 个字节,并把该 4 个字节作为 switch 表达式中的变量表达式(第 4 行),利用变量表达式分别与 switch 中各
个匹配项进行匹配:匹配成功,则执行该匹配项中的代码;否则,执行默认项中的代码.每个匹配项中的常量值(如
第 6 行的 0x095ea7b3)为对应函数签名的哈希值,这是对 Solidity 语言实现中所用约定的反映.实际上,使用 Yul
语言直接编写合约,不一定遵循该规范进行.
在 Isabelle/HOL 中执行代码块类型检查函数 type_b 所得结果“True”表明,MyToken 合约为良类型,即该合
约的派遣程序以及所有函数定义均满足类型规则.
value “type_b [] {} fte_blk_mytoken mytoken_code” 结果:(“True”:: “bool”)

6.3 接口函数执行的模拟
本节演示 MyToken 合约在 Isabelle/HOL 中按照小步语义的执行,具体考虑用户输入引起合约中 transfer_
func 函数执行的情况.
定义初始全局栈 gstk_token_contract,其中:唯一的全局栈帧含有全局状态 gs_init 和一局部栈;唯一的局部
栈帧含有 MyToken 合约代码 mytoken_code.