warp_types_pdr/
phase.rs

1//! PDR phase markers.
2//!
3//! Zero-sized types encoding the IC3/PDR workflow. Sealed —
4//! external crates cannot forge phases or create invalid transitions.
5//!
6//! # Phase machine
7//!
8//! ```text
9//!   Init
10//!     → build_model()       → Modeled
11//!   Modeled
12//!     → check()             → PdrResult
13//!       → Safe                terminal: inductive invariant found
14//!       → CounterexampleFound terminal: concrete trace to bad state
15//!       → Exhausted           terminal: frame budget exceeded
16//! ```
17
18// ============================================================================
19// Sealed trait
20// ============================================================================
21
22pub(crate) mod sealed {
23    pub(crate) struct SealToken;
24
25    #[allow(private_interfaces)]
26    pub trait Sealed {
27        #[doc(hidden)]
28        fn _sealed() -> SealToken;
29    }
30}
31
32// ============================================================================
33// Phase trait + markers
34// ============================================================================
35
36/// Marker trait for PDR phases. Sealed.
37pub trait Phase: sealed::Sealed + 'static {
38    /// Human-readable phase name.
39    const NAME: &'static str;
40}
41
42/// Initial state — no model loaded yet.
43#[derive(Debug)]
44pub struct Init;
45
46/// Model built — transition system loaded, ready for PDR.
47#[derive(Debug)]
48pub struct Modeled;
49
50/// Inductive invariant found — property is safe at all depths.
51/// Terminal phase.
52#[derive(Debug)]
53pub struct Safe;
54
55/// Counterexample trace found — property is violated.
56/// Terminal phase.
57#[derive(Debug)]
58pub struct CounterexampleFound;
59
60/// Frame budget exhausted without conclusive result.
61/// Terminal phase.
62#[derive(Debug)]
63pub struct Exhausted;
64
65// ============================================================================
66// Sealed + Phase impls
67// ============================================================================
68
69macro_rules! impl_phase {
70    ($ty:ty, $name:literal) => {
71        #[allow(private_interfaces)]
72        impl sealed::Sealed for $ty {
73            fn _sealed() -> sealed::SealToken {
74                sealed::SealToken
75            }
76        }
77        impl Phase for $ty {
78            const NAME: &'static str = $name;
79        }
80    };
81}
82
83impl_phase!(Init, "init");
84impl_phase!(Modeled, "modeled");
85impl_phase!(Safe, "safe");
86impl_phase!(CounterexampleFound, "counterexample-found");
87impl_phase!(Exhausted, "exhausted");
warp_types_pdr/phase.rs

warp_types_pdr/
phase.rs
