JPYCv2 形式検証

外観

JPYC.configureMinter_auth ​

名称・種別 ​

  • 名称: JPYC.configureMinter_auth
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:338-341
  • 概要: minter の構成・削除の成功は minterAdmin が呼んだことを含意する（権限）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {minter : JPYC.Address} {amount : JPYC.U256}, Eq (JPYC.configureMinter s ctx minter amount) (Except.ok s') → Eq ctx.sender s.minterAdmin

configureMinter の成功は、呼び出し元がminterAdminであったこと（ctx.sender = s.minterAdmin）を含意する、という認可定理です。

和訳 docstring ​

認可。 ミンターの設定・削除は minterAdmin のみが成功できる。

解説 ​

何を述べているか。 configureMinter が成功したなら、ctx.sender = s.minterAdmin、すなわち呼び出し元がminterAdmin本人だったことが導けます。*_ok 特徴づけの第 1 成分を取り出すだけです。

直感。 「この操作が通った ⇒ 権限者が呼んだ」。特権操作を権限者に閉じ込める、アクセス制御の中心的な保証です。

なぜ安全性に効くか。 権限のないアカウントは、たとえ他の条件を満たしても、この操作で状態を変えることができません。ロール検査ガードを最初に置く設計が、この性質として結実しています。

図解 ​

Lean ソースコード ​

lean
/-- **Authorization.** Configuring / removing a minter succeeds only for the minterAdmin. -/
theorem configureMinter_auth {s s' : State} {ctx : CallContext} {minter : Address} {amount : U256}
    (h : configureMinter s ctx minter amount = .ok s') : ctx.sender = s.minterAdmin :=
  (configureMinter_ok h).2.1

依存 ​