JPYC.updatePauser_ok
名称・種別
- 名称:
JPYC.updatePauser_ok - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:218-224 - 概要: 成功した updatePauser を順方向に特徴づける補助補題。
- 仕様: 対象外
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {newPauser : JPYC.Address}, Eq (JPYC.updatePauser s ctx newPauser) (Except.ok s') → And (Eq s.owner ctx.sender) (And (Ne newPauser JPYC.Address.zero) (Eq s' (s.setPauser newPauser)))updatePauser s ctx newPauser が成功したという仮定から、その成立条件（オーナーであること・newPauser ≠ 0）と結果状態の形を取り出す前向き特徴づけ補題です。
解説
何を述べているか。 updatePauser が Except.ok s' で成功したとき、オーナーであること・newPauser ≠ 0が成り立ち、結果 s' がs.setPauser newPauserに等しいことを取り出します。証明は do ブロック先頭から req_bind_eq_ok でガードを 1 枚ずつ剝がし、最後に pure_ok で pure の成功値を取り出します。
直感。 「成功した」という結果だけから、「どの条件が満たされていたか」「状態がどう変わったか」を逆算する分解です。後続の認可・効果・不変条件の定理は、すべてこの 1 本から枝分かれします。
なぜ安全性に効くか。 これは各関数の 仕様の核 です。updatePauser_ok を一度証明しておけば、*_auth（認可）・*_sets（効果）・*_wf / *_conserves（不変条件）が短く導けます。安全性主張を 1 か所に集約する設計です。
図解
Lean ソースコード
lean
theorem updatePauser_ok {s s' : State} {ctx : CallContext} {newPauser : Address}
(h : updatePauser s ctx newPauser = .ok s') :
s.owner = ctx.sender ∧ newPauser ≠ Address.zero ∧ s' = s.setPauser newPauser := by
unfold updatePauser onlyOwner at h
obtain ⟨h1, h⟩ := req_bind_eq_ok h
obtain ⟨h2, h⟩ := req_bind_eq_ok h
exact ⟨h1, h2, pure_ok h⟩