Enum IrViolation 

pub enum IrViolation {
    IdNotDense {
        what: &'static str,
        index: usize,
    },
    DanglingTensor {
        stage: StageId,
        tensor: TensorId,
    },
    DanglingBuffer {
        stage: Option<StageId>,
        buffer: BufferId,
    },
    DanglingStage {
        edge: EdgeId,
        stage: StageId,
    },
    DanglingGroup {
        stage: StageId,
        group: GroupId,
    },
    DanglingSemaphore {
        sem: SemId,
    },
    DanglingItem {
        stage: StageId,
        item: WorkItemId,
    },
    EdgeBufferNotInStagePorts {
        edge: EdgeId,
        stage: StageId,
        buffer: BufferId,
    },
    FifoProducerCount {
        buffer: BufferId,
        count: usize,
    },
    FifoConsumerCount {
        buffer: BufferId,
        count: usize,
    },
    CarryWithoutInit {
        buffer: BufferId,
    },
    CarryUpdatedTwice {
        buffer: BufferId,
    },
    CarryInitMovesWithTheBlocks {
        buffer: BufferId,
    },
    CarryNotARing {
        buffer: BufferId,
    },
    LoadReadsOutput {
        stage: StageId,
        tensor: TensorId,
    },
    StoreWritesInput {
        stage: StageId,
        tensor: TensorId,
    },
    TileGridMismatch {
        tensor: TensorId,
    },
    OutputUncovered {
        tensor: TensorId,
        tile: usize,
    },
    OutputOverlap {
        tensor: TensorId,
        tile: usize,
    },
    OperandDtypeMismatch {
        stage: StageId,
        buffer: BufferId,
        expected: Precision,
        found: Precision,
    },
    IntermNarrowerThanAcc {
        stage: StageId,
        interm: BufferId,
        acc: AccPolicy,
        found: Precision,
    },
    AccTilesExceeded {
        stage: StageId,
        needed: usize,
        available: usize,
    },
    BlockDivisibility {
        what: &'static str,
        value: usize,
        divisor: usize,
    },
    GridMismatch {
        expected: (usize, usize),
        found: (usize, usize),
    },
    PhaseOrder {
        have: &'static str,
        missing: &'static str,
    },
    StageUnplaced {
        stage: StageId,
    },
    EngineRoleMismatch {
        stage: StageId,
    },
    EngineSiteMismatch {
        stage: StageId,
    },
    GroupMalformed {
        group: GroupId,
        reason: &'static str,
    },
    GroupMemberMismatch {
        group: GroupId,
        site: Site,
        reason: &'static str,
    },
    CrossSiteLocalEdge {
        edge: EdgeId,
    },
    LocalCrossSiteEdge {
        edge: EdgeId,
    },
    MemoryOverlap {
        site: Site,
        a: BufferId,
        b: BufferId,
    },
    MemoryUnmapped {
        buffer: BufferId,
    },
    DuplicateEngineProgram {
        site: Site,
        engine: Engine,
    },
    CountingImbalance {
        buffer: BufferId,
        reserved: u64,
        pushed: u64,
        popped: u64,
    },
    AccumulatorNeverComputed {
        site: Site,
        engine: Engine,
    },
    SemaphoreImbalance {
        sem: SemId,
        incs: u64,
        waits: u64,
    },
    SemaphoreNotReset {
        sem: SemId,
        waits: u64,
        resets: u64,
    },
    AccImbalance {
        site: Site,
        acquires: u64,
        releases: u64,
    },
    HandshakeNotRequired {
        kind: HandshakeKind,
    },
    ItemCountMismatch {
        group: GroupId,
    },
    StageNotScheduled {
        stage: StageId,
        op: &'static str,
    },
    GenericOperandCount {
        stage: StageId,
        operands: usize,
        maps: usize,
    },
    GenericOperandOutOfRange {
        stage: StageId,
        operand: usize,
        operands: usize,
    },
    ContractionMalformed {
        stage: StageId,
        reason: &'static str,
    },
    IndirectOperandOutOfRange {
        stage: StageId,
        operand: usize,
        operands: usize,
    },
    IndirectMalformed {
        stage: StageId,
        reason: &'static str,
    },
    TripMalformed {
        trip: TripId,
        reason: &'static str,
    },
    TripLoopMalformed {
        reason: &'static str,
    },
    IndirectOutWithoutScatter {
        stage: StageId,
    },
    IndirectIndexNotAnOperand {
        stage: StageId,
        buffer: BufferId,
    },
    ArgMaxOutputNotInteger {
        stage: StageId,
        found: Precision,
    },
    TensorRoleDeferred {
        tensor: TensorId,
        role: TensorRole,
        until: &'static str,
    },
    TensorSpaceDeferred {
        tensor: TensorId,
        space: TensorSpace,
        until: &'static str,
    },
    SectionSpanMalformed {
        section: usize,
        what: &'static str,
    },
    SectionBarrierUnbalanced {
        sem: SemId,
        participants: usize,
        sites: usize,
        incs: u64,
        wait_ops: u64,
    },
    SectionBarrierMisplaced {
        section: usize,
        site: Site,
        engine: Engine,
        what: &'static str,
    },
    SectionBufferEscape {
        stage: StageId,
        buffer: BufferId,
        stage_section: usize,
        buffer_section: usize,
    },
}

A structural invariant the program breaks. Every arm is a lock.

Variants

IdNotDense

Fields

what: &'static str

index: usize

DanglingTensor

Fields

stage: StageId

tensor: TensorId

DanglingBuffer

Fields

stage: Option<StageId>

buffer: BufferId

DanglingStage

Fields

edge: EdgeId

stage: StageId

DanglingGroup

Fields

stage: StageId

group: GroupId

DanglingSemaphore

Fields

sem: SemId

DanglingItem

Fields

stage: StageId

item: WorkItemId

EdgeBufferNotInStagePorts

Fields

edge: EdgeId

stage: StageId

buffer: BufferId

FifoProducerCount

Fields

buffer: BufferId

count: usize

FifoConsumerCount

Fields

buffer: BufferId

count: usize

CarryWithoutInit

A carried buffer — one stage reads and writes it — that no other stage writes first.

Fields

buffer: BufferId

CarryUpdatedTwice

A carried buffer more than one stage updates, or more than one stage initializes.

Fields

buffer: BufferId

CarryInitMovesWithTheBlocks

A carry’s init that reads a value moving with the K blocks: the first page would differ per block.

Fields

buffer: BufferId

CarryNotARing

A carry that is not a scratch ring of two pages — the value before a block’s update and the value after.

Fields

buffer: BufferId

LoadReadsOutput

Fields

stage: StageId

tensor: TensorId

StoreWritesInput

Fields

stage: StageId

tensor: TensorId

TileGridMismatch

Fields

tensor: TensorId

OutputUncovered

Fields

tensor: TensorId

tile: usize

OutputOverlap

Fields

tensor: TensorId

tile: usize

OperandDtypeMismatch

Fields

stage: StageId

buffer: BufferId

expected: Precision

found: Precision

IntermNarrowerThanAcc

Fields

stage: StageId

interm: BufferId

acc: AccPolicy

found: Precision

AccTilesExceeded

Fields

stage: StageId

needed: usize

available: usize

BlockDivisibility

Fields

what: &'static str

value: usize

divisor: usize

GridMismatch

Fields

expected: (usize, usize)

found: (usize, usize)

PhaseOrder

Fields

have: &'static str

missing: &'static str

StageUnplaced

Fields

stage: StageId

EngineRoleMismatch

Fields

stage: StageId

EngineSiteMismatch

Fields

stage: StageId

GroupMalformed

Fields

group: GroupId

reason: &'static str

GroupMemberMismatch

Fields

group: GroupId

site: Site

reason: &'static str

CrossSiteLocalEdge

Fields

edge: EdgeId

LocalCrossSiteEdge

Fields

edge: EdgeId

MemoryOverlap

Fields

site: Site

a: BufferId

b: BufferId

MemoryUnmapped

Fields

buffer: BufferId

DuplicateEngineProgram

Fields

site: Site

engine: Engine

CountingImbalance

Fields

buffer: BufferId

reserved: u64

pushed: u64

popped: u64

AccumulatorNeverComputed

An accumulator was acquired and packed with no compute in between (a skipped compute is never a legal choreography: the packed tiles would be whatever the register file held).

Fields

site: Site

engine: Engine

SemaphoreImbalance

Fields

sem: SemId

incs: u64

waits: u64

SemaphoreNotReset

A counting semaphore was waited on without being put back to zero for the next round — the next wait would be satisfied by a count that has already been consumed.

Fields

sem: SemId

waits: u64

resets: u64

AccImbalance

Fields

site: Site

acquires: u64

releases: u64

HandshakeNotRequired

Fields

kind: HandshakeKind

ItemCountMismatch

Fields

group: GroupId

StageNotScheduled

A stage the output-coverage proof credits issues no data movement in the schedule. Coverage is proven over the WORK LIST; the schedule is what runs.

Fields

stage: StageId

op: &'static str

GenericOperandCount

A Generic whose access maps do not match its operands one for one.

Fields

stage: StageId

operands: usize

maps: usize

GenericOperandOutOfRange

A Generic body (or a predicate’s bound) naming an operand the stage does not have — the evaluator indexes pages by it, and a panic there is not a refusal.

Fields

stage: StageId

operand: usize

operands: usize

ContractionMalformed

A Generic whose contraction axis — the third iteration variable, LV_GEN_K — is malformed: not a sum fold, over another variable, stepped along by the output or by a map in a space without it, or a fourth axis.

Fields

stage: StageId

reason: &'static str

IndirectOperandOutOfRange

An indirect term whose index operand the stage does not have.

Fields

stage: StageId

operand: usize

operands: usize

IndirectMalformed

An indirect term or tile with a field that cannot mean anything (a zero modulus or stride, an inverted bound).

Fields

stage: StageId

reason: &'static str

TripMalformed

A trip that cannot count anything: read from what is not a program input or past its tensor, an empty or zero-based range, a zero divisor, or a trip no loop runs to.

Fields

trip: TripId

reason: &'static str

TripLoopMalformed

A loop that misuses a trip: runs to one the program does not declare, is bounded apart from it, nests inside another trip loop, or holds a semaphore or multicast op — the forms the certificate’s trip window (crate::spatial::certificate::trip_window) does not cover.

Fields

reason: &'static str

IndirectOutWithoutScatter

An OUTPUT map with an indirect term — a scatter — on a stage whose result reaches no Store with an indirect tile address to scatter through.

Fields

stage: StageId

IndirectIndexNotAnOperand

An indirect tile address whose index buffer is not one of the stage’s operands.

Fields

stage: StageId

buffer: BufferId

ArgMaxOutputNotInteger

An index-valued (ArgMax) reduction packed into a non-integer buffer.

Fields

stage: StageId

found: Precision

TensorRoleDeferred

A tensor role used outside the contract that gives it meaning; until names the phase that owns that contract (B-P7 sections for an activation, B-P6 the cross-token carry for state).

Fields

tensor: TensorId

role: TensorRole

until: &'static str

TensorSpaceDeferred

A tensor space used outside the contract that gives it meaning; until names the phase.

Fields

tensor: TensorId

space: TensorSpace

until: &'static str

SectionSpanMalformed

A section span that is not a scope: an id range that overlaps its neighbour, runs backwards, or leaves part of an id space in no section at all.

Fields

section: usize

what: &'static str

SectionBarrierUnbalanced

A section boundary whose barrier is not a rendezvous: the participants that post it and the engine programs that wait on it disagree.

Fields

sem: SemId

participants: usize

sites: usize

incs: u64

wait_ops: u64

SectionBarrierMisplaced

A rendezvous op that does not sit on its section boundary in one engine program, so the barrier balances but does not order that program’s work.

Fields

section: usize

site: Site

engine: Engine

what: &'static str

SectionBufferEscape

A stage of one section reads or writes a buffer that belongs to another — sections share tensors, never local memory.

Fields

stage: StageId

buffer: BufferId

stage_section: usize

buffer_section: usize

Trait Implementations

impl Clone for IrViolation

fn clone(&self) -> IrViolation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IrViolation

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

Formats the value using the given formatter.

impl From<IrViolation> for ComposeReject

fn from(v: IrViolation) -> Self

Converts to this type from the input type.

impl From<IrViolation> for SpatialReject

fn from(v: IrViolation) -> Self

Converts to this type from the input type.

impl PartialEq for IrViolation

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

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for IrViolation

impl StructuralPartialEq for IrViolation