JPYC.mint

名称・種別

名称: JPYC.mint
種別: def
モジュール: JpycFormalVerification.AccessControl
ソース: JpycFormalVerification/AccessControl.lean:166-187
概要: mint(_to,_amount)：許容額の範囲で新規発行する関数（minter 限定、checkAllowlist 付き）。
仕様: 対象外

型シグネチャ

lean

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

State・CallContext・受取人 dst・金額 amount を受け取り、登録ミンターが許可量の範囲内で新規トークンを発行する関数です。

和訳 docstring

登録ミンターが dst 宛に amount を発行する。総供給・受取人残高を加算し、ミンター許可量を減算する（各演算は checked）。dst は _to（Solidity の to は Lean の予約語）。v2/FiatTokenV2.sol:97-121。

解説

何を述べているか。 FiatTokenV2.mint です。whenNotPaused → onlyMinters → 送り手と受取人の notBlocklisted → checkAllowlist という 5 つのガードを通り、さらに「受取人がゼロアドレスでない」「金額が正」「金額 ≤ ミンターの許可量」を確かめてから、3 つの値（totalSupply_・balances[dst]・minterAllowed[sender]）を checked 演算で更新します。

直感。 「無から新しいお金を刷る」操作です。総供給と受取人残高が amount 増え、刷ったミンターの許可枠が amount 減ります。add? / sub? を使うので、あふれ・枠不足は revert になります。

なぜ安全性に効くか。 発行は最も危険な操作なので、ガードが何重にも掛かっています。総供給と残高がちょうど amount 増えること（mint_totalSupply / mint_balance）、許可量を超えないこと（mint_minterAllowed）、受取人以外の残高は不変（mint_frame）、そして SupplyConserved と WF が保たれること（mint_conserves / mint_wf）まで証明されます。3 つの書き込みは独立フィールドなので順序に依存しません。

図解

Lean ソースコード

lean

/-- `mint(_to, _amount)` — `v2/FiatTokenV2.sol:97-121` (`dst` models the `_to`
payee, whose Solidity name `to` is a Lean keyword).

The three storage writes (`totalSupply_`, `balances[_to]`, `minterAllowed[sender]`)
touch independent fields, so their values are all computed from the pre-state and
the write order is irrelevant; each `+` / `-` is checked (`add?` / `sub?`). -/
def mint (s : State) (ctx : CallContext) (dst : Address) (amount : U256) :
    Except Error State := do
  whenNotPaused s
  onlyMinters s ctx
  notBlocklisted s ctx.sender
  notBlocklisted s dst
  checkAllowlist s ctx.sender amount
  req (dst ≠ Address.zero) .mintToZero
  req (0 < amount) .mintAmountNotPositive
  let mintingAllowedAmount := s.minterAllowed ctx.sender
  req (amount ≤ mintingAllowedAmount) .mintExceedsMinterAllowance
  let newSupply ← add? s.totalSupply amount
  let newBalance ← add? (s.balances dst) amount
  let newMinterAllowed ← sub? mintingAllowedAmount amount
  pure (((s.setTotalSupply newSupply).setBalance dst newBalance).setMinterAllowed
    ctx.sender newMinterAllowed)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:97-121

solidity

function mint(address _to, uint256 _amount)
    external
    whenNotPaused
    onlyMinters
    notBlocklisted(msg.sender)
    notBlocklisted(_to)
    checkAllowlist(msg.sender, _amount)
    returns (bool)
{
    require(_to != address(0), "FiatToken: mint to the zero address");
    require(_amount > 0, "FiatToken: mint amount not greater than 0");

    uint256 mintingAllowedAmount = minterAllowed[msg.sender];
    require(
        _amount <= mintingAllowedAmount,
        "FiatToken: mint amount exceeds minterAllowance"
    );

    totalSupply_ = totalSupply_ + _amount;
    balances[_to] = balances[_to] + _amount;
    minterAllowed[msg.sender] = mintingAllowedAmount - _amount;
    emit Mint(msg.sender, _to, _amount);
    emit Transfer(address(0), _to, _amount);
    return true;
}

JPYC.mint ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​