JPYCv2 形式検証

外観

JPYC.configureMinter_ok ​

名称・種別 ​

  • 名称: JPYC.configureMinter_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:304-311
  • 概要: 成功した configureMinter を順方向に特徴づける補助補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {minter : JPYC.Address} {amount : JPYC.U256}, Eq (JPYC.configureMinter s ctx minter amount) (Except.ok s') → And (Eq s.paused Bool.false) (And (Eq ctx.sender s.minterAdmin) (Eq s' ((s.setMinter minter Bool.true).setMinterAllowed minter amount)))

configureMinter s ctx minter amount が成功したという仮定から、その成立条件（停止中でないこと・minterAdmin であること）と結果状態の形を取り出す前向き特徴づけ補題です。

解説 ​

何を述べているか。 configureMinter が Except.ok s' で成功したとき、停止中でないこと・minterAdmin であることが成り立ち、結果 s' が(s.setMinter minter true).setMinterAllowed minter amountに等しいことを取り出します。証明は do ブロック先頭から req_bind_eq_ok でガードを 1 枚ずつ剝がし、最後に pure_ok で pure の成功値を取り出します。

直感。 「成功した」という結果だけから、「どの条件が満たされていたか」「状態がどう変わったか」を逆算する分解です。後続の認可・効果・不変条件の定理は、すべてこの 1 本から枝分かれします。

なぜ安全性に効くか。 これは各関数の 仕様の核 です。configureMinter_ok を一度証明しておけば、*_auth（認可）・*_sets（効果）・*_wf / *_conserves（不変条件）が短く導けます。安全性主張を 1 か所に集約する設計です。

図解 ​

Lean ソースコード ​

lean
theorem configureMinter_ok {s s' : State} {ctx : CallContext} {minter : Address} {amount : U256}
    (h : configureMinter s ctx minter amount = .ok s') :
    s.paused = false ∧ ctx.sender = s.minterAdmin ∧
      s' = (s.setMinter minter true).setMinterAllowed minter amount := by
  unfold configureMinter whenNotPaused onlyMinterAdmin at h
  obtain ⟨hp, h⟩ := req_bind_eq_ok h
  obtain ⟨ha, h⟩ := req_bind_eq_ok h
  exact ⟨hp, ha, pure_ok h⟩

依存 ​