JPYCv2 形式検証

外観

JPYC.receiveWithAuthorization_marks_used ​

名称・種別 ​

  • 名称: JPYC.receiveWithAuthorization_marks_used
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:457-464
  • 概要: 成功した 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 (s'.authorizationStates frm nonce) 1

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

解説 ​

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

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

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

図解 ​

Lean ソースコード ​

lean
theorem receiveWithAuthorization_marks_used {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') :
    s'.authorizationStates frm nonce = 1 := by
  obtain ⟨_, _, _, _, _, htr⟩ := _receiveWithAuthorization_ok (receiveWithAuthorization_eq_ok h)
  rw [_transfer_authorizationStates htr]
  exact setAuthorizationState_self s frm nonce 1

依存 ​