JPYCv2 形式検証

外観

JPYC.State.setAllowance ​

名称・種別 ​

  • 名称: JPYC.State.setAllowance
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:31-34
  • 概要: allowed[owner][spender] を v に書き換える純粋な状態更新関数。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → JPYC.Address → JPYC.U256 → JPYC.State

State・所有者 owner・支払い委任先 spender・値 v を受け取り、allowed[owner][spender] だけを v に差し替えた新しい State を返します。

和訳 docstring ​

allowed[owner][spender] = v（許可額マッピングの 1 マスを v に更新）。

解説 ​

何を述べているか。 Solidity の二重マッピング代入 allowed[owner][spender] = v をモデル化したものです。allowed は「所有者 → （支払い委任先 → 許可額）」という入れ子の全域関数なので、外側を owner で、内側を spender で二重に Function.update します。

直感。 「誰が（owner）、誰に（spender）、いくらまで使ってよいか（v）」という 1 マスだけを書き換えます。他の所有者・他の委任先の許可額には触れません。

なぜ安全性に効くか。 approve 系と transferFrom の allowance 消費はすべてこの関数を通ります。更新箇所が 1 マスに限定されるので、setAllowance_allowed_self で「設定した値がそのまま読み出せる」こと、setAllowance_* 群で「残高・供給・フラグは不変」であることが示せます。

図解 ​

Lean ソースコード ​

lean
/-- `allowed[owner][spender] = v`. -/
def State.setAllowance (s : State) (owner spender : Address) (v : U256) : State :=
  { s with allowed :=
      Function.update s.allowed owner (Function.update (s.allowed owner) spender v) }

依存 ​