JPYCv2 形式検証

外観

JPYC.setAllowance_permitNonces ​

名称・種別 ​

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

型シグネチャ ​

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

許可額の設定 setAllowance は permit nonce マッピングに触れない、という @[simp] 等式です。

解説 ​

何を述べているか。 (s.setAllowance o sp v).permitNonces = s.permitNonces を示します。許可額（allowed）の更新は nonce 台帳（permitNonces）と別フィールドなので、定義から rfl で従います。

直感。 「承認額を書き換えても、permit の連番台帳はそのまま」という当たり前を機械が使える形にしています。

なぜ安全性に効くか。 permit は内部で nonce を進めた後に _approve（= setAllowance）で許可額を設定します。この補題があるので「_approve の後でも nonce は進めた値のまま」と言え、permit_nonce_increments / permit_nonce_frame が成立します。

図解 ​

Lean ソースコード ​

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

依存 ​