JPYCv2 形式検証

外観

JPYC.pause_sets_paused ​

名称・種別 ​

  • 名称: JPYC.pause_sets_paused
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:212-214
  • 概要: pause は paused を true に、unpause は false にする（効果）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext}, Eq (JPYC.pause s ctx) (Except.ok s') → Eq s'.paused Bool.true

pause の成功は paused = true を、unpause の成功は paused = false をもたらす、という効果定理（pause 側）です。

和訳 docstring ​

効果。 pause は paused := true、unpause は paused := false に設定する。

解説 ​

何を述べているか。 pause が成功した結果状態では paused = true です（対になる unpause_sets_unpaused は false）。pause_ok の結果状態から従います。

直感。 「非常停止ボタンを押したら、ちゃんと停止状態になる」を確認します。

なぜ安全性に効くか。 停止フラグが確実に立つことで、whenNotPaused を持つ全関数が以降 revert します（mint_paused などの停止系定理）。緊急停止が実効性を持つ根拠です。

図解 ​

Lean ソースコード ​

lean
/-- **Effect.** `pause` sets `paused := true`; `unpause` sets `paused := false`. -/
theorem pause_sets_paused {s s' : State} {ctx : CallContext} (h : pause s ctx = .ok s') :
    s'.paused = true := by obtain ⟨_, rfl⟩ := pause_ok h; rfl

依存 ​