JPYCv2 形式検証

外観

JPYC.blocklist_sets ​

名称・種別 ​

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

型シグネチャ ​

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

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

和訳 docstring ​

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

解説 ​

何を述べているか。 blocklist が成功した結果状態では blocklisted[account] = 1 です。blocklist_ok と setBlocklisted_self から従います。

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

なぜ安全性に効くか。 フラグが確実に立つことで、以降そのアカウントは notBlocklisted ガードに弾かれ、送金・受領に参加できません。凍結の実効性の根拠です。

図解 ​

Lean ソースコード ​

lean
/-- **Effect.** `blocklist` sets the flag to `1`; `unBlocklist` clears it to `0`. -/
theorem blocklist_sets {s s' : State} {ctx : CallContext} {account : Address}
    (h : blocklist s ctx account = .ok s') : s'.blocklisted account = 1 := by
  obtain ⟨_, rfl⟩ := blocklist_ok h; exact setBlocklisted_self s account 1

依存 ​