JPYC.setBalance_permitNonces

名称・種別

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

型シグネチャ

∀ (s : JPYC.State) (a : JPYC.Address) (v : JPYC.U256), Eq (s.setBalance a v).permitNonces s.permitNonces

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

解説

何を述べているか。 (s.setBalance a v).permitNonces = s.permitNonces を示します。残高（balances）の更新は nonce 台帳と別フィールドなので、定義から rfl で従います。

直感。 「残高を書き換えても permit の連番台帳はそのまま」を述べています。

なぜ安全性に効くか。 EIP-3009 の送金（内部 _transfer で setBalance を使う）が permit nonce を変えないことを保証し、nonce と authorization の状態管理が互いに干渉しないという独立性を支えます。

図解

Lean ソースコード

@[simp] theorem setBalance_permitNonces (s : State) (a : Address) (v : U256) :
    (s.setBalance a v).permitNonces = s.permitNonces := rfl

依存

• JPYC.Address
• JPYC.State
• JPYC.State.setBalance
• JPYC.U256