Enum CertifyFault 

pub enum CertifyFault {
    NotScheduled,
    Invalid(IrViolation),
    Starved {
        transition: usize,
        place: PlaceKind,
    },
    Deadlock {
        cycle: Vec<DeadlockNode>,
    },
    Bounds {
        buffer: BufferId,
    },
    ActivationOrder {
        tensor: TensorId,
        writer: Option<usize>,
        reader: usize,
        reason: &'static str,
    },
    StateOrder {
        tensor: TensorId,
        reader: Option<usize>,
        writer: Option<usize>,
        reason: &'static str,
    },
    UnreducedShard {
        tensor: TensorId,
        chips: usize,
    },
    TripCasesExceed {
        limit: usize,
    },
    Eval(ChoreoFault),
}

Variants

NotScheduled

Invalid(IrViolation)

Starved

A transition consumes a place nobody produces and that carries no initial token.

Fields

transition: usize

place: PlaceKind

Deadlock

A token-free cycle: the ring of waits that could never all fire, each named by the op that waits and the place it waits on. A deadlock is only actionable if you can see WHICH hand-off closed the ring, so the fault carries the ring rather than an index list.

Fields

cycle: Vec<DeadlockNode>

Bounds

Fields

buffer: BufferId

ActivationOrder

An ACTIVATION is not ordered: the section that writes it is not strictly before every section that reads it, or a barrier between them is missing. Without that order the reader takes whatever is in the tensor, which on a hundred-section forward is the whole answer.

Fields

tensor: TensorId

writer: Option<usize>

reader: usize

reason: &'static str

StateOrder

STATE is not ordered: more than one section writes it, one section both reads and writes it, or a barrier between the reader and the writer is missing. Unlike an activation a state tensor is FULL at the start of a run, so an unordered read yields last step’s value instead of faulting — which is exactly the silent wrong answer this obligation exists to make impossible.

Fields

tensor: TensorId

reader: Option<usize>

writer: Option<usize>

reason: &'static str

UnreducedShard

A TENSOR-PARALLEL SHARD REACHES AN OUTPUT WITHOUT BEING SUMMED. Each chip of a row-parallel shard computes a partial over its slice of the contraction — correctly shaped, fully written, and missing every term the other chips hold. Nothing about that partial looks wrong: the program runs, the store lands, the run reports success, and the number is 1/chips of the answer. This is the one obligation that cannot be recovered by inspecting the output, which is why it is checked here.

Fields

tensor: TensorId

chips: usize

TripCasesExceed

A part of the program runs to trips whose windows multiply past what one proof may hold.

Fields

limit: usize

Eval(ChoreoFault)

Trait Implementations

impl Clone for CertifyFault

fn clone(&self) -> CertifyFault

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CertifyFault

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

Formats the value using the given formatter.

impl PartialEq for CertifyFault

fn eq(&self, other: &CertifyFault) -> 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 CertifyFault