JPYCv2 形式検証

外観

JPYC.notBlocklisted ​

名称・種別 ​

  • 名称: JPYC.notBlocklisted
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:51-54
  • 概要: notBlocklisted(account) 修飾子。account がブロックリスト登録なら revert するガード。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → Except JPYC.Error Unit

State とアドレス account を受け取り、blocklisted[account] が 0 なら通過、1（ブロックリスト入り）なら Blocklistable: account is blocklisted で revert します。

和訳 docstring ​

notBlocklisted(account) ― require(blocklisted[account] == 0, …)。対応 Solidity: v1/Blocklistable.sol:65-71。

解説 ​

何を述べているか。 Solidity の notBlocklisted(account) modifier、require(blocklisted[account] == 0, …) をモデル化したガードです。req で s.blocklisted account = 0 を検査します。

直感。 ブロックリストに載っているアドレスが関与する取引を拒否します。フラグは WF により必ず 0 か 1 なので、「= 0 なら未ブロック、それ以外（= 1）ならブロック済み」という判定が破綻しません。

なぜ安全性に効くか。 送金・承認では送り手・受け手の双方にこのガードを掛けます。これにより「成功した取引には、ブロックされた当事者は含まれない」という対偶（各関数の *_not_blocklisted 定理）が導けます。制裁対応などコンプライアンス上の要請を、関数の入口で機械的に保証します。

図解 ​

Lean ソースコード ​

lean
/-- `notBlocklisted(account)` — `require(blocklisted[account] == 0, …)`.
Source: `v1/Blocklistable.sol:65-71`. -/
def notBlocklisted (s : State) (account : Address) : Except Error Unit :=
  req (s.blocklisted account = 0) .accountBlocklisted

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/Blocklistable.sol:65-71

solidity
modifier notBlocklisted(address _account) {
    require(
        blocklisted[_account] == 0,
        "Blocklistable: account is blocklisted"
    );
    _;
}

依存 ​