JPYCv2 形式検証

外観

JPYC.cancelAuthorization_wf ​

名称・種別 ​

  • 名称: JPYC.cancelAuthorization_wf
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:577-581
  • 概要: cancelAuthorization は健全性不変条件 WF を保つ、という定理。
  • 仕様: 対象

型シグネチャ ​

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

cancelAuthorization が成功するなら、結果状態も WF を満たす、という不変条件保存の定理です。

解説 ​

何を述べているか。 事前状態が WF を満たし、cancelAuthorization が成功すれば、結果も WF を満たします。authorization 台帳に 1 を書くだけなので WF_setAuthorizationState から直ちに従います。

直感。 キャンセルは 1 マスを 1 にするだけ。0/1 性は崩れません。

なぜ安全性に効くか。 取り消し操作も状態の健全性（フラグの 0/1 性・版数の範囲）を保つことを保証します。

図解 ​

Lean ソースコード ​

lean
theorem cancelAuthorization_wf {O : SigOracle} {s s' : State} {ctx : CallContext}
    {authorizer : Address} {nonce : Bytes32} {v : U8} {r sig : Bytes32} (hwf : WF s)
    (h : cancelAuthorization O s ctx authorizer nonce v r sig = .ok s') : WF s' := by
  obtain ⟨_, _, rfl⟩ := _cancelAuthorization_ok (cancelAuthorization_eq_ok h)
  exact WF_setAuthorizationState hwf authorizer nonce (Or.inr rfl)

依存 ​