JPYCv2 形式検証

外観

JPYC.permit_sets_allowance ​

名称・種別 ​

  • 名称: JPYC.permit_sets_allowance
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:200-207
  • 概要: 成功した permit は allowed[owner][spender] を value に設定する、という定理（効果）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {owner spender : JPYC.Address} {value deadline : JPYC.U256} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.permit O s ctx owner spender value deadline v r sig) (Except.ok s') → Eq (s'.allowed owner spender) value

permit の成功は、allowed[owner][spender] を value に設定する、という効果定理です。

和訳 docstring ​

効果。 成功した permit は allowed[owner][spender] = value を設定する。

解説 ​

何を述べているか。 permit が成功すると s'.allowed owner spender = value です。内部 _permit は最後に _approve owner spender value を呼び、それが許可額を value に書き込みます（setAllowance_allowed_self）。

直感。 「署名つき承認の本来の目的＝許可額の設定が、ちゃんと反映される」を確認します。これにより spender は transferFrom で最大 value まで引き出せるようになります。

なぜ安全性に効くか。 permit が「期待どおりの承認」を行うことを保証します。設定値が value ちょうどであること（多すぎず少なすぎず）が、承認の意味を確定させます。

図解 ​

Lean ソースコード ​

lean
/-- **Effect.** A successful `permit` sets `allowed[owner][spender] = value`. -/
theorem permit_sets_allowance {O : SigOracle} {s s' : State} {ctx : CallContext}
    {owner spender : Address} {value deadline : U256} {v : U8} {r sig : Bytes32}
    (h : permit O s ctx owner spender value deadline v r sig = .ok s') :
    s'.allowed owner spender = value := by
  obtain ⟨_, _, nextNonce, _, happ⟩ := _permit_ok (permit_eq_ok h)
  obtain ⟨_, _, rfl⟩ := _approve_ok happ
  exact setAllowance_allowed_self _ owner spender value

依存 ​