JPYCv2 形式検証

外観

JPYC.checkAllowlist_bind_eq_ok ​

名称・種別 ​

  • 名称: JPYC.checkAllowlist_bind_eq_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:58-66
  • 概要: checkAllowlist は状態を変えないので、成功時は後続が同じ状態で成功する、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {α : Type} {s : JPYC.State} {acc : JPYC.Address} {value : JPYC.U256} {f : Unit → Except JPYC.Error α} {b : α}, Eq (Except.instMonad.bind (JPYC.checkAllowlist s acc value) f) (Except.ok b) → Eq (f Unit.unit) (Except.ok b)

checkAllowlist s acc value >>= f が Except.ok b で成功するなら、続く f () が .ok b で成功する、という補題です。

和訳 docstring ​

checkAllowlist は状態を変えないので、成功時はどちらの枝でも続きが同じ結果で成功する。

解説 ​

何を述べているか。 checkAllowlist は状態を変えないガードなので、その後ろの処理 f の成功結果だけが残ります。上限超え（require する枝）でも上限以下（pure () の枝）でも、続きの結論は同じ f () = .ok b。

直感。 「allowlist チェックは関所であって、通り抜けても荷物（状態）は変わらない」。だから合成の成功は、後続 f の成功にそのまま帰着します。

なぜ安全性に効くか。 transfer / approve / transferFrom の証明で、checkAllowlist を本体到達の障害にせず通過させます。両方の分岐を req_bind_eq_ok と pure_eq/ok_bind で吸収する点がポイントです。

図解 ​

Lean ソースコード ​

lean
/-- `checkAllowlist` never changes the state, so on success its continuation
succeeds with the same result (whichever branch the cap check took). -/
theorem checkAllowlist_bind_eq_ok {α : Type} {s : State} {acc : Address} {value : U256}
    {f : Unit → Except Error α} {b : α}
    (h : (checkAllowlist s acc value >>= f) = .ok b) : f () = .ok b := by
  unfold checkAllowlist at h
  by_cases hc : value > allowlistLimitAmount
  · rw [if_pos hc] at h; exact (req_bind_eq_ok h).2
  · rw [if_neg hc] at h; rwa [pure_eq, ok_bind] at h

依存 ​