JPYCv2 形式検証

外観

JPYC.allowlistLimitAmount ​

名称・種別 ​

  • 名称: JPYC.allowlistLimitAmount
  • 種別: def
  • モジュール: JpycFormalVerification.State
  • ソース: JpycFormalVerification/State.lean:36-39
  • 概要: V2 アローリストの上限額（100,000 × 1e18）。超過する送金は許可登録を要求する。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.U256

型 U256 の 定数 です。値は 100000 * 1e18（= 10 万 JPYC を最小単位で表したもの）。

和訳 docstring ​

V2 の allowlist 上限 allowlistLimitAmount = 100000 * 1e18。これを超える額の送金は、該当アカウントが allowlist 登録済みであることを要求する。出典: v2/FiatTokenV2.sol:62。

解説 ​

何を述べているか。「事前許可なしに 1 回で動かせる額の上限」を表す定数で、10 万 JPYC（18 桁の小数なので最小単位では 100000 * 10^18）です。BitVec.ofNat 256 (…) で 256 ビット値に包んでいます。

直感。 大口の送金・発行には、あらかじめ allowlist へ登録しておくことを要求する仕組みのしきい値です。少額の通常取引はこの制約を受けません。

なぜ安全性に効くか。 Phase 1 / 2 の allowlist 上限定理（*_above_cap_allowlisted）で参照され、「上限を超える移動は allowlist 済みのアカウントに限る」という V2 固有の制約の基準値になります。

図解 ​

Lean ソースコード ​

lean
/-- The V2 allowlist cap, `allowlistLimitAmount = 100000 * 1e18`. Transfers whose
amount exceeds this require the relevant account to be allowlisted.
Source: `v2/FiatTokenV2.sol:62`. -/
def allowlistLimitAmount : U256 := BitVec.ofNat 256 (100000 * 10 ^ 18)

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:62-62

solidity
    // allowlist test
    uint256 public constant allowlistLimitAmount = 100000 * 1e18;

依存 ​