google · copybara-service · Nov 19, 2025
diff --git a/netkat/BUILD.bazel b/netkat/BUILD.bazel
@@ -276,14 +276,32 @@ cc_library(
     hdrs = ["paged_stable_vector.h"],
 )
 
+cc_library(
+    name = "counter_example",
+    srcs = ["counter_example.cc"],
+    hdrs = ["counter_example.h"],
+    deps = [
+        ":evaluator",
+        ":packet_set",
+        ":packet_transformer",
+        "@com_google_absl//absl/container:flat_hash_set",
+        "@com_google_absl//absl/log:check",
+        "@com_google_absl//absl/status",
+        "@com_google_absl//absl/status:statusor",
+    ],
+)
+
 cc_library(
     name = "analysis_engine",
     srcs = ["analysis_engine.cc"],
     hdrs = ["analysis_engine.h"],
     deps = [
+        ":counter_example",
         ":frontend",
         ":packet_set",
         ":packet_transformer",
+        "@com_google_absl//absl/log:check",
+        "@com_google_absl//absl/status:statusor",
     ],
 )
 

diff --git a/netkat/analysis_engine.cc b/netkat/analysis_engine.cc
@@ -14,6 +14,9 @@
 
 #include "netkat/analysis_engine.h"
 
+#include "absl/log/check.h"
+#include "absl/status/statusor.h"
+#include "netkat/counter_example.h"
 #include "netkat/frontend.h"
 #include "netkat/packet_set.h"
 #include "netkat/packet_transformer.h"
@@ -26,9 +29,24 @@ bool AnalysisEngine::CheckEquivalent(const Predicate& left,
          packet_transformer_manager_.Compile(Filter(right).ToProto());
 }
 
-bool AnalysisEngine::CheckEquivalent(const Policy& left, const Policy& right) {
-  return packet_transformer_manager_.Compile(left.ToProto()) ==
-         packet_transformer_manager_.Compile(right.ToProto());
+SuccessOrCounterExample AnalysisEngine::CheckEquivalent(const Policy& left,
+                                                        const Policy& right) {
+  PacketTransformerHandle left_packet_transformer =
+      packet_transformer_manager_.Compile(left.ToProto());
+  PacketTransformerHandle right_packet_transformer =
+      packet_transformer_manager_.Compile(right.ToProto());
+  if (left_packet_transformer == right_packet_transformer) {
+    return SuccessOrCounterExample();
+  }
+  absl::StatusOr<CounterExample> counter_example =
+      CounterExample::CreateEquivalenceCounterExample(
+          left_packet_transformer, right_packet_transformer,
+          &packet_transformer_manager_);
+  // This is expected to succeed since we already checked that the policies are
+  // not the same and the Analysis Engine owns the PacketTransformerManager, so
+  // this cannot be out of scope when creating the CounterExample.
+  CHECK_OK(counter_example.status());  // Crash OK
+  return SuccessOrCounterExample(*counter_example);
 }
 
 bool AnalysisEngine::ProgramForwardsAnyPacket(const Policy& program,

diff --git a/netkat/analysis_engine.h b/netkat/analysis_engine.h
@@ -21,6 +21,7 @@
 #ifndef GOOGLE_NETKAT_NETKAT_ANALYSIS_ENGINE_H_
 #define GOOGLE_NETKAT_NETKAT_ANALYSIS_ENGINE_H_
 
+#include "netkat/counter_example.h"
 #include "netkat/frontend.h"
 #include "netkat/packet_transformer.h"
 
@@ -49,7 +50,22 @@ class AnalysisEngine {
   // Checks whether two policies are "equivalent", meaning they have the same
   // packets transformations, meaning Evaluate(left, packet) == Evaluate(right,
   // packet) for all packets.
-  bool CheckEquivalent(const Policy& left, const Policy& right);
+  //
+  // Returns a counter example (i.e. an object demonstrating the difference
+  // between the two policies) for the given `left` and `right` policies if the
+  // policies are not equivalent, or `Success` if the policies are equivalent.
+  //
+  // Example:
+  //   SuccessOrCounterExample result = CheckEquivalent(l,r);
+  //   if(!result.IsSuccess()) {
+  //     CounterExample counter_example = result->GetCounterExampleOrDie();
+  //     ASSIGN_OR_RETURN(Packet input_from_left_but_not_right,
+  //            counter_example.GetInputPacketInLeftButNotRight());
+  //     ...
+  //   }
+  //
+  SuccessOrCounterExample CheckEquivalent(const Policy& left,
+                                          const Policy& right);
 
   // Returns whether any given packet, represented by the set of packets in
   // `packets`, is forwarded by `program`. A packet is considered "forwaded" if

diff --git a/netkat/analysis_engine_test.cc b/netkat/analysis_engine_test.cc
@@ -60,45 +60,54 @@ TEST(AnalysisEngineTest, CheckEquivalentSmokeTests) {
 TEST(AnalysisEngineTest, CheckPolicyEquivalentSmokeTests) {
   AnalysisEngine analyzer;
   // Checks Deny and Accept are equivalent to themselves but not each other.
-  EXPECT_TRUE(analyzer.CheckEquivalent(Policy::Deny(), Policy::Deny()));
-  EXPECT_TRUE(analyzer.CheckEquivalent(Policy::Accept(), Policy::Accept()));
-  EXPECT_FALSE(analyzer.CheckEquivalent(Policy::Accept(), Policy::Deny()));
-  EXPECT_FALSE(analyzer.CheckEquivalent(Policy::Deny(), Policy::Accept()));
+  EXPECT_TRUE(
+      analyzer.CheckEquivalent(Policy::Deny(), Policy::Deny()).IsSuccess());
+  EXPECT_TRUE(
+      analyzer.CheckEquivalent(Policy::Accept(), Policy::Accept()).IsSuccess());
+  EXPECT_FALSE(
+      analyzer.CheckEquivalent(Policy::Accept(), Policy::Deny()).IsSuccess());
+  EXPECT_FALSE(
+      analyzer.CheckEquivalent(Policy::Deny(), Policy::Accept()).IsSuccess());
 
   // Checks different policies are equivalent to themselves but are not
   // equivalent to each other.
   const Policy p1 = Sequence(Filter(Match("port", 10)), Modify("port", 20));
   const Policy p2 = Sequence(Filter(Match("switch", 42)), Modify("port", 21));
-  EXPECT_TRUE(analyzer.CheckEquivalent(p1, p1));
-  EXPECT_TRUE(analyzer.CheckEquivalent(p2, p2));
-  EXPECT_FALSE(analyzer.CheckEquivalent(p1, p2));
-  EXPECT_FALSE(analyzer.CheckEquivalent(p2, p1));
+  EXPECT_TRUE(analyzer.CheckEquivalent(p1, p1).IsSuccess());
+  EXPECT_TRUE(analyzer.CheckEquivalent(p2, p2).IsSuccess());
+  EXPECT_FALSE(analyzer.CheckEquivalent(p1, p2).IsSuccess());
+  EXPECT_FALSE(analyzer.CheckEquivalent(p2, p1).IsSuccess());
 
   // Checks Union of Policies are commutative.
-  EXPECT_TRUE(analyzer.CheckEquivalent(Union(p1, p2), Union(p2, p1)));
+  EXPECT_TRUE(
+      analyzer.CheckEquivalent(Union(p1, p2), Union(p2, p1)).IsSuccess());
 
   // Check Union of Policies are associative.
   const Policy p3 = Filter(Match("dst_mac", 30));
-  EXPECT_TRUE(analyzer.CheckEquivalent(Union(p1, Union(p2, p3)),
-                                       Union(Union(p1, p2), p3)));
+  EXPECT_TRUE(
+      analyzer
+          .CheckEquivalent(Union(p1, Union(p2, p3)), Union(Union(p1, p2), p3))
+          .IsSuccess());
 
   // Some Sequence of Policies are not commutative: modifying the same field
   // with different values in different order would result in different
   // policies.
   const Policy modify_port_1 = Modify("port", 10);
   const Policy modify_port_2 = Modify("port", 20);
-  EXPECT_FALSE(
-      analyzer.CheckEquivalent(Sequence(modify_port_1, modify_port_2),
-                               Sequence(modify_port_2, modify_port_1)));
+  EXPECT_FALSE(analyzer
+                   .CheckEquivalent(Sequence(modify_port_1, modify_port_2),
+                                    Sequence(modify_port_2, modify_port_1))
+                   .IsSuccess());
 
   // Sequence(p1, p2) can be equivalent to Sequence(p2, p1) depending
   // on what's p1 and p2: e.g., modifying different fields in different order
   // would result in equivalent policies.
   // This is the PA-MOD-MOD-COMM axiom in the NetKAT paper.
   const Policy modify_dst_mac = Modify("dst_mac", 1);
-  EXPECT_TRUE(
-      analyzer.CheckEquivalent(Sequence(modify_dst_mac, modify_port_1),
-                               Sequence(modify_port_1, modify_dst_mac)));
+  EXPECT_TRUE(analyzer
+                  .CheckEquivalent(Sequence(modify_dst_mac, modify_port_1),
+                                   Sequence(modify_port_1, modify_dst_mac))
+                  .IsSuccess());
 }
 
 // A netkat::Policy representing the given topology
@@ -115,17 +124,21 @@ TEST(AnalysisEngineTest, TopologyTraversalIsAccepted) {
   Policy traverse_topo_from_s1 = Sequence(
       Modify("switch", 1), Iterate(topology), Filter(Match("switch", 3)));
   EXPECT_TRUE(
-      analyzer.CheckEquivalent(traverse_topo_from_s1, Modify("switch", 3)));
+      analyzer.CheckEquivalent(traverse_topo_from_s1, Modify("switch", 3))
+          .IsSuccess());
 
   Policy traverse_topo_from_s2 = Sequence(
       Modify("switch", 2), Iterate(topology), Filter(Match("switch", 3)));
   EXPECT_TRUE(
-      analyzer.CheckEquivalent(traverse_topo_from_s2, Modify("switch", 3)));
+      analyzer.CheckEquivalent(traverse_topo_from_s2, Modify("switch", 3))
+          .IsSuccess());
 
   Policy traverse_from_non_existing_switch = Sequence(
       Modify("switch", 42), Iterate(topology), Filter(Match("switch", 3)));
-  EXPECT_TRUE(analyzer.CheckEquivalent(traverse_from_non_existing_switch,
-                                       Policy::Deny()));
+  EXPECT_TRUE(
+      analyzer
+          .CheckEquivalent(traverse_from_non_existing_switch, Policy::Deny())
+          .IsSuccess());
 }
 
 // TODO(anthonyroy): Consider fuzzing some of these tests. Doing so requires a

diff --git a/netkat/counter_example.cc b/netkat/counter_example.cc
@@ -0,0 +1,105 @@
+// Copyright 2025 The NetKAT authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#include "netkat/counter_example.h"
+
+#include <vector>
+
+#include "absl/log/check.h"
+#include "absl/status/status.h"
+#include "absl/status/statusor.h"
+#include "netkat/evaluator.h"
+#include "netkat/packet_set.h"
+#include "netkat/packet_transformer.h"
+
+namespace netkat {
+
+absl::StatusOr<CounterExample> CounterExample::CreateEquivalenceCounterExample(
+    PacketTransformerHandle left_policy, PacketTransformerHandle right_policy,
+    PacketTransformerManager* packet_transformer_manager) {
+  if (left_policy == right_policy) {
+    return absl::InvalidArgumentError(
+        "Left and right policies are the same, cannot create a counter "
+        "example.");
+  }
+  if (packet_transformer_manager == nullptr) {
+    return absl::InvalidArgumentError(
+        "Packet transformer manager is null, cannot create a counter example.");
+  }
+  return CounterExample(left_policy, right_policy, packet_transformer_manager);
+}
+
+CounterExample::CounterExample(
+    PacketTransformerHandle left_packet_transformer,
+    PacketTransformerHandle right_packet_transformer,
+    PacketTransformerManager* packet_transformer_manager)
+    : left_packet_transformer_(left_packet_transformer),
+      right_packet_transformer_(right_packet_transformer),
+      packet_transformer_manager_(packet_transformer_manager) {
+  // Compute the set of packets that are in L but not R, and vice versa.
+  PacketTransformerHandle left_diff_right_transformer =
+      packet_transformer_manager_->Difference(left_packet_transformer,
+                                              right_packet_transformer);
+  PacketTransformerHandle right_diff_left_transformer =
+      packet_transformer_manager_->Difference(right_packet_transformer,
+                                              left_packet_transformer);
+
+  // Compute the input packet sets to the difference of the left and right
+  // policies and vice versa.
+  PacketSetHandle fullset =
+      packet_transformer_manager_->GetPacketSetManager().FullSet();
+  input_packets_in_left_but_not_right_ =
+      packet_transformer_manager_->Pull(left_diff_right_transformer, fullset);
+  input_packets_in_right_but_not_left_ =
+      packet_transformer_manager_->Pull(right_diff_left_transformer, fullset);
+}
+
+PacketTransformerHandle CounterExample::GetLeftTransformer() const {
+  return left_packet_transformer_;
+}
+PacketTransformerHandle CounterExample::GetRightTransformer() const {
+  return right_packet_transformer_;
+}
+
+absl::StatusOr<Packet> CounterExample::GetInputPacketInLeftButNotRight() const {
+  if (packet_transformer_manager_ == nullptr) {
+    return absl::InvalidArgumentError(
+        "Packet transformer manager is null, cannot get input packets in left "
+        "but not right.");
+  }
+  std::vector<Packet> input_packets =
+      packet_transformer_manager_->GetPacketSetManager().GetConcretePackets(
+          input_packets_in_left_but_not_right_);
+  if (input_packets.empty()) {
+    return absl::NotFoundError("No input packets in left but not right found.");
+  }
+  return input_packets[0];
+}
+
+absl::StatusOr<Packet> CounterExample::GetInputPacketInRightButNotLeft() const {
+  if (packet_transformer_manager_ == nullptr) {
+    return absl::InvalidArgumentError(
+        "Packet transformer manager is null, cannot get input packets in right "
+        "but not left.");
+  }
+  std::vector<Packet> input_packets =
+      packet_transformer_manager_->GetPacketSetManager().GetConcretePackets(
+          input_packets_in_right_but_not_left_);
+  if (input_packets.empty()) {
+    return absl::NotFoundError("No input packets in right but not left found.");
+  }
+  return input_packets[0];
+}
+
+}  // namespace netkat