Module 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.

• Liveness — the schedule is unrolled into its event graph: one transition per executed op, one place per token (Data{buf,k} = the k-th page pushed, Space{buf,k} = the k-th reservation’s slot, returned by the pop depth pages earlier, Ready/Valid = the k-th round of a multicast semaphore pair, McastData = the k-th block landing at a receiver, Pc = program order). Every place has one producer and one consumer (a marked graph); by Commoner’s theorem the net is live iff every directed cycle carries a token, i.e. iff the token-free arcs form a DAG — the witness is a topological order of the transitions. A consumed place with neither a producer nor an initial token is a STARVED transition (a dropped increment, flag or pop) and earns no certificate.
• Bounds — per-buffer counting balance (reserve == push == pop over the run) and the evaluated high-water occupancy against the depth.
• PE datapaths — a SAT PlacementCertificate for every integer compute stage (psum + a·w at the 8-bit bound the fabric’s placer certification uses) and for ALU/select scalar bodies; float tensor datapaths are honestly Uncertified with the reason.
• Numerics — the exactness claim carried from the front end.

Structs

BufferBalance

ChoreographyCertificate

DeadlockNode

One transition in a token-free cycle: the op that waits, and the empty place it waits on.

LivenessWitness

MarkedGraph

Place

SectionProof

The liveness proof of ONE section: its graph’s shape, a digest that binds the witness to that exact graph, and the topological order over the section’s own transition numbering.

Transition

TripCase

★ ONE COUNT OF A TRIP, PROVED. The graph a part of the program unrolls to when each trip it runs to counts counts[i] (its trips in id order), carried like a section’s: its shape, its digest, and the witness-table entry that orders it. recheck rebuilds every one.

Enums

CertifyFault

ComputeStageCert

GraphProof

HOW THE LIVENESS PROOF IS CARRIED.

PlaceKind

Constants

SCALAR_DATAPATH_BUDGET_NODES

How large a datapath tree the scalar certificate will pay to build.

Functions

bounded_datapath_nodes

The BoundedExpr node count cells_to_bounded will materialise for body, computed from the cell DAG alone — one pass, no allocation, saturating so an astronomical body is priced rather than overflowing. Mirrors cells_to_bounded’s shapes exactly: an Arith cell is 1 + |a| + |b|, a Select is the comparison (1 + |ca| + |cb|) plus both arms plus the ite node, and a Val(k) operand costs a full copy of cell k.

build_marked_graph

Build the unrolled event graph of the whole schedule, every trip at its greatest count.

cells_to_bounded

Lower an ALU/select cell body to the bounded fragment (the placer’s own lowering vocabulary).

certifiable_operand

A precision’s role in a PE certificate (kept for lowerings that report it).

certify_choreography

certify_external_spatial

Import-and-certify at the spatial level: an EXTERNAL placement+schedule of the SAME computation as source earns a certificate iff it computes the same thing (structure and evaluation) and its choreography certifies. None is fail-closed.

decomposes_by_section

Does this choreography’s liveness proof decompose into one proof per section?

dry_inputs

Inputs for a dry run: deterministic fills where recorded, zeros for external data.

item_window

The item-loop window the event graph unrolls. Work items are rounds of one choreography whose state (FIFO occupancy, semaphore rounds) carries over with a dependence distance bounded by the deepest FIFO; the unrolled graph is periodic beyond that, so a token-free cycle exists in the full unrolling iff it exists within deepest FIFO + 2 consecutive rounds. Every engine of a site (and every member of a multicast group) loops the same count, so the cap keeps producer/consumer pairings consistent.

liveness_witness

Commoner’s condition on the unrolled net: a starved transition or a token-free cycle is a fault; else the topological order over token-free arcs is the witness.

scalar_certificate

The per-PE proof of a scalar ALU/select stage: the ROUTED grid proven equal to the body’s own datapath, for every 8-bit input, with the refutation kept.

scalar_certificate_within

scalar_certificate against an EXPLICIT gate ceiling — the seam a lock shrinks to prove the budget is live code and not a constant nobody reads.

schedule_digest

FNV-1a over the schedule’s serialization — binds a certificate to one choreography.

trip_window

★ THE TRIP WINDOW — A FEW COUNTS PROVE EVERY COUNT. A loop run to a trip unrolls to a different graph at each count, and a decode fold at a long context admits thousands of them. The certificate proves the counts lo ..= min(hi, max(lo, s + 1)), where s bounds how far, in rounds of the trip’s loops, one engine can run ahead of another it trades pages with — and that proves them all, by the shape the IR holds a trip loop to (a program input for its count, no semaphore or multicast in its body, no trip loop in another, every buffer it touches balanced per round — validate_trips and the per-round counting check): • per-round balance means advancing EVERY engine of a coupled set by one round leaves every buffer’s occupancy where it was; • so a stall with every engine of a set strictly inside its rounds cannot be the run’s final state — the same stall one round earlier is a smaller final state, and a marked graph has one; • a stall with an engine still at the start of its rounds has every engine of its set within s rounds of the start, and is the same stall at every count past s + 1: proved at s + 1, it is refused there; • a stall with an engine past its rounds has every engine within s rounds of the end, and the same stall one round shorter is a stall of the next count down — down to s + 1, which is proved. s is the most any path of per-round page traffic lets one engine lead another: over each set of engines that trade pages inside the trip’s loops, the sum of each such buffer’s depth, the pages it moves outside them, and one.