JPYC.receiveWithAuthorization_not_blocklisted

名称・種別

名称: JPYC.receiveWithAuthorization_not_blocklisted
種別: theorem
モジュール: JpycFormalVerification.SignaturesTheorems
ソース: JpycFormalVerification/SignaturesTheorems.lean:626-631
概要: receiveWithAuthorization の成功は関係者が非ブロックリストであることを含意する。
仕様: 対象

型シグネチャ

lean

∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {frm dst : JPYC.Address} {value validAfter validBefore : JPYC.U256} {nonce : JPYC.Bytes32} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.ok s') → And (Eq (s.blocklisted frm) 0) (Eq (s.blocklisted dst) 0)

receiveWithAuthorization の成功は、送金元（from）・受取人（to）がいずれもブロックリストに載っていなかったことを含意する、というブロックリスト相互作用の定理です。

解説

何を述べているか。 receiveWithAuthorization が成功したなら blocklisted frm = 0 ∧ blocklisted dst = 0 です。receiveWithAuthorization_guards の該当成分を取り出します。

直感。 notBlocklisted ガードの対偶です。「署名操作が通った ⇒ 送金元（from）・受取人（to）は誰もブロックされていなかった」。逆に言えば、いずれかがブロック済みなら操作は必ず失敗します。

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

図解

Lean ソースコード

lean

theorem receiveWithAuthorization_not_blocklisted {O : SigOracle} {s s' : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32}
    (h : receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s') :
    s.blocklisted frm = 0 ∧ s.blocklisted dst = 0 :=
  ⟨(receiveWithAuthorization_guards h).2.1, (receiveWithAuthorization_guards h).2.2.1⟩

JPYC.receiveWithAuthorization_not_blocklisted ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.receiveWithAuthorization_not_blocklisted

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存