Enum CreditError 

pub enum CreditError {
    SendAtZero {
        payload: Payload,
    },
    BurstOverflow {
        payload: Payload,
        budget: u64,
        burst: u64,
    },
    LoopUnsustainable {
        sends_per_iter: u64,
        recvs_per_iter: u64,
    },
}

The Presburger discharge’s negative verdict — the witness of an unconformant credit constraint. Surfaced verbatim by the type checker.

Variants

SendAtZero

An explicit !⁰A.S — the “no rule at n=0” axiom rejects it.

Fields

payload: Payload

BurstOverflow

A straight-line send burst exceeds the budget k: at the offending send the abstract credit window would fall below 0.

Fields

payload: Payload

budget: u64

burst: u64

LoopUnsustainable

A recursive body has Δ > 0 (per iteration drains the window): no finite budget makes unbounded iteration sound.

Fields

sends_per_iter: u64

recvs_per_iter: u64

Trait Implementations

impl Clone for CreditError

fn clone(&self) -> CreditError

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for CreditError

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Display for CreditError

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Eq for CreditError

impl PartialEq for CreditError

fn eq(&self, other: &CreditError) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for CreditError