Crate kimberlite_properties 

Antithesis-style property annotations for Deterministic Simulation Testing.

This crate provides lightweight macro_rules! macros for annotating code with temporal property assertions inspired by the Antithesis SDK.

Property Types

• ALWAYS: Condition must hold every time it is evaluated. A single false is a violation.
• SOMETIMES: Condition must be true at least once per simulation run. Guides exploration.
• NEVER: Condition must never be true. Equivalent to always!(!condition).
• REACHED: Code path must be reached at least once per simulation run.
• UNREACHABLE: Code path must never be reached. Violation on first reach.

Zero-Cost in Production

Without feature = "sim", all macros compile to nothing. No runtime overhead. With feature = "sim", assertions record to thread-local registries for VOPR tracking.

Usage

use kimberlite_properties::{always, sometimes, never, reached, unreachable_property};

fn apply_committed(state: State, cmd: Command) -> Result<(State, Vec<Effect>)> {
    let old_offset = state.offset();
    let (new_state, effects) = process(state, cmd)?;

    always!(
        new_state.offset() >= old_offset,
        "offset_monotonicity",
        "applied offset must never decrease"
    );

    sometimes!(
        effects.len() > 3,
        "batch_effects",
        "simulation should sometimes produce large effect batches"
    );

    Ok((new_state, effects))
}

Modules

registry

Thread-local property registry for simulation tracking.

Macros

always

Asserts that a condition is ALWAYS true when evaluated.

never

Asserts that a condition is NEVER true when evaluated.

reached

Asserts that a code path is reached at least once per simulation run.

sometimes

Asserts that a condition is true at least once per simulation run.

unreachable_property

Asserts that a code path is NEVER reached.