JPYC.sum_update_split

名称・種別

• 名称: JPYC.sum_update_split
• 種別: theorem
• モジュール: JpycFormalVerification.AccessControlTheorems
• ソース: JpycFormalVerification/AccessControlTheorems.lean:123-131
• 概要: 一点更新前後の総和を omega 向けに等式化した補題。
• 仕様: 対象

型シグネチャ

∀ (F : JPYC.Address → Nat) (i : JPYC.Address) (x : Nat), Eq (instHAdd.hAdd (Finset.univ.sum fun a => Function.update F i x a) (F i)) (instHAdd.hAdd x (Finset.univ.sum fun a => F a))

ℕ 値関数 F の 1 点更新について、「更新後の総和 + 旧値 = 新値 + 旧総和」という釣り合いの等式です。

和訳 docstring

ℕ 値関数の 1 点更新を omega で扱える形にしたもの ― 更新後の総和に旧値を足すと、新値に旧総和を足したものに等しい。

解説

何を述べているか。 (∑ a, update F i x a) + F i = x + ∑ a, F a を示します。位置 i の値を x に書き換えると、総和は「旧値 F i が消えて新値 x が入る」分だけ変化する、という当たり前を omega で扱える形に整えたものです。

直感。 全アドレスにわたる合計のうち、変わるのは i の 1 項だけ。だから「新総和 − 旧総和 = x − F i」。両辺に旧値・旧総和を移項して、引き算を避けた等式にしてあります（自然数の引き算は扱いにくいため）。

なぜ安全性に効くか。 ミント・バーンの供給保存の 本当に算術的な核心 です。Mathlib の Finset.sum_update_of_mem を 2 回使い、omega で締めます。これが totalBalances_setBalance に持ち上がり、mint/burn で「総供給の増減 = 残高総和の増減」を厳密に示します。

図解

Lean ソースコード

/-- A single point-update of a `ℕ`-valued function, in an `omega`-friendly form:
the new grand total plus the old value at `i` equals the new value plus the old
grand total. -/
theorem sum_update_split (F : Address → ℕ) (i : Address) (x : ℕ) :
    (∑ a, Function.update F i x a) + F i = x + ∑ a, F a := by
  have h1 := Finset.sum_update_of_mem (Finset.mem_univ i) F x
  have h2 := Finset.sum_update_of_mem (Finset.mem_univ i) F (F i)
  rw [Function.update_eq_self] at h2
  omega

依存

• JPYC.Address
• JPYC.instFintypeBitVec