JPYCv2 形式検証

外観

JPYC.State.setAllowlisted ​

名称・種別 ​

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

型シグネチャ ​

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

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

和訳 docstring ​

allowlisted[a] = v（許可リスト・フラグ・マッピングマッピングの該当キーを更新する）。

解説 ​

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

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

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

図解 ​

Lean ソースコード ​

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

依存 ​