Page 114 - 《软件学报》2025年第9期

王小兵 等: Solidity 到 MSVL 转换的等价性研究 4025

ra = TranExp(e). E-10 为反向使用, 因为单目运算可逆向操作, 所以可进行逆向推理.
(1) α ⊢ e∼ e ra 归纳假设
(2) α ⊢ µ ∼ s 已知条件
(3) p,g,l ⊢ unope,µ ⇒ v s ∧(mop 1 ra,σ, s,|σ|+1) ⇓ v m 假设

(4) ⇒ p,g,l ⊢ e,µ ⇒ v s1 ∧v s = unop v s1 ∧(ra,σ, s,|σ|+1) ⇓ v m1 ∧v m = mop 1 v m1 E-10, R8, (3)
(5) ⇒ α ⊢ v s1 ∼ v m1 ∧v s = unop v s1 ∧v m = mop 1 v m1 定义2, 3, 4, (1, 2, 4)

(6) ⇒ v s1 = v m1 ∧v s = unop v s1 ∧v m = mop 1 v m1 (5)

(7) ⇒ v s = v m (6)
(8) ⇒ α ⊢ v s ∼ v m V1, (7)

(9) ⇔ α ⊢ unop e∼ r mop 1 ra 定义3, (8)
(10) ⇒ α ⊢ unop e∼ e mop 1 ra 定义4, (9)

8 ) 对 于 S o l i d i t y 中 的 双 目 运 算 e 1 binop e 2 , M S V L 中 有 ra 1 mop 2 ra 2 = TranExp(e 1 binop e 2 ) , 其 中 ra 1 =

TranExp(e 1 ) 且 ra 2 = TranExp(e 2 ) . E-12 为反向使用, 因为双目运算可逆向操作, 所以可进行逆向推理.
(1) α ⊢ e 1 ∼ e ra 1 ∧α ⊢ e 2 ∼ e ra 2 归纳假设
(2) α ⊢ µ ∼ s 已知条件
(3) p,g,l ⊢ e 1 binop e 2 ,µ ⇒ v s ∧(ra 1 mop 2 ra 2 ,σ, s,|σ|+1) ⇓ v m 假设

(4) ⇒ p,g,l ⊢ e 1 ,µ ⇒ v s1 ∧ p,g,l ⊢ e 2 ,µ ⇒ v s2 ∧(ra 1 ,σ, s,|σ|+1) ⇓ v m1 ∧
(ra 2 ,σ, s,|σ|+1) ⇓ v m2 ∧v s = v s1 binop v s2 ∧v m = v m1 mop 2 v m2 E-12, R9, (3)

(5) ⇒ α ⊢ v s1 ∼ v m1 ∧α ⊢ v s2 ∼ v m2 ∧v s = v s1 binop v s2 ∧v m = v m1 mop 2 v m2 定义2, 3, 4, (1, 2, 4)

(6) ⇒ v s1 = v m1 ∧v s2 = v m2 ∧v s = v s1 binop v s2 ∧v m = v m1 mop 2 v m2 (5)

(7) ⇒ v s = v m V1, (6)

(8) ⇒ α ⊢ v s ∼ v m (7)
(9) ⇔ α ⊢ e 1 binop e 2 ∼ r ra 1 mop 2 ra 2 定义3, (8)
(10) ⇒ α ⊢ e 1 binop e 2 ∼ e ra 1 mop 2 ra 2 定义4, (9)

9) 对于 Solidity 中的参数列表 e = (e 1 ,...,e k ), MSVL 中记为 ra = (ra 1 ,...,ra k ) = TranExp(e ). 其中 e i 与
∗
∗
∗
ra i (1 ⩽ i ⩽ k) 均为右值表达式. E-13 为反向使用, 因为参数组成列表为可逆操作, 所以可进行逆向推理.
(1) α ⊢ e i ∼ ra i (1 ⩽ i ⩽ k) 归纳假设
(2) α ⊢ µ ∼ s 已知条件
(3) p,g,l ⊢ (e 1 ,...,e k ),µ ⇒ v s ∧((ra 1 ,...,ra k ),σ, s,|σ|+1) ⇓ v m 假设
(4) ⇒ p,g,l ⊢ e i ,µ ⇒ v si ∧v s = (v s1 , ...,v sk )∧

(ra i ,σ, s,|σ|+1) ⇓ v mi ∧v m = (v m1 ,...,v mk )(1 ⩽ i ⩽ k) E-13, R13, (3)
(5) ⇒ v si = v mi (1 ⩽ i ⩽ k) (1, 2, 4)

(6) ⇒ (v s1 ,...,v sk ) = (v m1 ,...,v mk ) (5)

(7) ⇒ α ⊢ (v s1 ,...,v sk ) ∼ (v m1 ,...,v mk ) V1, (6)
(8) ⇔ α ⊢ (e 1 ,...,e k )∼ r (ra 1 ,...,ra k ) 定义3, (7)
∗
∗
(9) ⇒ α ⊢ (e 1 ,...,e k )∼ e (ra 1 ,...,ra k ) 即 α ⊢ e ∼ e ra 定义4, (8)

10) 对于映射类型 le[e], MSVL 中没有映射类型, 因此使用结构体抽象描述键值对, 用结构体数组 id[ra] 抽象
e
描述映射类型, 满足 id[ra].left 与 求右值相等, 并且有 id[ra].right = TranExp(le[e]). 其中, le[e] 与 id[ra].right 均
为右值表达式. SOL2M 转换器为映射类型在 MSVL 中定义了函数 mapping_map, 其功能是遍历数组找到成员
id[ra].left = l, 且在 MSVL id[ra].right
变量 left 值与参数 l 值相同的结构体, 即满足 中有 l = TranExp(e). 其中 le[e] 与
均为右值表达式. E-7 为反向使用, 因为数组元素的位置具有唯一性, 由首地址与偏移量决定, 所以可进行逆向
推理.