JPYCv2 形式検証

外観

JPYC.onlyMinters ​

名称・種別 ​

  • 名称: JPYC.onlyMinters
  • 種別: def
  • モジュール: JpycFormalVerification.AccessControl
  • ソース: JpycFormalVerification/AccessControl.lean:87-89
  • 概要: onlyMinters 修飾子。minters[msg.sender] が偽なら revert する権限ガード。
  • 仕様: 対象外

型シグネチャ ​

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

State と CallContext を受け取り、ミンター（minters に登録された者）による呼び出しでなければ notMinter で revert するロール検査ガードです。

和訳 docstring ​

onlyMinters ― require(minters[msg.sender], …)（v2/FiatTokenV2.sol:85-88）。

解説 ​

何を述べているか。 Solidity の修飾子（modifier）onlyMinters ―「minters[msg.sender] でなければ revert する」をモデル化したものです。req を使って条件を表現し、満たせば Except.ok ()、満たさなければ Except.error .notMinter を返します。

直感。 関数本体に入る前の「関所」です。呼び出し元（msg.sender）がミンター（minters に登録された者）本人かどうかだけを見て、違えば即座に弾きます。 ここだけは真偽値マッピング minters[msg.sender] を直接見ます（アドレス一致ではなく登録フラグ）。

なぜ安全性に効くか。 特権操作を「ミンター（minters に登録された者）だけ」に閉じ込めるのが、アクセス制御の要です。このガードを最初に置くことで、対応する *_auth 定理（成功 ⇒ 呼び出し元が権限者）と *_unauthorized 定理（権限なし ⇒ notMinterで revert）が証明でき、「権限のない者は状態を変えられない」を保証します。比較の向き（minters[msg.sender]）は Solidity ソースに 1:1 で合わせています。

図解 ​

Lean ソースコード ​

lean
/-- `onlyMinters` — `require(minters[msg.sender], …)`. Source: `v2/FiatTokenV2.sol:85-88`. -/
def onlyMinters (s : State) (ctx : CallContext) : Except Error Unit :=
  req (s.minters ctx.sender = true) .notMinter

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:85-88

solidity
modifier onlyMinters() {
    require(minters[msg.sender], "FiatToken: caller is not a minter");
    _;
}

依存 ​