JPYCv2 形式検証

外観

JPYC.decreaseAllowance_allowance ​

名称・種別 ​

  • 名称: JPYC.decreaseAllowance_allowance
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:595-610
  • 概要: 成功した decreaseAllowance は allowed[msg.sender][spender] を decrement 分（checked）減らす、という効果定理。
  • 仕様: 対象

型シグネチャ ​

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 (instHAdd.hAdd (BitVec.toNat (s'.allowed ctx.sender spender)) (BitVec.toNat decrement)) (BitVec.toNat (s.allowed ctx.sender spender))

decreaseAllowance が成功したとき、新しい許可額 + decrement = 元の許可額（いずれも toNat の自然数）が成り立つ、という定理です。すなわち許可額がちょうど decrement だけ減ります。

和訳 docstring ​

効果。 成功した decreaseAllowance は allowed[msg.sender][spender] を decrement だけ減らす（ガード decrement ≤ allowed により checked な - が、ゼロを下回らずに成功する）。

解説 ​

何を述べているか。 許可額の 減額 が成功すれば、許可枠はちょうど decrement 分だけ減ります。式を 新値 + decrement = 旧値 の形で述べているのは、burn_balance と同じく自然数の引き算（桁借りの回り込みなし）を明示するためです。

直感。 decreaseAllowance_eq_ok で _decreaseAllowance に還元すると、本体はまず require(decrement ≤ allowed) を確認し、checked sub? で old - decrement を計算して _approve で書き込むだけ。書いた値が読める setAllowance_allowed_self と、成功した減算が自然数減算に一致する sub?_toNat を omega でまとめます。

なぜ安全性に効くか。 increaseAllowance_allowance と対称に、「減らすと言ったら、まさにその分だけ減る（しかもゼロ未満にならない）」を保証します。許可枠が想定外の巨大値に化けたり負に回り込んだりしないことの証明です。

図解 ​

Lean ソースコード ​

lean
/-- **Effect.** A successful `decreaseAllowance` lowers `allowed[msg.sender][spender]`
by `decrement` (the guard `decrement ≤ allowed` makes the checked `-` succeed
without dropping below zero). -/
theorem decreaseAllowance_allowance {s s' : State} {ctx : CallContext} {spender : Address}
    {decrement : U256} (h : decreaseAllowance s ctx spender decrement = .ok s') :
    (s'.allowed ctx.sender spender).toNat + decrement.toNat
      = (s.allowed ctx.sender spender).toNat := by
  have h := decreaseAllowance_eq_ok h
  unfold _decreaseAllowance at h
  obtain ⟨hle, h⟩ := req_bind_eq_ok h
  obtain ⟨v, hsub, h⟩ := bind_eq_ok h
  obtain ⟨_, _, rfl⟩ := _approve_ok h
  rw [setAllowance_allowed_self]
  have hv : v.toNat = (s.allowed ctx.sender spender).toNat - decrement.toNat := sub?_toNat hsub
  have hle' : decrement.toNat ≤ (s.allowed ctx.sender spender).toNat := BitVec.le_def.mp hle
  omega

依存 ​