JPYCv2 形式検証

外観

JPYC.mint_eq ​

名称・種別 ​

  • 名称: JPYC.mint_eq
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:378-399
  • 概要: 成功した mint の算術的書き込みと結果状態を順方向に特徴づける補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {dst : JPYC.Address} {amount : JPYC.U256}, Eq (JPYC.mint s ctx dst amount) (Except.ok s') → Exists fun ns => Exists fun nb => Exists fun nma => And (Eq (JPYC.add? s.totalSupply amount) (Except.ok ns)) (And (Eq (JPYC.add? (s.balances dst) amount) (Except.ok nb)) (And (Eq (JPYC.sub? (s.minterAllowed ctx.sender) amount) (Except.ok nma)) (Eq s' (((s.setTotalSupply ns).setBalance dst nb).setMinterAllowed ctx.sender nma))))

mint s ctx dst amount が成功したという仮定から、3 つの checked 演算（総供給・残高・許可量）が成功したことと、結果状態の形を取り出す前向き特徴づけ補題です。

和訳 docstring ​

mint 成功の前向き特徴づけ ― 算術的な書き込みと結果状態。

解説 ​

何を述べているか。 mint が成功したとき、add? totalSupply amount・add? balances[dst] amount・sub? minterAllowed[sender] amount がいずれも成功して値 ns/nb/nma を返し、結果 s' が「総供給を ns、balances[dst] を nb、minterAllowed[sender] を nma に更新した状態」に等しいことを取り出します。

直感。 多重ガード（停止・ミンター・ブロック・許可リスト・正値・上限）を全部剝がし、最後に残る「3 つの算術書き込み」を露出させます。証明は req_bind_eq_ok を繰り返し、bind_eq_ok で add?/sub? の成功を取り出して締めます。

なぜ安全性に効くか。 mint のあらゆる効果・不変条件定理（mint_totalSupply・mint_balance・mint_minterAllowed・mint_frame・mint_conserves・mint_wf）の出発点です。発行という最重要操作の振る舞いを 1 本に凝縮しています。

図解 ​

Lean ソースコード ​

lean
/-- Forward characterization of a successful `mint`: the arithmetic writes and the
resulting state. -/
theorem mint_eq {s s' : State} {ctx : CallContext} {dst : Address} {amount : U256}
    (h : mint s ctx dst amount = .ok s') :
    ∃ ns nb nma,
      add? s.totalSupply amount = .ok ns ∧
      add? (s.balances dst) amount = .ok nb ∧
      sub? (s.minterAllowed ctx.sender) amount = .ok nma ∧
      s' = ((s.setTotalSupply ns).setBalance dst nb).setMinterAllowed ctx.sender nma := by
  unfold mint whenNotPaused onlyMinters notBlocklisted at h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  have h := checkAllowlist_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨ns, hns, h⟩ := bind_eq_ok h
  obtain ⟨nb, hnb, h⟩ := bind_eq_ok h
  obtain ⟨nma, hnma, h⟩ := bind_eq_ok h
  exact ⟨ns, nb, nma, hns, hnb, hnma, pure_ok h⟩

依存 ​