JPYC.balanceOf

名称・種別

• 名称: JPYC.balanceOf
• 種別: def
• モジュール: JpycFormalVerification.ERC20
• ソース: JpycFormalVerification/ERC20.lean:68-69
• 概要: balanceOf(account)：口座残高を返す読み取り専用ビュー。
• 仕様: 対象外

型シグネチャ

JPYC.State → JPYC.Address → JPYC.U256

State とアドレス account を受け取り、その残高（s.balances account）を返す純粋な読み取り関数です。

和訳 docstring

balanceOf(account) ― アカウントの残高を返す。対応 Solidity: v2/FiatTokenV2.sol:181-188。

解説

何を述べているか。 ERC20 の balanceOf(account) ビューです。状態を変えず、balances マッピングを引くだけです。

直感。 台帳から 1 行を読むだけ。まだ一度も入金されていないアドレスは、全域関数の既定値である残高 0 を返します（State の mapping モデル）。

なぜ安全性に効くか。 読み取り専用なので、それ自体は状態を壊しません。むしろ transfer_frame などの定理が「balanceOf で観測される値が、無関係なアカウントについては変わらない」と主張するときの「観測窓」として機能します。

図解

Lean ソースコード

/-- `balanceOf(account)` — `v2/FiatTokenV2.sol:181-188`. -/
def balanceOf (s : State) (account : Address) : U256 := s.balances account

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:181-188

function balanceOf(address account)
    external
    view
    override
    returns (uint256)
{
    return balances[account];
}

依存

• JPYC.Address
• JPYC.State
• JPYC.U256