M. Moeller]Mark Moeller
Equal contribution.

Cornell University
Ithaca, NY

J. Jacobs]Jules Jacobs
[2]

Cornell University
Ithaca, NY

O. Savary Belanger]Olivier Savary Belanger

Portland, OR

D. Darais]David Darais

Portland, OR

C. Schlesinger]Cole Schlesinger

Portland, OR

S. Smolka]Steffen Smolka

Mountain View, CA

N. Foster]Nate Foster

Cornell University
Ithaca, NY

A. Silva]Alexandra Silva

Cornell University
Ithaca, NY

: A Fast Symbolic Verifier for NetKAT

We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present , an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications, and a verification engine that constructs a bisimulation or generates a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches. Our advancements underscore NetKAT's potential as a practical, declarative language for network specification and verification.

This research was developed with funding from the Defense Advanced Research Projects Agency (DARPA) and the Office of Naval Research (ONR). The views, opinions, and/or findings contained in this material are those of the authors and should not be interpreted as representing the official views or policies of the Department of the Navy, DARPA, or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation hereon. DISTRIBUTION A. Approved for public release; distribution unlimited.

§ INTRODUCTION

In the automata-theoretic approach to verification, programs and specifications are each encoded as automata, and verification tasks are reduced to standard questions in formal language theory—e.g., membership, emptiness, containment, etc. <cit.>. The approach became popular in the mid-1980s, driven by use of temporal logics and model checking in hardware verification, and it remains a powerful tool today. In particular, automata provide natural models of phenomena like transitive closure, which arises often in programs but is impossible to express in pure first-order logic.

NetKAT, a domain-specific language for specifying and verifying the behavior of network data planes, is a modern success story for the automata-theoretic approach.  NetKAT programs denote sets of traces (or “histories”) where a trace is the list of packets “seen” at each hop in the network. The NetKAT language specifies these traces using a regular expression-like syntax, as follows:

\[
p,q \Coloneqq \bot \mid \top \mid f \test v \mid f \testNE v \mid f \mut v \mid \text{dup} \mid p + q \mid p \cdot q \mid p^\star
\]

Unlike ordinary regular expressions, which are stateless, NetKAT programs manipulate state in packets. Accordingly, 's atoms are not letters, but actions that either drop or forward the current packet ($\bot$ or $\top$), modify a header field ($f \mut\, v$), test a header field against a value ($f \test v$, $f \testNE v$), or append the current packet to the trace ($\text{dup}$).
The regular expression operations copy and forward a packet to two different programs ($p + q$), sequence two programs ($p \cdot q$), or loop a program ($p^\star \equiv \top + p + p\!\cdot\!p + p\!\cdot\!p\!\cdot\!p + \cdots$).

A NetKAT program thus gives a declarative specification of the network's global behavior in terms of sets of traces. Specifically, we can model the location of a packet in the network using a special header field (usually named $\text{sw}$ for “switch”), that we can update ($\text{sw} \mut \ell$) to logically move the packet from its current location to a new location $\ell$. Given a declarative description of the intended behavior, the NetKAT compiler generates a set of local forwarding tables for individual switches that together realize the global behavior <cit.>.

Moreover, NetKAT not only plays a role as an implementation language, but also as a language for expressing verification queries, analogous to verification tools powered by SMT solvers <cit.>. In particular, as NetKAT includes a union operator (“+”), containment can be reduced to program equivalence—i.e., $p \sqsubseteq q$ if and only if $p + q \equiv q$. Hence, unlike other contemporary tools, which rely on bespoke encodings and algorithms for checking network properties like reachability, slice isolation, etc. <cit.>, NetKAT allows a wide range of practical verification questions to be answered using the same foundational mechanism, namely program equivalence. For example,

* Network Reachability: Are there any packets that
can go from location $121$ to $543$ in the network specified by the NetKAT program

$\textsf{net}$? Formally: $(\text{sw} \mut 121) \cdot \textsf{net}^\star
\cdot (\text{sw} = 543) \qequiv \zero$

* Slice Isolation: Are slices $\textsf{net}_1$ and
$\textsf{net}_2$ logically disjoint, even though their
implementation on shared infrastructure uses the same devices? Formally:
$\textsf{net}_1^\star + \textsf{net}_2^\star \qequiv (\textsf{net}_1 + \textsf{net}_2)^\star$

's $\text{dup}$ primitive is a key construct that enables reducing a wide range of network-specific properties to program equivalence. Recall that $\text{dup}$ appends the headers of the current packet to the trace. Hence, to verify properties involving the network's internal behavior, we add intermediate packets to the trace using $\text{dup}$, making them relevant for program equivalence. Conversely, if we only care about the input-output behavior of the entire network, we can omit $\text{dup}$ from the specification, so intermediate packets are not considered by the check for program equivalence.

The story so far is appealing, but there is a major fly in the ointment. To decide program equivalence, the automata-theoretic approach relies on the translation from NetKAT programs to automata. But standard NetKAT automata have an enormous space of potential transitions—i.e., the “alphabet” has a “character” for every possible packet. So using textbook algorithms for building automata and checking equivalence would clearly be impractical. In fact, NetKAT equivalence is PSPACE-complete <cit.>. Instead, what's needed are symbolic techniques for encoding the state space and transition structure of NetKAT automata that avoid combinatorial blowup in the common case.

Prior work on symbolic automata provides a potential solution to the problems that arise when working with large (or even infinite)
alphabets. The idea is to describe the transitions in the automata using logical formulas <cit.> or Binary Decision Diagrams (BDDs) <cit.> rather than concrete characters. Algorithms such as membership, containment, and equivalence can then be reformulated to work with these symbolic representations. Symbolic automata have been successfully applied to practical problems such as building input sanitizers for Unicode, which has tens of thousands of characters <cit.>. However, 's richer semantics precludes the direct adoption of standard notions of symbolic automata. In particular, 's transitions describe not only predicates but also transformations on the current packet. As Pous writes, it “seems feasible” to generalize his work to NetKAT, but
“not straightforward” <cit.>.

In this paper, we close this gap and develop symbolic techniques for checking program equivalence for NetKAT. In doing so, we address three key challenges:

Challenge 1: Expressive but Compact Symbolic Representations

The state space and transitions of NetKAT automata are very large due to the way the “alphabet” is built from the space of all possible packets. Orthogonally, these characters also encode packet transformations, as reflected in 's packet-processing semantics. It is crucial that the symbolic representations for NetKAT programs be compact and admit efficient equivalence checks.

Challenge 2: Extended Logical Operators

In the tradition of regular expressions, NetKAT only includes sequential composition ($e_1 \cdot e_2$) and union operators ($e_1 +
e_2$)—the latter computes the union of the sets of traces described by $e_1$ and $e_2$. However, when verifying network-wide properties it is often useful to have operators for intersection ($e_1 \cap e_2$), difference ($e_1 \setminus e_2$), and symmetric difference ($e_1
\oplus e_2$). Having native support for these operators at the level of syntax and in equivalence checking algorithms allows the reduction of all verification queries to an emptiness check—e.g., $A \equiv B$
reduces to $A \oplus B \equiv \zero$, and $A \sqsubseteq B$ reduces to $A \setminus B \equiv \zero$.

Challenge 3: Support for Counter-Examples

When an equivalence check fails, it can be hard to understand the cause of the failure, and which changes might be needed to resolve the problem. It is therefore important to be able to construct symbolic counter-examples that precisely capture the input packets and traces that cause equivalence to fail.

In addressing the above challenges, we make the following technical contributions:

Contribution 1: Efficient symbolic representations (<Ref>).

We design a symbolic data structure called Symbolic Packet Programs (s) for representing both sets of packets and transformations on packets in a symbolic manner. s generalize classic BDDs and are asymptotically more efficient than the representations used in prior work on NetKAT. In particular, s support efficient sequential composition ($e_1 \cdot e_2$) and can be made canonical which, with hash consing, allows us to check equivalence of s in constant time.

Contribution 2: Symbolic Brzozowski derivatives (<Ref>).

We introduce a new form of symbolic Brzozowski derivative to produce automata for NetKAT programs.
Our approach naturally and efficiently supports the extended “negative” logical operators mentioned above, in contrast to prior approaches that only support “positive” operators like union.

Contribution 3: Symbolic bisimilarity checking (<Ref>).

Building on the foundation provided by s and deterministic NetKAT automata, we develop symbolic algorithms for checking bisimilarity. We present a symbolic version of the standard algorithm that searches in the forward direction through the state space of the automata under consideration. We also present a novel backward algorithm that computes symbolic counter-examples to equivalence—i.e., the precise set of input packets for which equivalence fails.

Contribution 4: implementation (<Ref>) and evaluation (<Ref>).

Finally, we present a new verification tool, called , implemented in Scala.  implements symbolic bisimilarity checking, including an extended set of extended logical operators, as well as symbolic counter-examples.  We evaluate the performance of  on a variety of real-world topologies, and show that it efficiently answers a variety of verification queries and scales to much larger networks than prior work. Due to its use of our efficient data structures,  is several orders of magnitude faster than prior implementations of NetKAT on these realistic examples. Moreover,  is faster than prior work on synthetic combinatorial benchmarks by arbitrary large factors.

§ EXPRESSIONS AND AUTOMATA

This section reviews basic definitions for to set the stage for the new contributions presented in the subsequent sections.
is a language for specifying the packet-forwarding behavior of network data planes <cit.>.[Networks have a control plane, which computes paths through the topology using distributed routing protocols (or a software-defined networking controller), and a data plane, which implements paths using high-speed hardware and software pipelines. NetKAT models the behavior of the latter.]  The syntax and semantics of is presented in <Ref>, and is based on Kozen's Kleene Algebra with Tests (KAT) <cit.>.

Syntax     Description     Semantics

$p,q \Coloneqq $         $\Sem{p}(\alpha\!:\!\Pk) : \pow{\Pk^+} =$

$\mid\quad \bot$     False     $\emptyset$

$\mid\quad \top$     True     $\{ \alpha \}$

$\mid\quad f \test v$     Test equals     $\text{ if } \alpha_f = v \text{ then }  \{ \alpha \} \text{ else } \emptyset$

$\mid\quad f \testNE v$     Test not equals     $\text{ if } \alpha_f \neq v \text{ then } \{ \alpha \} \text{ else } \emptyset$

$\mid\quad f \mut\, v$     Modification     $\{ \alpha[f \mut\, v] \}$

$\mid\quad \text{dup}$     Duplication     $\{ \alpha\alpha \}$

$\mid\quad p + q$     Union     $\Sem{p}(\alpha) \cup \Sem{q}(\alpha)$

$\mid\quad p \cdot q$     Sequencing     $\{ \mathbf{a}\mathbf{b} \mid \mathbf{a}\beta \in \Sem{p}(\alpha),\ \mathbf{b} \in \Sem{q}(\beta) \}$

$\mid\quad p^\star$     Iteration     $\bigcup\limits_{n\geq 0} \Sem{p^n}$

Values $v \Coloneqq 0 \mid 1 \mid \ldots \mid n$
Fields $f \Coloneqq f_1 \mid \ldots \mid f_k$
Packets $\pk \Coloneqq \{f_1 = v_1, \ldots, f_k = v_k\}$

NetKAT syntax and semantics.

To a first approximation, can be thought of as a simple, imperative language that operates over packets, where a packet
is a finite record assigning values to fields. The basic primitives in are packet tests ($f \test v$, $f \testNE v$) and packet modifications ($f\mut v$). Program expressions are then compositionally built from tests and packet modifications, using union ($+$), sequencing ($\cdot$), and iteration ($\star$).  Conditionals and loops can be encoded in the standard way:

\[
\textbf{if } b\textbf{ then } p  \textbf{ else } q \triangleq b \cdot p + \neg b \cdot q \qquad\qquad
\textbf{while } b\textbf{ do } p   \triangleq (b \cdot p)^\star \cdot \neg b.
\]

In a network, conditionals can be used to model the behavior of the forwarding tables on individual switches while iteration can be used to model the iterated processing performed by the network as a whole;
the original paper on NetKAT provides further details <cit.>. Note that assignments and tests in are always against constant values.  This is a key restriction that makes equivalence decidable and aligns with the capabilities of data plane hardware. The $\text{dup}$ primitive makes a copy of the current packet and appends it to the trace, which only ever grows as the packet goes through the network. This primitive is crucial for expressing network-wide properties, as it allows the semantics to
“see” the intermediate packets processed on internal switches.

's formal semantics, given in <Ref>, defines the action of a program on an input packet $\alpha$, producing a set of output traces.  The semantics for $\top$ gives a single trace containing the single input packet $\alpha$, whereas $\bot$ produces no traces.  Tests ($f \test v$ and $f \testNE v$) produce a singleton trace or no traces, depending on whether the test succeeds or fails. Modifications ($f \mut v$) produce a singleton trace with the modified packet.  Duplication ($\text{dup}$) produces a single trace with two copies of the input packet.  Union ($p + q$) produces the union of the traces produced by $p$ and $q$.  Sequential composition ($p \cdot q$)
produces the concatenation of the traces produced by $p$ and $q$, where the last packet in output traces of $p$ is used as the input to $q$. Finally, iteration ($p^\star$) produces the union of the traces produced by $p$ iterated zero or more times.
Consider the following example:

\begin{align*}
(x \test 0 \cdot x \mut 1 \cdot \text{dup}\ +\ x \test 1 \cdot x \mut 0 \cdot \text{dup})^\star
\end{align*}

This program repeatedly flips the value of $x$ between $0$ and $1$, and traces the packet at each step. On input packet $x\test 0$, it produces the following traces:

\begin{align*}
\{ [x\test0], [x\test 0, x\test 1], [x\test 0, x\test 1, x\test 0], [x\test 0, x\test 1, x\test 0, x\test 1], \ldots \}
\end{align*}

Consider what happens if we change the program to $(x \test 0 \cdot x \mut 1 \cdot \text{dup}\ +\ x \mut 0 \cdot \dup)^\star$.
Unlike the previous example, where the tests were disjoint, this program can generate multiple outputs for a given input packet, as the right branch of the union can always be taken, leading to sequences $x\test 0, x\test 0, \ldots$. On the other hand, if the $x \mut 1$ assignment is performed, then the left branch cannot be taken the next time, because the test $x \test 0$ will fail. Hence, the program produces traces with sequences of $x \test 0$ packets, with singular $x \test 1$ packets between them.

As these simple examples show, despite the fact that assignments and tests in NetKAT programs are always against constant values, the behavior of NetKAT programs can be complicated, particularly when conditionals, iteration, and multiple packet fields are involved.

Traditional presentations of NetKAT distinguish a syntactic test fragment that includes negation:

\begin{align*}
t,r &\Coloneqq \bot \mid \top \mid f \test v \mid t \lor r \mid t \land r \mid \neg t \tag{Test fragment}\\
p,q &\Coloneqq t \mid f \mut\, v \mid p + q \mid p \cdot q \mid \text{dup} \mid p^\star \tag{General expressions}
\end{align*}

This distinction is necessary because negation $\neg p$ only makes sense on the test fragment.
We replace general negation $\neg t$ in our presentation with only negated field tests $f \testNE v$. There is no loss of generality—we translate a test fragment expression $t$ to $[t]_0$ using the DeMorgan rules:

\begin{align*}
[\bot]_0 &= \bot\\
[\top]_0 &= \top\\
[f \test v]_0 &= (f \test v)
\end{align*}

\begin{align*}
[t \lor r]_0 &= [t]_0 + [r]_0\\
[t \land r]_0 &= [t]_0 \cdot [r]_0\\
[\neg t]_0 &= [t]_1
\end{align*}

\begin{align*}
[\bot]_1 &= \top\\
[\top]_1 &= \bot\\
[f \test v]_1 &= (f \testNE v)
\end{align*}

\begin{align*}
[t \lor r]_1 &= [t]_1 \cdot [r]_1\\
[t \land r]_1 &= [t]_1 + [r]_1\\
[\neg t]_1 &= [t]_0
\end{align*}

Conditional dup, equivalence, and subsumption
An interesting feature of NetKAT is that dup need not appear the same number of times on all paths through the expression.
Consider the program $(f \mut\, v + f \mut\, w + \mathsf{dup})^\star$, which either sets field $f$ to $v$ or to $w$, or logs the packet to the trace, and then repeats.
Any number of writes can happen between two dups, and only the effect of the last write before the dup gets logged to the trace.
This is allowed and fully supported by .

The use of dup controls the type of equivalence that is checked.
If we insert a dup after every packet field write, then we obtain trace equivalence.
If we insert no dups whatsoever, we obtain input-output equivalence.
By inserting dups in some places but not others, we can control the equivalence that is checked in a fine-grained manner.

In addition to $p \equiv q$, we may want to check inclusion $p \sqsubseteq q$.
This can be expressed as $p + q \equiv q$ or equivalently, in , as $p \setminus q \equiv \bot$.
As before, the number of dups controls the type of inclusion that is checked: from trace inclusion to input-output inclusion, or something in between.

§.§ Automata

's semantics induce an equivalence $(p \equiv q) \triangleq (\Sem{p} = \Sem{q})$ on syntactic programs.  This equivalence is decidable, and can be computed by converting programs to automata and checking for automata equivalence. To convert programs to automata, the standard approach is to use Antimirov derivatives.  We do not give the details here, but the interested reader can find them in <cit.>, and for our symbolic automata, in <Ref>.  We continue with a brief overview of automata and how to check their equivalence.  A automaton $(S, s_0, \left<\epsilon, \delta\right>)$ consists of a set of states $S$, a start state $s_0$, and a pair of functions that depend on an input packet:

\[
\epsilon : S \times \Pk \to 2^\Pk \qquad\qquad  \delta : S\times\Pk \to S^\Pk
\]

Intuitively, the observation function $\epsilon$ is analogous to the notion of a final state, and models the output packets produced from an input packet at a given state. The transition function $\delta$
models the state transitions that can occur when processing an input packet at a given state. Because transitions can modify the input packet, the transition structure $\delta(s,\pk)$ is itself a function of the modified packet, and tells us to transition to state $\delta(s,\pk)(\pk')$ when input packet $\pk$ is modified to $\pk'$.

In terms of the semantics, a transition in the automaton corresponds to executing to the next dup in a NetKAT program, and appends the current packet to the trace.  It should also be noted that states in the automaton do not necessarily correspond to network devices;
because the location of the packet is modeled as just a field in the packet, there can be states in the automaton that handle packets from multiple devices, and the packets of a device can be handled by multiple states.

Carry-on packets
Unlike traditional regular expressions and automata, NetKAT is stateful, and the output packet of a transition is carried on to the next state.  This makes NetKAT fundamentally different from traditional regular expressions, resulting in challenges in the semantics (which is not a straightforward trace or language semantics) and in designing equivalence procedures, as they have to account for the carry-on packet. Technically it would be possible to fold the packet into the state of the automaton and approach the semantics and the problem of checking equivalence using classical automata. However, because the number of possible packets is exponential in the number of fields and values, such conversion results in enormous state blowup and is therefore impractical.

Input: A pair of NetKAT automata $(S, s_0, \delta, \epsilon)$, $(S', s'_0, \delta', \epsilon').$
Returns: A Boolean indicating whether the automata are equivalent.
$W \gets \{ (s_0, s'_0, \pk) \mid \pk \in \Pk \}$;
$W$ changes
$(s,s',\pk) \in W$
$\epsilon(s, \pk) \neq \epsilon'(s', \pk)$
$W \gets W \cup \{ (\delta(s, \pk)(\pk'), \delta'(s', \pk)(\pk'), \pk') \mid \pk' \in \Pk \}$

Bisimulation algorithm à la Hopcroft & Karp <cit.>

§.§ Bisimulation of NetKAT Automata

automata can be used to decide $p \equiv q$.  Intuitively, while traces may be infinite, transitions only depend on the current packet, which has a finite number of distinct possible values.

Given two automata $(S, s_0, \left<\epsilon, \delta\right>)$ and $(S', s'_0, \left<\epsilon', \delta'\right>)$, we check their equivalence by considering all possible input packets separately. We run the two automata in parallel, starting from an input packet $\pk$ at their respective start states. We first check that the immediate outputs $\epsilon(s_0, \pk)$ and $\epsilon'(s'_0, \pk)$ are the same. If so, we check that the transitions $\delta(s_0, \pk)$ and $\delta'(s'_0, \pk)$ are equivalent, by recursively checking the equivalence of the states $\delta(s_0, \pk)(\pk')$ and $\delta'(s'_0, \pk)(\pk')$ for all $\pk'$.

We can implement this strategy using a work list algorithm. The work list contains triples $(s, s', \pk)$, where $s$ and $s'$ are states in the two automata, and $\pk$ is an input packet. Initially, the work list contains $(s_0, s'_0, \pk)$ for all packets $\pk$. We then repeatedly take triples $(s, s', \pk)$ from the work list, and check that $\epsilon(s, \pk) = \epsilon'(s', \pk)$ and add $(\delta(s, \pk)(\pk'), \delta'(s', \pk)(\pk'), \pk')$ to the work list for all $\pk'$. If at any point we find that $\epsilon(s, \pk) \neq \epsilon'(t, \pk)$, then the automata are not equivalent. If the work list stabilizes, the automata are equivalent. This algorithm is shown in <Ref>.

Of course, the issue with this algorithm is that the space of packets is huge. The rest of this paper develops techniques for working with symbolic representations of packets and automata, allowing us to represent and manipulate large sets of packets and to efficiently check equivalence of automata without explicitly enumerating the space of packets.

§ SYMBOLIC REPRESENTATIONS

In this section, we develop symbolic techniques to trace an entire set of packets at once, vastly reducing the number of iterations required to compute a bisimulation in practice. These techniques will allow us to revise the approach of <Ref> with a much more efficient version in <Ref>.

First, we introduce a representation for symbolic packets, which represent sets of packets, or equivalently, the fragment of where all atoms are tests. This representation is essentially a natural n-ary variant of binary decision diagrams (BDDs) <cit.>. Second, we introduce Symbolic Packet Programs (s), a new representation for symbolic transitions in NetKAT automata, representing the $\text{dup}$-free fragment of —i.e., the fragment in which all atoms are tests or assignments. The primary challenge is to design this representation so that it is efficiently closed under the NetKAT operations. Furthermore, we need to be able to efficiently compute the transition of a symbolic packet over a , both forward and backward.

* $p + q$

Examples of $\SP$s, where $p \triangleq (a\test3 \cdot b\test4 \mathrel{+} b \testNE 5 \cdot c\test5)$ and $q \triangleq (b=3 \cdot c\test4 \mathrel{+} a\test5 \cdot c \testNE 5)$.

§.§ Symbolic Packets

We begin by choosing a representation for symbolic packets. A symbolic packet $p \subseteq \Pk$ is a set of concrete packets, represented compactly as a decision diagram. Syntactically, symbolic packets are NetKAT expressions with atoms restricted to tests, represented in the following canonical form:

\begin{align*}
p \in \SP \Coloneqq \bot \mid \top \mid
\underbrace{\SP(f, \ \{ \ldots, v_i \mapsto q_i, \ldots \},\ q)}_{\equiv \ \ \sum_i f \test v_i \cdot q_i\ +\ (\prod_i f \testNE v_i)\cdot q}
\end{align*}

That is, symbolic packets form an n-ary tree, where each child $q_i$ is labeled with a test of the current field $f$, and the default case $q$ is labeled with the negation of the other tests. Hence, a given concrete packet has a unique path through the tree.

The following conditions need to be satisfied for a symbolic packet to be in canonical form, inspired by the analogous properties of BDDs:

Reduced If a child $q_i$ is equal to the default case $q$, it is removed. If only the default case remains, the symbolic packet is reduced to the default case itself.

Ordered A path down the tree always follows the same order of fields,
and the children $q_i$ are ordered by the value $v_i$.

These conditions ensure the representation of a symbolic packet is unique, in the sense that two symbolic packets are semantically equal if and only if they are syntactically equal.

As with BDDs, we share nodes in the tree, making the representation of a symbolic packet a directed acyclic graph, as shown in <Ref>. Vertices are labeled with the packet field they test. Solid arrows labeled with a number encode the test value, and dashed arrows represent a default case. The sinks of the graph are labeled with $\top$ or $\bot$, indicating membership in the set.  On the left, we have a symbolic packet representing all packets where $a=3$ and $b=4$, or $b \neq 5$ and $c = 5$.  In the middle, we have a symbolic packet representing all packets where $a=3$ and $c=4$, or $a=5$ and $c \neq 5$.  On the right, we have the union of these symbolic packets.

\[
\begin{array}{ll}
\textbf{Primitive tests:}\\
\quad (f \test v) \triangleq \SP(f, \{v \mapsto \top\}, \bot) \qquad (f \testNE v) \triangleq \SP(f, \{v \mapsto \bot\}, \top)\\
\textbf{Operations, base cases:}\\
\quad \top \plusop \top \triangleq \top \quad \top \cdotop \top \triangleq \top \quad \top \capop \top \triangleq \top \quad \top \oplusop \top \triangleq \bot \quad \top \minusop \top \triangleq \bot\\
\quad \top \plusop \bot \triangleq \top \quad \top \cdotop \bot \triangleq \bot \quad \top \capop \bot \triangleq \bot \quad \top \oplusop \bot \triangleq \top \quad \top \minusop \bot \triangleq \top\\
\quad \bot \plusop \top \triangleq \top \quad \bot \cdotop \top \triangleq \bot \quad \bot \capop \top \triangleq \bot \quad \bot \oplusop \top \triangleq \top \quad \bot \minusop \top \triangleq \bot\\
\quad \bot \plusop \bot \triangleq \bot \quad \bot \cdotop \bot \triangleq \bot \quad \bot \capop \bot \triangleq \bot \quad \bot \oplusop \bot \triangleq \bot \quad \bot \minusop \bot \triangleq \bot\\
\textbf{Operations, inductive case:}\\
\quad \SP(f, b_p, d_p)\pmop \SP(f, b_q, d_q) \triangleq  \spsc(f,b'\!,d_p \pmop  d_q)\\
\quad\quad \text{ where }\  b' = \{v \mapsto b_p(v;d_p) \pmop b_q(v;d_q) \mid v\in \keys(b_p \cup b_q)\}\\
\textbf{Expansion:}\\
\quad p \equiv \SP(f, \emptyset, p) \text {\qquad if \qquad} p \in \{\top, \bot, \SP(f', b, d)\} \text{ where } f \sqsubset f'\\
\textbf{Smart constructor:}\\
\quad \spsc(f,b,d) \triangleq
\text{ if } b' = \emptyset \text{ then } d \text{ else } \SP(f, b', d)\\
\qquad \text{where } b' \triangleq \{v \mapsto p \mid v \mapsto p \in b, p \neq d\}
% \quad \spsc(f,b,d) \triangleq \begin{cases}
%   \SP(f, b', d) &\text{ if } b' \triangleq \{v \mapsto p \mid v \mapsto p \in b, p \neq d\} \neq \emptyset\\
%   d &\text{ if } b' = \emptyset
% \end{cases}
\end{array}
\]

Definition of the $\SP$ operations. The inductive case is identical for all operations (indicated by $\pmop$), and applies when both $\SP$s test the same field. Expansion inserts a trivial $\SP$ node to reduce the remaining cases to the inductive case. The notation $b(v;d)$ means the child $b(v)$ if $v \in \keys(b)$, or the default case $d$ otherwise.

Symbolic packets are closed under the NetKAT operations:

\begin{align*}
\nf{+}, \nf{\cdot}, \nf{\cap}, \nf{\oplus}, \nf{-}\ :\ \SP \times \SP \to \SP \qquad
\nf{\star}\ :\ \SP \to \SP \qquad
f \test v, f \testNE v\ :\ \SP
\end{align*}

As defined in <Ref>, operations on symbolic packets are computed by traversing the two trees in parallel, recursively taking the operation of the children, making sure to maintain canonical form using the smart constructor. Repetition $p^\star \triangleq \top$ is trivial for symbolic packets.
All other operations are defined in app:sp_ops.

Each of these operations is uniquely specified by two correctness conditions:

* They semantically match their counterpart: $\Sem{p \mathop{\nf{+}} q} = \Sem{p + q}$ for all $p,q \in \SP$.

* They maintain canonical form: $p \mathop{\nf{+}} q$ is reduced and ordered if $p,q$ are.

For further formal treatment of SPs, see app:sp_ops.

* $p \cdot q$

* $(p \oplus q)^\star$

Examples of s, where $p \triangleq (a \test 5 + b \test 2) \cdot (b \mut 1 + c \test 5)$, and $q \triangleq (b \test 1 \mathrel{+} c \mut 4 \mathrel{+} a \mut 1 \cdot b \mut 1)$.

§.§ Symbolic Transitions

We now introduce a representation for symbolic transitions in NetKAT automata.  Whereas symbolic packets represent the fragment of NetKAT where all atoms are tests, symbolic transitions correspond to the larger dup-free fragment, where all atoms are tests or assignments. This introduces additional challenges for a canonical representation, as well as for the operations. For instance, sequential composition is no longer equivalent to intersection, and the star operator is no longer trivial.

\begin{align*}
p \in \SPP \Coloneqq\ &\bot \mid \top \mid
\underbrace{
\SPP(f, \{ \ldots, v_i \mapsto \{ \ldots, w_{ij} \mapsto q_{ij}, \ldots \}, \ldots \}, \{ \ldots, w_i \mapsto q_i, \ldots \}, q)
\equiv\ \ \sum_i f \test v_i \cdot \sum_j f \mut w_{ij} \cdot q_{ij}\ +\ \
(\prod_i f \testNE v_i) \cdot (\sum_i f \mut w_i\ +\ (\prod_i f \testNE w_i) \cdot q)
% \\
% & \Sigma_m (f = v_m) \cdot \Sigma_\ldots + f \mut w_{m}^{k_m} \cdot p_{m}^{k_m})\ + \ldots ) + \\
% & (f \neq v_0 \cdots f \neq v_n) \cdot (\ldots + f \mut w_{n+1}^{k_{m}} \cdot p_{n+1}^{k_{m}}\ + \ldots + f \neq w_{n+1}^{0} \cdots f \neq w_{n+1}^{k_{n+1}}  \cdot p_{n+1}^{k_{n+1}+1})
% & (f = v_0) \cdot (f \mut w_{0}^{0} \cdot p_{0}^{0} + \ldots + f \mut w_{0}^{k_0} \cdot p_{0}^{k_0})\ + \\
% & \cdots \\
% & (f = v_n) \cdot (f \mut w_{n}^{0} \cdot p_{n}^{0} + \ldots + f \mut w_{n}^{k_n} \cdot p_{n}^{k_n})\ + \\
% & (f \neq v_0 \cdots f \neq v_n) \cdot (f \mut w_{n+1}^{0} \cdot p_{n+1}^{0} + \ldots + f \mut w_{n+1}^{k_{n+1}} \cdot p_{n+1}^{k_{n+1}}\ + \\
% & \phantom{(f \neq v_0 \cdots f \neq v_n) \cdot\ \ \ } f \neq w_{n+1}^{0} \cdots f \neq w_{n+1}^{k_{n+1}}  \cdot p_{n+1}^{k_{n+1}+1})
\end{align*}

Like SPs, s have two base cases, $\top$ and $\bot$. Also like SPs, s test a field $f$ of the input packet against a series of values $v_0,\dots,v_n$, with a default case $f \testNE v_0 \cdots f \testNE v_n$. However, instead of continuing recursively after the test, s non-deterministically assign a value $w_{ij}$ to the field $f$ of the output packet, and continue recursively with the corresponding child $q_{ij}$. This way, s can output more than one packet for a given input packet, and can also output packets with different values for the same field. The default case is further split into two cases, one where the field $f$ is non-deterministically assigned a new value (like in the other cases), and an identity case where the field $f$ keeps the same value as the input packet. However, the packet for the latter case is not produced when the input packet's field $f$ had a value that could also be produced by the explicit assignments in the default case. This ensures that for a given input packet, a given output packet is produced by a unique path through the .

The following conditions need to be satisfied for a  to be in canonical form:

Reduced If a child $q_{ij}$ is equal to $\bot$, it is removed (with
the exception of the default-identity case, which is always kept).  If one
of the default-assignment cases for a value $w$ is $\bot$, it is removed,
but to keep the behavior equivalent, an additional test for the same value
$w$ is added, with an empty sequence of assignments (if a test for the value
$w$ was already present, nothing is added).  Further, each of the
non-default cases is analyzed, and if we determine that it behaves
semantically like the default case for that input value, then it is removed.
If only the default case remains, the  is reduced to the default case

Ordered A path down the tree always follows the same order of fields,
and both the tests and the assignments are ordered by the value $v_i$ or

These conditions ensure the representation of a  is unique, in the sense that two s are semantically equal if and only if they are syntactically equal.

Like symbolic packets, we represent s as a directed acyclic graph, with duplicate nodes shared. Examples of s are shown in <Ref>. Vertices are labeled with the packet field that they test. Solid arrows labeled with a number represent the tests, and dashed arrows represent the default case. Each test is followed by a non-deterministic assignment of a new value to the field, indicated by the small diamonds. In the default case, the non-deterministic assignment also has an identity case (keeping the value of the field unchanged), indicated by a dashed arrow emanating from the diamond.

Consider the action of the first  in <Ref> on the concrete packet $a \test 5 \cdot b \test 3 \cdot c \test 5$. The first test $a \test 5$ succeeds, and the field $a$ is assigned the value $5$. The $b$ field is then tested, but the $b$ node only has a default case. The default case does have a non-deterministic assignment, which can set the $b$ field to the new value $1$, or it can keep the old value $3$. In case the new value of $b$ is $1$, the packet is immediately accepted by the $\top$ node, so the packet $a \test 5 \cdot b \test 1 \cdot c \test 5$ is produced. In case the old value of $b$ is kept, the $c$ field is tested, and in our case the value of the $c$ field is $5$. In this case, the value of the field is unchanged, and the packet $a \test 5 \cdot b \test 3 \cdot c \test 5$ is produced. In summary, for input packet $a \test 5 \cdot b \test 3 \cdot c \test 5$, the  produces packets $a \test 5 \cdot b \test 1 \cdot c \test 5$ and $a \test 5 \cdot b \test 3 \cdot c \test 5$.

When we sequentially compose the two s on the left, we get the third  shown.  In other words, if we take a concrete packet, and first apply the first , and then apply the second  to all of the resulting packets, then we get the same result as if we apply the  on the right directly to the concrete packet. Sequential composition is a relatively complex operation, but algorithmically it is a key strength of our representation and reduced/ordered invariant. To understand why, consider taking a concrete packet, and applying the first  to it.  Once we have applied the $a$-layer of the  to the packet, we already know what the value of the $a$ field in the output packet will be.  We can therefore immediately continue with the $a$ layer of the second , without having to consider the other layers of the first .  This is in contrast to a naive algorithm, which would have to consider the entire first  before being able to apply the second .  This property makes it possible to compute the sequential composition of two s efficiently in practice, and is a key contributor to the performance and scalability of our system.

\[
\begin{array}{ll}
\textbf{Primitive tests and mutation:}\\
\quad (f \test v) \triangleq \SPP(f, \{v \sto \{ v \sto \top \} \}, \emptyset, \bot) \qquad \text{\smash{\raisebox{-0.4\normalbaselineskip}{$(f \mut\, v) \triangleq \SPP(f, \emptyset, \{v \sto \top \}, \bot)$}}}\\
\quad (f \testNE v) \triangleq \SPP(f, \{v \sto \{ v \sto \bot \} \}, \emptyset, \top)\\
\textbf{Operations, base cases:}\\
\quad \textit{ Identical to those in \Cref{fig:spops}.}\\
\textbf{Operations, inductive cases:}\\
\quad \SPP(f, b_p, m_p, d_p)\pmop \SPP(f, b_q, m_q, d_q) \triangleq  \sppsc(f,b'\!,m_p \mathop{\vec{\pm}} m_q,d_p \pmop  d_q)\\
\whereindent \text{ where }\  b' = \{v \sto \get{p}{v} \mathop{\vec{\pm}} \get{q}{v} \mid v\in \keys(b_p \cup b_q \cup m_p \cup m_q) \}\\
\quad \SPP(f, b_p, m_p, d_p)\cdotop \SPP(f, b_q, m_q, d_q) \triangleq  \sppsc(f,b'\!,m_A \mathop{\vec{+}} m_B, d_p \cdotop  d_q)\\
\whereindent \text{ where }\  b' = \{v \sto \unionmaps{v'\! \sto p' \in \get{p}{v}}{ \{ w'\! \sto p' \nf{\cdot} q' \mid w'\! \sto q' \in \get{q}{v'}\} } \mid v\in \keys(b_p \cup b_q \cup m_p \cup m_q \cup m_A)\}\\
\whereindent \phantom{\text{ where }}\  m_A = \unionmaps{v'\! \sto p' \in m_p}{ \{ w'\! \sto p' \nf{\cdot} q' \mid w'\! \sto q' \in \get{q}{v'}\} },
\quad m_B = \{ w'\! \sto d_p \nf{\cdot} q' \mid w'\! \sto q' \in m_q \} \\
\quad m_1 \mathop{\vec{\pm}} m_2 \triangleq \{v \,\sto\, m_1(v;\bot) \pmop m_2(v;\bot) \mid v\in \keys(m_1 \cup m_2)\},
\quad  \vec{\Sigma} \triangleq \text{$n$-ary sum w.r.t. $\vec{+}$}\\
% if branches.contains(v) then branches(v)
% else if other.contains(v) || (id eq False) then other
% else other + (v -> id)
\quad \get{p}{v} \triangleq b_p(v; \text{ if } v \in m_p \lor d_p = \bot \text{ then } m_p \text{ else } m_p \cup \{ v \sto d_p \}) \text{\quad (similarly for $q(v)$)}\\
\textbf{Expansion:}\\
\quad p \equiv \SPP(f, \emptyset, \emptyset, p) \text {\qquad if \qquad} p \in \{\top, \bot, \SPP(f'\!, b, m, d)\} \text{ where } f \sqsubset f'\\
% \textbf{Push and pull:}\\
% \quad \mathsf{push}(p, q) \triangleq \mathsf{fwd}(\bar{p} \cdotop q), \quad \mathsf{fwd(\top) \triangleq \top},\quad \mathsf{fwd}(\bot) \triangleq \bot\\
% %
% \quad \mathsf{fwd}(\SPP(f, b, m, d)) \triangleq \spsc(f, b_A\ \vec{+}\ b_B, \mathsf{fwd}(d))\\
% \whereindent \text{ where }\  b_A = \{ v' \sto \mathsf{fwd}(p') \mid v' \sto p' \in m \}\ \vec{+} \unionmaps{v' \sto m' \in b}{ \{ w' \sto \mathsf{fwd}(p') \mid w' \sto p' \in m' \} }\\
% \whereindent \phantom{\text{ wh }}\  b_B = \{ v' \sto \mathsf{fwd}( d) \mid v' \in \keys(b_A) \setminus \keys(b \cup m) \}\ \vec{+}\
%     \{ v' \sto \bot \mid v' \in \keys(b \cup m) \setminus \keys(b_A) \}\\[1mm]
% %
% \quad \mathsf{pull}(p, q) \triangleq \mathsf{bwd}(p \cdotop \bar{q}), \qquad\! \mathsf{bwd}(\top) \triangleq \top,\quad\ \ \mathsf{bwd}(\bot) \triangleq \bot\\
% \quad \mathsf{bwd}(\SPP(f, b, m, d)) \triangleq \spsc(f, b', d' \plusop \mathsf{bwd}(d))\\
% \whereindent \text{ where }\  d' = \Sigma_{v' \sto p' \in m} \mathsf{bwd}(p')\\
% \whereindent \phantom{\text{ where }}\  b' = \{ \Sigma_{w' \sto p' \in m'} \mathsf{bwd}(p') \mid v' \sto m' \in b \} \plusop \{ v \sto d' \mid v \in \keys(m) \setminus \keys(b) \}\\
% \textbf{Smart constructor:}\\
% \quad \sppsc(f,b,m,d) \triangleq
%   d \text{ if } m' = \emptyset \land b'' = \emptyset \text{ else } \SPP(f, b'', m', d)\\
% \quad \text{ where }\  m' = \{ v \sto p \mid v \sto p \in m \land p \neq \bot \}\\
% \quad \phantom{\text{ where }}\  b' = \{ v \sto \{ w \sto p \mid w \sto p \in m \land p \neq \bot \} \mid v \sto m \in b \} \cup \{ v \sto \emptyset \mid v \sto \bot \in m \land v \notin b \}\\
% \quad \phantom{\text{ where }}\  b'' = \{ v \sto m \mid v \sto m \in b' \land m \neq (\text{if } v \in m' \lor d = \bot \text{ then } m' \text{ else } m' \cup \{ v \sto d \}) \}\\
\textbf{Repetition:}\\
\quad p^\star \triangleq \nf{\Sigma}_i p^i = \top \plusop p \plusop p \!\nf{\cdot}\! p \plusop p \!\nf{\cdot}\! p \!\nf{\cdot} \!p \plusop \ldots \text{\quad\ \ (sums in $\SPP$ converge in a finite number of steps)}
\end{array}
\]

Definition of the $\SPP$ operations. The inductive case is identical for all operations (indicated by $\pmop$), except $\cdotop$, which is given separately. Expansion inserts a trivial $\SPP$ node to reduce the remaining cases to the inductive case. The notation $b(v;d)$ means the child $b(v)$ if $v \in \keys(b)$, or by default $d$ otherwise.

s are closed not just under sequential composition, but under all of the NetKAT operations.  These operations are largely mechanical, but more complex than for SPs, as we need to take assignments into account while respecting the conditions that ensure uniqueness.  In particular, sequential composition is no longer equivalent to intersection, as the assignments in the first  clearly affect the tests in the second .  Furthermore, the star operator is no longer trivial, as the assignments in the  can affect the tests in the  itself, and a fixed point needs to be taken. We have the following operations on s:

\begin{align*}
\nf{+}, \nf{\cdot}, \nf{\cap}, \nf{\oplus}, \nf{-}\ :\ \SPP \times \SPP \to \SPP \qquad
\nf{\star}\ :\ \SPP \to \SPP \qquad
f \test v, f \testNE v, f \mut v \ :\ \SPP
\end{align*}

Push and pull
In addition to these operations for combining s, we also have the following operations, which “push” and “pull” a symbolic packet through a :

\begin{align*}
\mathsf{push} :\ \SP \times \SPP \to \SP \qquad\qquad
\mathsf{pull} :\ \SPP \times \SP \to \SP
\end{align*}

The push operation computes the effect of a  on a symbolic packet, giving a symbolic packet as a result. The new symbolic packet contains all of the packets that are produced by the  when applied to the packets in the input symbolic packet.

The pull operation simulates the effect of a  in reverse. This operation is used when computing the backward transition of a symbolic packet over a symbolic transition, for counter-example generation. The pull operation answers this question: given a set of output packets (represented symbolically), what are the possible input packets (also represented symbolically) that could have produced them?
In other words, a concrete packet $\pk$ is an element of $\mathsf{pull}(p,q)$ if and only if running the  $p$ on $\pk$ produces an output packet in $q$. In particular, it is okay if running the  on $\pk$ produces multiple output packets, as long as at least one of them is in $q$.

Each of these operations is uniquely specified by two correctness conditions:

* They semantically match their counterpart (e.g. $\Sem{p \mathop{\nf{+}} q} \equiv \Sem{p + q}$ for all $p,q \in \SPP$)

* They maintain the reduced & ordered invariant (e.g., $p \mathop{\nf{+}} q$ is reduced & ordered if $p,q$ are)

For push and pull, the correctness condition is as follows:

\[
% \Sem{\mathsf{push}\ p\ s} &= \{\pkp\in\Pk\mid \pk\in\pSem{p} \wedge \pkp\in\Sem{s}(\pk)\}\\
% \Sem{\mathsf{pull}\ s\ p} &= \{\pkp\in\Pk\mid \pk\in\pSem{p} \cap \Sem{s}(\pkp)\}\\
\beta \in \Sem{\mathsf{push}\ p\ s} \iff \exists \pk\in\pSem{p}.\ \pkp\in\Sem{s}(\pk)
\quad\text{and}\quad
\beta \in \Sem{\mathsf{pull}\ s\ p} \iff \exists \alpha \in \pSem{p}.\ \alpha \in \Sem{s}(\pkp)
\]

For further details, see app:spp.

§ SYMBOLIC NETKAT AUTOMATA VIA BRZOZOWSKI DERIVATIVES

With the symbolic packet and symbolic transition representations in place, we can now define symbolic NetKAT automata.  The construction of NetKAT automata shares some similarities with the construction of automata for regular expressions.  In prior work <cit.>, NetKAT automata were constructed via Antimirov derivatives <cit.>, which can be extended from regular expressions to NetKAT.  The Antimirov derivative constructs a non-deterministic automaton, and as such, is well suited for handling 's union operator by inserting transitions for the two sub-terms.  However, the Antimirov derivative is not well suited for our extended set of logical operators, as we cannot simply insert (non-deterministic) transitions for the operands of intersection, difference, and symmetric difference.  Instead, we extend the Brzozowski derivative <cit.> to NetKAT, which constructs a deterministic automaton directly, and is better suited for the logical operators.

In the rest of this section, we will first describe what symbolic NetKAT automata are, and then describe how to construct them via the Brzozowski derivative.

§.§ Symbolic NetKAT Automata

An automaton for a regular expression consists of a set of states, and transitions labeled with symbols from the alphabet.  Additionally, one of the states is designated as the initial state, and a subset of the states are designated as accepting states.  This way, an automaton for a regular expression models the set of strings that are accepted by the regular expression.

An automaton for a NetKAT program is similar, but instead of modeling a set of strings, it models the traces that are produced for a given input packet.  When a packet travels through the automaton, every state that it traverses acts as a $\text{dup}$ operation, appending a copy of the packet to the packet's trace.  Therefore, the transition between two states is labeled with a dup-free NetKAT program, represented symbolically as a . That is, each edge in the automaton is not labeled with a single letter, as it would be in a standard DFA or NFA, but with a potentially large . This is necessary because an edge in the automaton intuitively represents “what happens between two dups”. This is precisely a dup-free NetKAT program, which can itself have rich behavior, represented canonically as an . This is needed to support fine-grained control over equivalence and inclusion as discussed in <Ref>—e.g., via conditionally executed dups or assignments between dups.

Secondly, instead of having a boolean at each state to determine acceptance, NetKAT automata have an additional  at each state that determines the set of packets that are produced as output of the automaton when a packet reaches that state.  Therefore, a symbolic NetKAT automaton is a tuple $\mathcal{A} = \langle Q, q_o, \delta, \epsilon \rangle$ where $Q$ is a finite set of states,
$q_0 \in Q$ is the initial state,

* $\delta : Q \times Q \to \SPP$ is the transition function, and

* $\epsilon : Q \to \SPP$ is the output function.

Deterministic NetKAT automata

The notion of a deterministic NetKAT automaton is more subtle than for classic finite automata.  For classic automata, a deterministic automaton is one where for every state $q$ and symbol $a$, there is at most one transition from $q$ labeled with $a$.  For a NetKAT automaton, we need to take into account the fact that the transitions are labeled with s, which may produce multiple packets for a given input packet.  Therefore, we define a deterministic NetKAT automaton as one where for every state $q$ and packet $\pk$, the set of packets produced by $\mathsf{push}(\pk,\delta(q,q'))$ are disjoint for all $q' \in Q$.  This is equivalent to saying that $\delta(q,q_1')
\mathop{\nf{\cap}} \delta(q,q_2') = \bot$ for all $q_1',q_2' \in Q$
($q_1' \neq q_2'$).  Note that an input packet $\pk$ may produce multiple different packets at each successor state, but these packet sets at different successor states are disjoint.

§.§ Constructing Automata via Brzozowski Derivatives

We now describe how to construct a symbolic NetKAT automaton for a NetKAT program via the Brzozowski derivative.  We take the set of states to be the set of NetKAT expressions, and the initial state to be the NetKAT program itself.  Because we want to construct a deterministic automaton, we need a way to represent a non-intersecting outgoing symbolic transition structure (STS). We represent such a transition structure as a NetKAT expression in the following form:

\begin{align*}
r \in \mathsf{STS} \Coloneqq p_1 \cdot \mathrel{\text{dup}} \cdot\ q_1 + \ldots + p_n \cdot \mathrel{\text{dup}} \cdot\ q_n
\end{align*}

where $p_i \in \SPP$, and $q_i$ are NetKAT expressions, and the $p_i$ are disjoint ($p_i \mathop{\nf{\cap}} p_j = \bot$ for $i \neq j$).

Dup is an STS, by taking $r = \top \cdot\text{dup} \cdot \top$.
We extend the logical operators to STSs:

\begin{align*}
\tilde{+}, \tilde{\cap}, \tilde{\oplus}, \tilde{-}\ :\ \mathsf{STS} \times \mathsf{STS} \to \mathsf{STS}
\end{align*}

These operations need to be defined such that the resulting STS is deterministic. For $r_1 \cap r_2$:

\begin{align*}
(p_1 \cdot \text{dup} \cdot q_1 + \ldots + p_n \cdot \text{dup}\ \cdot q_n) \mathrel{\tilde{\cap}} (p'_1 \cdot \text{dup} \cdot q'_1 + \ldots + p'_n \cdot \text{dup} \cdot q'_n)
\end{align*}

To bring this in STS form, we distribute the intersection over the union, and combine the terms:

\begin{align*}
(p_1 \mathop{\nf{\cap}} p'_1) \cdot \text{dup} \cdot (q_1 \cap q'_1) +
(p_1 \mathop{\nf{\cap}} p'_2) \cdot \text{dup} \cdot (q_1 \cap q'_2) +
\ldots +
(p_n \mathop{\nf{\cap}} p'_n) \cdot \text{dup} \cdot (q_n \cap q'_n)
\end{align*}

This is not yet in STS form, as the $q_i \cap q'_i$ terms may not all be different, so we need to collect the terms with the same $q_i \cap q'_i$, and union their s. The other operators need a similar (albeit slightly more complicated) treatment in order to maintain determinism.

Second, we extend sequential composition to STSs, in two forms (denoted with the same symbol). We can compose an STS with a  on the left, or with a NetKAT expression on the right:

\begin{align*}
\tilde{\cdot} : \SPP \times \mathsf{STS} \to \mathsf{STS} \qquad
\tilde{\cdot} : \mathsf{STS} \times \mathsf{Exp} \to \mathsf{STS}
\end{align*}

Like the other operators, these need to be defined such that the resulting STS is deterministic.

All of the STS operations are defined in terms of  operations. Therefore, an efficient  implementation is crucial both for operations on symbolic packets and for operations on STSs.

Each of these operations is uniquely specified by two correctness conditions:

* They semantically match their counterpart (e.g. $\Sem{p \mathop{\nf{+}} q} \equiv \Sem{p + q}$ for all $p,q \in \mathsf{STS}$)

* They maintain the invariant that the transitions are pairwise disjoint.

Brzozowski derivative
With these operations in place, it is straightforward to define the Brzozowski derivative for NetKAT expressions:

\begin{align*}
\epsilon(p + q) &\triangleq \epsilon(p) \mathop{\nf{+}} \epsilon(q) \\
\epsilon(p \cap q) &\triangleq \epsilon(p) \mathop{\nf{\cap}} \epsilon(q) \\
\epsilon(p \oplus q) &\triangleq \epsilon(p) \mathop{\nf{\oplus}} \epsilon(q) \\
\epsilon(p - q) &\triangleq \epsilon(p) \mathop{\nf{-}} \epsilon(q) \\
\epsilon(p \cdot q) &\triangleq \epsilon(p) \mathop{\nf{\cdot}} \epsilon(q) \\
\epsilon(p^\star) &\triangleq \epsilon(p)^\star
\end{align*}

\begin{align*}
\epsilon(\text{dup}) &\triangleq \bot\\
\epsilon(f \test v) &\triangleq f \test v\\
\epsilon(f \testNE v) &\triangleq f \testNE v\\
\epsilon(f \mut v) &\triangleq f \mut v\\
\epsilon(\top) &\triangleq \top\\
\epsilon(\bot) &\triangleq \bot
\end{align*}

\begin{align*}
\delta(p + q) &\triangleq \delta(p) \mathop{\tilde{+}} \delta(q) \\
\delta(p \cap q) &\triangleq \delta(p) \mathop{\tilde{\cap}} \delta(q) \\
\delta(p \oplus q) &\triangleq \delta(p) \mathop{\tilde{\oplus}} \delta(q) \\
\delta(p - q) &\triangleq \delta(p) \mathop{\tilde{-}} \delta(q) \\
\delta(p \cdot q) &\triangleq
\delta(p) \mathop{\tilde{\cdot}} q \mathrel{\tilde{+}}
\epsilon(p) \mathop{\tilde{\cdot}} \delta(q) \\
\delta(p^\star) &\triangleq \epsilon(p)^\star \mathop{\tilde{\cdot}} \delta(p) \mathrel{\tilde{\cdot}} p^\star
\end{align*}

\begin{align*}
\delta(\text{dup}) &\triangleq \dup\\
\delta(f \test v) &\triangleq \bot\\
\delta(f \testNE v) &\triangleq \bot\\
\delta(f \mut v) &\triangleq \bot\\
\delta(\top) &\triangleq \bot\\
\delta(\bot) &\triangleq \bot
\end{align*}

We construct a deterministic symbolic NetKAT automaton for a NetKAT program $p$ as follows:

States $Q \triangleq \mathsf{Exp}$.

Initial state $q_0 \triangleq p$.

Transitions take $\delta(q,q')$ to be the  of $q'$ in the Brzozowski derivative of $\delta(q)$.

Output $\epsilon : Q \to \SPP$, defined above.

The Brzozowski derivative is guaranteed to transitively reach only finitely many essentially different NetKAT expressions from a given start state. Therefore, in the actual implementation, we do not use the infinite set $\mathsf{Exp}$ for the states, but instead use only the finitely many essentially different NetKAT terms reached from the start state.

The NetKAT automaton for an example program is shown in <Ref>. The edges are labeled with the s that represent the transitions. The output  of every state is $\top$, i.e., the automaton accepts all packets that reach a state.
Note that the s in the figure feature several diamonds without outgoing edges. These diamonds produce no output packet, i.e., the packet is dropped.

*NetKAT automaton

Symbolic NetKAT automaton for $p \triangleq \left((a \mut 1 \cdot b \mut 2 \cdot c \mut 3 \cdot \text{dup})^\star + (b \test 2 \cdot c \test 3 \cdot \text{dup})^\star\right)^\star$

For more details, see app:spp.

§ BISIMILARITY AND COUNTER-EXAMPLE GENERATION

After converting the NetKAT programs to automata, we can check equivalence of two NetKAT programs by checking whether their automata are bisimilar. Bisimilarity is a well-known notion of equivalence for automata. For NetKAT automata, two states are bisimilar for a given packet $\pk$ if (1) the states produce the same output packets, and (2) for each possible modified packet $\pk'$, the two states transition to states that are bisimilar for $\pk'$.

Historically, methods for computing bisimulations of automata <cit.> have been based on either on Moore's algorithm for minimization <cit.> or Hopcroft and Karp's algorithm <cit.>. Indeed, the naive approach shown in <Ref> follows the basic structure of Hopcroft-Karp, in the sense that it relates the start states and proceeds to follow transitions forward in the two automata.

Our situation is different, because we have already added the symmetric difference operator to NetKAT.  Therefore, we can reduce equivalence checks $A \equiv B$ to emptiness checks $A \oplus B \equiv
\bot$.

Subtlety of symmetric difference

The reader should note that the situation is a bit more subtle than it may seem at first sight.  In particular, consider the query $A \equiv B$, which asks whether two NetKAT programs $A$ and $B$ are equivalent. If they are inequivalent, then there must be some input packet that causes $A$ to produce a different output than $B$.  Output in this sense does not just mean the final output packet, but also the trace of the packet.  It can be the case that $A$ and $B$ produce the same final output packets, but differ in the trace of the packets. Therefore, the symmetric difference $A \oplus B$ takes the symmetric difference of the traces, not just of the output packets. In other words, the set $\Sem{A \oplus B}$ is the set of counter-example traces to the equivalence of $A$ and $B$.

Subtlety of the emptiness of an automaton

A second subtlety is the emptiness of an automaton.  Whereas for regular expressions, it is easy to check whether a DFA is empty (just check whether there are any reachable accepting states), this is not the case for NetKAT automata.  Because NetKAT automata manipulate and test the fields of packets, it is possible that a packet travels through the automaton, and even causes multiple packets to be produced (e.g., due to the presence of union in the original NetKAT expression), but nevertheless, it is possible that all of these packets are eventually dropped by the automaton, before producing any output packets.

The goal of this section is to develop a symbolic algorithm for this check, which is more efficient than the naive algorithm that checks all concrete input packets separately.

§.§ Forward Algorithm

To check whether a NetKAT automaton drops all input packets, we use an algorithm that works in the forward direction. The forward algorithm computes all output packets that the automaton can produce, across all possible input packets. More formally: given a NetKAT automaton for a NetKAT program $p$, the forward algorithm computes the set of final packets occurring in the traces $\Sem{p}(\pk)$ across all input packets $\pk$. The forward algorithm therefore starts with the complete symbolic packet $\top$ at the input state, and repeatedly applies all outgoing transitions $\delta$ to it.  In this way, the algorithm iteratively accumulates a symbolic packet at every state, which represents the set of packets that can reach that state from the start state.  Once we know the set of packets that can reach a state, we can determine the set of output packets by applying the output function $\epsilon$ to the symbolic packet of each state, and taking the union of the results.

$\doneR(q) \gets \bot \text{ for } q \in Q$;
$\todoR(q) \gets \bot \text{ for } q \in Q \setminus \{q_0\}$;
$\todoR(q_0) \gets \top$;
$\exists q.\ \todoR(q) \neq \bot$
set $p := \todoR(q) \mathrel{\nf{-}} \doneR(q)$;
$\todoR(q) \gets \bot$;
$\doneR(q) \pluseq p$;
$q' \in Q$
$\todoR(q') \pluseq \mathsf{push}(p,\delta(q,q'))$;
$\sum_{q \in Q} \mathsf{push}(\doneR(q), \epsilon(q))$;

Forward algorithm

$\doneR(q) \gets \bot \text{ for } q \in Q$;
$\todoR(q) \gets \mathsf{pull}(\epsilon(q), \top) \text{ for } q \in Q$;
$\exists q.\ \todoR(q) \neq \bot$
set $p := \todoR(q) \mathrel{\nf{-}} \doneR(q)$;
$\todoR(q) \gets \bot$;
$\doneR(q) \pluseq p$;
$q' \in Q$
$\todoR(q') \pluseq \mathsf{pull}(\delta(q',q), p)$;

Backward algorithm

Forward and backward algorithms for NetKAT automata

The forward algorithm is shown in <Ref>.  To determine the set of packets that a given NetKAT expression $p$ can produce, we convert it to a NetKAT automaton, and then use the forward algorithm to determine the symbolic output packet.  In our implementation, we also have a way to stop the algorithm early, if the user is only interested in a “yes” or “no” answer for the query $p \equiv\bot$. In this case, we can stop the algorithm as soon as any output packet is produced.

§.§ Backward Algorithm

The forward algorithm gives us the set of output packets that a NetKAT automaton can produce, but we are also interested in which input packets cause this output to be produced. For instance, for a given check $A \equiv B$, we want to know which input packets cause $A$ and $B$ to produce different sets of output traces.  More generally,  we want to know which input packets cause a NetKAT automaton to produce a nonempty set of output packets or, formally, given an automaton for a NetKAT program $p$, what is the set of initial packets $\pk$ for which $\Sem{p}(\pk)$ is nonempty.

To answer this question, we developed a backward algorithm, shown in <Ref>.  The backward algorithm computes all input packets that can cause the automaton to produce a nonempty set of output packets.  The backward algorithm therefore starts with the complete symbolic packet $\top$ at every state, and pulls it backwards through all observation functions $\epsilon$.  The algorithm then iteratively accumulates a symbolic packet at every state, which represents the set of packets that will cause the automaton to produce a nonempty set of output packets, when starting from that state.  The accumulation is done by pulling the symbolic packet backwards through all transitions until a fixpoint is reached.  Once the fixpoint is reached, we return the symbolic packet at the start state, which represents the set of input packets that will cause the automaton to produce a nonempty set of output packets when starting from the start state.

§ IMPLEMENTATION

$\NKcheck\ e_1\ \equiv\ e_2$

$\NKcheck\ e_1\ \nequiv\ e_2$

$\NKprint\ e$

$x = e$

$\NKfor\ i\ \in n_1..n_2\ \NKdo\ c$

$\NKforward\ e$,
$\NKbackward\ e$

$e_1 \!\cap \!e_2$,         $e_1 \!\oplus \!e_2$,         $e_1 \!-\! e_2$

$\NKexists{} f\ e$,         $\NKforall{} f\ e$

(+ , see <ref>)

NKPL syntax.

We have implemented the algorithms in a new system, , comprising 2500 lines of Scala. In this section we explain the system's interface. The implementation provides a surface syntax for expressing queries, which extends the core syntax from <Ref>. The extended syntax is shown in <Ref>. The language has statements and expressions, which we describe below.

The $\NKcheck\ e_1 \equiv e_2$ command runs the bisimulation algorithm. The system reports success if the expressions are equivalent (when $\equiv$ is used) or inequivalent (when $\nequiv$) is used, or reports failure otherwise. The other statements behave as expected:
The $\NKprint$ statement invokes the pretty printer, $x = e$ let-binds names to expressions, and $\NKfor$ runs a statement in a loop.

The $\NKforward\ e$ expression computes, in forward-flowing mode, the set of output packets resulting from running the symbolic packet $\top$ through the given expression $e$ (see <Ref>). Conversely $\NKbackward\ e$ computes the set of input packets which generate some output packet when run on the given expression (<Ref>). These are generally used in conjunction with the $\oplus, -, \cap$ operators to express the desired query. The user may combine these expressions with the $\NKexists$ and $\NKforall$ operators to reason about symbolic packets, and the $\NKprint$ operator to pretty print the symbolic packets, or the $\NKcheck$ operator to assert (in)equivalence of two expressions.

We note that the generality of the language allows us to express some queries in different, equivalent ways. For example, the two checks:
$e_1 \equiv e_2$ and $e_1 \oplus e_2 \equiv \zero$ are equivalent. However, the expression on the right lends itself to inspection of counterexample input packets: $\NKprint\ (\NKbackward\ e_1 \oplus e_2)$.
This statement pretty prints a symbolic packet having different behavior on $e_1$ and $e_2$ (i.e., packets that result in some valid history in one expression and not the other). In other words, it prints the set of all counter-example input packets for $e_1 \equiv e_2$.

Topologies and routing tables
While NetKAT can be used to specify routing policies declaratively, it is also possible to import topologies and routing tables into NetKAT. For example, a simple way to define routing tables and topologies in NetKAT is as follows:

$\mathsf{R} \triangleq$   $\sw \test 5 \cdot (\dst \test 6 \cdot \pt \mut 3 + \dst \test 8 \cdot \pt \mut 4)$
$\mathsf{T} \triangleq$   $\sw \test 5 \cdot (\pt=3 \cdot \sw \mut 6 + \pt=4 \cdot \sw \mut 8)$

$+\ \cdots\ +$
$+\ \cdots\ +$

$ \sw \test 7 \cdot (\dst \test 8 \cdot \pt \mut 2 + \dst \test 9 \cdot \pt \mut 1) $
$ \sw \test 7 \cdot (\pt=2 \cdot \sw \mut 8 + \pt=1 \cdot \sw \mut 9)$

The routing $\mathsf{R}$ tests the switch field (where the packet currently is), and the destination field (where the packet is supposed to end up), and then sets the port over which the packet should be sent out. The topology $\mathsf{T}$ tests the switch and port fields, and then transports the packet to the next switch. We define the action of the network by composing the route and topology:

\begin{align*}
\mathsf{net} \triangleq \mathsf{R} \cdot \mathsf{T} \cdot \text{dup}
\end{align*}

We include a dup to extend the trace of the packet at every hop.

[All-Pairs Reachability Queries]
A naive way to check reachability of all pairs of hosts in a network is to run the following command for each pair of end hosts $n_i$, $n_j$:

\[ \NKcheck\ (\sw \test n_i) \cdot \textsf{net}^\star \cdot (\sw \test n_j) \nequiv \bot \]

Of course, this requires a number of queries which is quadratic in the number of hosts—quickly becoming prohibitive. One might think that we could reduce the number of queries to $n$ by running:

\begin{align*}
&\NKfor\ i \in 1..n\ \NKdo\ \NKcheck\ (\NKforward\ (\sw \test i \cdot \textsf{net}^\star)) \equiv (\sw \in 1..n)
\end{align*}

This query does work if $\sw$ is the only field of our packets, because the left hand side contains the packets that can be reached from $i$ via the network, and the right hand side contains packets where the $\sw$ field is any value in $1..n$. Unfortunately, this does not quite work if the network also operates on other packet fields (say, fields $f_1$ and $f_2$), as the packets on the left hand side will have those fields, whereas the packets on the right hand side will only have a $\sw$ field. The $\NKexists$ and $\NKforall$ operators allow us to manipulate symbolic packets and express all pairs reachability in $n$ queries:

\begin{align*}
&\NKfor\ i \in 1..n\ \NKdo\ \NKcheck\ (\NKexists f_1\ (\NKexists f_2\
(\NKforward\ (\sw=i \cdot \textsf{net}^\star)))) \equiv (\sw \in 1..n)
\end{align*}

The operators $\NKexists$ and $\NKforall$ give the programmer the ability to reason about symbolic packets that may be computed, for instance, by $\NKforward$ or $\NKbackward$. The specifications are:

\[
p \in \NKexists f\ e \overset{\triangle}{\iff} \exists v\in V\colon p[f\mut v] \in \pSem{e} \quad\text{and}\quad
p \in \NKforall f\ e \overset{\triangle}{\iff} \forall v\in V\colon p[f\mut v] \in \pSem{e}
\]

The implementation does not iterate over $V$ (indeed, $V$ can be unknown). Rather, $\NKexists$ and $\NKforall$ are implemented directly as operations on symbolic packets. In fact, the implementation does not need to fix the sets of fields or
values up-front at all. Instead, it operates on a conceptually infinite set of fields and values. This works because s' default cases handle all remaining fields and all values.

Correctness and testing methodology

We validated our implementation with the following property-based fuzz testing methodology:

* We implemented the semantics $\Sem{p}(\pk)$ in Scala, as described in <Ref>.

* We repeatedly pick two SPs/SPPs $p$ and $q$ and a packet $\pk$. We enumerated small SPPs up to a bound and generated larger SPPs randomly. We generated packets exhaustively.

* We check the soundness (e.g., $\Sem{p \mathop{\nf{+}} q}(\pk) = \Sem{p}(\pk) \cup \Sem{q}(\pk)$) and canonicity (e.g., $\Sem{p}(\pk) = \Sem{q}(\pk)$ for all $\pk$ if and only if $p = q$) of the operations, as well as additional algebraic laws derived from the NetKAT axioms (e.g., $p \mathop{\nf{+}} q = q \mathop{\nf{+}} p$).

In addition to property-based testing for SPs and SPPs, we also generated hundreds of thousands of pairs of random NetKAT expressions and checked that 's bisimilarity check matches the output of . This revealed a subtle bug in Frenetic, which we reported and is now fixed.

Full reachability queries on Topology Zoo.  and results are averages of 100 runs, preceded by 10 runs of JIT warmup. -naive is without JIT warmup and uses $O(n^2)$ 1-to-1 queries.

§ EVALUATION

To evaluate , we conducted experiments in which we used it to solve a variety of verification tasks for a range of topologies and routes, as well as challenging combinatorial terms. The goal of our evaluation is to answer the following three questions:

* How does  perform compared to the state of the art
verifier, ?

* How does  perform compared to the state of the art
specialized network verification tool, ?

* How well does  scale with the size of topology?

* When does  perform asymptotically better than prior work?

§.§ Topology Zoo

Running time (in seconds) of , , and on Topology Zoo queries.  and results are averages of 100 runs, preceded by 10 runs of JIT warmup.

To begin to answer the first three questions, we conducted our experiments using The Internet Topology Zoo <cit.> dataset, a publicly available set of 261 network topologies, ranging in size from just 4 nodes (the original ARPANet) to 754 nodes (KDL, the Kentucky Data Link ISP topology).  For each topology, we generated a destination-based routing policy using an all-pairs shortest path scheme that connects every pair of routers to each other.

To demonstrate 's scalability, we first ran full (i.e., $O(n^2)$) reachability queries for every topology in the zoo using , [<https://github.com/frenetic-lang/frenetic>], and  <cit.>.
The results are shown in <Ref> in a log-log plot, so straight lines correspond to  polynomials with exponents related to their slope.

The figure shows two different configurations of : one that verifies full reachability using a quadratic number of point-to-point queries and does not use JIT warmup (“katch-naive”), and one that verifies full reachability using a linear number of queries and does use JIT warmup (“katch”).

Because of the size of the dataset, we set a timeout of 5 minutes per topology. Under these conditions,  was unable to complete for all but the smallest topologies. -naive handles most of the topologies in well under a second, and all but the largest in under 2 minutes. -naive exceeds the timeout on Kentucky Data Link—using a quadratic number of queries to check full reachability produces over 500k individual point-to-point queries in a network with 754 nodes! (However, -naive is able to finish it in just under 20 minutes.)

To avoid combinatorial blowup in the verification query itself, we also used 's high-level verification interface, to check full reachability using a linear number of queries, as discussed in <Ref>.  does not have an analogous linear mode.  does have an analogous mode, as it has specialized support for full reachability queries.  is faster than  for the smaller topologies, but slower for the larger ones. Indeed, the slope of the  line is steeper than the  line, indicating that  scales slightly better with the size of the network on these queries.
It is important to note that  has support for prefix-matching, ACLs, NAT, incrementality, and other features for which  does not have specialized support and which are not tested in this comparison.
One should therefore not draw strong conclusions from this comparison; we include it as it is encouraging that reachability via  equivalence can be competitive with a state-of-the-art specialized tool.

We also randomly sampled a subset of toplogies from the Topology Zoo of varying size and generated point-to-point (1-to-1) reachability and slicing queries to be checked against the routing configurations with no timeout. For each query, we ran  and also generated an equivalent query in the syntax of , and ran 's bisimulation verifier on those queries. We present a full table of results of these experiments in <Ref>. The table shows that 's relative speedup over  is considerable, and increases problem size. This is encouraging, because it shows that  is more scalable.  was unable to complete KDL within a 200GB memory limit (for comparison,  is able to complete the same query with well under 1GB).
We also include a selection of full-reachability results from <Ref> in the table.
The reader may wonder why full reachability takes only twice as long as 1-to-1 reachability. This is because a significant fraction of the time is spent constructing automata (which are similar for both queries), and much of the work in the full reachability queries is shared due to memoization of $\SPP$ operations.

§.§ Combinatorial Examples

Finally, we ran experiments to test the hypothesis that  have an asymptotic advantage for certain types of queries.  uses forwarding decision diagrams (), which is a different (and non-canonical) representation for automaton transitions. A key advantage of  over  is that  keep the updates to each field next to the tests of the same field. On the other hand,  keep all updates at the leaves, which can result in combinatorial explosion during sequencing. To test this, we generated the following NetKAT programs:

Inc: Treating the input packet's $n$ boolean fields as a binary number, increment it by one.

Flip: Sequentially flip the value of each of the $n$ boolean fields.

Nondet: Set each field of the packet to a range of values from $0$ to $n$.

For Inc, we tested that repeatedly incrementing (using the $\star$
operator) can turn packet $00\cdots0$ into $11\cdots1$.  For Flip, we tested that flipping all bits twice returns the original packet.  For Nondet, we tested that setting the fields non-deterministically twice is the same as doing it once.  The results of this experiment are shown in <Ref>.  Because the available fields are hardcoded in , we only ran the Inc and Flip experiments up to $n=10$. We ran the non-determinism test up to $n=15$.   finishes all three queries up to $n=100$ in under a one minute, demonstrating its asymptotic advantage for these queries, while Frenetic shows combinatorial blowup on larger packets.

Results of running  and on combinatorial benchmarks

Source of speedup
The speedup of  over  comes from several sources: (1) the use of  instead of , which can be exponentially more compact and support more efficient sequential composition, (2) the symbolic bisimulation algorithm operating on SPs, which can handle exponentially large sets of packets at once, and (3) a quadratic-doubling implementation of star, which can handle exponentially long traces quickly.
These differences show up most strongly in the combinatorially adversarial examples above, but the speedup is also considerable for the Topology Zoo benchmarks, which are based on real-world topologies and not designed to be adversarial.

Field order
The field order of SPs and SPPs can affect performance, just as for BDDs.
In practice, field orders that keep related fields close together are beneficial.
Our implementation allows the user to control the field order, but we did not use this for our benchmarks.
By default, the fields are in the order in which they first occur in the input file, which turned out to work well enough.

§ RELATED WORK

This section discusses the most closely related prior work to this paper, focusing on three areas: , network verification, and automata-theoretic approaches to verification.

was originally proposed as a semantic foundation for SDN data planes <cit.>. Indeed, being based on KAT <cit.>, the language provides a sound and complete algebraic reasoning system. Later work on developed an automata-theoretic (or coalgebraic) account of the language <cit.>, including a decision procedure based on Brzozowski derivatives and bisimulation, implemented in . However, the performance of this approach turns out to be poor, as shown in our experiments, due to the use of ad hoc data structures (“bases”) to encode packets and automata. 's compiler uses a variant of BDDs, called Forwarding Decision Diagrams (FDDs), as well as an algorithm for converting programs to automata using Antimirov derivatives <cit.>, improving on the earlier representation of transitions as sets of bases <cit.>. The s proposed in this paper improve on FDDs by ensuring uniqueness and supporting efficient sequential composition in the common case. In addition, the deterministic automata used in support additional “negative”
operators that are useful for verification. Other papers based on NetKAT have explored use of the language in other settings such as distributed control planes <cit.>, probabilistic networks <cit.>, and Kleene algebra over composable theories with unbounded state <cit.>. It would be interesting to extend the techniques developed in this paper to these richer settings. Another interesting direction for future work is to build a symbolic verifier for the guarded fragment of  <cit.>.

*Network Verification

Early work by Xie et al. <cit.> proposed a unifying mathematical model for Internet routers and developed algorithms for analyzing network-wide reachability. Although the paper did not discuss an implementation, its elegant formal model has been extremely influential in the community and has served as the foundation for many follow-on efforts, including this work. The emergence of software-defined networking (SDN) led to a surge of interest in static data plane verification, including systems such as Header Space Analysis (HSA) <cit.>, Anteater <cit.>, VeriFlow <cit.>, Atomic Predicates (AP) <cit.>, APKeep <cit.>. These systems all follow a common approach: they build a model of the network-wide forwarding behavior and then check whether given properties hold. However, they vary in the data structures and algorithms used to represent and analyze the network model. For instance, Anteater relies on first-order logic and SAT solvers, while VeriFlow uses prefix trees and custom graph-based algorithms. HSA, AP and APKeep are arguably the most related to our work as they use symbolic representations and BDDs respectively.

The primary difference between  and these systems is that the latter implement specialized algorithms for network-wide analysis queries, while  (and ) solve the more general equivalence problem, into which network-wide analysis queries can be encoded.
This generic approach is based on principled automata-theoretic foundations, but one might expect it to be less efficient than specialized algorithms.
was found to be comparable to or faster than HSA <cit.>, so by transitivity we expect  to be faster than HSA.
However, the current state of the art is , which is significantly faster than  and HSA.
We include a comparison with  in <Ref> on reachability queries.
The results show that  is competitive with  on these benchmarks, despite solving general NetKAT queries. As discussed, one should not draw strong conclusions from this comparison as  includes additional features; nevertheless, it offers a promising preliminary indication of NetKAT's scalability and performance.

Another line of work has explored how to lift verification from the data plane to the control plane. Batfish <cit.>
proposed using symbolic simulation to analyze distributed control planes—i.e., generating all possible data planes that might be produced starting from a given control-plane configuration. Like , Batfish uses a BDD-based representation for data plane analysis. MineSweeper <cit.> improves on Batfish using an SMT encoding of the converged states of the control plane that avoids having to explicitly simulate the underlying routing protocols. Recent work has focused on using techniques like modular reasoning <cit.> abstract interpretation <cit.>, and a form of symmetry reduction <cit.> to further improve the scalability of control-plane verification.

*Automata-Theoretic Approach and Symbolic Automata

Our work on builds on the large body of work on the automata-theoretic approach to verification and symbolic automata. The automata-theoretic approach was pioneered in the 1980s, with applications of temporal logics and model checking to hardware verification <cit.>. BDDs, originally proposed by Lee <cit.>, were further developed by Bryant <cit.>, and used by McMillan for symbolic model checking <cit.>. BDD-based techniques were a success story of symbolic model checking of hardware in the 1990s—Chaki and Gurfinkel give an overview <cit.>.

An influential line of work by D'Antoni and Veanus developed techniques for representing and transforming finite automata where the transitions are not labeled with individual characters but with elements of a so-called effective Boolean algebra <cit.>. Shifting from a concrete to a symbolic representation requires generalizing classical algorithms, such as minimization and equivalence, but facilitates building automata that work over huge alphabets, such as Unicode.

Pous <cit.> developed symbolic techniques for checking the equivalence of automata where transitions are specified using BDDs. The methods developed in this paper take Pous's work as a starting point but develop a non-trivial extension for . In particular, s provide a compact representation for “carry-on” packets, which is a critical and unique aspect of 's semantics. Bonchi and Pous <cit.> explored the use of up-to techniques for checking equivalence of automata. In principle, one can view the invariants enforced by 's term representations as a kind of up-to technique, but a full investigation of this idea requires more work.

Our backward algorithm for computing bisimulations can be seen as a variant of Moore's classic algorithm for computing the greatest bisimulation of classic automata.  Doenges et al. <cit.>
proposed an analogous approach for checking equivalence of automata that model the behavior of P4 packet parsers <cit.>. However, Leapfrog's model is simpler than 's and is based on classic finite automata. It achieves scalability due to a novel up-to technique that “leaps”
over internal buffering transitions rather than symbolic representations.

§ ACKNOWLEDGEMENTS

We wish to thank the PLDI reviewers for many helpful comments and suggestions, which improved the paper significantly. We are also grateful to Aaron Gember-Jacobson and Peng Zhang for making AP Keep available as open-source software, to Caleb Koch for early discussions on compact data structures for data plane verification, to the Cornell PLDG for helpful comments on early drafts, and to the EPFL DCSL group for providing a welcoming and supportive environment. This work was supported in part by ONR grant N68335-22-C-0411, DARPA grant W912CG-23-C-0032, ERC grant 101002697, and a Royal Society Wolfson fellowship.

§ DATA AVAILABILITY

The current version of the implementation is available at <https://github.com/cornell-netlab/KATch>.  A snapshot of the code as of artifact evaluation (with a dependencies-included Docker image) is available at <https://zenodo.org/doi/10.5281/zenodo.10806446>.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Anderson et al(2014)]
authorpersonCarolyn Jane Anderson,
personNate Foster, personArjun Guha,
personJean-Baptiste Jeannin, personDexter Kozen,
personCole Schlesinger, and personDavid Walker.
NetKAT: Semantic Foundations for Networks. In

authorpersonValentin Antimirov.
Partial derivatives of regular expressions and
finite automaton constructions.
journalTheoretical Computer Science
volume155, number2 (dateMar
year1996), pages291–319.

[Barnett et al(2005)]
authorpersonMichael Barnett,
personBor-Yuh Evan Chang, personRobert DeLine,
personBart Jacobs, and personK. Rustan M. Leino.
Boogie: A Modular Reusable Verifier for
Object-Oriented Programs. In booktitleFMCO.

[Beckett et al(2017)]
authorpersonRyan Beckett, personAarti
Gupta, personRatul Mahajan, and personDavid
Walker. year2017.
A General Approach to Network Configuration
Verification. In booktitleSIGCOMM.

[Beckett et al(2018)]
authorpersonRyan Beckett, personAarti
Gupta, personRatul Mahajan, and personDavid
Walker. year2018.
Control Plane Compression. In

[Beckett et al(2020)]
authorpersonRyan Beckett, personAarti
Gupta, personRatul Mahajan, and personDavid
Walker. year2020.
Abstract Interpretation of Distributed Network
Control Planes. In booktitlePOPL.

[Beckett et al(2016)]
authorpersonRyan Beckett, personRatul
Mahajan, personTodd Millstein, personJitendra
Padhye, and personDavid Walker.
Don't Mind the Gap: Bridging Network-Wide
Objectives and Device-Level Configurations. In

[Bonchi and Pous(2013)]
authorpersonFilippo Bonchi and
personDamien Pous. year2013.
Checking NFA Equivalence with Bisimulations up to
Congruence. In booktitlePOPL.

[Bosshart et al(2014)]
authorpersonPat Bosshart, personDan Daly,
personGlen Gibb, personMartin Izzard,
personNick McKeown, personJennifer Rexford,
personCole Schlesinger, personDan Talayco,
personAmin Vahdat, personGeorge Varghese, and
personDavid Walker. year2014.
P4: Programming Protocol-Independent Packet
journalSIGCOMM Computer Communication Review
volume44, number3 (dateJul
year2014), pages87–95.

[Brown et al(2023)]
authorpersonMatt Brown, personAri Fogel,
personDaniel Halperin, personVictor Heorhiadi,
personRatul Mahajan, and personTodd D. Millstein.
Lessons from the evolution of the Batfish
configuration analysis tool. In booktitleSIGCOMM.

authorpersonRandal E. Bryant.
Graph-Based Algorithms for Boolean Function
journalIEEE Trans. Comput. volumeC-35,
number8 (dateAug year1986),

authorpersonRandal E. Bryant.
Symbolic Boolean Manipulation with Ordered
Binary-Decision Diagrams.
journalComput. Surveys volume24,
number3 (dateSep year1992),

authorpersonJanusz A. Brzozowski.
Canonical regular expressions and minimal state
graphs for definite events. In booktitleProceedings of the
Symposium of Mathematical Theory of Automata.

[Burch et al(1990)]
authorpersonJerry R. Burch, personEdmund M.
Clarke, personKenneth L. McMillan, personDavid L.
Dill, and personL. J. Hwang. year1990.
Symbolic Model Checking: 1020 States and
Beyond. In booktitleLICS.

[Chaki and Gurfinkel(2018)]
authorpersonSagar Chaki and personArie
Gurfinkel. year2018.
BDD-Based Symbolic Model Checking.
In booktitleHandbook of Model Checking,
editorpersonEdmund M. Clarke,
personThomas A. Henzinger, personHelmut Veith, and
personRoderick Bloem (Eds.). publisherSpringer
International Publishing, pages219–245.

[D'Antoni and Veanes(2014)]
authorpersonLoris D'Antoni and
personMargus Veanes. year2014.
Minimization of Symbolic Automata. In

[D'Antoni and Veanes(2017)]
authorpersonLoris D'Antoni and
personMargus Veanes. year2017.
Forward Bisimulations for Nondeterministic Symbolic
Finite Automata. In booktitleTACAS.

[Doenges et al(2022)]
authorpersonRyan Doenges, personTobias
Kappé, personJohn Sarracino, personNate Foster,
and personGreg Morrisett. year2022.
Leapfrog: Certified Equivalence for Protocol
Parsers. In booktitlePLDI.

[Fogel et al(2015)]
authorpersonAri Fogel, personStanley Fung,
personLuis Pedrosa, personMeg Walraed-Sullivan,
personRamesh Govindan, personRatul Mahajan, and
personTodd Millstein. year2015.
A General Approach to Network Configuration
Analysis. In booktitleNSDI.

[Foster et al(2011)]
authorpersonNate Foster, personRob
Harrison, personMichael J. Freedman,
personChristopher Monsanto, personJennifer Rexford,
personAlec Story, and personDavid Walker.
Frenetic: A Network Programming Language. In

[Foster et al(2016)]
authorpersonNate Foster, personDexter
Kozen, personKonstantinos Mamouras, personMark
Reitblatt, and personAlexandra Silva.
Probabilistic NetKAT. In

[Foster et al(2015)]
authorpersonNate Foster, personDexter
Kozen, personMae Milano, personAlexandra Silva,
and personLaure Thompson. year2015.
A Coalgebraic Decision Procedure for NetKAT. In

[Greenberg et al(2022)]
authorpersonMichael Greenberg, personRyan
Beckett, and personEric Campbell.
Kleene Algebra Modulo Theories: A Framework for
Concrete KATs. In booktitlePLDI.

[Hooimeijer et al(2011)]
authorpersonPieter Hooimeijer,
personBenjamin Livshits, personDavid Molnar,
personPrateek Saxena, and personMargus Veanes.
Fast and Precise Sanitizer Analysis with BEK. In
booktitleUSENIX Conference on Security.

[Hopcroft and Karp(1971)]
authorpersonJohn E. Hopcroft and
personRichard M. Karp. year1971.
A Linear Algorithm for Testing Equivalence of
Finite Automata.

[Kazemian et al(2012)]
authorpersonPeyman Kazemian, personGeorge
Varghese, and personNick McKeown.
Header Space Analysis: Static Checking for
Networks. In booktitleNSDI.

[Khurshid et al(2012)]
authorpersonAhmed Khurshid, personWenxuan
Zhou, personMatthew Caesar, and personP. Brighten
Godfrey. year2012.
Veriflow: Verifying Network-Wide Invariants in Real
journalSIGCOMM Computer Communications Review
volume42, number4 (dateSep
year2012), pages467–472.

[Knight et al(2011)]
authorpersonSimon Knight, personHung X.
Nguyen, personNickolas Falkner, personRhys Bowden,
and personMatthew Roughan. year2011.
The Internet Topology Zoo.
journalIEEE Journal on Selected Areas in
Communications volume29, number9
(dateOct year2011), pages1765 –1775.

authorpersonDexter Kozen.
Kleene Algebra with Tests and Commutativity
Conditions. In booktitleTACAS.

authorpersonC. Y. Lee.
Representation of switching circuits by
binary-decision programs.
journalThe Bell System Technical Journal
volume38, number4 (dateJul
year1959), pages985–999.

[Leino and Wüstholz(2014)]
authorpersonK. Rustan M. Leino and
personValentin Wüstholz. year2014.
The Dafny Integrated Development Environment. In

[Mai et al(2011)]
authorpersonHaohui Mai, personAhmed
Khurshid, personRachit Agarwal, personMatthew
Caesar, personP. Brighten Godfrey, and
personSamuel Talmadge King. year2011.
Debugging the Data Plane with Anteater.
journalSIGCOMM Computer Communications Review
volume41, number4 (dateAug
year2011), pages290–301.

[Moeller et al(2024)]
authorpersonMark Moeller, personJules
Jacobs, personOlivier Savary Belanger, personDavid
Darais, personCole Schlesinger, personSteffen
Smolka, personNate Foster, and personAlexandra
Silva. year2024.
titleKATch: A Fast Symbolic Verifier for NetKAT.
[arxiv]2404.04760 [cs.PL]

authorpersonEdward F. Moore.
Gedanken-Experiments on Sequential Machines.
In booktitleAutomata Studies. (AM-34), Volume 34.

authorpersonDamien Pous.
Symbolic Algorithms for Language Equivalence and
Kleene Algebra with Tests. In booktitlePOPL.

[Smolka et al(2015)]
authorpersonSteffen Smolka, personSpiridon
Eliopoulos, personNate Foster, and personArjun
Guha. year2015.
A Fast Compiler for NetKAT. In

[Smolka et al(2019a)]
authorpersonSteffen Smolka, personNate
Foster, personJustin Hsu, personTobias Kappé,
personDexter Kozen, and personAlexandra Silva.
Guarded Kleene Algebra with Tests: Verification of
Uninterpreted Programs in Nearly Linear Time. In

[Smolka et al(2019b)]
authorpersonSteffen Smolka, personPraveen
Kumar, personNate Foster, personJustin Hsu,
personDexter Kozen, and personAlexandra Silva.
Scalable Verification of Probabilistic Networks.
In booktitlePLDI.

[Smolka et al(2017)]
authorpersonSteffen Smolka, personPraveen
Kumar, personNate Foster, personDexter Kozen, and
personAlexandra Silva. year2017.
Cantor Meets Scott: Semantic Foundations for
Probabilistic Networks. In booktitlePOPL.

[Tang et al(2023)]
authorpersonAlan Tang, personRyan Beckett,
personSteven Benaloh, personKarthick Jayaraman,
personTejas Patil, personTodd D. Millstein, and
personGeorge Varghese. year2023.
Lightyear: Using Modularity to Scale BGP Control
Plane Verification. In booktitleSIGCOMM.

[Thijm et al(2023)]
authorpersonTimothy Alberdingk Thijm,
personRyan Beckett, personAarti Gupta, and
personDavid Walker. year2023.
Modular Control Plane Verification via Temporal
Invariants. In booktitlePLDI.

[Torlak and Bodík(2013)]
authorpersonEmina Torlak and
personRastislav Bodík. year2013.
Growing Solver-aided Languages with Rosette. In
booktitleOnward! (SPLASH).

[Vardi and Wolper(1986)]
authorpersonMoshe Y. Vardi and
personPierre Wolper. year1986.
An Automata-Theoretic Approach to Automatic Program
Verification (Preliminary Report). In booktitleLICS.

[Xie et al(2005)]
authorpersonGeoffry G. Xie, personJibin
Zhan, personDavid A. Maltz, personHui Zhang,
personAlbert Greenberg, personGisli Hjalmtysson,
and personJennifer Rexford. year2005.
On Static Reachability Analysis of IP Networks.
In booktitleINFOCOMM.

[Yang and Lam(2016)]
authorpersonHongkun Yang and
personSimon S. Lam. year2016.
Real-Time Verification of Network Properties Using
Atomic Predicates.
journalIEEE/ACM Transactions on Networking
volume24, number2 (dateApr
year2016), pages887–900.

[Zhang et al(2020)]
authorpersonPeng Zhang, personXu Liu,
personHongkun Yang, personNing Kang,
personZhengchang Gu, and personHao Li.
APKeep: Realtime Verification for Real Networks.
In booktitleNSDI.

§ ASSUMPTIONS ON VALUES AND FIELDS

§.§ Set of Fields

We assume packet header fields come from a set $F$, and their values are from a set $V$. Both $F$ and $V$ must have a total order, $\sqsubset$. The implementation makes frequent use of finite maps, especially with $V$ as keys. We use the symbol ($\Mapsto$) to construct finite map types. For example, a concrete packet $\pk$ could naively be represented using the type $F \Mapsto V$, which we take to mean that $\pk = \{f_0 \mapsto v_0, \ldots, f_n \mapsto v_n\}$. We will sometimes use $\{\overline{f_i\mapsto v_i}\}$ to stand for $\{f_0 \mapsto v_0, \ldots, f_n \mapsto v_n\}$. All of our maps have only one binding for each key. We often collect they keys as a set with $\keys(\{f_0 \mapsto v_0, \ldots, f_n \mapsto v_n\}) \triangleq \{f_0,\ldots,f_n\}$.

§.§ Set of Values

We need one more assumption about the value space: it is larger than the values actually mentioned in any expressions. That we do not assume a fixed finite value space is a boon for compositionality: when determines that two expressions are equivalent, then they are equivalent under every value set containing the values in the two expressions. On the other hand, if $V$ is small, say $V=\{0,1\}$, then the test $f\test 0$ is semantically equivalent to $f\testNE 1$, but will not equate these two (unless both are preceded by, e.g. $(f\test 0 + f\test 1)$).

If one wants to reason about a small $V$ using , one can do any one of the following to avoid false negatives:

* Not using negative tests.

* Not referring to every value in $V$.

* Prefixing both sides of equations with tests representing the full set of values, e.g. for $V=\{0,1\}$, we run the query $(f\test 0 + f\test 1) \cdot e_1 \equiv (f\test 0 + f\test 1) \cdot e_2$. In this case, $f \test 0$ is equivalent to $f\testNE 1$ when appearing in $e_1$ or $e_2$.

§ OPERATIONS ON SYMBOLIC PACKETS

Recall the definition of SP from <Ref>:

\begin{align*}
p \in \SP \Coloneqq \bot \mid \top \mid
\underbrace{\SP(f, \ \{ \ldots, v_i \mapsto q_i, \ldots \},\ q)}_{\equiv \ \ \sum_i f \test v_i \cdot q_i\ +\ (\prod_i f \testNE v_i)\cdot q}
\end{align*}

We ensure that every SP ever constructed is canonical (i.e., it is Ordered and Reduced). This invariant is established by ensuring that:

* The $\SP$ constructor produces canonical-form SPs if its arguments are

* The other operations only construct SPs using the $\SP$ constructor.

The smart constructor for SPs has type

\[
\spsc\colon (F \times (V \Mapsto \SP) \times \SP) \to \SP
\]

and is defined as follows:

\[
\begin{array}{ll}
\quad \spsc(f,b,d) \triangleq
\text{ if } b' = \emptyset \text{ then } d \text{ else } \SP(f, b', d)\\
\qquad \text{where } b' \triangleq \{v \mapsto p \mid v \mapsto p \in b, p \neq d\}
\end{array}
\]

We have the following 0-ary operations:

\[p \in \SP \Coloneqq \top \mid \bot \mid (f \test v_0) \mid (f \testNE v_0) \]

The $\top$ and $\bot$ are translated directly to the corresponding SP objects.
The $f \test v_0$ and $f \testNE v_0$ are translated as follows:

\begin{align*}
(f \test v_0) &\triangleq \SP(f, \{v_0 \mapsto \one\}, \zero)\\
(f \testNE v_0) &\triangleq \SP(f, \{v_0 \mapsto \zero\}, \one)
\end{align*}

Other SPs are built from applying the following operations:

\[
\begin{array}{cc}
\nf{+}, \nf{\cdot}, \nf{\cap}, \nf{\oplus}, \nf{-}\ :\ \SP \times \SP \to \SP \qquad
\nf{\neg}, \nf{\star}\ :\ \SP \to \SP\\
\NKexists,\NKforall\ :\ F \to \SP \to \SP
\end{array}
\]

We define the base cases of the binary operations on SPs using the classic truth table definitions:

\[
\begin{array}{ll}
\top \plusop \top \triangleq \top \quad \top \cdotop \top \triangleq \top \quad \top \capop \top \triangleq \top \quad \top \oplusop \top \triangleq \bot \quad \top \minusop \top \triangleq \bot\\% \quad \negop \top \triangleq \bot\\
\top \plusop \bot \triangleq \top \quad \top \cdotop \bot \triangleq \bot \quad \top \capop \bot \triangleq \bot \quad \top \oplusop \bot \triangleq \top \quad \top \minusop \bot \triangleq \top\\% \quad \negop \bot \triangleq \top\\
\bot \plusop \top \triangleq \top \quad \bot \cdotop \top \triangleq \bot \quad \bot \capop \top \triangleq \bot \quad \bot \oplusop \top \triangleq \top \quad \bot \minusop \top \triangleq \bot\\
\bot \plusop \bot \triangleq \bot \quad \bot \cdotop \bot \triangleq \bot \quad \bot \capop \bot \triangleq \bot \quad \bot \oplusop \bot \triangleq \bot \quad \bot \minusop \bot \triangleq \bot\\
\end{array}
\]

The inductive case when the field $f$ matches both SPs can be expressed for all five operations generically, using $\pmop$ to stand for the operation:

\[
\begin{array}{ll}
\quad \SP(f, b_p, d_p)\pmop \SP(f, b_q, d_q) \triangleq  \spsc(f,b'\!,d_p \pmop  d_q)\\
\quad\quad \text{ where }\  b' = \{v \mapsto b_p(v;d_p) \pmop b_q(v;d_q) \mid v\in \keys(b_p \cup b_q)\},\text{ and}\\
\quad\quad \phantom{\text{ where }}\  b(v;d) \triangleq \text{if }v \in \keys(b) \text{ then } b[v] \text{ else }d\\
\end{array}
\]

When the fields do not match, we use a rule we call expansion to temporarily create an SP with a matching field.

\[
\begin{array}{ll}
\quad p \equiv \SP(f, \emptyset, p) \text {\qquad if \qquad} p \in \{\top, \bot, \SP(f', b, d)\} \text{ where } f \sqsubset f'\\
\end{array}
\]

Thus when we have different fields in the arguments to an operation, we simply apply expansion to the SP whose field is greater, reducing to the inductive case above.

The remaining operations are defined as follows:

\[
\begin{array}{ll}
%% \quad \negop \SP(f, b, d) \triangleq \spsc(f, b', \negop d)\\
%% \quad\quad \text{ where }\  b' = \{v\mapsto \negop p \mid v\mapsto p \in b\}\\
%% \quad \negop p \triangleq \one \minusop p\\
\quad p^{\starop} \triangleq \top\\
\end{array}
\]

\begin{align*}
\NKforall\ f_1\ p &\triangleq \begin{cases}
p       &\text{if } p = \bot \vee p = \top\\
\nf{\bigcap}_{i\leq n+1} p_i
&\text{if } p = \SP(f_1, \{v_0\mapsto p_0, \ldots, v_n\mapsto p_n\}, p_{n+1})\\
\spsc(f_2, \{v_i \mapsto \NKforall\ f_1\ p_i \mid i \leq n\}, \NKforall\ f_1\ p_{n+1})
&\text{if } p = \SP(f_2, \{v_0\mapsto p_0,\ldots, v_n\mapsto p_n\}, p_{n+1}), f_1 \neq f_2\\
\end{cases}\displaybreak[0]\\
\NKexists\ f_1\ p &\triangleq \begin{cases}
p     &\text{if } p = \bot \vee p = \top\\
\nf{\sum}_{i\leq n+1} p_i
&\text{if } p = \SP(f_1, \{v_0\mapsto p_0,\ldots, v_n\mapsto p_n\}, p_{n+1})\\
\spsc(f_2, \{v_i \mapsto \NKexists\ f_1\ p_i \mid i \leq n\}, \NKexists\ f_1\ p_{n+1})
&\text{if } p = \SP(f_2, \{v_0\mapsto p_0,\ldots, v_n\mapsto p_n\}, p_{n+1}), f_1 \neq f_2\\
\end{cases} \displaybreak[0]\\
\end{align*}

§.§ Correctness of SP operations

The goal of this section is to show that our representation of symbolic packets
is canonical and correct, in the sense that two SPs are semantically equivalent
if and only if they are syntactically equal.

First, we formally define a predicate on SPs that they are reduced and ordered.
Later we will prove the that this property implies they are canonical in the
above sense.

An SP $p$ is reduced and ordered for a field $f\in F$
if it satisfies:

\begin{align*}
&\ROf\colon \SP \to 2\\
&\ROf (p) \triangleq \begin{cases}
\top & \text{if }p = \top \vee p = \bot\ \vee\\
&\phantom{\text{if }}p = \SP(f', \{ v_0 \mapsto p_0, \ldots, v_n \mapsto p_n
\}, p_{n+1}), \text{ for } n \geq 0\ \wedge \\
& \phantom{\text{if }p = } f\sqsubset f'\  \wedge\\
& \phantom{\text{if }p = }
\forall i \in \{0,\ldots, n+1\}\colon \ROx{f'}(p_i)\ \wedge\\
& \phantom{\text{if }p = }
\forall i \in \{0,\ldots, n\}\colon p_i \neq p_{n+1}\\
\bot & \text{otherwise}
\end{cases}
\end{align*}

Moreover an SP $p$ is reduced and ordered if it satisfies:

\begin{align*}
&\RO\colon \SP \to 2\\
&\RO\ (p) \triangleq \exists f \in F\colon \ROf\ (p)
\end{align*}

For an SP $p$ such that $\ROf(p)$, then for any concrete packet $\pk$, we have
$\pk\in\pSem{p}$ implies $\forall v\in V\colon \pk[f\mut v]\in\pSem{p}$ and
$\pk\notin\pSem{p}$ implies $\forall v\in V\colon \pk[f\mut v]\notin\pSem{p}$.

By straightforward induction on $p$. The lemma holds trivially for $p=\top$ and
$p=\bot$. For the remaining cases, $\ROf(p)$ means that $p$ does not test $f$,
so the same path must be taken on $\pk[f\mut v]$ for each $v\in V$.

Now we show that our smart constructor only produces SPs which are $\RO$.

If $f \sqsubset f'$ and $\ROx{f'} (p_0),\ldots, \ROx{f'} (p_{n+1})$, then $\ROf\ (\spsc\ (f, \{ v_0 \mapsto p_0, \ldots, v_n \mapsto p_n \}, p_{n+1}))$.

After considering the assumption, we only need to argue that no child $p_i$ in $\spsc\ (f, \{ v_0 \mapsto p_0, \ldots, v_n \mapsto p_n \}, p_{n+1})$ is equal to the default case. This is true by assumption in the first case of $\spsc$ and true by construction of the second case.

If $\RO(p_1)$ and $\RO(p_2)$, then all of the following hold:

* $\RO(p_1 \nf{+} p_2)$,

* $\RO(p_1 \nf{\cdot} p_2)$,

* $\RO(p_1 \nf{\cap} p_2)$,

* $\RO(p_1 \nf{-} p_2)$,

* $\RO(p_1 \nf{\oplus} p_2)$,

* $\RO(p_1^{\nf{\star}})$,

* $\RO(\NKforall\ f\ p_1)$, and

* $\RO(\NKexists\ f\ p_1)$.

By structural induction on $p_1, p_2$. If $p_1,p_2\in\{\zero,\one\}$ the statement holds trivially by the base cases of all the operators. For the inductive case, we consider that the inductive cases use the smart constructor and apply <Ref> to conclue the result is $\RO$. We need to be slightly careful in the use of the expansion rule, which temporarily constructs a non-canonical SP (e.g., $\SP(f_1, \emptyset, p_2)$ for $p_2$, which is not $\RO$ because the test branch map is empty). This construction still works because we apply the inductive case after expansion, which calls the smart constructor—the premises of <Ref> are still met for this call by the assumptions for the original $p_1, p_2$.

Next, the smart constructor produces symbolic packets which are semantically equivalent to the plain datatype constructor:

$\pSem{\spsc(f, \{ v_0 \mapsto p_0, \ldots, v_n \mapsto p_n \}, p_{n+1})}
= \pSem{\SP(f, \{ v_0 \mapsto p_0, \ldots, v_n \mapsto p_n \}, p_{n+1})}$

The case that we return $p_{n+1}$ holds trivially, since if $p_0 = \ldots = p_n = p_{n+1}$ then also $\pSem{p_0} = \ldots = \pSem{p_{n+1}} = \pSem{\SP(f, \{ v_0 \mapsto p_0, \ldots, v_n \mapsto p_n \}, p_{n+1})}$.

In the other case we only delete branches. This is fine because branches we delete are syntactically the same as the default case. Any packets that would have gone to the deleted branch are handled equivalently by the default (i.e., $p_{n+1}$) case.

Next we will show that two SPs in canonical form are syntactically equal if and only if they
are semantically equal.

For all $p_1, p_2\in \SP$, if $\RO (p_1)$ and $\RO (p_2)$, then $p_1 = p_2 \iff \pSem{p_1} = \pSem{p_2}$.

Suppose $\RO (p_1)$ and $\RO (p_2)$.  We will show
$p_1 = p_2 \iff \pSem{p_1} = \pSem{p_2}$.

That $p_1 = p_2 \Rightarrow \pSem{p_1} = \pSem{p_2}$ is immediate because $\pSem{\cdot}$ is a function. For the other direction, we will show $p_1\neq p_2 \Rightarrow \pSem{p_1}\neq\pSem{p_2}$. We show this property by induction on $p_1, p_2$ structurally. So let $p_1, p_2\in\SP$ such that $\RO(p_1),\RO(p_2)$, and $p_1\neq p_2$. Considering symmetry, there is only one base case, i.e. that $p_1 = \top$ and $p_2 = \bot$. Then $\pSem{p_1} = \Pk \neq \emptyset = \pSem{p_2}$.

There are four inductive cases after considering symmetry:

* Let $p_1 = \top$ and $p_2 = \SP(f, \{\ldots, v_i\mapsto p_i,\ldots\}, p_{n+1})$.
It suffices to find a packet $\pk\notin\Sem{p_2}$ (since $\Sem{p_1}=\Pk$). From $\RO(p_2)$, there is a $p_i \neq p_{n+1}$ (syntactically!). Apply the induction hypothesis to get that $\pSem{p_i} \neq \pSem{p_{n+1}}$. This means that $\pSem{p_i} \neq \Pk$ or $\pSem{p_{n+1}} \neq \Pk$. In the first case, $\pSem{p_i} \neq \Pk$. Pick a packet $\pk\notin\pSem{p_i}$, then since $\ROx{f'}(p_i)$, $p_i$ cannot test $f$, so it is also the case that $\pk[f\mut v_i] \notin \pSem{p_i}$. This in turn means $\pk\notin\pSem{p}$ and therefore that $\pSem{p} \neq \top$. On the other hand if instead $\pSem{p_{n+1}} \neq \Pk$, then we pick $\pk\notin\pSem{p_{n+1}}$. By the assumption in <Ref>, then we can pick a value $v_{n+1}\notin \{v_0,\ldots,v_n\}$. Then by $\ROx{f'}(p_{n+1})$ and <Ref> we have $\pk[f\mut v_{n+1}]\notin \pSem{p_{n+1}}$ and thus $\pk[f\mut v_{n+1}]\notin \pSem{p}$, as needed.

* Let $p_1 = \bot$ and $p_2 = \SP(f, \{\ldots,v_i\mapsto p_i,\ldots\}, p_{n+1})$. We need to show $\pSem{p_2} \neq \emptyset$. By $\RO(p_2)$ there is a $p_i\neq p_{n+1}$. Apply the induction hypothesis to get $\pSem{p_i} \neq \pSem{p_{n+1}}$. Now this means either $\pSem{p_i}\neq\emptyset$ or $\pSem{p_{n+1}}\neq\emptyset$. These two subcases are similar to those in the previous case.

* Let
$p_1 = \SP(f, \{v_{1,0} \mapsto p_{1,0},\ldots, v_{1,n} \mapsto p_{1,n}\}, p_{1,n+1})$ and
$p_2 = \SP(f, \{v_{2,0} \mapsto p_{2,0},\ldots, v_{2,m} \mapsto p_{2,m}\}, p_{2,m+1})$.
We know that $p_1 \neq p_2$. There are two subcases for how this can
be true:

* We have $v_{1,i} \notin \{v_{2,0},\ldots,v_{2,m}\}$ (w.l.o.g.).
From $\RO(p_1)$, we know that $p_{1,i} \neq p_{1,n+1}$. Apply the
induction hypothesis to get that $\pSem{p_{1,i}} \neq \pSem{p_{1,n+1}}$.
In particular, let $\pk\in\pSem{p_{1,i}\oplus p_{1,n+1}}$. Then
choose $v_{1,n+1}\notin\{v_{1,0},\ldots,v_{1,n},
v_{2,0},\ldots,v_{2,m+1}\}$ and observe
that $\pk[f\mut v_{1,i}]\in\pSem{p_1} \iff \pk[f\mut
v_{1,n+1}]\notin\pSem{p_1}$. But from $v_{1,i} \notin \{v_{2,0},\ldots,v_{2,m}\}$ we know both of these packets will go to the default case of $p_2$. And $p_{2,m+1}$ is
$\ROx{f'}$, which means both packets are in $\pSem{p_2}$ or not in
$\pSem{p_2}$. We conclude $\pSem{p_1}\neq\pSem{p_2}$.

* Otherwise we can renumber $p_2$ so that
$v_{1,i} = v_{2,i}$ for all $i \in \{0,\ldots,n\}$ (noting that $(n=m)$ or else we could resolve in the previous case). Moreover there must be some $i\in \{0,\ldots,n+1\}$ for which
$p_{1,i}\neq p_{2,i}$. Applying the inductive hypothesis, we get
that $\pSem{p_{1,i}}\neq \pSem{p_{2,i}}$. Let
$\pk\in\pSem{p_{1,i}}\oplus \pSem{p_{2,i}}$. If $i \leq n$, then
$\pk[f\mut v_i]\in \pSem{p_1}\oplus\pSem{p_2}$, and otherwise if
$i=n+1$, we get $v_{n+1}\notin\{v_0,\ldots,v_n\}$ from the
assumption in <Ref> and we have
$\pk[f\mut v_{n+1}]\in \pSem{p_1}\oplus\pSem{p_2}$. In either case we
see that $\pSem{p_1}\neq\pSem{p_2}$ as needed.

* Let
$p_1 = \SP(f_1, \{v_{1,0} \mapsto p_{1,0},\ldots, v_{1,n} \mapsto p_{1,n}\}, p_{1,n+1})$,
$p_2 = \SP(f_2, \{v_{2,0} \mapsto p_{2,0},\ldots, v_{2,m} \mapsto p_{2,n}\}, p_{2,m+1})$, and
without loss of generality assume $f_1 \sqsubset f_2$.
Assume $\RO(p_1)$.
Then there is at least one $i\leq n$ for which $p_{1,i}\neq p_{1,n+1}$.
By the induction hypothesis, $\pSem{p_{1,i}}\neq \pSem{p_{1,n+1}}$.
Let $\pk\pSem{p_{1,i}}\oplus\pSem{p_{1,n+1}}$.
Let $v_{n+1}\notin\{v_0,\ldots,v_n\}$.
Now consider the two packets $\pk[f_1\mut v_i]$ and $\pk[f_1\mut v_{n+1}]$.
Clearly by construction one is in $\pSem{p_1}$ and the other is not. But they differ only by $f_1$ and $p_2$ cannot test $f_1$ because $f_1\sqsubset f_2$ and $\RO(p_2)$, so they must either both be in $\pSem{p_2}$ or both not be in $\pSem{p_2}$.
Thus one of the two packets witnesses $\pSem{p_1}\neq\pSem{p_2}$.

Finally, we show that the remaining operations defined above have the expected meanings semantically.

For SPs $p_1, p_2$, all of the following hold.

* $\pSem{p_1 \nf{+} p_2} = \pSem{p_1} \cup \pSem{p_2}.$

* $\pSem{p_1 \nf{\cdot} p_2} = \pSem{p_1} \cdot \pSem{p_2}.$

* $\pSem{p_1 \nf{\cap} p_2} = \pSem{p_1} \cap \pSem{p_2}.$

* $\pSem{p_1 \nf{-} p_2} = \pSem{p_1} - \pSem{p_2}.$

* $\pSem{p_1 \nf{\oplus} p_2} = \pSem{p_1} \oplus \pSem{p_2}.$

* $\pSem{p^{\nf{\star}}} = \pSem{p}^\star$

* $\pSem{\NKforall\ f\ p} = \{\pk\in\Pk \mid \forall v\in V\colon \pk[f\mut v] \in \pSem{p}\}$

* $\pSem{\NKexists\ f\ p} = \{\pk\in\Pk \mid \exists v\in V\colon \pk[f\mut v] \in \pSem{p}\}$

We again proceed by structural induction on $p_1, p_2$. We only show the cases for $\nf{+}$ and $\NKforall$ because the other cases are similar or reduce directly to the other operators.

* The base cases are trivial. For the inductive cases, let
$p_1 = \SP(f, \{\ldots, v_{1,j} \mapsto p_{1,j}, \ldots\},
p_{1,n+1})$, and let $p_2 = \SP(f, \{\ldots, v_{2,k} \mapsto p_{2,k},\ldots\}, p_{2,m+1})$.
Considering $\pk_f$, we either have a value $v_j \in \{v_{1,0},\ldots, v_{1,n}\}$ corresponding to a child $p_j = p_{1,j}$, or $v_j\notin\{v_{1,0},\ldots, v_{1,n}\}$, in which case we have $p_j = p_{1,n+1}.$ Similarly (treating the default cases uniformly with nondefault cases), we can select the child $p_k$ from $\{p_{2,0},\ldots, p_{2,n+1}\}.$ From this:

\begin{align*}
\pk \in \pSem{p_1 \nf{+} p_2} &\iff \pk\in\pSem{p_j \nf{+} p_k} & \text{Case analysis for $v_i,v_j$}\\
&\iff \pk\in\pSem{p_j} \cup \pSem{p_k} &\text{Induction hypothesis}\\
&\iff \pk\in\pSem{p_1} \cup \pSem{p_2} &\text{Definitions of $p_1,p_2$}
\end{align*}

On the other hand, let $p_1 = \SP(f_1, \{\ldots, v_{1,j} \mapsto p_{1,j},\ldots\}, p_{1,n+1})$, $p_2 = \SP(f_2, \{\ldots, v_{2,k} \mapsto p_{2,k}, \ldots\}, p_{2,m+1})$,  and w.l.o.g., suppose $f_1 \sqsubset f_2$. We see that the result is really by reduction to the previous case, since $p_1$ and $\SP(f_1,\emptyset,p_2)$ do match on their top level field ($f_1$). Clearly, $\pSem{p_2} = \pSem{\SP(f_1,\emptyset,p_2)}$, so that this method produces the correct result by the previous argument.

* Let $S =\{\pk\in\Pk \mid \forall v\in V\colon \pk[f\mut v] \in \pSem{p}\}$.
We need to show $\pSem{\NKforall\ f\ p} = S$:

* Base cases: let $p = \top$ or $p = \bot$. Then trivially $\pk\in S$ iff $\pk\in\pSem{\NKforall\ p\ f_1} = \pSem{p}$.

* Let $p = \SP(f_1, \{v_0\mapsto p_0, \ldots, v_n\mapsto p_n\}, p_{n+1})$. Then $\pk\in S$ iff $\pk\in \pSem{p_i}$ for $i\leq 0 \leq n+1$, since the children (incl. default case) cover all values $v\in V$. But this is the same as $\pk\in \nf{\bigcap}_{i\leq n+1} p_i$.

* Let $p = \SP(f_2, \{v_0\mapsto p_0, \ldots, v_n\mapsto p_n\}, p_{n+1})$, with $f_1\neq f_2$. Then $\pk\in \pSem{p}$ iff $\pk\in\pSem{\NKforall f_1 p_i}$ for some child $p_i$ of $p$, depending on the value of $\pk_{f_2}$. By the induction hypothesis, this is equivalent to $\pk[f_1 \mut v]\in \pSem{p_i}$ for all $v\in V$. But then we know $\pk[f_1 \mut v]_{f_2} = \pk_{f_2}$, so this is equivalent to $\pk[f_1\mut v]\in\pSem{p}$ for all $v\in V$, i.e. that $\pk\in S$, as needed.

§ OPERATIONS ON SYMBOLIC PACKET PROGRAMS

In the implementation, there is also datatype defined for SPPs. We define its
operations in this section.

Recall the definition of :

\begin{align*}
p \in \SPP \Coloneqq\ &\bot \mid \top \mid
\underbrace{
\SPP(f, \{ \ldots, v_i \mapsto \{ \ldots, w_{ij} \mapsto q_{ij}, \ldots \}, \ldots \}, \{ \ldots, w_i \mapsto q_i, \ldots \}, q)
\equiv\ \ \sum_i f \test v_i \cdot \sum_j f \mut w_{ij} \cdot q_{ij}\ +\ \
(\prod_i f \testNE v_i) \cdot (\sum_i f \mut w_i\ +\ (\prod_i f \testNE w_i) \cdot q)
\end{align*}

As before, our $\SPP$ tuple here matches the  object type in the
implementation, and we also only construct which are
canonical, in the sense of <Ref>. We formalize this
canonicalization property in <Ref>.

First of all, there is a straightforward embedding from SP into SPP:

\[
\begin{array}{ll}
\quad\SPPid\colon \SP \to \SPP\\
\SPPid (\zero) = \zero \qquad \SPPid (\one) = \one\\
\SPPid(\SP(f, b, d)) = \SPP(f, \{v_i\mapsto\{v_i\mapsto p_i\} \mid v_i\mapsto p_i \in b\}, \SPPid (d))\\
\end{array}
\]

Observe that by applying the embedding to the SP definition for $f\test v$ and $f\testNE v$, we obtain the SPP forms for them:

\begin{align*}
(f\test v) &=  \SPP(f, \{v\mapsto\one\}, \emptyset, \zero) \\
(f\testNE v) &= \SPP(f, \{v\mapsto\zero\}, \emptyset, \one)
\end{align*}

In addition to this embedding, we only need one additional constructor:

\begin{align*}
(f \mut v) &\triangleq \SPP(f, \emptyset, \{v \mapsto \one\}, \zero)
\end{align*}

The remaining SPPs we will construct from the operations given below.

§.§ Canonicalization

Once again, we define a smart constructor to help maintain the invariant that
all SPPs in memory are canonical:

\begin{align*}
\sppsc\colon (F\times (V\Mapsto(V\Mapsto\SPP)) \times (V\Mapsto\SPP) \times \SPP) \to \SPP
\end{align*}

Here is the definition:

\begin{align*}
\quad\sppsc(f,b,m,d) \triangleq\
&\text{if } m' = \emptyset \land b'' = \emptyset \text{ then } d \text{ else } \SPP(f, b'', m', d)\\
\text{ where }\\
&m' = \{ v \sto p \mid v \sto p \in m \land p \neq \bot \}\\
\quad \phantom{\text{ where }}\  &b' = \{ v \sto \{ w \sto p \mid w \sto p \in m \land p \neq \bot \} \mid v \sto m \in b \} \cup \{ v \sto \emptyset \mid v \sto \bot \in m \land v \notin b \}\\
\quad \phantom{\text{ where }}\  &b'' = \{ v \sto m \mid v \sto m \in b' \land m \neq (\text{if } v \in \keys(m') \lor d = \bot \text{ then } m' \text{ else } m' \cup \{ v \sto d \}) \}\\
\end{align*}

§.§ Operations

In the rest of this section we give the definitions for the remaining operations used to
build SPPs.

\begin{align*}
\nf{+}, \nf{\cdot}, \nf{\cap}, \nf{\oplus}, \nf{-}\ :\ \SPP \times \SPP \to \SPP \qquad
\nf{\star}\ :\ \SPP \to \SPP \qquad
\end{align*}

The base cases are identical to the corresponding operations on SPs, so we omit them here.
Similar to SPs, the inductive case for $\nf{+}, \nf{\cap}, \nf{\oplus},$ and $\nf{-}$ can be expressed at once. We do so here using $\pmop$. The notation $b(v;d)$ means the child $b(v)$ if $v \in \keys(b)$, or by default $d$ otherwise.

\[
\begin{array}{ll}
\quad \SPP(f, b_p, m_p, d_p)\pmop \SPP(f, b_q, m_q, d_q) \triangleq  \sppsc(f,b'\!,m_p \mathop{\vec{\pm}} m_q,d_p \pmop  d_q)\\
\whereindent \text{ where }\  b' = \{v \sto \get{p}{v} \mathop{\vec{\pm}} \get{q}{v} \mid v\in \keys(b_p \cup b_q \cup m_p \cup m_q) \}\\
\quad m_1 \mathop{\vec{\pm}} m_2 \triangleq \{v \,\sto\, m_1(v;\bot) \pmop m_2(v;\bot) \mid v\in \keys(m_1 \cup m_2)\},\\
\quad \get{p}{v} \triangleq b_p(v; \text{ if } v \in m_q \lor d_p = \bot \text{ then } m_p \text{ else } m_p \cup \{ v \sto d_p \}) \text{\quad (similarly for $q(v)$)}\\
\end{array}
\]

Sequencing ($\nf{\cdot}$) is more subtle and needs to be defined separately (using $\vec{\Sigma} \triangleq \text{$n$-ary sum w.r.t. $\vec{+}$}$ as defined above):

\[
\begin{array}{ll}
\quad \SPP(f, b_p, m_p, d_p)\cdotop \SPP(f, b_q, m_q, d_q) \triangleq  \sppsc(f,b'\!,m_A \mathop{\vec{+}} m_B, d_p \cdotop  d_q)\\
\whereindent \text{ where }\  b' = \{v \sto \unionmaps{v'\! \sto p' \in \get{p}{v}}{ \{ w'\! \sto p' \nf{\cdot} q' \mid w'\! \sto q' \in \get{q}{v'}\} } \mid v\in \keys(b_p \cup b_q \cup m_p \cup m_q \cup m_A)\}\\
\whereindent \phantom{\text{ where }}\  m_A = \unionmaps{v'\! \sto p' \in m_p}{ \{ w'\! \sto p' \nf{\cdot} q' \mid w'\! \sto q' \in \get{q}{v'}\} },
\quad m_B = \{ w'\! \sto d_p \nf{\cdot} q' \mid w'\! \sto q' \in m_q \} \\
\end{array}
\]

The expansion rule works similarly to the SP case. Namely, when the fields do not match, we expand the SPP with the greater field by:

\[
\quad p \equiv \SPP(f, \emptyset, \emptyset, p) \text {\qquad if \qquad} p \in \{\top, \bot, \SPP(f'\!, b, m, d)\} \text{ where } f \sqsubset f'\\
\]

Finally star is defined by:

\[
\begin{array}{ll}
p^{\nf{\star}} \triangleq \nf{\Sigma}_{i=0,1,\ldots} p^{i}\\
\whereindent\text{ where } \quad p^0 \triangleq \top \\
\whereindent\phantom{\text{ where }} \quad p^n \triangleq p \nf{\cdot} p^{n-1} \quad \text{ for }n \geq 1
\end{array}
\]

In the implementation we perform repeated concatenations until the SPP no longer changes (i.e., the fixpoint is reached).

§.§ Push and Pull

First we define two helper functions which “flatten” SPPs into SPs:

\begin{align*}
\mathsf{fwd} :\ \SPP \to \SP \qquad\qquad \mathsf{bwd} :\ \SPP \to \SP
\end{align*}

The idea of $\mathsf{fwd}$ is to collect a symbolic packet representing the set of output packets
for an SPP when the input packets can be any packet:

\[
\begin{array}{ll}
\quad\mathsf{fwd}(\one) \triangleq \one\\
\quad\mathsf{fwd}(\zero) \triangleq \zero\\
\quad\mathsf{fwd}(\SPP(f, b, m, d)) \triangleq \spsc(f, b_A \vecplus b_B \vecplus b_C \vecplus b_D, \mathsf{fwd}(d))\\
\quad\whereindent \text{ where }\ b_A = \{ v' \sto \mathsf{fwd}(p') \mid v' \sto p' \in m \}\\
\quad\whereindent \phantom{\text{ where }}\ b_B = \unionmaps{v' \sto m' \in b}{ \{ w' \sto \mathsf{fwd}(p') \mid w' \sto p' \in m' \} }\\
\quad\whereindent \phantom{\text{ where }}\  b_C = \{ v' \sto \mathsf{fwd}( d) \mid v' \in \keys(b_B) \setminus (\keys(b) \cup \keys(m)) \}\\
\quad\whereindent \phantom{\text{ where }}\ b_D = \{ v' \sto \bot \mid v' \in \keys(b) \setminus \keys(b_B) \}
\end{array}
\]

Conversely, $\mathsf{bwd}$ gives the set of input packets which, when input to the given SPP, produce some nonempty set of packets as output:

\[
\begin{array}{ll}
\quad\mathsf{bwd}(\one) \triangleq \one\\
\quad\mathsf{bwd}(\zero) \triangleq \zero\\
\quad\mathsf{bwd}(\SPP(f, b, m, d)) \triangleq \spsc(f, b_A \vecplus b_B, d' \plusop \mathsf{bwd}(d))\\
\quad\whereindent \text{ where }\  d' = \nf{\Sigma}_{v' \sto p' \in m} \mathsf{bwd}(p')\\
\quad\whereindent \phantom{\text{ where }}\  b_A = \{ v' \sto \nf{\Sigma}_{w' \sto p' \in m'} \mathsf{bwd}(p') \mid v' \sto m' \in b \}\\
\quad\whereindent \phantom{\text{ where }}\  b_B = \{ v \sto d' \mid v \in \keys(m) \setminus \keys(b) \}
\end{array}
\]

Recall the push and pull operations which are described in <Ref>:

\begin{align*}
\mathsf{push} :\ \SP \to \SPP \to \SP \qquad\qquad \mathsf{pull} :\ \SPP \to \SP \to \SP
\end{align*}

We conclude the section with their definitions:

\begin{align*}
&\mathsf{push}\ p\ s \triangleq \mathsf{fwd}((\SPPid\ p) \cdotop s),\\
&\mathsf{pull}\ s\ p \triangleq \mathsf{bwd}(s \cdotop (\SPPid\ p)),
\end{align*}

§.§ Correctness of SPP operations

Finally, we give proofs that the SPP operations maintain a canonical form and have the expected
semantic meanings.

An SPP $p$ is reduced and ordered for a field $f\in F$ if it satisfies:

\begin{align*}
&\ROsppf\colon \SPP \to 2\\
&\ROsppf (\zero) \triangleq \one \qquad\qquad \ROsppf (\one) \triangleq \one\\
\end{align*}

$\ROsppf (\SPP(f',b,m,d)) \triangleq \one$ if all of the following hold:

* $b\neq\emptyset \vee m\neq\emptyset$

* $f \sqsubset f'$

* $\forall (v_i\mapsto m_i)\in b.\ (\forall (v_j\mapsto p_j)\in m_i.\ \ROsppx{f'}(p_j) \wedge p_j\neq \zero)$

$\wedge ((m_i\neq m \wedge (v_i\in\keys(m)\vee d=\zero))\vee(m_i\neq(m\cup \{v_i\mapsto d\})\wedge v_i\notin\keys(m)\wedge d\neq\zero))$

* $(\forall v\mapsto p_i) \in m.\ \ROsppx{f'}(p_i) \wedge p_i\neq \zero$

* $\ROsppx{f'}(d)$

$\ROsppf (\SPP(f',b,m,d)) \triangleq \zero$ otherwise.

More generally, an SPP $p$ is reduced and ordered if it satisfies:

\begin{align*}
&\ROspp\colon \SPP \to 2\\
&\ROspp\ (p) \triangleq \exists f \in F\colon \ROsppf\ (p)
\end{align*}

Using this definition, we first establish that the smart constructor only produces reduced and ordered SPPs, provided the children in the test and mutation branches are already reduced and ordered.

Let $f\in F, b\in V\Mapsto(V\Mapsto\SPP), m\in V\Mapsto\SPP, d\in\SPP$. If all of the following hold:

* $f \sqsubset f'$,

* $\forall v_i\mapsto m_i\in b.\ (\forall v_j\mapsto p_j\in m_i.\ \ROsppx{f'}(p_j))$

* $\forall v_i\mapsto p_i \in m.\ \ROsppx{f'}(p_i)$

* $\ROsppx{f'}(d)$

Then $\ROsppf\ (\sppsc(f, b, m, d))$.

Clearly if $\sppsc(f, b, m, d) = \zero$ or $\sppsc(f, b, m, d) = \one$ then the result holds trivially.
So suppose $\SPP(f, b'', m', d) = \sppsc(f, b, m, d)$. Note the variable names are chosen to match those in the definition of $\sppsc$). We establish the criteria of $\ROspp$ one at a time, following the list in the definition.

* Holds because both $b''$ and $m'$ being empty is prevented by the outermost if statement in $\sppsc$.

* By assumption (a).

* Let $(v_i\mapsto m_i)\in b''$ and let $v_j \mapsto p_j\in m_i$. We have $\ROsppx{f'}(p_j)$ by assumption (b). In addition, $p_j \neq \zero$ because such bindings are filtered out in the construction of $b'$, and the construction of $b''$ only removes more bindings (not adding any). The remaining condition matches precisely what is checked by the construction of $b''$.

* Let $(v_i\mapsto p_i)\in m'$. That we have $\ROsppx{f'}(p_i)$ holds by assumption (c). That $p_i\neq\zero$ is true because such bindings are removed by the construction of $m'$ from $m$.

* By assumption (d).

Next, it follows that all of the operations maintain the property of being reduced and ordered.

If for SPPs $p_1,p_2$, we have $\ROspp(p_1)$ and $\ROspp(p_2)$, then all of the following hold:

* $\ROspp(p_1 \nf{+} p_2)$,

* $\ROspp(p_1 \nf{\cdot} p_2)$,

* $\ROspp(p_1 \nf{\cap} p_2)$,

* $\ROspp(p_1 \nf{-} p_2)$,

* $\ROspp(p_1 \nf{\oplus} p_2)$,

* $\ROspp(p_1^{\nf{\star}})$,

Because we only use the smart constructor to create SPPs in the definitions of all of the operations,
we only need to show that the premises of <Ref> are satisfied when the smart constructor is used.
Indeed, these premises are guaranteed by $\ROspp(p_1)$, and $\ROspp(p_2)$, and comparisons of $f, f'$ in the definitions of the operations. We only need to be slightly careful in the cases where the smart constructor is not used (since the expansion form is not RO), but each of these is a direct reduction to a case where the smart constructor is used. Note that the default case of the expansion form is still RO by assumption, and the expansion rule itself maintains the field order.

The main benefit of canonicalization is that, after establishing reduced an ordered form, we can check semantic equivalence by checking syntactic equivalence, which we show next.

For all $p_1, p_2\in \SP$, if $\ROspp (p_1)$ and $\ROspp (p_2)$, then $p_1 = p_2 \iff \pSem{p_1} = \pSem{p_2}$.

Suppose $\ROspp(p_1)$ and $\ROspp(p_2)$.
($\Rightarrow$) is immediate because $\Sem{\cdot}$ is a function. ($\Leftarrow$). Suppose $p_1 \neq p_2$ (syntactically). We will show $\Sem{p_1} \neq \Sem{p_2}$ by induction on the structure of $p_1, p_2$:

* Let $p_1=\zero$, and let $p_2=\one$. Then $\Sem{p_1}=\emptyset$ and $\pk\in\Sem{p_2}(\pk)$ for all $\pk\in\Pk$.

* Let $p_1=\zero$, and let $p_2=\SPP(f,b,m,d)$.
We only need to show that $\Sem{p_2}$ is nonempty. First of all, if $d\neq\zero$, we are done, since by induction this means $\Sem{d}\neq\emptyset$, and moreover $\pkp\in\Sem{d}(\pk)$ means that $\pkp\in\Sem{p_2}(\pk[f\mut v])$ for any $v\notin\keys(b)\cup\keys(m)$. So assume $d=\zero$. Either $b\neq\emptyset$ or $m\neq\emptyset$. If $m\neq\emptyset$ we are done, because $v\mapsto p \in m$ means that $p\neq\zero$, and thus by the induction hypothesis that there are $\pk,\pkp\in\Pk$ for which $\pkp\in\Sem{p}$. It follows that $\pkp[f\mut v]\in\Sem{p_2}(\pk)$. So assume $m = \emptyset$. Then there is some $(v_i\mapsto m_i)\in b$. Now because $d=\zero$ and $m=\emptyset$, item (3) of the definition of $\ROsppf$ says that $m_i\neq\emptyset$. Thus there is some $v_j\mapsto p_j\in m_i$ for which $p_j\neq\zero$. So there are packets $\pk,\pkp$ such that $\pkp\in\Sem{p_j}(\pk)$, and thus $\pkp[f\mut v_j]\in\Sem{p_2}(\pk[f\mut v_i])$.

* Let $p_1=\one$, and let $p_2=\SPP(f,b,m,d)$. We need to show $p_2$ modifies $(\pkp\in\Sem{p_2}(\pk)$ for $\pkp\neq\pk$) or drops a packet ($\Sem{p_2}(\pk)=\emptyset$).
If $d\neq\one$, then by the induction hypothesis, either $\pkp\in\Sem{d}(\pk)$ for $\pkp\neq\pk$ or $\Sem{d}(\pk)=\emptyset$. Then for $\pk[f\mut v]$ for $v\notin\keys(b)\cup\keys(m)$, we have either $\pkp[f\mut v]\in\Sem{p_2}(\pk[f\mut v])$ with $\pkp[f\mut v]\neq \pk[f\mut v]$ or $\Sem{p_2}(\pk[f\mut v])=\emptyset$, respectively. So assume $d=\one$. If $(v_i\mapsto p_i)\in m$, then since $p_i\neq\zero$, we have $\pk[f\mut v_i]\in\Sem{p_2}(\pk[f\mut v_j])$ for any $v_j\neq v_i$. So assume $m=\emptyset$. Since then $b\neq\emptyset$,  there is some $(v_i\mapsto m_i)\in b$. From item (3) of the definition of $\ROsppf$, we know $m_i\neq\{v_i\mapsto\one\}$. There are several subcases based on what $m_i$ can be:

* If $m_i=\emptyset$, we are done since then $\Sem{p_2}(\pk[f\mut v_i])=\emptyset$.

* If $m_i=\{v_j\mapsto\one,\ldots\}$, with $v_j\neq v_i$. Then $\pk[f\mut v_j]\in\Sem{p_2}\pk[f\mut v_i]$ (for any $\pk$).

* If $m_i = \{v_j \mapsto p_j,\ldots\}$ with $p_j\neq\one$ (but possibly $v_i=v_j$), then we have by the induction hypothesis either a packet $\pk$ such that $\Sem{p_j}(\pk)=\emptyset$ (in which case $\Sem{p_2}(\pk[f\mut v_i])=\emptyset$), or some $\pkp[f\mut v_j]\neq\pk[f\mut v_j]$ such that $\pkp\in\Sem{p_j}(\pk)$ (in which case $\pkp[v\mut v_j]\in\Sem{p_2}(\pk[f\mut v_i]$).

* Let $p_1=\SPP(f_1,b_1,m_1,d_1)$, and let $p_2=\SPP(f_2,b_2,m_2,d_2)$. We proceed by the cases in which $p_1$ and $p_2$ may differ syntactically, and show why each leads to a difference in semantics:

* Suppose $f_1\sqsubset f_2$, and suppose $v_i\mapsto p_i\in m_1$. Then $p_i\neq\zero$, meaning there are packets $\pk,\pkp$ for which $\pkp\in\Sem{p_i}(\pk)$. Pick $v_j\notin\keys(b_1)\cup\keys(m_1)$. Then
$\pkp[f_1\mut v_i]\in\Sem{p_1}(\pk[f_1\mut v_j])$, but $p_2$ cannot modify $f_1$ at all, so we must have $\pkp[f_1\mut v_i]\notin\Sem{p_2}(\pk[f_1\mut v_j])$. On the other hand suppose $m_1=\emptyset$. Then there must be $v_i\mapsto m_i\in b_1$. Now we have two cases, in item (3) of $\ROspp (p_1)$:

* Let $d_1=\zero$. Then $m_i\neq\emptyset$. Let $v_j\mapsto p_j\in m_i$. Note $p_j\neq\zero$.
Then for $\pk,\pkp$ such that $\pkp\in\Sem{p_j}(\pk)$, we have $\pkp[f_1\mut v_j]\in\Sem{p_1}(\pk[f_1\mut v_i])$. If $v_i\neq v_j$, we are done, since $p_2$ cannot modify $f_1$. Otherwise let $v_j'\notin\keys(b_1)\cup\keys(m_1)$. Then because $d_1=\zero$, $\Sem{p_1}(\pk[f_1\mut v_i])\neq\emptyset=\Sem{p_1}(\pk[f_1\mut v_j'])$. But $p_2$ cannot test $f_1$, so we must have $\Sem{p_2}(\pk[f_1\mut v_i])=\Sem{p_2}(\pk[f_1\mut v_j'])$.

* Let $d_1\neq\zero$. Then $m_i\neq\{v_i\mapsto d_1\}$. This means for any $v_j\notin\keys(b_1)\cup\keys(m_1)$, there must be some $\pk,\pkp$ such that
$\pkp[f_1\mut v_i] \in \Sem{p_1}(\pk[f_1\mut v_i]) \iff \pkp[f_1\mut v_j]\notin\Sem{p_1}(\pk[f_1\mut v_j])$. But $p_2$ cannot test $f_1$, so we are done.

For the remaining cases, we let $f = f_1 = f_2$.

* Suppose $d_1\neq d_2$.
Then by the induction hypothesis there is a packet $\pk$ for which $\Sem{d_1}(\pk)\neq\Sem{d_2}(\pk)$. We just pick a value $v\notin\keys(b_1)\cup\keys(m_1)\cup\keys(m_2)\cup\keys(b_2)$, and we get $\Sem{p_1}(\pk[f\mut v])\neq\Sem{p_2}(\pk[f\mut v])$.

* Suppose $\keys(m_1)\neq\keys(m_2)$.
Then (w.l.o.g.) let $v_i\mapsto p_i\in m_1$ and $v_i\notin\keys(m_2)$, and choose $v\notin\keys(b_1)\cup\keys(m_1)\cup\keys(b_2)\cup\keys(m_2)$. Then since $p_i\neq\zero$, there are $\pk,\pkp\in\Pk$ such that $\pkp\in\Sem{p_i}(\pk)$. This means $\pkp[f\mut v_i]\in\Sem{p_1}(\pk[f\mut v])$, but $\pkp[f\mut v_i]\notin\Sem{p_2}(\pk[f\mut v])$.

* Suppose $v\mapsto p_i\in m_1$, while $v\mapsto p_j\in m_2$, and $p_i\neq p_j$.
By the induction hypothesis, there is a $\pk\in\Pk$ for which $\Sem{p_i}(\pk)\neq\Sem{p_j}(\pk)$. Pick $v\notin\keys(b_1)\cup\keys(b_2)\cup\keys(m_1)\cup\keys(m_2)$. Then $\Sem{p_1}(\pk[f\mut v]) \neq \Sem{p_2}(\pk[f\mut v])$.

* Assume $d_1=d_2$ and $m_1=m_2$, but suppose $\keys(b_1)\neq\keys(b_2)$.