JPYCv2 形式検証

外観

JPYC.decreaseAllowance ​

名称・種別 ​

  • 名称: JPYC.decreaseAllowance
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:125-132
  • 概要: decreaseAllowance(spender,decrement)：承認額をチェック付きで減らす関数（checkAllowlist なし）。
  • 仕様: 対象外

型シグネチャ ​

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

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

和訳 docstring ​

decreaseAllowance(spender, decrement) ― 許可額を decrement だけ減らす（この関数には checkAllowlist modifier が付かない）。対応 Solidity: v2/FiatTokenV2.sol:389-398。

解説 ​

何を述べているか。 decreaseAllowance(spender, decrement) です。現在の許可額から decrement を引いた値を新しい許可額にします。内部の _decreaseAllowance は、まず decrement ≤ 現在の許可額 を要求（FiatToken: decreased allowance below zero）してから checked な sub? で引きます。

直感。 increaseAllowance の逆です。許可額をマイナスにはできないので、減らしすぎる指定は revert します。この関数だけ checkAllowlist を持たない（許可額を減らす方向は規制対象でない）点が increaseAllowance との違いです。

なぜ安全性に効くか。 「減らしすぎてアンダーフロー」を require が防ぎ、checked sub? が二重に保証します。許可額のみを更新するため、wf_decreaseAllowance が WF 保存を示します。

図解 ​

Lean ソースコード ​

lean
/-- `decreaseAllowance(spender, decrement)` — `v2/FiatTokenV2.sol:389-398`
(note: this function carries no `checkAllowlist` modifier). -/
def decreaseAllowance (s : State) (ctx : CallContext) (spender : Address)
    (decrement : U256) : Except Error State := do
  whenNotPaused s
  notBlocklisted s ctx.sender
  notBlocklisted s spender
  _decreaseAllowance s ctx.sender spender decrement

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:389-398

solidity
function decreaseAllowance(address spender, uint256 decrement)
    external
    whenNotPaused
    notBlocklisted(msg.sender)
    notBlocklisted(spender)
    returns (bool)
{
    _decreaseAllowance(msg.sender, spender, decrement);
    return true;
}

依存 ​