warp_types_pdr/
session.rs

1//! PDR session with lifetime-branded phase tracking.
2//!
3//! `PdrSession<'s, P>` follows the pattern from `warp_types_bmc::BmcSession`:
4//! - `'s` is an invariant lifetime brand (prevents cross-session mixing)
5//! - `P: Phase` tracks the current PDR workflow phase
6//! - Transitions consume the session and produce a new phase
7//! - Terminal states (`Safe`, `CounterexampleFound`, `Exhausted`) have no outgoing transitions
8//!
9//! Zero-sized — all PDR state (frames, obligations) lives inside `checker::check()`.
10
11use core::marker::PhantomData;
12use crate::phase::*;
13
14// ============================================================================
15// PDR session
16// ============================================================================
17
18/// A PDR session branded with lifetime `'s` and phase `P`.
19///
20/// Zero-sized — all phase tracking is compile-time only.
21#[must_use = "dropping a PdrSession loses phase tracking — use a transition or terminal"]
22pub struct PdrSession<'s, P: Phase> {
23    _brand: PhantomData<fn(&'s ()) -> &'s ()>,
24    _phase: PhantomData<P>,
25}
26
27impl<'s, P: Phase> PdrSession<'s, P> {
28    pub(crate) fn new() -> Self {
29        PdrSession {
30            _brand: PhantomData,
31            _phase: PhantomData,
32        }
33    }
34
35    /// Current phase name.
36    pub fn phase_name(&self) -> &'static str {
37        P::NAME
38    }
39}
40
41// ============================================================================
42// Phase transitions
43// ============================================================================
44
45impl<'s> PdrSession<'s, Init> {
46    /// Load a transition system model. Consumes Init, produces Modeled.
47    pub fn build_model(self) -> PdrSession<'s, Modeled> {
48        PdrSession::new()
49    }
50}
51
52impl<'s> PdrSession<'s, Modeled> {
53    /// Check result: property is safe (inductive invariant found).
54    pub fn check_safe(self) -> PdrSession<'s, Safe> {
55        PdrSession::new()
56    }
57
58    /// Check result: counterexample found.
59    pub fn check_counterexample(self) -> PdrSession<'s, CounterexampleFound> {
60        PdrSession::new()
61    }
62
63    /// Check result: frame budget exhausted.
64    pub fn check_exhausted(self) -> PdrSession<'s, Exhausted> {
65        PdrSession::new()
66    }
67}
68
69// ============================================================================
70// Entry point
71// ============================================================================
72
73/// Create a PDR session with a fresh lifetime brand.
74pub fn with_session<R>(f: impl for<'s> FnOnce(PdrSession<'s, Init>) -> R) -> R {
75    f(PdrSession::new())
76}
warp_types_pdr/session.rs

warp_types_pdr/
session.rs
