|
| 1 | +//! A compile-time-checked layer for writing *read-only* test properties and |
| 2 | +//! *ghost state* on top of the rest of the SDK. |
| 3 | +//! |
| 4 | +//! This module addresses two problems that arise when you sprinkle property |
| 5 | +//! checks (assertions, guidance, randomness) throughout a system under test: |
| 6 | +//! |
| 7 | +//! 1. **Property code must never mutate the system it observes.** If the |
| 8 | +//! expression inside an assertion has a side effect that the program relies |
| 9 | +//! on, then the program behaves differently depending on whether the SDK is |
| 10 | +//! compiled in — a silent, dangerous divergence. The [`observe!`] macro |
| 11 | +//! turns "my property accidentally mutated the system" into a *compile |
| 12 | +//! error*. |
| 13 | +//! |
| 14 | +//! 2. **You sometimes want state that exists only to express properties.** In |
| 15 | +//! formal verification this is called *ghost state*: auxiliary state that |
| 16 | +//! exists only to express properties and is erased from production builds, |
| 17 | +//! so it can never change the behavior of the system it describes. A common |
| 18 | +//! use is holding a *reference model* of the system — a simplified shadow to |
| 19 | +//! diff the real system against — but it can just as well be an event |
| 20 | +//! counter or the set of keys you have seen. [`GhostState<T>`] is opaque |
| 21 | +//! ghost state whose *only* mutator is [`GhostState::mutate`] and whose only |
| 22 | +//! reader is [`observe!`]. Because nothing else can touch it, and because |
| 23 | +//! the closures that do touch it are provably incapable of mutating the |
| 24 | +//! surrounding system, the entire ghost state — its construction, mutation, |
| 25 | +//! and observation — can be safely compiled out with **zero** effect on |
| 26 | +//! program behavior. |
| 27 | +//! |
| 28 | +//! # How the read-only guarantee works |
| 29 | +//! |
| 30 | +//! Everything here is enforced with a single, ordinary Rust trait bound: |
| 31 | +//! [`Fn`]. A closure that satisfies `Fn` captures its environment by shared |
| 32 | +//! reference (or copy) only — the borrow checker rejects any attempt to take a |
| 33 | +//! `&mut` borrow of, reassign, or move out of a captured variable. No `unsafe`, |
| 34 | +//! no procedural macros, no AST inspection. `observe!`, [`GhostState::new`] |
| 35 | +//! and [`GhostState::mutate`] all require `Fn` closures, so any attempt to |
| 36 | +//! mutate the surrounding system from inside them fails to compile. |
| 37 | +//! |
| 38 | +//! ```compile_fail |
| 39 | +//! use antithesis_sdk::observe; |
| 40 | +//! let mut counter = 0u64; |
| 41 | +//! // ERROR: cannot assign to `counter`, it is captured in a `Fn` closure |
| 42 | +//! observe!(|| { counter += 1; }); |
| 43 | +//! ``` |
| 44 | +//! |
| 45 | +//! ```compile_fail |
| 46 | +//! use antithesis_sdk::observe; |
| 47 | +//! let mut items = vec![1, 2, 3]; |
| 48 | +//! // ERROR: `Vec::pop` needs `&mut`, which a `Fn` closure cannot obtain |
| 49 | +//! observe!(|| { items.pop(); }); |
| 50 | +//! ``` |
| 51 | +//! |
| 52 | +//! Mutable *locals* created inside the closure are unaffected — the bound only |
| 53 | +//! constrains captures: |
| 54 | +//! |
| 55 | +//! ``` |
| 56 | +//! use antithesis_sdk::observe; |
| 57 | +//! let readings = [3u64, 7, 1]; |
| 58 | +//! observe!(|| { |
| 59 | +//! let mut total = 0; // local: fine |
| 60 | +//! for r in &readings { // reading the environment: fine |
| 61 | +//! total += *r; |
| 62 | +//! } |
| 63 | +//! let _ = total; |
| 64 | +//! }); |
| 65 | +//! ``` |
| 66 | +//! |
| 67 | +//! # Compiling out |
| 68 | +//! |
| 69 | +//! This layer is gated on the crate's `full` feature, just like the rest of the |
| 70 | +//! SDK. When `full` is disabled, [`GhostState<T>`] becomes a zero-sized type, |
| 71 | +//! `new`'s initializer is never run, and the `mutate`/`observe!` closures are |
| 72 | +//! type-checked but **never executed**. The read-only and type checks still |
| 73 | +//! happen in *every* build configuration, so the same source compiles |
| 74 | +//! identically whether or not the SDK is active. |
| 75 | +//! |
| 76 | +//! # Limitation |
| 77 | +//! |
| 78 | +//! `Fn` enforces read-only access *through the reference system*. It stops |
| 79 | +//! `&mut` borrows, reassignment, moves, and `&mut self` method calls, but it |
| 80 | +//! does **not** stop interior mutability (`Cell`, `RefCell`, `Mutex`, atomics) |
| 81 | +//! or `unsafe`. That is the borrow checker's definition of "read-only," and it |
| 82 | +//! is the one seam in the guarantee. |
| 83 | +//! |
| 84 | +//! # Thread-safety |
| 85 | +//! |
| 86 | +//! [`GhostState<T>`] is deliberately single-threaded and lock-free: |
| 87 | +//! [`mutate`](GhostState::mutate) takes `&mut self`. Introducing |
| 88 | +//! synchronization here could perturb the ordering of the system under test, |
| 89 | +//! and any concurrency should be a property of the system itself, not of the |
| 90 | +//! Antithesis instrumentation. Wrap the ghost state in your own synchronization |
| 91 | +//! primitive if you need to share it — that primitive then belongs to (and is |
| 92 | +//! visible to Antithesis as part of) your system. |
| 93 | +
|
| 94 | +/// Opaque *ghost state* whose inner `T` can be read only through [`observe!`] |
| 95 | +/// and mutated only through [`GhostState::mutate`]. |
| 96 | +/// |
| 97 | +/// When the crate's `full` feature is enabled this holds a `T`; otherwise it is |
| 98 | +/// a zero-sized type and every access is compiled out. See the [module |
| 99 | +/// docs](self) for the full rationale. |
| 100 | +/// |
| 101 | +/// The common base traits are derived and available whenever `T` implements |
| 102 | +/// them, with identical bounds in both build configurations. |
| 103 | +/// |
| 104 | +/// # Example |
| 105 | +/// |
| 106 | +/// ``` |
| 107 | +/// use antithesis_sdk::{observe, ghost::GhostState}; |
| 108 | +/// use serde_json::json; |
| 109 | +/// |
| 110 | +/// // A tiny reference model: the number of items we believe are in flight. |
| 111 | +/// let mut in_flight = GhostState::new(|| 0i64); |
| 112 | +/// |
| 113 | +/// // Drive it from your system's events. |
| 114 | +/// in_flight.mutate(|n| *n += 1); |
| 115 | +/// in_flight.mutate(|n| *n -= 1); |
| 116 | +/// |
| 117 | +/// // Check a property over it — read-only. |
| 118 | +/// observe!(in_flight, |n: &i64| { |
| 119 | +/// antithesis_sdk::assert_always!(*n >= 0, "never negative in flight", &json!({ "n": *n })); |
| 120 | +/// }); |
| 121 | +/// ``` |
| 122 | +#[cfg(feature = "full")] |
| 123 | +#[derive(Debug, Default, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] |
| 124 | +pub struct GhostState<T>(T); |
| 125 | + |
| 126 | +/// See the [`full`-featured definition](GhostState) for documentation. |
| 127 | +#[cfg(not(feature = "full"))] |
| 128 | +#[derive(Debug, Default, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] |
| 129 | +pub struct GhostState<T>(::core::marker::PhantomData<T>); |
| 130 | + |
| 131 | +#[cfg(feature = "full")] |
| 132 | +impl<T> GhostState<T> { |
| 133 | + /// Creates ghost state, initializing the inner `T` with `init`. |
| 134 | + /// |
| 135 | + /// `init` is a read-only closure (it may observe the surrounding system but |
| 136 | + /// not mutate it). When the SDK is compiled out, `init` is **never called** |
| 137 | + /// and no `T` is constructed. |
| 138 | + pub fn new<F: Fn() -> T>(init: F) -> Self { |
| 139 | + GhostState(init()) |
| 140 | + } |
| 141 | + |
| 142 | + /// The sole way to mutate the ghost state. |
| 143 | + /// |
| 144 | + /// `f` receives an exclusive `&mut T` to the ghost state's interior (which |
| 145 | + /// it may freely mutate); everything it captures from the surrounding |
| 146 | + /// environment is read-only, enforced by the `Fn` bound. When the SDK is |
| 147 | + /// compiled out, `f` is type-checked but never called. |
| 148 | + pub fn mutate<F: Fn(&mut T)>(&mut self, f: F) { |
| 149 | + f(&mut self.0) |
| 150 | + } |
| 151 | + |
| 152 | + /// Private read accessor. The only callers are the crate-internal |
| 153 | + /// `__observe*` helpers in this module — there is deliberately **no** public |
| 154 | + /// way to obtain a `&T`, so ghost state can only be read from inside an |
| 155 | + /// `observe!` closure. |
| 156 | + fn inner(&self) -> &T { |
| 157 | + &self.0 |
| 158 | + } |
| 159 | +} |
| 160 | + |
| 161 | +#[cfg(not(feature = "full"))] |
| 162 | +impl<T> GhostState<T> { |
| 163 | + /// See the [`full`-featured definition](GhostState::new). |
| 164 | + #[allow(unused_variables)] |
| 165 | + pub fn new<F: Fn() -> T>(init: F) -> Self { |
| 166 | + GhostState(::core::marker::PhantomData) |
| 167 | + } |
| 168 | + |
| 169 | + /// See the [`full`-featured definition](GhostState::mutate). |
| 170 | + #[allow(unused_variables)] |
| 171 | + pub fn mutate<F: Fn(&mut T)>(&mut self, f: F) {} |
| 172 | +} |
| 173 | + |
| 174 | +// Generates the per-arity `__observeN` helper functions that back `observe!`. |
| 175 | +// |
| 176 | +// These are defined and instantiated *within this crate*, so the `full` cfg is |
| 177 | +// resolved against this crate's features (not the downstream crate's). Each |
| 178 | +// function carries the `Fn(&T0, ..)` bound that enforces read-only access and |
| 179 | +// pins the closure's parameter types to the ghost states' inner types. When |
| 180 | +// `full` is off the body is empty, so the closure is type-checked but never |
| 181 | +// executed. |
| 182 | +macro_rules! define_observe_helpers { |
| 183 | + ($( $name:ident ( $($ty:ident : $arg:ident),* ) ),* $(,)?) => {$( |
| 184 | + #[cfg(feature = "full")] |
| 185 | + #[doc(hidden)] |
| 186 | + #[allow(clippy::too_many_arguments)] |
| 187 | + pub fn $name<$($ty,)* F: Fn($(&$ty),*)>( |
| 188 | + $($arg: &GhostState<$ty>,)* f: F, |
| 189 | + ) { |
| 190 | + f($($arg.inner()),*) |
| 191 | + } |
| 192 | + |
| 193 | + #[cfg(not(feature = "full"))] |
| 194 | + #[doc(hidden)] |
| 195 | + #[allow(unused_variables, clippy::too_many_arguments)] |
| 196 | + pub fn $name<$($ty,)* F: Fn($(&$ty),*)>( |
| 197 | + $($arg: &GhostState<$ty>,)* f: F, |
| 198 | + ) {} |
| 199 | + )*}; |
| 200 | +} |
| 201 | + |
| 202 | +define_observe_helpers! { |
| 203 | + __observe0(), |
| 204 | + __observe1(T0: m0), |
| 205 | + __observe2(T0: m0, T1: m1), |
| 206 | + __observe3(T0: m0, T1: m1, T2: m2), |
| 207 | + __observe4(T0: m0, T1: m1, T2: m2, T3: m3), |
| 208 | + __observe5(T0: m0, T1: m1, T2: m2, T3: m3, T4: m4), |
| 209 | + __observe6(T0: m0, T1: m1, T2: m2, T3: m3, T4: m4, T5: m5), |
| 210 | + __observe7(T0: m0, T1: m1, T2: m2, T3: m3, T4: m4, T5: m5, T6: m6), |
| 211 | + __observe8(T0: m0, T1: m1, T2: m2, T3: m3, T4: m4, T5: m5, T6: m6, T7: m7), |
| 212 | +} |
| 213 | + |
| 214 | +/// Runs a read-only observation block, optionally borrowing one or more |
| 215 | +/// [`GhostState`]s. |
| 216 | +/// |
| 217 | +/// The block is a closure that may call any of this crate's APIs — assertions, |
| 218 | +/// guidance, randomness, lifecycle — but is forbidden by the compiler from |
| 219 | +/// mutating anything it captures from the surrounding system (see the [module |
| 220 | +/// docs](self)). With no ghost state it is a pure property block; with ghost |
| 221 | +/// state it receives a shared `&T` to each one's interior. It evaluates to `()`. |
| 222 | +/// |
| 223 | +/// When the SDK is compiled out the closure is type-checked but never executed. |
| 224 | +/// |
| 225 | +/// Up to 8 ghost states may be observed at once. |
| 226 | +/// |
| 227 | +/// # Examples |
| 228 | +/// |
| 229 | +/// ``` |
| 230 | +/// use antithesis_sdk::{observe, ghost::GhostState}; |
| 231 | +/// use serde_json::json; |
| 232 | +/// |
| 233 | +/// // No ghost state: a plain property block over the surrounding system. |
| 234 | +/// let temperature = 42; |
| 235 | +/// observe!(|| { |
| 236 | +/// antithesis_sdk::assert_always!(temperature < 100, "not overheating", &json!({ "t": temperature })); |
| 237 | +/// }); |
| 238 | +/// |
| 239 | +/// // One ghost state. |
| 240 | +/// let seen = GhostState::new(|| 0u64); |
| 241 | +/// observe!(seen, |count: &u64| { |
| 242 | +/// let _ = *count; |
| 243 | +/// }); |
| 244 | +/// |
| 245 | +/// // Several ghost states with a trailing comma. |
| 246 | +/// let a = GhostState::new(|| 1u64); |
| 247 | +/// let b = GhostState::new(|| String::from("ok")); |
| 248 | +/// observe!(a, b, |x: &u64, y: &String| { |
| 249 | +/// let _ = (*x, y.len()); |
| 250 | +/// },); |
| 251 | +/// ``` |
| 252 | +#[macro_export] |
| 253 | +macro_rules! observe { |
| 254 | + ($closure:expr $(,)?) => { |
| 255 | + $crate::ghost::__observe0($closure) |
| 256 | + }; |
| 257 | + ($m0:expr, $closure:expr $(,)?) => { |
| 258 | + $crate::ghost::__observe1(&$m0, $closure) |
| 259 | + }; |
| 260 | + ($m0:expr, $m1:expr, $closure:expr $(,)?) => { |
| 261 | + $crate::ghost::__observe2(&$m0, &$m1, $closure) |
| 262 | + }; |
| 263 | + ($m0:expr, $m1:expr, $m2:expr, $closure:expr $(,)?) => { |
| 264 | + $crate::ghost::__observe3(&$m0, &$m1, &$m2, $closure) |
| 265 | + }; |
| 266 | + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $closure:expr $(,)?) => { |
| 267 | + $crate::ghost::__observe4(&$m0, &$m1, &$m2, &$m3, $closure) |
| 268 | + }; |
| 269 | + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $m4:expr, $closure:expr $(,)?) => { |
| 270 | + $crate::ghost::__observe5(&$m0, &$m1, &$m2, &$m3, &$m4, $closure) |
| 271 | + }; |
| 272 | + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $m4:expr, $m5:expr, $closure:expr $(,)?) => { |
| 273 | + $crate::ghost::__observe6(&$m0, &$m1, &$m2, &$m3, &$m4, &$m5, $closure) |
| 274 | + }; |
| 275 | + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $m4:expr, $m5:expr, $m6:expr, $closure:expr $(,)?) => { |
| 276 | + $crate::ghost::__observe7(&$m0, &$m1, &$m2, &$m3, &$m4, &$m5, &$m6, $closure) |
| 277 | + }; |
| 278 | + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $m4:expr, $m5:expr, $m6:expr, $m7:expr, $closure:expr $(,)?) => { |
| 279 | + $crate::ghost::__observe8(&$m0, &$m1, &$m2, &$m3, &$m4, &$m5, &$m6, &$m7, $closure) |
| 280 | + }; |
| 281 | + ($($rest:tt)*) => { |
| 282 | + ::std::compile_error!( |
| 283 | +r#"Invalid syntax when calling macro `observe`. |
| 284 | +Example usage: |
| 285 | + `observe!(|| { /* read-only property checks */ })` |
| 286 | + `observe!(ghost, |g: &T| { /* read-only checks over `g` and the environment */ })` |
| 287 | +Up to 8 ghost states may be observed at once; the final argument must be the closure."# |
| 288 | + ); |
| 289 | + }; |
| 290 | +} |
0 commit comments