10. 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.
10.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
10.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 _ => {}
10.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! 🐙
And not only at 66 cycles: any latency delivers, proved once and for all rather than checked at a value.
/-- A word committed to a `sending` link with `n` cycles left is delivered
(`waiting`) after exactly `n + 1` wire cycles. -/
theorem sending_delivers {w : Nat} (n : Nat) (v : BitVec w) :
ticks (n + 1) (EdgeLink.sending v n) = EdgeLink.waiting v := w:Natn:Natv:BitVec w⊢ ticks (n + 1) (sending v n) = waiting v
induction n with
w:Natv:BitVec w⊢ ticks (0 + 1) (sending v 0) = waiting v All goals completed! 🐙
w:Natv:BitVec wn:Natih:ticks (n + 1) (sending v n) = waiting v⊢ ticks (n + 1 + 1) (sending v (n + 1)) = waiting v All goals completed! 🐙
/-- **Liveness: the wire always delivers.** A word pushed onto an idle link of
*any* latency `K` is delivered after `K + 1` cycles — the latency appears in
the count of waiting cycles and nowhere else. -/
theorem link_delivers {w : Nat} (K : Nat) (v : BitVec w) :
(ticks (K + 1) (push K EdgeLink.idle v)).peek = some v := w:NatK:Natv:BitVec w⊢ (ticks (K + 1) (push K idle v)).peek = some v
w:NatK:Natv:BitVec w⊢ (waiting v).peek = some v
All goals completed! 🐙
10.4. The assembly
The lens lemmas are the bricks; now we lay them into a wall. We build a whole mosaic whose every outgoing mailbox is a serialised link rather than a strap, define one clock cycle for it, and prove — element by element, mailbox by mailbox — that through the lens it behaves exactly as the all-strap mosaic did, with the wire latency showing up only as waiting.
First the serialised mosaic, and the lens that reads it back as an ordinary one. An element sends where its own link is idle; its inbox is whatever its neighbour has delivered — the peeked word, never the one still in flight.
end EdgeLink
open EdgeLink
/-- A mosaic whose outgoing mailboxes are serialised links, not straps. -/
structure LinkMesh (ι : Type) (cfg : CoreConfig) where
elem : ι → State cfg
halted : ι → Bool
link : ι → Dir → EdgeLink cfg.wordBits
/-- The strap-mosaic a link-mosaic depicts: read each mailbox through `abs`. -/
def LinkMesh.abs {ι : Type} {cfg : CoreConfig} (lm : LinkMesh ι cfg) :
MeshState ι cfg where
elem := lm.elem
halted := lm.halted
strap := fun i d => (lm.link i d).abs
/-- What element `i` sees over links. -/
def linkEnv {ι : Type} (w : Wiring ι) {cfg : CoreConfig}
(lm : LinkMesh ι cfg) (i : ι) : MeshIn cfg.wordBits where
canSend d := (lm.link i d).canPush
inbox d := (lm.link (w.next i d) (Dir.opp d)).peek
def lElemResult {ι : Type} (w : Wiring ι) {cfg : CoreConfig}
(progs : ι → Program) (lm : LinkMesh ι cfg) (i : ι) : StepResult cfg :=
if lm.halted i then .stall
else step cfg (progs i) (linkEnv w lm i) (lm.elem i)
/-- One clock of the link-mosaic: every non-halted element steps over its link
environment; then every link accepts its owner's push or serves its consumer's
pop, and the wire advances one cycle. `K`/`K'` are the send/ack latencies —
arbitrary, and (the theorems will show) invisible. -/
def lstep {ι : Type} (K K' : Nat) (w : Wiring ι) {cfg : CoreConfig}
(progs : ι → Program) (lm : LinkMesh ι cfg) : LinkMesh ι cfg :=
let res := lElemResult w progs lm
{ elem := fun i =>
match res i with
| .next s _ => s
| _ => lm.elem i
halted := fun i =>
lm.halted i ||
match res i with
| .halt => true
| _ => false
link := fun i d =>
let pushed : Option (BitVec cfg.wordBits) :=
match res i with
| .next _ out =>
match out.push with
| some (d', v) => if d' = d then some v else none
| none => none
| _ => none
let popped : Bool :=
match res (w.next i d) with
| .next _ out => out.pop = some (Dir.opp d)
| _ => false
let base : EdgeLink cfg.wordBits :=
match pushed with
| some v => (lm.link i d).push K v
| none => if popped then (lm.link i d).pop K' else lm.link i d
base.tick }
/-- A wiring is well-formed when the consumer of `i`'s `d`-link reads exactly
that link back. Every physical wiring — the torus, a ring, the pair harness —
satisfies it. -/
def Wiring.involutive {ι : Type} (w : Wiring ι) : Prop :=
∀ i d, w.next (w.next i d) (Dir.opp d) = i
Now the guarantees. Two say nothing is ever lost or invented; three say the
mailboxes are faithful — a sent word appears at once, a taken word clears at
once, and the wire's own churn between those events is invisible. Each is proved
for any mosaic, any wiring, any latency; K never reaches a conclusion.
/-- **Element governance.** Each cycle, every element either idles or advances
by exactly one `step` — the instruction set. Serialising links changes *when*
an element steps, never *how*. -/
theorem lstep_elem_governed {ι : Type} (K K' : Nat) (w : Wiring ι)
{cfg : CoreConfig} (progs : ι → Program) (lm : LinkMesh ι cfg) (i : ι) :
(lstep K K' w progs lm).elem i = lm.elem i
∨ ∃ s' o, lElemResult w progs lm i = .next s' o
∧ (lstep K K' w progs lm).elem i = s' := ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ι⊢ (lstep K K' w progs lm).elem i = lm.elem i ∨
∃ s' o, lElemResult w progs lm i = StepResult.next s' o ∧ (lstep K K' w progs lm).elem i = s'
ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ι⊢ (match lElemResult w progs lm i with
| StepResult.next s out => s
| x => lm.elem i) =
lm.elem i ∨
∃ s' o,
lElemResult w progs lm i = StepResult.next s' o ∧
(match lElemResult w progs lm i with
| StepResult.next s out => s
| x => lm.elem i) =
s'
cases h : lElemResult w progs lm i with
ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιs':State cfgo:MeshOut cfg.wordBitsh:lElemResult w progs lm i = StepResult.next s' o⊢ (match StepResult.next s' o with
| StepResult.next s out => s
| x => lm.elem i) =
lm.elem i ∨
∃ s'_1 o_1,
StepResult.next s' o = StepResult.next s'_1 o_1 ∧
(match StepResult.next s' o with
| StepResult.next s out => s
| x => lm.elem i) =
s'_1 All goals completed! 🐙
ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιh:lElemResult w progs lm i = StepResult.halt⊢ (match StepResult.halt with
| StepResult.next s out => s
| x => lm.elem i) =
lm.elem i ∨
∃ s' o,
StepResult.halt = StepResult.next s' o ∧
(match StepResult.halt with
| StepResult.next s out => s
| x => lm.elem i) =
s' ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιh:lElemResult w progs lm i = StepResult.halt⊢ (match StepResult.halt with
| StepResult.next s out => s
| x => lm.elem i) =
lm.elem i; All goals completed! 🐙
ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιh:lElemResult w progs lm i = StepResult.stall⊢ (match StepResult.stall with
| StepResult.next s out => s
| x => lm.elem i) =
lm.elem i ∨
∃ s' o,
StepResult.stall = StepResult.next s' o ∧
(match StepResult.stall with
| StepResult.next s out => s
| x => lm.elem i) =
s' ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιh:lElemResult w progs lm i = StepResult.stall⊢ (match StepResult.stall with
| StepResult.next s out => s
| x => lm.elem i) =
lm.elem i; All goals completed! 🐙
/-- **No mailbox overwritten while full.** A push lands only on an idle link. -/
theorem lmesh_no_overwrite {ι : Type} (w : Wiring ι) {cfg : CoreConfig}
(progs : ι → Program) (lm : LinkMesh ι cfg) (i : ι) (d : Dir)
{s' : State cfg} {out : MeshOut cfg.wordBits} {v : BitVec cfg.wordBits}
(hres : lElemResult w progs lm i = .next s' out)
(hpush : out.push = some (d, v)) :
(lm.link i d).canPush = true := ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshres:lElemResult w progs lm i = StepResult.next s' outhpush:out.push = some (d, v)⊢ (lm.link i d).canPush = true
ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshres:(if lm.halted i = true then StepResult.stall else step cfg (progs i) (linkEnv w lm i) (lm.elem i)) =
StepResult.next s' outhpush:out.push = some (d, v)⊢ (lm.link i d).canPush = true
ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:lm.halted i = truehres:StepResult.stall = StepResult.next s' out⊢ (lm.link i d).canPush = trueι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:¬lm.halted i = truehres:step cfg (progs i) (linkEnv w lm i) (lm.elem i) = StepResult.next s' out⊢ (lm.link i d).canPush = true
ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:lm.halted i = truehres:StepResult.stall = StepResult.next s' out⊢ (lm.link i d).canPush = true All goals completed! 🐙
ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:¬lm.halted i = truehres:step cfg (progs i) (linkEnv w lm i) (lm.elem i) = StepResult.next s' out⊢ (lm.link i d).canPush = true ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:¬lm.halted i = truehres:step cfg (progs i) (linkEnv w lm i) (lm.elem i) = StepResult.next s' outthis:(linkEnv w lm i).canSend d = true⊢ (lm.link i d).canPush = true
All goals completed! 🐙
/-- **No mailbox popped while empty.** A pop takes only a delivered word. -/
theorem lmesh_no_lost_pop {ι : Type} (w : Wiring ι) {cfg : CoreConfig}
(progs : ι → Program) (lm : LinkMesh ι cfg) (i : ι) (d : Dir)
{s' : State cfg} {out : MeshOut cfg.wordBits}
(hres : lElemResult w progs lm i = .next s' out)
(hpop : out.pop = some d) :
((lm.link (w.next i d) (Dir.opp d)).peek).isSome := ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:lElemResult w progs lm i = StepResult.next s' outhpop:out.pop = some d⊢ (lm.link (w.next i d) d.opp).peek.isSome = true
ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:(if lm.halted i = true then StepResult.stall else step cfg (progs i) (linkEnv w lm i) (lm.elem i)) =
StepResult.next s' outhpop:out.pop = some d⊢ (lm.link (w.next i d) d.opp).peek.isSome = true
ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:lm.halted i = truehres:StepResult.stall = StepResult.next s' out⊢ (lm.link (w.next i d) d.opp).peek.isSome = trueι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:¬lm.halted i = truehres:step cfg (progs i) (linkEnv w lm i) (lm.elem i) = StepResult.next s' out⊢ (lm.link (w.next i d) d.opp).peek.isSome = true
ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:lm.halted i = truehres:StepResult.stall = StepResult.next s' out⊢ (lm.link (w.next i d) d.opp).peek.isSome = true All goals completed! 🐙
ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:¬lm.halted i = truehres:step cfg (progs i) (linkEnv w lm i) (lm.elem i) = StepResult.next s' out⊢ (lm.link (w.next i d) d.opp).peek.isSome = true ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:¬lm.halted i = truehres:step cfg (progs i) (linkEnv w lm i) (lm.elem i) = StepResult.next s' outthis:((linkEnv w lm i).inbox d).isSome = true⊢ (lm.link (w.next i d) d.opp).peek.isSome = true
All goals completed! 🐙
theorem Dir.opp_opp (d : Dir) : Dir.opp (Dir.opp d) = d := d:Dir⊢ d.opp.opp = d ⊢ east.opp.opp = east⊢ west.opp.opp = west⊢ north.opp.opp = north⊢ south.opp.opp = south ⊢ east.opp.opp = east⊢ west.opp.opp = west⊢ north.opp.opp = north⊢ south.opp.opp = south All goals completed! 🐙
/-- **A push is faithful.** When `i` sends `v` on side `d`, the outgoing link —
seen through `abs` — holds `v` at once, though the word has only begun to cross
the wire. -/
theorem lstep_push_faithful {ι : Type} (K K' : Nat) (w : Wiring ι)
{cfg : CoreConfig} (progs : ι → Program) (lm : LinkMesh ι cfg) (i : ι)
(d : Dir) {s' : State cfg} {out : MeshOut cfg.wordBits}
{v : BitVec cfg.wordBits}
(hres : lElemResult w progs lm i = .next s' out)
(hpush : out.push = some (d, v)) :
((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs.push v := ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshres:lElemResult w progs lm i = StepResult.next s' outhpush:out.push = some (d, v)⊢ ((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs.push v
ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshres:lElemResult w progs lm i = StepResult.next s' outhpush:out.push = some (d, v)hcp:(lm.link i d).canPush = true⊢ ((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs.push v
ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshres:lElemResult w progs lm i = StepResult.next s' outhpush:out.push = some (d, v)hcp:(lm.link i d).canPush = true⊢ (push K (lm.link i d) v).tick.abs = (lm.link i d).abs.push v
ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshres:lElemResult w progs lm i = StepResult.next s' outhpush:out.push = some (d, v)hcp:(lm.link i d).canPush = true⊢ (push K (lm.link i d) v).abs = (lm.link i d).abs.push v
All goals completed! 🐙
/-- **A hold is faithful.** With neither a push on `d` nor a pop of that link,
the mailbox through `abs` is unchanged — mid-flight and mid-ack cycles included. -/
theorem lstep_hold_faithful {ι : Type} (K K' : Nat) (w : Wiring ι)
{cfg : CoreConfig} (progs : ι → Program) (lm : LinkMesh ι cfg) (i : ι)
(d : Dir)
(hnp : (match lElemResult w progs lm i with
| .next _ out => (match out.push with
| some (d', v) => if d' = d then some v else none | none => none)
| _ => none) = none)
(hnpop : (match lElemResult w progs lm (w.next i d) with
| .next _ out => out.pop = some (Dir.opp d) | _ => false) = false) :
((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs := ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirhnp:(match lElemResult w progs lm i with
| StepResult.next s out =>
match out.push with
| some (d', v) => if d' = d then some v else none
| none => none
| x => none) =
nonehnpop:(match lElemResult w progs lm (w.next i d) with
| StepResult.next s out => decide (out.pop = some d.opp)
| x => false) =
false⊢ ((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs
ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirhnp:(match lElemResult w progs lm i with
| StepResult.next s out =>
match out.push with
| some (d', v) => if d' = d then some v else none
| none => none
| x => none) =
nonehnpop:(match lElemResult w progs lm (w.next i d) with
| StepResult.next s out => decide (out.pop = some d.opp)
| x => false) =
false⊢ (if false = true then pop K' (lm.link i d) else lm.link i d).tick.abs = (lm.link i d).abs
ι:TypeK:NatK':Natw:Wiring ιcfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirhnp:(match lElemResult w progs lm i with
| StepResult.next s out =>
match out.push with
| some (d', v) => if d' = d then some v else none
| none => none
| x => none) =
nonehnpop:(match lElemResult w progs lm (w.next i d) with
| StepResult.next s out => decide (out.pop = some d.opp)
| x => false) =
false⊢ (if false = true then pop K' (lm.link i d) else lm.link i d).abs = (lm.link i d).abs
All goals completed! 🐙
/-- **A pop is faithful.** When the consumer of link `(i,d)` takes its word, that
mailbox through `abs` empties — a real emptying, not the wire merely still
acking, because conservation and the wiring involution pin the peeked word to
this very link. -/
theorem lstep_pop_faithful {ι : Type} (K K' : Nat) (w : Wiring ι)
(hwf : w.involutive) {cfg : CoreConfig} (progs : ι → Program)
(lm : LinkMesh ι cfg) (i : ι) (d : Dir)
{s' : State cfg} {out : MeshOut cfg.wordBits}
(hres : lElemResult w progs lm (w.next i d) = .next s' out)
(hpop : out.pop = some (Dir.opp d)) :
((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs.pop := ι:TypeK:NatK':Natw:Wiring ιhwf:w.involutivecfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:lElemResult w progs lm (w.next i d) = StepResult.next s' outhpop:out.pop = some d.opp⊢ ((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs.pop
ι:TypeK:NatK':Natw:Wiring ιhwf:w.involutivecfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:lElemResult w progs lm (w.next i d) = StepResult.next s' outhpop:out.pop = some d.opphpeek0:(lm.link (w.next (w.next i d) d.opp) d.opp.opp).peek.isSome = true⊢ ((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs.pop
ι:TypeK:NatK':Natw:Wiring ιhwf:w.involutivecfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:lElemResult w progs lm (w.next i d) = StepResult.next s' outhpop:out.pop = some d.opphpeek0:(lm.link i d).peek.isSome = true⊢ ((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs.pop
ι:TypeK:NatK':Natw:Wiring ιhwf:w.involutivecfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:lElemResult w progs lm (w.next i d) = StepResult.next s' outhpop:out.pop = some d.opphpeek0:(lm.link i d).peek.isSome = truehnp:(match lElemResult w progs lm i with
| StepResult.next s o =>
match o.push with
| some (d', v) => if d' = d then some v else none
| none => none
| x => none) =
none⊢ ((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs.pop
ι:TypeK:NatK':Natw:Wiring ιhwf:w.involutivecfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:lElemResult w progs lm (w.next i d) = StepResult.next s' outhpop:out.pop = some d.opphpeek0:(lm.link i d).peek.isSome = truehnp:(match lElemResult w progs lm i with
| StepResult.next s o =>
match o.push with
| some (d', v) => if d' = d then some v else none
| none => none
| x => none) =
nonehpopped:(match lElemResult w progs lm (w.next i d) with
| StepResult.next s o => decide (o.pop = some d.opp)
| x => false) =
true⊢ ((lstep K K' w progs lm).link i d).abs = (lm.link i d).abs.pop
ι:TypeK:NatK':Natw:Wiring ιhwf:w.involutivecfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:lElemResult w progs lm (w.next i d) = StepResult.next s' outhpop:out.pop = some d.opphpeek0:(lm.link i d).peek.isSome = truehnp:(match lElemResult w progs lm i with
| StepResult.next s o =>
match o.push with
| some (d', v) => if d' = d then some v else none
| none => none
| x => none) =
nonehpopped:(match lElemResult w progs lm (w.next i d) with
| StepResult.next s o => decide (o.pop = some d.opp)
| x => false) =
true⊢ (pop K' (lm.link i d)).tick.abs = (lm.link i d).abs.pop
ι:TypeK:NatK':Natw:Wiring ιhwf:w.involutivecfg:CoreConfigprogs:ι → Programlm:LinkMesh ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:lElemResult w progs lm (w.next i d) = StepResult.next s' outhpop:out.pop = some d.opphpeek0:(lm.link i d).peek.isSome = truehnp:(match lElemResult w progs lm i with
| StepResult.next s o =>
match o.push with
| some (d', v) => if d' = d then some v else none
| none => none
| x => none) =
nonehpopped:(match lElemResult w progs lm (w.next i d) with
| StepResult.next s o => decide (o.pop = some d.opp)
| x => false) =
true⊢ (pop K' (lm.link i d)).abs = (lm.link i d).abs.pop
All goals completed! 🐙
The wall stands. An element wired through a serialised link runs the very same instruction set; each mailbox, seen through the lens, obeys the very same one-word discipline; no word is lost, none invented; and every word eventually crosses, whatever the latency. The only difference a chip boundary makes is that an element sometimes waits — and waiting is precisely the stutter that every refinement in this book was built to absorb. The mosaic does not care where the chip edge is.
end Tilessa