Compute

A surprising amount of low-level computing is circular: ring buffers wrap, work queues round-robin, and array layouts tile by a fixed stride. This page shows how the S1 vocabulary makes those patterns checkable — you can prove the addressing is safe, even though you cannot prove it is fast.

Lesson Goal

See four computing patterns — circular buffers, direction bins, stride layouts, and round-robin schedules — as finite circles, and understand exactly what “proved” buys you here (address safety and closure) versus what it does not (speed).

The Idea

Each pattern is a circle C_n with a stride:

A ring buffer of size n: writing at position i lands at i mod n.
Direction bins: a ray’s index lands in one of n bins.
A stride layout: element k lands at (k · stride) mod n.
A round-robin schedule: task t goes to worker t mod n.

The proved seed says the address wraps correctly and closes after a full pass. That is real — off-by-one and overflow bugs are exactly what it rules out. It says nothing about cache locality or throughput; those are benchmark questions.

Two honest tiers, as everywhere in the applications. The COMP* theorems themselves (an index stays in range, closes after a full pass, normalizes idempotently) are elementary modular-index bookkeeping — the same finite-closure family as the cyclic-memory facts in the AI lane. They are honest and useful, but not deep. The one genuinely non-trivial structural fact here is coverage: a stride layout visits every cell iff the stride is coprime to n — which is not a separate result but the very same proved coverage rule as strided attention, AIT-T0002. That is where the orbit/gcd theory does real work.

Worked Example

A ring buffer of size 8, writing a stream of indices:

write 6  -> slot 6 mod 8 = 6
write 13 -> slot 13 mod 8 = 5
write 16 -> slot 16 mod 8 = 0   (back to the start: one full lap)

And a round-robin over 4 workers:

task 6 -> worker 6 mod 4 = 2
task 7 -> worker 7 mod 4 = 3
task 8 -> worker 8 mod 4 = 0   (the schedule closes and repeats)

Both are just C_n rotation. The closure facts (adding a full size changes nothing) are what the cards below certify.

Common Mistake

Proving an address wraps correctly is not proving a kernel is fast. The CoilLayout/stencil fixtures (COMPL-B0001, COMPL-B0002) are executable references for expected outputs — they are not performance claims, and they do not prove cache locality, stencil correctness, or backend speed. See What “Proved” Means Here.

Checkpoint

In a ring buffer of size 8, where does write 20 land, and after how many more writes does the slot return to that position? (Answer: slot 4; every 8 writes.)

Source Trail

Showcase evidence: SHOW-011 circular compute layouts and schedules.

Proof-carrying compute paper: Circular Computation

Layout paper: Coil Layout, Stencil, And NTT