JPYC.updateAllowlister_auth

名称・種別

名称: JPYC.updateAllowlister_auth
種別: theorem
モジュール: JpycFormalVerification.AccessControlTheorems
ソース: JpycFormalVerification/AccessControlTheorems.lean:646-648
概要: ロール付け替え updateAllowlister の成功は owner が呼んだことを含意する（権限）。
仕様: 対象

型シグネチャ

lean

∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {newAllowlister : JPYC.Address}, Eq (JPYC.updateAllowlister s ctx newAllowlister) (Except.ok s') → Eq s.owner ctx.sender

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

解説

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

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

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

図解

Lean ソースコード

lean

theorem updateAllowlister_auth {s s' : State} {ctx : CallContext} {newAllowlister : Address}
    (h : updateAllowlister s ctx newAllowlister = .ok s') : s.owner = ctx.sender :=
  (updateAllowlister_ok h).1

JPYC.updateAllowlister_auth ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.updateAllowlister_auth

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存