JPYC.approve

名称・種別

名称: JPYC.approve
種別: def
モジュール: JpycFormalVerification.ERC20
ソース: JpycFormalVerification/ERC20.lean:86-93
概要: approve(spender,value)：承認額を value に設定する関数。
仕様: 対象外

型シグネチャ

lean

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

State・呼び出し文脈 CallContext・委任先 spender・金額 value を受け取り、4 つのガードを通過したのち allowed[msg.sender][spender] = value を設定した新しい状態を返します（失敗時は revert）。

和訳 docstring

approve(spender, value) ― 呼び出し元の許可額を value に設定する。対応 Solidity: v2/FiatTokenV2.sol:197-208。

解説

何を述べているか。 ERC20 の approve(spender, value) です。msg.sender が spender に対する許可額を value に設定します（加算ではなく上書き）。本体は内部関数 _approve で、ゼロアドレスを弾いてから許可額を書き込みます。

直感。 4 つの関所を順に通ります ― whenNotPaused → 送り手の notBlocklisted → spender の notBlocklisted → checkAllowlist。すべて通れば許可額を上書きします。

なぜ安全性に効くか。 「停止中でない」「双方がブロックされていない」「大口なら許可済み」という前提が揃ったときだけ成功します。成功時に許可額がちょうど value になることは approve_allowance が、WF と SupplyConserved が保たれることは wf_approve / approve_conserves が示します。

図解

Lean ソースコード

lean

/-- `approve(spender, value)` — `v2/FiatTokenV2.sol:197-208`. -/
def approve (s : State) (ctx : CallContext) (spender : Address) (value : U256) :
    Except Error State := do
  whenNotPaused s
  notBlocklisted s ctx.sender
  notBlocklisted s spender
  checkAllowlist s ctx.sender value
  _approve s ctx.sender spender value

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:197-208

solidity

function approve(address spender, uint256 value)
    external
    override
    whenNotPaused
    notBlocklisted(msg.sender)
    notBlocklisted(spender)
    checkAllowlist(msg.sender, value)
    returns (bool)
{
    _approve(msg.sender, spender, value);
    return true;
}

JPYC.approve ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​