JPYCv2 形式検証

外観

JPYC.receiveWithAuthorization_eq_ok ​

名称・種別 ​

  • 名称: JPYC.receiveWithAuthorization_eq_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:409-418
  • 概要: 成功した receiveWithAuthorization を内部処理に還元する補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {frm dst : JPYC.Address} {value validAfter validBefore : JPYC.U256} {nonce : JPYC.Bytes32} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.ok s') → Eq (JPYC._receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.ok s')

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

解説 ​

何を述べているか。 receiveWithAuthorization が Except.ok s' で成功したとき、先頭の modifier ガード（停止・ブロック・許可リスト）を剝がした内部関数も .ok s' を返します。証明は req_bind_eq_ok でガードを 1 枚ずつ剝がし、checkAllowlist_bind_eq_ok で締めます。

直感。 「外側のラッパは modifier を並べているだけ」という事実を使い、証明を本質的な内部処理に集中させるための前処理です。

なぜ安全性に効くか。 これ自体は安全性の主張ではなく 証明インフラ です。receiveWithAuthorizationに関する効果・不変条件・リプレイ防止の各定理は、まずこの補題で内部処理に降りてから論じます。

図解 ​

Lean ソースコード ​

lean
theorem receiveWithAuthorization_eq_ok {O : SigOracle} {s s' : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32}
    (h : receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s') :
    _receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s' := by
  unfold receiveWithAuthorization 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

依存 ​