JPYCv2 形式検証

外観

JPYC.cancelAuthorization_marks_used ​

名称・種別 ​

  • 名称: JPYC.cancelAuthorization_marks_used
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:545-551
  • 概要: 成功した cancelAuthorization は認可を使用済みにする（効果）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {authorizer : JPYC.Address} {nonce : JPYC.Bytes32} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.cancelAuthorization O s ctx authorizer nonce v r sig) (Except.ok s') → Eq (s'.authorizationStates authorizer nonce) 1

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

和訳 docstring ​

効果。 成功した cancelAuthorization は対象 authorization を使用済みにする。

解説 ​

何を述べているか。 cancelAuthorization が成功した結果状態では s'.authorizationStates authorizer nonce = 1 です。内部で setAuthorizationState authorizer nonce 1 を行い、それがそのまま読めます（setAuthorizationState_self）。cancelAuthorization は送金を伴わないので、結果状態はこの 1 マス更新だけです。

直感。 「キャンセル＝その引換券に使用済みの判を押す」。これにより、本来の送金を後から実行しようとしても未使用ガードに弾かれます。

なぜ安全性に効くか。 cancelAuthorization_blocks_transfer（キャンセル後は送金不可）の直接の根拠です。署名者が漏れた署名を事前に無効化できる安全弁を実現します。

図解 ​

Lean ソースコード ​

lean
/-- **Effect.** A successful `cancelAuthorization` marks the authorization used. -/
theorem cancelAuthorization_marks_used {O : SigOracle} {s s' : State} {ctx : CallContext}
    {authorizer : Address} {nonce : Bytes32} {v : U8} {r sig : Bytes32}
    (h : cancelAuthorization O s ctx authorizer nonce v r sig = .ok s') :
    s'.authorizationStates authorizer nonce = 1 := by
  obtain ⟨_, _, rfl⟩ := _cancelAuthorization_ok (cancelAuthorization_eq_ok h)
  exact setAuthorizationState_self s authorizer nonce 1

依存 ​