JPYC.mint_minterAllowed
名称・種別
- 名称:
JPYC.mint_minterAllowed - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:455-466 - 概要: mint は minterAllowed を超えられず、成功時は残り許容額が 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') → And (instLEBitVec.le amount (s.minterAllowed ctx.sender)) (Eq (instHAdd.hAdd (BitVec.toNat (s'.minterAllowed ctx.sender)) (BitVec.toNat amount)) (BitVec.toNat (s.minterAllowed ctx.sender)))mint は呼び出し元の許可量 minterAllowed を超えられず、成功時には残許可量がちょうど amount 減る、という上限定理です。
和訳 docstring
上限。 mint は呼び出し元の minterAllowed を超えられず、成功時に残許可量が amount 減る。
解説
何を述べているか。 mint が成功すると、(1) amount ≤ s.minterAllowed sender（上限を超えていない）、(2) (s'.minterAllowed sender).toNat + amount.toNat = (s.minterAllowed sender).toNat（残枠がちょうど amount 減る）が成り立ちます。mint_eq の sub? minterAllowed amount = .ok nma から、減算が成功する条件（amount ≤ 許可量）と差の値を取り出します。
直感。 「発行できるのは枠の範囲内だけ。発行したらその分だけ枠が減る」。checked な sub? は、引いて負になる（=枠不足）ときに revert するので、成功した時点で amount ≤ 許可量 が確定します。
なぜ安全性に効くか。 これが 発行量の上限制御 の核心です。たとえミンターでも、設定された minterAllowed を超えて一度に・累積で発行することはできません。鍵が漏れても被害が枠で頭打ちになる、という被害限定の保証になります。
図解
Lean ソースコード
lean
/-- **Bound.** `mint` cannot exceed the caller's `minterAllowed`; on success the
remaining allowance drops by `amount`. -/
theorem mint_minterAllowed {s s' : State} {ctx : CallContext} {dst : Address} {amount : U256}
(h : mint s ctx dst amount = .ok s') :
amount ≤ s.minterAllowed ctx.sender ∧
(s'.minterAllowed ctx.sender).toNat + amount.toNat = (s.minterAllowed ctx.sender).toNat := by
obtain ⟨ns, nb, nma, hns, hnb, hnma, rfl⟩ := mint_eq h
obtain ⟨_, hle⟩ := sub?_eq_ok hnma
refine ⟨BitVec.le_def.mpr hle, ?_⟩
rw [setMinterAllowed_self]
have : nma.toNat = (s.minterAllowed ctx.sender).toNat - amount.toNat := sub?_toNat hnma
omega