JPYCv2 形式検証

外観

JPYC.State.setMinterAllowed ​

名称・種別 ​

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

型シグネチャ ​

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

State・アドレス a・値 vを受け取り、ミント許可量マッピング（minterAllowed）のうち指定キーの値だけを差し替えた新しい State を返します。

和訳 docstring ​

minterAllowed[a] = v（ミント許可量マッピングマッピングの該当キーを更新する）。

解説 ​

何を述べているか。 Solidity のマッピング代入 minterAllowed[a] = v をモデル化したものです。ミント許可量マッピングは「アドレス → 値」の全域関数で、その指定キーの 1 点だけを Function.update で書き換え、他のキー・他のフィールドはそのまま残します。

直感。 「ミント許可量マッピングという台帳の、特定アドレスの行だけを書き換える」操作です。他のアドレスのエントリには影響しません。

なぜ安全性に効くか。 更新箇所を 1 点に限定することで、setMinterAllowed_self で「設定した値がそのまま読み出せる」こと、関連する *_wf / *_conserves 補題で「他フィールド・WF は不変」であることが証明できます。

図解 ​

Lean ソースコード ​

lean
/-- `minterAllowed[a] = v`. -/
def State.setMinterAllowed (s : State) (a : Address) (v : U256) : State :=
  { s with minterAllowed := Function.update s.minterAllowed a v }

依存 ​