JPYCv2 形式検証

外観

JPYC.sum_double_update_nat ​

名称・種別 ​

  • 名称: JPYC.sum_double_update_nat
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:234-253
  • 概要: 二点を書き換えても対の合計が不変なら、有限和の総計も不変である、という補題。
  • 仕様: 対象外

型シグネチャ ​

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

有限なアドレス空間上で、関数 F の 2 点 i, j（相異なる）を x, y に書き換えたとき、もし x + y = F i + F j ならば総和は変わらない、という補題です。

和訳 docstring ​

相異なる 2 点を、合計を保ったまま書き換えても、有限和は変わらない。

解説 ​

何を述べているか。 全アドレスにわたる総和 ∑ a, F a について、相異なる 2 点だけを書き換えても、その 2 点の合計が保たれていれば（x + y = F i + F j）、総和全体は不変だと示します。

直感。 「A から B へお金を移しても、A と B の合計が同じなら全体の合計は変わらない」という、会計の基本そのものです。証明は Finset.sum_update_of_mem で 2 点を総和から括り出し、残りは omega で潰します。

なぜ安全性に効くか。 これが SupplyConserved の数学的な心臓です。送金は送り手と受け手の残高だけを、合計を保ちながら動かすので、この補題により総供給（= 全残高の和）が不変だと結論できます。お金が湧かず消えないことの根拠です。

図解 ​

Lean ソースコード ​

lean
/-- Sum (over the finite address space) of a function with two distinct points
reset: if the new pair-total equals the old pair-total, the grand total is
unchanged. -/
theorem sum_double_update_nat {F : Address → ℕ} {i j : Address} {x y : ℕ}
    (hij : i ≠ j) (hxy : x + y = F i + F j) :
    ∑ a, Function.update (Function.update F i x) j y a = ∑ a, F a := by
  have hi : i ∈ (Finset.univ : Finset Address) \ {j} := by simp [hij]
  have key : ∀ (p q : ℕ),
      ∑ a, Function.update (Function.update F i p) j q a
        = q + (p + ∑ a ∈ ((Finset.univ : Finset Address) \ {j}) \ {i}, F a) := by
    intro p q
    rw [Finset.sum_update_of_mem (Finset.mem_univ j), Finset.sum_update_of_mem hi]
  have hrhs : ∑ a, F a
      = F j + (F i + ∑ a ∈ ((Finset.univ : Finset Address) \ {j}) \ {i}, F a) := by
    rw [← key (F i) (F j)]
    have hself : Function.update (Function.update F i (F i)) j (F j) = F := by
      rw [Function.update_eq_self, Function.update_eq_self]
    rw [hself]
  rw [key x y, hrhs]
  omega

依存 ​