JPYCv2 形式検証

外観

JPYC.transferFrom_allowance ​

名称・種別 ​

  • 名称: JPYC.transferFrom_allowance
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:424-436
  • 概要: 承認が有限なら transferFrom は allowed を value だけ減らし、無限承認は据え置く（承認整合性）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {frm dst : JPYC.Address} {value : JPYC.U256}, Eq (JPYC.transferFrom s ctx frm dst value) (Except.ok s') → Eq (s'.allowed frm ctx.sender) (ite (Eq (s.allowed frm ctx.sender) JPYC.MAX_U256) (s.allowed frm ctx.sender) (instHSub.hSub (s.allowed frm ctx.sender) value))

transferFrom が成功したとき、結果の許可額 s'.allowed frm ctx.sender は ― 元が MAX_U256（無限承認）なら据え置き、そうでなければ value だけ減った値 ― になる、という定理です。

和訳 docstring ​

許可額の整合性 ― 有限承認は transferFrom 成功でちょうど value 減り、無限承認（type(uint256).max）は据え置かれる。

解説 ​

何を述べているか。 allowance integrity（許可額の整合性）です。成功後の許可額は、無限承認（MAX_U256）なら不変、有限ならちょうど value 減ります（if で正確に場合分け）。

直感。 許可額の更新は allowanceStep だけが行い、後続の _transfer は allowed に触れません（_transfer_allowed）。だから結果の許可額は中間状態 s₁ の許可額に等しく、setAllowance_allowed_self で値が確定します。

なぜ安全性に効くか。 「使った分だけ、ちょうど許可枠が減る」ことを保証し、同じ承認での二重支払い（過剰消費）を防ぎます。無限承認の慣習も忠実に再現しつつ、有限承認では枠が確実に目減りする ― allowance を使ったリプレイ攻撃への防御です。

図解 ​

Lean ソースコード ​

lean
/-- **Allowance integrity.** When the approval is finite, a successful
`transferFrom` decreases `allowed[from][spender]` by exactly `value`; an infinite
(`type(uint256).max`) approval is left untouched. -/
theorem transferFrom_allowance {s s' : State} {ctx : CallContext} {frm dst : Address}
    {value : U256} (h : transferFrom s ctx frm dst value = .ok s') :
    s'.allowed frm ctx.sender
      = if s.allowed frm ctx.sender = MAX_U256 then s.allowed frm ctx.sender
        else s.allowed frm ctx.sender - value := by
  obtain ⟨s₁, hstep, htrans⟩ := transferFrom_eq_ok h
  have hpres : s'.allowed = s₁.allowed := _transfer_allowed htrans
  rcases hstep with ⟨hmax, rfl⟩ | ⟨hmax, _, rfl⟩
  · rw [hpres, if_pos hmax]
  · rw [hpres, setAllowance_allowed_self, if_neg hmax]

依存 ​