JPYCv2 形式検証

外観

JPYC.State.setAllowlister ​

名称・種別 ​

  • 名称: JPYC.State.setAllowlister
  • 種別: def
  • モジュール: JpycFormalVerification.AccessControl
  • ソース: JpycFormalVerification/AccessControl.lean:54-55
  • 概要: allowlister を a に書き換える純粋な状態更新関数。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → JPYC.State

State と値を 1 つ受け取り、許可リスト管理者（allowlister）（allowlister）だけを差し替えた新しい State を返す純関数です。

和訳 docstring ​

allowlister = a（許可リスト管理者（allowlister）を更新する）。

解説 ​

何を述べているか。 Solidity の代入文 allowlister = a をモデル化した補助関数です。状態 s のうち 許可リスト管理者（allowlister）（allowlister）のフィールドだけを新しい値に置き換え、残りのフィールドはそのまま引き継ぎます（レコード更新 { s with … }）。

直感。 「台帳の 1 項目だけを書き換える」操作です。許可リスト管理者（allowlister）以外の残高・許可額・各種フラグ・ロールには一切触れません。

なぜ安全性に効くか。 状態変更を「ちょうど 1 フィールドだけ」に閉じ込めるのが、安全性証明の基本戦略です。この純関数を通すことで、対応する定理（setAllowlister_* / *_wf / *_conserves）が「他フィールドは不変」「WF と SupplyConserved は保たれる」と機械的に示せます。

図解 ​

Lean ソースコード ​

lean
/-- `allowlister = a`. -/
def State.setAllowlister (s : State) (a : Address) : State := { s with allowlister := a }

依存 ​