JPYC.Address

名称・種別

• 名称: JPYC.Address
• 種別: abbrev
• モジュール: JpycFormalVerification.Address
• ソース: JpycFormalVerification/Address.lean:13-14
• 概要: Solidity の address を表す語型（BitVec 160）。
• 仕様: 対象外

型シグネチャ

Type

Type と表示されるのは、これが値ではなく 型そのもの だからです。Address は BitVec 160（160 ビットのビット列）の別名（abbrev）で、Solidity の address 型に対応します。

和訳 docstring

Solidity の address 型。

解説

何を述べているか。 Ethereum 上のアカウント（外部所有アカウントやコントラクト）を一意に指す 160 ビットのアドレスを表す型です。

直感。 Solidity の address は 20 バイト = 160 ビットです。ここでは不透明（opaque）な型にするのではなく、あえて BitVec 160 の別名にしています。こうすると等価判定（DecidableEq）と有限性（Fintype）が「ただ」で手に入ります。mapping を全域関数として表す方針（primer §3.1）とも噛み合います。

なぜ安全性に効くか。 アドレスが 有限型 であることが、全アカウントの残高総和 Σ balances（SupplyConserved）を「そもそも定義可能」にしている土台です。残高マップ balances : Address → U256 のキー型でもあり、モデルのいたるところで現れます。

図解

Lean ソースコード

/-- A Solidity `address`. -/
abbrev Address : Type := BitVec 160

依存

（なし）