JPYCv2 形式検証

外観

JPYC.allowance ​

名称・種別 ​

  • 名称: JPYC.allowance
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:74-75
  • 概要: allowance(owner,spender)：承認額を返す読み取り専用ビュー。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → JPYC.Address → JPYC.U256

State・所有者 owner・支払い委任先 spender を受け取り、許可額 allowed[owner][spender] を返す純粋なビューです。

和訳 docstring ​

allowance(owner, spender) ― 許可額を返す。対応 Solidity: v2/FiatTokenV2.sol:159-166。

解説 ​

何を述べているか。 ERC20 の allowance(owner, spender) ビューです。二重マッピング allowed を引いて「owner が spender にどれだけの支払いを委任しているか」を返します。

直感。 「この人（spender）は、あの人（owner）の残高をいくらまで動かしてよいか」という上限額の読み取りです。設定がなければ既定値 0。

なぜ安全性に効くか。 approve_allowance は承認後にこの値が value になることを、transferFrom_allowance は transferFrom 後にこの値が value だけ減る（無限承認は不変）ことを保証します。allowance を「観測する」窓口がこのビューです。

図解 ​

Lean ソースコード ​

lean
/-- `allowance(owner, spender)` — `v2/FiatTokenV2.sol:159-166`. -/
def allowance (s : State) (owner spender : Address) : U256 := s.allowed owner spender

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:159-166

solidity
function allowance(address owner, address spender)
    external
    view
    override
    returns (uint256)
{
    return allowed[owner][spender];
}

依存 ​