JPYC.mint_totalSupply
名称・種別
- 名称:
JPYC.mint_totalSupply - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:438-444 - 概要: mint は totalSupply を amount だけ増やす（桁あふれなし）、という定理（効果・供給）。
- 仕様: 対象
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {dst : JPYC.Address} {amount : JPYC.U256}, Eq (JPYC.mint s ctx dst amount) (Except.ok s') → Eq (BitVec.toNat s'.totalSupply) (instHAdd.hAdd (BitVec.toNat s.totalSupply) (BitVec.toNat amount))mint の成功は、総供給を（自然数換算で）ちょうど amount 増やす、という効果定理です。
和訳 docstring
効果（供給）。 mint は totalSupply を amount だけ増やす（あふれなし）。
解説
何を述べているか。 mint が成功すると s'.totalSupply.toNat = s.totalSupply.toNat + amount.toNat です。mint_eq が与える add? totalSupply amount = .ok ns から、checked 加算が「あふれずに」成功したこと（add?_toNat）を使います。
直感。 「刷った分だけ、世の中のトークン総量が増える」。add? が成功した時点であふれは起きていないので、ℕ 上の素直な足し算として総供給が増えます。
なぜ安全性に効くか。 発行量が記録上ちょうど amount であること（過不足なし）を保証します。mint_conserves の供給保存と組み合わさり、「発行は帳簿の釣り合いを保ったまま総量を増やす」を厳密に示します。
図解
Lean ソースコード
lean
/-- **Effect (supply).** `mint` raises `totalSupply` by `amount` (no overflow). -/
theorem mint_totalSupply {s s' : State} {ctx : CallContext} {dst : Address} {amount : U256}
(h : mint s ctx dst amount = .ok s') :
s'.totalSupply.toNat = s.totalSupply.toNat + amount.toNat := by
obtain ⟨ns, nb, nma, hns, hnb, hnma, rfl⟩ := mint_eq h
show ns.toNat = s.totalSupply.toNat + amount.toNat
exact add?_toNat hns