JPYCv2 形式検証

外観

JPYC.minterAllowance ​

名称・種別 ​

  • 名称: JPYC.minterAllowance
  • 種別: def
  • モジュール: JpycFormalVerification.AccessControl
  • ソース: JpycFormalVerification/AccessControl.lean:242-243
  • 概要: minterAllowance(minter)：minter の残り発行許容額を返す読み取り専用ビュー。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → JPYC.U256

State とアドレス minter を受け取り、そのミンターの残りミント許可量を U256 で返します。

和訳 docstring ​

minter の残りミント許可量を返す（v2/FiatTokenV2.sol:139-141）。

解説 ​

何を述べているか。 FiatTokenV2.minterAllowance です。minterAllowed[minter] をそのまま返します。

直感。 状態を 読むだけ の関数（Solidity の view）で、書き込みは一切しません。返り値はそのミンターがあと何トークン発行できるか（残枠）です。

なぜ安全性に効くか。 これ自体は状態を変えないので安全性の主役ではありませんが、ガードや他の証明が参照する「観測値」を定義します。たとえばブロック判定・許可リスト判定・ミンター判定は、対応するフラグマッピングをこの形で読み出します。

図解 ​

Lean ソースコード ​

lean
/-- `minterAllowance(minter)` — `v2/FiatTokenV2.sol:139-141`. -/
def minterAllowance (s : State) (minter : Address) : U256 := s.minterAllowed minter

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:139-141

solidity
function minterAllowance(address minter) external view returns (uint256) {
    return minterAllowed[minter];
}

依存 ​