JPYC.configureMinter_wf

名称・種別

名称: JPYC.configureMinter_wf
種別: theorem
モジュール: JpycFormalVerification.AccessControlTheorems
ソース: JpycFormalVerification/AccessControlTheorems.lean:363-365
概要: configureMinter は健全性不変条件 WF を保つ、という定理。
仕様: 対象

型シグネチャ

lean

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

configureMinter が成功するなら、結果状態も WF を満たす、という不変条件保存の定理です。

解説

何を述べているか。 事前状態 s が WF を満たし、configureMinter が成功して s' になったとき、s' もまた WF を満たします。

直感。 WF はフラグ（blocklisted/allowlisted/authorizationStates）が 0/1 のみ、initializedVersion ∈ {0,1,2} を要求します。minters / minterAllowed の更新はフラグ 4 種（ブロック・許可・署名・version）に触れないので、WF は保たれます（WF.of_flags_eq）。

なぜ安全性に効くか。 すべての操作が WF を保つので、「正規の操作を続ける限りフラグが壊れた値にならない」が帰納的に保証されます。フラグに依存する判定ロジック全体の前提が、操作後も成り立ち続けます。

図解

Lean ソースコード

lean

theorem configureMinter_wf {s s' : State} {ctx : CallContext} {minter : Address} {amount : U256}
    (hwf : WF s) (h : configureMinter s ctx minter amount = .ok s') : WF s' := by
  obtain ⟨_, _, rfl⟩ := configureMinter_ok h; exact WF.of_flags_eq hwf rfl rfl rfl rfl

JPYC.configureMinter_wf ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.configureMinter_wf

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存