Floorplans: designing the machine, and what its traffic costs

Part J, lesson J3. You need lesson J1 (places and their doors). This is the lesson where you design a machine: where its places stand, and the roads between them.

A floorplan says where every place of a machine stands and how roads and wires join them. On the site it is a text file you write yourself — the town every example runs on is one, and Shor's algorithm names its own (floorplan "shor"):

floorplan shor_d3 "A machine for Shor's algorithm (surface code, d = 3)"
region memory
place mem1      mem_d3  at 31 10
...
junction j0_4 at 31 0
road j0_4.s -- mem1.in as door_mem1_in
road j0_3.e -- j0_4.w as street0_j0_3_j0_4
wires auto bus 88

Nine rules (F1-F9) judge a floorplan before any program runs on it. Lesson J1 did F1. This lesson does the two a designer meets first — F6, every place can send a bundle to every other, and F5, a bundle can wait in front of every door — and then the number a designer optimises: traffic, how far the ions travel.

1. A floorplan as a graph

A road joins two doors and has a length in sites. A door is a place's (depot.out, mem.in) or one of a junction's four arms (n e s w); a bundle may cross a junction from any arm to any other. A place is an end, never a thoroughfare: nothing passes through it.

For Lean, every door gets a number — the doors of places are 1 to 8, arm k of junction j is 100 + 4j + k — because numbers compare in a step, and names would have to be compared letter by letter. The names stay beside them, for reading.

A route from door a to door b is the list of doors a bundle passes after a, each one step from the one before, the last of them b. Checking a route is easy — one step at a time — and that is how this lesson proves that a bundle can get somewhere: by showing the way.

A small machine: a depot, a preparation place, a memory and a readout, side by side below one street. Every door takes a road of 9 sites up to the s arm of its own junction; the junctions are joined left to right by the street.

On the corridor every door hangs off a junction of its own — door d off junction d - 1 — so the way from one door to another is always the same shape: down the door road to the s arm, across to e (or w), along the street, across to s, up the door road. way writes it down; F6 then needs only that each of these routes really is one.

Exercise 1 ★ corridor_f6 open

Prove that the corridor satisfies F6. (f6_by_way, and let the kernel check the twelve routes.)

Showing that a bundle cannot get somewhere needs a different witness: a closed region, a set of doors no step leaves. A bundle that starts inside one stays inside it, however long its route — so a door outside it is out of reach.

Exercise 2 ★★★ trapped open

Prove it: a route that starts in a closed region ends in it. (Induction on the route; simp turns contains and all into ∈ and ∀.)

Exercise 3 ★★ a_missing_road open

Take away the street road between j3 and j4. Prove that F6 then fails: the doors left of the gap — the depot's and prep's, and every arm of j0 to j3 — are a closed region, and the memory's door is not in it.

Exercise 4 ★★ what_the_cut_leaves open

In cut, a block prepared at prep can still reach the depot, but no route takes it to the memory. Prove both.

2. F5: room to wait

A bundle that reaches a door while the place is busy waits on the road in front of it. That road must hold the whole bundle — nine ions for a block — or the ions would spill back into the junction behind them (G4, G14 on the schedule). F5 asks it of the floorplan, for every road that ends at a door of a place.

Exercise 5 ★ corridor_f5 open

Prove that every door road of the corridor holds a bundle of nine.

Exercise 6 ★ a_short_door open

Move junction j4 down so its road to mem.in is only 4 sites, and F5 fails. Prove it.

3. Traffic

Every bundle a program moves travels a route of roads, and costs ion-sites: its ions times the sites it crosses. Summed over a program, that is its traffic, the number the design page shows in its Traffic panel and the floorplan optimiser reduces. A route here is the list of roads a bundle takes, by number.

A block is prepared, rests in the memory, and is read out: three trips of nine ions — from the depot to prep (its door road, s01, s12, prep's door road), from prep to mem, from mem to post.

Exercise 7 ★ corridor_traffic open

Compute the traffic of the three trips on the corridor and prove the number.

A designer can do better without moving a single place: shorten the street between the doors the program uses most. Here the street segments between prep and the memory, and between the memory and the readout, are pulled in to 3 sites.

Exercise 8 ★★ tight_is_better open

Prove that tight has less traffic for these trips, and that it still satisfies F5 and F6.

Exercise 9 ★★★ longer_road open

In general, a longer road never makes a trip cheaper. Prove the step everything rests on: lengthening the road with a given number by one site never lowers lengthOf for that number, for any list of roads. (Induction on the list; omega finishes the arithmetic.)

What the site does with this

Shor's algorithm on the floorplan shor, on the design page: its Floorplan button shows the text the machine was built from, and its Traffic panel the number this lesson is about.

The floorplan rules F1-F9 are evaluated on every floorplan the design page loads, by the rule language of Part E, with words for footprints, crossings and reachability: there reachable is decided by a search over the roads, and the routes and closed regions of this lesson are what that search finds. Traffic is measured on the real schedule: Shor's algorithm on shor moves 313,727 ion-sites. The optimiser searched 150 rearrangements of that floorplan's places, scheduling each, and found one (shor_traffic) that moves 199,580 — 36% less — while every rule still holds and the compiled program signs off the same. Its makespan hardly changed (11.16 s to 11.04 s): Shor's critical path is lattice surgery, not travel, so a faster Shor needs more bridges, which is the next design decision, not the layout.