JPYC.receiveWithAuthorization_above_cap_allowlisted

名称・種別

名称: JPYC.receiveWithAuthorization_above_cap_allowlisted
種別: theorem
モジュール: JpycFormalVerification.SignaturesTheorems
ソース: JpycFormalVerification/SignaturesTheorems.lean:648-653
概要: 上限超の receiveWithAuthorization 成功は payer(from) が許可登録済みであることを含意する。
仕様: 対象

型シグネチャ

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') → GT.gt value JPYC.allowlistLimitAmount → Eq (s.allowlisted frm) 1

receiveWithAuthorization で allowlistLimitAmount（上限額）を超える額が成功したなら、送金元（from）は許可リスト登録済み（allowlisted frm = 1）だった、という許可リスト・キャップの定理です。

解説

何を述べているか。 receiveWithAuthorization が成功し、かつ金額 value が上限 allowlistLimitAmount を超えるなら、allowlisted frm = 1、すなわち送金元（from）が許可リストに載っていたことが導けます。receiveWithAuthorization_guards の条件付き含意に「上限超」を当てて得ます（おおもとは checkAllowlist_bind_cap）。

直感。 checkAllowlist ガードの対偶です。「署名で大口（10 万トークン超）を動かせた ⇒ その人は登録済みだった」。未登録なら上限超の署名操作は必ず失敗します。

なぜ安全性に効くか。 JPYC 固有の 送金上限つき許可リスト を、署名つき操作にも一貫して適用する保証です。署名経由でも、大口の資金移動は事前に審査・登録されたアカウントだけに限定されます。

図解

Lean ソースコード

lean

theorem receiveWithAuthorization_above_cap_allowlisted {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')
    (hcap : value > allowlistLimitAmount) : s.allowlisted frm = 1 :=
  (receiveWithAuthorization_guards h).2.2.2 hcap

JPYC.receiveWithAuthorization_above_cap_allowlisted ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.receiveWithAuthorization_above_cap_allowlisted

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存