JPYC.instFintypeBitVec

名称・種別

• 名称: JPYC.instFintypeBitVec
• 種別: instance
• モジュール: JpycFormalVerification.State
• ソース: JpycFormalVerification/State.lean:26-36
• 概要: 任意の BitVec が有限型であることを与えるインスタンス。総供給=Σ残高 の表現に必要。
• 仕様: 対象

型シグネチャ

(w : Nat) → Fintype (BitVec w)

(w : Nat) → Fintype (BitVec w)：任意のビット幅 w について、BitVec w が 有限型（Fintype） であることを与えるインスタンスです。

和訳 docstring

すべての BitVec w は有限。この Mathlib 版では提供されていないが、Address（= BitVec 160）を Fintype にし、全体不変条件 totalSupply = Σ balances を表現可能にするために必要。将来 Mathlib が Fintype (BitVec w) インスタンスを追加した場合にそちらが優先され、インスタンスの diamond が生じないよう low 優先度を付けている。

解説

何を述べているか。 「BitVec w には 2^w 個しか値がない」、つまり 有限である ことを Lean に教えるインスタンスです。Fin (2^w) との同型（Equiv）を介して構成しています。

直感。 型クラスのインスタンスは、必要なときに自動的に使われる「裏方」です。普段は意識しませんが、これがないと次の総和が書けません。

なぜ安全性に効くか。 無限にありうるアドレス全体にわたる残高の総和 ∑ a : Address, balances a を 有限和 として定義できるのは、Address が有限型だからです。これが State.totalBalances ／ SupplyConserved（供給保存）を表現するための前提になっています。

なお、このインスタンスには (priority := low) を付けています。現状 Fintype (BitVec w) を与える候補は他に無いので解決には影響しませんが、将来 Mathlib が同名のインスタンスを追加しても、そちらが優先されてインスタンスの衝突（diamond）が起きないようにするための予防的な配慮です。

図解

Lean ソースコード

/-- Every `BitVec w` is finite. Not provided by this Mathlib version, but needed
so that `Address` (= `BitVec 160`) is a `Fintype` and the global
`totalSupply = Σ balances` invariant is expressible. Given a `low` priority so
that a future Mathlib `Fintype (BitVec w)` instance, if one is ever added, is
preferred and no instance diamond arises. -/
instance (priority := low) instFintypeBitVec (w : Nat) : Fintype (BitVec w) :=
  Fintype.ofEquiv (Fin (2 ^ w))
    { toFun := BitVec.ofFin
      invFun := BitVec.toFin
      left_inv := fun _ => rfl
      right_inv := fun _ => rfl }

依存

（なし）