JPYC.mint_totalBalances
名称・種別
- 名称:
JPYC.mint_totalBalances - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:476-484 - 概要: 成功した mint は totalBalances を 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 s'.totalBalances (instHAdd.hAdd s.totalBalances (BitVec.toNat amount))mint の成功は、残高総和 totalBalances をちょうど amount 増やす、という補題です。
和訳 docstring
mint の成功は totalBalances を amount だけ増やす。
解説
何を述べているか。 mint が成功すると s'.totalBalances = s.totalBalances + amount.toNat です。totalBalances_setBalance（1 点書き換えの総和への効果）に、nb = balances[dst] + amount を代入して omega で締めます。総供給と許可量の更新は balances に触れないので、総和は setBalance dst nb の効果だけで決まります。
直感。 「受取人 1 人の残高が amount 増えれば、全員の残高合計も amount 増える」。当たり前ですが、ℕ 上の総和できちんと示す必要があります。
なぜ安全性に効くか。 mint_totalSupply（総供給 +amount）と並べることで、mint_conserves（totalSupply = totalBalances が保たれる）が omega 一発で出ます。供給保存の算術的な半分を担います。
図解
Lean ソースコード
lean
/-- A successful `mint` raises `totalBalances` by `amount`. -/
theorem mint_totalBalances {s s' : State} {ctx : CallContext} {dst : Address} {amount : U256}
(h : mint s ctx dst amount = .ok s') : s'.totalBalances = s.totalBalances + amount.toNat := by
obtain ⟨ns, nb, nma, hns, hnb, hnma, rfl⟩ := mint_eq h
have hkey := totalBalances_setBalance s dst nb
have hnb' : nb.toNat = (s.balances dst).toNat + amount.toNat := add?_toNat hnb
have heq : (((s.setTotalSupply ns).setBalance dst nb).setMinterAllowed ctx.sender nma).totalBalances
= (s.setBalance dst nb).totalBalances := rfl
rw [heq]; omega