The seams — where the layers meet

The tower's thesis is that the layers connect formally: each layer's conclusion is the next layer's hypothesis, so a single theorem should say the physical die realises the ISA. That theorem exists and type-checks —

-- lean/ThinkingSand/EndToEnd.lean
theorem chip_realises_isa : dieBeh = isaBeh := by
  rw [iface_L1_timing, iface_L1_L0, middle, iface_L3, iface_L4_L5]

where dieBeh is the physical die's pad-trace behaviour and isaBeh the ISA reference's, both of type List (Val (Fin nIn)) → List (Val (Fin nOut)) — an input pad-trace to an output pad-trace. It type-checks because the abstraction targets line up: that is what "the layers connect" means, made mechanical. Its content is entirely in what it assumes, and #print axioms on chip_realises_isa reads that back exactly.

One boundary is a real proof; the rest are the seams. The middle — netBeh = rtlBeh, the netlist and RTL agreeing on every pad-trace — is sorry-free: it lifts the proved one-step commutation l2_commutes across cycles (trace_refines). Every other arrow is a named axiom, because the layer that would discharge it is still proof-phase. Those axioms are this page. Each is a seam: a theorem the tower needs and does not yet have, sitting exactly at a layer boundary. They are scored on the scoreboard as the IF/* section (tools/check-interfaces.py), and this appendix is their long form.

Building the composition is what surfaced the seams as first-class objects. The per-layer boards score each layer's internal obligations; none scored the arrows between layers. Two of the seven were nowhere at all before this page — the extraction-composition (iface_L1_L0) and the front-end commutation (frontEndCommutes) — while the other five had a home inside a layer's TODO list but were not marked as the load-bearing composition step.

The ledger

The composition, bottom-up (die → timed → netlist → RTL → arch → ISA), with the one proved link in bold:

Each seam below records: what it connects, what is proved below it and assumed above, the executable precursor on a layer board (the empirical version, where one exists), and the discharge route — what turns the axiom into a theorem.

S-timing — the timing bridge

iface_L1_timing : dieBeh = timedBeh — the real, continuous-time silicon has the same observable behaviour as a discrete two-phase synchronous machine.

Connects L1 (timing) to the discrete world every layer above L1 lives in. It is the book's M5 bridge theorem: if static timing closes — every path meets setup and hold at every corner — then the clocked circuit's sampled behaviour is exactly a Mealy machine's, with no metastability inside the operating event.

Below: the entire L1 board — nine-corner STA (PASS), the SDC completeness audit, the crosstalk and IR-drop bounds — establishes the hypothesis (closure with margin). Above: every functional layer silently assumes the discrete model is faithful.

Precursor: L1's checkers bound the analog margins but do not state the reduction; they are the empirical evidence that M5's hypothesis holds for this die.

Discharge route: M5 is open mathematics — turning metric timing margins into a behaviour-preservation statement about the discretisation. It is a general theorem about synchronous circuits, not specific to this design; see L1/07 and the axiom register's M5.

S-extract — extraction and grounding

iface_L1_L0 : timedBeh = netBeh — the discrete machine the silicon implements is denote theLib theNetlist: the gate graph the book reasons about.

Connects L1 (geometry) and L0 (devices) up to the netlist object L2 consumes. This seam is the one the composition newly forced into the open: three certificates each pass on their own, but nothing joined them into a single behaviour equality.

• celltopo (L0/ccc, PASS): each cell's transistors compute its Liberty function — so theLib is grounded. Archetype ①.
• routecheck (L1, PASS): the layout has the connectivity the netlist claims — no opens, no shorts. Archetype ②.
• LVS device-match (L1/02, no checker yet): the extracted devices and nets are exactly theNetlist.

Below: the three certificates. Above: L2 takes theNetlist as the object of record. Precursor: celltopo and routecheck are the passing islands.

Discharge route: an LVS device-and-connectivity match producing the extracted netlist, then the lemma extracted = theNetlist ∧ celltopo ⇒ timedBeh combinationally equals netBeh. See L2/00 (S1) and L1/02.

S-frontend — the RTL front-end

frontEndCommutes : CommutesM (denote theLib s0) rho — the front-end that produces the trail head s0 from the elaborated RTL preserves the cone functions, so ρ- commutation transports from ⟦RTL⟧ to the start of the synthesis trail.

Connects L3 (⟦RTL⟧) to the head of L2's equivalence trail. The trail itself — s0 → s1 → … → s7 = N, seven per-pass PassCerts against miterCNF — is checked. What is not checked is the step that builds s0: Yosys proc/techmap/flatten turning elaborated RTL into the first gate netlist. It is the single still-open factor of the otherwise-proved l2_commutes.

Below: L3's construct census (PASS) makes ⟦RTL⟧ a well-defined object; the ABC trail (L2) carries s0 to N. Above: L2's one-step goal quantifies over ⟦RTL⟧.

Precursor: L3/comb-checks (PASS) shows the naive-netlist oracle ⟦s0⟧ is well- defined (no combinational cycles). Discharge route: a CEC of ⟦RTL⟧ against ⟦s0⟧ — the same certificate machinery as the trail, applied to the front-end. See L3/00.

S-reset — matched reset

reset_corr : Val.rename rho resetF = resetR — the netlist's reset state maps, under the register correspondence ρ, onto the RTL's reset state.

Connects L2's register correspondence to L3's temporal lift: it is the base case of the induction in trace_refines. Without it, the one-step commutation never anchors, and the two machines could agree step-for-step yet start from unrelated states. In the axiom base of chip_realises_isa it is the anonymous sorryAx — a theorem := sorry rather than a named axiom.

Below: ρ itself (L2/03, F5); L3's X/init idioms (PASS) show no flop carries a power-up value. Above: the whole trace_refines lift and everything it feeds.

Precursor: L3/x-idiom + L3/init-idiom (PASS) — the necessary condition (no stray power-up values), but not the ρ-image equality itself. The IBuf residual (an unreset flop) is the concrete way this seam fails when it fails.

Discharge route: reset-state extraction from both sides and the ρ-image check; mechanical once ρ is pinned. See L2/03.

S-refine — RTL refines the ISA

iface_L3 : rtlBeh = archBeh — the RTL's observable behaviour refines the microarchitecture-to-ISA abstraction.

Connects L3 (RTL) to L4 (ISA) through L3's refinement. This is the work the book names: the inductive invariant relating pipeline state to architectural state, the project's irreducible content.

Below: the RTL object (L3). Above: the ISA (L4). Precursor: L3/cosim (PASS) — 1631 committed instructions matched against spike instruction-by-instruction, zero mismatches. That is the oracle: strong evidence, executed, but not the theorem. The gap between the oracle and iface_L3 is exactly the invariant α.

Discharge route: proof-phase — the stage graph, the WCET/occupancy bounds, and the invariant proper. See L3/08, L3/09.

S-isa — the ISA and system boundary

iface_L4_L5 : archBeh = isaBeh — the microarchitectural behaviour equals the ISA reference at the observable pad boundary.

Connects L4 (the ISA specification) and L5 (the system: memory map, devices, boot) up to the top-level observable isaBeh. It bundles the Sail-RISC-V model, the memory map, and the boot/observation contract into a single behaviour on pad-traces.

Below: the refinement (S-refine). Above: the top-level statement. Precursor: L5/memmap, L5/boundary, L5/b3-smoke (all PASS) — the observables are scored (the map is consistent, the boundary is the documented 18 signals, an image boots and the UART emits). What is not scored is their equality to the Sail reference at the boundary.

Discharge route: import sail-riscv at a pin (L4/sail-pin), the L3 refinement, and the L5 device models (L5/sys-models). See L4/00, L5/00. Rests on the specification-side axioms S2–S4.

S-miter — the certificate anchor

miterCNF_sound : Unsat (miterCNF lib A B) → MealyEq (denote lib A) (denote lib B) — the miter CNF faithfully encodes inequivalence of two netlists, so a refutation of it proves the machines equal.

Not an inter-layer arrow but the trust anchor every equivalence certificate rests on: each equiv is miterCNF_sound ∘ checkRefutation_sound, and l2_commutes (hence the whole middle) depends on it. Currently a trusted axiom.

Unlike E1 or the M-series, it is dischargeable: it is a statement about a Tseitin encoding, provable outright. The polarity of the emitted miter was falsification-tested in trail-cec (a wrong-polarity miter is satisfiable, so a dropped clause would show up as a spurious SAT), but that is evidence, not a proof.

Discharge route: a verified Tseitin encoding of denote into CNF, making miterCNF_sound a theorem — the clearest single "promote an assumption to a proof" target in the stack. See L2/04; in the axiom register it is the paradigm T→theorem entry.

Closing the tower

chip_realises_isa is real but conditional, and it now says precisely on what: closing the tower is discharging these seven rows and nothing else. Four are proof-phase layer work already priced in the dispatch (S-timing = M5, S-refine and S-isa = the L3/L4/L5 theorems); two are mechanical once their upstream tool exists (S-extract's LVS, S-reset's extraction); and one, S-miter, is a self-contained encoding proof that needs no artifact at all. There is no eighth, hidden seam: the composition is exhaustive by construction, because a missing arrow would leave chip_realises_isa failing to type-check, not silently unsound.