JPYCv2 形式検証

外観

JPYC.req_bind_eq_ok ​

名称・種別 ​

  • 名称: JPYC.req_bind_eq_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:48-56
  • 概要: do ブロック先頭の require を 1 つ剥がす補題：成功は条件を強制し後続を成功させる。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {α : Type} {c : Prop} [inst : Decidable c] {e : JPYC.Error} {f : Unit → Except JPYC.Error α} {b : α}, Eq (Except.instMonad.bind (JPYC.req c e) f) (Except.ok b) → And c (Eq (f Unit.unit) (Except.ok b))

req c e >>= f が Except.ok b で成功するなら、条件 c が成り立ち、かつ続く f () が .ok b で成功する、という補題です。

和訳 docstring ​

do ブロック先頭の require を 1 枚剥がす ― 成功は条件の成立と続きの成功を強制する。

解説 ​

何を述べているか。 do ブロックの先頭から require を 1 枚剥がします。成功という結果から「そのガードは通った（c が真）」と「続きも成功した」を同時に取り出します。

直感。 req_bind を使って if に開き、c の真偽で場合分け。偽なら .error になって成功と矛盾、真なら条件と続きの成功が手に入ります。

なぜ安全性に効くか。 transfer_eq_ok / approve_eq_ok / transferFrom_eq_ok が、先頭のガード（whenNotPaused、notBlocklisted …）を 1 つずつ剥がして本体へ到達するための基本ステップです。「成功した呼び出しでは、すべてのガードが満たされていた」を導く道具になります。

図解 ​

Lean ソースコード ​

lean
/-- Peel one `require` from the front of a `do` block: success forces the
condition and leaves the continuation succeeding. -/
theorem req_bind_eq_ok {α : Type} {c : Prop} [Decidable c] {e : Error}
    {f : Unit → Except Error α} {b : α} (h : (req c e >>= f) = .ok b) :
    c ∧ f () = .ok b := by
  rw [req_bind] at h
  by_cases hc : c
  · rw [if_pos hc] at h; exact ⟨hc, h⟩
  · rw [if_neg hc] at h; exact absurd h (by simp)

依存 ​