JPYCv2 形式検証

外観

JPYC.State.setBalance ​

名称・種別 ​

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

型シグネチャ ​

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

State とアドレス a・値 v を受け取り、balances のうち a 番地だけを v に差し替えた新しい State を返す純関数です。

和訳 docstring ​

balances[a] = v（残高マッピングの a 番地を v に更新）。

解説 ​

何を述べているか。 Solidity の代入文 balances[a] = v をモデル化した補助関数です。状態 s の balances（アドレス→残高の全域関数）のうち、キー a の値だけを v に置き換え、それ以外のフィールドは丸ごと引き継ぎます（Function.update）。

直感。 「台帳の 1 行だけを書き換える」操作です。許可額・各種フラグ・ロールといった残高以外の情報は一切変わりません。

なぜ安全性に効くか。 送金・ミント・バーンなど、残高を動かすあらゆる処理はこの 1 点更新を経由します。「ちょうど 1 か所しか変わらない」ことが構造として保証されるため、setBalance_balances 以下の setBalance_* 補題で「他フィールドは不変」と機械的に示せます。これが フレーム性 や 供給保存 の証明の土台です。

図解 ​

Lean ソースコード ​

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

依存 ​