JPYC.toNat_double_update

名称・種別

• 名称: JPYC.toNat_double_update
• 種別: theorem
• モジュール: JpycFormalVerification.ERC20Theorems
• ソース: JpycFormalVerification/ERC20Theorems.lean:227-232
• 概要: 二点同時更新を toNat で押し通すための補題。
• 仕様: 対象外

型シグネチャ

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

2 点更新した BitVec 値関数に toNat（自然数化）を施した値は、各点の値を先に toNat してから 2 点更新したものに等しい、という等式です。

和訳 docstring

toNat を 2 点更新の内側へ押し込む。

解説

何を述べているか。 Function.update (Function.update f i x) j y a を toNat で自然数に落とす操作と、先に各点を toNat してから同じ 2 点更新を行う操作が一致することを示します。

直感。 「更新してから数に変換」しても「変換してから更新」しても同じ、という素直な交換則です。a が i か j か、それ以外かで場合分けすればすべて rfl。

なぜ安全性に効くか。 大域供給保存 _transfer_totalBalances の計算で、BitVec の世界の残高更新を ℕ（自然数）の世界の総和計算へ橋渡しします。BitVec のままでは扱いにくい「総和」を、自然数の足し算として omega で処理できるようにします。

図解

Lean ソースコード

/-- Pushing `toNat` through a double point-update. -/
theorem toNat_double_update (f : Address → U256) (i j : Address) (x y : U256) (a : Address) :
    (Function.update (Function.update f i x) j y a).toNat
      = Function.update (Function.update (fun b => (f b).toNat) i x.toNat) j y.toNat a := by
  simp only [Function.update_apply]
  split_ifs <;> rfl

依存

• JPYC.Address
• JPYC.U256