Module clock 

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

A spatial program has no meaningful global clock. Sixty-four sites run concurrently, each engine advances when its inputs are present, and “how long does it take” is not a property any one of them holds. Asking a simulator for a cycle count answers a different question — ttsim’s counter advances once per simulated clock while it steps the RV32 cores, so a 4x deeper reduction moves it by one cycle (benchmarks/silicon/ttsim_instrument_audit.json).

But the choreography is not an arbitrary concurrent program. certificate already proves it is a Petri MARKED GRAPH — every place has exactly one producer and one consumer — and certifies its liveness by Commoner’s theorem. Marked graphs have a classical and exact steady-state result: the system settles into a period equal to the maximum cycle mean

    Π  =  max over directed cycles C of   ( Σ delay(t) for t ∈ C ) / ( Σ tokens(p) for p ∈ C )

That is the spatial clock. It is a THEOREM about the graph the compiler already builds and already proves live, evaluated at per-transition delays that are architectural facts — a DRAM tile’s bandwidth occupancy, an engine’s issue rate — rather than regression coefficients. Nothing here is fitted, so nothing here can be corrupted by a counter that cannot see work.

It also EXPLAINS itself: the cycle that attains the maximum is the critical cycle, and it names the exact chain of events that sets the period. “Bound on DRAM bandwidth” is a summary; the critical cycle is the evidence. ════════════════════════════════════════════════════════════════════════════════════════════════

Structs

Period

The steady-state period of a marked graph, with the cycle that attains it.

Functions

cycle_period

The spatial clock. The maximum cycle mean of g under delay, by parametric search: for a candidate period λ, give each edge the weight delay(producer) − λ·tokens. A positive-weight cycle exists exactly when some cycle’s mean exceeds λ, so Bellman-Ford’s longest-path relaxation decides the comparison and bisection converges on Π.