JPYCv2 形式検証

外観

JPYC.setAllowance_initializedVersion ​

名称・種別 ​

  • 名称: JPYC.setAllowance_initializedVersion
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:98-99
  • 概要: setAllowance は initializedVersion を変えない、という frame 補題。
  • 仕様: 対象外

型シグネチャ ​

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

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

解説 ​

何を述べているか。 許可額を更新しても、初期化バージョン（initializedVersion）は 変わらない ことを示します。

直感。 State.setAllowance は allowed マッピングの 1 マスだけを書き換える操作なので、他のフィールドには触れません（rfl）。

なぜ安全性に効くか。 @[simp] 補題として、approve 系・transferFrom の許可額消費の証明で「許可額更新は初期化バージョンを保つ」を自動適用します。これにより、承認操作が残高・供給・WF を壊さないことが機械的に示せます。

図解 ​

Lean ソースコード ​

lean
@[simp] theorem setAllowance_initializedVersion (s : State) (o sp : Address) (v : U256) :
    (s.setAllowance o sp v).initializedVersion = s.initializedVersion := rfl

依存 ​