JPYC.permit_above_cap_allowlisted

名称・種別

名称: JPYC.permit_above_cap_allowlisted
種別: theorem
モジュール: JpycFormalVerification.SignaturesTheorems
ソース: JpycFormalVerification/SignaturesTheorems.lean:635-639
概要: 上限超の額の permit 成功は owner が許可登録済みであることを含意する。
仕様: 対象

型シグネチャ

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

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

解説

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

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

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

図解

Lean ソースコード

lean

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

JPYC.permit_above_cap_allowlisted ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.permit_above_cap_allowlisted

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存