JPYCv2 形式検証

外観

JPYC.toNat_single_update ​

名称・種別 ​

  • 名称: JPYC.toNat_single_update
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:117-121
  • 概要: 一点更新を toNat で押し通すための補題（toNat_double_update の単点版）。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ (f : JPYC.Address → JPYC.U256) (i : JPYC.Address) (x : JPYC.U256) (a : JPYC.Address), Eq (BitVec.toNat (Function.update f i x a)) (Function.update (fun b => BitVec.toNat (f b)) i (BitVec.toNat x) a)

残高関数 f の 1 点更新を取ってから toNat（自然数化）したものは、先に各値を toNat してから 1 点更新したものに等しい、という補題です。

和訳 docstring ​

1 点更新を toNat で押し通す補題（toNat_double_update の 1 点版）。

解説 ​

何を述べているか。 (Function.update f i x a).toNat = Function.update (fun b => (f b).toNat) i x.toNat a を示します。「1 点だけ書き換える」操作と「U256 を ℕ に変換する」操作は順番を入れ替えてよい、ということです。

直感。 更新したキー i では新値 x を toNat、それ以外では元の値を toNat ―― どちらの順序でも結果は同じ。証明は i と一致するか否かで場合分け（split）し、両枝とも rfl。

なぜ安全性に効くか。 残高の総和 totalBalances は ℕ 上で計算します（U256 のままだと足し算であふれてしまう）。この補題が「BitVec の世界」と「ℕ の世界」を橋渡しし、totalBalances_setBalance を経て mint_conserves / burn_conserves の供給保存へつながります。

図解 ​

Lean ソースコード ​

lean
/-- Pushing `toNat` through a single point-update (cf. `toNat_double_update`). -/
theorem toNat_single_update (f : Address → U256) (i : Address) (x : U256) (a : Address) :
    (Function.update f i x a).toNat
      = Function.update (fun b => (f b).toNat) i x.toNat a := by
  simp only [Function.update_apply]; split <;> rfl

依存 ​