JPYCv2 形式検証

外観

JPYC.initializeV1_blocklists_self ​

名称・種別 ​

  • 名称: JPYC.initializeV1_blocklists_self
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:172-182
  • 概要: initializeV1 は自身のアドレスをブロックリスト登録する（blocklisted[address(this)]=1）（効果）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {self : JPYC.Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : JPYC.U8} {newMinterAdmin newPauser newBlocklister newRescuer newOwner : JPYC.Address}, Eq (JPYC.initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner) (Except.ok s') → Eq (s'.blocklisted self) 1

initializeV1 の成功は、コントラクト自身のアドレスをブロックリストに載せる（blocklisted[address(this)] = 1）、という効果定理です。

和訳 docstring ​

効果。 initializeV1 はコントラクト自身のアドレスをブロックリストに載せる（blocklisted[address(this)] = 1）。

解説 ​

何を述べているか。 initializeV1 が成功した結果状態では s'.blocklisted self = 1 です。initializeResult の blocklisted := Function.update s.blocklisted self 1 という書き込みから、同じキーでの読み出し（Function.update_self）で従います。

直感。 「コントラクト自身（プロキシのアドレス）を、最初からブロックリストに入れておく」措置です。これにより、誤ってコントラクト自身宛てに送られたトークンが（送金・受領を通じて）動かされる事故を防ぎます。

なぜ安全性に効くか。 コントラクトアドレスへの誤送金を、設計レベルで凍結します。self はブロック済みなので、notBlocklisted ガードを持つ送金・受領・発行に self が関与すると revert します。資金がコントラクトに吸い込まれて回収不能になるリスクを軽減する措置です。

図解 ​

Lean ソースコード ​

lean
/-- **Effect.** `initializeV1` blocklists the contract's own address
(`blocklisted[address(this)] = 1`). -/
theorem initializeV1_blocklists_self {O : SigOracle} {s s' : State} {ctx : CallContext}
    {self : Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : U8}
    {newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address}
    (h : initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
      newMinterAdmin newPauser newBlocklister newRescuer newOwner = .ok s') :
    s'.blocklisted self = 1 := by
  obtain ⟨_, _, _, _, _, _, rfl⟩ := initializeV1_ok h
  show (Function.update s.blocklisted self 1) self = 1
  rw [Function.update_self]

依存 ​