JPYC.WF

名称・種別

• 名称: JPYC.WF
• 種別: structure
• モジュール: JpycFormalVerification.State
• ソース: JpycFormalVerification/State.lean:133-148
• 概要: フラグ写像が 0/1 のみ・initializedVersion∈{0,1,2} を保証する健全性不変条件。
• 仕様: 対象外

型シグネチャ

JPYC.State → Prop

State → Prop：状態を受け取り「その状態は整合している」という 命題（Prop） を返します。4 つの条項（3 つのフラグが 0/1 であること、initializedVersion ≤ 2）からなります。

和訳 docstring

well-formedness（整合性）不変条件。

bool を uint256 で持つ符号化が依存している構造的事実を記録する：フラグマップ（blocklisted / allowlisted / authorizationStates）は常に 0 か 1 のみを保持し、initializedVersion ∈ {0,1,2} である。なお「すべての残高が 256 ビットに収まる」は構成上（各フィールドが BitVec）自明に成り立つので、別の条項は不要。後続フェーズのあらゆる状態変更操作は、この WF を保存することを要求される。

解説

何を述べているか。 状態が満たすべき健全性の前提です（primer §3.6）。「フラグは 0 か 1」「初期化バージョンは 0/1/2 のいずれか」という、コードが暗黙に頼っている性質を明文化します。

直感。 もしフラグが 2 のような壊れた値を取れてしまうと、if flag == 1 のような判定の意味が崩れます。WF はそれを禁じます。Prop を返すのは、これが「計算」ではなく「主張（命題）」だからです。

なぜ安全性に効くか。 後続のすべての状態変更関数が WF を保つことを証明済み（*_wf）なので、正規の操作を行っている限り、状態が壊れた値になることはありません。これは権限・フラグ系のすべての判定が意味を持つための土台です。

図解

Lean ソースコード

/-- Well-formedness invariant.

It records the structural facts the boolean-as-`uint256` encoding relies on:
the flag maps only ever hold `0` or `1`, and `initializedVersion ∈ {0,1,2}`.
Note that "every balance fits in 256 bits" holds *by construction* here (every
field is a `BitVec`), so it needs no separate clause. Every state-changing
operation in later phases is required to preserve `WF`. -/
structure WF (s : State) : Prop where
  /-- `blocklisted` is a 0/1 flag. -/
  blocklistedBinary : ∀ a, s.blocklisted a = 0 ∨ s.blocklisted a = 1
  /-- `allowlisted` is a 0/1 flag. -/
  allowlistedBinary : ∀ a, s.allowlisted a = 0 ∨ s.allowlisted a = 1
  /-- `authorizationStates` is a 0/1 flag. -/
  authStateBinary : ∀ a n, s.authorizationStates a n = 0 ∨ s.authorizationStates a n = 1
  /-- `initializedVersion ∈ {0,1,2}`. -/
  initializedVersionValid : s.initializedVersion.toNat ≤ 2

依存

• JPYC.State