JPYCv2 形式検証

外観

JPYC.decreaseAllowance_eq_ok ​

名称・種別 ​

  • 名称: JPYC.decreaseAllowance_eq_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:584-593
  • 概要: 成功した decreaseAllowance は呼び出し元からの _decreaseAllowance に還元される、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {decrement : JPYC.U256}, Eq (JPYC.decreaseAllowance s ctx spender decrement) (Except.ok s') → Eq (JPYC._decreaseAllowance s ctx.sender spender decrement) (Except.ok s')

decreaseAllowance が成功するなら、内部の _decreaseAllowance s ctx.sender spender decrement も同じ結果で成功する、という還元定理です。

和訳 docstring ​

成功した decreaseAllowance は、呼び出し元を所有者とする _decreaseAllowance の成功に還元される（decreaseAllowance は checkAllowlist 修飾子を持たない）。

解説 ​

何を述べているか。 外部関数 decreaseAllowance の成功は、ガードを通過した後の内部関数 _decreaseAllowance（所有者 = ctx.sender）の成功に等しいと示します。

直感。 increaseAllowance_eq_ok と同様ですが、decreaseAllowance には checkAllowlist 修飾子が無い分シンプルです。whenNotPaused・notBlocklisted×2 を req_bind_eq_ok で剥がすと _decreaseAllowance がそのまま残ります。

なぜ安全性に効くか。 decreaseAllowance の性質（許可額の減分・供給保存）を、_decreaseAllowance／_approve の補題を持ち上げて導くための要石です。外部入口と内部本体をつなぎます。

図解 ​

Lean ソースコード ​

lean
/-- A successful `decreaseAllowance` reduces to `_decreaseAllowance` from the
caller (`decreaseAllowance` carries no `checkAllowlist` modifier). -/
theorem decreaseAllowance_eq_ok {s s' : State} {ctx : CallContext} {spender : Address}
    {decrement : U256} (h : decreaseAllowance s ctx spender decrement = .ok s') :
    _decreaseAllowance s ctx.sender spender decrement = .ok s' := by
  unfold decreaseAllowance whenNotPaused notBlocklisted at h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  exact h

依存 ​