JPYC.req_bind

名称・種別

• 名称: JPYC.req_bind
• 種別: theorem
• モジュール: JpycFormalVerification.ERC20Theorems
• ソース: JpycFormalVerification/ERC20Theorems.lean:21-26
• 概要: require の後続処理：条件成立なら f() に進み、不成立なら revert に短絡する、という補題。
• 仕様: 対象外

型シグネチャ

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

「req のあとに続く処理 f」全体は、条件 c が真なら f ()、偽なら Except.error e に等しい、という書き換え規則です。

和訳 docstring

require のあとに処理が続く形 ― 条件が成り立てば f () に進み、そうでなければ revert に短絡する。

解説

何を述べているか。 do ブロックで req c e の直後に処理 f が続くとき、その合成 req c e >>= f が if c then f () else .error e に等しいことを示します。

直感。 ガード付きの逐次処理を「条件が真なら続行、偽なら即 revert」という素直な if 式に開く道具です。証明は req を展開して場合分けするだけ（unfold; split）。

なぜ安全性に効くか。 これ自体は安全性の主張ではなく、証明インフラです。後続の transfer_eq_ok などが「ガードを 1 枚ずつ剥がす」ために繰り返し使います。Except モナドの do 記法を、人が追える明示的な分岐へ機械的に変換します。

図解

Lean ソースコード

/-- A `require` followed by more work: proceeds with `f ()` when the condition
holds, otherwise short-circuits to the revert. -/
theorem req_bind {α : Type} {c : Prop} [Decidable c] {e : Error}
    {f : Unit → Except Error α} :
    (req c e >>= f) = if c then f () else .error e := by
  unfold req; split <;> rfl

依存

• JPYC.Error
• JPYC.req