JPYCv2 形式検証

外観

JPYC.transferWithAuthorization_unused ​

名称・種別 ​

  • 名称: JPYC.transferWithAuthorization_unused
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:281-288
  • 概要: 成功した transferWithAuthorization は (from,nonce) 認可が未使用だったことを要求する（単回使用）。
  • 仕様: 対象

型シグネチャ ​

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') → Eq (s.authorizationStates frm nonce) 0

transferWithAuthorization の成功は、対象の authorization が 未使用 だったことを含意する、という単一使用性（前提）の定理です。

和訳 docstring ​

単一使用（前提）。 成功した transferWithAuthorization は (from, nonce) authorization が未使用であることを要する。

解説 ​

何を述べているか。 transferWithAuthorization が成功したなら s.authorizationStates frm nonce = 0、すなわちその authorization が呼び出し前に未使用だったことが導けます。内部処理の特徴づけから requireUnusedAuthorization の通過条件を取り出します。

直感。 「この操作が通った ⇒ その引換券はまだ使われていなかった」。使用済みなら未使用ガードに弾かれて失敗します。

なぜ安全性に効くか。 transferWithAuthorizationの 一回限り性 の前提側です。対になる *_marks_used（成功後は 1）と組み合わせると、同じ authorization が二度通らないこと（*_no_replay）が導けます。

図解 ​

Lean ソースコード ​

lean
/-- **Single-use (unused).** A successful `transferWithAuthorization` requires the
`(from, nonce)` authorization to have been unused. -/
theorem transferWithAuthorization_unused {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') :
    s.authorizationStates frm nonce = 0 :=
  (_transferWithAuthorization_ok (transferWithAuthorization_eq_ok h)).2.2.1

依存 ​