Programming and Reasoning with KAT - Lab 1

This lab consists of a few pencil-and-paper Kleene Algebra exercises and an interactive tutorial that introduces the basic features of NetKAT.

Kleene Algebra Exercises

// By the definition of 2x2 matrix multiplication we have [ a b ] · [ 1 0 ] = [ (a·1 + b·0) (a·0 + b·1) ] [ c d ] [ 0 1 ] [ (c·1 + d·0) (c·0 + d·1) ] ≡ // By Unit and Annihilator for the Kleene Algebra we have [ a b ] [ c d ] // We analyze two cases // Case 1: min(q,r) = q // Then we also have min(p·q, p·r) = p·q // By then definition of multiplication in the tropical Kleene Algebra // Hence p·(q + r) ≡ // Definition of addition p·q ≡ // By definition of addition and the property above p·q + p·r // Case 2: min(q,r) = r // Symmetric to the previous case 1 + x* ≡ // Fixpoint 1 + (1 + x·x*) ≡ // Associativity (1 + 1) + x·x* ≡ // Idempotence 1 + x·x* ≡ // Fixpoint x* x + x* ≡ // Fixpoint x + 1 + x·x* ≡ // Fixpoint x + 1 + x·(1 + x·x*) ≡ // Distributivity x + 1 + x·1 + x·x·x* ≡ // Unit x + 1 + x + x·x·x* ≡ // Commutativity 1 + x + x + x·x·x* ≡ // Associativity, Idempotence 1 + x + x·x·x* ≡ // Distributivity 1 + x·(1 + x·x*) ≡ // Fixpoint 1 + x·x* ≡ // Fixpoint x* // Prove inclusions in each direction // Lemma: x* ≤ x*·x* // By Exercise above 1 ≤ x* => // Monotonicity x*·1 ≤ x*·x* => // Unit x* ≤ x*·x* // Lemma: x* ≤ x*·x* x* + x·x* + x* ≡ // Fixpoint 1 + x·x* + x·x* + x* ≡ // Idempotence 1 + x·x* + x* ≡ // Fixpoint x* + x* ≡ // Idempotence x* // Prove inclusions in each direction //Lemma: x* ≤ x** x* + x** ≡ // Fixpoint x* + 1 + x*·x** ≡ // Fixpoint x* + 1 + x*·(1 + x*·x**) ≡ // Distributivity x* + 1 + x* + x*·x*·x** ≡ // Associativity, Idempotence 1 + x* + x*·x*·x** ≡ // Distributivity 1 + x*·(1 + x*·x**) ≡ // Fixpoint 1 + x*·x** ≡ // Fixpoint x** // Auxiliary Lemma: 1 + x*·x* ≤ x* Proof. 1 + x*·x* ≡ // By previous Lemma 1 + x* ≡ // Fixpoint 1 + 1 + x·x* ≡ // Associativity, Idempotence 1 + x·x* ≡ // Fixpoint x* // Lemma: x** ≤ x* //By Auxiliary Lemma and Least Fixpoint (q + p·y ≤ y → p*·q ≤ y) with - q = 1, - p = x*, and - y = x*, // we have: x**·1 ≤ x* // Then, by Idempotence, we have x** ≤ x* //Lemma: (a*·b)*·a* ≤ (a + b)* //See proof from Lecture 1 using mononoticity //Lemma: (a + b)* ≤ (a*·b)*·a* //Observe 1 ≤ a*·(b·a*)* a·a*·(b·a*)* ≤ a*·(b·a*)* b·a*·(b·a*)* ≤ (b·a*)* ≤ a*·(b·a*)* //Hence 1 + (a + b)·a*·(b·a*)* ≤ 1 + a·a*·(b·a*)* + b·a*·(b·a*)* ≤ a*·(b·a*)* // By Least Fixpoint (q + p·y ≤ y → p*·q ≤ y) with - q = 1 - p = (a + b) - y = a*·(a*·b)* // we have (a + b)*·1 ≤ a*·(a*·b)* // By Idempotence we have (a + b)* ≤ a*·(a*·b)* // By the Sliding rule (proved next), we have (a + b)* ≤ (a*·b)*·a* //Prove inclusions in each direction //Lemma: p·(q·p)* ≤ (p·q)*·p //We first show: p + ((p· q)*· p)· (q·p) ≤ (p·q)*·p. p + ((p·q)*·p)·(q·p) ≡ // Associativity p + ((p·q)*·(p·q))·p ≡ // Distributivity (1 + (p·q)*·(p·q))·p = // Fixpoint (p·q)*·p // By Least Fixpoint (q + y·p ≤ y -> q·p* ≤ y) with - q = p - p = (q·p) - y = (p·q)*·p // we have p·(q·p)* ≤ (p·q)*·p //Lemma: (p·q)*·p ≤ p·(q·p)* // We first show: p + (p·q)·p·(q·p)* ≤ p·(q·p)* p + (p·q)·p·(q·p)* ≡ // Associativity p + p·(q·p)·(q·p)* ≡ // Distributivity p·(1 + (q·p)·(q·p)* ≡ // Fixpoint p·(q·p)* // By Least Fixpoint (q + p·y ≤ y -> p*·q ≤ y) with - q = p - p = (p·q) - y = (p·q)*·p // we have (p·q)*·p ≤ p·(q·p)* //Prove each implication separately //For the forward implication, by c ≤ 1 // and monotocity, we have b·p·c ≤ b·p. //The backward implication is trivial //Prove each implication separately //For the forward implication b·p·!c ≡ // Assumption b·p·c·!c ≡ // Contradiction b·p·0 ≡ // Annihilator //For the reverse implication b·p ≡ // Unit b·p·1 ≡ // Excluded middle b·p·(c + !c) ≡ // Distributivity b·p·c + b·p·!c ≡ // Assumption b·p·c + 0 ≡ // Unit b·p·c

NetKAT Tutorial

The rest of this lab is an interactive tutorial that introduces the basic features of NetKAT.

Packets and Variables

In NetKAT, a packet is represented as a sequence (or vector) of bits. We use variables like x0, x1, x2, and so on, to refer to these bits. For example, if a packet is 101, then:

• x0 would be 1 (the first bit)
• x1 would be 0 (the second bit)
• x2 would be 1 (the third bit)

Real-World Example: Ethernet Frame

In real networking, packets have structured fields. Here's a simplified Ethernet frame showing how packet bits correspond to actual network data:

In this example:

• x0-x47 would represent the 48-bit destination MAC address
• x48-x95 would represent the 48-bit source MAC address
• x96-x111 would represent the 16-bit EtherType field
• x112 and beyond would be the start of the payload data, but the payload is typically not modeled in NetKAT

NetKAT policies can test or modify any of these bits to implement network behavior like filtering, forwarding, or packet transformation.

Tests (Packet Filters)

Tests are conditions that check the value of a packet bit. They act as filters: if the condition is true, the packet passes through; otherwise, it is dropped (or "filtered out").

Try this example in the interactive editor below:

// You can edit this to test different programs x2 == 1 // The analysis results will be displayed here:

You can also test for equality to 0, like x3 == 0.

x1 == 0

Note that the examples displayed are as wide as the largest bit mentioned in the program.

Assignments

Assignments modify the packet's bits. The expression x2 := 1 sets the third bit of the packet to 1, regardless of its previous value.

Experiment with this assignment in the editor below:

x2 := 1 x2 := 0

Sequential Composition

Sequential composition, denoted by a semicolon ;, combines two NetKAT expressions by executing them one after the other. The packet output by the first expression becomes the input to the second.

See this sequential flow in action in the editor below:

x2 == 1; x1 := 0 x0 == 1; x2 := 0

You can also chain multiple assignments together:

x0 := 1; x2 := 0

Choice (Union)

Choice, denoted by a plus sign +, combines two NetKAT expressions and can be interpreted in two ways:

Nondeterministic Interpretation: The network can choose to follow either path - it's an "either/or" decision where one path is selected.

Multicast Interpretation: The network simultaneously sends copies of the packet down both paths - it's a "both" scenario. This is useful for modeling broadcast scenarios, load balancing, or redundant forwarding where you want a packet to reach multiple destinations.

Watch the effect of branching in the editor below:

x0 := 1 + x1 := 1 x0 == 1 + x1 := 0

Dup (Logging)

The dup keyword is a special NetKAT operator that records the current packet state to the trace output without modifying it. This is extremely useful for observing the packet state at various points in your NetKAT expression.

See how dup creates intermediate trace entries in the editor below:

x1 := 1; dup; x2 := 1 x0 := 1; dup; x1 := 1; dup

Iteration (Kleene Star)

Iteration, denoted by an asterisk * (Kleene star) after an expression e (i.e., e*), allows an expression to be executed zero or more times.

Explore the multiple iteration paths in the editor below:

((x0:=1 + (x0==1;x1:=1) + (x1==1; x2:=1)); dup)*

This shows multiple paths in the trace, corresponding to 0, 1, 2, etc., iterations, up to a limit defined by the analyzer to prevent infinite loops in the visualization.

((x0 := 0 + x0 := 1); dup)*

Logical Operators

NetKAT expressions represent sets of traces (sequences of packet transformations). NetKAT's logical operators correspond to set operations on these trace sets, making them powerful tools for both constructing complex policies and verifying network properties.

Union (+)

We've already seen the union operator +. From a formal perspective, this represents the set union of traces from both expressions - the result contains all traces that are generated by either the left or right expression. This gives us a third interpretation alongside the nondeterministic and multicast views:

• Nondeterministic: Choose one path
• Multicast: Send packets down both paths
• Set-theoretic: Union of two trace sets

Intersection (&)

The intersection operator & represents the set intersection of traces. A trace appears in the result only if it's generated by both expressions.

Symmetric Difference / XOR (^)

The XOR operator ^ represents the symmetric difference of trace sets - traces that are in one set but not both.

Difference (-)

The difference operator - represents the set difference - traces that are in the first set but not in the second set.

Using Logical Operators for Verification

These set operations are particularly powerful for network verification:

Subset Check (A ⊆ B)

To verify that the trace set of A is a subset of the trace set of B, check if A - B is empty. If it's not empty, the analyzer will show you traces that are in A's set but not in B's set.

Equality Check (A = B)

To verify that two expressions generate the same trace set, check if A ^ B is empty. If it's not empty, the traces show you which traces appear in one set but not the other.