JPYC.burn_balance
名称・種別
- 名称:
JPYC.burn_balance - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:541-551 - 概要: burn は呼び出し元の残高を amount だけ減らす、という定理（効果・残高）。
- 仕様: 対象
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {amount : JPYC.U256}, Eq (JPYC.burn s ctx amount) (Except.ok s') → Eq (instHAdd.hAdd (BitVec.toNat (s'.balances ctx.sender)) (BitVec.toNat amount)) (BitVec.toNat (s.balances ctx.sender))burn の成功は、呼び出し元の残高を（自然数換算で）ちょうど amount 減らす、という効果定理です。
和訳 docstring
効果（残高）。 burn は呼び出し元の残高を amount だけ減らす。
解説
何を述べているか。 burn が成功すると (s'.balances sender).toNat + amount.toNat = (s.balances sender).toNat です。burn_eq の sub? balances[sender] amount = .ok nb から、最後に書かれた残高がそのまま読めることと差の値を使います。
直感。 「焼いた人の残高が、焼いた分だけ減る」。残高不足なら sub? が revert するので、成功時は必ず amount ≤ 残高 です。
なぜ安全性に効くか。 呼び出し元が確かに amount を失ったことを保証します。burn_totalSupply と burn_frame と合わせ、焼却の効果が「総供給と呼び出し元だけにちょうど反映される」ことを示します。
図解
Lean ソースコード
lean
/-- **Effect (balance).** `burn` lowers the caller's balance by `amount`. -/
theorem burn_balance {s s' : State} {ctx : CallContext} {amount : U256}
(h : burn s ctx amount = .ok s') :
(s'.balances ctx.sender).toNat + amount.toNat = (s.balances ctx.sender).toNat := by
obtain ⟨ns, nb, hns, hnb, rfl⟩ := burn_eq h
have hbal : ((s.setTotalSupply ns).setBalance ctx.sender nb).balances ctx.sender = nb := by
simp [setTotalSupply_balances, Function.update_self]
rw [hbal]
have : nb.toNat = (s.balances ctx.sender).toNat - amount.toNat := sub?_toNat hnb
obtain ⟨_, hle⟩ := sub?_eq_ok hnb
omega