JPYCv2 形式検証

外観

JPYC.burn_totalBalances ​

名称・種別 ​

  • 名称: JPYC.burn_totalBalances
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:561-569
  • 概要: 成功した burn は totalBalances を amount だけ減らす、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {amount : JPYC.U256}, Eq (JPYC.burn s ctx amount) (Except.ok s') → Eq (instHAdd.hAdd s'.totalBalances (BitVec.toNat amount)) s.totalBalances

burn の成功は、残高総和 totalBalances をちょうど amount 減らす、という補題です。

解説 ​

何を述べているか。 burn が成功すると s'.totalBalances + amount.toNat = s.totalBalances です。totalBalances_setBalance に nb = balances[sender] - amount（sub? の成功で amount ≤ 残高）を代入し omega で締めます。

直感。 「呼び出し元 1 人の残高が amount 減れば、全員の残高合計も amount 減る」。

なぜ安全性に効くか。 burn_totalSupply と並べることで burn_conserves（供給保存）が omega で出ます。焼却側の供給保存の算術的な半分です。

図解 ​

Lean ソースコード ​

lean
theorem burn_totalBalances {s s' : State} {ctx : CallContext} {amount : U256}
    (h : burn s ctx amount = .ok s') : s'.totalBalances + amount.toNat = s.totalBalances := by
  obtain ⟨ns, nb, hns, hnb, rfl⟩ := burn_eq h
  have hkey := totalBalances_setBalance s ctx.sender nb
  have hnb' : nb.toNat = (s.balances ctx.sender).toNat - amount.toNat := sub?_toNat hnb
  obtain ⟨_, hle⟩ := sub?_eq_ok hnb
  have heq : ((s.setTotalSupply ns).setBalance ctx.sender nb).totalBalances
      = (s.setBalance ctx.sender nb).totalBalances := rfl
  rw [heq]; omega

依存 ​