Module spatial 

The spatial IR — the one program every spatial backend lowers FROM.

A ir::SpatialProgram is a graph of stages (loads, stores, multicast receives, tile compute, scalar dataflow bodies) connected through bounded buffers by typed handshakes (FIFO, semaphore pair, barrier, valid/ready, token), placed onto a described mesh of sites (target::SpatialTarget) and choreographed by a per-engine schedule of ir::ChoreoOps. Its meaning is the executable token semantics in eval (the golden oracle every lowering is proven against), and every verified program carries a certificate::ChoreographyCertificate (deadlock-freedom + buffer bounds + per-PE SAT).

The stakeholder’s three words are three passes over this IR, never per-backend code: size_buffers (buffering), fuse_readers (reader fusion / multicast), synthesize_handshakes (semaphore choreography). A lowering reads only the IR and its target — the “choreography census” locks assert that every semaphore / circular buffer / kernel a backend emits is the image of an IR object.

A REWRITE of this IR — a pass, a legalization, an imported placement — is answerable to equiv::equivalent_under: two programs, one corpus, a typed equiv::Divergence when they part company. Structure is deliberately not consulted, because a legalization’s whole job is to change it.

Modules

certificate

ChoreographyCertificate — what a verified spatial program PROVES about itself, re-checkable by a checker that trusts only a ~100-line PR/RUP refutation checker, a ~40-line topological-order verifier, and integer arithmetic — never the passes that produced the schedule.

clock

════════════════════════════════════════════════════════════════════════════════════════════════ THE SPATIAL CLOCK — a period computed from the graph, not fitted to a counter.

cost

The calibrated cycle model — what makes “streamed vs multicast vs blocked” an EMERGENT plan decision.

d5005

The Intel PAC D5005: a Stratix 10 SX 2800 on four channels of DDR4, as a decode card.

decode

The cost of one token: batch-1 decode, priced on a machine from the checkpoint itself.

decode_chip

The decode chip — what an SRAM-resident LOGOS system must achieve to decode one user faster than GPUs can.

decode_engine

The LOGOS decode engine: a spatial dataflow on one card that holds its sequences’ token-rows on chip and streams the weights through them once a pass.

describe

describe — what a lowered program actually DOES, as facts derived from the IR.

equiv

equiv — the differential that decides whether two spatial programs MEAN the same thing.

eval

eval_choreography — the executable MEANING of a placed + scheduled spatial program.

fit

The fit report — what a model or a workload needs from an RDU, sized against ONE source of chip facts (RduChipFacts) and written down with every number labeled.

fpga_decode

A decode on one ZCU104: what the board holds, how fast its programmable logic reads it, and what a token of each checkpoint we have costs there.

handoff

What one chip hands another when they share a model’s work.

int8_model

An int8 transformer as a LOGOS decode step: one token in, its logits and the next token out, the KV cache carried.

ir

SpatialProgram — the spatial IR proper.

link

The spatial link: each op of the one IR that the shared optimizer leaves the spatial chips (super::shim::SpatialShim), as the section templates it composes from.

lower

The lowering seam: every backend is a pure function of a VERIFIED program and its target, and every construct it emits is the image of an IR object (the census bijection).

part

What a programmable part holds, as facts with sources: its logic, its flip-flops, its multipliers and every kind of on-chip memory it carries, counted the way its vendor’s data sheet counts them.

passes

The target-parametric passes: every one is fn(&SpatialProgram, &SpatialTarget) -> Result<SpatialProgram, SpatialReject>, reads only the program and the descriptor, and leaves validate() holding. The order is pinned in super::pipeline::PASS_ORDER. There is no strategy input anywhere: tile chooses the plan by the cost model, fuse_readers re-derives the same comparison, and every later pass is a function of the structure.

pipeline

The front-end bridge and the pinned pass order.

programs

programs — the LOGOS source of the reference programs the spatial lane is anchored on.

rdu_chip

RduChipFacts — ONE source of facts for the SambaNova RDU family, from which BOTH chip descriptors (the spatial mesh SpatialTarget and the scalar-fabric envelope FabricTarget) are derived.

residency

Residency — which tensors the SRAM holds, and what leaves the chip.

roofs

Roofs — the rates a chip sustains, each one cited: the roofline a program’s work is held against.

serving

The cost of a pass: batched, speculative decode on one card that holds its tokens and streams its weights.

shim

What the spatial chips run whole (CUDA persistent, Tensix, the RDU, the fabric): their answer to the shared optimizer.

streamed

A model as the RDU would run it: one lowered program per LAYER KIND, and a manifest.

target

SpatialTarget — the described MESH a spatial program is placed onto.

tensor_parallel

════════════════════════════════════════════════════════════════════════════════════════════════ TENSOR PARALLELISM FOR A WHOLE PROGRAM — Megatron over RDUs, as ONE spatial program.

value_range

Proven value ranges: the interval every integer tensor of a program holds over every run that meets the program’s preconditions — every gather’s index inside its table, every attention attending at least one position.

wide_int

64-bit integers on a chip whose integer lanes are 32 bits wide.

work

THE WORK MODEL — what a program makes the machine do, counted from the program itself.