JPYCv2 形式検証

外観

JPYC.increaseAllowance_allowance ​

名称・種別 ​

  • 名称: JPYC.increaseAllowance_allowance
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:562-573
  • 概要: 成功した increaseAllowance は allowed[msg.sender][spender] を increment 分（checked）増やす、という効果定理。
  • 仕様: 対象

型シグネチャ ​

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

increaseAllowance が成功したとき、新しい許可額 s'.allowed ctx.sender spender を toNat（自然数）で見ると、元の許可額に increment を加えた値にちょうど等しい、という定理です。

和訳 docstring ​

効果。 成功した increaseAllowance は allowed[msg.sender][spender] を increment だけ増やす（+ は checked なので、新しい値はオーバーフローしない）。

解説 ​

何を述べているか。 許可額の 増額 が成功すれば、許可枠はちょうど increment 分だけ増えます。toNat で述べているのは、checked 加算が成功した結果あふれが起きていない（自然数の加算と一致する）ことまで含めて保証するためです。

直感。 approve_allowance（上書き）の増分版です。increaseAllowance_eq_ok で _increaseAllowance に還元すると、本体は add? で old + increment を計算し _approve で書き込むだけ。書いた値がそのまま読める setAllowance_allowed_self と、成功した加算が自然数加算に一致する add?_toNat で確定します。

なぜ安全性に効くか。 「増やすと言ったら、まさにその分だけ増える（しかもあふれない）」という ERC20 の契約を保証します。増額時に枠が想定外の値に化けることが無いことの証明で、approve 側の対称性を埋めます。

図解 ​

Lean ソースコード ​

lean
/-- **Effect.** A successful `increaseAllowance` raises `allowed[msg.sender][spender]`
by `increment` (the `+` is checked, so the new value does not overflow). -/
theorem increaseAllowance_allowance {s s' : State} {ctx : CallContext} {spender : Address}
    {increment : U256} (h : increaseAllowance s ctx spender increment = .ok s') :
    (s'.allowed ctx.sender spender).toNat
      = (s.allowed ctx.sender spender).toNat + increment.toNat := by
  have h := increaseAllowance_eq_ok h
  unfold _increaseAllowance at h
  obtain ⟨v, hadd, h⟩ := bind_eq_ok h
  obtain ⟨_, _, rfl⟩ := _approve_ok h
  rw [setAllowance_allowed_self]
  exact add?_toNat hadd

依存 ​