JPYC.permit_wf

名称・種別

名称: JPYC.permit_wf
種別: theorem
モジュール: JpycFormalVerification.SignaturesTheorems
ソース: JpycFormalVerification/SignaturesTheorems.lean:218-224
概要: permit は健全性不変条件 WF を保つ、という定理。
仕様: 対象

型シグネチャ

lean

∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {owner spender : JPYC.Address} {value deadline : JPYC.U256} {v : JPYC.U8} {r sig : JPYC.Bytes32}, JPYC.WF s → Eq (JPYC.permit O s ctx owner spender value deadline v r sig) (Except.ok s') → JPYC.WF s'

permit が成功するなら、結果状態も WF を満たす、という不変条件保存の定理です。

和訳 docstring

permit の WF 保存。

解説

何を述べているか。 事前状態 s が WF を満たし、permit が成功して s' になったとき、s' もまた WF を満たします。

直感。 permit が触るのは nonce（setPermitNonce）と許可額（_approve）だけで、フラグ（ブロック・許可リスト・authorization）にも initializedVersion にも触れません（WF.of_flags_eq）。だから 0/1 性も版数の範囲も保たれます。

なぜ安全性に効くか。 すべての操作が WF を保つので、「正規の操作を続ける限りフラグが壊れた値にならない」が帰納的に保証されます。フラグに依存する判定ロジック全体の前提が、操作後も成り立ち続けます。

図解

Lean ソースコード

lean

/-- **WF preservation** for `permit`. -/
theorem permit_wf {O : SigOracle} {s s' : State} {ctx : CallContext} {owner spender : Address}
    {value deadline : U256} {v : U8} {r sig : Bytes32}
    (hwf : WF s) (h : permit O s ctx owner spender value deadline v r sig = .ok s') : WF s' := by
  obtain ⟨_, _, nextNonce, _, happ⟩ := _permit_ok (permit_eq_ok h)
  have hwf' : WF (s.setPermitNonce owner nextNonce) := WF.of_flags_eq hwf rfl rfl rfl rfl
  exact _approve_wf hwf' happ

JPYC.permit_wf ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.permit_wf

名称・種別

型シグネチャ

和訳 docstring

解説

図解

Lean ソースコード

依存