JPYCv2 形式検証

外観

JPYC.req ​

名称・種別 ​

  • 名称: JPYC.req
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:42-44
  • 概要: require(cond, err) のモデル。cond が真なら続行、偽なら err で revert する。
  • 仕様: 対象外

型シグネチャ ​

lean
(cond : Prop) → [Decidable cond] → JPYC.Error → Except JPYC.Error Unit

命題 cond（Decidable なもの）と失敗理由 err を受け取り、cond が成り立てば Except.ok ()、成り立たなければ Except.error err を返します。

和訳 docstring ​

require(cond, err) ― cond が成り立てば続行、そうでなければ err で revert する。

解説 ​

何を述べているか。 Solidity の require(cond, msg) を 1 対 1 で写し取った関数です。条件 cond が真なら何もせず処理を続行（pure ()）、偽なら指定された Error で revert します（Except と revert モデル）。

直感。 「関所」です。条件を満たせば通過、満たさなければその場で打ち切り。条件を Bool ではなく Decidable な命題（Prop）として持つのがポイントで、後続の証明が if/split でガードの真偽にそのまま場合分けできます。

なぜ安全性に効くか。 すべてのガード（whenNotPaused / notBlocklisted など）と require 文はこの req の上に組み立てられています。req の意味が「条件を満たすときだけ通す」と一点に定まっているため、各関数の制御フローがソースと 1 対 1 であることを精密に追跡できます。

図解 ​

Lean ソースコード ​

lean
/-- `require(cond, err)` — proceed if `cond`, else revert with `err`. -/
def req (cond : Prop) [Decidable cond] (err : Error) : Except Error Unit :=
  if cond then pure () else throw err

依存 ​