JPYCv2 形式検証

外観

JPYC.totalSupply ​

名称・種別 ​

  • 名称: JPYC.totalSupply
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:71-72
  • 概要: totalSupply()：総供給量を返す読み取り専用ビュー。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.U256

State を受け取り、記録上の総供給量（s.totalSupply）を返す純粋なビューです。

和訳 docstring ​

totalSupply() ― 総供給量を返す。対応 Solidity: v2/FiatTokenV2.sol:172-174。

解説 ​

何を述べているか。 ERC20 の totalSupply() ビューです。状態に保持された総供給量フィールドをそのまま返します。

直感。 「いま何トークン発行されていることになっているか」を読むだけの関数です。

なぜ安全性に効くか。 SupplyConserved は「この totalSupply が全残高の合計と一致する」という不変条件でした。transfer_totalSupply / transferFrom_totalSupply は送金で総供給が変わらないことを、mint/burn 系（Phase 2）は意図どおりに増減することを、いずれもこのビューを基準に述べています。

図解 ​

Lean ソースコード ​

lean
/-- `totalSupply()` — `v2/FiatTokenV2.sol:172-174`. -/
def totalSupply (s : State) : U256 := s.totalSupply

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:172-174

solidity
function totalSupply() external view override returns (uint256) {
    return totalSupply_;
}

依存 ​