Boundary Sufficiency

Network changes are often local, but the verification work is not. A small spanning-tree configuration change can appear to require recomputing port roles across every switch, even when the affected area is separated from the rest of the network by only a few links.

The central result

This paper shows that full-network recomputation is unnecessary under a precise condition: the sub-network being checked does not contain the elected root. If a region N is separated from the rest of the network R by a boundary B, then the roles inside N depend only on its own topology and configuration, plus the root-path distances supplied at the boundary switches.

Everything else about the remote network can be discarded. The boundary acts as a compact interface between the part being changed and the part that is already known to be stable.

A denotational model of STP

The model treats STP as an executable function from a topology and configuration to a total assignment of port roles. A topology is a finite set of switches connected by links with positive costs. A configuration supplies bridge priorities, port-cost overrides, and optional RootGuard or LoopGuard settings.

Bridge identifiers elect a unique root. Once the root is known, each switch chooses a lowest-cost path toward it, with bridge identifiers and port identifiers providing deterministic tie-breakers. The resulting root, designated, and blocking roles form the active spanning tree.

Why the boundary is enough

Two observations make the decomposition work. First, when the root is in R, a shortest path from a boundary switch to the root never benefits from entering N and returning. All link costs are positive, so detouring through the isolated region can only make the path longer. Boundary distances can therefore be computed entirely within R.

Second, every shortest path from a switch in N has an equivalent path that crosses the boundary exactly once. The path can be split into an internal prefix and a shortest continuation beginning at the boundary. This gives the local computation the exact information it needs without exposing the internal structure of R.

Boundary sufficiency. If the elected root lies in R, port roles on switches in N are determined by N's topology, N's configuration, and the vector of root-path distances at B. No other information about R is required.

Diagram showing local network N connected across boundary edges to remote network R and its root. — Figure 1. A local region N can see the rest of the network R through boundary distances at B.

Mechanized in Haskell

The result was mechanized in Haskell using the same relaxation and role-assignment functions for both the monolithic computation and the local witness function. This matters because agreement cannot be dismissed as an artifact of two independently implemented algorithms.

The local function seeds the boundary switches with their known distances, then computes roles over the internal switches and cut edges. It was checked against the full computation on five structurally different cases: a six-switch ring, a minimal one-switch region, a two-arm topology, a RootGuard case, and a negative control with the root placed inside the local region.

data Weekend = Saturday | Sunday

showDay :: Weekend -> String
showDay Saturday = "Drink some coffee."
showDay Sunday   = "Think about things."

Six-switch ring benchmark split into local region N and remote region R. — Figure 2. A six-switch ring split into local region N and remote region R, with two cut edges and the root in R.

The measured speedup

Correctness was followed by a scaling measurement on a 500-switch ring with a 20-switch local region and a boundary of width two. Averaged over three trials, the full recomputation took 2,634 ms. The local computation, given the two boundary distances as fixed inputs, took 2.0 ms: roughly a 1,300x difference.

The absolute numbers come from an intentionally unoptimized reference implementation, but both paths share those inefficiencies. The relative improvement comes from never touching the remote region, exactly as the theorem predicts.

Where the guarantee fails

The precondition is load-bearing. If the root migrates into N, the effect can travel arbitrarily far through R. For every distance k, construct a chain extending k hops from the boundary. When the root is at the far end, that switch has no root port. When the root moves into N, the same switch acquires a root port toward the chain. Its role changes exactly k hops away.

This rules out any fixed-radius static guarantee in the failure case. It does not rule out incremental shortest-path algorithms that touch only switches whose distances actually change; that is a different, output-sensitive problem left for future work.

Chain construction showing a port role changing when the root migrates into local region N. — Figure 3. Root migration can change a port role arbitrarily far from the boundary.

Limitations and next steps

The model captures RootGuard and LoopGuard as configuration constraints, but it does not model every physical failure mode, such as asymmetric unidirectional loss. The mechanization uses synthetic topologies and one 500-switch benchmark rather than production data. Guard compositionality and incremental recomputation also remain open questions.

The broader lesson is deliberately narrow: general-purpose modular verification is valuable, but some protocols have enough structure to admit exact decompositions with no solver in the loop. STP is one such case. The useful engineering move is to identify the boundary, validate the precondition, and pass only the summary the local computation actually needs.