Trait BalanceGuards

Source

pub trait BalanceGuards<T: LazyBalanceMarker, M: ManualBalanceModel<T>> {
    // Provided methods
    fn deposit(
        _state: &BalanceState<T, M>,
        _user: &M::User,
        _amount: &T::Asset,
        _subject: &T::Subject,
    ) -> bool { ... }
    fn withdraw(_state: &BalanceState<T, M>, _user: &M::User) -> bool { ... }
    fn mint(
        _state: &BalanceState<T, M>,
        _value: &T::Asset,
        _subject: &T::Subject,
    ) -> bool { ... }
    fn reap(
        _state: &BalanceState<T, M>,
        _value: &T::Asset,
        _subject: &T::Subject,
    ) -> bool { ... }
    fn drain(_state: &BalanceState<T, M>) -> bool { ... }
    fn flow(_state: &BalanceState<T, M>, _next: &BalanceOp<T, M>) -> bool { ... }
    fn invariant(_state: &BalanceState<T, M>) -> Result<(), String> { ... }
}

Expand description

Defines validity checks for operations during state exploration.

Each method determines whether a candidate operation (BalanceOp) can be appended to the current trace, i.e., whether the next step in the sequence is valid given the current state.

A sequence is an ordered list of operations (Vec<BalanceOp>) being explored.
The trace is the current prefix of that sequence already applied to reach the current BalanceState.

Each guard method receives the current state (derived from the trace) and the inputs of the next operation, and returns:

true: operation is allowed
false: operation is disallowed (guarded)

During execution, an operation (BalanceOp) is permitted if:

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

guard(...) is the normal allow/disallow check (this trait)
BalanceTraps may override and allow a disallowed operation

§Flow

flow is an additional filter applied after guards:

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

Both must return true for the operation to proceed
Unlike guards, flow is combined (&&), not overridden
Used only to control exploration, not correctness

§Invariant

invariant must hold for every state reached via the trace evaluated at each step

§Example

trace:   [Deposit(A, 100)]
next:    Withdraw(A)

guard_withdraw(state, A) = true -> allowed (valid transition)

--------

trace:   []
next:    Withdraw(A)

guard_withdraw(state, A) = false -> disallowed (no receipt)

trap_override(...) = true -> allowed (forced invalid case for testing)

flow(...) = false -> blocked regardless of guard/trap

BalanceGuards should only express validity conditions for extending the sequence. They should not include exploration logic or testing behavior.

Provided Methods§

Source

fn deposit( _state: &BalanceState<T, M>, _user: &M::User, _amount: &T::Asset, _subject: &T::Subject, ) -> bool

Returns true if BalanceOp::Deposit is allowed to be appended to the current trace, given the current state and inputs.