JPYCv2 形式検証

外観

JPYC.permit_not_expired ​

名称・種別 ​

  • 名称: JPYC.permit_not_expired
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:168-172
  • 概要: 成功した permit は deadline 内である、という定理（期限）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {owner spender : JPYC.Address} {value deadline : JPYC.U256} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.permit O s ctx owner spender value deadline v r sig) (Except.ok s') → GE.ge deadline ctx.blockTimestamp

permit の成功は、期限内（deadline ≥ block.timestamp）だったことを含意する、という期限の定理です。

和訳 docstring ​

期限。 成功した permit は期限内である。

解説 ​

何を述べているか。 permit が成功したなら deadline ≥ ctx.blockTimestamp です。_permit 先頭の期限ガードの通過条件を取り出します。

直感。 「この承認が通った ⇒ 期限切れではなかった」。署名に埋め込まれた deadline を過ぎていれば、permitExpired で revert します。

なぜ安全性に効くか。 署名つき承認に有効期限を与える保証です。漏れた署名が無期限に有効化することを防ぎ、古い承認の使い回しを時間で打ち切ります。

図解 ​

Lean ソースコード ​

lean
/-- **Deadline.** A successful `permit` is within its deadline. -/
theorem permit_not_expired {O : SigOracle} {s s' : State} {ctx : CallContext} {owner spender : Address}
    {value deadline : U256} {v : U8} {r sig : Bytes32}
    (h : permit O s ctx owner spender value deadline v r sig = .ok s') :
    deadline ≥ ctx.blockTimestamp := (_permit_ok (permit_eq_ok h)).1

依存 ​