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

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

仅当以下条件成立:
′ α ⊢ µ ∼ s i , 并且在 p,g,l, f ⊢ stmt,µ ⇒ out,µ , 那么 中一定
′
对于任意的 µ, s i ,µ ,out, 如果有 Solidity 中有 MSVL
∗
′
存在某个 σ 满足 (ms,σ i−1 , s i ,i) → (true,σ,∅,|σ|+1), 且 α ⊢ µ ∼ s |σ| .
定义 6 描述了 Solidity 语句与 MSVL 语句的等价定义, 其含义为如果 Solidity 语句与 MSVL 语句在执行前的
状态等价, 那么执行后的状态也等价.

3.3 表达式等价性证明
定理 1. 通过 SOL2M 转换器, 将 Solidity 表达式 e 转换为 MSVL 表达式 a, 记为 a = TranExp(e). 对于给定的
内存注入 α, 任意的 µ ∈ S, s ∈ M, 如果 α ⊢ µ ∼ s, 则 α ⊢ e∼ e a.
证明: 对 e 的结构使用结构归纳法对定理进行证明. 归纳奠基:

1) 对于常数 c, 显然成立.
,
2) 对于变量 id s id m = TranExp(id s ), 其中 id s 和 id m 均为左值表达式.
(1) α ⊢ µ ∼ s 已知条件
( )
l
l

(2) ⇒ ∀δ m ,addr,i m ,µ. p,g,l ⊢ id s ,µ ⇒ addr ∧ s (id m ) = (bl,δ m ) →
α ⊢ load(S,addr, sizeof (τ s )) ∼ ptr(bl,i m ) E-1, 定义1, (1)
l
l
(3) (id m ,σ, s,|σ|+1) ⇒ s (id m ) L1
( )
l l

(4) ⇒ ∀δ m ,addr,i m ,µ. p,g,l ⊢ id s ,µ ⇒ addr ∧(id m ,σ, s,|σ|+1) ⇒ (bl,δ m )
→ α ⊢ load(S,addr, sizeof (τ s )) ∼ ptr(bl,i m ) (1, 2, 3)
(5) ⇔ α ⊢ id s ∼ l id m 定义2, (4)
(6) ⇒ α ⊢ id s ∼ e id m 定义4, (5)

3) 对于类型为 τ 的一维数组元素, Solidity 中表示为 le[e], 其中 le 为 id, MSVL 中表示为 id m [ra], 其中 id m [ra] =
,
e
,
TranExp(le[e]) ra = TranExp(e) id m 、le、id m [ra] 和 le[e] 均为左值表达式, 和 ra 均为右值表达式. E-2 为反向
使用, 因为数组元素的位置具有唯一性, 由首地址与偏移量决定, 所以可进行逆向推理.
(1) α ⊢ le∼ e id m ∧α ⊢ e∼ e ra 归纳假设
(2) α ⊢ µ ∼ s 已知条件
l
(3) p,g,l ⊢ le[e],µ ⇒ addr +i s 假设
l ( ( ))
(4) E-2, (3)
⇒ p,g,l ⊢ le,µ ⇒ addr ∧ p,g,l ⊢ e,µ ⇒ v s ∧ i s = v s · sizeo f τ s le
l
(5) (id m [ra],σ, s,|σ|+1) ⇒ (bl,i m ) 假设
l

(6) ⇒ (id m ,σ, s,|σ|+1) ⇒ (bl,0)∧(ra,σ, s,|σ|+1) ⇓ v m ∧i m = v m · sizeof (τ m ) L2, (5)
l l
(7) (id m ,σ, s,|σ|+1) ⇒ (bl,0)∧ p,g,l ⊢ le,µ ⇒ addr ∧(ra,σ, s,|σ|+1) ⇓ v m ∧ p,g,l ⊢ e,µ ⇒ v s (4, 6)
(8) ⇒ α ⊢ load(S,addr, sizeof (τ s )) ∼ ptr(bl,0)∧α ⊢ v s ∼ v m 定义2, 3, 4, (1, 2, 7)

(9) ⇒ α ⊢ load(S,addr, sizeof (τ s )) ∼ ptr(bl,0)∧v s = v m v s 与v m 均为整型数值, V1, (8)

(10) ⇒ α ⊢ load(S,addr +v s · sizeof (τ s ), sizeo f (τ s )) ∼ ptr(bl,v m · sizeo f (τ m )) 引理1, (9)

(11) ⇒ α ⊢ load(S,addr +i s , sizeo f (τ s )) ∼ ptr(bl,i m ) (10)
(12) ⇔ α ⊢ le[e]∼ l id m [ra] 定义2, E-2, R5, 假设, (11)

(13) ⇔ α ⊢ le[e]∼ e id m [ra] 定义4, (12)

二维数组同理可证, Solidity 中表示为 le[e 1 ], 其中 le 为 id[e 2 ].
,
4) 对于结构体成员变量, Solidity 中表示为 le.id s , MSVL 中表示为 la.id m , 且 la.id m = TranExp(le.id s ) la =
,
TranExp(le) le、la、le.id s 和 la.id m 为左值表达式, id m 和 id s 均为右值表达式. Solidity 程序中结构体 Struct s 成员
λ 中的第 个成员, 转换为 MSVL λ 中的第 个成员. 假设结构体成员列表中
列表 k 程序中结构体 Struct m 成员列表 k
第 i 个成员的类型为 τ i . field_offset(id,φ) 返回结构体成员列表 φ 中成员变量 id 在内存中的偏移量, 为了简化书写,