Trait ManualBalanceModel

pub trait ManualBalanceModel<T>: Clone + Debug
where
    T: LazyBalanceMarker,
{
    type User: Sortable + Hash + Copy;
    type Error: Debug + Clone + 'static;

    // Required methods
    fn new() -> Self;
    fn deposit(
        &mut self,
        user: Self::User,
        amount: T::Asset,
        lazy_result: &(T::Asset, T::Receipt),
    ) -> Result<(), Self::Error>;
    fn withdraw(
        &mut self,
        user: Self::User,
        lazy_result: &T::Asset,
    ) -> Result<T::Asset, Self::Error>;
    fn mint(
        &mut self,
        amount: T::Asset,
        lazy_result: &T::Asset,
    ) -> Result<(), Self::Error>;
    fn reap(
        &mut self,
        amount: T::Asset,
        lazy_result: &T::Asset,
    ) -> Result<(), Self::Error>;
    fn drain(&mut self) -> Result<(), Self::Error>;
    fn total(&self) -> T::Asset;
}

A user-indexed eager balance model over a LazyBalance system, primarily intended for testing and validation.

This model consumes the resolved outputs of lazy balance operations (lazy_result) and maintains a concrete, user-facing state without any deferred semantics (no receipts, no lazy evaluation).

Unlike LazyBalance, implementations are free to use the simplest possible accounting logic (e.g., a single global state machine or direct user balances), as correctness is derived from the provided results rather than internal computation.

It is not a source of truth and must remain consistent with the underlying LazyBalance execution.

This makes it suitable as a reference model for:

• validating lazy execution behavior
• testing invariants and edge cases
• comparing expected vs actual outcomes

Required Associated Types

type User: Sortable + Hash + Copy

Simple user identifier type for the model.

type Error: Debug + Clone + 'static

Error type returned by model operations.

Required Methods

fn new() -> Self

Creates a new instance with an empty manual balance state.

fn deposit( &mut self, user: Self::User, amount: T::Asset, lazy_result: &(T::Asset, T::Receipt), ) -> Result<(), Self::Error>

Applies a deposit for user.

amount is the requested input. The lazy model is assumed to have been executed with the same inputs, and lazy_result contains its resolved output:

• actual deposited value
• corresponding receipt

This method consumes that result to update the manual balance state.

fn withdraw( &mut self, user: Self::User, lazy_result: &T::Asset, ) -> Result<T::Asset, Self::Error>

Applies a withdrawal for user.

The lazy model is assumed to have been executed with the same inputs, and lazy_result contains the resolved asset produced by that withdrawal.

This method consumes that result to update the manual balance state.

Returns the withdrawn amount.

fn mint( &mut self, amount: T::Asset, lazy_result: &T::Asset, ) -> Result<(), Self::Error>

Applies a mint operation.

The lazy model is assumed to have been executed with the same input, and lazy_result contains the resolved asset produced by that mint.

This method consumes that result to update the manual balance state.

fn reap( &mut self, amount: T::Asset, lazy_result: &T::Asset, ) -> Result<(), Self::Error>

Applies a reap operation.

The lazy model is assumed to have been executed with the same input, and lazy_result contains the resolved asset produced by that reap.

This method consumes that result to update the manual balance state.

fn drain(&mut self) -> Result<(), Self::Error>

Applies a drain (full reap), resetting the manual balance state.

Brings the model into a fully drained state, consistent with a corresponding lazy balance drain operation.

fn total(&self) -> T::Asset

Returns the total aggregated value tracked by the model.

This is a utility method for external use and is not used by the model checker during exploration.

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