JPYCv2 形式検証

外観

JPYC.isAllowlisted ​

名称・種別 ​

  • 名称: JPYC.isAllowlisted
  • 種別: def
  • モジュール: JpycFormalVerification.AccessControl
  • ソース: JpycFormalVerification/AccessControl.lean:238-239
  • 概要: isAllowlisted(account)：許可登録状態を返す読み取り専用ビュー。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → Bool

State とアドレス account を受け取り、そのアカウントが許可リスト登録済みかを Bool で返します。

和訳 docstring ​

account が許可リスト登録済みかを返す（v2/FiatTokenV2.sol:608-610）。

解説 ​

何を述べているか。 FiatTokenV2.isAllowlisted です。allowlisted[account] == 1 を判定して返します。

直感。 状態を 読むだけ の関数（Solidity の view）で、書き込みは一切しません。返り値は許可リスト登録済みなら true、そうでなければ false です。

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

図解 ​

Lean ソースコード ​

lean
/-- `isAllowlisted(account)` — `v2/FiatTokenV2.sol:608-610`. -/
def isAllowlisted (s : State) (account : Address) : Bool := s.allowlisted account == 1

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:608-610

solidity
function isAllowlisted(address _account) external view returns (bool) {
    return allowlisted[_account] == 1;
}

依存 ​