JPYC.transferFrom

名称・種別

名称: JPYC.transferFrom
種別: def
モジュール: JpycFormalVerification.ERC20
ソース: JpycFormalVerification/ERC20.lean:178-188
概要: transferFrom(from,to,value)：承認を allowanceStep で処理後、_transfer で送金する関数。
仕様: 対象外

型シグネチャ

lean

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

State・CallContext・所有者 frm・受取人 dst・金額 value を受け取り、msg.sender が frm の許可額を消費して frm から dst へ送金する新しい状態を返します。

和訳 docstring

transferFrom(from, to, value) ― 許可額を allowanceStep で消費し、残高を _transfer で移す。対応 Solidity: v2/FiatTokenV2.sol:234-255。

解説

何を述べているか。 ERC20 の transferFrom(from, to, value) です。msg.sender（支払い者）が、あらかじめ from から委任された許可額を使って、from から to へ送金します。許可額の消費は allowanceStep、残高の移動は内部の _transfer が担います。

直感。 ガードは 5 つ ― whenNotPaused、msg.sender・frm・dst の三者すべての notBlocklisted、そして frm を主体とする checkAllowlist。通過後、許可額を消費し（無限承認なら据え置き）、残高を移します。

なぜ安全性に効くか。 第三者送金は allowance を悪用されると危険です。成功時に許可額がちょうど value 減ること（無限承認は不変）を transferFrom_allowance が示し、リプレイ的な多重支払いを防ぎます。総供給不変（transferFrom_totalSupply）・WF・SupplyConserved 保存も併せて証明されます。

図解

Lean ソースコード

lean

/-- `transferFrom(from, to, value)` — `v2/FiatTokenV2.sol:234-255`. The allowance
is handled by `allowanceStep`, then the balances move via `_transfer`. -/
def transferFrom (s : State) (ctx : CallContext) (frm dst : Address) (value : U256) :
    Except Error State := do
  whenNotPaused s
  notBlocklisted s ctx.sender
  notBlocklisted s frm
  notBlocklisted s dst
  checkAllowlist s frm value
  let s₁ ← allowanceStep s frm ctx.sender value
  _transfer s₁ frm dst value

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:234-255

solidity

function transferFrom(
    address from,
    address to,
    uint256 value
)
    external
    override
    whenNotPaused
    notBlocklisted(msg.sender)
    notBlocklisted(from)
    notBlocklisted(to)
    checkAllowlist(from, value)
    returns (bool)
{
    uint256 _allowed = allowed[from][msg.sender];
    if (_allowed != type(uint256).max) {
        require(_allowed >= value, "FiatToken: transfer amount exceeds allowance");
        allowed[from][msg.sender] = _allowed - value;
    }
    _transfer(from, to, value);
    return true;
}

JPYC.transferFrom ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​