6. The Edge of the Chip
Every mosaic so far lived on one piece of silicon, where a strap is a handful of wires between neighbouring elements. But chips end. A mosaic that matters will span packages: several small chips on a board, each carrying a few tesserae, joined by a couple of pins per direction. Words that crossed a strap in one cycle must now be serialised down a wire, bit by bit, and acknowledged on the way back — tens of cycles instead of one.
The specification chapter made a bold promise about this:
Mesh semantics are invariant under link serialization — the mosaic does
not care where the chip edge is.
This chapter pays the core of that promise. We model the serialised link — any serialised link, of any latency — and prove that through the right lens it is a strap: same pushes, same pops, same contents, with the extra cycles invisible except as waiting. The strap discipline was designed for exactly this moment: nothing about hold-until-pop ever mentioned time, so stretching time cannot break it.
6.1. The link, as a state machine
A stop-and-wait link has four moods. It is idle (empty, willing to accept a word); it is sending (a word is crossing the wire, some cycles remain); it is waiting (the word has arrived and sits in the far-side mailbox until the consumer takes it); or it is acking (the acknowledgement is returning, after which the producer may send again). We make the four moods the four constructors of the state — the word in flight lives inside the state, so no separate bookkeeping can disagree with it.
namespace Tilessa
/-- A stop-and-wait serialised link. `sending`/`acking` carry a countdown
of remaining wire cycles; the latency is arbitrary. -/
inductive EdgeLink (w : Nat) where
| idle
| sending (v : BitVec w) (left : Nat)
| waiting (v : BitVec w)
| acking (left : Nat)
deriving Repr, DecidableEq
namespace EdgeLink
/-- The producer may push only when the link is idle. -/
def canPush {w : Nat} : EdgeLink w → Bool
| .idle => true
| _ => false
/-- What the consumer's side sees: a word, once it has fully arrived. -/
def peek {w : Nat} : EdgeLink w → Option (BitVec w)
| .waiting v => some v
| _ => none
/-- Accept a word for transmission (`K` = wire cycles to cross). -/
def push {w : Nat} (K : Nat) (l : EdgeLink w) (v : BitVec w) : EdgeLink w :=
match l with
| .idle => .sending v K
| s => s
/-- The consumer takes the delivered word; the acknowledgement starts
back (`K'` = wire cycles to return). -/
def pop {w : Nat} (K' : Nat) : EdgeLink w → EdgeLink w
| .waiting _ => .acking K'
| s => s
/-- One clock cycle of the wire itself. -/
def tick {w : Nat} : EdgeLink w → EdgeLink w
| .sending v 0 => .waiting v
| .sending v (n + 1) => .sending v n
| .acking 0 => .idle
| .acking (n + 1) => .acking n
| s => s
6.2. The lens
Which strap does a link state depict? Read the logical mailbox off the mood: a word committed to the wire — still flying, or delivered and unclaimed — is in the mailbox; once popped, the mailbox is empty, even while the acknowledgement is still travelling (the producer just cannot refill quite yet — a delay, not a difference).
/-- The strap a link state depicts. -/
def abs {w : Nat} : EdgeLink w → Strap w
| .idle => {}
| .sending v _ => { q := some v }
| .waiting v => { q := some v }
| .acking _ => {}
6.3. The invariance theorems
Five facts say that, through the lens, the link behaves as the strap. The wire's own activity is invisible; a permitted push is a strap push; a delivered word is the strap's word; taking it is a strap pop; and the link is never more permissive than the strap — only slower.
/-- Time on the wire is invisible through the lens. -/
theorem abs_tick {w : Nat} (l : EdgeLink w) :
(tick l).abs = l.abs := w:Natl:EdgeLink w⊢ l.tick.abs = l.abs
cases l with
w:Nat⊢ idle.tick.abs = idle.abs All goals completed! 🐙
w:Natv:BitVec w⊢ (waiting v).tick.abs = (waiting v).abs All goals completed! 🐙
w:Natv:BitVec wleft:Nat⊢ (sending v left).tick.abs = (sending v left).abs w:Natv:BitVec w⊢ (sending v 0).tick.abs = (sending v 0).absw:Natv:BitVec wn✝:Nat⊢ (sending v (n✝ + 1)).tick.abs = (sending v (n✝ + 1)).abs w:Natv:BitVec w⊢ (sending v 0).tick.abs = (sending v 0).absw:Natv:BitVec wn✝:Nat⊢ (sending v (n✝ + 1)).tick.abs = (sending v (n✝ + 1)).abs All goals completed! 🐙
w:Natleft:Nat⊢ (acking left).tick.abs = (acking left).abs w:Nat⊢ (acking 0).tick.abs = (acking 0).absw:Natn✝:Nat⊢ (acking (n✝ + 1)).tick.abs = (acking (n✝ + 1)).abs w:Nat⊢ (acking 0).tick.abs = (acking 0).absw:Natn✝:Nat⊢ (acking (n✝ + 1)).tick.abs = (acking (n✝ + 1)).abs All goals completed! 🐙
/-- If the link accepts a push, so would the strap. -/
theorem canPush_abs {w : Nat} (l : EdgeLink w)
(h : l.canPush = true) : l.abs.canPush = true := w:Natl:EdgeLink wh:l.canPush = true⊢ l.abs.canPush = true
w:Nath:idle.canPush = true⊢ idle.abs.canPush = truew:Natv✝:BitVec wleft✝:Nath:(sending v✝ left✝).canPush = true⊢ (sending v✝ left✝).abs.canPush = truew:Natv✝:BitVec wh:(waiting v✝).canPush = true⊢ (waiting v✝).abs.canPush = truew:Natleft✝:Nath:(acking left✝).canPush = true⊢ (acking left✝).abs.canPush = true w:Nath:idle.canPush = true⊢ idle.abs.canPush = truew:Natv✝:BitVec wleft✝:Nath:(sending v✝ left✝).canPush = true⊢ (sending v✝ left✝).abs.canPush = truew:Natv✝:BitVec wh:(waiting v✝).canPush = true⊢ (waiting v✝).abs.canPush = truew:Natleft✝:Nath:(acking left✝).canPush = true⊢ (acking left✝).abs.canPush = true All goals completed! 🐙
/-- A permitted push is exactly a strap push. -/
theorem abs_push {w : Nat} (K : Nat) (l : EdgeLink w)
(v : BitVec w) (h : l.canPush = true) :
(push K l v).abs = l.abs.push v := w:NatK:Natl:EdgeLink wv:BitVec wh:l.canPush = true⊢ (push K l v).abs = l.abs.push v
w:NatK:Natv:BitVec wh:idle.canPush = true⊢ (push K idle v).abs = idle.abs.push vw:NatK:Natv:BitVec wv✝:BitVec wleft✝:Nath:(sending v✝ left✝).canPush = true⊢ (push K (sending v✝ left✝) v).abs = (sending v✝ left✝).abs.push vw:NatK:Natv:BitVec wv✝:BitVec wh:(waiting v✝).canPush = true⊢ (push K (waiting v✝) v).abs = (waiting v✝).abs.push vw:NatK:Natv:BitVec wleft✝:Nath:(acking left✝).canPush = true⊢ (push K (acking left✝) v).abs = (acking left✝).abs.push v w:NatK:Natv:BitVec wh:idle.canPush = true⊢ (push K idle v).abs = idle.abs.push vw:NatK:Natv:BitVec wv✝:BitVec wleft✝:Nath:(sending v✝ left✝).canPush = true⊢ (push K (sending v✝ left✝) v).abs = (sending v✝ left✝).abs.push vw:NatK:Natv:BitVec wv✝:BitVec wh:(waiting v✝).canPush = true⊢ (push K (waiting v✝) v).abs = (waiting v✝).abs.push vw:NatK:Natv:BitVec wleft✝:Nath:(acking left✝).canPush = true⊢ (push K (acking left✝) v).abs = (acking left✝).abs.push v All goals completed! 🐙
/-- A delivered word is the strap's word — the consumer never sees
anything the strap would not show. -/
theorem peek_abs {w : Nat} (l : EdgeLink w) (v : BitVec w)
(h : l.peek = some v) : l.abs.q = some v := w:Natl:EdgeLink wv:BitVec wh:l.peek = some v⊢ l.abs.q = some v
w:Natv:BitVec wh:idle.peek = some v⊢ idle.abs.q = some vw:Natv:BitVec wv✝:BitVec wleft✝:Nath:(sending v✝ left✝).peek = some v⊢ (sending v✝ left✝).abs.q = some vw:Natv:BitVec wv✝:BitVec wh:(waiting v✝).peek = some v⊢ (waiting v✝).abs.q = some vw:Natv:BitVec wleft✝:Nath:(acking left✝).peek = some v⊢ (acking left✝).abs.q = some v w:Natv:BitVec wh:idle.peek = some v⊢ idle.abs.q = some vw:Natv:BitVec wv✝:BitVec wleft✝:Nath:(sending v✝ left✝).peek = some v⊢ (sending v✝ left✝).abs.q = some vw:Natv:BitVec wv✝:BitVec wh:(waiting v✝).peek = some v⊢ (waiting v✝).abs.q = some vw:Natv:BitVec wleft✝:Nath:(acking left✝).peek = some v⊢ (acking left✝).abs.q = some v All goals completed! 🐙
/-- Taking a delivered word is exactly a strap pop. -/
theorem abs_pop {w : Nat} (K' : Nat) (l : EdgeLink w)
(h : l.peek.isSome) : (pop K' l).abs = l.abs.pop := w:NatK':Natl:EdgeLink wh:l.peek.isSome = true⊢ (pop K' l).abs = l.abs.pop
w:NatK':Nath:idle.peek.isSome = true⊢ (pop K' idle).abs = idle.abs.popw:NatK':Natv✝:BitVec wleft✝:Nath:(sending v✝ left✝).peek.isSome = true⊢ (pop K' (sending v✝ left✝)).abs = (sending v✝ left✝).abs.popw:NatK':Natv✝:BitVec wh:(waiting v✝).peek.isSome = true⊢ (pop K' (waiting v✝)).abs = (waiting v✝).abs.popw:NatK':Natleft✝:Nath:(acking left✝).peek.isSome = true⊢ (pop K' (acking left✝)).abs = (acking left✝).abs.pop w:NatK':Nath:idle.peek.isSome = true⊢ (pop K' idle).abs = idle.abs.popw:NatK':Natv✝:BitVec wleft✝:Nath:(sending v✝ left✝).peek.isSome = true⊢ (pop K' (sending v✝ left✝)).abs = (sending v✝ left✝).abs.popw:NatK':Natv✝:BitVec wh:(waiting v✝).peek.isSome = true⊢ (pop K' (waiting v✝)).abs = (waiting v✝).abs.popw:NatK':Natleft✝:Nath:(acking left✝).peek.isSome = true⊢ (pop K' (acking left✝)).abs = (acking left✝).abs.pop All goals completed! 🐙
Read together: any sequence of pushes, pops, and wire cycles on the link
projects, through abs, to the same sequence of pushes and pops on a
strap, with the ticks erased. An element wired to an EdgeLink stalls
where it would not have stalled on a strap — and stalling is precisely
the stutter that the pipeline chapter's refinement theorem, and the mesh
chapter's conservation theorems, already tolerate everywhere. The
latency K appears in no theorem's conclusion: two wire cycles or two
thousand, same mosaic.
And the wire really does deliver — here is a word crossing a 66-cycle link (a 64-bit word plus framing on a 2-wire serial line), checked by running the state machine during the build:
/-- Let the wire run for `n` cycles. -/
def ticks {w : Nat} : Nat → EdgeLink w → EdgeLink w
| 0, l => l
| n + 1, l => ticks n (tick l)
example :
(ticks 67 (push 66 .idle (42 : BitVec 64))).peek = some 42 := ⊢ (ticks 67 (push 66 idle 42)).peek = some 42
All goals completed! 🐙
example :
(ticks 67 (push 66 .idle (42 : BitVec 64))).abs.q = some 42 := ⊢ (ticks 67 (push 66 idle 42)).abs.q = some 42
All goals completed! 🐙
6.4. What remains
The lens argument is the load-bearing wall; one wall is not yet the house. The full statement — an entire mosaic with some straps replaced by links, proved equivalent as a whole to the all-strap mosaic — needs the mesh step generalised over anything with this push/pop/peek/tick interface, and a stuttering simulation assembled from the five lemmas above, element by element. That assembly is bookkeeping rather than insight, and it is queued; the insight is on this page. Nothing about a mailbox ever depended on where its two ends live.
end EdgeLink
end Tilessa