JPYCv2 形式検証

外観

JPYC.State.empty ​

名称・種別 ​

  • 名称: JPYC.State.empty
  • 種別: def
  • モジュール: JpycFormalVerification.State
  • ソース: JpycFormalVerification/State.lean:103-131
  • 概要: 全ゼロ・初期化前の状態。各不変条件が充足可能であることの正規の証人。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State

型 State の 定数 です。すべてのフィールドが 0 / 空 / 未割当になった初期状態を表します。

和訳 docstring ​

全ゼロ / 初期化前の状態：すべての残高と許可額は 0、ロールは未割当、停止していない、initializedVersion = 0。下記の不変条件が充足可能であることの正規の証人として働く。

解説 ​

何を述べているか。 すべてが「まっさら」な状態で、デプロイ直後・初期化前を表します。

直感。 全残高 0、全ロール未割当（Address.zero）、paused = false、initializedVersion = 0 です。

なぜ安全性に効くか。 不変条件 WF や SupplyConserved が「空虚に真」なのではなく、実際に成立する状態が存在する ことを示す証人です（wf_empty / supplyConserved_empty）。証人がないと「不変条件を保つ」という定理が、充足不能な前提のうえの無意味な主張になりかねません。テストの初期状態としても使われます。

図解 ​

Lean ソースコード ​

lean
/-- The all-zero / pre-initialization state: every balance and allowance is `0`,
no roles assigned, not paused, `initializedVersion = 0`. Acts as a canonical
witness that the invariants below are satisfiable. -/
def State.empty : State where
  name := ""
  symbol := ""
  currency := ""
  decimals := 0
  totalSupply := 0
  initializedVersion := 0
  balances := fun _ => 0
  allowed := fun _ _ => 0
  minters := fun _ => false
  minterAllowed := fun _ => 0
  allowlisted := fun _ => 0
  owner := Address.zero
  pauser := Address.zero
  blocklister := Address.zero
  rescuer := Address.zero
  minterAdmin := Address.zero
  allowlister := Address.zero
  paused := false
  blocklisted := fun _ => 0
  domainSeparator := 0
  chainId := 0
  domainName := ""
  version := ""
  permitNonces := fun _ => 0
  authorizationStates := fun _ _ => 0

依存 ​