JPYCv2 形式検証

外観

JPYC.increaseAllowance_eq_ok ​

名称・種別 ​

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

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {increment : JPYC.U256}, Eq (JPYC.increaseAllowance s ctx spender increment) (Except.ok s') → Eq (JPYC._increaseAllowance s ctx.sender spender increment) (Except.ok s')

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

和訳 docstring ​

成功した increaseAllowance は、呼び出し元を所有者とする _increaseAllowance の成功に還元される（修飾子ガードと checkAllowlist 引数の加算は成功時には無影響）。approve_eq_ok と同型。

解説 ​

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

直感。 approve_eq_ok と同じ構造です。whenNotPaused・notBlocklisted×2 を req_bind_eq_ok で剥がし、checkAllowlist の引数に渡る checked 加算を bind_eq_ok で、checkAllowlist 自体を checkAllowlist_bind_eq_ok で吸収すると _increaseAllowance が残ります。

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

図解 ​

Lean ソースコード ​

lean
/-- A successful `increaseAllowance` reduces to `_increaseAllowance` from the
caller (modifier guards and the `checkAllowlist` argument add are no-ops on
success), mirroring `approve_eq_ok`. -/
theorem increaseAllowance_eq_ok {s s' : State} {ctx : CallContext} {spender : Address}
    {increment : U256} (h : increaseAllowance s ctx spender increment = .ok s') :
    _increaseAllowance s ctx.sender spender increment = .ok s' := by
  unfold increaseAllowance 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
  obtain ⟨_, _, h⟩ := bind_eq_ok h
  exact checkAllowlist_bind_eq_ok h

依存 ​