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

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

↣ ((b∧ms 1 )∨(¬b∧ms 2 ),σ i−1 , s i ,i) IF
↣ (ms 2 ,σ i−1 , s i ,i) B4, T1, F1, F2, (5)
∗
′
→ (true,σ,∅,|σ|+1)∧(α ⊢ µ ∼ s |σ| ) (4)
(7) ⇔ P(if (e) stmt 1 else stmt 2 ,µ,µ ,out) TER, (6)

′
3) 规则 (S-2)、(S-3) 与 (S-4) 处理 return 返回语句, 对于带有返回值的“return e”语句, SOL2M 转换器转换时引
rflag 标志语句是否具有返回值.
入变量 RVal 存储返回值, 以及变量
4) 规则 (S-7) 与 (S-8) 是处理顺序语句“ stmt 1 ; stmt 2 ”, TranStmt(stmt 1 ; stmt 2 ) = “ms 1 ;ms 2 ”. 其中 ms 1 = TranStmt
(stmt 1 ) ms 2 = TranStmt(stmt 2 ). 对于规则 (S-7), 其中 stmt 1 正常执行结束, 不存在 return 语句或是执行失败, 其证明
,
如下:
(1) α ⊢ µ ∼ s i 已知条件
(2) p,g,l, f ⊢ stmt 1 ,µ ⇒ Normal,µ 1 ∧ P(stmt 1 ,µ,µ 1 ,Normal)∧
p,g,l, f ⊢ stmt 2 ,µ 1 ⇒ out,µ 2 ∧ P(stmt 2 ,µ 1 ,µ 2 ,out) 归纳假设
)
∗ (

(3) ⇒ (ms 1 ,σ i−1 , s i ,i) → true,σ j ,∅, j+1 ∧α ⊢ µ 1 ∼ s j ∧
( ) ∗
ms 2 ,σ j−1 , s j , j → (true,σ,∅,|σ|+1)∧α ⊢ µ 2 ∼ s |σ| TER, (1, 2)
(4) ⇒ (ms 1 ;ms 2 ,σ i−1 , s i ,i)

∗
→ (empty;ms 2 ,σ j−1 , s j , j) (3)
( )
↣ ms 2 ,σ j−1 , s j , j CHOP

∗
→ (true,σ,∅,|σ|+1)∧α ⊢ µ 2 ∼ s |σ| (3)

(5) ⇔ P(stmt 1 ; stmt 2 ,µ,µ 2 ,out) TER, (4)
对于规则 (S-8), stmt 1 为 return 语句或是执行失败时, 其证明同理可得.
le = e ”, 规则 le = e ”的操作语义, 赋值语句的操作语义与其一致.
5) 对于赋值语句“ (E-7) 给出了赋值表达式“
,
TranStmt(le = e) = la := ra”, 其中 la = TranExp(le) ra = TranExp(e).
“
(1) α ⊢ le∼ e la 定理1
(2) α ⊢ e∼ e ra 定理1
(3) α ⊢ µ ∼ s i 已知条件
l l
(4) p,g,l ⊢ le ⇒ addr ∧(la,σ i−1 , s i ,i) ⇒ (bl, j m ) 假设

(5) ⇒ α ⊢ load(S,addr, sizeof (τ s )) ∼ ptr(bl, j m ) 定义2, 4, (1, 3, 4)
(6) p,g,l ⊢ e ⇒ v s ∧(ra,σ i−1 , s i ,i) ⇓ v m 假设
(7) ⇒ α ⊢ v s ∼ v m 定义3, 4, (2, 3, 6)

在 MSVL 程序中有:
l
(8) s (x m ) = (bl, j m ) 假设
i
(9) (la := ra,σ i−1 , s i ,i)
)
(
↣ (〇 x m ⇐ v m ∧empty ,σ i−1 , s i ,i) UASS, (8)
( )
→ ( x m ⇐ v m ∧empty ,σ i , s i+1 ,i+1) TR1
( l r )
↣ (empty,σ i , s , s [v m /x m ] ,i+1) MIN1
i+1 i+1
(10) ⇒ s l (x m ) = (bl, j m )∧ s r (x m ) = v m (9)
i+1 i+1
在 Solidity 程序中有:
l
(11) (α ⊢ µ ∼ s i )∧ s (x m ) = (bl, j m )∧α ⊢ load(S,addr, sizeo f (τ s )) ∼ ptr(bl, j m ) (3, 5, 8)
i
l

(12) ⇒ p,g,l ⊢ x s ,µ ⇒ addr 定义1
(13) store(S,addr,τ,v s ) = S 假设
′
l
(14) ⇒ p,g,l ⊢ x s ,µ ⇒ addr ∧load(S ,addr, sizeof (τ s )) = v s E-9, (12, 13)
′
′