JPYCv2 形式検証

外観

JPYC.transferWithAuthorization_marks_used ​

名称・種別 ​

  • 名称: JPYC.transferWithAuthorization_marks_used
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:290-299
  • 概要: 成功した 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) 1

transferWithAuthorization の成功は、対象の authorization を 使用済み（= 1）にする、という単一使用性（効果）の定理です。

和訳 docstring ​

単一使用（効果）。 成功した transferWithAuthorization は (from, nonce) authorization を使用済みにする。

解説 ​

何を述べているか。 transferWithAuthorization が成功した結果状態では s'.authorizationStates frm nonce = 1 です。内部で setAuthorizationState … 1 を行い、その後の _transfer は authorization 台帳に触れない（_transfer_authorizationStates）ので、1 がそのまま読めます（setAuthorizationState_self）。

直感。 「使ったら、その引換券は使用済みの判を押される」を確認します。

なぜ安全性に効くか。 transferWithAuthorizationの 一回限り性 の効果側です。transferWithAuthorization_unused と組み合わさり、リプレイ不可（*_no_replay）の直接の根拠になります。

図解 ​

Lean ソースコード ​

lean
/-- **Single-use (marked).** A successful `transferWithAuthorization` marks the
`(from, nonce)` authorization used. -/
theorem transferWithAuthorization_marks_used {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 = 1 := by
  obtain ⟨_, _, _, _, htr⟩ := _transferWithAuthorization_ok (transferWithAuthorization_eq_ok h)
  rw [_transfer_authorizationStates htr]
  exact setAuthorizationState_self s frm nonce 1

依存 ​