JPYC.burn

名称・種別

名称: JPYC.burn
種別: def
モジュール: JpycFormalVerification.AccessControl
ソース: JpycFormalVerification/AccessControl.lean:189-201
概要: burn(_amount)：呼び出し元が自身のトークンを焼却する関数（minter 限定）。
仕様: 対象外

型シグネチャ

lean

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

State・CallContext・金額 amount を受け取り、登録ミンターが自分自身のトークンを焼却（burn）する関数です。

和訳 docstring

登録ミンターが自分のトークン amount を焼却する。総供給と自残高を減算する（checked）。v2/FiatTokenV2.sol:340-354。

解説

何を述べているか。 FiatTokenV2.burn です。whenNotPaused → onlyMinters → 送り手の notBlocklisted を通り、「金額が正」「金額 ≤ 自分の残高」を確かめてから、totalSupply_ と balances[sender] を checked な sub? で減らします。

直感。 「お金を破棄する」操作です。mint の逆で、総供給と呼び出し元の残高が amount 減ります。焼けるのは 自分の トークンだけです。

なぜ安全性に効くか。 総供給と残高がちょうど amount 減ること（burn_totalSupply / burn_balance）、残高不足なら revert（sub? が burnExceedsBalance）、呼び出し元以外の残高は不変（burn_frame）、SupplyConserved と WF 保存（burn_conserves / burn_wf）が証明されます。

図解

Lean ソースコード

lean

/-- `burn(_amount)` — `v2/FiatTokenV2.sol:340-354`. The caller burns its own
tokens; `totalSupply_ -= _amount` and `balances[sender] -= _amount` are checked. -/
def burn (s : State) (ctx : CallContext) (amount : U256) :
    Except Error State := do
  whenNotPaused s
  onlyMinters s ctx
  notBlocklisted s ctx.sender
  let balance := s.balances ctx.sender
  req (0 < amount) .burnAmountNotPositive
  req (amount ≤ balance) .burnExceedsBalance
  let newSupply ← sub? s.totalSupply amount
  let newBalance ← sub? balance amount
  pure ((s.setTotalSupply newSupply).setBalance ctx.sender newBalance)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:340-354

solidity

function burn(uint256 _amount)
    external
    whenNotPaused
    onlyMinters
    notBlocklisted(msg.sender)
{
    uint256 balance = balances[msg.sender];
    require(_amount > 0, "FiatToken: burn amount not greater than 0");
    require(balance >= _amount, "FiatToken: burn amount exceeds balance");

    totalSupply_ = totalSupply_ - _amount;
    balances[msg.sender] = balance - _amount;
    emit Burn(msg.sender, _amount);
    emit Transfer(msg.sender, address(0), _amount);
}

JPYC.burn ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​