Assertion Reference

• Boolean Assertions
  • assert_always!(condition, message)
  • assert_always_or_unreachable!(condition, message)
  • assert_sometimes!(condition, message)
  • assert_reachable!(message)
  • assert_unreachable!(message)
• Numeric Assertions
  • Always numeric example
  • Sometimes numeric example
• Compound Assertions
  • assert_sometimes_all!(message, [(name, bool), ...])
  • assert_sometimes_each!(message, [(key, value), ...]) / assert_sometimes_each!(message, [(key, value), ...], [(quality_key, quality_value), ...])
• Validation: validate_assertion_contracts()
  • Always violations (definite bugs)
  • Coverage violations (statistical)
• Related Functions

Moonpool provides 15 assertion macros for testing distributed system properties. All macros follow the Antithesis principle: assertions never crash your program. Violations are recorded in shared memory and reported after the simulation completes, allowing the system to continue running and discover cascading failures.

Every macro is tracked in shared memory via moonpool-explorer, enabling cross-process visibility across forked exploration timelines.

Boolean Assertions

These macros test boolean conditions. Always-type assertions record violations but do not panic. Sometimes-type assertions guide exploration by triggering forks on discovery.

assert_always!(condition, message)

Records a violation if condition is false. The simulation continues; violations are collected and reported at the end. Validated by validate_assertion_contracts() which flags the assertion if fail_count > 0, or if must_hit and the assertion was never reached.

#![allow(unused)]
fn main() {
assert_always!(
    granted_count <= 1,
    "lock never granted to two nodes simultaneously"
);
}

assert_always_or_unreachable!(condition, message)

Like assert_always!, but does not require the code path to be reached. If the code is never executed, the assertion passes silently. Useful for guarding optional error-handling paths.

#![allow(unused)]
fn main() {
assert_always_or_unreachable!(
    retry_count < max_retries,
    "retry count within bounds when retry path taken"
);
}

assert_sometimes!(condition, message)

Records pass/fail statistics. The first time the condition is true is a discovery: in exploration mode the explorer anchors alternate timelines at that point. Validated by checking that pass_count > 0 after enough iterations.

#![allow(unused)]
fn main() {
assert_sometimes!(
    saw_leader_election,
    "leader election triggered at least once"
);
}

assert_reachable!(message)

Marks a code path as “should be reached.” Always passes true as the condition. First reach is a discovery. Validated by checking that pass_count > 0.

#![allow(unused)]
fn main() {
if connection_failed {
    assert_reachable!("retry path exercised");
    retry().await;
}
}

assert_unreachable!(message)

Marks a code path that should never execute. If reached, records a violation (but does not panic). Validated by checking that pass_count == 0.

#![allow(unused)]
fn main() {
match state {
    State::Valid => { /* ok */ }
    State::Invalid => {
        assert_unreachable!("invalid state should never occur");
    }
}
}

Numeric Assertions

These macros compare a value against a threshold. Always-type numeric assertions record violations on failure. Sometimes-type numeric assertions track watermarks (best observed value); a watermark improvement is a discovery.

All values are cast to i64 internally.

Always numeric example

#![allow(unused)]
fn main() {
assert_always_greater_than!(
    queue.len(),
    0,
    "queue never empty during processing"
);

assert_always_less_than_or_equal_to!(
    latency_ms,
    timeout_ms,
    "response latency within timeout"
);
}

Sometimes numeric example

#![allow(unused)]
fn main() {
assert_sometimes_greater_than!(
    concurrent_connections,
    5,
    "achieved high concurrency"
);

assert_sometimes_less_than!(
    retry_delay_ms,
    100,
    "fast retry path exercised"
);
}

Watermark tracking: For sometimes numeric assertions, the explorer tracks the best value observed so far. When a new evaluation improves the watermark (higher for gt/ge, lower for lt/le), it creates a replay anchor for timelines that might push the metric even further.

Compound Assertions

These macros track multi-dimensional properties across multiple conditions or identity keys.

assert_sometimes_all!(message, [(name, bool), ...])

Tracks a frontier: the maximum number of conditions that have been simultaneously true. When the frontier advances (more conditions true at once than ever before), a replay anchor is created.

#![allow(unused)]
fn main() {
assert_sometimes_all!("all_nodes_healthy", [
    ("node_a", node_a_healthy),
    ("node_b", node_b_healthy),
    ("node_c", node_c_healthy),
]);
}

If previously at most 2 of the 3 conditions were true at once, and now all 3 are true, the frontier advances from 2 to 3 and a replay anchor is created.

assert_sometimes_each!(message, [(key, value), ...]) / assert_sometimes_each!(message, [(key, value), ...], [(quality_key, quality_value), ...])

Each unique combination of identity keys gets its own bucket. A new bucket is a discovery. If quality keys are provided, the explorer also tracks quality watermarks per bucket, and a quality improvement is a fresh discovery (registering a healthier exemplar for the same state).

#![allow(unused)]
fn main() {
// Identity keys only -- guide on first discovery of each (lock, depth) combo
assert_sometimes_each!("gate", [("lock", lock_id), ("depth", depth)]);

// With quality watermarks -- also guide when health improves for a known bucket
assert_sometimes_each!("descended", [("to_floor", floor)], [("health", hp)]);
}

Validation: validate_assertion_contracts()

After the simulation completes, validate_assertion_contracts() reads all assertion slots from shared memory and checks each one against its kind-specific contract. It returns two vectors:

Always violations (definite bugs)

These indicate real bugs and are safe to check regardless of iteration count.

Coverage violations (statistical)

These are only meaningful with enough iterations for statistical coverage. A single iteration may not trigger every path.

Related Functions