JPYC.unpause_ok

名称・種別

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

型シグネチャ

∀ {s s' : JPYC.State} {ctx : JPYC.CallContext}, Eq (JPYC.unpause s ctx) (Except.ok s') → And (Eq ctx.sender s.pauser) (Eq s' (s.setPaused Bool.false))

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

解説

何を述べているか。 unpause が Except.ok s' で成功したとき、pauser であることが成り立ち、結果 s' がs.setPaused falseに等しいことを取り出します。証明は do ブロック先頭から req_bind_eq_ok でガードを 1 枚ずつ剝がし、最後に pure_ok で pure の成功値を取り出します。

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

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

図解

Lean ソースコード

theorem unpause_ok {s s' : State} {ctx : CallContext} (h : unpause s ctx = .ok s') :
    ctx.sender = s.pauser ∧ s' = s.setPaused false := by
  unfold unpause onlyPauser at h
  obtain ⟨h1, h⟩ := req_bind_eq_ok h
  exact ⟨h1, pure_ok h⟩

依存

• JPYC.Address
• JPYC.CallContext
• JPYC.Error
• JPYC.State
• JPYC.State.setPaused
• JPYC.req_bind_eq_ok
• JPYC.unpause