JPYCv2 形式検証

外観

JPYC.allowlist_sets ​

名称・種別 ​

  • 名称: JPYC.allowlist_sets
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:615-618
  • 概要: allowlist はフラグを 1 に、unAllowlist は 0 にする（効果）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {account : JPYC.Address}, Eq (JPYC.allowlist s ctx account) (Except.ok s') → Eq (s'.allowlisted account) 1

allowlist の成功は allowlisted[account] = 1 をもたらす、という効果定理です。

和訳 docstring ​

効果。 allowlist はフラグを 1 に、unAllowlist は 0 に設定する。

解説 ​

何を述べているか。 allowlist が成功した結果状態では allowlisted[account] = 1 です。allowlist_ok と setAllowlisted_self から従います。

直感。 「許可リストに載せたら、ちゃんとフラグが 1 になる」を確認します。

なぜ安全性に効くか。 フラグが確実に立つことで、そのアカウントは checkAllowlist の上限超チェックを通過できます。大口送金の特権が設定どおりに有効化される根拠です。

図解 ​

Lean ソースコード ​

lean
/-- **Effect.** `allowlist` sets the flag to `1`; `unAllowlist` clears it to `0`. -/
theorem allowlist_sets {s s' : State} {ctx : CallContext} {account : Address}
    (h : allowlist s ctx account = .ok s') : s'.allowlisted account = 1 := by
  obtain ⟨_, _, rfl⟩ := allowlist_ok h; exact setAllowlisted_self s account 1

依存 ​