JPYCv2 形式検証

外観

JPYC.checkAllowlist ​

名称・種別 ​

  • 名称: JPYC.checkAllowlist
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:56-64
  • 概要: checkAllowlist(account,value) 修飾子（V2）。上限超の額は account の許可登録を要求する。
  • 仕様: 対象外

型シグネチャ ​

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

State・アドレス account・金額 value を受け取り、value が allowlistLimitAmount を 超える 場合に限り allowlisted[account] = 1 を要求するガードです。上限以下なら無条件で通過します。

和訳 docstring ​

checkAllowlist(account, value)（V2 のみ）― allowlistLimitAmount を超える金額は、当事者が allowlist 登録済みであることを要求する。対応 Solidity: v2/FiatTokenV2.sol:593-601。

解説 ​

何を述べているか。 JPYCv2（V2）で追加された checkAllowlist modifier のモデルです。送金額・承認額が上限 allowlistLimitAmount（10 万トークン）を超えるときだけ、当事者が許可リスト（allowlist）に登録済み（= 1）であることを要求します。上限以下なら何の制約もなく pure () で通過します。

直感。 「大口の取引には事前審査（KYC 相当）を求める」という仕組みです。少額決済は誰でも自由に、大口は許可された主体だけに限定されます。

なぜ安全性に効くか。 transfer / transferFrom / approve / increaseAllowance に組み込まれます。「上限超えの取引が成功したなら、当事者は必ず allowlisted だった」という性質（各関数の *_above_cap_allowlisted 定理）の根拠になり、規制要件をコードレベルで強制します。証明では分岐 value > allowlistLimitAmount を checkAllowlist_bind_eq_ok で吸収し、どちらの枝でも状態が変わらないことを使います。

図解 ​

Lean ソースコード ​

lean
/-- `checkAllowlist(account, value)` (V2-only): amounts strictly above
`allowlistLimitAmount` require the account to be allowlisted.
Source: `v2/FiatTokenV2.sol:593-601`. -/
def checkAllowlist (s : State) (account : Address) (value : U256) :
    Except Error Unit :=
  if value > allowlistLimitAmount then
    req (s.allowlisted account = 1) .accountNotAllowlisted
  else
    pure ()

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:593-601

solidity
modifier checkAllowlist(address _account, uint256 _value) {
    if (_value > allowlistLimitAmount) {
        require(
            allowlisted[_account] == 1,
            "FiatToken: account is not allowlisted"
        );
    }
    _;
}

依存 ​