JPYCv2 形式検証

外観

JPYC.transferFrom_eq_ok ​

名称・種別 ​

  • 名称: JPYC.transferFrom_eq_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:349-378
  • 概要: 成功した transferFrom が承認ステップ s₁ と _transfer に分解される、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {frm dst : JPYC.Address} {value : JPYC.U256}, Eq (JPYC.transferFrom s ctx frm dst value) (Except.ok s') → Exists fun s₁ => And (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)))))) (Eq (JPYC._transfer s₁ frm dst value) (Except.ok s'))

transferFrom が成功するなら、ある中間状態 s₁ を経由していて、(無限承認なら s₁ = s／有限なら許可額が value 以上で value 減った s₁)、かつ _transfer s₁ frm dst value が成功する、という分解定理です。

和訳 docstring ​

成功した transferFrom は、許可額ステップ s₁（無限承認は据え置き／有限は value 減）を経て _transfer が成功する形に分解される。

解説 ​

何を述べているか。 transferFrom の成功を「許可額ステップ（allowanceStep）で得た中間状態 s₁」と「s₁ からの残高移動 _transfer」の 2 段に分解します。分岐条件も保持し、無限承認（MAX_U256）なら据え置き、有限なら value ≤ 許可額 かつ value 減を明示します。

直感。 ガードを req_bind_eq_ok で 4 枚剥がし、checkAllowlist_bind_eq_ok を吸収、残りを bind_eq_ok で「許可額ステップ」と「送金」に割ります。許可額ステップは allowanceStep を展開して分岐ごとに s₁ を特定します。

なぜ安全性に効くか。 transferFrom のすべての性質（許可額の減少・供給保存・WF・総供給不変）を、この分解を通して _transfer と許可額ステップに帰着させる中心定理です。第三者送金の正しさを、許可と残高の 2 観点に整理します。

図解 ​

Lean ソースコード ​

lean
/-- A successful `transferFrom` factors through an allowance step `s₁`, carrying
the branch condition: an infinite (`type(uint256).max`) approval leaves `s₁ = s`,
otherwise the allowance covered `value` and was debited by it. In both cases a
successful `_transfer` from `frm` follows. -/
theorem transferFrom_eq_ok {s s' : State} {ctx : CallContext} {frm dst : Address}
    {value : U256} (h : transferFrom s ctx frm dst value = .ok s') :
    ∃ s₁ : State,
      ((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))) ∧
      _transfer s₁ frm dst value = .ok s' := by
  unfold transferFrom whenNotPaused notBlocklisted at h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  have h := checkAllowlist_bind_eq_ok h
  obtain ⟨s₁, hstep, htrans⟩ := bind_eq_ok h
  refine ⟨s₁, ?_, htrans⟩
  unfold allowanceStep at hstep
  by_cases hc : s.allowed frm ctx.sender ≠ MAX_U256
  · right
    rw [if_pos hc] at hstep
    obtain ⟨hle, hstep⟩ := req_bind_eq_ok hstep
    obtain ⟨d, hsub, hstep⟩ := bind_eq_ok hstep
    obtain ⟨hd, _⟩ := sub?_eq_ok hsub
    exact ⟨hc, hle, by rw [pure_ok hstep, hd]⟩
  · left
    rw [if_neg hc] at hstep
    exact ⟨not_not.mp hc, pure_ok hstep⟩

依存 ​