JPYCv2 形式検証

外観

JPYC.transferWithAuthorization_within_window ​

名称・種別 ​

  • 名称: JPYC.transferWithAuthorization_within_window
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:327-335
  • 概要: 成功した transferWithAuthorization は (validAfter,validBefore) 内である、という定理（有効期間）。
  • 仕様: 対象

型シグネチャ ​

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.transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.ok s') → And (GT.gt ctx.blockTimestamp validAfter) (instLTBitVec.lt ctx.blockTimestamp validBefore)

transferWithAuthorization の成功は、有効ウィンドウ内（validAfter < block.timestamp < validBefore）だったことを含意する、という有効期間の定理です。

和訳 docstring ​

有効期間。 成功した transferWithAuthorization は有効ウィンドウ内である。

解説 ​

何を述べているか。 transferWithAuthorization が成功したなら ctx.blockTimestamp > validAfter ∧ ctx.blockTimestamp < validBefore です。requireValidAuthorization の 2 つの時間ガードの通過条件を取り出します。

直感。 「この送金が通った ⇒ 署名で指定された有効期間の中にいた」。開始前なら authorizationNotYetValid、終了後なら authorizationExpired で revert します。

なぜ安全性に効くか。 署名つき送金に時間の窓を与えます。署名者は「いつからいつまで有効か」を制御でき、漏れた署名が無期限に有効化するのを防ぎます。

図解 ​

Lean ソースコード ​

lean
/-- **Validity window.** A successful `transferWithAuthorization` is within
`(validAfter, validBefore)`. -/
theorem transferWithAuthorization_within_window {O : SigOracle} {s s' : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32}
    (h : transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s') :
    ctx.blockTimestamp > validAfter ∧ ctx.blockTimestamp < validBefore :=
  ⟨(_transferWithAuthorization_ok (transferWithAuthorization_eq_ok h)).1,
   (_transferWithAuthorization_ok (transferWithAuthorization_eq_ok h)).2.1⟩

依存 ​