JPYCv2 形式検証

外観

JPYC.setAllowance_allowed_self ​

名称・種別 ​

  • 名称: JPYC.setAllowance_allowed_self
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:100-102
  • 概要: setAllowance 後、当該 (owner,spender) の allowed が設定値になる、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ (s : JPYC.State) (o sp : JPYC.Address) (v : JPYC.U256), Eq ((s.setAllowance o sp v).allowed o sp) v

(s.setAllowance o sp v).allowed o sp は v に等しい、という等式です。

解説 ​

何を述べているか。 許可額を v に設定した直後に、同じ鍵 (o, sp) で読み出すと、ちゃんと v が返ってくることを示します（Function.update_self）。

直感。 「書いた値はそのまま読める」という当たり前を、二重マッピングについて確認しています。証明は setAllowance を展開して Function.update_self を使うだけです。

なぜ安全性に効くか。 approve_allowance（承認後の許可額が value）と transferFrom_allowance（消費後の許可額）を結論づける核心の補題です。「設定した／減らした値が、実際にその通り反映される」ことを保証します。

図解 ​

Lean ソースコード ​

lean
@[simp] theorem setAllowance_allowed_self (s : State) (o sp : Address) (v : U256) :
    (s.setAllowance o sp v).allowed o sp = v := by
  simp [State.setAllowance, Function.update_self]

依存 ​