JPYC.permit_not_blocklisted

名称・種別

名称: JPYC.permit_not_blocklisted
種別: theorem
モジュール: JpycFormalVerification.SignaturesTheorems
ソース: JpycFormalVerification/SignaturesTheorems.lean:613-617
概要: permit の成功は owner・spender が非ブロックリストであることを含意する。
仕様: 対象

型シグネチャ

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}, Eq (JPYC.permit O s ctx owner spender value deadline v r sig) (Except.ok s') → And (Eq (s.blocklisted owner) 0) (Eq (s.blocklisted spender) 0)

permit の成功は、所有者（owner）・支出者（spender）がいずれもブロックリストに載っていなかったことを含意する、というブロックリスト相互作用の定理です。

解説

何を述べているか。 permit が成功したなら blocklisted owner = 0 ∧ blocklisted spender = 0 です。permit_guards の該当成分を取り出します。

直感。 notBlocklisted ガードの対偶です。「署名操作が通った ⇒ 所有者（owner）・支出者（spender）は誰もブロックされていなかった」。逆に言えば、いずれかがブロック済みなら操作は必ず失敗します。

なぜ安全性に効くか。 ブロックリストの意味 ―― 凍結アカウントは署名を使っても取引に関われない ―― を保証します。署名つき操作がブロックリストの抜け穴にならないことの裏付けです。

図解

Lean ソースコード

lean

theorem permit_not_blocklisted {O : SigOracle} {s s' : State} {ctx : CallContext}
    {owner spender : Address} {value deadline : U256} {v : U8} {r sig : Bytes32}
    (h : permit O s ctx owner spender value deadline v r sig = .ok s') :
    s.blocklisted owner = 0 ∧ s.blocklisted spender = 0 :=
  ⟨(permit_guards h).2.1, (permit_guards h).2.2.1⟩

JPYC.permit_not_blocklisted ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.permit_not_blocklisted

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存