JPYC.State.setMinter

名称・種別

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

型シグネチャ

JPYC.State → JPYC.Address → Bool → JPYC.State

State・アドレス a・真偽値 bを受け取り、ミンター・フラグ・マッピング（minters）のうち指定キーの値だけを差し替えた新しい State を返します。

和訳 docstring

minters[a] = b（ミンター・フラグ・マッピングマッピングの該当キーを更新する）。

解説

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

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

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

図解

Lean ソースコード

/-- `minters[a] = b`. -/
def State.setMinter (s : State) (a : Address) (b : Bool) : State :=
  { s with minters := Function.update s.minters a b }

依存

• JPYC.Address
• JPYC.State