12.1. The metric🔗

A cell has a position in the mesh. Distance between two positions is Manhattan distance — and it is measured in hops, so it is the transport cost. Cost is zero exactly at the destination.

12.2. Deterministic routing and monotone progress🔗

Routing is dimension-order: resolve the horizontal offset first, then the vertical, then deliver to the local cell. Dimension-order routing is the classic deadlock-free policy, and here it is what makes progress exact. A hop is one nearest-neighbour step in the chosen direction.

The first transport theorem is that a hop pays down the remaining cost by exactly one whenever the packet is not already home. Not at most one, not at least one — exactly one. So hop count equals Manhattan distance on the nose, and arrival is neither early nor late. Strict monotone progress — deadlock-freedom — is the immediate corollary.

12.3. Delivery timing🔗

Iterating the hop gives hops, the position after n cycles. The exact-progress law lifts to a two-sided timing guarantee: a packet injected at here bound for dst is at its destination exactly at cycle manhattan here dst, and is strictly in transit before then.

12.4. Packets and faithful transport🔗

A packet carries an opaque payload to a destination. Advancing it changes only its position; the payload is copied verbatim. Payload-independence is the no-corruption guarantee made structural, and because advancing is a function there is no duplication and no drop.

12.5. Uniform composition🔗

The mesh is the same cell type at every coordinate, each clocked by the single proved cellClock. The composition operator is pointwise — clocking the mesh at a coordinate is definitionally the single-cell clock there — so it introduces no cross-cell coupling in the compute path. Every single-cell theorem lifts unchanged; in particular the execute-path refinement against the ISA step function holds at every executing coordinate with a one-line proof. This is "one proved element, one uniform composition, no special cases" stated as equations.

12.6. End to end: transport into a cell🔗

The two layers meet in the delivery theorem. A value produced at cell src and addressed to dst, carried as a host-write and run for manhattan src dst network cycles, arrives as that host-write at cell dst — on time, payload intact — and leaves every other cell of the mesh exactly as it was. The write delivered is the same applyHostWrites the single-cell lifecycle proofs already reason about, so the mesh inherits their guarantees without restating them.

Composed with the pointwise refinement, this closes the loop: the mesh is the proved cell, repeated, plus a transport layer that provably delivers on time and touches nothing it should not.

12.7. Generated RTL🔗

The router and a single in-flight packet are rendered to SystemVerilog from the same Lean RTL DSL as the cell. The combinational honeycomb_router is the dimension-order decision — routeDir and neighbour — with its dir output encoded by the shared Dir.code, so the DSL and the emitted Verilog agree on one numbering by construction. The sequential honeycomb_flit holds one packet and advances it a hop per clock, pulsing deliver the cycle its position reaches the destination: exactly hop manhattan src dst, payload carried verbatim. An Icarus golden test drives it and checks that timing and that payload against the model.

12.8. A first multi-cell mesh🔗

honeycomb_mesh puts two proved honeycomb_cell instances at (0,0) and (1,0) with one router-driven transport channel between them. A host-write injected at the mesh boundary — a data-memory address and value bound for a destination cell — is advanced one hop per clock and, on arrival, drives that cell's host-write ports, so the value lands in exactly the destination cell's data memory and no other cell is touched. It is the RTL image of injected_packet_delivered, and an Icarus golden test drives it: a write delivered across the fabric to the right cell, on time, with the other cell's memory left untouched.

For this first fabric, packet injection is host-driven at the mesh boundary — a cell-to-network interface, an st to a memory-mapped network port, is future work — and the single channel carries one packet at a time. What it establishes is two real cells wired at coordinates with a router between them, and delivery across the fabric that matches the proved model.

12.9. Cell-to-network interface🔗

The first fabric injected packets at the mesh boundary. This layer lets a program inject its own: a store (st) to a memory-mapped network aperture address emits a packet instead of writing local memory. The whole descriptor fits in the low 15 bits of the store address — bit 14 the network flag, then the destination coordinate and the remote address — so a program builds it with a single li and sends with one st; the stored value is the payload.

The addressing convention is proved self-consistent (encode/decode roundtrip), and a net-store is proved to produce exactly the packet the transport model's inject builds. Composed with injected_packet_delivered, that closes the loop in the model: a program's store lands its value in the destination cell's data memory, on time, and nowhere else.

The RTL implements the convention. honeycomb_cell_net is the cell with the aperture: an st whose address has bit 14 set suppresses the local write and pulses the net-out ports instead. honeycomb_mesh_net wires that into the transport — cell0 runs a program and injects, cell1 receives — with no host send port. An Icarus golden test loads a four-instruction program (li, li, st, halt) into cell0, starts it, and checks the stored value arrives in cell1's data memory.

The send is not only golden-tested; it has a proved semantic model. execNet layers the aperture over the base execDecoded, returning the architectural state and an optional emitted packet. On any ordinary instruction — including a store to a non-aperture address — it is execDecoded and emits nothing, so the existing execute-path refinement holds unchanged (execNet_ordinary_refines_step): the network extension is conservative, with no regression. On an aperture store it emits the transport inject (execNet_send_inject) and only advances the program counter, leaving local memory untouched (execNet_send_preserves_data) — exactly what the RTL does by suppressing the local write. Composed with delivery, a program's store lands in the destination cell's data memory (execNet_send_delivered).

Lifted to the busy/halt-gated cell cycle, netCellExecCycle is the model the generated honeycomb_cell_net corresponds to — the analogue of the base cell's wordCellExecCycle. On an ordinary cycle it commits the same architectural state as the ISA step (netCellExecCycle_refines_step), and on a net-store cycle it emits the transport packet and leaves data memory untouched (netCellExecCycle_send). So the network cell now stands exactly where the base cell does: a proved cycle model, generated RTL, and golden tests.

12.10. Link contention and deadlock freedom🔗

The transport so far moved one packet at a time. With many in flight, several may want the same outgoing link in one cycle; a router arbitrates, and a blocked packet waits while holding the link it is on. The danger is deadlock: a ring of packets each holding a link the next one needs, forever. Dimension-order routing rules this out, and here is why.

Give every directed link — a channel, a position and an outgoing direction — a global rank, independent of any packet's destination: east/west channels rank below all north/south ones (X is resolved before Y), and within a dimension the rank rises in the direction of travel. The one fact that carries the argument is that the rank strictly increases at every route step — the channel a packet uses next always outranks the one it is on.

A deadlock is a cycle in the channel-dependency relation (ChanDep): each packet on one channel needs the next, closing back on itself. But every dependency edge strictly raises the rank, so a cycle would force a rank to be strictly less than itself. There is none — contention can delay a packet, never deadlock the fabric.

12.11. Multi-hop: per-cell routers🔗

The meshes above move a packet with one shared router. honeycomb_station gives each cell its own router and a one-packet inbox: it holds a packet, asks its router which way to go, and forwards it to that neighbour — or delivers locally on arrival. honeycomb_line3 wires three stations in a line, so a packet injected at station 0 for column 2 physically hops 0→1→2 through the middle station's own routing hardware, one hop per clock, delivered only at the destination column. Each station reuses the router whose decision mirrors the proved routeDir; an Icarus golden test injects a packet, checks it arrives at the far station in exactly two hops with its payload intact, and that the intermediate stations forward rather than deliver it.

This is real multi-hop over per-cell routers, with one packet in flight; the deadlock-free arbitration proved above is what lets many packets share the links without the fabric locking up.

12.12. Turning routes: a 2-D grid🔗

honeycomb_station2 is the station with all four nearest-neighbour ports, and honeycomb_grid2 wires four of them into a 2×2 mesh. A packet injected at (0,0) for (1,1) turns a corner under dimension-order routing — east to (1,0), then north to (1,1) — two hops through two different per-cell routers, delivered only at the destination cell. This is the first rendered mesh where a route actually turns rather than running straight. A golden test drives the corner route and the two one-hop neighbours, checking hop counts and payloads.

12.13. Link arbitration: flow-controlled contention🔗

The grids so far assume one packet in flight. honeycomb_fstation adds flow control so many packets can share the links. Each of its five packet sources — the inject port and the four neighbour input ports — owns a dedicated one-packet buffer: a port accepts exactly when its own buffer is free, so a buffer is the physical image of one directed channel, the resource the deadlock-freedom proof ranks. A buffered packet forwards only when it wins its outgoing direction's pointer round-robin arbitration and the downstream grants; a blocked packet waits in place — never dropped — and every wait runs from a buffer to the strictly higher-ranked channel buffer of its next hop, so the waiting can never close into a cycle (no_dep_cycle, carried onto the buffers by no_bufwait_cycle). An earlier revision shared one buffer among all five sources; that buffer sat outside the channel model, and two head-on packets on a line could wedge it — the honeycomb_hline3 fabric and its golden test drive exactly that exchange, which the per-port station carries through. honeycomb_fgrid2 wires four stations into a 2×2 with two injection points, so two packets bound for the same corner arrive together; a golden test injects both the same cycle and checks both are delivered, neither lost.

12.14. A general N×M mesh🔗

honeycombGridModule n m generates the whole fabric: a honeycomb_fstation at every coordinate, bidirectional nearest-neighbour links between every adjacent pair — each edge carries a packet lane and a grant in both directions — and a delivery port per cell, so any coordinate can be a destination. Injection is at (0,0), and a packet routes there by dimension order over as many hops as the grid is wide. It is emitted as a concrete 3×3 (honeycomb_grid3), where (0,0)→(2,2) is a four-hop route that turns; a golden test drives it and the two straight two-hop edges. Nothing below the generator is new — the same proved routers, arbitration, and deadlock-freedom, now composed at scale from one Lean function.

12.15. A program driving the fabric🔗

honeycomb_progline puts a real program on the mesh. Cell 0 is a honeycomb_cell_net: it runs a loaded program, and when it executes an st to the network aperture its net-out ports pulse — those drive station 0's injection directly, with no host send port. The packet then routes through a line of flow-controlled honeycomb_fstations to cell 2, a plain honeycomb_cell, where it lands as a data-memory write. This composes the three proved pieces — the cell-to-network send, the arbitrated deadlock-free fabric, and a receiving cell — so a program running on the mesh drives real multi-hop traffic. A golden test loads the send program, starts cell 0, and checks the value arrives two hops away in cell 2's memory.

12.16. Backpressure🔗

The line above lets the one packet fit an idle fabric. honeycomb_cell_net_bp removes that assumption: it is honeycomb_cell_net plus a net_ready input from the network, and when a net-store is executing but the network cannot accept it (!net_ready) the cell stalls — it holds the program counter, keeps offering net_send, and retires nothing — completing the store only once accepted. So a program can send while the mesh is busy without dropping a packet. Only the execute step is re-gated; everything else, including the proved net-out logic, is the net cell verbatim. A golden test drives net_ready low across the store and checks the cell freezes in place, then releases it and checks the store retires.

12.17. One cell, repeated🔗

honeycomb_tile is the machine's repeating unit: a back-pressured honeycomb_cell_net_bp wired to its own honeycomb_fstation. Inside the tile the cell's net-out drives the station's injection, the station's inject_ready feeds the cell's net_ready (backpressure), and the station's delivery writes the cell's data memory — so every tile can both source and sink traffic. Its only outward difference from any other tile is the my_x/my_y it is placed at. honeycombTileGridModule n m tiles it across a grid with the same bidirectional links as the mesh generator, emitted as a 2×2 (honeycomb_tilegrid2).

This is the flat vision as literal hardware: identical tiles, with role chosen by which program each runs, not by any silicon variation. A golden test loads a send program on tile (0,0), leaves the rest idle, and checks the value lands in tile (1,1)'s memory two hops away.

12.18. Booting one tile from another🔗

Self-hosting is control plus load. A tile decodes the top two bits of a delivered packet's remote-address to choose the delivery's effect: 00 a data-memory write, 01 an instruction-memory write, 10 a start command. The aperture and its proof are unchanged — this is purely a delivery-side convention — and a tile's instruction port and start are now the host's or the network's. So a program on one tile can write another tile's program and launch it.

A capability, not ambient authority. Instruction-write and start take effect only while the target is halted. A running tile cannot be reprogrammed or restarted by a peer — to reload it, it must first yield. Data delivery stays open (a running compute tile legitimately receives operands). This is self-governed and flat: no privileged loader tile, every tile identical; a tile controls its own reprogrammability by whether it is running. It also removes a real hazard — writing the instruction memory of an executing cell is otherwise undefined.

Two golden tests exercise this. A remote start: tile (0,0) sends a start command to (1,1), which was loaded but never host-started, and only then does it run. A remote boot loader: tile (0,0), host-seeded with a loader program in its instruction memory and a worker program in its data memory, relays the worker word by word into (1,1)'s instruction memory (op 01, permitted because (1,1) is halted) and then starts it — (1,1), untouched by the host, runs the freshly loaded program. One tile bootstraps another, entirely over the proved transport.

12.19. Scheduling a kernel across tiles🔗

Load-and-start of a single tile composes into distribution across many. An orchestrator tile is host-seeded with a scatter program in its instruction memory and a handful of small worker programs in its data memory. When it runs it loads worker A into one neighbour and starts it, then worker B into another and starts it — every load and launch a net-store, gated by the same halted rule. Each worker, untouched by the host, runs and sends one result back to a distinct address in the orchestrator's data memory (an ordinary data-write, op 00). The orchestrator gathers them.

A golden test drives exactly this on the 2×2 array: the orchestrator at (0,0) brings up workers at (1,0) and (0,1), and their two distinct results arrive in (0,0)'s memory — data[10] from A, data[11] from B. One tile distributes work to several and collects the results, entirely over the proved transport, with no host involvement past the initial bring-up. That is the scatter-launch-gather core of a self-hosted kernel.

12.20. The boot ROM: the machine brings itself up🔗

Everything above still seeds one tile through host ports. honeycomb_bootgrid removes the host entirely — it has no program-load ports at all. Every cell is a honeycomb_boottile carrying the same boot image (a ROM in instruction memory and a worker program in data memory, baked in at reset), and every cell auto-starts into it out of reset. The ROM reads the cell's own coordinate — the reserved data address 255 returns the packed {x, y}, which is 0 exactly at the origin — and branches: the root (0,0) loads the worker into its neighbour's instruction memory and starts it; every other cell halts, becoming loadable through the halted-gate.

There is no master in the reset logic. Each cell self-selects by position — the one non-uniformity the flat design keeps — from an identical image. The load and start reuse the proved transport and the halted-gate capability unchanged. A golden test does nothing but assert reset and release it, then watches the neighbour's memory fill: the array comes up on its own.

This is where "self-hosting" stops being a promise. The boot image is the trusted computing base — the one code not delivered over the network — and it bootstraps the array with no external loader. It is also where a real capability model anchors: the ROM is where the token below is minted and handed to the programs it launches.

12.21. A capability on delivery: integrity and availability🔗

The boot ROM promised a place to anchor a real capability, and this is it. Two gaps remained in the self-hosting fabric against a malicious or buggy tile. First, integrity: a delivered instr-write or start was gated only on the target being halted — ambient authority, so any peer could reprogram a halted tile — and a delivered data-write was ungated entirely, so any tile could scribble any other's data memory, its private state, even the register it would load a secret from. Second, availability: nothing bounded what a tile injected, so a flooder could saturate links and starve legitimate traffic (the fabric is deadlock-free, but not starvation-free).

Both are now closed by a capability the trusted boot image installs in every tile — capability = (may-touch: token + mailbox) + (may-consume: injection budget) — and proved, not merely asserted.

Integrity. Each tile holds a secret 64-bit token and a mailbox window. The delivery decode capDecode honors a privileged op only on an exact token match with the target halted, and a data-write only on a token match with the address inside the mailbox; everything else is dropped. So authorization is unforgeable — exact token equality (cap_unforgeable), one value in 2^64 — an authorized write is confined to the mailbox (cap_data_confined), and a tile's private state, placed outside its mailbox, is unwritable by any peer (cap_private_unwritable): the scribble hole closed, least authority. Composed with the proved transport, an authorized message lands in the destination's mailbox and nowhere else (cap_authorized_data_delivered).

Availability. A round-robin arbiter serves offers in rotation, so it is work-conserving (firstOffer_isSome — never idle under demand) and a continuously offering input is served within a bounded number of grants (rr_bounded_wait): no starvation. A per-tile token bucket caps injection — accepted injections over any window are at most the refilled credit (inject_bounded) — so a flooder's fabric footprint is bounded. The two compose: because the round-robin bound holds for any offer pattern of the other inputs, a continuously-offering victim is served within a bounded number of grants even against a flooder that offers everywhere every cycle — and in every window, not just once (no_starve_under_flooder, no_starve_windowed). And the fabric now deploys a fair arbiter (review R2 closed): every station arbitrates its outgoing links and its delivery port by pointer round-robin — the rotated priority scan rrFirst, whose bounded wait is proved against adversarial per-grant request patterns (rr_ptr_served_within: a persistent requester is served within five grants, whatever the other four sources do) — with the pointer stepping past each winner on a grant. On the generated chain, station_serialises and station_serves_loser are the two instance theorems (the winner departs and the pointer rotates; from the rotated pointer the previous loser wins even against a refilled rival), and the tb_rrfair golden test drives a line-rate flooder against a transit stream: under the old fixed priority the transit starves outright; under the deployed round-robin every transit packet is delivered. Capped sources and fair links together mean a malicious tile cannot starve its peers.

Each mechanism is generated to RTL as the direct twin of its Lean definition — honeycomb_capgate for the decode, honeycomb_rrarb for the arbiter, honeycomb_tbucket for the quota — and golden-tested (test/mesh/tb_cap*.sv). They compose into honeycomb_captile, which wraps the base net cell so a delivered packet reaches its instruction memory, data memory, or start only when the capability authorizes, and its outbound send is quota-limited. The end-to-end golden (test/mesh/tb_captile.sv) drives the real cell: an authorized message lands in the mailbox while a wrong-token or out-of-mailbox delivery is dropped, and a loaded-but-unstarted worker runs only under a token-matching remote start — one tile cannot scribble or hijack another.

12.22. The router RTL, refined against the model🔗

The generated fabric has until now been checked by golden simulation; its _from_dsl theorems only state that the emitted text is the DSL's render. The combinational core — the router — can be taken further. Giving the SV DSL an evaluation semantics in Lean (evalExpr over expressions, runAssigns over a block; see HoneycombBook.MeshRefine) lets us prove the generated honeycomb_router, run as an AST under that semantics, computes exactly the proved routing model: its dir output is routeDir's port code, its next_x/next_y are neighbour's next hop, and its arrived is the destination test (router_refines_routeDir). So the router RTL refines the routing model — the first RTL-level refinement of the transport fabric, not merely a golden test. Refining the emitted SystemVerilog text stays deliberately out of scope (that needs a parser); this refines the DSL value the text is rendered from, one layer up.

The sequential flit follows. Giving the DSL's always_ff block a non-blocking step semantics (evalBlock: right-hand sides read the current registers, the block folds into the next state) and taking the flit's routing wires from the refined router instance, flit_advances proves the generated honeycomb_flit register update is InFlight.advance: a live packet that is not yet home steps its position to hop pos dst — exactly the model's advance — carrying its destination and payload verbatim and staying valid. So both halves of transport, the routing decision and the one-hop-per-clock advance, are now refined at the RTL level.

Iterating the clock closes the timing. The flit never writes its rst_n/inject inputs, so they persist across cycles, and before manhattan src dst cycles the packet is not yet home (hops_not_before) — so the advance step applies every cycle. Hence flit_tracks: after k ≤ manhattan src dst clocks the register position is hops k src dst, the position of InFlight.advanceN; and flit_arrives: at exactly cycle manhattan src dst the position is dst, so the combinational deliver (valid ∧ arrived) pulses then and not before — the RTL image of hops_arrives.

Composition closes the single-packet story. The 1×2 mesh drives a per-cell delivery strobe deliverAt x y = delivered ∧ dst == (x,y); evaluating that generated expression (deliver_isolation) shows that when a packet is delivered for (dstx, dsty) the strobe fires for exactly that cell and is 0 for every other — the carried write reaches the destination and nowhere else, the RTL image of injected_packet_delivered's isolation clause. Composed with the timing above, the mesh delivers to exactly the destination cell at exactly cycle manhattan.

The capability decode joins the same treatment. honeycomb_capgate was proved as the model capDecode and generated as RTL, golden-tested; running that generated AST under the combinational semantics, capgate_refines_capDecode shows all five of its effect outputs (data-write, instr-write, start, weight-write, and the read-tagged get that the whole DistMem read path rests on) are exactly capDecode's effect — the 64-bit token compare bridges through BitVec.toNat (injective, so the RTL's numeric equality is capAuthorizes), the op code and halted flag map across, and the 9-bit mailbox compare is inMailbox. So the capability decode RTL refines the proved decision, not merely matches it on tested vectors.

The read path's reply is not a new mechanism either. The request carries a return capability — a capability for a reply region homed at the requester — and the response is an ordinary capability-checked put through it, so the put theorems transfer verbatim: both legs of a lowered get are authorized at their gates (get_round_trip_coherent), the served value lands in exactly the requester's reply cell and nowhere else (get_response_delivered), and a response presenting any other token is inert (response_forgery_rejected). The RTL rendering of the echoed return capability is milestone-9 work; the generated honeycomb_readresp still responds by convention.

The first step into the flow-controlled fabric is the single-station no-loss invariant. honeycomb_fstation adds backpressure so many packets can share a link, and each of its five sources owns its own one-packet buffer: a buffer holds a live packet until it departs — dep_<s> = dwin_<s> ∨ sent_<s>, winning the delivery port at its destination or winning its outgoing direction with the downstream granting. fstation_accepts proves an input port grants exactly when its own buffer is free (no cross-port coupling — the buffer is a dedicated channel resource); fstation_holds_i/fstation_holds_s prove a live, non-departing packet is held unchanged for the next cycle (validity, destination, and carried write all persist) — it waits in place, never dropped or overwritten; fstation_frees_i/fstation_frees_n prove a departing packet clears its buffer; fstation_latches_w/fstation_latches_s that a free buffer latches its own port's offer; and fstation_delivered that a station delivers locally exactly when some buffer holds a packet at its own coordinate. This per-port buffer structure is what lets the deadlock-freedom rank argument transfer to the hardware's own resources (no_bufwait_cycle): every wait runs from a buffer to the strictly higher-ranked channel buffer of its next hop, and inject buffers are pure sources, so no ring of waiting buffers can close.