JPYC.cancelAuthorization_conserves

名称・種別

名称: JPYC.cancelAuthorization_conserves
種別: theorem
モジュール: JpycFormalVerification.SignaturesTheorems
ソース: JpycFormalVerification/SignaturesTheorems.lean:569-573
概要: cancelAuthorization は供給保存不変条件 SupplyConserved を保つ、という定理。
仕様: 対象

型シグネチャ

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.SupplyConserved s → Eq (JPYC.cancelAuthorization O s ctx authorizer nonce v r sig) (Except.ok s') → JPYC.SupplyConserved s'

cancelAuthorization が成功するなら、結果状態も SupplyConserved を満たす、という供給保存の定理です。

解説

何を述べているか。 事前状態が SupplyConserved を満たし、cancelAuthorization が成功すれば、結果も供給保存を満たします。キャンセルは authorization 台帳のマスを変えるだけで、残高・総供給に触れません。

直感。 取り消しは送金ではないので、トークンの動きは一切なし。帳簿の釣り合いはそのままです。

なぜ安全性に効くか。 取り消し操作が会計健全性に対して完全に中立であることを保証します。

図解

Lean ソースコード

lean

theorem cancelAuthorization_conserves {O : SigOracle} {s s' : State} {ctx : CallContext}
    {authorizer : Address} {nonce : Bytes32} {v : U8} {r sig : Bytes32} (hc : SupplyConserved s)
    (h : cancelAuthorization O s ctx authorizer nonce v r sig = .ok s') : SupplyConserved s' := by
  obtain ⟨_, _, rfl⟩ := _cancelAuthorization_ok (cancelAuthorization_eq_ok h)
  exact supplyConserved_of_balances_totalSupply_eq hc rfl rfl

JPYC.cancelAuthorization_conserves ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.cancelAuthorization_conserves

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存