The discipline stops at the edge

A subject the papers are about. The loosest grouping, and the one to reach for last.

A timing discipline is a promise about what a circuit does not depend on. This set collects the works showing that such promises hold inside a block and are surrendered where blocks meet. Membership requires the boundary to be where the concession is made or the failure occurs, not merely somewhere the work happens to mention.

**The pattern was not stated by any member; it emerges from holding them together.** Three independent records name a different edge and give up the same thing at it:

- martin1993tomorrows reports the first asynchronous microprocessor as entirely delay-insensitive "**with the exception of isochronic forks and the interfaces with the memories**". Two exceptions: one is a wire branch, the other is where the processor meets something it did not design. - porcher2012synthese builds monitors as quasi-delay-insensitive circuits precisely so the checker survives the degradation that fells a clocked design -- and then proves that connecting such a monitor to the synchronous circuit it watches **re-imports that circuit's timing assumptions into the monitor**. The repair, clock stretching, works by reaching back and controlling the watched circuit's clock, so the observer stops being passive. - plassan2018conclusive takes clock-domain crossings as its whole subject, because a destination register may capture data mid-change: "compliance with the setup and hold time requirements is not guaranteed". A modern system-on-chip has tens of clocks, so it has tens of these edges by construction.

**The theoretical members explain why the edge is where it goes wrong.** martin1990limitations proves that a circuit depending on *no* delay assumption is almost nothing -- closed delay-insensitive circuits admit only C-elements as multiple-input operators -- and names the isochronic fork as the weakest assumption that restores usefulness. manohar1995quasidelayinsensitive shows that assumption buys back everything computable and costs the arbiter. So the concession is not sloppiness: a discipline strong enough to be worth having is too strong to survive contact, and the practical question is only where you put the seam.

**What crossing an edge costs, when someone prices it.** tarawneh2017metastability treats the two-flop synchroniser's latency as the tax on every clock-domain crossing and removes it by doing the synchronising inside the computation, confining the resulting corruption instead. bund2020synchronizerfree removes the synchroniser from a link controller outright. Both are attacks on the same tax, and plassan2018conclusive states exactly what the tax buys: stability "within a certain probability", with **no way of telling whether the stable value is the old one or the new**.

**Why this is not the same question as the-switch-or-the-curve**, which several members also belong to: that set asks how much of the device a model admits -- a question about depth. This asks where a model's guarantee stops holding -- a question about extent. A model can be exquisitely faithful to a transistor and still make no promise about what happens when its block is wired to another one.

**The gap this set named has been partly filled.** It previously ended by observing that the corpus held a great deal on proving a block correct and very little on what composing two verified blocks guarantees. garavel2009semantics is the first member to address that directly: it gives value-passing CHP a semantics that handles **channels open to the environment** -- a block whose interface is not closed off -- and independent of which handshake protocol is eventually used, then translates it into LOTOS and reports compositional verification of an asynchronous DES implementation and a network-on-chip interconnect. Open channels are the boundary problem stated as a requirement on a semantics rather than as a failure in silicon.

The assume-guarantee half of that gap is now half-closed. kastenbaum2021mechanically formalises a generic assume-guarantee contract theory in Coq and proves the theorems that make it correct, observing that contract frameworks are usually used to prove abstractions sound while the frameworks themselves had not been proved correct. That establishes the device the set was looking for -- but its subject is cyber-physical systems, in which hardware is one component type among several, and no circuit appears in it. **So the corpus holds the composition principle proved, and still holds nothing applying assume-guarantee reasoning to a circuit.** That remains the gap.