JPYCv2 形式検証

外観

JPYC.isBlocklisted ​

名称・種別 ​

  • 名称: JPYC.isBlocklisted
  • 種別: def
  • モジュール: JpycFormalVerification.AccessControl
  • ソース: JpycFormalVerification/AccessControl.lean:236-237
  • 概要: isBlocklisted(account)：ブロックリスト登録状態を返す読み取り専用ビュー。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → Bool

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

和訳 docstring ​

account がブロックリスト登録済みかを返す（v1/Blocklistable.sol:78-80）。

解説 ​

何を述べているか。 Blocklistable.isBlocklisted です。blocklisted[account] == 1 を判定して返します。

直感。 状態を 読むだけ の関数（Solidity の view）で、書き込みは一切しません。返り値はブロック済みなら true、そうでなければ false です。

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

図解 ​

Lean ソースコード ​

lean
/-- `isBlocklisted(account)` — `v1/Blocklistable.sol:78-80`. -/
def isBlocklisted (s : State) (account : Address) : Bool := s.blocklisted account == 1

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/Blocklistable.sol:78-80

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

依存 ​