JPYC.mint_balance
名称・種別
- 名称:
JPYC.mint_balance - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:446-453 - 概要: mint は受取人の残高を 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'.balances dst)) (instHAdd.hAdd (BitVec.toNat (s.balances dst)) (BitVec.toNat amount))mint の成功は、受取人 dst の残高を（自然数換算で）ちょうど amount 増やす、という効果定理です。
和訳 docstring
効果（残高）。 mint は受取人の残高を amount だけ増やす。
解説
何を述べているか。 mint が成功すると (s'.balances dst).toNat = (s.balances dst).toNat + amount.toNat です。mint_eq の add? balances[dst] amount = .ok nb と、最後に書かれた残高がそのまま読めること（他の更新は balances に触れない）から従います。
直感。 「受け取った人の残高が、刷った分だけ増える」。setMinterAllowed などの後続更新は balances を変えないので、dst の残高は nb のまま読めます。
なぜ安全性に効くか。 受取人が確かに amount を受け取ったことを保証します。mint_totalSupply（総供給 +amount）と mint_frame（他人の残高は不変）と合わせ、発行の効果が「総供給と受取人だけにちょうど反映される」ことを示します。
図解
Lean ソースコード
lean
/-- **Effect (balance).** `mint` raises the recipient's balance by `amount`. -/
theorem mint_balance {s s' : State} {ctx : CallContext} {dst : Address} {amount : U256}
(h : mint s ctx dst amount = .ok s') :
(s'.balances dst).toNat = (s.balances dst).toNat + amount.toNat := by
obtain ⟨ns, nb, nma, hns, hnb, hnma, rfl⟩ := mint_eq h
have hbal : (((s.setTotalSupply ns).setBalance dst nb).setMinterAllowed ctx.sender nma).balances dst = nb := by
simp [setMinterAllowed_balances, setTotalSupply_balances, Function.update_self]
rw [hbal]; exact add?_toNat hnb