JPYC.Address.zero

名称・種別

• 名称: JPYC.Address.zero
• 種別: def
• モジュール: JpycFormalVerification.Address
• ソース: JpycFormalVerification/Address.lean:16-18
• 概要: ゼロアドレス address(0)。多くのガードが拒否する特別な値。
• 仕様: 対象外

型シグネチャ

JPYC.Address

戻り値の型は JPYC.Address。引数を取らない 定数 で、ゼロアドレス address(0)（全ビット 0）を表します。

和訳 docstring

ゼロアドレス address(0)。FiatTokenV2 の多くのガードがこれを禁止する（例:「ゼロアドレスへの送金」）。

解説

何を述べているか。 「宛先なし」を意味する特別なアドレス、全ビットが 0 の値です。0 : BitVec 160 として定義しています。

直感。 Solidity の多くの require は、送金先や新しいロールにゼロアドレスを指定することを禁止します。ゼロアドレスへ送ると資金が事実上焼失し、ロールをゼロアドレスにすると権限が永久に失われるからです。

なぜ安全性に効くか。 transferToZero / mintToZero / newOwnerZero などのガード（Error）が比較する基準点です。これにより「ゼロアドレスへ送って資金消失」「ロールをゼロにして権限喪失」といった事故を排除できます。

図解

Lean ソースコード

/-- The zero address, `address(0)`. Many `FiatTokenV2` guards forbid it
(e.g. `transfer to the zero address`). -/
def Address.zero : Address := 0

依存

• JPYC.Address