Places: a gadget is a box with doors and a promise

*Part J, lesson J1. You need Parts A and B of this tutorial (sites, rails, shuttles, gates) and lesson E1 (a device as data). This lesson starts Part J, where single devices become a whole fault-tolerant machine; it uses only lists, records and decide.*

A fault-tolerant computer is too big to compile ion by ion. The site builds it the way chips are built: from places, each a small verified device with a job — prepare a logical block, extract its syndrome, measure Z̄Z̄ between two blocks by lattice surgery, distil a magic state, keep a block in memory — and from roads that carry bundles of ions between them. A place is compiled and checked once (as hardware, by the device rules of Part E; as logic, by the flows and fault distance its specification states), and then used as a black box with doors.

Here is one, the magic-state factory, standing in the town every example runs on. It is selected: the panel on the right lists its doors — in takes fresh ions, out gives the magic state — and the timeline below shows when each place is busy.

And here is what the box hides: the factory's one op, produce, on its own device, every step of it checked by the device rules.

Every door says what crosses it. A door of a place carries ions (a bundle of width ions with a role: a block's data, a magic state, fresh ions from a depot) or bits (a signal: a syndrome for the decoder, an outcome, a decision that switches an op on). Each is entered (in), left (out), or both (inout, the four arms of a junction).

This lesson writes doors as Lean data — the real ones, as the place library declares them — and the first floorplan rule as a Lean function.

1. Doors

2. F1: a road joins two doors that agree

The floorplan rule F1, as the site states it in the rule language (the floorplan rule set, floorplan.rules on the Rules page):

rule F1 "A road or a wire joins two doors that agree" core
  (for all r in roads, a in ends(r), b in ends(r) where a != b:
     medium(a) = medium(b)
     and (role(a) = role(b) or role(a) = "any" or role(b) = "any")
     and (role(a) != "data" or role(b) != "data" or
          (width(a) = width(b) and (code(a) = none or code(b) = none or code(a) = code(b))))
     and (dir(a) != dir(b) or dir(a) = "inout"))
  and (for all w in wires, a in ends(w), b in ends(w) where a != b:
     medium(a) = medium(b)
     and (signal(a) = signal(b) or signal(a) = "any" or signal(b) = "any")
     and (dir(a) != dir(b) or dir(a) = "inout"))

Here is the same condition on one pair of doors, as a Lean function that computes a Bool.

Exercise 1 ★ road_to_a_bridge open

A road from a junction's arm to a bridge's door is allowed. Prove it.

Exercise 2 ★ factory_to_pharmacy open

A factory's magic ion may go straight to the pharmacy's magic door.

Exercise 3 ★ bits_are_not_ions open

No road joins a door of bits to a door of ions: a syndrome never travels on a conveyor.

Exercise 4 ★ wires_carry_their_signal open

A wire from the classical memory's decision door to a workshop's control door is fine; a wire from a bridge's syndrome door to that control door is not.

Exercise 5 ★★ outs_never_meet open

Two doors that are both left (outward) never accept each other, whatever else they say. Prove it for all doors. (simp [accepts, dirOk, ha, hb] unfolds what you need.)

Exercise 6 ★★ data_widths_match open

When two data doors accept each other, they carry bundles of the same width. Prove it.

3. A place's promise: what goes in comes out

An op of a place moves bundles through its doors. Its transfers say which door, which way, and how many ions — measured by replaying the op's program, not typed beside it. A place keeps its own resident ions (a bridge's 23 ancillas, a pharmacy's 8): every op ends with them home, so whatever comes in, in one op, goes out again in the same op.

Exercise 7 ★ ops_conserve_ions open

Prove that both ops send out exactly as many ions as they take in.

Exercise 8 ★★ injection_makes_a_block open

The pharmacy turns one magic ion and eight fresh ions into one block of nine: its out door is a data door of the code, so it is accepted by a bridge's in door. Prove that the pharmacy's out door, written below, accepts bridgeInA.

What is checked, and what is not

F1 judges each road at its two ends, so a junction's arm, which accepts any role, joins any door. A road never checks that what arrives through a chain of junctions is what the far door expects. That is the schedule's job: G1 requires every bundle an op takes in to arrive in the exact order its verified program takes it, and G2 follows every ion. Lesson J2 writes those schedule rules down; lesson J3 builds whole floorplans out of places and roads.