JPYCv2 形式検証

外観

JPYC.cancelAuthorization_blocks_transfer ​

名称・種別 ​

  • 名称: JPYC.cancelAuthorization_blocks_transfer
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:561-575
  • 概要: (authorizer,nonce) を取り消した後は、同じ (from,nonce) の transferWithAuthorization は成功しない。
  • 仕様: 対象

型シグネチャ ​

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') → ∀ {ctx' : JPYC.CallContext} {dst' : JPYC.Address} {value' validAfter' validBefore' : JPYC.U256} {v' : JPYC.U8} {r' sig' : JPYC.Bytes32} {s'' : JPYC.State}, Ne (JPYC.transferWithAuthorization O s' ctx' authorizer dst' value' validAfter' validBefore' nonce v' r' sig') (Except.ok s'')

ある (authorizer, nonce) をキャンセルした後は、同じ (from, nonce) の transferWithAuthorization が二度と成功しない、という 取り消しの実効性 の定理です。

和訳 docstring ​

キャンセルの実効性。 authorization をキャンセルした後は、同じ (from, nonce) の transferWithAuthorization は成功しない。

解説 ​

何を述べているか。 cancelAuthorization が成功して状態が s' になったあと、同じ (authorizer, nonce) を from に使う transferWithAuthorization（他の引数・文脈は自由）は .ok にならないことを示します。背理法で、キャンセルが立てた使用済みマーク（= 1、cancelAuthorization_marks_used）と、送金成功に必要な未使用条件（= 0、transferWithAuthorization_unused）の矛盾を使います。

直感。 「取り消した送金指示は、もう実行できない」。キャンセルも送金も同じ authorization スロットを共有し、キャンセルがそれを使い切るからです。

なぜ安全性に効くか。 取り消し機能が 実効的 であることの保証です。署名してしまった指示が漏れても、署名者は使われる前にキャンセルすれば確実に無効化できます。

図解 ​

Lean ソースコード ​

lean
/-- **Cancel prevents use.** After a `(authorizer, nonce)` authorization is
canceled, no `transferWithAuthorization` with the same `(from, nonce)` can
succeed. -/
theorem cancelAuthorization_blocks_transfer {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')
    {ctx' : CallContext} {dst' : Address} {value' validAfter' validBefore' : U256} {v' : U8}
    {r' sig' : Bytes32} {s'' : State} :
    transferWithAuthorization O s' ctx' authorizer dst' value' validAfter' validBefore' nonce v' r' sig'
      ≠ .ok s'' := by
  intro hxfer
  have hused := cancelAuthorization_marks_used h
  have hunused := transferWithAuthorization_unused hxfer
  rw [hused] at hunused
  exact absurd hunused (by decide)

依存 ​