JPYCv2 形式検証

外観

JPYC.approve_allowance ​

名称・種別 ​

  • 名称: JPYC.approve_allowance
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:484-490
  • 概要: 成功した approve は allowed[msg.sender][spender] を value に設定する、という定理。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {value : JPYC.U256}, Eq (JPYC.approve s ctx spender value) (Except.ok s') → Eq (s'.allowed ctx.sender spender) value

approve が成功したとき、結果の許可額 s'.allowed ctx.sender spender はちょうど value になる、という定理です。

和訳 docstring ​

承認は許可額を設定する ― 成功した approve は allowed[msg.sender][spender] を value にする。

解説 ​

何を述べているか。 承認が成功すれば、allowed[msg.sender][spender] が指定どおり value に 設定 されます（加算ではなく上書き）。

直感。 approve_eq_ok で _approve に還元すると、本体は State.setAllowance で許可額を書き込むだけ。書いた値がそのまま読める setAllowance_allowed_self で value が確定します。

なぜ安全性に効くか。 「承認したら、まさにその額が許可枠になる」という ERC20 の契約を保証します。意図した額と異なる枠が設定される、といった齟齬が無いことの証明です。

図解 ​

Lean ソースコード ​

lean
/-- **Approve sets the allowance.** A successful `approve` makes
`allowed[msg.sender][spender]` equal to `value`. -/
theorem approve_allowance {s s' : State} {ctx : CallContext} {spender : Address} {value : U256}
    (h : approve s ctx spender value = .ok s') :
    s'.allowed ctx.sender spender = value := by
  obtain ⟨_, _, rfl⟩ := _approve_ok (approve_eq_ok h)
  exact setAllowance_allowed_self s ctx.sender spender value

依存 ​