Trait LazyBalanceModelChecker

pub trait LazyBalanceModelChecker: Sized {
    type LazyBalance: LazyBalanceMarker;
    type ManualBalance: ManualBalanceModel<Self::LazyBalance> + BalanceStateHasher<Self::LazyBalance, Self::ManualBalance> + BalanceGuards<Self::LazyBalance, Self::ManualBalance> + Clone;
    type TrapFn: Fn(&BalanceState<Self::LazyBalance, Self::ManualBalance>, &BalanceOp<Self::LazyBalance, Self::ManualBalance>) -> bool;
    type FlowFn: Fn(&BalanceState<Self::LazyBalance, Self::ManualBalance>, &BalanceOp<Self::LazyBalance, Self::ManualBalance>) -> bool;
    type Hasher: Fn(&BalanceState<Self::LazyBalance, Self::ManualBalance>) -> u64;

    // Provided methods
    fn initiate_results(    ) -> BalanceModelResults<Self::LazyBalance, Self::ManualBalance> { ... }
    fn explore(
        users: &[<Self::ManualBalance as ManualBalanceModel<Self::LazyBalance>>::User],
        deposits: &[<Self::LazyBalance as LazyBalance>::Asset],
        adjustments: &[<Self::LazyBalance as LazyBalance>::Asset],
        subjects: &[<Self::LazyBalance as LazyBalance>::Subject],
        max_depth: u32,
        allowed_bps: u32,
        allowed_diff: u32,
        results: &mut BalanceModelResults<Self::LazyBalance, Self::ManualBalance>,
    )
       where <Self::LazyBalance as LazyBalance>::Id: Default,
             <Self::LazyBalance as LazyBalance>::Asset: From<<Self::LazyBalance as LazyBalance>::Asset> + Into<<Self::LazyBalance as LazyBalance>::Asset> { ... }
    fn explore_traps(
        users: &[<Self::ManualBalance as ManualBalanceModel<Self::LazyBalance>>::User],
        deposits: &[<Self::LazyBalance as LazyBalance>::Asset],
        adjustments: &[<Self::LazyBalance as LazyBalance>::Asset],
        subjects: &[<Self::LazyBalance as LazyBalance>::Subject],
        max_depth: u32,
        allowed_bps: u32,
        allowed_diff: u32,
        traps: Option<BalanceTraps<Self::TrapFn, Self::FlowFn>>,
        results: &mut BalanceModelResults<Self::LazyBalance, Self::ManualBalance>,
    )
       where <Self::LazyBalance as LazyBalance>::Id: Default,
             <Self::LazyBalance as LazyBalance>::Asset: From<<Self::LazyBalance as LazyBalance>::Asset> + Into<<Self::LazyBalance as LazyBalance>::Asset> { ... }
    fn explore_custom(
        users: &[<Self::ManualBalance as ManualBalanceModel<Self::LazyBalance>>::User],
        deposits: &[<Self::LazyBalance as LazyBalance>::Asset],
        adjustments: &[<Self::LazyBalance as LazyBalance>::Asset],
        subjects: &[<Self::LazyBalance as LazyBalance>::Subject],
        max_depth: u32,
        allowed_bps: u32,
        allowed_diff: u32,
        traps: Option<BalanceTraps<Self::TrapFn, Self::FlowFn>>,
        hasher: Option<Self::Hasher>,
        results: &mut BalanceModelResults<Self::LazyBalance, Self::ManualBalance>,
    )
       where <Self::LazyBalance as LazyBalance>::Id: Default,
             <Self::LazyBalance as LazyBalance>::Asset: From<<Self::LazyBalance as LazyBalance>::Asset> + Into<<Self::LazyBalance as LazyBalance>::Asset> { ... }
    fn write_reports(
        dir: PathBuf,
        results: &BalanceModelResults<Self::LazyBalance, Self::ManualBalance>,
        write_pass: bool,
        write_exit: bool,
        write_trap: bool,
    ) { ... }
}

Unified model checker interface over the lazy balance model checker module.

This trait provides a single entrypoint API to access all model-checking utilities.

By implementing this trait on a tester type, you bind:

• the lazy model (Self::LazyBalance) under test
• the manual reference model (Self::ManualBalance)
• guards, hashing, and execution semantics

Underlying System

• ManualBalanceModel: eager balance reference model
• BalanceOp: balance operations set
• BalanceState: execution state (lazy + manual + trace)
• BalanceGuards: operation validity rules
• BalanceTraps: controlled invalid execution
• BalanceModelResults: result aggregation

What happens during execution

• sequences of BalanceOp are explored (breadth-first)
• each step builds on a trace to form a BalanceState
• operations are filtered using:
  • BalanceGuards -> define normal validity
  • BalanceTraps -> allow controlled invalid cases

An operation is considered valid for execution if:

• it passes the guard, OR
• it is explicitly allowed by a trap

Additionally, exploration is further controlled by flow:

• both guard flow and trap flow must allow the operation

• if either blocks it, the operation is not explored further

• both models are executed:

  • lazy: Self::LazyBalance via LazyBalance
  • manual: Self::ManualBalance vi ManualBalanceModel

• results are classified into:

  • BalanceFailure: execution error
  • BalanceExit: drift between models
  • pass: successful sequence
  • trap: expected failure via BalanceTraps

Usage

struct Tester;

impl LazyBalanceModelChecker for Tester {
    type LazyBalance = Balance;
    type ManualBalance = Manual;

    type TrapFn = fn(
        &BalanceState<Self::LazyBalance, Self::ManualBalance>,
        &BalanceOp<Self::LazyBalance, Self::ManualBalance>,
    ) -> bool;

    type FlowFn = fn(
        &BalanceState<Self::LazyBalance, Self::ManualBalance>,
        &BalanceOp<Self::LazyBalance, Self::ManualBalance>,
    ) -> bool;

    type Hasher = fn(
        &BalanceState<Self::LazyBalance, Self::ManualBalance>,
    ) -> u64;
}

let mut results = Tester::initiate_results();

Tester::explore(..., &mut results);
// or
Tester::explore_with_traps(..., Some(traps), &mut results);
// or
Tester::explore_custom(..., Some(traps), &mut results);

Tester::write_reports(path, &results, false, false, false);

Required Associated Types

type LazyBalance: LazyBalanceMarker

Lazy balance implementation.

type ManualBalance: ManualBalanceModel<Self::LazyBalance> + BalanceStateHasher<Self::LazyBalance, Self::ManualBalance> + BalanceGuards<Self::LazyBalance, Self::ManualBalance> + Clone

Manual (reference) model used for validation.

This type provides an eager execution layer over the lazy model:

• consumes resolved outputs from Self::LazyBalance via LazyBalance
• maintains a concrete, user-facing state

Unlike the lazy model, this operates as a direct global state model via ManualBalanceModel methods:

• no deferred receipts
• no lazy resolution
• updates are applied immediately to a single state

It must also define:

• BalanceStateHasher: for state deduplication during exploration
• BalanceGuards: for operation validity and invariants

Acts as the reference baseline against which the lazy model is evaluated for correctness and precision.

type TrapFn: Fn(&BalanceState<Self::LazyBalance, Self::ManualBalance>, &BalanceOp<Self::LazyBalance, Self::ManualBalance>) -> bool

Trap predicate used for trap-based testing.

Represents a single trap condition applied across all operations:

• evaluated per (state, op)
• returns true to override guards defined in BalanceGuards via Self::ManualBalance

This trap is injected globally during exploration, so it will be evaluated for every operation (BalanceOp). Implementations should therefore:

• precisely target the intended operation/condition
• return false for all unrelated operations

Unlike BalanceGuards, which define validity for all operations at once, this is defined per invocation to inject a specific invalid scenario.

Used to enable controlled violations:

guard(...) || trap(...)

type FlowFn: Fn(&BalanceState<Self::LazyBalance, Self::ManualBalance>, &BalanceOp<Self::LazyBalance, Self::ManualBalance>) -> bool

Flow predicate used to control exploration.

Applied globally across all operations:

• evaluated per (state, op)
• returns true to allow the candidate operation BalanceOp to proceed
• returns false to block exploration of that operation

Combined with the base guard flow as:

guard_flow(...) && trap_flow(...)

Unlike Self::TrapFn, this does not override validity; it only restricts whether an operation is explored.

Since this is combined using &&, returning false will prevent the operation from being explored entirely. Therefore implementations should:

• return true by default
• only return false when explicitly pruning a specific case

Used to shape the search space (e.g., pruning, targeting).

type Hasher: Fn(&BalanceState<Self::LazyBalance, Self::ManualBalance>) -> u64

Optional additional custom state hasher.

Provides an additional hashing layer over BalanceState during exploration:

• evaluated alongside BalanceStateHasher from Self::ManualBalance
• used for further deduplication of states

Since Self::ManualBalance already defines a primary hashing strategy via BalanceStateHasher, this acts as an optional second-stage filter.

This is particularly useful when:

• multiple exploration strategies or model checkers are run
• additional pruning is needed beyond the primary state hash

In such cases, this hasher can be applied on top of the base hasher to refine state uniqueness and avoid revisiting equivalent states.

If provided, both hashes are used during exploration.

Provided Methods

fn initiate_results() -> BalanceModelResults<Self::LazyBalance, Self::ManualBalance>

Creates a new BalanceModelResults container.

fn explore( users: &[<Self::ManualBalance as ManualBalanceModel<Self::LazyBalance>>::User], deposits: &[<Self::LazyBalance as LazyBalance>::Asset], adjustments: &[<Self::LazyBalance as LazyBalance>::Asset], subjects: &[<Self::LazyBalance as LazyBalance>::Subject], max_depth: u32, allowed_bps: u32, allowed_diff: u32, results: &mut BalanceModelResults<Self::LazyBalance, Self::ManualBalance>, )

where <Self::LazyBalance as LazyBalance>::Id: Default, <Self::LazyBalance as LazyBalance>::Asset: From<<Self::LazyBalance as LazyBalance>::Asset> + Into<<Self::LazyBalance as LazyBalance>::Asset>,

Runs model exploration under valid conditions (guards only).

Explores sequences of operations using BalanceGuards without any trap overrides.

Parameters

• users: set of users participating in operations
• deposits: input values used for deposit operations
• adjustments: values used for mint / reap operations
• subjects: contextual inputs (e.g. precision, forced flags)
• max_depth: maximum sequence length to explore
• allowed_bps: maximum allowed drift in basis points (e.g. 10 = 0.10%, 100 = 1%)
• allowed_diff: maximum allowed absolute value difference (not percentage-based)
• results: mutable container collecting outcomes

Behavior

• generates operation sequences up to max_depth
• filters using BalanceGuards (guard(...))
• executes both lazy and manual models
• compares results and records:
• pass: valid execution
• fail: error
• exit: withdrawals drifts between balance models

This is the standard correctness check without testing invalid scenarios.

fn explore_traps( users: &[<Self::ManualBalance as ManualBalanceModel<Self::LazyBalance>>::User], deposits: &[<Self::LazyBalance as LazyBalance>::Asset], adjustments: &[<Self::LazyBalance as LazyBalance>::Asset], subjects: &[<Self::LazyBalance as LazyBalance>::Subject], max_depth: u32, allowed_bps: u32, allowed_diff: u32, traps: Option<BalanceTraps<Self::TrapFn, Self::FlowFn>>, results: &mut BalanceModelResults<Self::LazyBalance, Self::ManualBalance>, )

where <Self::LazyBalance as LazyBalance>::Id: Default, <Self::LazyBalance as LazyBalance>::Asset: From<<Self::LazyBalance as LazyBalance>::Asset> + Into<<Self::LazyBalance as LazyBalance>::Asset>,

Runs exploration with trap overrides (guard || trap).

Extends Self::explore by allowing controlled violations of guards using BalanceTraps.

Parameters

• users: set of users participating in operations
• deposits: input values used for deposit operations
• adjustments: values used for mint / reap operations
• subjects: contextual inputs (e.g. precision, forced flags)
• max_depth: maximum sequence length to explore
• allowed_bps: maximum allowed drift in basis points (e.g. 10 = 0.10%, 100 = 1%)
• allowed_diff: maximum allowed absolute value difference
• traps: optional trap configuration (trap, flow, reason)
• results: mutable container collecting outcomes

Behavior

• operations are allowed using:

guard(...) || trap(...)

• trap is applied globally to every operation:

  • should return true only for the intended operation(s)
  • should return false by default for all unrelated operations

• flow further filters exploration:

guard_flow(...) && trap_flow(...)

• should return true for the intended operation(s) or by default

• return false only to explicitly block exploration of a case

• typically used to:

  • force invalid transitions
  • trigger expected errors
  • validate edge-case behavior

• executes both lazy and manual models and records:

  • pass / fail / exit / trap outcomes

This is used for adversarial and trap-based testing.

fn explore_custom( users: &[<Self::ManualBalance as ManualBalanceModel<Self::LazyBalance>>::User], deposits: &[<Self::LazyBalance as LazyBalance>::Asset], adjustments: &[<Self::LazyBalance as LazyBalance>::Asset], subjects: &[<Self::LazyBalance as LazyBalance>::Subject], max_depth: u32, allowed_bps: u32, allowed_diff: u32, traps: Option<BalanceTraps<Self::TrapFn, Self::FlowFn>>, hasher: Option<Self::Hasher>, results: &mut BalanceModelResults<Self::LazyBalance, Self::ManualBalance>, )

where <Self::LazyBalance as LazyBalance>::Id: Default, <Self::LazyBalance as LazyBalance>::Asset: From<<Self::LazyBalance as LazyBalance>::Asset> + Into<<Self::LazyBalance as LazyBalance>::Asset>,

Runs full custom exploration (custom traps + optional additional hasher).

This is the most flexible entrypoint, allowing control over:

• trap behavior
• additional state hashing

Parameters

• users: set of users participating in operations
• deposits: input values used for deposit operations
• adjustments: values used for mint / reap operations
• subjects: contextual inputs (e.g. precision, forced flags)
• max_depth: maximum sequence length to explore
• allowed_bps: maximum allowed drift in basis points (e.g. 10 = 0.10%, 100 = 1%)
• allowed_diff: maximum allowed absolute value difference
• traps: optional trap configuration (guard || trap)
• hasher: optional additional state hasher (second-stage pruning)
• results: mutable container collecting outcomes

Behavior

• combines:

  • BalanceGuards -> base validity
  • BalanceTraps -> override (guard || trap)
  • flow -> exploration control (guard_flow && trap_flow)

• if hasher is provided:

  • used alongside BalanceStateHasher from Self::ManualBalance
  • enables additional state deduplication

• executes both lazy and manual models and records:

  • pass / fail / exit / trap outcomes

Use this when:

• testing complex trap scenarios
• adding custom state pruning logic
• requiring full control over exploration behavior

fn write_reports( dir: PathBuf, results: &BalanceModelResults<Self::LazyBalance, Self::ManualBalance>, write_pass: bool, write_exit: bool, write_trap: bool, )

Writes CSV reports for analysis.

Exports the contents of BalanceModelResults into CSV files under the given directory.

Parameters

• dir: output directory where CSV files will be created
• results: collected model checking results
• write_pass: whether to write successful sequences
• write_exit: whether to write drift cases (BalanceExit)
• write_trap: whether to write trapped sequences

Behavior

• always writes failures

• optionally writes:

  • pass: successful executions
  • exit: drift between lazy and manual models
  • trap: expected trap-triggered sequences

• file names are timestamped to avoid overwriting

• prints a summary of results after writing

Useful for:

• debugging failures
• analyzing drift behavior
• validating trap scenarios

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors