JPYC.burn_totalSupply
名称・種別
- 名称:
JPYC.burn_totalSupply - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:531-539 - 概要: burn は totalSupply を 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'.totalSupply) (BitVec.toNat amount)) (BitVec.toNat s.totalSupply)burn の成功は、総供給を（自然数換算で）ちょうど amount 減らす、という効果定理です。
和訳 docstring
効果（供給）。 burn は totalSupply を amount だけ減らす（アンダーフローなし）。
解説
何を述べているか。 burn が成功すると s'.totalSupply.toNat + amount.toNat = s.totalSupply.toNat、すなわち総供給が amount 減ります。burn_eq の sub? totalSupply amount = .ok ns から、減算成功の条件（amount ≤ 総供給）と差の値を使い omega で締めます。
直感。 「焼いた分だけ、世の中のトークン総量が減る」。checked な sub? は負になる引き算を弾くので、アンダーフローは起きません。
なぜ安全性に効くか。 焼却量が記録上ちょうど amount であること（過不足なし）を保証します。burn_conserves と組み合わさり、焼却が帳簿の釣り合いを保つことを示します。
図解
Lean ソースコード
lean
/-- **Effect (supply).** `burn` lowers `totalSupply` by `amount` (no underflow). -/
theorem burn_totalSupply {s s' : State} {ctx : CallContext} {amount : U256}
(h : burn s ctx amount = .ok s') :
s'.totalSupply.toNat + amount.toNat = s.totalSupply.toNat := by
obtain ⟨ns, nb, hns, hnb, rfl⟩ := burn_eq h
show ns.toNat + amount.toNat = s.totalSupply.toNat
have : ns.toNat = s.totalSupply.toNat - amount.toNat := sub?_toNat hns
obtain ⟨_, hle⟩ := sub?_eq_ok hns
omega