JPYCv2 形式検証

外観

JPYC.WF.of_flags_eq ​

名称・種別 ​

  • 名称: JPYC.WF.of_flags_eq
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:292-298
  • 概要: WF はフラグ写像と initializedVersion だけに依存し、それらを保つ遷移は WF を保つ、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s s' : JPYC.State}, JPYC.WF s → Eq s'.blocklisted s.blocklisted → Eq s'.allowlisted s.allowlisted → Eq s'.authorizationStates s.authorizationStates → Eq s'.initializedVersion s.initializedVersion → JPYC.WF s'

状態 s が WF を満たし、s' のフラグ 3 種と initializedVersion が s と一致するなら、s' も WF を満たす、という補題です。

和訳 docstring ​

WF はフラグと initializedVersion のみに依存する ― それらを保つ遷移は WF を保存する。

解説 ​

何を述べているか。 WF はフラグ（blocklisted / allowlisted / authorizationStates）と initializedVersion だけに依存します。だから、これら 4 つが元の状態と同じなら、残高や許可額がどう変わっても WF は保たれます。

直感。 「健全性チェックの対象はフラグとバージョンだけ。そこさえ触っていなければ整合性は崩れない」。各条項を仮定の等式で書き換えるだけで証明できます。

なぜ安全性に効くか。 これが WF 保存証明の万能ツールです。送金・承認は残高や許可額しか変えずフラグ・バージョンには触れないので、_transfer_wf / _approve_wf などが軒並みこの補題 1 本に帰着します。フラグを uint256 で持つ符号化の安全性（必ず 0/1）が、全操作を通じて保たれます。

図解 ​

Lean ソースコード ​

lean
/-- Well-formedness depends only on the flag mappings and `initializedVersion`;
any transition preserving those preserves `WF`. -/
theorem WF.of_flags_eq {s s' : State} (hwf : WF s)
    (hb : s'.blocklisted = s.blocklisted) (ha : s'.allowlisted = s.allowlisted)
    (hau : s'.authorizationStates = s.authorizationStates)
    (hi : s'.initializedVersion = s.initializedVersion) : WF s' :=
  wf_of_flags_eq_version_valid hwf hb ha hau (by rw [hi]; exact hwf.initializedVersionValid)

依存 ​