JPYCv2 形式検証

外観

JPYC.setBalance_balances ​

名称・種別 ​

  • 名称: JPYC.setBalance_balances
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:73-74
  • 概要: setBalance 後の balances は当該アドレスだけが書き換わる点更新になる、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ (s : JPYC.State) (a : JPYC.Address) (v : JPYC.U256), Eq (s.setBalance a v).balances (Function.update s.balances a v)

(s.setBalance a v).balances は Function.update s.balances a v に等しい、という等式です。

解説 ​

何を述べているか。 State.setBalance を施した後の balances は、元の balances の a 番地だけを v に置き換えたもの（Function.update）に正確に一致します。

直感。 「残高を更新する関数は、残高マッピングをまさに 1 点更新したものになる」という、定義をほどいただけの等式（rfl）です。

なぜ安全性に効くか。 @[simp] 補題として、送金やミントの証明中で残高更新を自動的に正規形へ書き換えます。フレーム性や供給保存の計算で Function.update の補題（update_of_ne など）を使える形に整えます。

図解 ​

Lean ソースコード ​

lean
@[simp] theorem setBalance_balances (s : State) (a : Address) (v : U256) :
    (s.setBalance a v).balances = Function.update s.balances a v := rfl

依存 ​