JPYCv2 形式検証

外観

JPYC.totalBalances_setBalance ​

名称・種別 ​

  • 名称: JPYC.totalBalances_setBalance
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:133-139
  • 概要: 1 回の setBalance が totalBalances に与える効果を自然数上で釣り合わせた補題。
  • 仕様: 対象

型シグネチャ ​

lean
∀ (s : JPYC.State) (i : JPYC.Address) (v : JPYC.U256), Eq (instHAdd.hAdd (s.setBalance i v).totalBalances (BitVec.toNat (s.balances i))) (instHAdd.hAdd (BitVec.toNat v) s.totalBalances)

残高を 1 か所だけ setBalance i v で書き換えたとき、(新 totalBalances) + (旧残高).toNat = v.toNat + (旧 totalBalances) という釣り合いの等式です。

和訳 docstring ​

1 回の setBalance が totalBalances に与える効果を、ℕ 上で釣り合いの形に表したもの。

解説 ​

何を述べているか。 State.setBalance で位置 i の残高を v に変えると、残高総和 totalBalances（= 全残高を ℕ で合計したもの）が「旧残高が抜けて v が入る」分だけ動く、という等式です。

直感。 toNat_single_update（toNat と更新の交換）と sum_update_split（総和の 1 点更新）を合成しただけです。1 人の残高を書き換えたときの総和の変化を、omega で使える釣り合いの形にしています。

なぜ安全性に効くか。 mint_totalBalances / burn_totalBalances を経て、供給保存（mint_conserves / burn_conserves）に直結します。「総供給」と「残高の総和」が常に一致し続けることを、機械的に証明するための要石です。

図解 ​

Lean ソースコード ​

lean
/-- The effect of one `setBalance` on `totalBalances`, balanced over `ℕ`. -/
theorem totalBalances_setBalance (s : State) (i : Address) (v : U256) :
    (s.setBalance i v).totalBalances + (s.balances i).toNat = v.toNat + s.totalBalances := by
  unfold State.totalBalances
  simp only [setBalance_balances]
  rw [Finset.sum_congr rfl (fun a _ => toNat_single_update s.balances i v a)]
  exact sum_update_split (fun b => (s.balances b).toNat) i v.toNat

依存 ​