JPYCv2 形式検証

外観

JPYC.transferFrom_step_balances ​

名称・種別 ​

  • 名称: JPYC.transferFrom_step_balances
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:386-396
  • 概要: 承認ステップは残高も totalSupply も触らないので s₁ は s と同じ供給事実を満たす、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s s₁ : JPYC.State} {ctx : JPYC.CallContext} {frm : JPYC.Address} {value : JPYC.U256}, Or (And (Eq (s.allowed frm ctx.sender) JPYC.MAX_U256) (Eq s₁ s)) (And (Ne (s.allowed frm ctx.sender) JPYC.MAX_U256) (And (instLEBitVec.le value (s.allowed frm ctx.sender)) (Eq s₁ (s.setAllowance frm ctx.sender (instHSub.hSub (s.allowed frm ctx.sender) value))))) → And (Eq s₁.balances s.balances) (And (Eq s₁.totalSupply s.totalSupply) (JPYC.WF s → JPYC.WF s₁))

許可額ステップの分岐（無限承認で s₁ = s／有限で許可額を減らした s₁）のもとで、s₁ は残高・総供給が s と同じで、WF s ならば WF s₁ も成り立つ、という補題です。

解説 ​

何を述べているか。 allowanceStep で得た中間状態 s₁ は、残高（balances）・総供給（totalSupply）が元の s と同一で、WF も引き継ぐことを示します。

直感。 許可額ステップが触るのは allowed だけ。残高にも供給にもフラグにも触れないので、これらは s と完全に一致します（setAllowance_balances など、または据え置きなら自明）。WF 保存は WF.of_flags_eq によります。

なぜ安全性に効くか。 「許可額の操作は残高勘定に影響しない」を確立し、transferFrom の供給保存・WF・総供給の証明を、許可額ステップを飛ばして _transfer の対応補題へ橋渡しします。許可と残高の独立性が、証明をモジュール化します。

図解 ​

Lean ソースコード ​

lean
/-- The allowance step touches neither balances nor `totalSupply`, so the step
state `s₁` satisfies the same supply/well-formedness facts as `s`. -/
theorem transferFrom_step_balances {s s₁ : State} {ctx : CallContext} {frm : Address}
    {value : U256}
    (hstep : (s.allowed frm ctx.sender = MAX_U256 ∧ s₁ = s) ∨
       (s.allowed frm ctx.sender ≠ MAX_U256 ∧ value ≤ s.allowed frm ctx.sender ∧
        s₁ = s.setAllowance frm ctx.sender (s.allowed frm ctx.sender - value))) :
    s₁.balances = s.balances ∧ s₁.totalSupply = s.totalSupply ∧ (WF s → WF s₁) := by
  rcases hstep with ⟨_, rfl⟩ | ⟨_, _, rfl⟩
  · exact ⟨rfl, rfl, id⟩
  · exact ⟨rfl, rfl, fun hwf => WF.of_flags_eq hwf rfl rfl rfl rfl⟩

依存 ​