JPYC.transfer

名称・種別

名称: JPYC.transfer
種別: def
モジュール: JpycFormalVerification.ERC20
ソース: JpycFormalVerification/ERC20.lean:154-161
概要: transfer(to,value)：各ガードを通過後に _transfer で送金する関数。
仕様: 対象外

型シグネチャ

lean

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

State・CallContext・受取人 dst・金額 value を受け取り、4 つのガードを通過したのち msg.sender から dst へ value を移す新しい状態を返します。

和訳 docstring

transfer(to, value) ― 呼び出し元から to へ value を送金する。対応 Solidity: v2/FiatTokenV2.sol:263-274。

解説

何を述べているか。 ERC20 の transfer(to, value) です。呼び出し元 msg.sender の残高から value を引き、dst の残高に value を足します。本体は内部関数 _transfer（ゼロアドレス検査・残高検査・checked な減算/加算）です。

直感。 4 つの関所（whenNotPaused → 送り手・受取人の notBlocklisted → checkAllowlist）を通過したら送金。残高不足なら transfer amount exceeds balance で revert します。

なぜ安全性に効くか。 ステーブルコインの心臓部です。成功時に総供給が不変であること（transfer_totalSupply）、無関係なアカウントに影響しないこと（transfer_frame）、残高不足では失敗し状態が変わらないこと、自己送金が安全であること（transfer_self）が、後続の定理群で証明されます。

図解

Lean ソースコード

lean

/-- `transfer(to, value)` — `v2/FiatTokenV2.sol:263-274`. -/
def transfer (s : State) (ctx : CallContext) (dst : Address) (value : U256) :
    Except Error State := do
  whenNotPaused s
  notBlocklisted s ctx.sender
  notBlocklisted s dst
  checkAllowlist s ctx.sender value
  _transfer s ctx.sender dst value

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:263-274

solidity

function transfer(address to, uint256 value)
    external
    override
    whenNotPaused
    notBlocklisted(msg.sender)
    notBlocklisted(to)
    checkAllowlist(msg.sender, value)
    returns (bool)
{
    _transfer(msg.sender, to, value);
    return true;
}

JPYC.transfer ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​