JPYCv2 形式検証

外観

JPYC.increaseAllowance ​

名称・種別 ​

  • 名称: JPYC.increaseAllowance
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:103-114
  • 概要: increaseAllowance(spender,increment)：承認額をチェック付きで増やす関数。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.CallContext → JPYC.Address → JPYC.U256 → Except JPYC.Error JPYC.State

State・CallContext・委任先 spender・増分 increment を受け取り、許可額を increment だけ 増やした 新しい状態を返します。

和訳 docstring ​

increaseAllowance(spender, increment) ― 許可額を increment だけ増やす。checkAllowlist には「増分後の許可額」が（先行 modifier の後に）checked 加算で渡されるため、モデルでも checkAllowlist の手前に add? が現れる。対応 Solidity: v2/FiatTokenV2.sol:371-381。

解説 ​

何を述べているか。 increaseAllowance(spender, increment) です。現在の許可額に increment を足した値を新しい許可額として設定します。加算は checked な add? なので、2²⁵⁶ を超えるとオーバーフローで revert します。

直感。 approve の「上書き」と違い、こちらは「積み増し」です。checkAllowlist には 増分後の値 allowed[msg.sender][spender] + increment が渡される点に注意。この checked 加算は modifier 評価時に行われるため、Lean モデルでも checkAllowlist の前に add? が現れます。

なぜ安全性に効くか。 既存の approve を一度 0 にしてから再設定する「フロントランニング」リスクを避ける ERC20 拡張です。許可額の更新は State.setAllowance 経由なので残高・供給に触れず、wf_increaseAllowance が WF 保存を保証します。

図解 ​

Lean ソースコード ​

lean
/-- `increaseAllowance(spender, increment)` — `v2/FiatTokenV2.sol:371-381`.
The `checkAllowlist` modifier argument `allowed[msg.sender][spender] + increment`
is a checked add evaluated (after the preceding modifiers) before the body, so it
appears here ahead of `checkAllowlist`. -/
def increaseAllowance (s : State) (ctx : CallContext) (spender : Address)
    (increment : U256) : Except Error State := do
  whenNotPaused s
  notBlocklisted s ctx.sender
  notBlocklisted s spender
  let checkValue ← add? (s.allowed ctx.sender spender) increment
  checkAllowlist s ctx.sender checkValue
  _increaseAllowance s ctx.sender spender increment

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:371-381

solidity
function increaseAllowance(address spender, uint256 increment)
    external
    whenNotPaused
    notBlocklisted(msg.sender)
    notBlocklisted(spender)
    checkAllowlist(msg.sender, allowed[msg.sender][spender] + increment)
    returns (bool)
{
    _increaseAllowance(msg.sender, spender, increment);
    return true;
}

依存 ​