JPYCv2 形式検証

外観

JPYC.permit_eq_ok ​

名称・種別 ​

  • 名称: JPYC.permit_eq_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:140-149
  • 概要: 成功した permit は owner からの _permit の成功に還元される、という補題。
  • 仕様: 対象外

型シグネチャ ​

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') → Eq (JPYC._permit O s ctx owner spender value deadline v r sig) (Except.ok s')

外側の permit が成功するなら、modifier ガードを剝がした内部 _permit も同じ結果で成功する、という橋渡し補題です。

和訳 docstring ​

成功した permit は所有者についての _permit の成功に帰着する。

解説 ​

何を述べているか。 permit が Except.ok s' で成功したとき、停止・ブロック（owner/spender）・許可リストの 4 ガードを剝がした内部 _permit も .ok s' を返します。証明は req_bind_eq_ok でガードを剝がし checkAllowlist_bind_eq_ok で締めます。

直感。 「外側の permit は modifier を並べているだけ」を使い、本質的な内部処理（期限・nonce・署名・承認）に証明を集中させる前処理です。

なぜ安全性に効くか。 これは 証明インフラ です。permit の効果・nonce・署名・不変条件の各定理は、まずこの補題で _permit に降りてから論じます。

図解 ​

Lean ソースコード ​

lean
/-- A successful `permit` reduces to a successful `_permit` for the owner. -/
theorem permit_eq_ok {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') :
    _permit O s ctx owner spender value deadline v r sig = .ok s' := by
  unfold permit whenNotPaused notBlocklisted at h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  exact checkAllowlist_bind_eq_ok h

依存 ​