From 9e4d986b5b57ae7ae78528ac2e2ae12523f7f289 Mon Sep 17 00:00:00 2001 From: Carl Sverre <82591+carlsverre@users.noreply.github.com> Date: Mon, 13 Jul 2026 12:11:13 -0700 Subject: [PATCH] Add compile-time-checked ghost/observe layer Add an optional layer on top of the existing API for writing read-only test properties and ghost state: - `observe!` runs a property block that may call any precept API and may optionally borrow one or more `GhostState`s. Its `Fn` bound makes it easier to avoid unintentionally mutating the system under test. - `GhostState` is opaque auxiliary state that exists only to express properties. Its only mutator is `GhostState::mutate` and its only reader is `observe!`, and it is compiled out entirely (to a zero-sized type) when the `enabled` feature is off. Ported from antithesis-sdk-rust#34, adapted to precept's `enabled` feature gate and `expect_*` macros. Co-Authored-By: Claude --- CHANGELOG.md | 5 + src/ghost.rs | 359 +++++++++++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 4 + 3 files changed, 368 insertions(+) create mode 100644 src/ghost.rs diff --git a/CHANGELOG.md b/CHANGELOG.md index 3a0cfa6..bb1bd99 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,11 @@ All notable changes will be documented in this file. +## Unreleased + +- Added `observe!`, a property block that may call any precept API and may optionally borrow one or more `GhostState`s; its `Fn` bound makes it easier to avoid unintentionally mutating the system under test. +- Added `GhostState`, opaque auxiliary state for expressing test properties, readable only via `observe!` and mutable only via `GhostState::mutate`, compiled out entirely when the `enabled` feature is off. + ## 0.2.0 - 2025-12-10 - Added new fault system diff --git a/src/ghost.rs b/src/ghost.rs new file mode 100644 index 0000000..98f3436 --- /dev/null +++ b/src/ghost.rs @@ -0,0 +1,359 @@ +//! A compile-time-checked layer for writing *read-only* test properties and +//! *ghost state* on top of the rest of precept. +//! +//! This module addresses two problems that arise when you sprinkle property +//! checks (expectations, events, randomness) throughout a system under test: +//! +//! 1. **Property code must never mutate the system it observes.** If the +//! expression inside an expectation has a side effect that the program +//! relies on, then the program behaves differently depending on whether +//! precept is compiled in — a silent, dangerous divergence. The [`observe!`] +//! macro turns "my property accidentally mutated the system" into a *compile +//! error*. +//! +//! 2. **You sometimes want state that exists only to express properties.** In +//! formal verification this is called *ghost state*: auxiliary state that +//! exists only to express properties and is erased from production builds, +//! so it can never change the behavior of the system it describes. A common +//! use is holding a *reference model* of the system — a simplified shadow to +//! diff the real system against — but it can just as well be an event +//! counter or the set of keys you have seen. [`GhostState`] is opaque +//! ghost state whose *only* mutator is [`GhostState::mutate`] and whose only +//! reader is [`observe!`]. Because nothing else can touch it, and because +//! the closures that do touch it are provably incapable of mutating the +//! surrounding system, the entire ghost state — its construction, mutation, +//! and observation — can be safely compiled out with **zero** effect on +//! program behavior. +//! +//! # How the read-only guarantee works +//! +//! Everything here is enforced with a single, ordinary Rust trait bound: +//! [`Fn`]. A closure that satisfies `Fn` captures its environment by shared +//! reference (or copy) only — the borrow checker rejects any attempt to take a +//! `&mut` borrow of, reassign, or move out of a captured variable. No `unsafe`, +//! no procedural macros, no AST inspection. `observe!`, [`GhostState::new`] +//! and [`GhostState::mutate`] all require `Fn` closures, so any attempt to +//! mutate the surrounding system from inside them fails to compile. +//! +//! ```compile_fail +//! use precept::observe; +//! let mut counter = 0u64; +//! // ERROR: cannot assign to `counter`, it is captured in a `Fn` closure +//! observe!(|| { counter += 1; }); +//! ``` +//! +//! ```compile_fail +//! use precept::observe; +//! let mut items = vec![1, 2, 3]; +//! // ERROR: `Vec::pop` needs `&mut`, which a `Fn` closure cannot obtain +//! observe!(|| { items.pop(); }); +//! ``` +//! +//! Mutable *locals* created inside the closure are unaffected — the bound only +//! constrains captures: +//! +//! ``` +//! use precept::observe; +//! let readings = [3u64, 7, 1]; +//! observe!(|| { +//! let mut total = 0; // local: fine +//! for r in &readings { // reading the environment: fine +//! total += *r; +//! } +//! let _ = total; +//! }); +//! ``` +//! +//! # Compiling out +//! +//! This layer is gated on the crate's `enabled` feature, just like the rest of +//! precept. When `enabled` is disabled, [`GhostState`] becomes a zero-sized +//! type, `new`'s initializer is never run, and the `mutate`/`observe!` closures +//! are type-checked but **never executed**. The read-only and type checks still +//! happen in *every* build configuration, so the same source compiles +//! identically whether or not precept is active. +//! +//! # Limitation +//! +//! `Fn` enforces read-only access *through the reference system*. It stops +//! `&mut` borrows, reassignment, moves, and `&mut self` method calls, but it +//! does **not** stop interior mutability (`Cell`, `RefCell`, `Mutex`, atomics) +//! or `unsafe`. That is the borrow checker's definition of "read-only," and it +//! is the one seam in the guarantee. +//! +//! # Thread-safety +//! +//! [`GhostState`] is deliberately single-threaded and lock-free: +//! [`mutate`](GhostState::mutate) takes `&mut self`. Introducing +//! synchronization here could perturb the ordering of the system under test, +//! and any concurrency should be a property of the system itself, not of the +//! precept instrumentation. Wrap the ghost state in your own synchronization +//! primitive if you need to share it — that primitive then belongs to (and is +//! visible to precept as part of) your system. + +/// Opaque *ghost state* whose inner `T` can be read only through [`observe!`] +/// and mutated only through [`GhostState::mutate`]. +/// +/// When the crate's `enabled` feature is on this holds a `T`; otherwise it is +/// a zero-sized type and every access is compiled out. See the [module +/// docs](self) for the full rationale. +/// +/// The common base traits are derived and available whenever `T` implements +/// them, with identical bounds in both build configurations. +/// +/// # Example +/// +/// ``` +/// use precept::{observe, ghost::GhostState}; +/// +/// // A tiny reference model: the number of items we believe are in flight. +/// let mut in_flight = GhostState::new(|| 0i64); +/// +/// // Drive it from your system's events. +/// in_flight.mutate(|n| *n += 1); +/// in_flight.mutate(|n| *n -= 1); +/// +/// // Check a property over it — read-only. +/// observe!(in_flight, |n: &i64| { +/// precept::expect_always!(*n >= 0, "never negative in flight", { "n": *n }); +/// }); +/// ``` +#[cfg(feature = "enabled")] +#[derive(Debug, Default, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct GhostState(T); + +/// See the [`enabled` definition](GhostState) for documentation. +#[cfg(not(feature = "enabled"))] +#[derive(Debug, Default, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct GhostState(::core::marker::PhantomData); + +#[cfg(feature = "enabled")] +impl GhostState { + /// Creates ghost state, initializing the inner `T` with `init`. + /// + /// `init` is a read-only closure (it may observe the surrounding system but + /// not mutate it). When precept is compiled out, `init` is **never called** + /// and no `T` is constructed. + pub fn new T>(init: F) -> Self { + GhostState(init()) + } + + /// The sole way to mutate the ghost state. + /// + /// `f` receives an exclusive `&mut T` to the ghost state's interior (which + /// it may freely mutate); everything it captures from the surrounding + /// environment is read-only, enforced by the `Fn` bound. When precept is + /// compiled out, `f` is type-checked but never called. + pub fn mutate(&mut self, f: F) { + f(&mut self.0) + } + + /// Private read accessor. The only callers are the crate-internal + /// `__observe*` helpers in this module — there is deliberately **no** public + /// way to obtain a `&T`, so ghost state can only be read from inside an + /// `observe!` closure. + fn inner(&self) -> &T { + &self.0 + } +} + +#[cfg(not(feature = "enabled"))] +impl GhostState { + /// See the [`enabled` definition](GhostState::new). + #[allow(unused_variables)] + pub fn new T>(init: F) -> Self { + GhostState(::core::marker::PhantomData) + } + + /// See the [`enabled` definition](GhostState::mutate). + #[allow(unused_variables)] + pub fn mutate(&mut self, f: F) {} +} + +// Generates the per-arity `__observeN` helper functions that back `observe!`. +// +// These are defined and instantiated *within this crate*, so the `enabled` cfg +// is resolved against this crate's features (not the downstream crate's). Each +// function carries the `Fn(&T0, ..)` bound that enforces read-only access and +// pins the closure's parameter types to the ghost states' inner types. When +// `enabled` is off the body is empty, so the closure is type-checked but never +// executed. +macro_rules! define_observe_helpers { + ($( $name:ident ( $($ty:ident : $arg:ident),* ) ),* $(,)?) => {$( + #[cfg(feature = "enabled")] + #[doc(hidden)] + #[allow(clippy::too_many_arguments)] + pub fn $name<$($ty,)* F: Fn($(&$ty),*)>( + $($arg: &GhostState<$ty>,)* f: F, + ) { + f($($arg.inner()),*) + } + + #[cfg(not(feature = "enabled"))] + #[doc(hidden)] + #[allow(unused_variables, clippy::too_many_arguments)] + pub fn $name<$($ty,)* F: Fn($(&$ty),*)>( + $($arg: &GhostState<$ty>,)* f: F, + ) {} + )*}; +} + +define_observe_helpers! { + __observe0(), + __observe1(T0: m0), + __observe2(T0: m0, T1: m1), + __observe3(T0: m0, T1: m1, T2: m2), + __observe4(T0: m0, T1: m1, T2: m2, T3: m3), + __observe5(T0: m0, T1: m1, T2: m2, T3: m3, T4: m4), + __observe6(T0: m0, T1: m1, T2: m2, T3: m3, T4: m4, T5: m5), + __observe7(T0: m0, T1: m1, T2: m2, T3: m3, T4: m4, T5: m5, T6: m6), + __observe8(T0: m0, T1: m1, T2: m2, T3: m3, T4: m4, T5: m5, T6: m6, T7: m7), +} + +/// Runs a read-only observation block, optionally borrowing one or more +/// [`GhostState`]s. +/// +/// The block is a closure that may call any of precept's APIs — expectations, +/// events, randomness — but is forbidden by the compiler from mutating anything +/// it captures from the surrounding system (see the [module docs](self)). With +/// no ghost state it is a pure property block; with ghost state it receives a +/// shared `&T` to each one's interior. It evaluates to `()`. +/// +/// When precept is compiled out the closure is type-checked but never executed. +/// +/// Up to 8 ghost states may be observed at once. +/// +/// # Examples +/// +/// ``` +/// use precept::{observe, ghost::GhostState}; +/// +/// // No ghost state: a plain property block over the surrounding system. +/// let temperature = 42; +/// observe!(|| { +/// precept::expect_always!(temperature < 100, "not overheating", { "t": temperature }); +/// }); +/// +/// // One ghost state. +/// let seen = GhostState::new(|| 0u64); +/// observe!(seen, |count: &u64| { +/// let _ = *count; +/// }); +/// +/// // Several ghost states with a trailing comma. +/// let a = GhostState::new(|| 1u64); +/// let b = GhostState::new(|| String::from("ok")); +/// observe!(a, b, |x: &u64, y: &String| { +/// let _ = (*x, y.len()); +/// },); +/// ``` +#[macro_export] +macro_rules! observe { + ($closure:expr $(,)?) => { + $crate::ghost::__observe0($closure) + }; + ($m0:expr, $closure:expr $(,)?) => { + $crate::ghost::__observe1(&$m0, $closure) + }; + ($m0:expr, $m1:expr, $closure:expr $(,)?) => { + $crate::ghost::__observe2(&$m0, &$m1, $closure) + }; + ($m0:expr, $m1:expr, $m2:expr, $closure:expr $(,)?) => { + $crate::ghost::__observe3(&$m0, &$m1, &$m2, $closure) + }; + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $closure:expr $(,)?) => { + $crate::ghost::__observe4(&$m0, &$m1, &$m2, &$m3, $closure) + }; + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $m4:expr, $closure:expr $(,)?) => { + $crate::ghost::__observe5(&$m0, &$m1, &$m2, &$m3, &$m4, $closure) + }; + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $m4:expr, $m5:expr, $closure:expr $(,)?) => { + $crate::ghost::__observe6(&$m0, &$m1, &$m2, &$m3, &$m4, &$m5, $closure) + }; + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $m4:expr, $m5:expr, $m6:expr, $closure:expr $(,)?) => { + $crate::ghost::__observe7(&$m0, &$m1, &$m2, &$m3, &$m4, &$m5, &$m6, $closure) + }; + ($m0:expr, $m1:expr, $m2:expr, $m3:expr, $m4:expr, $m5:expr, $m6:expr, $m7:expr, $closure:expr $(,)?) => { + $crate::ghost::__observe8(&$m0, &$m1, &$m2, &$m3, &$m4, &$m5, &$m6, &$m7, $closure) + }; + ($($rest:tt)*) => { + ::std::compile_error!( + r#"Invalid syntax when calling macro `observe`. +Example usage: + `observe!(|| { /* read-only property checks */ })` + `observe!(ghost, |g: &T| { /* read-only checks over `g` and the environment */ })` +Up to 8 ghost states may be observed at once; the final argument must be the closure."# + ); + }; +} + +#[cfg(test)] +mod tests { + use super::GhostState; + + // Compiles and runs in *both* feature configurations. With `enabled` off + // the closures are type-checked but never executed (and `GhostState` is a + // zero-sized type); with it on they run. Either way this must not panic. + #[test] + fn compiles_and_runs_in_all_configs() { + let mut g = GhostState::new(|| 0i64); + g.mutate(|n| *n += 1); + observe!(g, |n: &i64| { + let _ = *n; + }); + observe!(|| {}); + } + + // The remaining tests exercise the real `enabled` behavior: the value the + // closures observe only exists when the crate is enabled. + + // Build ghost state, mutate it repeatedly, then read it back through the + // sole read path (`observe!`) and assert a property from inside the block. + #[cfg(feature = "enabled")] + #[test] + fn ghost_mutate_and_observe() { + let mut seen = GhostState::new(|| 0i64); + for _ in 0..3 { + seen.mutate(|n: &mut i64| *n += 1); + } + + observe!(seen, |n: &i64| { + assert_eq!(*n, 3, "ghost state should have counted 3 events"); + // A precept expectation inside an observe block is allowed. With no + // dispatcher installed it routes to the no-op dispatcher. + crate::expect_always!(*n >= 0, "seen count is never negative", { "seen": *n }); + }); + } + + // Ghost state with several inner types can be observed together, and + // derived traits pass through when the inner type supports them. + #[cfg(feature = "enabled")] + #[test] + fn ghost_multi_and_derives() { + let a = GhostState::new(|| 10u64); + let b = GhostState::new(|| String::from("hello")); + + observe!(a, b, |x: &u64, y: &String| { + assert_eq!(*x, 10); + assert_eq!(y, "hello"); + }); + + // derived traits available because the inner types implement them + let b2 = b.clone(); // Clone (String inner is not Copy) + assert_eq!(b, b2); + let a2 = a; // Copy (u64 inner) + assert_eq!(a, a2); + let d: GhostState = Default::default(); + assert_eq!(format!("{d:?}"), "GhostState(0)"); + } + + // A pure `observe!` block (no ghost state) can still call precept APIs. + #[cfg(feature = "enabled")] + #[test] + fn observe_no_ghost_state() { + let temperature = 42; + observe!(|| { + crate::expect_always!(temperature < 100, "not overheating", { "t": temperature }); + }); + } +} diff --git a/src/lib.rs b/src/lib.rs index 07d8639..ade12ce 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,7 +1,11 @@ pub mod dispatch; pub mod fault; +pub mod ghost; pub mod random; +#[doc(inline)] +pub use crate::ghost::GhostState; + #[doc(hidden)] pub mod catalog;